A.1.2 Dependent function types (Π-types)

We introduce a primitive constant cΠ, but write cΠ(A,λx.B) as (x:A)B. Judgments concerning such expressions and expressions of the form λx.b are introduced by the following rules:

  • if ΓA:𝒰n and Γ,x:AB:𝒰n, then Γ(x:A)B:𝒰n

  • if Γ,x:Ab:B then Γ(λx.b):((x:A)B)

  • if Γg:(x:A)B and Γt:A then Γg(t):B[t/x]

If x does not occur freely in B, we abbreviate (x:A)B as the non-dependent function type AB and derive the following rule:

  • if Γg:AB and Γt:A then Γg(t):B

Using non-dependent function types and leaving implicit the context Γ, the rules above can be written in the following alternative style that we use in the rest of this section of the appendix.

  • if A:𝒰n and B:A𝒰n, then (x:A)B(x):𝒰n

  • if x:Ab:B then λx.b:(x:A)B(x)

  • if g:(x:A)B(x) and t:A then g(t):B(t)

Title A.1.2 Dependent function types (Π-types)