# INDUCTIVE BASIS

These types form the inductive basis of MLTT foundations and are built-in into type checker.

# EMPTY

The Empty type represents False-type logical π, type without inhabitants, Void or β₯ (Bottom). As it has not inhabitants it lacks both constructors and eliminators, however, it has induction.

## Formation

## Elimination

```
def Empty-ind (C: π β U) (z: π) : C z := indβ (C z) z
```

```
def isEmpty (A: U): U := A β π
```

The witness of

# UNIT

Unit type is the simplest type equipped with full set of MLTT inference rules. It contains single inhabitant β (star).

## Formation

## Introduction

## Elimination

```
def 1-ind (C: π β U) (x: C β
) (z: π) : C z := indβ C x z
```

## Computation

# BOOL

π is a logical boolean type or 0-sphere which has two
inhabitants false (or

## Formation

## Introduction

## Elimination

`def 2-ind (C: π β U) (x: C 0β) (y: C 1β) (z: π) : C z := indβ C x y z`

# W

Well-founded trees without mutual recursion represented as

## Formation

```
def W' (A : U) (B : A β U) : U := W (x : A), B x
```

## Introduction

```
def sup' (A: U) (B: A β U) (x: A) (f: B x β W' A B)
: W' A B
:= sup A B x f
```

## Elimination

```
def W-ind (A : U) (B : A β U)
(C : (W (x : A), B x) β U)
(g : Ξ (x : A) (f : B x β (W (x : A), B x)), (Ξ (b : B x), C (f b)) β C (sup A B x f))
(a : A) (f : B a β (W (x : A), B x)) (b : B a) : C (f b) := indα΅ A B C g (f b)
```

## Computation

```
def indα΅-Ξ² (A : U) (B : A β U)
(C : (W (x : A), B x) β U) (g : Ξ (x : A)
(f : B x β (W (x : A), B x)), (Ξ (b : B x), C (f b)) β C (sup A B x f))
(a : A) (f : B a β (W (x : A), B x))
: PathP (<_> C (sup A B a f))
(indα΅ A B C g (sup A B a f))
(g a f (Ξ» (b : B a), indα΅ A B C g (f b)))
:= <_> g a f (Ξ» (b : B a), indα΅ A B C g (f b))
```