\begin{code}

{-# OPTIONS --without-K --exact-split --safe #-}

module UF-Equiv where

open import SpartanMLTT
open import UF-Base
open import UF-Subsingletons
open import UF-Retracts
open import Unit-Properties

\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

โˆ˜-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

Eq : ๐“ค ฬ‡ โ†’ ๐“ฅ ฬ‡ โ†’ ๐“ค โŠ” ๐“ฅ ฬ‡
Eq = _โ‰ƒ_

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 : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (e : X โ‰ƒ Y) โ†’ is-equiv โŒœ e โŒ
eqtofun-     = prโ‚‚
โŒœโŒ-is-equiv  = eqtofun-

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 (Eq 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-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)โปยน)

qinv : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } โ†’ (X โ†’ Y) โ†’ ๐“ค โŠ” ๐“ฅ ฬ‡
qinv f = ฮฃ g ๊ž‰ (codomain f โ†’ domain f), (g โˆ˜ f โˆผ id) ร— (f โˆ˜ g โˆผ id)

equivs-are-qinvs : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (f : X โ†’ Y) โ†’ is-equiv f โ†’ qinv f
equivs-are-qinvs {๐“ค} {๐“ฅ} {X} {Y} f ((s , fs) , (r , rf)) = s , (sf , fs)
 where
  sf : (x : X) โ†’ s (f x) โ‰ก x
  sf x = s (f x)         โ‰กโŸจ (rf (s (f x)))โปยน โŸฉ
         r (f (s (f x))) โ‰กโŸจ ap r (fs (f x)) โŸฉ
         r (f x)         โ‰กโŸจ rf x โŸฉ
         x               โˆŽ

inverses-are-sections : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (f : X โ†’ Y) (e : is-equiv f)
                      โ†’ f โˆ˜ inverse f e โˆผ id
inverses-are-sections f ((s , fs) , (r , rf)) = fs

inverses-are-retractions : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (f : X โ†’ Y) (e : is-equiv f)
                         โ†’ inverse f e โˆ˜ f โˆผ id
inverses-are-retractions f e = prโ‚ (prโ‚‚ (equivs-are-qinvs 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

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)

pt-pf-equiv : {X : ๐“ค ฬ‡ } (x : X) โ†’ singleton-type x โ‰ƒ singleton-type' x
pt-pf-equiv 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
                                      (prโ‚ (pt-pf-equiv x) ,
                                      (prโ‚ (prโ‚‚ ((pt-pf-equiv 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)

\end{code}

Equivalence of transports.

\begin{code}

transports-are-equivs : {X : ๐“ค ฬ‡ } {A : X โ†’ ๐“ฅ ฬ‡ } {x y : X} (p : x โ‰ก y)
                      โ†’ is-equiv (transport A p)
transports-are-equivs refl = id-is-equiv _

back-transports-are-equivs : {X : ๐“ค ฬ‡ } {A : X โ†’ ๐“ฅ ฬ‡ } {x y : X} (p : x โ‰ก y)
                           โ†’ is-equiv (back-transport A p)
back-transports-are-equivs p = transports-are-equivs (p โปยน)

\end{code}

\begin{code}

fiber : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } โ†’ (X โ†’ Y) โ†’ Y โ†’ ๐“ค โŠ” ๐“ฅ ฬ‡
fiber f y = ฮฃ x ๊ž‰ domain f , f x โ‰ก y

fiber-point : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } {f : X โ†’ Y} {y : Y} โ†’ fiber f y โ†’ X
fiber-point = prโ‚

fiber-identification : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } {f : X โ†’ Y} {y : Y} (w : fiber f y) โ†’ f (fiber-point w) โ‰ก y
fiber-identification = prโ‚‚

is-vv-equiv : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } โ†’ (X โ†’ Y) โ†’ ๐“ค โŠ” ๐“ฅ ฬ‡
is-vv-equiv f = โˆ€ y โ†’ is-singleton (fiber f y)

is-vv-equiv-NB : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (f : X โ†’ Y) โ†’ is-vv-equiv f โ‰ก (ฮ  y ๊ž‰ Y , โˆƒ! x ๊ž‰ X , f x โ‰ก y)
is-vv-equiv-NB 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                  โ‰กโŸจ ap (ฮป - โ†’ ฮท (h x) โˆ™ -) ((trans-sym' (ฮท x))โปยน) โŸฉ
   ฮท (h x) โˆ™ (ฮท x โˆ™ (ฮท x)โปยน)       โ‰กโŸจ (โˆ™assoc (ฮท (h x)) (ฮท x) (ฮท x โปยน))โปยน โŸฉ
   ฮท (h x) โˆ™ ฮท x โˆ™ (ฮท x)โปยน         โ‰กโŸจ ap (ฮป - โ†’ ฮท (h x) โˆ™ - โˆ™ (ฮท x)โปยน) ((ap-id-is-id' (ฮท x))) โŸฉ
   ฮท (h x) โˆ™ ap id (ฮท x) โˆ™ (ฮท x)โปยน โ‰กโŸจ homotopies-are-natural' h id ฮท {h x} {x} {ฮท x} โŸฉ
   ap h (ฮท x)                      โˆŽ

qinvs-are-haes : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (f : X โ†’ Y) โ†’ qinv f โ†’ is-hae f
qinvs-are-haes {๐“ค} {๐“ฅ} {X} {Y} f (g , (ฮท , ฮต)) = g , ฮท , ฮต' , ฯ„
 where
  ฮต' : f โˆ˜ g โˆผ id
  ฮต' y = f (g y)         โ‰กโŸจ (ฮต (f (g y)))โปยน โŸฉ
         f (g (f (g y))) โ‰กโŸจ ap f (ฮท (g y)) โŸฉ
         f (g y)         โ‰กโŸจ ฮต y โŸฉ
         y               โˆŽ

  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)         โ‰กโŸจ ap (ฮป - โ†’ - โˆ™ ฮต (f x)) (ap (ap f) (a x)) โŸฉ
        ap f (ap g (ap f (ฮท x))) โˆ™ ฮต (f x)   โ‰กโŸจ ap (ฮป - โ†’ - โˆ™ ฮต (f x)) (ap-ap g f (ap f (ฮท x))) โŸฉ
        ap (f โˆ˜ g) (ap f (ฮท x)) โˆ™ ฮต (f x)    โ‰กโŸจ (homotopies-are-natural (f โˆ˜ g) id ฮต {f (g (f x))} {f x} {ap f (ฮท x)})โปยน โŸฉ
        ฮต (f (g (f x))) โˆ™ ap id (ap f (ฮท x)) โ‰กโŸจ ap (ฮป - โ†’ ฮต (f (g (f x))) โˆ™ -) (ap-ap f id (ฮท x)) โŸฉ
        ฮต (f (g (f x))) โˆ™ ap f (ฮท x)         โˆŽ

  ฯ„ : (x : X) โ†’ ap f (ฮท x) โ‰ก ฮต' (f x)
  ฯ„ x = ap f (ฮท x)                                           โ‰กโŸจ refl-left-neutral โปยน โŸฉ
        refl โˆ™ ap f (ฮท x)                                    โ‰กโŸจ ap (ฮป - โ†’ - โˆ™ ap f (ฮท x)) ((trans-sym (ฮต (f (g (f x)))))โปยน) โŸฉ
        (ฮต (f (g (f x))))โปยน โˆ™ ฮต (f (g (f x))) โˆ™ ap f (ฮท x)   โ‰กโŸจ โˆ™assoc ((ฮต (f (g (f x))))โปยน) (ฮต (f (g (f x)))) (ap f (ฮท x)) โŸฉ
        (ฮต (f (g (f x))))โปยน โˆ™ (ฮต (f (g (f x))) โˆ™ ap f (ฮท x)) โ‰กโŸจ ap (ฮป - โ†’ (ฮต (f (g (f x))))โปยน โˆ™ -) (b x)โปยน โŸฉ
        (ฮต (f (g (f x))))โปยน โˆ™ (ap f (ฮท (g (f x))) โˆ™ ฮต (f x)) โ‰กโŸจ refl โŸฉ
        ฮต' (f x)                                             โˆŽ

equivs-are-haes : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (f : X โ†’ Y)
                โ†’ is-equiv f โ†’ is-hae f
equivs-are-haes f e = qinvs-are-haes f (equivs-are-qinvs f e)

\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         โ‰กโŸจ ap (ฮป - โ†’ - โˆ™ p) (ap-โˆ™ f ((ap g p)โปยน) (ฮท x)) โŸฉ
        ap f ((ap g p)โปยน) โˆ™ ap f (ฮท x) โˆ™ p  โ‰กโŸจ ap (ฮป - โ†’ ap f - โˆ™ ap f (ฮท x) โˆ™ p) (ap-sym g p) โŸฉ
        ap f (ap g (p โปยน)) โˆ™ ap f (ฮท x) โˆ™ p โ‰กโŸจ ap (ฮป - โ†’ ap f (ap g (p โปยน)) โˆ™ - โˆ™ p) (ฯ„ x) โŸฉ
        ap f (ap g (p โปยน)) โˆ™ ฮต (f x) โˆ™ p    โ‰กโŸจ ap (ฮป - โ†’ - โˆ™ ฮต (f x) โˆ™ p) (ap-ap g f (p โปยน)) โŸฉ
        ap (f โˆ˜ g) (p โปยน) โˆ™ ฮต (f x) โˆ™ p     โ‰กโŸจ ap (ฮป - โ†’ - โˆ™ p) (homotopies-are-natural (f โˆ˜ g) id ฮต {y} {f x} {p โปยน})โปยน โŸฉ
        ฮต y โˆ™ ap id (p โปยน) โˆ™ p              โ‰กโŸจ ap (ฮป - โ†’ ฮต y โˆ™ - โˆ™ p) (ap-id-is-id (p โปยน)) โŸฉ
        ฮต y โˆ™ p โปยน โˆ™ p                      โ‰กโŸจ โˆ™assoc (ฮต y) (p โปยน) p         โŸฉ
        ฮต y โˆ™ (p โปยน โˆ™ p)                    โ‰กโŸจ ap (ฮป - โ†’ ฮต y โˆ™ -) (trans-sym p) โŸฉ
        ฮต y โˆ™ refl                          โ‰กโŸจ refl โŸฉ
        ฮต y                                 โˆŽ

    ฯ† : 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)), prโ‚

\end{code}

Then with functional and propositional extensionality, which follow
from univalence, we conclude that ยฌX = (X โ‰ƒ 0) = (X โ‰ก 0).

And similarly, with similar a observation:

\begin{code}

singletons-are-equiv-to-๐Ÿ™ : {X : ๐“ค ฬ‡ } โ†’ is-singleton X โ‡” X โ‰ƒ ๐Ÿ™ {๐“ฅ}
singletons-are-equiv-to-๐Ÿ™ {๐“ค} {๐“ฅ} {X} = forth , back
 where
  forth : is-singleton X โ†’ X โ‰ƒ ๐Ÿ™
  forth (xโ‚€ , ฯ†) = unique-to-๐Ÿ™ , (((ฮป _ โ†’ xโ‚€) , (ฮป x โ†’ (๐Ÿ™-all-* x)โปยน)) , ((ฮป _ โ†’ xโ‚€) , ฯ†))
  back : X โ‰ƒ ๐Ÿ™ โ†’ is-singleton X
  back (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)
        (ฯƒ : ฮฃ ฮณ ๊ž‰ x โ‰ก x' , ap f ฮณ โˆ™ p' โ‰ก p)
      โ†’ from-identifications-in-fibers f y x x' p p' (identifications-in-fibers f y x x' p p' ฯƒ) โ‰ก ฯƒ
ฮท-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)
        (q : (x , p) โ‰ก (x' , p'))
      โ†’ identifications-in-fibers f y x x' p p' (from-identifications-in-fibers f y x x' p p' q) โ‰ก q
ฮต-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 = retract-of-singleton (r , s , rs) (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

logically-equivalent-props-give-is-equiv : {P : ๐“ค ฬ‡ } {Q : ๐“ฅ ฬ‡ }
                                         โ†’ is-prop P
                                         โ†’ is-prop Q
                                         โ†’ (f : P โ†’ Q)
                                         โ†’ (Q โ†’ P)
                                         โ†’ is-equiv f
logically-equivalent-props-give-is-equiv 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 , logically-equivalent-props-give-is-equiv i j f g)

equiv-to-set : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } โ†’ X โ‰ƒ Y โ†’ is-set Y โ†’ is-set X
equiv-to-set e = subtypes-of-sets-are-sets โŒœ e โŒ (equivs-are-lc โŒœ e โŒ (โŒœโŒ-is-equiv e))
\end{code}

5th March 2019. A more direct proof that quasi-invertible maps
are Voevodky equivalences (have contractible fibers).

\begin{code}

qinv-is-vv-equiv : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (f : X โ†’ Y) โ†’ qinv f โ†’ is-vv-equiv f
qinv-is-vv-equiv {๐“ค} {๐“ฅ} {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 โ†’ y โ‰ก yโ‚€) a โŸฉ
      (ฮฃ y ๊ž‰ Y , y โ‰ก yโ‚€)       โ—€
  ฮณ : is-contr (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}

Associativities and precedences.

\begin{code}

infix  0 _โ‰ƒ_
infix  0 _โ‰…_
infix  1 _โ– 
infixr 0 _โ‰ƒโŸจ_โŸฉ_
infixl 2 _โ—_
infix  1 โŒœ_โŒ
\end{code}