Library UniMath.CategoryTheory.Bicategories.Bicategories.EquivToAdjequiv
Internal equivalences in bicategories can be refined to adjoint equivalences.
Authors: Dan Frumin, Niels van der Weide
Ported from: https://github.com/nmvdw/groupoids
Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Local Open Scope cat.
Require Import UniMath.CategoryTheory.Bicategories.Bicategories.Bicat. Import Bicat.Notations.
Require Import UniMath.CategoryTheory.Bicategories.Bicategories.Unitors.
Require Import UniMath.CategoryTheory.Bicategories.Bicategories.Invertible_2cells.
Require Import UniMath.CategoryTheory.Bicategories.Bicategories.BicategoryLaws.
Require Import UniMath.CategoryTheory.Bicategories.Bicategories.Adjunctions.
Require Import UniMath.CategoryTheory.Bicategories.Bicategories.Univalence.
Local Open Scope bicategory_scope.
Definition representable_faithful
{C : bicat}
{X Y Z : C}
{f : C⟦X,Y⟧} {g : C⟦Y,X⟧}
(η : id₁ X ==> g ∘ f)
(k₁ k₂ : C⟦Z,X⟧)
(α β : k₁ ==> k₂)
(Hη : is_invertible_2cell η)
: f ◅ α = f ◅ β -> α = β.
Show proof.
intros Hαβ.
rewrite (whisker_l_iso_id₁ η _ _ α Hη).
rewrite (whisker_l_iso_id₁ η _ _ β Hη).
rewrite (whisker_l_eq k₁ k₂ α β Hαβ).
reflexivity.
rewrite (whisker_l_iso_id₁ η _ _ α Hη).
rewrite (whisker_l_iso_id₁ η _ _ β Hη).
rewrite (whisker_l_eq k₁ k₂ α β Hαβ).
reflexivity.
Definition representable_full
{C : bicat}
{X Y Z : C}
{f : C⟦X,Y⟧} {g : C⟦Y,X⟧}
(η : id₁ X ==> g ∘ f)
(θ : f ∘ g ==> id₁ Y)
(Hη : is_invertible_2cell η)
(k₁ k₂ : C⟦Z,X⟧)
(α : f ∘ k₁ ==> f ∘ k₂)
: k₁ ==> k₂.
Show proof.
refine (_ o rinvunitor _).
refine (_ o η ▻ _).
refine (_ o lassociator _ _ _).
refine (_ o g ◅ α).
refine (_ o rassociator _ _ _).
refine (_ o Hη^-1 ▻ k₂).
apply runitor.
refine (_ o η ▻ _).
refine (_ o lassociator _ _ _).
refine (_ o g ◅ α).
refine (_ o rassociator _ _ _).
refine (_ o Hη^-1 ▻ k₂).
apply runitor.
Definition full_spec
{C : bicat}
{X Y Z : C}
{f : C⟦X,Y⟧} {g : C⟦Y,X⟧}
(η : id₁ X ==> g ∘ f)
(θ : f ∘ g ==> id₁ Y)
(Hη : is_invertible_2cell η)
(Hθ : is_invertible_2cell θ)
(k₁ k₂ : C⟦Z,X⟧)
(α : f ∘ k₁ ==> f ∘ k₂)
: f ◅ (representable_full η θ Hη k₁ k₂ α) = α.
Show proof.
refine (representable_faithful (Hθ^-1) (f ∘ k₁) (f ∘ k₂) _ α _ _).
{ is_iso. }
apply (vcomp_lcancel (lassociator _ _ _)).
{ is_iso. }
rewrite <- whisker_l_hcomp.
apply (vcomp_rcancel (rassociator _ _ _)).
{ is_iso. }
rewrite <- !vassocr.
rewrite lassociator_rassociator, id2_right.
apply (vcomp_rcancel (Hη^-1 ▻ k₂)).
{ is_iso. }
apply (vcomp_rcancel (runitor k₂)).
{ is_iso. }
apply (vcomp_lcancel (η ▻ k₁)).
{ is_iso. }
apply (vcomp_lcancel (rinvunitor k₁)).
{ is_iso. }
rewrite <- !vassocr.
rewrite <- (whisker_l_iso_id₁ η k₁ k₂ (representable_full η θ Hη k₁ k₂ α) Hη).
reflexivity.
{ is_iso. }
apply (vcomp_lcancel (lassociator _ _ _)).
{ is_iso. }
rewrite <- whisker_l_hcomp.
apply (vcomp_rcancel (rassociator _ _ _)).
{ is_iso. }
rewrite <- !vassocr.
rewrite lassociator_rassociator, id2_right.
apply (vcomp_rcancel (Hη^-1 ▻ k₂)).
{ is_iso. }
apply (vcomp_rcancel (runitor k₂)).
{ is_iso. }
apply (vcomp_lcancel (η ▻ k₁)).
{ is_iso. }
apply (vcomp_lcancel (rinvunitor k₁)).
{ is_iso. }
rewrite <- !vassocr.
rewrite <- (whisker_l_iso_id₁ η k₁ k₂ (representable_full η θ Hη k₁ k₂ α) Hη).
reflexivity.
Section EquivToAdjEquiv.
Context {C : bicat}
{X Y : C}.
Variable (f : C⟦X,Y⟧)
(Hf : left_equivalence f).
Local Definition g : C⟦Y,X⟧ := left_adjoint_right_adjoint Hf.
Local Definition η : id₁ X ==> g ∘ f := left_adjoint_unit Hf.
Local Definition θ : f ∘ g ==> id₁ Y := left_adjoint_counit Hf.
Local Definition ηiso := left_equivalence_unit_iso Hf.
Local Definition θiso := left_equivalence_counit_iso Hf.
Local Definition ε : f ∘ g ==> id₁ Y.
Show proof.
refine (representable_full (θiso^-1) (ηiso^-1) _ (f ∘ g) (id₁ Y) _).
{ is_iso. }
exact ((linvunitor g)
o runitor g
o ηiso^-1 ▻ g
o rassociator _ _ _).
{ is_iso. }
exact ((linvunitor g)
o runitor g
o ηiso^-1 ▻ g
o rassociator _ _ _).
Definition εiso : is_invertible_2cell ε.
Show proof.
unfold ε, representable_full.
is_iso.
is_iso.
Definition equiv_to_adjequiv_d : left_adjoint_data f.
Show proof.
refine (g ,, _).
split.
- exact η.
- exact ε.
split.
- exact η.
- exact ε.
Local Definition first_triangle_law
: (lunitor g)
o g ◅ ε
o lassociator g f g
o η ▻ g
o rinvunitor _
= id₂ g.
Show proof.
rewrite !vassocr.
unfold ε.
rewrite (full_spec (θiso^-1) (ηiso^-1) _ (is_invertible_2cell_inv _) (f ∘ g) (id₁ Y) _).
rewrite <- !vassocr.
rewrite linvunitor_lunitor, id2_right.
rewrite !vassocr.
rewrite !(maponpaths (fun z => _ o (_ o z)) (!(vassocr _ _ _))).
rewrite lassociator_rassociator, id2_right.
rewrite !(maponpaths (fun z => _ o z) (!(vassocr _ _ _))).
rewrite lwhisker_vcomp.
rewrite vcomp_rinv.
rewrite lwhisker_id2.
rewrite id2_right.
rewrite rinvunitor_runitor.
reflexivity.
unfold ε.
rewrite (full_spec (θiso^-1) (ηiso^-1) _ (is_invertible_2cell_inv _) (f ∘ g) (id₁ Y) _).
rewrite <- !vassocr.
rewrite linvunitor_lunitor, id2_right.
rewrite !vassocr.
rewrite !(maponpaths (fun z => _ o (_ o z)) (!(vassocr _ _ _))).
rewrite lassociator_rassociator, id2_right.
rewrite !(maponpaths (fun z => _ o z) (!(vassocr _ _ _))).
rewrite lwhisker_vcomp.
rewrite vcomp_rinv.
rewrite lwhisker_id2.
rewrite id2_right.
rewrite rinvunitor_runitor.
reflexivity.
Local Definition whisker_ηg_type
: Type.
Show proof.
refine (η ▻ g = inv_cell (η := (lunitor g o g ◅ ε o lassociator g f g)) _ o runitor g).
unfold ε, representable_full.
is_iso.
unfold ε, representable_full.
is_iso.
Local Definition whisker_ηg
: whisker_ηg_type.
Show proof.
use vcomp_move_L_Mp.
{ cbn.
is_iso.
- apply Hf.
- apply Hf.
}
cbn.
refine (_ @ id2_right _).
use vcomp_move_L_pM.
{ is_iso. }
cbn.
apply first_triangle_law.
{ cbn.
is_iso.
- apply Hf.
- apply Hf.
}
cbn.
refine (_ @ id2_right _).
use vcomp_move_L_pM.
{ is_iso. }
cbn.
apply first_triangle_law.
Local Definition η_natural
: η ▻ (g ∘ f) o rinvunitor (g ∘ f) o η
=
(g ∘ f) ◅ η o linvunitor (g ∘ f) o η.
Show proof.
rewrite !vassocr.
rewrite rinvunitor_natural.
rewrite linvunitor_natural.
rewrite <- !vassocr.
rewrite lwhisker_hcomp, rwhisker_hcomp.
rewrite <- !interchange.
rewrite !id2_left, !id2_right.
rewrite lunitor_V_id_is_left_unit_V_id.
reflexivity.
rewrite rinvunitor_natural.
rewrite linvunitor_natural.
rewrite <- !vassocr.
rewrite lwhisker_hcomp, rwhisker_hcomp.
rewrite <- !interchange.
rewrite !id2_left, !id2_right.
rewrite lunitor_V_id_is_left_unit_V_id.
reflexivity.
Local Definition η_natural_help
: η ▻ (g ∘ f) o rinvunitor (g ∘ f)
=
(g ∘ f) ◅ η o linvunitor (g ∘ f)
:= vcomp_lcancel η ηiso η_natural.
Local Definition η_whisker_l_hcomp
: (g ∘ f) ◅ η = rassociator (g ∘ f) f g o g ◅ (f ◅ η) o lassociator (id₁ X) f g.
Show proof.
rewrite !vassocr.
use vcomp_move_L_Mp.
{ is_iso. }
cbn.
rewrite rwhisker_rwhisker.
reflexivity.
use vcomp_move_L_Mp.
{ is_iso. }
cbn.
rewrite rwhisker_rwhisker.
reflexivity.
Local Definition η_whisker_r_hcomp
: η ▻ (g ∘ f) = lassociator f g(g ∘ f) o η ▻ g ▻ f o rassociator f g (id₁ X).
Show proof.
use vcomp_move_L_pM.
{ is_iso. }
cbn.
rewrite lwhisker_lwhisker.
reflexivity.
{ is_iso. }
cbn.
rewrite lwhisker_lwhisker.
reflexivity.
Local Definition help1
: lassociator f g (g ∘ f) o (η ▻ g o rinvunitor _) ▻ f
=
(rassociator (g ∘ f) f g)
o g ◅ (f ◅ η)
o lassociator (id₁ X) f g
o linvunitor (g ∘ f).
Show proof.
rewrite <- η_whisker_l_hcomp.
rewrite <- lwhisker_vcomp.
rewrite left_unit_inv_assoc.
rewrite <- !vassocr.
rewrite lwhisker_lwhisker.
rewrite !vassocr.
rewrite !(maponpaths (fun z => _ o z) (!(vassocr _ _ _))).
rewrite rassociator_lassociator, id2_right.
exact η_natural_help.
rewrite <- lwhisker_vcomp.
rewrite left_unit_inv_assoc.
rewrite <- !vassocr.
rewrite lwhisker_lwhisker.
rewrite !vassocr.
rewrite !(maponpaths (fun z => _ o z) (!(vassocr _ _ _))).
rewrite rassociator_lassociator, id2_right.
exact η_natural_help.
Local Definition help2
: g ◅ (lassociator f g f o εiso^-1 ▻ f o rinvunitor _)
=
g ◅ (f ◅ η o linvunitor f).
Show proof.
rewrite <- !rwhisker_vcomp.
rewrite !vassocr.
rewrite lwhisker_hcomp, rwhisker_hcomp.
rewrite <- triangle_l_inv.
rewrite !(maponpaths (fun z => _ o z) (!(vassocr _ _ _))).
unfold assoc.
rewrite <- !lwhisker_hcomp.
rewrite <- rwhisker_lwhisker.
pose help1 as p.
rewrite whisker_ηg in p.
cbn in p.
rewrite !vassocr in p.
rewrite rinvunitor_runitor, id2_left in p.
rewrite <- !lwhisker_vcomp in p.
rewrite linvunitor_assoc in p.
rewrite <- !vassocr in p.
rewrite !vassocr in p.
rewrite !(maponpaths (fun z => _ o (_ o z)) (!(vassocr _ _ _))) in p.
rewrite rassociator_lassociator, id2_right in p.
rewrite <- bc_whisker_l_compose in p.
rewrite <- !vassocr in p.
pose @inverse_pentagon_5 as q.
rewrite !lwhisker_hcomp in p.
rewrite q in p ; clear q.
rewrite !vassocr in p.
use vcomp_rcancel. 2: exact (rassociator (f · g) f g).
{ is_iso. }
rewrite rwhisker_vcomp.
refine (_ @ p) ; clear p.
cbn.
rewrite !vassocr, !lwhisker_hcomp, !rwhisker_hcomp.
reflexivity.
rewrite !vassocr.
rewrite lwhisker_hcomp, rwhisker_hcomp.
rewrite <- triangle_l_inv.
rewrite !(maponpaths (fun z => _ o z) (!(vassocr _ _ _))).
unfold assoc.
rewrite <- !lwhisker_hcomp.
rewrite <- rwhisker_lwhisker.
pose help1 as p.
rewrite whisker_ηg in p.
cbn in p.
rewrite !vassocr in p.
rewrite rinvunitor_runitor, id2_left in p.
rewrite <- !lwhisker_vcomp in p.
rewrite linvunitor_assoc in p.
rewrite <- !vassocr in p.
rewrite !vassocr in p.
rewrite !(maponpaths (fun z => _ o (_ o z)) (!(vassocr _ _ _))) in p.
rewrite rassociator_lassociator, id2_right in p.
rewrite <- bc_whisker_l_compose in p.
rewrite <- !vassocr in p.
pose @inverse_pentagon_5 as q.
rewrite !lwhisker_hcomp in p.
rewrite q in p ; clear q.
rewrite !vassocr in p.
use vcomp_rcancel. 2: exact (rassociator (f · g) f g).
{ is_iso. }
rewrite rwhisker_vcomp.
refine (_ @ p) ; clear p.
cbn.
rewrite !vassocr, !lwhisker_hcomp, !rwhisker_hcomp.
reflexivity.
Local Definition help3
: lassociator f g f o εiso^-1 ▻ f o rinvunitor f
=
f ◅ η o linvunitor f.
Show proof.
use (representable_faithful _ _ _ _ _ _ help2).
- exact f.
- exact (εiso^-1).
- is_iso.
- exact f.
- exact (εiso^-1).
- is_iso.
Definition equiv_to_adjequiv_isadj : left_adjoint_axioms equiv_to_adjequiv_d.
Show proof.
split ; cbn.
- refine (maponpaths (fun z => ((z • _) • _) • _) (!help3) @ _).
rewrite !vassocr.
rewrite !(maponpaths (fun z => _ o (_ o z)) (!(vassocr _ _ _))).
rewrite lassociator_rassociator, id2_right.
rewrite !(maponpaths (fun z => _ o z) (!(vassocr _ _ _))).
rewrite lwhisker_vcomp.
rewrite vcomp_lid.
rewrite lwhisker_id2.
rewrite id2_right.
rewrite rinvunitor_runitor.
reflexivity.
- rewrite <- !vassocr.
exact first_triangle_law.
- refine (maponpaths (fun z => ((z • _) • _) • _) (!help3) @ _).
rewrite !vassocr.
rewrite !(maponpaths (fun z => _ o (_ o z)) (!(vassocr _ _ _))).
rewrite lassociator_rassociator, id2_right.
rewrite !(maponpaths (fun z => _ o z) (!(vassocr _ _ _))).
rewrite lwhisker_vcomp.
rewrite vcomp_lid.
rewrite lwhisker_id2.
rewrite id2_right.
rewrite rinvunitor_runitor.
reflexivity.
- rewrite <- !vassocr.
exact first_triangle_law.
Definition equiv_to_isadjequiv : left_adjoint_equivalence f.
Show proof.
use tpair.
- exact equiv_to_adjequiv_d.
- cbn.
split.
+ exact equiv_to_adjequiv_isadj.
+ split.
* exact ηiso.
* exact εiso.
- exact equiv_to_adjequiv_d.
- cbn.
split.
+ exact equiv_to_adjequiv_isadj.
+ split.
* exact ηiso.
* exact εiso.
Definition equiv_to_adjequiv : adjoint_equivalence X Y
:= (f ,, equiv_to_isadjequiv).
End EquivToAdjEquiv.
Section CompositionEquivalence.
Context {C : bicat}
{X Y Z : C}.
Variable (f : C⟦X,Y⟧)
(g : C⟦Y,Z⟧)
(A₁ : left_equivalence f)
(A₂ : left_equivalence g).
Local Notation finv := (left_adjoint_right_adjoint A₁).
Local Notation ginv := (left_adjoint_right_adjoint A₂).
Local Definition comp_unit
: id₁ X ==> (finv ∘ ginv) ∘ (g ∘ f).
Show proof.
refine (rassociator (g ∘ f) _ _ o _).
refine ((_ ◅ _) o (left_adjoint_unit A₁)).
refine (lassociator f g _ o _).
exact (((left_adjoint_unit A₂) ▻ f) o rinvunitor f).
refine ((_ ◅ _) o (left_adjoint_unit A₁)).
refine (lassociator f g _ o _).
exact (((left_adjoint_unit A₂) ▻ f) o rinvunitor f).
Local Definition comp_unit_isiso
: is_invertible_2cell comp_unit.
Show proof.
unfold comp_unit.
is_iso.
- exact (left_equivalence_unit_iso A₁).
- exact (left_equivalence_unit_iso A₂).
is_iso.
- exact (left_equivalence_unit_iso A₁).
- exact (left_equivalence_unit_iso A₂).
Local Definition comp_counit
: (g ∘ f) ∘ (finv ∘ ginv) ==> (id₁ Z).
Show proof.
refine (_ o lassociator _ f g).
refine (left_adjoint_counit A₂ o (g ◅ _)).
refine (_ o rassociator _ _ _).
refine (runitor _ o _).
exact (left_adjoint_counit A₁ ▻ _).
refine (left_adjoint_counit A₂ o (g ◅ _)).
refine (_ o rassociator _ _ _).
refine (runitor _ o _).
exact (left_adjoint_counit A₁ ▻ _).
Local Definition comp_counit_isiso
: is_invertible_2cell comp_counit.
Show proof.
unfold comp_counit.
is_iso.
- exact (left_equivalence_counit_iso A₁).
- exact (left_equivalence_counit_iso A₂).
is_iso.
- exact (left_equivalence_counit_iso A₁).
- exact (left_equivalence_counit_iso A₂).
Definition comp_equiv
: left_equivalence (f · g).
Show proof.
use tpair.
- repeat (use tpair).
* exact (finv ∘ ginv).
* exact comp_unit.
* exact comp_counit.
- split.
* exact comp_unit_isiso.
* exact comp_counit_isiso.
End CompositionEquivalence.- repeat (use tpair).
* exact (finv ∘ ginv).
* exact comp_unit.
* exact comp_counit.
- split.
* exact comp_unit_isiso.
* exact comp_counit_isiso.
Definition comp_adjequiv
{C : bicat}
{X Y Z : C}
(f : adjoint_equivalence X Y)
(g : adjoint_equivalence Y Z)
: adjoint_equivalence X Z.
Show proof.
use (equiv_to_adjequiv (f · g)).
use comp_equiv.
- exact f.
- exact g.
use comp_equiv.
- exact f.
- exact g.