Library UniMath.Bicategories.PseudoFunctors.Biequivalence

Biequivalence

Marco Maggesi, Niels van der Weide July 2019

Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.PrecategoryBinProduct.
Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations.
Require Import UniMath.Bicategories.Core.Univalence.
Require Import UniMath.Bicategories.Core.BicategoryLaws.
Require Import UniMath.Bicategories.Core.EquivToAdjequiv.
Require Import UniMath.Bicategories.Core.Invertible_2cells.
Require Import UniMath.Bicategories.Morphisms.Adjunctions.
Require Import UniMath.Bicategories.Morphisms.Properties.ClosedUnderInvertibles.
Require Import UniMath.Bicategories.Morphisms.Properties.Composition.
Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat.
Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor.
Require Import UniMath.Bicategories.PseudoFunctors.Examples.Composition.
Require Import UniMath.Bicategories.PseudoFunctors.Examples.Identity.
Require Import UniMath.Bicategories.Transformations.PseudoTransformation.
Require Import UniMath.Bicategories.Transformations.Examples.Unitality.
Require Import UniMath.Bicategories.Modifications.Modification.
Require Import UniMath.Bicategories.Modifications.Examples.Unitality.

Import PseudoFunctor.Notations.

Local Open Scope cat.
Local Open Scope bicategory_scope.

Section Biequivalence.

Definition is_biequivalence_unit_counit {C D : bicat}
           (F : psfunctor C D) (G : psfunctor D C)
  : UU
  := pstrans (comp_psfunctor G F) (id_psfunctor C) ×
     pstrans (comp_psfunctor F G) (id_psfunctor D).

Definition unit_of_is_biequivalence {C D : bicat}
           {F : psfunctor C D}
           {G : psfunctor D C}
           (e : is_biequivalence_unit_counit F G)
  : pstrans (comp_psfunctor G F) (id_psfunctor C)
  := pr1 e.

Definition counit_of_is_biequivalence {C D : bicat}
           {F : psfunctor C D}
           {G : psfunctor D C}
           (e : is_biequivalence_unit_counit F G)
  : pstrans (comp_psfunctor F G) (id_psfunctor D)
  := pr2 e.

Definition is_biequivalence_adjoints {C D : bicat}
           {F : psfunctor C D}
           {G : psfunctor D C}
           (e : is_biequivalence_unit_counit F G)
  : UU
  := left_adjoint_equivalence (unit_of_is_biequivalence e) ×
     left_adjoint_equivalence (counit_of_is_biequivalence e).

Definition is_biequivalence_adjoint_unit {C D : bicat}
           {F : psfunctor C D}
           {G : psfunctor D C}
           {e : is_biequivalence_unit_counit F G}
           (a : is_biequivalence_adjoints e)
  : left_adjoint_equivalence (unit_of_is_biequivalence e)
  := pr1 a.

Definition is_biequivalence_adjoint_counit {C D : bicat}
           {F : psfunctor C D}
           {G : psfunctor D C}
           {e : is_biequivalence_unit_counit F G}
           (a : is_biequivalence_adjoints e)
  : left_adjoint_equivalence (counit_of_is_biequivalence e)
  := pr2 a.

Definition invunit_of_is_biequivalence {C D : bicat}
           {F : psfunctor C D}
           {G : psfunctor D C}
           {e : is_biequivalence_unit_counit F G}
           (a : is_biequivalence_adjoints e)
  : pstrans (id_psfunctor C) (comp_psfunctor G F)
  := left_adjoint_right_adjoint (is_biequivalence_adjoint_unit a).

Definition invcounit_of_is_biequivalence {C D : bicat}
           {F : psfunctor C D}
           {G : psfunctor D C}
           {e : is_biequivalence_unit_counit F G}
           (a : is_biequivalence_adjoints e)
  : pstrans (id_psfunctor D) (comp_psfunctor F G)
  := left_adjoint_right_adjoint (is_biequivalence_adjoint_counit a).

Definition unitcounit_of_is_biequivalence {C D : bicat}
           {F : psfunctor C D}
           {G : psfunctor D C}
           {e : is_biequivalence_unit_counit F G}
           (a : is_biequivalence_adjoints e)
  : invertible_modification
      (comp_pstrans (invunit_of_is_biequivalence a)
                  (unit_of_is_biequivalence e))
      (id_pstrans _).
Show proof.
  refine (left_adjoint_counit (is_biequivalence_adjoint_unit a) ,, _).
  exact (left_equivalence_counit_iso (is_biequivalence_adjoint_unit a)).

Definition unitunit_of_is_biequivalence {C D : bicat}
           {F : psfunctor C D}
           {G : psfunctor D C}
           {e : is_biequivalence_unit_counit F G}
           (a : is_biequivalence_adjoints e)
  : invertible_modification
      (comp_pstrans (unit_of_is_biequivalence e)
                  (invunit_of_is_biequivalence a))
      (id_pstrans _).
Show proof.
  refine (inv_of_invertible_2cell _).
  refine (left_adjoint_unit (is_biequivalence_adjoint_unit a) ,, _).
  exact (left_equivalence_unit_iso (is_biequivalence_adjoint_unit a)).

Definition counitunit_of_is_biequivalence {C D : bicat}
           {F : psfunctor C D}
           {G : psfunctor D C}
           {e : is_biequivalence_unit_counit F G}
           (a : is_biequivalence_adjoints e)
  : invertible_modification
      (comp_pstrans (counit_of_is_biequivalence e)
                  (invcounit_of_is_biequivalence a))
      (id_pstrans _).
Show proof.
  refine (inv_of_invertible_2cell _).
  refine (left_adjoint_unit (is_biequivalence_adjoint_counit a) ,, _).
  exact (left_equivalence_unit_iso (is_biequivalence_adjoint_counit a)).

Definition counitcounit_of_is_biequivalence {C D : bicat}
           {F : psfunctor C D}
           {G : psfunctor D C}
           {e : is_biequivalence_unit_counit F G}
           (a : is_biequivalence_adjoints e)
  : invertible_modification
      (comp_pstrans (invcounit_of_is_biequivalence a)
                  (counit_of_is_biequivalence e))
      (id_pstrans _).
Show proof.
  refine (left_adjoint_counit (is_biequivalence_adjoint_counit a) ,, _).
  exact (left_equivalence_counit_iso (is_biequivalence_adjoint_counit a)).

Definition is_biequivalence {C D : bicat} (F : psfunctor C D) : UU
  := ∑ (G : psfunctor D C) (e : is_biequivalence_unit_counit F G),
     is_biequivalence_adjoints e.

Definition inv_psfunctor_of_is_biequivalence
           {C D : bicat} {F : psfunctor C D}
           (e : is_biequivalence F)
  : psfunctor D C
  := pr1 e.

Coercion unit_counit_from_is_biequivalence
           {C D : bicat} {F : psfunctor C D}
           (e : is_biequivalence F)
  : is_biequivalence_unit_counit F
      (inv_psfunctor_of_is_biequivalence e)
  := pr12 e.

Coercion adjoints_from_is_biequivalence
           {C D : bicat} {F : psfunctor C D}
           (e : is_biequivalence F)
  : is_biequivalence_adjoints e
  := pr22 e.

Definition biequivalence (C D : bicat) : UU
  := ∑ F : psfunctor C D, is_biequivalence F.

Coercion psfunctor_of_biequivalence {C D : bicat}
         (e : biequivalence C D)
  : psfunctor C D
  := pr1 e.

Coercion is_biequivalence_of_biequivalence {C D : bicat} (e : biequivalence C D)
  : is_biequivalence (psfunctor_of_biequivalence e)
  := pr2 e.

End Biequivalence.

Section Builder.

Context {C D : bicat} (F : psfunctor C D) (G : psfunctor D C)
        (η : pstrans (id_psfunctor C) (comp_psfunctor G F))
        (ηinv : pstrans (comp_psfunctor G F) (id_psfunctor C))
        (ε : pstrans (comp_psfunctor F G) (id_psfunctor D))
        (εinv : pstrans (id_psfunctor D) (comp_psfunctor F G))
        (pη : invertible_modification
               (id_pstrans (comp_psfunctor G F))
               (comp_pstrans ηinv η))
        (qη : invertible_modification
               (comp_pstrans η ηinv)
               (id_pstrans (id_psfunctor C)))
        (pε : invertible_modification
               (id_pstrans (comp_psfunctor F G))
               (comp_pstrans ε εinv))
        (qε : invertible_modification
               (comp_pstrans εinv ε)
               (id_pstrans (id_psfunctor D))).

Definition make_is_biequivalence : is_biequivalence F.
Show proof.
  refine (G,, _).
  refine ((ηinv,, ε),, _).
  split.
  - apply equiv_to_isadjequiv.
    + use tpair.
      * use tpair.
        ** exact η.
        ** split.
           *** exact (pr1 pη).
           *** exact (pr1 qη).
      * split.
        ** apply pη.
        ** apply qη.
  - apply equiv_to_isadjequiv.
    + use tpair.
      * use tpair.
        ** exact εinv.
        ** split.
           *** exact (pr1 pε).
           *** exact (pr1 qε).
      * split.
        ** apply pε.
        ** apply qε.

End Builder.

Section Builder_From_Unit_Counit.

Context {C D : bicat} (F : psfunctor C D) (G : psfunctor D C)
        (a : is_biequivalence_unit_counit F G)
        (η : pstrans (id_psfunctor C) (comp_psfunctor G F))
        (εinv : pstrans (id_psfunctor D) (comp_psfunctor F G)).

Local Notation "'ηinv'" := (unit_of_is_biequivalence a).
Local Notation "'ε'" := (counit_of_is_biequivalence a).

Context (pη : invertible_modification
                (comp_pstrans ηinv η)
                (id_pstrans (comp_psfunctor G F)))
        (qη : invertible_modification
                (comp_pstrans η ηinv)
                (id_pstrans (id_psfunctor C)))
        (pε : invertible_modification
                (comp_pstrans ε εinv)
                (id_pstrans (comp_psfunctor F G)))
        (qε : invertible_modification
                (comp_pstrans εinv ε)
                (id_pstrans (id_psfunctor D))).

Definition make_is_biequivalence_from_unit_counit : is_biequivalence F.
Show proof.
  use make_is_biequivalence.
  - exact G.
  - exact η.
  - exact ηinv.
  - exact ε.
  - exact εinv.
  - exact (inv_of_invertible_2cell pη).
  - exact qη.
  - exact (inv_of_invertible_2cell pε).
  - exact qε.

End Builder_From_Unit_Counit.

Section Pointwise.

Context {C D : bicat}
        (HC : is_univalent_2 C)
        (HD : is_univalent_2 D)
        (e : biequivalence C D).

Definition biequivalence_to_object_equivalence
  : ob C ≃ ob D.
Show proof.
  pose (F := psfunctor_of_biequivalence e).
  pose (G := inv_psfunctor_of_is_biequivalence e).
  pose (η := is_biequivalence_adjoint_unit (pr2 e)).
  pose (ε := is_biequivalence_adjoint_counit (pr2 e)).
  use make_weq.
  - exact (λ x, F x).
  - use isweq_iso.
    + exact (λ x, G x).
    + intro x.
      cbn.
      apply (isotoid_2_0 (pr1 HC)).
      use tpair.
      * exact (unit_of_is_biequivalence (pr2 e) x).
      * cbn.
        apply (pointwise_adjequiv (unit_of_is_biequivalence (pr2 e))).
        apply η.
    + intro y.
      cbn.
      apply (isotoid_2_0 (pr1 HD)).
      use tpair.
      * exact (counit_of_is_biequivalence (pr2 e) y).
      * cbn.
        apply (pointwise_adjequiv (counit_of_is_biequivalence (pr2 e))).
        apply ε.

End Pointwise.

Definition id_is_biequivalence (B : bicat) : is_biequivalence (id_psfunctor B).
Show proof.
  use make_is_biequivalence_from_unit_counit.
  - exact (id_psfunctor B).
  - use tpair.
    + apply lunitor_pstrans.
    + apply lunitor_pstrans.
  - apply linvunitor_pstrans.
  - apply linvunitor_pstrans.
  - apply lunitor_linvunitor_pstrans.
  - apply linvunitor_lunitor_pstrans.
  - apply lunitor_linvunitor_pstrans.
  - apply linvunitor_lunitor_pstrans.

Biequivalences reflect adjoint equivalences
Section BiequivReflectAdjequiv.
  Context {B₁ B₂ : bicat}
          (L : biequivalence B₁ B₂).

  Let R : psfunctor B₂ B₁ := inv_psfunctor_of_is_biequivalence L.
  Let η : pstrans (comp_psfunctor R L) (id_psfunctor B₁) := unit_of_is_biequivalence L.
  Let Hη : left_adjoint_equivalence η := is_biequivalence_adjoint_unit L.

  Context {x y : B₁}
          {f : x --> y}
          (Hf : left_adjoint_equivalence (#L f)).

  Let f' : x --> y
    := left_adjoint_right_adjoint (pointwise_adjequiv _ Hη x) · #R(#L f) · η y.

  Definition biequiv_reflect_adjequiv_cell
    : invertible_2cell f f'
    := comp_of_invertible_2cell
         (linvunitor_invertible_2cell _)
         (comp_of_invertible_2cell
            (rwhisker_of_invertible_2cell
               _
               (inv_of_invertible_2cell
                  (left_equivalence_counit_iso (pointwise_adjequiv _ Hη x))))
            (comp_of_invertible_2cell
               (rassociator_invertible_2cell _ _ _)
               (comp_of_invertible_2cell
                  (lwhisker_of_invertible_2cell
                     _
                     (psnaturality_of η f))
                  (lassociator_invertible_2cell _ _ _)))).

  Definition biequiv_reflect_adjequiv
    : left_adjoint_equivalence f.
  Show proof.
    use left_adjoint_equivalence_invertible.
    - exact f'.
    - use comp_left_adjoint_equivalence.
      + use comp_left_adjoint_equivalence.
        * apply inv_left_adjoint_equivalence.
        * use (psfunctor_preserves_adjequiv' R).
          exact Hf.
      + exact (pointwise_adjequiv _ Hη y).
    - exact biequiv_reflect_adjequiv_cell.
    - apply property_from_invertible_2cell.
End BiequivReflectAdjequiv.