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 to be βcoherentβ is:

• Being an isomorphism implies being an equivalence (

• Being an equivalence implies being an isomorphism ( 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 is a function equipped with a homotopy Symmetrically, a right inverse to is a function equipped with a homotopy

linv : (A β B) β Type _
linv f = Ξ£[ g β (_ β _) ] (g β f β‘ id)

rinv : (A β B) β Type _
rinv f = Ξ£[ h β (_ β _) ] (f β h β‘ id)


A map 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 is an equivalence, then so are pre- and post- composition with 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 has inverse then and are inverses to and

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 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 over id, and the fibres of an equivalence are contractible. Dually, rinv(f) is the fibre of 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 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)