unit

unitCenter

def unitCenter : Unit

The canonical element of Unit, the center of its contraction.

unitContraction

def unitContraction (x : Unit) : unit ≡ x

Every element of Unit is connected to unit by a path.

unitContr

def unitContr : isContr Unit

Unit is contractible, with center unit.

unitEta

def unitEta (x : Unit) : x ≡ unit

Eta for Unit: every element is equal to unit.

unitUnique

def unitUnique (x : Unit) (y : Unit) : x ≡ y

Any two elements of Unit are equal.

unitIsProp

def unitIsProp : isProp Unit

Unit is a proposition: any two elements are equal.

unitIsSet

def unitIsSet : isSet Unit

Unit is a set, derived from being a proposition.

unitIsSetDirect

def unitIsSetDirect : isSet Unit

Unit is a set, proved directly by case analysis on the endpoints.

allPathsUnit

def allPathsUnit (x : Unit) (y : Unit) (p : x ≡ y) : unitUnique x y ≡ p

Every path between two elements of Unit equals the canonical one from unitUnique.

unitRefl

def unitRefl : unit ≡ unit

The constant path at unit.

pathUnitRefl

def pathUnitRefl (p : unit ≡ unit) : unitRefl ≡ p

Every loop at unit equals the constant path unitRefl.

unitPathTrivial

def unitPathTrivial (x : Unit) : x ≡ x

The constant loop at any element of Unit.

terminal

def terminal {A : Type} (a : A) : Unit

The unique map from any type to Unit, sending everything to unit.

terminalUnique

def terminalUnique {A : Type} (f : A -> Unit) (g : A -> Unit) : f ≡ g

Any two functions into Unit are equal, so Unit is a terminal object.

terminalCompose

def terminalCompose {A B : Type} (f : A -> B) : (fun (a : A) => terminal (f a)) ≡ (fun (a : A) => unit)

Composing any function with terminal gives the constant function to unit.

constUnit

def constUnit {A : Type} (f : A -> Unit) (a1 : A) (a2 : A) : f a1 ≡ f a2

Every function into Unit is constant: it takes equal values on any two inputs.

funToUnitCenter

def funToUnitCenter (A : Type) : A -> Unit

The constant function from a type to Unit, the center of the contractible function type.

funToUnitContr

def funToUnitContr (A : Type) : isContr (A -> Unit)

The function type A -> Unit is contractible.

funToUnitIsProp

def funToUnitIsProp (A : Type) : isProp (A -> Unit)

The function type A -> Unit is a proposition.

funToUnitIsSet

def funToUnitIsSet (A : Type) : isSet (A -> Unit)

The function type A -> Unit is a set.

transportUnitRefl

def transportUnitRefl (x : Unit) : transport (fun i => Unit) x ≡ x

Transport along the constant family at Unit is the identity.

transportUnitConst

def transportUnitConst (A : Type) (p : A ≡ A) (x : Unit) : transport (fun i => Unit) x ≡ x

Transport along the constant family at Unit is the identity, whatever path in the base is given.

unitProdFwd

def unitProdFwd {A : Type} (p : Unit × A) : A

Forward map of Unit × A ≅ A: drops the unit component.

unitProdBwd

def unitProdBwd {A : Type} (a : A) : Unit × A

Backward map of Unit × A ≅ A: pairs unit with a value.

unitProdFwdBwd

def unitProdFwdBwd {A : Type} (a : A) : unitProdFwd (unitProdBwd a) ≡ a

Pairing with unit on the left and then dropping it gives back the value.

unitProdBwdFwd

def unitProdBwdFwd {A : Type} (p : Unit × A) : unitProdBwd (unitProdFwd p) ≡ p

Dropping the unit component and pairing it back gives the original pair.

prodUnitFwd

def prodUnitFwd {A : Type} (p : A × Unit) : A

Forward map of A × Unit ≅ A: drops the unit component.

prodUnitBwd

def prodUnitBwd {A : Type} (a : A) : A × Unit

Backward map of A × Unit ≅ A: pairs a value with unit.

prodUnitFwdBwd

def prodUnitFwdBwd {A : Type} (a : A) : prodUnitFwd (prodUnitBwd a) ≡ a

Pairing with unit on the right and then dropping it gives back the value.

prodUnitBwdFwd

def prodUnitBwdFwd {A : Type} (p : A × Unit) : prodUnitBwd (prodUnitFwd p) ≡ p

Dropping the unit component and pairing it back gives the original pair.

sigmaUnitFwdNonDep

def sigmaUnitFwdNonDep {B : Type} (p : (x : Unit) × B) : B

Forward map of a non-dependent sum over Unit to its fiber: takes the second component.

sigmaUnitBwdNonDep

def sigmaUnitBwdNonDep {B : Type} (b : B) : (x : Unit) × B

Backward map into a non-dependent sum over Unit: pairs unit with a value.

sigmaUnitFwdBwdNonDep

def sigmaUnitFwdBwdNonDep {B : Type} (b : B) : sigmaUnitFwdNonDep (sigmaUnitBwdNonDep b) ≡ b

Injecting into the sum over Unit and projecting back gives the original value.

sigmaUnitBwdFwdNonDep

def sigmaUnitBwdFwdNonDep {B : Type} (p : (x : Unit) × B) : sigmaUnitBwdNonDep (sigmaUnitFwdNonDep p) ≡ p

Projecting out of the sum over Unit and injecting back gives the original pair.

unitProdUnitFwd

def unitProdUnitFwd (p : Unit × Unit) : Unit

Forward map of Unit × Unit ≅ Unit.

unitProdUnitBwd

def unitProdUnitBwd (u : Unit) : Unit × Unit

Backward map of Unit × Unit ≅ Unit, giving (unit, unit).

unitProdUnitFwdBwd

def unitProdUnitFwdBwd (u : Unit) : unitProdUnitFwd (unitProdUnitBwd u) ≡ u

The round trip Unit -> Unit × Unit -> Unit is the identity.

unitProdUnitBwdFwd

def unitProdUnitBwdFwd (p : Unit × Unit) : unitProdUnitBwd (unitProdUnitFwd p) ≡ p

The round trip Unit × Unit -> Unit -> Unit × Unit is the identity.

isContrUnitProd

def isContrUnitProd : isContr (Unit × Unit)

Unit × Unit is contractible, with center (unit, unit).

emptyElim

def emptyElim {A : Type} (e : Empty) : A

Ex falso: an element of Empty yields an element of any type (same as absurd).

emptyRec

def emptyRec (A : Type) (e : Empty) : A

Non-dependent eliminator for Empty with the target type given explicitly.

emptyIsProp

def emptyIsProp : isProp Empty

Empty is a proposition, vacuously.

emptyIsSet

def emptyIsSet : isSet Empty

Empty is a set, derived from being a proposition.

neg

def neg (A : Type) : Type

Negation of a type: functions from it to Empty.

negIntro

def negIntro {A : Type} (f : A -> Empty) : neg A

Builds a negation from a function into Empty.

negElim

def negElim {A : Type} (n : neg A) (a : A) : Empty

Applies a negation to an element, giving a contradiction in Empty.

negIsProp

def negIsProp (A : Type) : isProp (neg A)

Every negation is a proposition.

negIsSet

def negIsSet (A : Type) : isSet (neg A)

Every negation is a set.

DoubleNeg

def DoubleNeg (A : Type) : Type

Double negation of a type: the negation of its negation.

dnIntro

def dnIntro {A : Type} (a : A) : DoubleNeg A

Double negation introduction: an element of A gives not-not A.

dnMap

def dnMap {A B : Type} (f : A -> B) : DoubleNeg A -> DoubleNeg B

Double negation is functorial: a map A -> B lifts to not-not A -> not-not B.

dnBind

def dnBind {A B : Type} (nna : DoubleNeg A) (f : A -> DoubleNeg B) : DoubleNeg B

Monadic bind for double negation.

dnIsProp

def dnIsProp (A : Type) : isProp (DoubleNeg A)

Every double negation is a proposition.

tripleNegFwd

def tripleNegFwd {A : Type} (nnna : neg (DoubleNeg A)) : neg A

Triple negation implies single negation.

tripleNegBwd

def tripleNegBwd {A : Type} (na : neg A) : neg (DoubleNeg A)

Single negation implies triple negation.

tripleNegFwdBwd

def tripleNegFwdBwd {A : Type} (na : neg A) : tripleNegFwd (tripleNegBwd na) ≡ na

Going from not A to triple negation and back gives the original proof.

tripleNegBwdFwd

def tripleNegBwdFwd {A : Type} (nnna : neg (DoubleNeg A)) : tripleNegBwd (tripleNegFwd nnna) ≡ nnna

Going from triple negation to not A and back gives the original proof.

emptyProdAbsurd

def emptyProdAbsurd {A B : Type} (p : Empty × A) : B

A pair with an Empty first component yields anything.

prodEmptyAbsurd

def prodEmptyAbsurd {A B : Type} (p : A × Empty) : B

A pair with an Empty second component yields anything.

emptyProdIsProp

def emptyProdIsProp {A : Type} : isProp (Empty × A)

Empty × A is a proposition, vacuously.

prodEmptyIsProp

def prodEmptyIsProp {A : Type} : isProp (A × Empty)

A × Empty is a proposition, vacuously.

negEmptyCenter

def negEmptyCenter : neg Empty

The canonical proof of not Empty, the center of its contraction.

negEmptyIsContr

def negEmptyIsContr : isContr (neg Empty)

not Empty is contractible.

negEmptyIsProp

def negEmptyIsProp : isProp (neg Empty)

not Empty is a proposition.

negUnitAbsurd

def negUnitAbsurd (n : neg Unit) : Empty

A negation of Unit gives a contradiction, since unit exists.

emptyFunCenter

def emptyFunCenter (A : Type) : Empty -> A

The empty function from Empty to any type, the center of the contractible function type.

emptyFunIsContr

def emptyFunIsContr (A : Type) : isContr (Empty -> A)

The function type Empty -> A is contractible.

emptyFunIsProp

def emptyFunIsProp (A : Type) : isProp (Empty -> A)

The function type Empty -> A is a proposition.

emptyFunIsSet

def emptyFunIsSet (A : Type) : isSet (Empty -> A)

The function type Empty -> A is a set.

unitIsNotEmpty

def unitIsNotEmpty : neg (Unit -> Empty)

Unit is inhabited, so a map Unit -> Empty is impossible.

unitDecElement

def unitDecElement : Unit

An explicit element of Unit, witnessing that it is inhabited.

unitInd

def unitInd (P : Unit -> Type) (p : P unit) : (x : Unit) -> P x

Induction principle for Unit: a value of P unit gives a section of P.

unitRec

def unitRec {A : Type} (a : A) : Unit -> A

Non-dependent recursor for Unit: the constant function at a given value.

unitRecComp

def unitRecComp {A : Type} (a : A) : unitRec a unit ≡ a

unitRec a at unit computes to a.

unitIndComp

def unitIndComp (P : Unit -> Type) (p : P unit) : unitInd P p unit ≡ p

unitInd P p at unit computes to p.

unitProdMap

def unitProdMap {A B : Type} (f : A -> B) (p : Unit × A) : Unit × B

Maps a function over the non-unit component of Unit × A.

prodUnitMap

def prodUnitMap {A B : Type} (f : A -> B) (p : A × Unit) : B × Unit

Maps a function over the non-unit component of A × Unit.

unitProdMapId

def unitProdMapId {A : Type} (p : Unit × A) : unitProdMap (fun (a : A) => a) p ≡ (unit, snd p)

unitProdMap with the identity returns the pair with unit and the same second component.

prodUnitMapId

def prodUnitMapId {A : Type} (p : A × Unit) : prodUnitMap (fun (a : A) => a) p ≡ (fst p, unit)

prodUnitMap with the identity returns the pair with the same first component and unit.

unitProdMapComp

def unitProdMapComp {A B C : Type} (f : A -> B) (g : B -> C) (p : Unit × A) : unitProdMap g (unitProdMap f p) ≡ unitProdMap (fun (a : A) => g (f a)) p

Composition law for unitProdMap: mapping twice equals mapping the composite once.

prodUnitMapComp

def prodUnitMapComp {A B C : Type} (f : A -> B) (g : B -> C) (p : A × Unit) : prodUnitMap g (prodUnitMap f p) ≡ prodUnitMap (fun (a : A) => g (f a)) p

Composition law for prodUnitMap: mapping twice equals mapping the composite once.

unitBasePoint

def unitBasePoint : Unit

The base point of Unit as a pointed type.

unitLoop

def unitLoop : unitBasePoint ≡ unitBasePoint

The constant loop at the base point of Unit.

emptyToEmpty

def emptyToEmpty : Empty -> Empty

The identity function on Empty, defined by empty pattern matching.

emptyToEmptyEq

def emptyToEmptyEq (f : Empty -> Empty) : emptyToEmpty ≡ f

Every function Empty -> Empty equals emptyToEmpty.

emptyEndoIsContr

def emptyEndoIsContr : isContr (Empty -> Empty)

The function type Empty -> Empty is contractible.

unitWitness

def unitWitness : Unit

An explicit element of Unit, witnessing that it is inhabited.

negUnitToEmpty

def negUnitToEmpty (f : neg Unit) : Empty

A negation of Unit gives a contradiction, since unit exists.

negNegUnit

def negNegUnit : DoubleNeg Unit

The double negation of Unit holds.

sigmaConstUnitFwd

def sigmaConstUnitFwd {A : Type} (p : (x : A) × Unit) : A

Forward map of the sum of the constant family Unit over A to A: takes the first component.

sigmaConstUnitBwd

def sigmaConstUnitBwd {A : Type} (a : A) : (x : A) × Unit

Backward map from A to the sum of the constant family Unit: pairs a value with unit.

sigmaConstUnitFwdBwd

def sigmaConstUnitFwdBwd {A : Type} (a : A) : sigmaConstUnitFwd (sigmaConstUnitBwd a) ≡ a

Pairing with unit and projecting back gives the original value.

sigmaConstUnitBwdFwd

def sigmaConstUnitBwdFwd {A : Type} (p : (x : A) × Unit) : sigmaConstUnitBwd (sigmaConstUnitFwd p) ≡ p

Projecting the first component and pairing it with unit gives the original pair.

sigmaEmptyBaseAbsurd

def sigmaEmptyBaseAbsurd {B : Empty -> Type} {C : Type} (p : (x : Empty) × B x) : C

A dependent pair whose first component lies in Empty yields anything.

sigmaEmptyBaseIsProp

def sigmaEmptyBaseIsProp {B : Empty -> Type} : isProp ((x : Empty) × B x)

A dependent sum over Empty is a proposition, vacuously.

constToUnit

def constToUnit (A : Type) : A -> Unit

The constant function from a type to Unit.

constToUnitUnique

def constToUnitUnique (A : Type) (f : A -> Unit) : constToUnit A ≡ f

Every function into Unit equals constToUnit.

constFromUnit

def constFromUnit {A : Type} (a : A) : Unit -> A

The function from Unit that always returns a given value.

constFromUnitComp

def constFromUnitComp {A : Type} (a : A) : constFromUnit a unit ≡ a

constFromUnit a at unit computes to a.

unitProdProdFwd

def unitProdProdFwd {A B : Type} (p : (Unit × A) × B) : A × B

Forward map of (Unit × A) × B ≅ A × B: drops the unit component.

unitProdProdBwd

def unitProdProdBwd {A B : Type} (p : A × B) : (Unit × A) × B

Backward map of (Unit × A) × B ≅ A × B: inserts unit.

unitProdProdFwdBwd

def unitProdProdFwdBwd {A B : Type} (p : A × B) : unitProdProdFwd (unitProdProdBwd p) ≡ p

Inserting unit and dropping it again gives the original pair.

unitProdProdBwdFwd

def unitProdProdBwdFwd {A B : Type} (p : (Unit × A) × B) : unitProdProdBwd (unitProdProdFwd p) ≡ p

Dropping the unit component and inserting it again gives the original nested pair.

negContra

def negContra {A B : Type} (f : A -> B) (nb : neg B) : neg A

Contrapositive: a map A -> B turns not B into not A.

negContraComp

def negContraComp {A B C : Type} (f : A -> B) (g : B -> C) (nc : neg C) : negContra f (negContra g nc) ≡ negContra (fun (a : A) => g (f a)) nc

Contrapositives compose: taking them one after the other equals the contrapositive of the composite.

negContraId

def negContraId {A : Type} (na : neg A) : negContra (fun (a : A) => a) na ≡ na

The contrapositive of the identity is the identity.

unitPathIsContr

def unitPathIsContr (x : Unit) (y : Unit) : isContr (x ≡ y)

The path type between two elements of Unit is contractible.

unitPathIsProp

def unitPathIsProp (x : Unit) (y : Unit) : isProp (x ≡ y)

The path type between two elements of Unit is a proposition.

unitPathPath

def unitPathPath (x : Unit) (y : Unit) (p q : x ≡ y) (r s : p ≡ q) : r ≡ s

Any two paths between paths in Unit are equal.

absurdUnit

def absurdUnit (e : Empty) : Unit

An element of Empty yields an element of Unit.

absurdPath

def absurdPath {A : Type} {a b : A} (e : Empty) : a ≡ b

An element of Empty yields a path between any two elements.

absurdProd

def absurdProd {A B : Type} (e : Empty) : A × B

An element of Empty yields an element of any product type.

absurdFun

def absurdFun {A B : Type} (e : Empty) : A -> B

An element of Empty yields a function of any type.

unitToUnitCenter

def unitToUnitCenter : Unit -> Unit

The constant function on Unit, the center of the contractible type Unit -> Unit.

unitToUnitIsContr

def unitToUnitIsContr : isContr (Unit -> Unit)

The function type Unit -> Unit is contractible.

unitToUnitIsProp

def unitToUnitIsProp : isProp (Unit -> Unit)

The function type Unit -> Unit is a proposition.

piUnitIsContr

def piUnitIsContr (A : Type) : isContr ((x : A) -> Unit)

A dependent function type into Unit is contractible.

piUnitIsProp

def piUnitIsProp (A : Type) : isProp ((x : A) -> Unit)

A dependent function type into Unit is a proposition.

negInhabited

def negInhabited {A : Type} (a : A) (na : neg A) : Empty

An element of A together with not A gives a contradiction in Empty.

negInhabitedContra

def negInhabitedContra {A B : Type} (a : A) (na : neg A) : B

An element of A together with not A yields anything.

curryUnitFwd

def curryUnitFwd {A B : Type} (f : Unit × A -> B) : A -> B

Turns a function on Unit × A into a function on A by supplying unit.

curryUnitBwd

def curryUnitBwd {A B : Type} (g : A -> B) : Unit × A -> B

Turns a function on A into a function on Unit × A by ignoring the unit component.

curryUnitFwdBwd

def curryUnitFwdBwd {A B : Type} (g : A -> B) : curryUnitFwd (curryUnitBwd g) ≡ g

Extending a function on A to Unit × A and restricting it back gives the original function.

unitPathSym

def unitPathSym (p : unit ≡ unit) : sym p ≡ unitRefl

The inverse of any loop at unit equals unitRefl.

unitPathTrans

def unitPathTrans (p : unit ≡ unit) (q : unit ≡ unit) : trans p q ≡ unitRefl

The composite of any two loops at unit equals unitRefl.

unitPathCongEq

def unitPathCongEq {B : Type} (f : Unit -> B) (p : unit ≡ unit) (q : unit ≡ unit) : cong f p ≡ cong f q

Applying a function to any two loops at unit gives equal paths.

isContrToUnit

def isContrToUnit (A : Type) (h : isContr A) : A -> Unit

The map from a contractible type to Unit, one half of its equivalence with Unit.

unitToIsContr

def unitToIsContr (A : Type) (h : isContr A) : Unit -> A

The map from Unit to a contractible type, sending unit to the center.

isContrToUnitRT

def isContrToUnitRT (A : Type) (h : isContr A) (u : Unit) : isContrToUnit A h (unitToIsContr A h u) ≡ u

Going from Unit to a contractible type and back is the identity on Unit.

unitToIsContrRT

def unitToIsContrRT (A : Type) (h : isContr A) (a : A) : unitToIsContr A h (isContrToUnit A h a) ≡ fst h

Going from a contractible type to Unit and back lands on the center.

fiberTerminalFwd

def fiberTerminalFwd (A : Type) (fb : fiber A Unit (fun (_ : A) => unit) unit) : A

Forward map from the fiber of the terminal map over unit to A: takes the point.

fiberTerminalBwd

def fiberTerminalBwd (A : Type) (a : A) : fiber A Unit (fun (_ : A) => unit) unit

Backward map from A into the fiber of the terminal map over unit.

fiberTerminalFwdBwd

def fiberTerminalFwdBwd (A : Type) (a : A) : fiberTerminalFwd A (fiberTerminalBwd A a) ≡ a

Injecting into the fiber of the terminal map and projecting back gives the original element.

unit_is_contr

theorem unit_is_contr : isContr Unit

Unit is contractible.

unit_is_prop

theorem unit_is_prop : isProp Unit

Unit is a proposition.

unit_is_set

theorem unit_is_set : isSet Unit

Unit is a set.

empty_is_prop

theorem empty_is_prop : isProp Empty

Empty is a proposition.

empty_is_set

theorem empty_is_set : isSet Empty

Empty is a set.

neg_is_prop

theorem neg_is_prop (A : Type) : isProp (neg A)

Every negation is a proposition.

dn_is_prop

theorem dn_is_prop (A : Type) : isProp (DoubleNeg A)

Every double negation is a proposition.

fun_to_unit_contr

theorem fun_to_unit_contr (A : Type) : isContr (A -> Unit)

The function type A -> Unit is contractible.

fun_from_empty_contr

theorem fun_from_empty_contr (A : Type) : isContr (Empty -> A)

The function type Empty -> A is contractible.

unit_to_unit_contr

theorem unit_to_unit_contr : isContr (Unit -> Unit)

The function type Unit -> Unit is contractible.

neg_empty_contr

theorem neg_empty_contr : isContr (neg Empty)

not Empty is contractible.