Skip to content
Cella Lang

hlevel

isTrunc

Section titled “isTrunc”
def isTrunc (n : Nat) (A : Type) : Type

The truncation level predicate: level 0 is contractibility, and level n+1 means every path space is of level n.

isTruncMap

Section titled “isTruncMap”
def isTruncMap (n : Nat) (A : Type) (B : Type) (f : A -> B) : Type

A map is n-truncated when every one of its fibers is of truncation level n.

isTrunc0_is_isContr

Section titled “isTrunc0_is_isContr”
def isTrunc0_is_isContr (A : Type) (h : isTrunc zero A) : isContr A

A type of truncation level 0 is contractible (the two notions agree definitionally).

isContr_is_isTrunc0

Section titled “isContr_is_isTrunc0”
def isContr_is_isTrunc0 (A : Type) (h : isContr A) : isTrunc zero A

A contractible type has truncation level 0 (the two notions agree definitionally).

isProp_to_isTrunc1

Section titled “isProp_to_isTrunc1”
def isProp_to_isTrunc1 (A : Type) (h : isProp A) : isTrunc (succ zero) A

A proposition has truncation level 1: all its path spaces are contractible.

isTrunc1_to_isProp

Section titled “isTrunc1_to_isProp”
def isTrunc1_to_isProp (A : Type) (h : isTrunc (succ zero) A) : isProp A

A type of truncation level 1 is a proposition, taking the center of each path space.

isSet_to_isTrunc2

Section titled “isSet_to_isTrunc2”
def isSet_to_isTrunc2 (A : Type) (h : isSet A) : isTrunc (succ (succ zero)) A

A set has truncation level 2: its path spaces are propositions.

isTrunc2_to_isSet

Section titled “isTrunc2_to_isSet”
def isTrunc2_to_isSet (A : Type) (h : isTrunc (succ (succ zero)) A) : isSet A

A type of truncation level 2 is a set.

isContr_to_isTrunc1

Section titled “isContr_to_isTrunc1”
def isContr_to_isTrunc1 (A : Type) (h : isContr A) : isTrunc (succ zero) A

A contractible type has truncation level 1.

isSetUnit

Section titled “isSetUnit”
def isSetUnit : isSet Unit

Unit is a set.

constPath

Section titled “constPath”
def constPath {A : Type} {x : A} {y : A} (d : Dec (x ≡ y)) (r : x ≡ y) : x ≡ y

Turns a decision on x ≡ y into an endofunction on x ≡ y that returns the decided path whenever one exists.

constPathConst

Section titled “constPathConst”
def constPathConst {A : Type} {x : A} {y : A} (d : Dec (x ≡ y)) (p : x ≡ y) (q : x ≡ y) : constPath d p ≡ constPath d q

The endofunction constPath is constant: it sends any two paths to the same path.

decPathFn

Section titled “decPathFn”
def decPathFn {A : Type} (dec : isDiscrete A) (x : A) (z : A) (r : x ≡ z) : x ≡ z

For a discrete type, the constant endofunction on paths from x to z obtained from deciding x ≡ z.

hedbergMotive

Section titled “hedbergMotive”
def hedbergMotive {A : Type} (dec : isDiscrete A) (x : A) (z : A) (r : x ≡ z) : Type

Motive for Hedberg’s theorem: a path r equals its image under decPathFn, corrected by the image of refl.

hedbergKey

Section titled “hedbergKey”
def hedbergKey {A : Type} (dec : isDiscrete A) (x : A) {y : A} (p : x ≡ y) : hedbergMotive dec x y p

Every path from x is recovered from its decPathFn image, the key step of Hedberg’s theorem.

hedberg

Section titled “hedberg”
def hedberg {A : Type} (dec : isDiscrete A) : isSet A

Hedberg’s theorem: a type with decidable path equality is a set.

DecEq.toDiscrete

Section titled “DecEq.toDiscrete”
def DecEq.toDiscrete {A : Type} (d : DecEq A) : isDiscrete A

Turns decidable core equality into decidable paths, so Hedberg’s theorem applies.

DecEq.uip

Section titled “DecEq.uip”
def DecEq.uip {A : Type} (d : DecEq A) (x : A) (y : A) (a : x = y) (b : x = y) : a = b

Uniqueness of identity proofs for a type with decidable equality: any two proofs of x = y are equal.

isSetBool

Section titled “isSetBool”
def isSetBool : isSet Bool

Bool is a set, proved by Hedberg’s theorem from decidable equality.

isPropFunToProp

Section titled “isPropFunToProp”
def isPropFunToProp (A : Type) (B : Type) (hb : isProp B) : isProp (A -> B)

Functions into a proposition form a proposition.

isPropProdProp

Section titled “isPropProdProp”
def isPropProdProp (A : Type) (B : Type) (ha : isProp A) (hb : isProp B) : isProp (A × B)

The product of two propositions is a proposition.

isContrProd2

Section titled “isContrProd2”
def isContrProd2 (A : Type) (B : Type) (ha : isContr A) (hb : isContr B) : isContr (A × B)

The product of two contractible types is contractible.

isPropPathIsContr

Section titled “isPropPathIsContr”
def isPropPathIsContr (A : Type) (h : isProp A) (x : A) (y : A) : isContr (x ≡ y)

In a proposition every path space is contractible.

isContrCumulative

Section titled “isContrCumulative”
def isContrCumulative {A : Type} (h : isContr A) : isSet A

A contractible type is a set.

isPropNatToUnit

Section titled “isPropNatToUnit”
def isPropNatToUnit : isProp (Nat -> Unit)

Functions from Nat to Unit form a proposition.

isPropBoolToUnit

Section titled “isPropBoolToUnit”
def isPropBoolToUnit : isProp (Bool -> Unit)

Functions from Bool to Unit form a proposition.

isPropUnitToUnit

Section titled “isPropUnitToUnit”
def isPropUnitToUnit : isProp (Unit -> Unit)

Functions from Unit to Unit form a proposition.

isPropUnitUnit

Section titled “isPropUnitUnit”
def isPropUnitUnit : isProp (Unit × Unit)

Unit × Unit is a proposition.

isSetUnitUnit

Section titled “isSetUnitUnit”
def isSetUnitUnit : isSet (Unit × Unit)

Unit × Unit is a set.

isPropEmptyToAny

Section titled “isPropEmptyToAny”
def isPropEmptyToAny (A : Type) : isProp (Empty -> A)

Functions out of Empty form a proposition.

isPropNotNat

Section titled “isPropNotNat”
def isPropNotNat : isProp (Nat -> Empty)

The negation Nat -> Empty is a proposition.

isPropNotBool

Section titled “isPropNotBool”
def isPropNotBool : isProp (Bool -> Empty)

The negation Bool -> Empty is a proposition.

isContrAToUnit

Section titled “isContrAToUnit”
def isContrAToUnit (A : Type) : isContr (A -> Unit)

Functions from any type into Unit form a contractible type.

isContr_to_isTrunc0

Section titled “isContr_to_isTrunc0”
def isContr_to_isTrunc0 (A : Type) (h : isContr A) : isTrunc zero A

A contractible type has truncation level 0.

isContr_to_isProp

Section titled “isContr_to_isProp”
def isContr_to_isProp (A : Type) (h : isContr A) : isProp A

A contractible type is a proposition.

isContr_to_isSet

Section titled “isContr_to_isSet”
def isContr_to_isSet (A : Type) (h : isContr A) : isSet A

A contractible type is a set.

unit_isContr

Section titled “unit_isContr”
def unit_isContr : isContr Unit

Unit is contractible.

unit_isProp

Section titled “unit_isProp”
def unit_isProp : isProp Unit

Unit is a proposition.

unit_isSet

Section titled “unit_isSet”
def unit_isSet : isSet Unit

Unit is a set.

isOfHLevel

Section titled “isOfHLevel”
def isOfHLevel (n : Nat) (A : Type) : Type

The h-level predicate, an alias for isTrunc.

isPropImpliesIsSet

Section titled “isPropImpliesIsSet”
def isPropImpliesIsSet (A : Type) (h : isProp A) : isSet A

Every proposition is a set.

isSetToIsGroupoid

Section titled “isSetToIsGroupoid”
def isSetToIsGroupoid (A : Type) (h : isSet A) : isGroupoid A

Every set is a groupoid.

isGroupoidUnit

Section titled “isGroupoidUnit”
def isGroupoidUnit : isGroupoid Unit

Unit is a groupoid.

isGroupoidBool

Section titled “isGroupoidBool”
def isGroupoidBool : isGroupoid Bool

Bool is a groupoid.

isTrunc1_to_isTrunc2

Section titled “isTrunc1_to_isTrunc2”
def isTrunc1_to_isTrunc2 (A : Type) (h : isTrunc (succ zero) A) : isTrunc (succ (succ zero)) A

Truncation level 1 implies truncation level 2.

isPropPiType

Section titled “isPropPiType”
def isPropPiType (A : Type) (B : A -> Type) (h : (x : A) -> isProp (B x)) : isProp ((x : A) -> B x)

A dependent function type into a family of propositions is a proposition.

isSetPiType

Section titled “isSetPiType”
def isSetPiType (A : Type) (B : A -> Type) (h : (x : A) -> isSet (B x)) : isSet ((x : A) -> B x)

A dependent function type into a family of sets is a set.

isPropProdType

Section titled “isPropProdType”
def isPropProdType (A : Type) (B : Type) (ha : isProp A) (hb : isProp B) : isProp (A × B)

The product of two propositions is a proposition.

isSetProdType

Section titled “isSetProdType”
def isSetProdType (A : Type) (B : Type) (ha : isSet A) (hb : isSet B) : isSet (A × B)

The product of two sets is a set.

isPropUnitUnit_v3

Section titled “isPropUnitUnit_v3”
def isPropUnitUnit_v3 : isProp (Unit × Unit)

Unit × Unit is a proposition, via the product lemma.

isSetBoolBool

Section titled “isSetBoolBool”
def isSetBoolBool : isSet (Bool × Bool)

Bool × Bool is a set.

isSetUnitBool

Section titled “isSetUnitBool”
def isSetUnitBool : isSet (Unit × Bool)

Unit × Bool is a set.

retractIsProp

Section titled “retractIsProp”
def retractIsProp (A : Type) (B : Type) (r : B -> A) (s : A -> B) (ret : (a : A) -> r (s a) ≡ a) (hB : isProp B) : isProp A

A retract of a proposition is a proposition.

retractIsProp_Unit

Section titled “retractIsProp_Unit”
def retractIsProp_Unit : isProp Unit

Unit is a proposition, as a retract of itself.

retractIsContr

Section titled “retractIsContr”
def retractIsContr (A : Type) (B : Type) (r : B -> A) (s : A -> B) (ret : (a : A) -> r (s a) ≡ a) (hB : isContr B) : isContr A

A retract of a contractible type is contractible.

retractIsContr_Unit

Section titled “retractIsContr_Unit”
def retractIsContr_Unit : isContr Unit

Unit is contractible, as a retract of itself.

isSetArrow

Section titled “isSetArrow”
def isSetArrow (A : Type) (B : Type) (hB : isSet B) : isSet (A -> B)

Functions into a set form a set.

isPropArrow2

Section titled “isPropArrow2”
def isPropArrow2 (A : Type) (B : Type) (C : Type) (hC : isProp C) : isProp (A -> B -> C)

Two-argument functions into a proposition form a proposition.

isPropArrow3

Section titled “isPropArrow3”
def isPropArrow3 (A : Type) (B : Type) (C : Type) (D : Type) (hD : isProp D) : isProp (A -> B -> C -> D)

Three-argument functions into a proposition form a proposition.

isContr_isProp_isSet_chain

Section titled “isContr_isProp_isSet_chain”
def isContr_isProp_isSet_chain (A : Type) (h : isContr A) : isSet A

A contractible type is a set, going through propositions.

isContr_isProp_isSet_isGroupoid_chain

Section titled “isContr_isProp_isSet_isGroupoid_chain”
def isContr_isProp_isSet_isGroupoid_chain (A : Type) (h : isContr A) : isGroupoid A

A contractible type is a groupoid, going through propositions and sets.

isTrunc0_to_isTrunc2

Section titled “isTrunc0_to_isTrunc2”
def isTrunc0_to_isTrunc2 (A : Type) (h : isTrunc zero A) : isTrunc (succ (succ zero)) A

Truncation level 0 implies truncation level 2.

isGroupoidBoolBool

Section titled “isGroupoidBoolBool”
def isGroupoidBoolBool : isGroupoid (Bool × Bool)

Bool × Bool is a groupoid.

isSetBool3

Section titled “isSetBool3”
def isSetBool3 : isSet ((Bool × Bool) × Bool)

(Bool × Bool) × Bool is a set.

isSetUnit3

Section titled “isSetUnit3”
def isSetUnit3 : isSet ((Unit × Unit) × Unit)

(Unit × Unit) × Unit is a set.

isPropUnit3

Section titled “isPropUnit3”
def isPropUnit3 : isProp ((Unit × Unit) × Unit)

(Unit × Unit) × Unit is a proposition.

isContrUnit3

Section titled “isContrUnit3”
def isContrUnit3 : isContr ((Unit × Unit) × Unit)

(Unit × Unit) × Unit is contractible.

isSetArrow2

Section titled “isSetArrow2”
def isSetArrow2 (A : Type) (B : Type) (C : Type) (hC : isSet C) : isSet (A -> B -> C)

Two-argument functions into a set form a set.

hProp

Section titled “hProp”
def hProp : Type 1

The type of propositions: a type together with a proof that it is a proposition.

isPropPathBool

Section titled “isPropPathBool”
def isPropPathBool (a : Bool) (b : Bool) : isProp (a ≡ b)

Paths between two booleans form a proposition.

bool_path_hProp

Section titled “bool_path_hProp”
def bool_path_hProp (a : Bool) (b : Bool) : hProp

The path type between two booleans, packaged as an hProp.

isOfHLevel2Def

Section titled “isOfHLevel2Def”
def isOfHLevel2Def (A : Type) : isOfHLevel (succ (succ zero)) A ≡ ((x : A) -> (y : A) -> (x0 : x ≡ y) -> (x1 : x ≡ y) -> isContr (x0 ≡ x1))

Unfolds h-level 2: any two parallel paths have a contractible space of paths between them.

isTrunc0_Unit

Section titled “isTrunc0_Unit”
def isTrunc0_Unit : isTrunc zero Unit

Unit has truncation level 0.

isTrunc1_Unit

Section titled “isTrunc1_Unit”
def isTrunc1_Unit : isTrunc (succ zero) Unit

Unit has truncation level 1.

isTrunc2_Unit

Section titled “isTrunc2_Unit”
def isTrunc2_Unit : isTrunc (succ (succ zero)) Unit

Unit has truncation level 2.

isTrunc2_Bool

Section titled “isTrunc2_Bool”
def isTrunc2_Bool : isTrunc (succ (succ zero)) Bool

Bool has truncation level 2.

isTrunc2_UnitUnit

Section titled “isTrunc2_UnitUnit”
def isTrunc2_UnitUnit : isTrunc (succ (succ zero)) (Unit × Unit)

Unit × Unit has truncation level 2.

unit_isTrunc0

Section titled “unit_isTrunc0”
def unit_isTrunc0 : isTrunc zero Unit

Unit has truncation level 0.

unit_isTrunc1

Section titled “unit_isTrunc1”
def unit_isTrunc1 : isTrunc (succ zero) Unit

Unit has truncation level 1.

unit_isTrunc2

Section titled “unit_isTrunc2”
def unit_isTrunc2 : isTrunc (succ (succ zero)) Unit

Unit has truncation level 2.

bool_isTrunc2

Section titled “bool_isTrunc2”
def bool_isTrunc2 : isTrunc (succ (succ zero)) Bool

Bool has truncation level 2.

isOfHLevel_0_Unit

Section titled “isOfHLevel_0_Unit”
def isOfHLevel_0_Unit : isOfHLevel zero Unit

Unit has h-level 0.

isTrunc2_BoolBool

Section titled “isTrunc2_BoolBool”
def isTrunc2_BoolBool : isTrunc (succ (succ zero)) (Bool × Bool)

Bool × Bool has truncation level 2.

isTrunc1_UnitUnit

Section titled “isTrunc1_UnitUnit”
def isTrunc1_UnitUnit : isTrunc (succ zero) (Unit × Unit)

Unit × Unit has truncation level 1.

isOfHLevel_2_BoolBool

Section titled “isOfHLevel_2_BoolBool”
def isOfHLevel_2_BoolBool : isOfHLevel (succ (succ zero)) (Bool × Bool)

Bool × Bool has h-level 2.

isSetNatToBool

Section titled “isSetNatToBool”
def isSetNatToBool : isSet (Nat -> Bool)

Functions from Nat to Bool form a set.

isSetBoolToBool

Section titled “isSetBoolToBool”
def isSetBoolToBool : isSet (Bool -> Bool)

Functions from Bool to Bool form a set.

isSetUnitToUnit

Section titled “isSetUnitToUnit”
def isSetUnitToUnit : isSet (Unit -> Unit)

Functions from Unit to Unit form a set.

isSetBoolToUnit

Section titled “isSetBoolToUnit”
def isSetBoolToUnit : isSet (Bool -> Unit)

Functions from Bool to Unit form a set.

isSetNatNatToBool

Section titled “isSetNatNatToBool”
def isSetNatNatToBool : isSet (Nat -> Nat -> Bool)

Two-argument functions from Nat to Bool form a set.