INDUCTIVE SPACES

form the inductive base for well-founded spaces of MLTT-80 that allow to manipulate F-algebras. For coinductive streams (G-coalgebras) one may need spaces with reversed intro-elim rules.

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 cartesian product, like for binary trees 𝟏 × 𝟏. Here is example for List MLTT encoding:

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 -types.

Formation

(-Formation). For and , type is defined as or

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

Introduction

(-Introduction). Elements of are called well-founded trees and created with single constructor:

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

Elimination

(Induction Principle ). The induction principle states that for any types and and type family over and the function , where

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

( computes). The induction principle satisfies the equation:

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

(-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

(Empty). Empty-type is defined as built-in 𝟎-type:

Elimination

(Induction Principle ). 𝟎-type is satisfying the induction principle:

def Empty-ind (C: 𝟎 → U) (z: 𝟎) : C z := ind₀ (C z) z

(Negation or isEmpty). For any type A negation of A is defined as arrow from A to 𝟎:

def isEmpty (A: U): U := A → 𝟎

The witness of is obtained by assuming A and deriving a contradiction. This techniques is called proof of negation and is applicable to any types in constrast to proof by contradiction which implies (double negation elimination) and is applicable only to decidable types with property.

UNIT

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

Formation

(Unit). Unit-type is defined as built-in 𝟏-type:

Introduction

(Star). 𝟏-type containts single inhabitant ★:

Elimination

. (Induction Principle ). 𝟏-type satisfies induction principle that for any family indexed by there is a function

def 1-ind (C: 𝟏 → U) (x: C ★) (z: 𝟏) : C z := ind₁ C x z

Computation

(Unit Computes). The following equation holds:

Uniqueness

(Unit Unique).

BOOL

𝟐 is a logical boolean type or 0-sphere which has two inhabitants false (or ) and true (or ).

Formation

(Bool). Boolean-type or 0-sphere is defined as built-in 𝟐-type:

Introduction

(Bool Constructors and ). or and or .

Elimination

(Induction Principle ).

def 2-ind (C: 𝟐 → U) (x: C 0₂) (y: C 1₂) (z: 𝟐) : C z := ind₂ C x y z