RulesForTheStandardSetFormers

Martin-Löf type theory

We present the intensional version of Martin-Löf type theory from 1986, see Nordström, Petersson, and Smith 1989. (It is not exactly the same theory since Agda has A -> B : Set provided A, B : Set, whereas this is not the case in Martin-Löf's logical framework.) Identifiers are similar to those in Martin-Löf's Bibliopolis book.

The empty set and the unit set:

 module MLTT.Sets where

 data N₀ : Set where

 R₀ : {C : N₀ -> Set} -> (c : N₀) -> C c
 R₀ ()

 data  N₁ : Set where
   0₁ : N₁

 R₁ : {C : N₁ -> Set} -> C 0₁ -> (c : N₁) -> C c
 R₁ d 0₁ = d

In Martin-Löf's presentation there is a countable family of finite sets, but each of these can be defined as disjoint unions of unit sets.

The disjoint union (sum) of two sets:

 data _+_ (A B : Set) : Set where
   i : A -> A + B
   j : B -> A + B

 D : {A B : Set} -> {C : A + B -> Set}
   -> ((a : A) -> C (i a)) -> ((b : B) -> C (j b)) -> (c : A + B) -> C c
 D d e (i a) = d a
 D d e (j b) = e b

The disjoint union of a family of sets:

 data Σ (A : Set) (B : A -> Set) : Set where
   _,_ : (a : A) -> B a -> Σ A B

 E : {A : Set} -> {B : A -> Set} -> {C : Σ A B -> Set}
   -> ((x : A) -> (y : B x) -> C (x , y))
   -> (z : Σ A B) -> C z
 E d (x , y) = d x y

In intensional type theory E (split) is not derivable from the projections, hence it is taken as a primitive.

 data Π (A : Set) (B : A -> Set) : Set where
   Λ : ((a : A) -> B a) -> Π A B

 F :  {A : Set} -> {B : A -> Set} -> {C : Π A B -> Set}
   -> ((b : (x : A) -> B x) -> C (Λ b))
   -> (z : Π A B) -> C z
 F d (Λ b) = d b

In intensional type theory F (funsplit) is more general than application and hence taken as a primitive

In the Agda version of Martin-Löf type theory, the framework function space (x : A) -> B x more or less replaces Π A B.

The natural numbers:

 data N : Set where
   O : N
   s : N -> N

 R : {C : N -> Set} -> C O -> ((n : N) -> C n -> C (s n)) -> (c : N) -> C c
 R d e O = d
 R d e (s n) = e n (R d e n)

The well-orderings:

 data W (A : Set) (B : A -> Set) : Set where
   sup : (a : A) -> (b : B a -> W A B) -> W A B

 wrec : {A : Set} -> {B : A -> Set} -> {C : W A B -> Set}
      -> ((a : A) -> (b : B a -> W A B) -> ((x : B a) -> C (b x)) -> C (sup a b))
      -> (c : W A B) -> C c
 wrec {C = C} d (sup a b) = d a b (\x -> wrec {C = C} d (b x))

The identity set:

 data I (A : Set) : A -> A -> Set where
   r : {a : A} -> I A a a

 J : {A : Set} -> {a b : A} -> {C : (x y : A) -> (z : I A x y) -> Set}
   -> ({x : A} -> C x x r)
   -> (c : I A a b) -> C a b c
 J d r = d

The first universe a la Tarski:

 mutual
  data U : Set where
     n₀ : U
     n₁ : U
     _⊕_ : U -> U -> U
     σ : (a : U) -> (T a -> U) -> U
     π : (a : U) -> (T a -> U) -> U
     n : U
     w : (a : U) -> (T a -> U) -> U
     i : (a : U) -> T a -> T a -> U

  T : U -> Set
  T n₀        = N₀
  T n₁        = N₁
  T (a ⊕ b)   = T a + T b
  T (σ a b)   = Σ (T a) (\x -> T (b x))
  T (π a b)   = Π (T a) (\x -> T (b x))
  T n         = N
  T (w a b)   = W (T a) (\x -> T (b x))
  T (i a b c) = I (T a) b c

Note that this is a mutual inductive-recursive definition of U and T which is included in a mutual block.