This is how it works in Yatima. Since we use self-types and lambda-encodings for our datatypes, all type expressions are built up via some combination of self types, pi types and a few type-level constants (like primitives).
For example, the type of booleans can be expressed as:
def Bool : Type =
@self ∀
(0 P : ∀ (Bool) -> Type)
(& true : P (data λ P t f => t))
(& false : P (data λ P t f => f))
-> P self
def true : Bool = data λ P t f => t
def false : Bool = data λ P t f => f