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 to be βcoherentβ is:
Being an
isomorphism
implies being anequivalence
(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)