Library UniMath.Bicategories.PseudoFunctors.Display.Base

We construct the bicategory of pseudofunctors as a displayed bicategory. This is the first layer and it just consists of plain functions mapping objects to objects.
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.Morphisms.Adjunctions.
Require Import UniMath.Bicategories.Core.Invertible_2cells.
Require Import UniMath.Bicategories.Core.Univalence.
Require Import UniMath.Bicategories.Core.AdjointUnique.

Local Open Scope cat.

Section BasePseudoFunctor.
  Variable (C D : bicat).

  Definition ps_base_data : prebicat_data.
  Show proof.
    use build_prebicat_data.
    - exact (ob C ob D).
    - exact (λ f g, (x : C), f x --> g x).
    - exact (λ f g α β, (x : C), α x ==> β x).
    - exact (λ f x, id₁ (f x)).
    - exact (λ f g h α β x, α x · β x).
    - exact (λ f g α x, id₂ (α x)).
    - exact (λ f g α β γ m₁ m₂ x, m₁ x m₂ x).
    - exact (λ f g h α β γ m x, α x m x).
    - exact (λ f g h α β γ m x, m x γ x).
    - exact (λ f g α x, lunitor (α x)).
    - exact (λ f g α x, linvunitor (α x)).
    - exact (λ f g α x, runitor (α x)).
    - exact (λ f g α x, rinvunitor (α x)).
    - exact (λ f₁ f₂ f₃ f₄ α β γ x, lassociator (α x) (β x) (γ x)).
    - exact (λ f₁ f₂ f₃ f₄ α β γ x, rassociator (α x) (β x) (γ x)).

  Definition ps_base_laws
    : prebicat_laws ps_base_data.
  Show proof.
    repeat split ; intros ; apply funextsec ; intro.
    - apply id2_left.
    - apply id2_right.
    - apply vassocr.
    - apply lwhisker_id2.
    - apply id2_rwhisker.
    - apply lwhisker_vcomp.
    - apply rwhisker_vcomp.
    - apply vcomp_lunitor.
    - apply vcomp_runitor.
    - apply lwhisker_lwhisker.
    - apply rwhisker_lwhisker.
    - apply rwhisker_rwhisker.
    - apply vcomp_whisker.
    - apply lunitor_linvunitor.
    - apply linvunitor_lunitor.
    - apply runitor_rinvunitor.
    - apply rinvunitor_runitor.
    - apply lassociator_rassociator.
    - apply rassociator_lassociator.
    - apply runitor_rwhisker.
    - apply lassociator_lassociator.

  Definition ps_base
    : bicat.
  Show proof.
    use build_bicategory.
    - exact ps_base_data.
    - exact ps_base_laws.
    - intros ? ? ? ?.
      use impred_isaset ; intro.
      apply D.

  Definition all_is_invertible_to_is_invertible_2cell
             {F G : ps_base}
             {η ε : F --> G}
             (α : η ==> ε)
    : ( (X : C), is_invertible_2cell (α X)) is_invertible_2cell α.
  Show proof.
    intros .
    use tpair ; cbn in *.
    - exact (λ x, ( x)^-1).
    - split ; apply funextsec ; intro X ; cbn.
      + apply vcomp_rinv.
      + apply vcomp_linv.

  Definition is_invertible_2cell_to_all_is_invertible
             {F G : ps_base}
             {η ε : F --> G}
             (α : η ==> ε)
    : is_invertible_2cell α ( (X : C), is_invertible_2cell (α X)).
  Show proof.
    intros X.
    use tpair.
    - exact (^-1 X).
    - split ; cbn.
      + exact (maponpaths (λ φ, φ X) (vcomp_rinv )).
      + exact (maponpaths (λ φ, φ X) (vcomp_linv )).

  Definition all_is_invertible_is_is_invertible_2cell
             {F G : ps_base}
             {η ε : F --> G}
             (α : η ==> ε)
    : ( (X : C), is_invertible_2cell (α X)) is_invertible_2cell α.
  Show proof.
    use weqimplimpl.
    - exact (all_is_invertible_to_is_invertible_2cell α).
    - exact (is_invertible_2cell_to_all_is_invertible α).
    - apply impred ; intro.
      apply isaprop_is_invertible_2cell.
    - apply isaprop_is_invertible_2cell.

  Definition invertible_2cell_ps_base
             {F G : ps_base}
             (η ε : F --> G)
    : ( (X : C), invertible_2cell (η X) (ε X))
      
      invertible_2cell η ε.
  Show proof.
    intros α.
    use tpair.
    - intros X.
      exact (α X).
    - apply all_is_invertible_is_is_invertible_2cell.
      apply α.

  Definition invertible_2cell_ps_base_inv
             {F G : ps_base}
             (η ε : F --> G)
    : invertible_2cell η ε
      
      ( (X : C), invertible_2cell (η X) (ε X)).
  Show proof.
    intros α X.
    use tpair.
    - exact (cell_from_invertible_2cell α X).
    - apply is_invertible_2cell_to_all_is_invertible.
      apply α.

  Definition invertible_2cell_ps_base_weq
             {F G : ps_base}
             (η ε : F --> G)
    : ( (X : C), invertible_2cell (η X) (ε X))
        
        invertible_2cell η ε.
  Show proof.
    refine (make_weq (invertible_2cell_ps_base η ε) _).
    use isweq_iso.
    - exact (invertible_2cell_ps_base_inv η ε).
    - intros α.
      apply funextsec ; intro X.
      apply subtypePath.
      { intro ; apply isaprop_is_invertible_2cell. }
      reflexivity.
    - intros α.
      apply subtypePath.
      { intro ; apply isaprop_is_invertible_2cell. }
      apply funextsec ; intro X.
      reflexivity.

  Definition ps_base_is_univalent_2_1
             (HD_2_1 : is_univalent_2_1 D)
    : is_univalent_2_1 ps_base.
  Show proof.
    intros F G η ε.
    use weqhomot.
    - simple refine (invertible_2cell_ps_base_weq η ε _)%weq.
      simple refine (_ make_weq _ (isweqtoforallpaths _ _ _))%weq.
      simple refine (weqonsecfibers _ _ _).
      intro X ; cbn.
      exact (make_weq (idtoiso_2_1 (η X) (ε X)) (HD_2_1 _ _ _ _)).
    - intros p.
      induction p.
      use subtypePath.
      { intro ; apply isaprop_is_invertible_2cell. }
      reflexivity.

  Definition all_is_adjequiv_to_is_adjequiv
             {F G : ps_base}
             (η : F --> G)
    : ( (X : C), left_adjoint_equivalence (η X)) left_adjoint_equivalence η.
  Show proof.
    intros .
    use tpair.
    - use tpair.
      + intros X.
        exact (pr11 ( X)).
      + split ; intros X ; cbn.
        * exact (pr121 ( X)).
        * exact (pr221 ( X)).
    - split ; split ; cbn.
      + apply funextsec ; intro X.
        exact (pr112 ( X)).
      + apply funextsec ; intro X.
        exact (pr212 ( X)).
      + apply all_is_invertible_is_is_invertible_2cell.
        exact (λ X, pr122 ( X)).
      + apply all_is_invertible_is_is_invertible_2cell.
        exact (λ X, pr222 ( X)).

  Definition is_adjequiv_to_all_is_adjequiv
             {F G : ps_base}
             (η : F --> G)
    : left_adjoint_equivalence η ( (X : C), left_adjoint_equivalence (η X)).
  Show proof.
    intros X.
    use tpair.
    - use tpair.
      + exact (pr11 X).
      + split ; cbn.
        * exact (pr121 X).
        * exact (pr221 X).
    - split ; split ; cbn.
      + exact (maponpaths (λ φ, φ X) (pr112 )).
      + exact (maponpaths (λ φ, φ X) (pr212 )).
      + exact (is_invertible_2cell_to_all_is_invertible (pr121 ) (pr122 ) X).
      + exact (is_invertible_2cell_to_all_is_invertible (pr221 ) (pr222 ) X).

  Definition all_is_adjequiv_is_is_adjequiv
             {F G : ps_base}
             (η : F --> G)
    : ( (X : C), left_adjoint_equivalence (η X)) left_adjoint_equivalence η.
  Show proof.
    refine (make_weq (all_is_adjequiv_to_is_adjequiv η) _).
    use isweq_iso.
    - exact (is_adjequiv_to_all_is_adjequiv η).
    - intros .
      apply funextsec ; intro X.
      use subtypePath.
      {
        intro.
        do 2 apply isapropdirprod ; try (apply D)
        ; apply isaprop_is_invertible_2cell.
      }
      reflexivity.
    - intros .
      use subtypePath.
      {
        intro.
        do 2 apply isapropdirprod ; try (apply ps_base)
        ; apply isaprop_is_invertible_2cell.
      }
      reflexivity.

  Definition adjequiv_ps_base
             (F G : ps_base)
    : ( (X : C), adjoint_equivalence (F X) (G X))
      
      adjoint_equivalence F G.
  Show proof.
    intros η.
    use tpair.
    - intros X.
      exact (η X).
    - apply all_is_adjequiv_is_is_adjequiv.
      apply η.

  Definition adjequiv_ps_base_inv
             (F G : ps_base)
    : adjoint_equivalence F G
      
      ( (X : C), adjoint_equivalence (F X) (G X)).
  Show proof.
    intros η X.
    use tpair.
    - exact (pr1 η X).
    - apply is_adjequiv_to_all_is_adjequiv.
      apply η.

  Definition adjequiv_ps_base_weq
             (F G : ps_base)
    : ( (X : C), adjoint_equivalence (F X) (G X))
      
      adjoint_equivalence F G.
  Show proof.
    refine (make_weq (adjequiv_ps_base F G) _).
    use isweq_iso.
    - exact (adjequiv_ps_base_inv F G).
    - intros η.
      apply funextsec ; intro X.
      use total2_paths_b.
      + reflexivity.
      + cbn.
        use subtypePath.
        {
          intro.
          do 2 apply isapropdirprod ; try (apply D)
          ; apply isaprop_is_invertible_2cell.
        }
        reflexivity.
    - intros η.
      use total2_paths_b.
      + reflexivity.
      + cbn.
        use subtypePath.
        {
          intro.
          do 2 apply isapropdirprod ; try (apply ps_base)
          ; apply isaprop_is_invertible_2cell.
        }
        reflexivity.

  Definition ps_base_is_univalent_2_0
             (HD : is_univalent_2 D)
    : is_univalent_2_0 ps_base.
  Show proof.
    intros F G.
    use weqhomot.
    - simple refine (adjequiv_ps_base_weq F G _)%weq.
      simple refine (_ make_weq _ (isweqtoforallpaths _ _ _))%weq.
      simple refine (weqonsecfibers _ _ _).
      intro X ; cbn.
      exact (make_weq (idtoiso_2_0 (F X) (G X)) (pr1 HD _ _)).
    - intros p.
      induction p.
      use subtypePath.
      {
        intro.
        apply isaprop_left_adjoint_equivalence.
        exact (ps_base_is_univalent_2_1 (pr2 HD)).
      }
      reflexivity.

  Definition ps_base_is_univalent_2
             (HD : is_univalent_2 D)
    : is_univalent_2 ps_base.
  Show proof.
    split.
    - apply ps_base_is_univalent_2_0; assumption.
    - apply ps_base_is_univalent_2_1.
      exact (pr2 HD).

End BasePseudoFunctor.