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

module 1Lab.Equiv.Biinv where

private variable
  ℓ : Level
  A B C : Type ℓ

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)$ to be “coherent” is:

Being an isomorphism implies being an equivalence ( $is-iso (f) \to is-equiv (f))$

Being an equivalence implies being an isomorphism ( $is-equiv (f) \to 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 \to B$ is a function $g : B \to A$ equipped with a homotopy $g \circ f \sim id .$ Symmetrically, a right inverse to $f$ is a function $h : B \to A$ equipped with a homotopy $f \circ h \sim id .$

linv : (A → B) → Type _
linv f = Σ[ g ∈ (_ → _) ] (g ∘ f ≡ id)

rinv : (A → B) → Type _
rinv f = Σ[ h ∈ (_ → _) ] (f ∘ h ≡ id)

A map $f$ 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 $f$ is an equivalence, then so are pre- and post- composition with $f .$ 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 \to B$ has inverse $f^{- 1} : B \to A,$ then $(f^{- 1} \circ -)$ and $(- \circ f^{- 1})$ are inverses to $(f \circ -)$ and $(- \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 record where
  module f = Equiv (f , f-eqv)
  from f x   = f.from (f x)
  rinv f i x = f.ε (f x) i
  linv f i x = f.η (f x) i

is-equiv→post-is-equiv {f = f} f-eqv = is-iso→is-equiv record where
  module f = Equiv (f , f-eqv)
  from f x   = f (f.from x)
  rinv f i x = f (f.η x i)
  linv f i x = f (f.ε x i)

With this lemma, it can be shown that if $f$ 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 $(- \circ f)$ over id, and the fibres of an equivalence are contractible. Dually, rinv(f) is the fibre of $(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
  where
    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 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} = is-contr-if-inhabited→is-prop 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)
    where
      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) \to 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.from , funext (iiso .is-iso.linv)
is-iso→is-biinv iiso .snd = iiso .is-iso.from , funext (iiso .is-iso.rinv)