INDUCTIVE

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

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

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

(). false or .

(). true or .

Elimination

(Induction Principle ).

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