HoTT library reference card
Table of Contents
Working with IsHProp and hProp
IsHProp
| Type/Lemma | Name | Location | Comments |
|---|---|---|---|
IsHProp A → Π (x y : A), x = y |
path_ishprop |
Basics.Trunc | |
Π (x y : A), x = y → IsHProp A |
hprop_allpath |
Basics.Trunc | |
IsHProp A <~> Π (x y : A), x = y |
equiv_hrop_allpath |
HProp | |
(A → B) → (B → A) → (A <~> B) |
equiv_iff_hprop |
Basics.Trunc | there is an _uncurried version |
IsHProp A, B → (A → B) → (B → A) → (A = B) |
path_iff_hprop |
TruncType |
Other
equiv_path_trunctypefrom TruncType:(A <~> B) <~> (A = B :> TruncType n)
Equivalences
| Type/Lemma | Name | Location | Comments |
|---|---|---|---|
(Π (b : B), Contr {a : A & f a = b}) -> IsEquiv f |
isequiv_fcontr |
EquivalenceVarieties | A map is an equivalence if it is contractible |
BiInv f -> IsEquiv f |
isequiv_biinv |
EquivalenceVarieties | |
Π (f : A → B) (g : B → A), Sect g f -> Sect f g -> A <~> B |
equiv_adjointify |
Equivalences | A map is an equivalence if you can provide two sections |
