Types and terms¶

#lang rzk-1

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!

Let bindings¶

Local definitions are written let x := val in body and can carry an optional type annotation let x : A := val in body. The bound name is in scope in body only.

#def example-let
  : Unit
  :=
  let x := unit in
  let y : Unit := x in
  y

Patterns are supported in the binder, so you can destructure a pair directly:

#def example-let-pair
  : Unit
  :=
  let (a , b) := (unit , unit) in
  a

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!