Dependent types

In this file we will look at Rzk primitives to work with dependent types.

Reference material

This page is mostly based on the introduction of dependent types in the HoTT Book (Sections 1.2–1.6), immediately introducing corresponding formalizations in Rzk and noting some differences.

This is a literate Rzk file:

#lang rzk-1

Functions

The type (x : A) → B x is the type of (dependent) functions with an argument of type A and, for each input x, the output type B x.

As a simple example of a dependent function, consider the identity function:

#define identity
  : ( A : U) → (x : A) → A
  := \ A x → x

Since we are not using x in the type of identity, we can simply write the type of the argument, without providing its name:

#define identity₁
  : ( A : U) → A → A
  := \ A x → x

We can write this definition differently, by putting (A : U) into parameters (before :), and omitting it in the lambda abstraction:

#define identity₂
  ( A : U)
  : A → A
  := \ x → x

We could also move x into parameters as well, although this probably does not increase readability anymore:

#define identity₃
  ( A : U)
  ( x : A)
  : A
  := x

Another, less trivial example of a dependent function is the one that swaps the arguments of another function:

#define swap
  ( A B C : U)
  : ( A → B → C) → (B → A → C)
  := \ f → \ b a → f a b

Product types

Rzk does not have built-in product types, since they are a special case of Σ-types, which we will discuss soon. For now, we give definition of product types:

#define prod
  ( A B : U)
  : U
  := Σ (_ : A) , B

The type prod A B corresponds to the product type \(A \times B\). The Unit type corresponds to the type \(\mathbf{1}\).

The intended elements of prod A B are only pairs (a, b) : prod A B where a : A and b : B. Similarly, intended element of Unit is only unit. However, formally, this is not immediately true and instead is a theorem that we can prove.

Remark on type formers

Formally, we have the following constituents of the definition for product types and function types (for comparison):

1. Type formation:

   • prod A B is a type whenever A and B are types
   • A → B is a type whenever A and B are types

2. Constructors (introduction rules):

   • (x , y) is a term of type prod A B whenever x : A and y : B
   • \ x → y is a term of type A → B whenever for any x : A we have y : B

3. Eliminators (elimination rules):

   • Given z : prod A B, we can project the first and second components:
   • first z : A and second z : B

   • it is also possible to pattern match (deconstruct) in a function argument or when introducing a parameter, e.g.

     #define swap-prod₁
       ( A B : U)
       : prod A B → prod B A
       := \ (x , y) → (y , x)
     
     #define swap-prod₂
       ( A B : U)
       ( (x , y) : prod A B)
       : prod B A
       := ( y , x)
     

   • more generally, eliminators come in a form of an induction principle, which we will discuss below and can be defined in Rzk in terms of pattern matching or first and second:

     #define ind-prod
       ( A B : U)
       ( C : prod A B → U)
       ( f : (a : A) → (b : B) → C (a , b))
       : (z : prod A B) → C z
       := \ (a , b) → f a b
     

   • Given f : A → B, we can apply it to an argument of type a : A:

   • f a : B

   Built-in eliminators in Rzk

   Built-in eliminators in Rzk need to be always fully applied (e.g. first without an argument is invalid syntax!). Technically, this corresponds with the "second presentation" of type theory in Appendix A.2 of the HoTT Book. In practice, this is not always convenient for users, as we often want to curry some of these built-ins, so wrapper functions are introduced (by users), for example:

   #define pr₁
     ( A B : U)
     : prod A B → A
     := \ p → first p
   

4. Computation rules:

   • Projecting from a pair is computed as follows for any x : A and y : B:
   • first (x , y) ≡ x
   • second (x , y) ≡ y
   • Applying an lambda abstraction is computed by substituting the argument into a body:
   • (\ x → y) a ≡ y{x ↦ a} when a : A and for all x : A, y : B.

5. Uniqueness principle (optional):

   • For any z : prod A B, we have z ≡ (first z, second z)
   • This holds definitionally for product types and Σ-types in Rzk, but is provable in a weaker (propositional) form in HoTT Book
   • For any function f : A → B, we have f ≡ \ x → f x

Recursion principle

Following the HoTT Book, for each type former we can formalize its recursion principle. A recursion principle for type T is a function that allows to produce a result of arbitrary type C from a value of type T:

#define rec-T
  ( C : U)
  -- ... (parameters to the recursion principle)
  : T → C

For example, for the product type prod A B, recursion principle looks like this:

#define rec-prod
  ( A B : U)
  ( C : U)
  ( f : A → B → C)
  : prod A B → C
  := \ (a , b) → f a b

For the Unit type, recursion principle is trivial:

#define rec-Unit
  ( C : U)
  ( c : C)
  : Unit → C
  := \ unit → c

Induction principle

To define a dependent function out of a type, we use its induction principle, which can be seen as a dependent version of the recursion principle. An induction principle for type T is a function that allows to produce a result of arbitrary type C z from a value z : T:

#define ind-T
  ( C : T → U)
  -- ... (parameters to the induction principle)
  : (z : T) → C z

For example, for the product type prod A B, induction principle looks like this:

#define ind-prod
  ( A B : U)
  ( C : prod A B → U)
  ( f : (a : A) → (b : B) → C (a , b))
  : ( z : prod A B) → C z
  := \ (a , b) → f a b

We can use ind-prod to prove the uniqueness principle for products. Here we use the identity type, which we will cover later, but for now it is sufficient to know that there is always an element refl_{x} : x =_{A} x for any x : A.

#define uniq-prod
  ( A B : U)
  ( z : prod A B)
  : ( first z , second z) =_{prod A B} z
  := ind-prod A B
      ( \ z' → (first z' , second z') =_{prod A B} z') -- C
      ( \ a b → refl_{(a , b)})
        -- C (a, b)
        -- ≡ ( \ z' → (first z', second z') =_{prod A B} z') (a, b)
        -- ≡ (first (a, b), second (a, b)) =_{prod A B} (a, b)
        -- ≡ (a, second (a, b)) =_{prod A B} (a, b)
        -- ≡ (a, b) =_{prod A B} (a, b)
      z

Since in Rzk the uniqueness principle is builtin, a simpler proof also works:

#define uniq-prod'
  ( A B : U)
  ( z : prod A B)
  : ( first z , second z) =_{prod A B} z
  := refl_{z} -- works in Rzk, not in HoTT Book, since in Rzk we have (first z, second z) ≡ z

For the Unit type, induction principle is trivial:

#define ind-Unit
  ( C : Unit → U)
  ( c : C unit)
  : ( z : Unit) → C z
  := \ unit → c

Unlike rec-Unit, induction principle for Unit is not useless, since it allows, for example, to prove the uniqueness principle:

#define uniq-Unit
  ( z : Unit)
  : unit =_{Unit} z
  := ind-Unit
      ( \ z' → unit =_{Unit} z')
      ( refl_{unit})
      z

Again, since Rzk has a builtin uniqueness principle for Unit, a simpler proof also works:

#define uniq-Unit'
  ( z : Unit)
  : unit =_{Unit} z
  := refl_{z} -- works in Rzk, not in HoTT Book, since in Rzk we have unit ≡ z

Dependent pair types (Σ-types)

A straightforward generalization of product types to dependent pairs Σ (a : A), B a where A is a type and B : A → U is a type family indexed in A.

The indended values of Σ (a : A), B a are pairs (a , b) of terms a : A and b : B a. Note that the type of the second component may depend on the value of the first component. When the type family B is constant, e.g. (\ _ → C), then Σ (a : A), B a becomes exactly the product type prod A C.

To eliminate dependent pairs, we use first, second, or pattern matching on pairs. However, the types of projections are less obvious compared to the case of product types.

Projections

The first projection can be easily defined in terms of pattern matching:

#define pr₁
  ( A : U)
  ( B : A → U)
  : ( Σ ( a : A) , B a) → A
  := \ (a , _) → a

However, second projection requires some care. For instance, we might try this:

-- NOTE: incorrect definition
#define pr₂
  ( A : U)
  ( B : A → U)
  : (Σ (a : A), B a) → B a  -- ERROR!
  := \ (_ , b) → b

undefined variable: a

We get the undefined variable error since a is not visible outside of Σ-type definition. To access it, we need a dependent function:

#define pr₂
  ( A : U)
  ( B : A → U)
  : ( z : Σ (a : A) , B a) → B (pr₁ A B z)
  := \ (_ , b) → b

In Rzk, it is sometimes more convenient to talk about Σ-types as "total" types (as in "total spaces"):

#define total-type
  ( A : U)
  ( B : A → U)
  : U
  := Σ (a : A) , B a

We can use pattern matching in the function type and this new definition to write second projection slightly differently:

#define pr₂'
  ( A : U)
  ( B : A → U)
  ( ( a , b) : total-type A B)
  : B a
  := b

Recursion and induction principles

The recursion principle for Σ-types is a simple generalization of the recursion principle for product types:

#define rec-Σ
  ( A : U)
  ( B : A → U)
  ( C : U)
  ( f : (a : A) → B a → C)
  : total-type A B → C
  := \ (a , b) → f a b

The induction principle is, again, a generalization of the recursion principle to dependent types:

#define ind-Σ
  ( A : U)
  ( B : A → U)
  ( C : total-type A B → U)
  ( f : (a : A) → (b : B a) → C (a , b))
  : ( z : total-type A B) → C z
  := \ (a , b) → f a b

As before, using ind-Σ we may prove the uniqueness principle, now for Σ-types:

#define uniq-Σ
  ( A : U)
  ( B : A → U)
  ( z : total-type A B)
  : ( pr₁ A B z , pr₂ A B z) =_{total-type A B} z
  := ind-Σ A B
      ( \ z → (pr₁ A B z , pr₂ A B z) =_{total-type A B} z)
      ( \ a b → refl_{(a , b)})
      z

And again, Rzk can accept a simpler proof, since uniqueness for Σ-types is already built into it:

#define uniq-Σ'
  ( A : U)
  ( B : A → U)
  ( z : total-type A B)
  : ( pr₁ A B z , pr₂ A B z) =_{total-type A B} z
  := refl_{z} -- works in Rzk, but not in HoTT Book

Type-theoretic "axiom" of choice

Using ind-Σ we can also prove a type-theoretic axiom of choice:

#define AxiomOfChoice
  : U
  := (A : U)
    → ( B : U)
    → ( R : A → B → U)
    → ( ( x : A) → Σ (y : B) , R x y)
    → ( Σ ( f : A → B) , (x : A) → R x (f x))

You are encouraged to try proving this yourself first.

If you encounter problems, try looking for the proof in the HoTT Book Section 1.6 (page 32).

If you still have issues formalizing it in Rzk, you may peek here:

Proof of the type theoretic axiom of choice

#define ac : AxiomOfChoice
  := \ A B R g → ( \ a → first (g a) , \ x → second (g x))
  -- g    : (x : A) → Σ (y : B), R x y
  -- x    : A
  -- g x  : Σ (y : B), R x y
  -- second (g x) : R x (first (g x))

  -- f : A → B
  -- f := \ a → first (g a)
  --
  -- R x (f x)
  -- == R x ((\ a → first (g a)) x)
  -- == R x (first (g x))

Coproducts

Given types \(A\) and \(B\) a coproduct type \(A + B\) corresponds intuitively to a disjoint union of \(A\) and \(B\) (in set theory). We also have a nullary version: \(\mathbf{0}\) (empty type).

In Rzk, the empty type and coproduct types are declared as inductive types with the #data command.

The empty type

The empty type is an inductive type with no constructors:

#data Void

The declaration generates the induction principle ind-Void and its non-dependent version rec-Void:

#check ind-Void : (C : Void → U) → (z : Void) → C z
#check rec-Void : (C : U) → Void → C

Since there are no values of type Void, the induction principle corresponds to the principle that from falsehood anything follows.

The coproduct type

The coproduct is an inductive type with two constructors — one injecting a term from A and one injecting a term of B:

#data coprod
  ( A B : U)
  :=
    inl (a : A)
  | inr (b : B)

To eliminate a coproduct, the generated induction principle asks for two handlers — one for the left case and one for the right:

#check ind-coprod
  : ( A : U) → (B : U)
  → ( C : coprod A B → U)
  → ( ( a : A) → C (inl A B a))
  → ( ( b : B) → C (inr A B b))
  → ( z : coprod A B) → C z

The computation rules are definitional: ind-coprod A B C l r (inl A B a) computes to l a automatically, with no explicit rewriting. For example, the following holds by refl:

#define compute-ind-coprod-inl
  ( A B : U)
  ( C : coprod A B → U)
  ( l : (a : A) → C (inl A B a))
  ( r : (b : B) → C (inr A B b))
  ( a : A)
  : ind-coprod A B C l r (inl A B a) = l a
  := refl

Recursion for coproducts is the generated non-dependent version:

#check rec-coprod
  : ( A : U) → (B : U)
  → ( C : U)
  → ( ( a : A) → C)
  → ( ( b : B) → C)
  → coprod A B → C

The uniqueness principle for coproducts says that any coproduct is either an inl or an inr. Proving the uniqueness is fairly straightforward, except we have to provide some intermediate types explicitly:

#define uniq-coprod
  ( A B : U)
  ( z : coprod A B)
  : coprod
      ( Σ ( a : A) , inl A B a = z)
      ( Σ ( b : B) , inr A B b = z)
  := ind-coprod A B
      ( \ z' → coprod
          ( Σ ( a : A) , inl A B a = z')
          ( Σ ( b : B) , inr A B b = z'))
      ( \ a' → inl
          ( Σ ( a : A) , (inl A B a = inl A B a'))
          ( Σ ( b : B) , (inr A B b = inl A B a'))
          ( a' , refl))
      ( \ b' → inr
          ( Σ ( a : A) , (inl A B a = inr A B b'))
          ( Σ ( b : B) , (inr A B b = inr A B b'))
          ( b' , refl))
      z

Booleans

The booleans are an inductive type with two constructors and no fields:

#data Bool := false | true

The generated induction and recursion principles have the expected types:

#check ind-Bool
  : ( C : Bool → U)
  → C false
  → C true
  → ( z : Bool) → C z

#check rec-Bool : (C : U) → C → C → Bool → C

#define uniq-Bool
  ( z : Bool)
  : coprod (z = false) (z = true)
  := ind-Bool
      ( \ z' → coprod (z' = false) (z' = true))
      ( inl (false = false) (false = true) refl)
      ( inr (true = false) (true = true) refl)
      z

#define not
  : Bool → Bool
  := rec-Bool Bool true false

Since the computation rules of an inductive type are definitional, not (not false) computes to false and not (not true) to true, and the following proof goes through by induction with two refl cases:

#define not-not-is-identity
  : ( z : Bool) → not (not z) = z
  := ind-Bool
      ( \ z → not (not z) = z)
      ( refl)
      ( refl)

Inductive types and the simplicial structure

An inductive type comes with exactly its induction principle. How the type interacts with the simplicial structure of Rzk is a separate matter, and generally not derivable. In particular, the induction principle of Bool does not prove that Bool is discrete: discreteness of Bool is equivalent to the assumption that there merely exists a type with two points not connected by an arrow, and the unaugmented theory cannot prove this assumption. Thus a user who wants Bool discrete must still assume a disconnectedness principle; declaring #data Bool proves nothing new about 2 → Bool.

Natural numbers

The natural numbers are a recursive inductive type: the succ constructor stores a natural number. The generated induction principle provides an induction hypothesis for the recursive field:

#data ℕ := zero | succ (n : ℕ)

#check ind-ℕ
  : ( C : ℕ → U)
  → C zero
  → ( ( n : ℕ) → C n → C (succ n))
  → ( n : ℕ) → C n

#check rec-ℕ : (C : U) → C → ((n : ℕ) → C → C) → ℕ → C

#define double-ℕ
  : ℕ → ℕ
  := rec-ℕ ℕ zero (\ _ m → succ (succ m))

Since the computation rules are definitional, doubling a numeral computes, and the result can be checked with refl:

#define double-two
  : double-ℕ (succ (succ zero)) =_{ℕ} succ (succ (succ (succ zero)))
  := refl