Library HoTT.Equiv.BiInv
From HoTT.Basics Require Import Overture Equivalences Tactics Iff Trunc.
From HoTT.Basics Require Import PathGroupoids.
From HoTT.Types Require Import Sigma Prod Equiv.
Local Open Scope path_scope.
Generalizable Variables A B f.
From HoTT.Basics Require Import PathGroupoids.
From HoTT.Types Require Import Sigma Prod Equiv.
Local Open Scope path_scope.
Generalizable Variables A B f.
Bi-invertible maps
Class IsBiInv {A B : Type} (e : A → B) := {
sect_biinv : B → A ;
retr_biinv : B → A ;
eisretr_biinv : e o sect_biinv == idmap ;
eissect_biinv : retr_biinv o e == idmap ;
}.
Arguments sect_biinv {A B}%_type_scope e%_function_scope {_} _.
Arguments retr_biinv {A B}%_type_scope e%_function_scope {_} _.
Arguments eisretr_biinv {A B}%_type_scope e%_function_scope {_} _.
Arguments eissect_biinv {A B}%_type_scope e%_function_scope {_} _.
Record BiInv A B := {
biinv_fun : A → B ;
biinv_isbiinv :: IsBiInv biinv_fun
}.
Coercion biinv_fun : BiInv >-> Funclass.
Arguments biinv_fun {A B} _ _.
Arguments biinv_isbiinv {A B} _.
The record is equivalent to a product type. This is used below in a 'product of contractible types is contractible' argument.
Definition prod_isbiinv (A B : Type) `{f : A → B}
: {g : B → A & g o f == idmap} × {h : B → A & f o h == idmap} <~> IsBiInv f.
Proof.
make_equiv.
Defined.
Definition issig_biinv (A B : Type) : {f : A → B & IsBiInv f} <~> BiInv A B
:= ltac:(issig).
: {g : B → A & g o f == idmap} × {h : B → A & f o h == idmap} <~> IsBiInv f.
Proof.
make_equiv.
Defined.
Definition issig_biinv (A B : Type) : {f : A → B & IsBiInv f} <~> BiInv A B
:= ltac:(issig).
Definition sect_retr_homotopic_isbiinv {A B : Type} (f : A → B) `{bi : !IsBiInv f}
: sect_biinv f == retr_biinv f.
Proof.
revert bi.
intros [h g r s].
exact (fun y ⇒ (s (h y))^ @ ap g (r y)).
Defined.
: sect_biinv f == retr_biinv f.
Proof.
revert bi.
intros [h g r s].
exact (fun y ⇒ (s (h y))^ @ ap g (r y)).
Defined.
From a bi-invertible map, we can construct a half-adjoint equivalence in two ways. Here we take the inverse to be the retraction. Note that isequiv_adjointify modifies the last field provided. So in order that eissect_biinv f not be modified, we first use isequiv_adjointify to prove that retr_biinv f is an equivalence, and then use isequiv_inverse to deduce that f is an equivalence.
#[export] Instance isequiv_retr_biinv {A B : Type} (f : A → B) `{bi : !IsBiInv f}
: IsEquiv (retr_biinv f).
Proof.
srefine (isequiv_adjointify (retr_biinv f) f (eissect_biinv f) _); intro b.
(* This inlined proof will be modified by isequiv_adjointify: *)
exact (ap f (sect_retr_homotopic_isbiinv f b)^ @ eisretr_biinv f b).
Defined.
#[export] Instance isequiv_isbiinv {A B : Type} (f : A → B) `{bi : !IsBiInv f}
: IsEquiv f
:= isequiv_inverse (retr_biinv f).
: IsEquiv (retr_biinv f).
Proof.
srefine (isequiv_adjointify (retr_biinv f) f (eissect_biinv f) _); intro b.
(* This inlined proof will be modified by isequiv_adjointify: *)
exact (ap f (sect_retr_homotopic_isbiinv f b)^ @ eisretr_biinv f b).
Defined.
#[export] Instance isequiv_isbiinv {A B : Type} (f : A → B) `{bi : !IsBiInv f}
: IsEquiv f
:= isequiv_inverse (retr_biinv f).
Now we extract the proof generated by isequiv_adjointify; it will satisfy the adjoint law eisadj.
Definition retr_is_sect_isbiinv {A B : Type} (f : A → B) `{bi : !IsBiInv f}
: f o retr_biinv f == idmap
:= eisretr f.
: f o retr_biinv f == idmap
:= eisretr f.
f is an equivalence in a second way. Here we take the inverse to be the section. Again, the last field we provide is modified, and we extract it.
Definition isequiv_isbiinv' {A B : Type} (f : A → B) `{bi : !IsBiInv f}
: IsEquiv f.
Proof.
srefine (isequiv_adjointify f (sect_biinv f) (eisretr_biinv f) _); intro a.
exact (sect_retr_homotopic_isbiinv f (f a) @ eissect_biinv f a).
Defined.
Definition sect_is_retr_isbiinv {A B : Type} (f : A → B) `{bi : !IsBiInv f}
: sect_biinv f o f == idmap
:= eissect f (IsEquiv:=isequiv_isbiinv' f).
#[export] Instance isequiv_sect_biinv {A B : Type} (f : A → B) `{bi : !IsBiInv f}
: IsEquiv (sect_biinv f)
:= isequiv_inverse f (feq:=isequiv_isbiinv' f).
Definition isbiinv_isequiv {A B : Type} (f : A → B)
: IsEquiv f → IsBiInv f.
Proof.
intros [g s r adj].
exact (Build_IsBiInv _ _ f g g s r).
Defined.
Definition iff_isbiinv_isequiv {A B : Type} (f : A → B)
: IsBiInv f ↔ IsEquiv f.
Proof.
split.
- apply isequiv_isbiinv.
- apply isbiinv_isequiv.
Defined.
#[export] Instance ishprop_isbiinv `{Funext} {A B : Type} (f : A → B)
: IsHProp (IsBiInv f) | 0.
Proof.
apply hprop_inhabited_contr.
intros bif.
(* This uses implicitly that the product of contractible types is contractible: *)
srapply (contr_equiv' _ (prod_isbiinv A B)).
Defined.
Definition equiv_isbiinv_isequiv `{Funext} {A B : Type} (f : A → B)
: IsBiInv f <~> IsEquiv f.
Proof.
apply equiv_iff_hprop_uncurried, iff_isbiinv_isequiv.
Defined.
: IsEquiv f.
Proof.
srefine (isequiv_adjointify f (sect_biinv f) (eisretr_biinv f) _); intro a.
exact (sect_retr_homotopic_isbiinv f (f a) @ eissect_biinv f a).
Defined.
Definition sect_is_retr_isbiinv {A B : Type} (f : A → B) `{bi : !IsBiInv f}
: sect_biinv f o f == idmap
:= eissect f (IsEquiv:=isequiv_isbiinv' f).
#[export] Instance isequiv_sect_biinv {A B : Type} (f : A → B) `{bi : !IsBiInv f}
: IsEquiv (sect_biinv f)
:= isequiv_inverse f (feq:=isequiv_isbiinv' f).
Definition isbiinv_isequiv {A B : Type} (f : A → B)
: IsEquiv f → IsBiInv f.
Proof.
intros [g s r adj].
exact (Build_IsBiInv _ _ f g g s r).
Defined.
Definition iff_isbiinv_isequiv {A B : Type} (f : A → B)
: IsBiInv f ↔ IsEquiv f.
Proof.
split.
- apply isequiv_isbiinv.
- apply isbiinv_isequiv.
Defined.
#[export] Instance ishprop_isbiinv `{Funext} {A B : Type} (f : A → B)
: IsHProp (IsBiInv f) | 0.
Proof.
apply hprop_inhabited_contr.
intros bif.
(* This uses implicitly that the product of contractible types is contractible: *)
srapply (contr_equiv' _ (prod_isbiinv A B)).
Defined.
Definition equiv_isbiinv_isequiv `{Funext} {A B : Type} (f : A → B)
: IsBiInv f <~> IsEquiv f.
Proof.
apply equiv_iff_hprop_uncurried, iff_isbiinv_isequiv.
Defined.
Some lemmas to send equivalences and biinvertible maps back and forth.
Definition equiv_biinv A B (f : BiInv A B) : A <~> B
:= Build_Equiv A B f _.
Definition biinv_equiv A B (e : A <~> B) : BiInv A B
:= Build_BiInv A B e (isbiinv_isequiv e (equiv_isequiv e)).
Definition equiv_biinv_equiv `{Funext} A B
: BiInv A B <~> (A <~> B).
Proof.
nrefine ((issig_equiv A B) oE _ oE (issig_biinv A B)^-1).
napply (equiv_functor_sigma_id equiv_isbiinv_isequiv).
Defined.
Definition biinv_idmap (A : Type) : BiInv A A.
Proof.
by nrefine (Build_BiInv A A idmap (Build_IsBiInv A A idmap idmap idmap _ _)).
Defined.
Assume we have a commutative square g o e == e' o f in which e and e' are bi-invertible. Then f and g also commute with the retractions and sections, and the homotopies in these new squares each satisfy a coherence condition.
Section EquivalenceCompatibility.
Context {A B C D : Type}.
Context (e : BiInv A B) (e' : BiInv C D) (f : A → C) (g : B → D).
Context (pe : g o e == e' o f).
Let s := sect_biinv e.
Let r := retr_biinv e.
Let re := eissect_biinv e : r o e == idmap.
Let es := eisretr_biinv e : e o s == idmap.
Let s' := sect_biinv e'.
Let r' := retr_biinv e'.
Let re' := eissect_biinv e' : r' o e' == idmap.
Let es' := eisretr_biinv e' : e' o s' == idmap.
The following lemmas express the coherence conditions mentioned above.
Definition biinv_compat_pr : r' o g == f o r.
Proof.
rapply (equiv_ind e).
exact (fun a ⇒ ap r' (pe a) @ (re' (f a) @ (ap f (re a))^)).
Defined.
Definition biinv_compat_ps : s' o g == f o s.
Proof.
intro b.
apply (equiv_inj e').
exact (es' (g b) @ (ap g (es b))^ @ pe (s b)).
Defined.
Definition biinv_compat_pre (x : A)
: re' (f x) = (ap r' (pe x))^ @ biinv_compat_pr (e x) @ ap f (re x).
Proof.
unfold biinv_compat_pr.
rewrite equiv_ind_comp.
apply moveL_pM.
apply moveL_Vp.
reflexivity.
Defined.
Definition biinv_compat_pes (y : B)
: es' (g y) = ap e' (biinv_compat_ps y) @ (pe (s y))^ @ ap g (es y).
Proof.
rewrite ap_equiv_inj.
apply moveL_pM.
apply moveL_pV.
reflexivity.
Defined.
End EquivalenceCompatibility.