Martin Escardo Notion of equivalence and its basic properties. \begin{code} {-# OPTIONS --safe --without-K #-} module UF.Equiv where open import MLTT.Spartan open import MLTT.Unit-Properties open import UF.Base open import UF.Retracts open import UF.Subsingletons \end{code} We take Joyal's version of the notion of equivalence as the primary one because it is more symmetrical. \begin{code} is-equiv : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } โ (X โ Y) โ ๐ค โ ๐ฅ ฬ is-equiv f = has-section f ร is-section f inverse : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } (f : X โ Y) โ is-equiv f โ (Y โ X) inverse f = prโ โ prโ equivs-have-sections : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } (f : X โ Y) โ is-equiv f โ has-section f equivs-have-sections f = prโ equivs-are-sections : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } (f : X โ Y) โ is-equiv f โ is-section f equivs-are-sections f = prโ section-retraction-equiv : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } (f : X โ Y) โ has-section f โ is-section f โ is-equiv f section-retraction-equiv f hr hs = (hr , hs) equivs-are-lc : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } (f : X โ Y) โ is-equiv f โ left-cancellable f equivs-are-lc f e = sections-are-lc f (equivs-are-sections f e) _โ_ : ๐ค ฬ โ ๐ฅ ฬ โ ๐ค โ ๐ฅ ฬ X โ Y = ฮฃ f ๊ (X โ Y) , is-equiv f Aut : ๐ค ฬ โ ๐ค ฬ Aut X = (X โ X) id-is-equiv : (X : ๐ค ฬ ) โ is-equiv (id {๐ค} {X}) id-is-equiv X = (id , ฮป x โ refl) , (id , ฮป x โ refl) โ-refl : (X : ๐ค ฬ ) โ X โ X โ-refl X = id , id-is-equiv X ๐๐ : {X : ๐ค ฬ } โ X โ X ๐๐ = โ-refl _ โ-is-equiv : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } {Z : ๐ฆ ฬ } {f : X โ Y} {f' : Y โ Z} โ is-equiv f โ is-equiv f' โ is-equiv (f' โ f) โ-is-equiv {๐ค} {๐ฅ} {๐ฆ} {X} {Y} {Z} {f} {f'} ((g , fg) , (h , hf)) ((g' , fg') , (h' , hf')) = (g โ g' , fg'') , (h โ h' , hf'') where fg'' : (z : Z) โ f' (f (g (g' z))) ๏ผ z fg'' z = ap f' (fg (g' z)) โ fg' z hf'' : (x : X) โ h (h' (f' (f x))) ๏ผ x hf'' x = ap h (hf' (f x)) โ hf x \end{code} For type-checking efficiency reasons: \begin{code} โ-is-equiv-abstract : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } {Z : ๐ฆ ฬ } {f : X โ Y} {f' : Y โ Z} โ is-equiv f โ is-equiv f' โ is-equiv (f' โ f) โ-is-equiv-abstract {๐ค} {๐ฅ} {๐ฆ} {X} {Y} {Z} {f} {f'} = ฮณ where abstract ฮณ : is-equiv f โ is-equiv f' โ is-equiv (f' โ f) ฮณ = โ-is-equiv โ-comp : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } {Z : ๐ฆ ฬ } โ X โ Y โ Y โ Z โ X โ Z โ-comp {๐ค} {๐ฅ} {๐ฆ} {X} {Y} {Z} (f , d) (f' , e) = f' โ f , โ-is-equiv d e _โ_ : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } {Z : ๐ฆ ฬ } โ X โ Y โ Y โ Z โ X โ Z _โ_ = โ-comp _โโจ_โฉ_ : (X : ๐ค ฬ ) {Y : ๐ฅ ฬ } {Z : ๐ฆ ฬ } โ X โ Y โ Y โ Z โ X โ Z _ โโจ d โฉ e = d โ e _โ : (X : ๐ค ฬ ) โ X โ X _โ = โ-refl Eqtofun : (X : ๐ค ฬ ) (Y : ๐ฅ ฬ ) โ X โ Y โ X โ Y Eqtofun X Y (f , _) = f eqtofun โ_โ : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } โ X โ Y โ X โ Y eqtofun = Eqtofun _ _ โ_โ = eqtofun eqtofun- โโ-is-equiv โ_โ-is-equiv : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } (e : X โ Y) โ is-equiv โ e โ eqtofun- = prโ โโ-is-equiv = eqtofun- โ_โ-is-equiv = โโ-is-equiv back-eqtofun โ_โโปยน : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } โ X โ Y โ Y โ X back-eqtofun e = prโ (prโ (prโ e)) โ_โโปยน = back-eqtofun idtoeq : (X Y : ๐ค ฬ ) โ X ๏ผ Y โ X โ Y idtoeq X Y p = transport (X โ_) p (โ-refl X) idtoeq-traditional : (X Y : ๐ค ฬ ) โ X ๏ผ Y โ X โ Y idtoeq-traditional X _ refl = โ-refl X \end{code} We would have a definitional equality if we had defined the traditional one using J (based), but because of the idiosyncracies of Agda, we don't with the current definition: \begin{code} eqtoeq-agreement : (X Y : ๐ค ฬ ) (p : X ๏ผ Y) โ idtoeq X Y p ๏ผ idtoeq-traditional X Y p eqtoeq-agreement {๐ค} X _ refl = refl idtofun : (X Y : ๐ค ฬ ) โ X ๏ผ Y โ X โ Y idtofun X Y p = โ idtoeq X Y p โ idtofun' : {X Y : ๐ค ฬ } โ X ๏ผ Y โ X โ Y idtofun' = idtofun _ _ idtofun-agreement : (X Y : ๐ค ฬ ) (p : X ๏ผ Y) โ idtofun X Y p ๏ผ Idtofun p idtofun-agreement X Y refl = refl equiv-closed-under-โผ : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } (f g : X โ Y) โ is-equiv f โ g โผ f โ is-equiv g equiv-closed-under-โผ {๐ค} {๐ฅ} {X} {Y} f g (hass , hasr) h = has-section-closed-under-โผ f g hass h , is-section-closed-under-โผ f g hasr h equiv-closed-under-โผ' : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } {f g : X โ Y} โ is-equiv f โ f โผ g โ is-equiv g equiv-closed-under-โผ' ise h = equiv-closed-under-โผ _ _ ise (ฮป x โ (h x)โปยน) invertible : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } โ (X โ Y) โ ๐ค โ ๐ฅ ฬ invertible f = ฮฃ g ๊ (codomain f โ domain f), (g โ f โผ id) ร (f โ g โผ id) qinv = invertible inverses-are-retractions : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } (f : X โ Y) (e : is-equiv f) โ inverse f e โ f โผ id inverses-are-retractions f ((g , ฮต) , (g' , ฮท)) = ฮท' where ฮท' : g โ f โผ id ฮท' x = g (f x) ๏ผโจ (ฮท (g (f x)))โปยน โฉ g' (f (g (f x))) ๏ผโจ ap g' (ฮต (f x)) โฉ g' (f x) ๏ผโจ ฮท x โฉ x โ inverses-are-retractions' : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } (๐ : X โ Y) โ โ ๐ โโปยน โ โ ๐ โ โผ id inverses-are-retractions' (f , e) = inverses-are-retractions f e equivs-are-qinvs : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } (f : X โ Y) โ is-equiv f โ qinv f equivs-are-qinvs {๐ค} {๐ฅ} {X} {Y} f e@((g , ฮต) , (g' , ฮท)) = g , inverses-are-retractions f e , ฮต naive-inverses-are-sections : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } (f : X โ Y) (e : is-equiv f) โ f โ inverse f e โผ id naive-inverses-are-sections f ((g' , ฮต) , (g , ฮท)) = ฮต inverses-are-sections : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } (f : X โ Y) (e : is-equiv f) โ f โ inverse f e โผ id inverses-are-sections f e@((g , ฮต) , (g' , ฮท)) = ฮต' where ฮต' : f โ g โผ id ฮต' y = f (g y) ๏ผโจ (ฮต (f (g y)))โปยน โฉ f (g (f (g y))) ๏ผโจ ap f (inverses-are-retractions f e (g y)) โฉ f (g y) ๏ผโจ ฮต y โฉ y โ inverses-are-sections' : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } (๐ : X โ Y) โ โ ๐ โ โ โ ๐ โโปยน โผ id inverses-are-sections' (f , e) = inverses-are-sections f e inverses-are-equivs : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } (f : X โ Y) (e : is-equiv f) โ is-equiv (inverse f e) inverses-are-equivs f e = (f , inverses-are-retractions f e) , (f , inverses-are-sections f e) โโโปยน-is-equiv : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } (e : X โ Y) โ is-equiv โ e โโปยน โโโปยน-is-equiv (f , i) = inverses-are-equivs f i โ_โโปยน-is-equiv : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } (e : X โ Y) โ is-equiv โ e โโปยน โ_โโปยน-is-equiv = โโโปยน-is-equiv inversion-involutive : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } (f : X โ Y) (e : is-equiv f) โ inverse (inverse f e) (inverses-are-equivs f e) ๏ผ f inversion-involutive f e = refl \end{code} That the above proof is refl is an accident of our choice of notion of equivalence as primary. \begin{code} qinvs-are-equivs : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } (f : X โ Y) โ qinv f โ is-equiv f qinvs-are-equivs f (g , (gf , fg)) = (g , fg) , (g , gf) qinveq : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } (f : X โ Y) โ qinv f โ X โ Y qinveq f q = (f , qinvs-are-equivs f q) lc-split-surjections-are-equivs : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } (f : X โ Y) โ left-cancellable f โ ((y : Y) โ ฮฃ x ๊ X , f x ๏ผ y) โ is-equiv f lc-split-surjections-are-equivs f l s = qinvs-are-equivs f (g , ฮท , ฮต) where g : codomain f โ domain f g y = prโ (s y) ฮต : f โ g โผ id ฮต y = prโ (s y) ฮท : g โ f โผ id ฮท x = l p where p : f (g (f x)) ๏ผ f x p = ฮต (f x) โ-sym : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } โ X โ Y โ Y โ X โ-sym {๐ค} {๐ฅ} {X} {Y} (f , e) = inverse f e , inverses-are-equivs f e โ-sym-is-linv : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } (๐ฏ : X โ Y) โ โ ๐ฏ โโปยน โ โ ๐ฏ โ โผ id โ-sym-is-linv (f , e) x = inverses-are-retractions f e x โ-sym-is-rinv : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } (๐ฏ : X โ Y) โ โ ๐ฏ โ โ โ ๐ฏ โโปยน โผ id โ-sym-is-rinv (f , e) y = inverses-are-sections f e y โ-gives-โ : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } โ X โ Y โ X โ Y โ-gives-โ (f , (g , fg) , (h , hf)) = h , f , hf โ-gives-โท : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } โ X โ Y โ Y โ X โ-gives-โท (f , (g , fg) , (h , hf)) = f , g , fg Id-retract-l : {X Y : ๐ค ฬ } โ X ๏ผ Y โ retract X of Y Id-retract-l p = โ-gives-โ (idtoeq (lhs p) (rhs p) p) Id-retract-r : {X Y : ๐ค ฬ } โ X ๏ผ Y โ retract Y of X Id-retract-r p = โ-gives-โท (idtoeq (lhs p) (rhs p) p) equiv-to-prop : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } โ Y โ X โ is-prop X โ is-prop Y equiv-to-prop e = retract-of-prop (โ-gives-โ e) equiv-to-singleton : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } โ Y โ X โ is-singleton X โ is-singleton Y equiv-to-singleton e = retract-of-singleton (โ-gives-โ e) equiv-to-singleton' : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } โ X โ Y โ is-singleton X โ is-singleton Y equiv-to-singleton' e = retract-of-singleton (โ-gives-โท e) singleton-types-are-equivalent : {X : ๐ค ฬ } (x : X) โ singleton-type x โ singleton-type' x singleton-types-are-equivalent x = f , ((g , fg) , (g , gf)) where f : singleton-type x โ singleton-type' x f (y , p) = y , (p โปยน) g : singleton-type' x โ singleton-type x g (y , p) = y , (p โปยน) fg : f โ g โผ id fg (y , p) = ap (ฮป - โ y , -) (โปยน-involutive p) gf : g โ f โผ id gf (y , p) = ap (ฮป - โ y , -) (โปยน-involutive p) singleton-types'-are-singletons : {X : ๐ค ฬ } (x : X) โ is-singleton (singleton-type' x) singleton-types'-are-singletons x = retract-of-singleton (โ-gives-โท (singleton-types-are-equivalent x)) (singleton-types-are-singletons x) singleton-types'-are-props : {X : ๐ค ฬ } (x : X) โ is-prop (singleton-type' x) singleton-types'-are-props x = singletons-are-props (singleton-types'-are-singletons x) transports-are-equivs : {X : ๐ค ฬ } {A : X โ ๐ฅ ฬ } {x y : X} (p : x ๏ผ y) โ is-equiv (transport A p) transports-are-equivs refl = id-is-equiv _ transport-โ : {X : ๐ค ฬ } (A : X โ ๐ฅ ฬ ) {x y : X} (p : x ๏ผ y) โ A x โ A y transport-โ A p = transport A p , transports-are-equivs p back-transports-are-equivs : {X : ๐ค ฬ } {A : X โ ๐ฅ ฬ } {x y : X} (p : x ๏ผ y) โ is-equiv (transportโปยน A p) back-transports-are-equivs p = transports-are-equivs (p โปยน) is-vv-equiv : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } โ (X โ Y) โ ๐ค โ ๐ฅ ฬ is-vv-equiv f = each-fiber-of f is-singleton _ : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } (f : X โ Y) โ is-vv-equiv f ๏ผ (ฮ y ๊ Y , โ! x ๊ X , f x ๏ผ y) _ = ฮป f โ refl vv-equivs-are-equivs : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } (f : X โ Y) โ is-vv-equiv f โ is-equiv f vv-equivs-are-equivs {๐ค} {๐ฅ} {X} {Y} f ฯ = (g , fg) , (g , gf) where ฯ' : (y : Y) โ ฮฃ c ๊ (ฮฃ x ๊ X , f x ๏ผ y) , ((ฯ : ฮฃ x ๊ X , f x ๏ผ y) โ c ๏ผ ฯ) ฯ' = ฯ c : (y : Y) โ ฮฃ x ๊ X , f x ๏ผ y c y = prโ (ฯ y) d : (y : Y) โ (ฯ : ฮฃ x ๊ X , f x ๏ผ y) โ c y ๏ผ ฯ d y = prโ (ฯ y) g : Y โ X g y = prโ (c y) fg : (y : Y) โ f (g y) ๏ผ y fg y = prโ (c y) e : (x : X) โ g (f x) , fg (f x) ๏ผ x , refl e x = d (f x) (x , refl) gf : (x : X) โ g (f x) ๏ผ x gf x = ap prโ (e x) fiber' : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } (f : X โ Y) โ Y โ ๐ค โ ๐ฅ ฬ fiber' f y = ฮฃ x ๊ domain f , y ๏ผ f x fiber-lemma : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } (f : X โ Y) (y : Y) โ fiber f y โ fiber' f y fiber-lemma f y = g , (h , gh) , (h , hg) where g : fiber f y โ fiber' f y g (x , p) = x , (p โปยน) h : fiber' f y โ fiber f y h (x , p) = x , (p โปยน) hg : โ ฯ โ h (g ฯ) ๏ผ ฯ hg (x , refl) = refl gh : โ ฯ โ g (h ฯ) ๏ผ ฯ gh (x , refl) = refl is-hae : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } โ (X โ Y) โ ๐ค โ ๐ฅ ฬ is-hae {๐ค} {๐ฅ} {X} {Y} f = ฮฃ g ๊ (Y โ X) , ฮฃ ฮท ๊ g โ f โผ id , ฮฃ ฮต ๊ f โ g โผ id , ฮ x ๊ X , ap f (ฮท x) ๏ผ ฮต (f x) haes-are-equivs : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } (f : X โ Y) โ is-hae f โ is-equiv f haes-are-equivs {๐ค} {๐ฅ} {X} f (g , ฮท , ฮต , ฯ) = qinvs-are-equivs f (g , ฮท , ฮต) id-homotopies-are-natural : {X : ๐ค ฬ } (h : X โ X) (ฮท : h โผ id) {x : X} โ ฮท (h x) ๏ผ ap h (ฮท x) id-homotopies-are-natural h ฮท {x} = ฮท (h x) ๏ผโจ refl โฉ ฮท (h x) โ refl ๏ผโจ I โฉ ฮท (h x) โ (ฮท x โ (ฮท x)โปยน) ๏ผโจ II โฉ ฮท (h x) โ ฮท x โ (ฮท x)โปยน ๏ผโจ III โฉ ฮท (h x) โ ap id (ฮท x) โ (ฮท x)โปยน ๏ผโจ IV โฉ ap h (ฮท x) โ where I = ap (ฮป - โ ฮท (h x) โ -) ((trans-sym' (ฮท x))โปยน) II = (โassoc (ฮท (h x)) (ฮท x) (ฮท x โปยน))โปยน III = ap (ฮป - โ ฮท (h x) โ - โ (ฮท x)โปยน) ((ap-id-is-id' (ฮท x))) IV = homotopies-are-natural' h id ฮท {h x} {x} {ฮท x} half-adjoint-condition : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } (f : X โ Y) (e : is-equiv f) (x : X) โ ap f (inverses-are-retractions f e x) ๏ผ inverses-are-sections f e (f x) half-adjoint-condition {๐ค} {๐ฅ} {X} {Y} f e@((g , ฮต) , (g' , ฮท)) = ฯ where ฮท' : g โ f โผ id ฮท' = inverses-are-retractions f e ฮต' : f โ g โผ id ฮต' = inverses-are-sections f e a : (x : X) โ ฮท' (g (f x)) ๏ผ ap g (ap f (ฮท' x)) a x = ฮท' (g (f x)) ๏ผโจ id-homotopies-are-natural (g โ f) ฮท' โฉ ap (g โ f) (ฮท' x) ๏ผโจ (ap-ap f g (ฮท' x))โปยน โฉ ap g (ap f (ฮท' x)) โ b : (x : X) โ ap f (ฮท' (g (f x))) โ ฮต (f x) ๏ผ ฮต (f (g (f x))) โ ap f (ฮท' x) b x = ap f (ฮท' (g (f x))) โ ฮต (f x) ๏ผโจ I โฉ ap f (ap g (ap f (ฮท' x))) โ ฮต (f x) ๏ผโจ II โฉ ap (f โ g) (ap f (ฮท' x)) โ ฮต (f x) ๏ผโจ III โฉ ฮต (f (g (f x))) โ ap id (ap f (ฮท' x)) ๏ผโจ IV โฉ ฮต (f (g (f x))) โ ap f (ฮท' x) โ where I = ap (ฮป - โ - โ ฮต (f x)) (ap (ap f) (a x)) II = ap (ฮป - โ - โ ฮต (f x)) (ap-ap g f (ap f (ฮท' x))) III = (homotopies-are-natural (f โ g) id ฮต {_} {_} {ap f (ฮท' x)})โปยน IV = ap (ฮป - โ ฮต (f (g (f x))) โ -) (ap-ap f id (ฮท' x)) ฯ : (x : X) โ ap f (ฮท' x) ๏ผ ฮต' (f x) ฯ x = ap f (ฮท' x) ๏ผโจ I โฉ refl โ ap f (ฮท' x) ๏ผโจ II โฉ (ฮต (f (g (f x))))โปยน โ ฮต (f (g (f x))) โ ap f (ฮท' x) ๏ผโจ III โฉ (ฮต (f (g (f x))))โปยน โ (ฮต (f (g (f x))) โ ap f (ฮท' x)) ๏ผโจ IV โฉ (ฮต (f (g (f x))))โปยน โ (ap f (ฮท' (g (f x))) โ ฮต (f x)) ๏ผโจ refl โฉ ฮต' (f x) โ where I = refl-left-neutral โปยน II = ap (ฮป - โ - โ ap f (ฮท' x)) ((trans-sym (ฮต (f (g (f x)))))โปยน) III = โassoc ((ฮต (f (g (f x))))โปยน) (ฮต (f (g (f x)))) (ap f (ฮท' x)) IV = ap (ฮป - โ (ฮต (f (g (f x))))โปยน โ -) (b x)โปยน equivs-are-haes : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } (f : X โ Y) โ is-equiv f โ is-hae f equivs-are-haes {๐ค} {๐ฅ} {X} {Y} f e@((g , ฮต) , (g' , ฮท)) = inverse f e , inverses-are-retractions f e , inverses-are-sections f e , half-adjoint-condition f e qinvs-are-haes : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } (f : X โ Y) โ qinv f โ is-hae f qinvs-are-haes {๐ค} {๐ฅ} {X} {Y} f = equivs-are-haes f โ qinvs-are-equivs f \end{code} The following could be defined by combining functions we already have, but a proof by path induction is direct: \begin{code} identifications-in-fibers : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } (f : X โ Y) (y : Y) (x x' : X) (p : f x ๏ผ y) (p' : f x' ๏ผ y) โ (ฮฃ ฮณ ๊ x ๏ผ x' , ap f ฮณ โ p' ๏ผ p) โ (x , p) ๏ผ (x' , p') identifications-in-fibers f .(f x) x x refl p' (refl , r) = g where g : x , refl ๏ผ x , p' g = ap (ฮป - โ (x , -)) (r โปยน โ refl-left-neutral) \end{code} Using this we see that half adjoint equivalences have singleton fibers. \begin{code} haes-are-vv-equivs : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } (f : X โ Y) โ is-hae f โ is-vv-equiv f haes-are-vv-equivs {๐ค} {๐ฅ} {X} f (g , ฮท , ฮต , ฯ) y = (c , ฮป ฯ โ ฮฑ (prโ ฯ) (prโ ฯ)) where c : fiber f y c = (g y , ฮต y) ฮฑ : (x : X) (p : f x ๏ผ y) โ c ๏ผ (x , p) ฮฑ x p = ฯ where ฮณ : g y ๏ผ x ฮณ = (ap g p)โปยน โ ฮท x q : ap f ฮณ โ p ๏ผ ฮต y q = ap f ฮณ โ p ๏ผโจ refl โฉ ap f ((ap g p)โปยน โ ฮท x) โ p ๏ผโจ I โฉ ap f ((ap g p)โปยน) โ ap f (ฮท x) โ p ๏ผโจ II โฉ ap f (ap g (p โปยน)) โ ap f (ฮท x) โ p ๏ผโจ III โฉ ap f (ap g (p โปยน)) โ ฮต (f x) โ p ๏ผโจ IV โฉ ap (f โ g) (p โปยน) โ ฮต (f x) โ p ๏ผโจ V โฉ ฮต y โ ap id (p โปยน) โ p ๏ผโจ VI โฉ ฮต y โ p โปยน โ p ๏ผโจ VII โฉ ฮต y โ (p โปยน โ p) ๏ผโจ VIII โฉ ฮต y โ refl ๏ผโจ refl โฉ ฮต y โ where I = ap (ฮป - โ - โ p) (ap-โ f ((ap g p)โปยน) (ฮท x)) II = ap (ฮป - โ ap f - โ ap f (ฮท x) โ p) (ap-sym g p) III = ap (ฮป - โ ap f (ap g (p โปยน)) โ - โ p) (ฯ x) IV = ap (ฮป - โ - โ ฮต (f x) โ p) (ap-ap g f (p โปยน)) V = ap (ฮป - โ - โ p) (homotopies-are-natural (f โ g) id ฮต {y} {f x} {p โปยน})โปยน VI = ap (ฮป - โ ฮต y โ - โ p) (ap-id-is-id (p โปยน)) VII = โassoc (ฮต y) (p โปยน) p VIII = ap (ฮป - โ ฮต y โ -) (trans-sym p) ฯ : g y , ฮต y ๏ผ x , p ฯ = identifications-in-fibers f y (g y) x (ฮต y) p (ฮณ , q) \end{code} Here are some corollaries: \begin{code} qinvs-are-vv-equivs : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } (f : X โ Y) โ qinv f โ is-vv-equiv f qinvs-are-vv-equivs f q = haes-are-vv-equivs f (qinvs-are-haes f q) equivs-are-vv-equivs : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } (f : X โ Y) โ is-equiv f โ is-vv-equiv f equivs-are-vv-equivs f ie = qinvs-are-vv-equivs f (equivs-are-qinvs f ie) \end{code} We pause to characterize negation and singletons. Recall that ยฌ X and is-empty X are synonyms for the function type X โ ๐. \begin{code} equiv-can-assume-pointed-codomain : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } (f : X โ Y) โ (Y โ is-vv-equiv f) โ is-vv-equiv f equiv-can-assume-pointed-codomain f ฯ y = ฯ y y maps-to-๐-are-equivs : {X : ๐ค ฬ } (f : X โ ๐ {๐ฅ}) โ is-vv-equiv f maps-to-๐-are-equivs f = equiv-can-assume-pointed-codomain f ๐-elim negations-are-equiv-to-๐ : {X : ๐ค ฬ } โ is-empty X โ X โ ๐ negations-are-equiv-to-๐ = (ฮป f โ f , vv-equivs-are-equivs f (maps-to-๐-are-equivs f)) , eqtofun \end{code} Then with functional and propositional extensionality, which follow from univalence, we conclude that ยฌ X = (X โ 0) = (X ๏ผ 0). And similarly, with similar proof: \begin{code} singletons-are-equiv-to-๐ : {X : ๐ค ฬ } โ is-singleton X โ X โ ๐ {๐ฅ} singletons-are-equiv-to-๐ {๐ค} {๐ฅ} {X} = f , g where f : is-singleton X โ X โ ๐ f (xโ , ฯ) = unique-to-๐ , (((ฮป _ โ xโ) , (ฮป x โ (๐-all-โ x)โปยน)) , ((ฮป _ โ xโ) , ฯ)) g : X โ ๐ โ is-singleton X g (f , (s , fs) , (r , rf)) = retract-of-singleton (r , f , rf) ๐-is-singleton \end{code} The following again could be defined by combining functions we already have: \begin{code} from-identifications-in-fibers : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } (f : X โ Y) (y : Y) (x x' : X) (p : f x ๏ผ y) (p' : f x' ๏ผ y) โ (x , p) ๏ผ (x' , p') โ ฮฃ ฮณ ๊ x ๏ผ x' , ap f ฮณ โ p' ๏ผ p from-identifications-in-fibers f .(f x) x x refl refl refl = refl , refl ฮท-pif : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } (f : X โ Y) (y : Y) (x x' : X) (p : f x ๏ผ y) (p' : f x' ๏ผ y) โ from-identifications-in-fibers f y x x' p p' โ identifications-in-fibers f y x x' p p' โผ id ฮท-pif f .(f x) x x _ refl (refl , refl) = refl \end{code} Then the following is a consequence of natural-section-is-section, but also has a direct proof by path induction: \begin{code} ฮต-pif : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } (f : X โ Y) (y : Y) (x x' : X) (p : f x ๏ผ y) (p' : f x' ๏ผ y) โ identifications-in-fibers f y x x' p p' โ from-identifications-in-fibers f y x x' p p' โผ id ฮต-pif f .(f x) x x refl refl refl = refl prโ-is-vv-equiv : (X : ๐ค ฬ ) (Y : X โ ๐ฅ ฬ ) โ ((x : X) โ is-singleton (Y x)) โ is-vv-equiv (prโ {๐ค} {๐ฅ} {X} {Y}) prโ-is-vv-equiv {๐ค} {๐ฅ} X Y iss x = g where c : fiber prโ x c = (x , prโ (iss x)) , refl p : (y : Y x) โ prโ (iss x) ๏ผ y p = prโ (iss x) f : (w : ฮฃ ฯ ๊ ฮฃ Y , prโ ฯ ๏ผ x) โ c ๏ผ w f ((x , y) , refl) = ap (ฮป - โ (x , -) , refl) (p y) g : is-singleton (fiber prโ x) g = c , f prโ-is-equiv : (X : ๐ค ฬ ) (Y : X โ ๐ฅ ฬ ) โ ((x : X) โ is-singleton (Y x)) โ is-equiv (prโ {๐ค} {๐ฅ} {X} {Y}) prโ-is-equiv X Y iss = vv-equivs-are-equivs prโ (prโ-is-vv-equiv X Y iss) prโ-is-vv-equiv-converse : {X : ๐ค ฬ } {A : X โ ๐ฅ ฬ } โ is-vv-equiv (prโ {๐ค} {๐ฅ} {X} {A}) โ ((x : X) โ is-singleton (A x)) prโ-is-vv-equiv-converse {๐ค} {๐ฅ} {X} {A} isv x = ฮณ where f : ฮฃ A โ X f = prโ {๐ค} {๐ฅ} {X} {A} s : A x โ fiber f x s a = (x , a) , refl r : fiber f x โ A x r ((x , a) , refl) = a rs : (a : A x) โ r (s a) ๏ผ a rs a = refl ฮณ : is-singleton (A x) ฮณ = retract-of-singleton (r , s , rs) (isv x) logical-equivs-of-props-are-equivs : {P : ๐ค ฬ } {Q : ๐ฅ ฬ } โ is-prop P โ is-prop Q โ (f : P โ Q) โ (Q โ P) โ is-equiv f logical-equivs-of-props-are-equivs i j f g = qinvs-are-equivs f (g , (ฮป x โ i (g (f x)) x) , (ฮป x โ j (f (g x)) x)) logically-equivalent-props-are-equivalent : {P : ๐ค ฬ } {Q : ๐ฅ ฬ } โ is-prop P โ is-prop Q โ (P โ Q) โ (Q โ P) โ P โ Q logically-equivalent-props-are-equivalent i j f g = (f , logical-equivs-of-props-are-equivs i j f g) \end{code} 5th March 2019. A more direct proof that quasi-invertible maps are Voevodky equivalences (have contractible fibers). \begin{code} qinvs-are-vv-equivs' : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } (f : X โ Y) โ qinv f โ is-vv-equiv f qinvs-are-vv-equivs' {๐ค} {๐ฅ} {X} {Y} f (g , ฮท , ฮต) yโ = ฮณ where a : (y : Y) โ (f (g y) ๏ผ yโ) โ (y ๏ผ yโ) a y = r , s , rs where r : y ๏ผ yโ โ f (g y) ๏ผ yโ r p = ฮต y โ p s : f (g y) ๏ผ yโ โ y ๏ผ yโ s q = (ฮต y)โปยน โ q rs : (q : f (g y) ๏ผ yโ) โ r (s q) ๏ผ q rs q = ฮต y โ ((ฮต y)โปยน โ q) ๏ผโจ (โassoc (ฮต y) ((ฮต y)โปยน) q)โปยน โฉ (ฮต y โ (ฮต y)โปยน) โ q ๏ผโจ ap (_โ q) ((sym-is-inverse' (ฮต y))โปยน) โฉ refl โ q ๏ผโจ refl-left-neutral โฉ q โ b : fiber f yโ โ singleton-type' yโ b = (ฮฃ x ๊ X , f x ๏ผ yโ) โโจ ฮฃ-reindex-retract g (f , ฮท) โฉ (ฮฃ y ๊ Y , f (g y) ๏ผ yโ) โโจ ฮฃ-retract (ฮป y โ f (g y) ๏ผ yโ) (_๏ผ yโ) a โฉ (ฮฃ y ๊ Y , y ๏ผ yโ) โ ฮณ : is-singleton (fiber f yโ) ฮณ = retract-of-singleton b (singleton-types'-are-singletons yโ) maps-of-singletons-are-equivs : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } (f : X โ Y) โ is-singleton X โ is-singleton Y โ is-equiv f maps-of-singletons-are-equivs f (c , ฯ) (d , ฮณ) = ((ฮป y โ c) , (ฮป x โ f c ๏ผโจ singletons-are-props (d , ฮณ) (f c) x โฉ x โ)) , ((ฮป y โ c) , ฯ) is-fiberwise-equiv : {X : ๐ค ฬ } {A : X โ ๐ฅ ฬ } {B : X โ ๐ฆ ฬ } โ Nat A B โ ๐ค โ ๐ฅ โ ๐ฆ ฬ is-fiberwise-equiv ฯ = โ x โ is-equiv (ฯ x) \end{code} Added 1st December 2019. Sometimes it is is convenient to reason with quasi-equivalences directly, in particular if we want to avoid function extensionality, and we introduce some machinery for this. \begin{code} _โ _ : ๐ค ฬ โ ๐ฅ ฬ โ ๐ค โ ๐ฅ ฬ X โ Y = ฮฃ f ๊ (X โ Y) , qinv f id-qinv : (X : ๐ค ฬ ) โ qinv (id {๐ค} {X}) id-qinv X = id , (ฮป x โ refl) , (ฮป x โ refl) โ -refl : (X : ๐ค ฬ ) โ X โ X โ -refl X = id , (id-qinv X) โ-qinv : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } {Z : ๐ฆ ฬ } {f : X โ Y} {f' : Y โ Z} โ qinv f โ qinv f' โ qinv (f' โ f) โ-qinv {๐ค} {๐ฅ} {๐ฆ} {X} {Y} {Z} {f} {f'} = ฮณ where ฮณ : qinv f โ qinv f' โ qinv (f' โ f) ฮณ (g , gf , fg) (g' , gf' , fg') = (g โ g' , gf'' , fg'' ) where fg'' : (z : Z) โ f' (f (g (g' z))) ๏ผ z fg'' z = ap f' (fg (g' z)) โ fg' z gf'' : (x : X) โ g (g' (f' (f x))) ๏ผ x gf'' x = ap g (gf' (f x)) โ gf x โ -comp : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } {Z : ๐ฆ ฬ } โ X โ Y โ Y โ Z โ X โ Z โ -comp {๐ค} {๐ฅ} {๐ฆ} {X} {Y} {Z} (f , d) (f' , e) = f' โ f , โ-qinv d e _โ โจ_โฉ_ : (X : ๐ค ฬ ) {Y : ๐ฅ ฬ } {Z : ๐ฆ ฬ } โ X โ Y โ Y โ Z โ X โ Z _ โ โจ d โฉ e = โ -comp d e _โพ : (X : ๐ค ฬ ) โ X โ X _โพ = โ -refl \end{code} Added by Tom de Jong, November 2021. \begin{code} โ-2-out-of-3-right : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } {Z : ๐ฆ ฬ } โ {f : X โ Y} {g : Y โ Z} โ is-equiv f โ is-equiv (g โ f) โ is-equiv g โ-2-out-of-3-right {๐ค} {๐ฅ} {๐ฆ} {X} {Y} {Z} {f} {g} i j = equiv-closed-under-โผ (g โ f โ fโปยน) g k h where ๐ : X โ Y ๐ = (f , i) fโปยน : Y โ X fโปยน = โ ๐ โโปยน k : is-equiv (g โ f โ fโปยน) k = โ-is-equiv (โโโปยน-is-equiv ๐) j h : g โผ g โ f โ fโปยน h y = ap g ((โ-sym-is-rinv ๐ y) โปยน) โ-2-out-of-3-left : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } {Z : ๐ฆ ฬ } โ {f : X โ Y} {g : Y โ Z} โ is-equiv g โ is-equiv (g โ f) โ is-equiv f โ-2-out-of-3-left {๐ค} {๐ฅ} {๐ฆ} {X} {Y} {Z} {f} {g} i j = equiv-closed-under-โผ (gโปยน โ g โ f) f k h where ๐ : Y โ Z ๐ = (g , i) gโปยน : Z โ Y gโปยน = โ ๐ โโปยน k : is-equiv (gโปยน โ g โ f) k = โ-is-equiv j (โโโปยน-is-equiv ๐) h : f โผ gโปยน โ g โ f h x = (โ-sym-is-linv ๐ (f x)) โปยน \end{code} Added by Martin Escardo 2nd November 2023. \begin{code} involutions-are-equivs : {X : ๐ค ฬ } โ (f : X โ X) โ involutive f โ is-equiv f involutions-are-equivs f f-involutive = qinvs-are-equivs f (f , f-involutive , f-involutive) involution-swap : {X : ๐ค ฬ } (f : X โ X) โ involutive f โ {x y : X} โ f x ๏ผ y โ f y ๏ผ x involution-swap f f-involutive {x} {y} e = f y ๏ผโจ ap f (e โปยน) โฉ f (f x) ๏ผโจ f-involutive x โฉ x โ open import UF.Sets involution-swap-โ : {X : ๐ค ฬ } (f : X โ X) โ involutive f โ is-set X โ {x y : X} โ (f x ๏ผ y) โ (f y ๏ผ x) involution-swap-โ f f-involutive X-is-set {x} {y} = qinveq (involution-swap f f-involutive {x} {y}) (involution-swap f f-involutive {y} {x}, I y x , I x y) where I : โ a b โ involution-swap f f-involutive {a} {b} โ (involution-swap f f-involutive {b} {a}) โผ id I a b e = X-is-set _ _ \end{code} Associativities and precedences. \begin{code} infix 0 _โ_ infix 0 _โ _ infix 1 _โ infixr 0 _โโจ_โฉ_ infixl 2 _โ_ infix 1 โ_โ \end{code}