equiv

uaBeta

def uaBeta {A B : Type} (e : Equiv A B) (x : A) : transport (ua e) x ≡ fst e x

Univalence computation rule: transporting along ua e applies the forward function of e.

equivToPath

def equivToPath {A B : Type} (e : Equiv A B) : A ≡ B

Turns an equivalence into a path between types via univalence.

notInvol2

def notInvol2 (b : Bool) : not (not b) ≡ b

Boolean negation is an involution: not (not b) is path-equal to b.

notFiberContrTrue

def notFiberContrTrue : isContr (fiber Bool Bool not true)

The fiber of not over true is contractible, centered at false.

notFiberContrFalse

def notFiberContrFalse : isContr (fiber Bool Bool not false)

The fiber of not over false is contractible, centered at true.

notIsEquiv

def notIsEquiv : isEquiv Bool Bool not

Boolean negation is an equivalence: every fiber is contractible.

notEquiv

def notEquiv : Equiv Bool Bool

The equivalence Bool ≃ Bool given by boolean negation.

notPathBool

def notPathBool : Bool ≡ Bool

The nontrivial path Bool ≡ Bool obtained from notEquiv by univalence.

uaBetaNot

def uaBetaNot (x : Bool) : transport (ua notEquiv) x ≡ not x

Transporting along ua notEquiv computes to not, definitionally.

uaIdTransport

def uaIdTransport (A : Type) (x : A) : transport (ua (idEquiv A)) x ≡ x

Transporting along ua of the identity equivalence is the identity.

notPathRoundtrip

def notPathRoundtrip (x : Bool) : transport notPathBool (transport notPathBool x) ≡ x

Transporting twice along notPathBool returns the original boolean.

equivInvFun

def equivInvFun {A B : Type} (e : Equiv A B) (b : B) : A

The inverse function of an equivalence, taken from the centers of its fibers.

equivSection

def equivSection {A B : Type} (e : Equiv A B) (b : B) : fst e (equivInvFun e b) ≡ b

The inverse of an equivalence is a right inverse: applying the forward function to it gives back the input.

pathToFun

def pathToFun (A : Type) (B : Type) (p : A ≡ B) (a : A) : B

Turns a path between types into a function by transport.

pathToFunRefl

def pathToFunRefl (A : Type) (a : A) : pathToFun A A refl a ≡ a

pathToFun along refl is the identity.

equivPreservesContr

def equivPreservesContr {A B : Type} (e : Equiv A B) (h : isContr A) : isContr B

Equivalences preserve contractibility: if A is contractible and A ≃ B, then B is contractible.

idEquivBool

def idEquivBool : Equiv Bool Bool

The identity equivalence on Bool.

notEquivForward

def notEquivForward (b : Bool) : fst notEquiv b ≡ not b

The forward function of notEquiv is not.

equivRetraction

def equivRetraction {A B : Type} (e : Equiv A B) (a : A) : equivInvFun e (fst e a) ≡ a

The inverse of an equivalence is a left inverse: inverting the image of a gives back a.

transportSymTransport

def transportSymTransport {A B : Type} (p : A ≡ B) (a : A) : transport (sym p) (transport p a) ≡ a

Transporting along a path and then back along its inverse returns the original element.

uaDoubleTransport

def uaDoubleTransport {A B : Type} (e : Equiv A B) (a : A) : transport (sym (ua e)) (transport (ua e) a) ≡ a

Transporting along ua e and then back along its inverse returns the original element.

pathToFunBool

def pathToFunBool (p : Bool ≡ Bool) (b : Bool) : Bool

Turns a path Bool ≡ Bool into a function on Bool by transport.

natIdEquiv

def natIdEquiv : Equiv Nat Nat

The identity equivalence on Nat.

fiberIdCenter

def fiberIdCenter (A : Type) (a : A) : fiber A A (fun (x : A) => x) a

The canonical point (a, refl) in the fiber of the identity function over a.

idEquivListNat

def idEquivListNat : Equiv (List Nat) (List Nat)

The identity equivalence on List Nat.

notFiberFalseCenter

def notFiberFalseCenter : fiber Bool Bool not false

The center (true, refl) of the fiber of not over false.

notFiberTrueCenter

def notFiberTrueCenter : fiber Bool Bool not true

The center (false, refl) of the fiber of not over true.

fiberSuccOne

def fiberSuccOne : fiber Nat Nat succ (succ zero)

The point (0, refl) in the fiber of succ over 1.

fiberSuccTwo

def fiberSuccTwo : fiber Nat Nat succ (succ (succ zero))

The point (1, refl) in the fiber of succ over 2.

boolIdEquiv

def boolIdEquiv : Equiv Bool Bool

The identity equivalence on Bool.

uaIdTransportBool

def uaIdTransportBool (b : Bool) : transport (ua (idEquiv Bool)) b ≡ b

Transporting a boolean along ua of the identity equivalence computes to itself.

uaIdTransportListNat

def uaIdTransportListNat (xs : List Nat) : transport (ua (idEquiv (List Nat))) xs ≡ xs

Transporting a list of naturals along ua of the identity equivalence computes to itself.

equivSymPath

def equivSymPath {A B : Type} (e : Equiv A B) : B ≡ A

The inverse path B ≡ A induced by an equivalence A ≃ B through univalence.

fiberSuccThree

def fiberSuccThree : fiber Nat Nat succ (succ (succ (succ zero)))

The point (2, refl) in the fiber of succ over 3.

fiberSuccFour

def fiberSuccFour : fiber Nat Nat succ (succ (succ (succ (succ zero))))

The point (3, refl) in the fiber of succ over 4.

fiberAddZero

def fiberAddZero (n : Nat) : fiber Nat Nat (add zero) n

The point (n, refl) in the fiber of add zero over n.

fiberNotTrue

def fiberNotTrue : fiber Bool Bool not true

The point (false, refl) in the fiber of not over true.

fiberNotFalse

def fiberNotFalse : fiber Bool Bool not false

The point (true, refl) in the fiber of not over false.

pathToFunNat

def pathToFunNat (p : Nat ≡ Nat) (n : Nat) : Nat

Turns a path Nat ≡ Nat into a function on Nat by transport.

idEquivOptionNat

def idEquivOptionNat : Equiv (Option Nat) (Option Nat)

The identity equivalence on Maybe Nat.

idEquivPairNB

def idEquivPairNB : Equiv (Pair Nat Bool) (Pair Nat Bool)

The identity equivalence on Pair Nat Bool.

fiberIdCenterNat

def fiberIdCenterNat (n : Nat) : fiber Nat Nat (fun (x : Nat) => x) n

The canonical point (n, refl) in the fiber of the identity on Nat over n.

fiberIdCenterBool

def fiberIdCenterBool (b : Bool) : fiber Bool Bool (fun (x : Bool) => x) b

The canonical point (b, refl) in the fiber of the identity on Bool over b.

pathSym

def pathSym {A B : Type} (p : A ≡ B) : B ≡ A

Inverts a path between types.

equivTransPath

def equivTransPath {A B C : Type} (p : A ≡ B) (q : B ≡ C) : A ≡ C

Composes two paths between types.

transportConstType

def transportConstType {A : Type} (a : A) : transport (fun i => A) a ≡ a

Transporting along a constant type family is the identity.

uaIdCompute

def uaIdCompute {A : Type} (a : A) : transport (ua (idEquiv A)) a ≡ a

Transporting along ua of the identity equivalence is the identity.

equivForwardPath

def equivForwardPath {A B : Type} (e1 : Equiv A B) (e2 : Equiv A B) (h : (a : A) -> fst e1 a ≡ fst e2 a) : fst e1 ≡ fst e2

Two equivalences with pointwise equal forward functions have path-equal forward functions, by function extensionality.

transportConstUa

def transportConstUa {A B C : Type} (e : Equiv A B) (c : C) : transport (fun i => C) c ≡ c

Transporting along a constant type family is the identity, regardless of the given equivalence.

idEquivEitherNB

def idEquivEitherNB : Equiv (Either Nat Bool) (Either Nat Bool)

The identity equivalence on Either Nat Bool.

fiberRefl_succ

def fiberRefl_succ (n : Nat) : fiber Nat Nat succ (succ n)

The point (n, refl) in the fiber of succ over succ n.

equivEq

def equivEq {A : Type} : Equiv A A

The identity equivalence on a type, viewed as an equivalence between equal types.

fiberAddSucc2

def fiberAddSucc2 : fiber Nat Nat (add (succ zero)) (succ zero)

The point (0, refl) in the fiber of add 1 over 1.

fiberAddSucc3

def fiberAddSucc3 : fiber Nat Nat (add (succ zero)) (succ (succ zero))

The point (1, refl) in the fiber of add 1 over 2.

fiberAddSucc4

def fiberAddSucc4 : fiber Nat Nat (add (succ zero)) (succ (succ (succ zero)))

The point (2, refl) in the fiber of add 1 over 3.

fiberSuccFive

def fiberSuccFive : fiber Nat Nat succ (succ (succ (succ (succ (succ zero)))))

The point (4, refl) in the fiber of succ over 5.

fiberSuccSix

def fiberSuccSix : fiber Nat Nat succ (succ (succ (succ (succ (succ (succ zero))))))

The point (5, refl) in the fiber of succ over 6.

compEquivFun

def compEquivFun {A B C : Type} (e1 : Equiv A B) (e2 : Equiv B C) (a : A) : C

Composes the forward functions of two equivalences.

compEquivPath

def compEquivPath {A B C : Type} (e1 : Equiv A B) (e2 : Equiv B C) : A ≡ C

The path A ≡ C obtained by composing the univalence paths of two equivalences.

fiberConstCenter

def fiberConstCenter (A : Type) (B : Type) (b : B) (a : A) : fiber A B (fun (_ : A) => b) b

Any a gives a point (a, refl) in the fiber of a constant function over its value.

fiberSucc

def fiberSucc (n : Nat) : fiber Nat Nat succ (succ n)

The point (n, refl) in the fiber of succ over succ n.

isEquivId

def isEquivId (A : Type) : isEquiv A A (fun (x : A) => x)

The identity function is an equivalence.

equivToIsoFun

def equivToIsoFun {A B : Type} (e : Equiv A B) : A -> B

The forward function of an equivalence, viewed as half of an isomorphism.

equivToIsoInv

def equivToIsoInv {A B : Type} (e : Equiv A B) : B -> A

The inverse function of an equivalence, viewed as half of an isomorphism.

isoToEquiv_id

def isoToEquiv_id (A : Type) : Equiv A A

The equivalence induced by the identity isomorphism, namely idEquiv.

equivPreservesIsProp

def equivPreservesIsProp {A B : Type} (e : Equiv A B) (h : isProp A) : isProp B

Equivalences preserve being a proposition: if A is a proposition and A ≃ B, then B is a proposition.

equivProdFun

def equivProdFun {A A2 B B2 : Type} (eA : Equiv A A2) (eB : Equiv B B2) (p : A × B) : A2 × B2

The forward function of the product of two equivalences, acting componentwise.

equivProdInv

def equivProdInv {A A2 B B2 : Type} (eA : Equiv A A2) (eB : Equiv B B2) (p : A2 × B2) : A × B

The inverse function of the product of two equivalences, acting componentwise.

equivFunPost

def equivFunPost {A B B2 : Type} (e : Equiv B B2) (f : A -> B) : A -> B2

Post-composes a function with the forward function of an equivalence.

equivFunPostInv

def equivFunPostInv {A B B2 : Type} (e : Equiv B B2) (f : A -> B2) : A -> B

Post-composes a function with the inverse of an equivalence.

equivPreservesContr_id

def equivPreservesContr_id : isContr Unit

Unit is contractible, obtained by transferring isContrUnit along the identity equivalence.

pathToFunNotPath

def pathToFunNotPath (b : Bool) : pathToFun Bool Bool (ua notEquiv) b ≡ not b

pathToFun along ua notEquiv computes to not.

uaIdProd

def uaIdProd (A : Type) (B : Type) (p : A × B) : transport (ua (idEquiv (A × B))) p ≡ p

Transporting a pair along ua of the identity equivalence on a product leaves it unchanged.

uaIdFun

def uaIdFun (A : Type) (B : Type) (f : A -> B) : transport (ua (idEquiv (A -> B))) f ≡ f

Transporting a function along ua of the identity equivalence on a function type leaves it unchanged.

fiberAdd0_at

def fiberAdd0_at (n : Nat) : fiber Nat Nat (add zero) n

The point (n, refl) in the fiber of add zero over n.

fiberIdOption

def fiberIdOption (mx : Option Nat) : fiber (Option Nat) (Option Nat) (fun (x : Option Nat) => x) mx

The canonical point (mx, refl) in the fiber of the identity on Maybe Nat over mx.

isoLem

def isoLem {A : Type} {B : Type} (f : A -> B) (g : B -> A) (s : (y : B) -> f (g y) ≡ y) (t : (x : A) -> g (f x) ≡ x) (y : B) (x0 : A) (x1 : A) (p0 : f x0 ≡ y) (p1 : f x1 ≡ y) : PathP (fun (i : I) => fiber A B f y) (x0, p0) (x1, p1)

Key lemma for isoToIsEquiv: given an isomorphism, any two points of a fiber of f are connected by a path.

isoToIsEquiv

def isoToIsEquiv {A : Type} {B : Type} (f : A -> B) (g : B -> A) (s : (y : B) -> f (g y) ≡ y) (t : (x : A) -> g (f x) ≡ x) : isEquiv A B f

An isomorphism (functions both ways with section and retraction) makes the forward function an equivalence.

isoToEquiv

def isoToEquiv {A : Type} {B : Type} (f : A -> B) (g : B -> A) (s : (y : B) -> f (g y) ≡ y) (t : (x : A) -> g (f x) ≡ x) : Equiv A B

Builds an equivalence from an isomorphism.

isoToPath

def isoToPath {A : Type} {B : Type} (f : A -> B) (g : B -> A) (s : (y : B) -> f (g y) ≡ y) (t : (x : A) -> g (f x) ≡ x) : A ≡ B

Builds a path between types from an isomorphism, via univalence.