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 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 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) 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)