# Rules For The Standard Set Formers

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.