Types and terms¶
Functions (dependent products)¶
Function (dependent product) types \(\prod_{x : A} B\) are written (x : A) -> B x. Values of function types are \(\lambda\)-abstractions written in one of the following ways:
\x -> <body>— this is usually fine;\(x : A) -> <body>— this sometimes helps the typechecker.
Dependent sums¶
Dependent sum type \(\sum_{x : A} B\) is written ∑ (x : A), B or Sigma (x : A), B. Values of dependent sum types are pairs written as (x, y).
To access components of a dependent pair p, use first p and second p.
Warning
first and second are not valid syntax without an argument!
Identity types¶
Identity (path) type \(x =_A y\) is written x =_{A} y.
Tip
Specifying the type A is optional: x = y is valid syntax!
Any identity type has value refl_{x : A} whose type is x =_{A} x whenever x : A
Tip
Specifying term and type of refl_{x : A} is optional: refl_{x} and refl are both valid syntax.
Path induction is done using \(\mathcal{J}\) path eliminator:
- for
- any type \(A\) and \(a : A\),
- type family \(C : \prod_{x : A} ((a =_A x) \to \mathcal{U})\) and
- \(d : C(a,\mathsf{refl}_a)\) and
- \(x : A\) and \(p : a =_A x\)
- we have \(\mathcal{J}(A, a, C, d, x, p) : C(x, p)\)
In rzk-1 we write idJ(A, a, C, d, x, p)
Warning
idJ is not valid syntax without exactly 6-tuple provided as an argument!