Library UniMath.Bicategories.PseudoFunctors.Display.Identitor

The second layer of the construction of the bicategory of pseudofunctors consists of three parts. Second part: we add a 2-cell witnessing preservation of the identity.
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.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.Bicategories.DisplayedBicats.DispBicat.
Import DispBicat.Notations.
Require Import UniMath.Bicategories.PseudoFunctors.Display.Base.
Require Import UniMath.Bicategories.PseudoFunctors.Display.Map1Cells.
Require Import UniMath.Bicategories.Core.Invertible_2cells.
Require Import UniMath.Bicategories.Core.BicategoryLaws.
Require Import UniMath.Bicategories.Core.Unitors.
Require Import UniMath.Bicategories.DisplayedBicats.Examples.DisplayedCatToBicat.
Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence.

Local Open Scope cat.

Section Identitor.
  Variable (C D : bicat).

  Definition identitor_disp_cat_data
    : disp_cat_ob_mor (map1cells C D).
  Show proof.
    use tpair.
    - exact (λ F, ∏ (X : C), id₁ (Fobj F X) ==> Fmor F (id₁ X)).
    - exact (λ F G Fid Gid η,
             ∏ (X : C),
             (ηobj η X ◃ Gid X)
               • ηmor η (id₁ X)
             =
             (runitor (ηobj η X))
               • linvunitor (ηobj η X)
               • (Fid X ▹ ηobj η X)).

  Definition identitor_disp_id_comp
    : disp_cat_id_comp (map1cells C D) identitor_disp_cat_data.
  Show proof.
    split.
    - intros F Fid X ; cbn in *.
      rewrite !vassocr.
      rewrite runitor_lunitor_identity.
      rewrite lunitor_linvunitor, id2_left.
      rewrite vcomp_lunitor.
      rewrite !vassocl.
      rewrite rinvunitor_natural.
      rewrite !vassocr.
      rewrite lunitor_runitor_identity.
      rewrite runitor_rinvunitor, id2_left.
      rewrite rwhisker_hcomp.
      reflexivity.
    - intros F G H Fid Gid Hid η ε ηid εid X ; cbn in *.
      rewrite !vassocr.
      rewrite <- lwhisker_lwhisker_rassociator.
      rewrite !vassocl.
      rewrite !(maponpaths (λ z, _ • z) (vassocr _ _ _)).
      rewrite lwhisker_vcomp.
      rewrite εid.
      rewrite <- !lwhisker_vcomp.
      rewrite !vassocr.
      rewrite runitor_triangle.
      rewrite !vassocl.
      apply maponpaths.
      rewrite !(maponpaths (λ z, _ • z) (vassocr _ _ _)).
      rewrite rwhisker_lwhisker.
      rewrite !vassocl.
      rewrite !(maponpaths (λ z, _ • (_ • z)) (vassocr _ _ _)).
      rewrite rwhisker_vcomp.
      rewrite ηid.
      rewrite <- !rwhisker_vcomp.
      rewrite !vassocr.
      rewrite lwhisker_hcomp.
      rewrite triangle_l_inv.
      rewrite <- rwhisker_hcomp.
      rewrite rwhisker_vcomp.
      rewrite rinvunitor_runitor, id2_rwhisker, id2_left.
      rewrite !vassocl.
      rewrite rwhisker_rwhisker_alt.
      rewrite !vassocr.
      rewrite linvunitor_assoc.
      reflexivity.

  Definition identitor_disp_cat
    : disp_bicat (map1cells C D).
  Show proof.
    use disp_cell_unit_bicat.
    use tpair.
    - exact identitor_disp_cat_data.
    - exact identitor_disp_id_comp.

  Definition identitor_is_disp_univalent_2_1
    : disp_univalent_2_1 identitor_disp_cat.
  Show proof.
    apply disp_cell_unit_bicat_univalent_2_1.
    intros F G η Fid Gid ; simpl in *.
    apply impred ; intro.
    apply D.

  Definition identitor_is_disp_univalent_2_0
             (HD_2_1 : is_univalent_2_1 D)
    : disp_univalent_2_0 identitor_disp_cat.
  Show proof.
    use disp_cell_unit_bicat_univalent_2_0.
    - apply map1cells_is_univalent_2_1.
      exact HD_2_1.
    - intros ; simpl.
      apply impred ; intro.
      apply D.
    - intro ; cbn.
      apply impred_isaset ; intro.
      apply D.
    - intros F Fid Fid' η ; cbn in *.
      apply funextsec ; intro X.
      induction η as [η₁ η₂].
      specialize (η₁ X).
      specialize (η₂ X).
      rewrite !vassocr in η₁.
      rewrite vcomp_lunitor in η₁.
      rewrite !vassocl in η₁.
      rewrite rinvunitor_natural in η₁.
      rewrite <- rwhisker_hcomp in η₁.
      rewrite lunitor_runitor_identity, lunitor_V_id_is_left_unit_V_id in η₁.
      rewrite !vassocr in η₁.
      rewrite !runitor_rinvunitor, !id2_left in η₁.
      apply rwhisker_id_inj.
      exact (!η₁).

  Definition identitor_is_disp_univalent_2
             (HD_2_1 : is_univalent_2_1 D)
    : disp_univalent_2 identitor_disp_cat.
  Show proof.
    split.
    - apply identitor_is_disp_univalent_2_0; assumption.
    - exact identitor_is_disp_univalent_2_1.

  Definition identitor_disp_left_adjequiv_over_id
             {F : map1cells C D}
             {Fid Gid : identitor_disp_cat F}
             (ηid : Fid -->[ internal_adjoint_equivalence_identity _ ] Gid)
    : disp_left_adjoint_equivalence (internal_adjoint_equivalence_identity _) ηid.
  Show proof.
    apply disp_cell_unit_bicat_left_adjoint_equivalence_weq.
    intro x.
    cbn.
    pose (ηid x) as p.
    cbn in p.
    rewrite !vassocr.
    rewrite vcomp_lunitor.
    rewrite !vassocl.
    rewrite rinvunitor_natural.
    rewrite <- rwhisker_hcomp.
    rewrite lunitor_runitor_identity.
    rewrite <- lunitor_V_id_is_left_unit_V_id.
    rewrite !vassocr.
    refine (!p @ _).
    rewrite !vassocr.
    rewrite vcomp_lunitor.
    rewrite !vassocl.
    rewrite rinvunitor_natural.
    rewrite <- rwhisker_hcomp.
    rewrite lunitor_runitor_identity.
    rewrite <- lunitor_V_id_is_left_unit_V_id.
    apply idpath.

  Definition identitor_disp_left_adjequiv
             {HD : is_univalent_2 D}
             {F G : map1cells C D}
             (η : adjoint_equivalence F G)
             {F₂ : identitor_disp_cat F}
             {G₂ : identitor_disp_cat G}
             (η₂ : F₂ -->[ η ] G₂)
    : disp_left_adjoint_equivalence η η₂.
  Show proof.
    revert F G η F₂ G₂ η₂.
    use J_2_0.
    - apply map1cells_is_univalent_2_0.
      exact HD.
    - intros F F₂ G₂ η₂.
      apply identitor_disp_left_adjequiv_over_id.
End Identitor.