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_trunctype from 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
       

Last updated: 2017-12-02 za 16:47

Emacs 25.2.2 (Org mode 9.1.3)

Validate