open import 1Lab.HLevel.Retracts
open import 1Lab.HLevel
open import 1Lab.Equiv
open import 1Lab.Path
open import 1Lab.Type

module 1Lab.Equiv.Biinv where

Bi-invertible mapsπŸ”—

Recall the three conditions that make up the notion of equivalence.

To be more specific, what we need for a notion of equivalence isβˆ’equiv(f)\id{is-equiv}(f) to be β€œcoherent” is:

  • Being an isomorphism implies being an equivalence (isβˆ’iso(f)β†’isβˆ’equiv(f)\id{is-iso}(f) \to \id{is-equiv}(f))

  • Being an equivalence implies being an isomorphism (isβˆ’equiv(f)β†’isβˆ’iso(f)\id{is-equiv}(f) \to \id{is-iso}(f)); Taken together with the first point we may summarise: β€œBeing an equivalence and being an isomorphism are logically equivalent.”

  • Most importantly, being an equivalence must be a proposition.

The β€œblessed” definition of equivalence is that of a map with contractible fibres. However, this definition is highly abstract, so it begs the question: Is it possible to describe a simpler notion of equivalence that still satisfies the three conditions? The answer is yes! Paradoxically, adding more data to is-iso leaves us with a good notion of equivalence.

A left inverse to a function f:Aβ†’Bf : A \to B is a function g:Bβ†’Ag : B \to A equipped with a homotopy g∘f∼idg \circ f \sim \id{id}. Symmetrically, a right inverse to ff is a function h:Bβ†’Ah : B \to A equipped with a homotopy f∘h∼idf \circ h \sim \id{id}.

linv : (A β†’ B) β†’ Type _
linv f = Ξ£[ g ∈ (_ β†’ _) ] (g ∘ f ≑ id)

rinv : (A β†’ B) β†’ Type _
rinv f = Ξ£[ h ∈ (_ β†’ _) ] (f ∘ h ≑ id)

A map ff equipped with a choice of left- and right- inverse is said to be biinvertible. Perhaps surprisingly, is-biinv is a good notion of equivalence.

is-biinv : (A β†’ B) β†’ Type _
is-biinv f = linv f Γ— rinv f

If ff is an equivalence, then so are pre- and post- composition with ff. This can be proven using equivalence induction, but a more elementary argument β€” directly constructing quasi-inverses β€” suffices, and doesn’t use the sledgehammer that is univalence.

The proof is as follows: If f:Aβ†’Bf : A \to B has inverse fβˆ’1:Bβ†’Af^{-1} : B β†’ A, then (fβˆ’1βˆ˜βˆ’)(f^{-1} \circ -) and (βˆ’βˆ˜fβˆ’1)(- \circ f^{-1}) are inverses to (fβˆ˜βˆ’)(f \circ -) and (βˆ’βˆ˜f)(- \circ f).

is-equivβ†’pre-is-equiv  : {f : A β†’ B} β†’ is-equiv f β†’ is-equiv {A = C β†’ A} (f ∘_)
is-equivβ†’post-is-equiv : {f : A β†’ B} β†’ is-equiv f β†’ is-equiv {A = B β†’ C} (_∘ f)
The proof is by is-equiv→is-iso and is-iso→is-equiv. Nothing too clever.
is-equiv→pre-is-equiv {f = f} f-eqv = is-iso→is-equiv isiso where
  f-iso : is-iso f
  f-iso = is-equiv→is-iso f-eqv

  f⁻¹ : _
  f⁻¹ = f-iso .is-iso.inv

  isiso : is-iso (_∘_ f)
  isiso .is-iso.inv f x = f⁻¹ (f x)
  isiso .is-iso.rinv f = funext Ξ» x β†’ f-iso .is-iso.rinv _
  isiso .is-iso.linv f = funext Ξ» x β†’ f-iso .is-iso.linv _

is-equiv→post-is-equiv {f = f} f-eqv = is-iso→is-equiv isiso where
  f-iso : is-iso f
  f-iso = is-equiv→is-iso f-eqv

  f⁻¹ : _
  f⁻¹ = f-iso .is-iso.inv

  isiso : is-iso _
  isiso .is-iso.inv f x = f (f⁻¹ x)
  isiso .is-iso.rinv f = funext Ξ» x β†’ ap f (f-iso .is-iso.linv _)
  isiso .is-iso.linv f = funext Ξ» x β†’ ap f (f-iso .is-iso.rinv _)

With this lemma, it can be shown that if ff is an isomorphism, then linv(f) and rinv(f) are both contractible.

is-iso→is-contr-linv : {f : A → B} → is-iso f → is-contr (linv f)
is-iso→is-contr-linv isiso =
  is-equiv→post-is-equiv (is-iso→is-equiv isiso) .is-eqv id

is-iso→is-contr-rinv : {f : A → B} → is-iso f → is-contr (rinv f)
is-iso→is-contr-rinv isiso =
  is-equiv→pre-is-equiv (is-iso→is-equiv isiso) .is-eqv id

This is because linv(f) is the fibre of (βˆ’βˆ˜f)(- \circ f) over id, and the fibres of an equivalence are contractible. Dually, rinv(f) is the fibre of (fβˆ˜βˆ’)(f \circ -) over id.

_ : {f : A β†’ B} β†’ linv f ≑ fibre (_∘ f) id
_ = refl

_ : {f : A β†’ B} β†’ rinv f ≑ fibre (f ∘_) id
_ = refl

We show that if a map is biinvertible, then it is invertible. This is because if a function has two inverses, they coincide:

is-biinv→is-iso : {f : A → B} → is-biinv f → is-iso f
is-biinvβ†’is-iso {f = f} ((g , g∘f≑id) , h , h∘f≑id) = iso h (happly h∘f≑id) beta
    beta : (x : _) β†’ h (f x) ≑ x
    beta x =
      h (f x)         β‰‘βŸ¨ happly (sym g∘f≑id) _ βŸ©β‰‘
      g (f (h (f x))) β‰‘βŸ¨ ap g (happly h∘f≑id _) βŸ©β‰‘
      g (f x)         β‰‘βŸ¨ happly g∘f≑id _ βŸ©β‰‘
      x               ∎

Finally, we can show that being biinvertible is a proposition. Since propositions are those types which are contractible if inhabited suffices to show that is-biinv is contractible when it is inhabited:

is-biinv-is-prop : {f : A β†’ B} β†’ is-prop (is-biinv f)
is-biinv-is-prop {f = f} = contractible-if-inhabited contract where
  contract : is-biinv f β†’ is-contr (is-biinv f)
  contract ibiinv =
    ×-is-hlevel 0 (is-iso→is-contr-linv iiso)
                  (is-iso→is-contr-rinv iiso)
      iiso = is-biinv→is-iso ibiinv

Since is-biinv is a product of contractibles whenever it is inhabited, then it is contractible. Finally, we have that isβˆ’iso(f)β†’isβˆ’biinv(f)\id{is-iso}(f) \to \id{is-biinv}(f): pick the given inverse as both a left- and right- inverse.

is-iso→is-biinv : {f : A → B} → is-iso f → is-biinv f
is-iso→is-biinv iiso .fst = iiso .is-iso.inv , funext (iiso .is-iso.linv)
is-iso→is-biinv iiso .snd = iiso .is-iso.inv , funext (iiso .is-iso.rinv)