# INDUCTIVE SPACES

```
def B: U := W (x: + ℕ ℕ), +-rec ℕ ℕ (λ (f: + ℕ ℕ), U) 𝟎 𝟏×𝟏 x
def L (A: U): U := W (x: M A), M-rec A U 𝟎 (λ (a: A), 𝟏) x
def N: U := W (x: 𝟐), ind₂ (λ (f: 𝟐), U) 𝟎 𝟏 x
def M (A: U): U := Σ (x: 𝟐), ind₂ (λ (f: 𝟐), U) 𝟏 A x
def + (A B: U): U := Σ (x: 𝟐), ind₂ (λ (f: 𝟐), U) A B x
def V (A: U₁): ℕ → U := ℕ-iter U 𝟏 (λ (X: U), A × X)
def F: ℕ → U := ℕ-iter U 𝟎 (+ 𝟏)
```

For multiple
occurance of fixpoint variable in W-fiber encoded
argument use

```
def List (A: U)
: Π (w : M A), U
:= λ (w : M A),
ind₂ (λ (x: 𝟐),
Π (u: ind₂ (λ (x: 𝟐), U) 𝟏 A x), U)
(ind₁ (λ (x: 𝟏), U) 𝟎)
(λ (a: A), 𝟏) w.1 w.2
```

# 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

there is a dependent function:

```
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))
```

## Uniqueness

# 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

## Uniqueness

# 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`