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

\end{code}

Added by Carlo Angiuli on November 20, 2025.

Special syntax for definitional steps in equivalence chain reasoning:

\begin{code}

_β‰ƒβŸ¨refl⟩_ : (X : 𝓀 Μ‡ ) {Y : π“₯ Μ‡ } β†’ X ≃ Y β†’ X ≃ Y
_ β‰ƒβŸ¨refl⟩ e = e

_β‰ƒβŸ¨by-definition⟩_ : (X : 𝓀 Μ‡ ) {Y : π“₯ Μ‡ } β†’ X ≃ Y β†’ X ≃ Y
_β‰ƒβŸ¨by-definition⟩_ = _β‰ƒβŸ¨refl⟩_

\end{code}

End of addition.

\begin{code}

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)

lc-retractions-are-equivs : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                          β†’ left-cancellable f
                          β†’ has-section f
                          β†’ is-equiv f
lc-retractions-are-equivs f lc-f (s , H) =
 lc-split-surjections-are-equivs f lc-f (Ξ» y β†’ s y , H y)

≃-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 _

transports-are-equivs' : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ ) {x y : X} (p : x ＝ y)
                      β†’ is-equiv (transport A p)
transports-are-equivs' A 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)

id-is-vv-equiv : (X : 𝓀 Μ‡ ) β†’ is-vv-equiv (id {𝓀} {X})
id-is-vv-equiv X y = (y , refl) , (Ξ» where (.y , refl) β†’ refl)

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β‚€ , Ο†) =
 qinveq
  unique-to-πŸ™
  ((Ξ» _ β†’ xβ‚€) , (Ο† , (Ξ» x β†’ (πŸ™-all-⋆ x)⁻¹)))

types-equiv-to-πŸ™-are-singletons : {X : 𝓀 Μ‡ } β†’ X ≃ πŸ™ {π“₯} β†’ is-singleton X
types-equiv-to-πŸ™-are-singletons (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 _β‰ƒβŸ¨_⟩_
infixr 0 _β‰ƒβŸ¨refl⟩_
infixr 0 _β‰ƒβŸ¨by-definition⟩_
infixl 2 _●_
infix  1 ⌜_⌝

\end{code}