Library UniMath.Bicategories.Morphisms.Examples.MorphismsInStructuredCat

Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.whiskering.
Require Import UniMath.CategoryTheory.categories.StandardCategories.
Require Import UniMath.CategoryTheory.Adjunctions.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.limits.terminal.
Require Import UniMath.CategoryTheory.limits.binproducts.
Require Import UniMath.CategoryTheory.limits.pullbacks.
Require Import UniMath.CategoryTheory.limits.initial.
Require Import UniMath.CategoryTheory.limits.bincoproducts.
Require Import UniMath.CategoryTheory.limits.Preservation.
Require Import UniMath.Bicategories.Core.Bicat.
Import Bicat.Notations.
Require Import UniMath.Bicategories.Core.Invertible_2cells.
Require Import UniMath.Bicategories.Core.Unitors.
Require Import UniMath.Bicategories.Core.BicategoryLaws.
Require Import UniMath.Bicategories.Core.Univalence.
Require Import UniMath.Bicategories.Core.EquivToAdjequiv.
Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats.
Require Import UniMath.Bicategories.Core.Examples.StructuredCategories.
Require Import UniMath.Bicategories.Morphisms.Adjunctions.
Require Import UniMath.Bicategories.Morphisms.Examples.MorphismsInBicatOfUnivCats.
Require Import UniMath.Bicategories.DisplayedBicats.DispBicat.
Require Import UniMath.Bicategories.DisplayedBicats.DispAdjunctions.
Require Import UniMath.Bicategories.DisplayedBicats.Examples.Sub1Cell.

Local Open Scope cat.

1. Adjunctions of categories with a terminal object
Section DispAdjunctionTerminalObj.
  Context {C₁ C₂ : bicat_of_univ_cats}
          (a : adjunction C₁ C₂)
          (CC₁ : disp_bicat_terminal_obj C₁)
          (CC₂ : disp_bicat_terminal_obj C₂).

  Definition isaprop_disp_adjunction_univ_cat_with_terminal_obj
    : isaprop (disp_adjunction a CC₁ CC₂).
  Show proof.
    use (isaprop_total2 (_ ,, _) (λ _, _ ,, _)) ; simpl.
    - apply isapropdirprod.
      + apply isapropunit.
      + apply isaprop_preserves_terminal.
    - use (isaprop_total2 (_ ,, _) (λ _, _ ,, _)).
      + use (isaprop_total2 (_ ,, _) (λ _, _ ,, _)).
        * simpl.
          apply isapropdirprod.
          ** apply isapropunit.
          ** apply isaprop_preserves_terminal.
        * apply isapropdirprod.
          ** simpl ; apply isapropdirprod ; apply isapropunit.
          ** simpl ; apply isapropdirprod ; apply isapropunit.
      + apply isapropdirprod ; apply disp_bicat_terminal_obj.

  Section MakeDispAdj.
    Context (H : preserves_terminal (pr1 a)).

    Let F : CC₁ -->[ a ] CC₂ := tt ,, H.

    Local Definition disp_left_adjoint_data_univ_cat_with_terminal_obj
      : disp_left_adjoint_data a F.
    Show proof.
      refine ((tt ,, _) ,, ((tt ,, tt) ,, (tt ,, tt))).
      exact (right_adjoint_preserves_terminal _ (left_adjoint_to_is_left_adjoint a)).

    Local Definition disp_left_adjoint_axioms_univ_cat_with_terminal_obj
      : disp_left_adjoint_axioms a disp_left_adjoint_data_univ_cat_with_terminal_obj.
    Show proof.
      split ; apply disp_2cells_isaprop_subbicat.

    Local Definition disp_left_adjoint_univ_cat_with_terminal_obj
      : disp_left_adjoint a F.
    Show proof.
      simple refine (_ ,, _).
      - exact disp_left_adjoint_data_univ_cat_with_terminal_obj.
      - exact disp_left_adjoint_axioms_univ_cat_with_terminal_obj.

    Definition disp_adjunction_univ_cat_with_terminal_obj
      : disp_adjunction a CC₁ CC₂.
    Show proof.
      simple refine (_ ,, _).
      - exact F.
      - exact disp_left_adjoint_univ_cat_with_terminal_obj.
  End MakeDispAdj.

  Definition disp_adj_weq_preserves_terminal
    : disp_adjunction a CC₁ CC₂ ≃ preserves_terminal (pr1 a).
  Show proof.
    use weqimplimpl.
    - intro aa.
      apply aa.
    - exact disp_adjunction_univ_cat_with_terminal_obj.
    - apply isaprop_disp_adjunction_univ_cat_with_terminal_obj.
    - apply isaprop_preserves_terminal.
End DispAdjunctionTerminalObj.

2. Adjunctions of categories with binary products
Section DispAdjunctionBinproduct.
  Context {C₁ C₂ : bicat_of_univ_cats}
          (a : adjunction C₁ C₂)
          (CC₁ : disp_bicat_binprod C₁)
          (CC₂ : disp_bicat_binprod C₂).

  Definition isaprop_disp_adjunction_univ_cat_with_binprod
    : isaprop (disp_adjunction a CC₁ CC₂).
  Show proof.
    use (isaprop_total2 (_ ,, _) (λ _, _ ,, _)) ; simpl.
    - apply isapropdirprod.
      + apply isapropunit.
      + apply isaprop_preserves_binproduct.
    - use (isaprop_total2 (_ ,, _) (λ _, _ ,, _)).
      + use (isaprop_total2 (_ ,, _) (λ _, _ ,, _)).
        * simpl.
          apply isapropdirprod.
          ** apply isapropunit.
          ** apply isaprop_preserves_binproduct.
        * apply isapropdirprod.
          ** simpl ; apply isapropdirprod ; apply isapropunit.
          ** simpl ; apply isapropdirprod ; apply isapropunit.
      + apply isapropdirprod ; apply disp_bicat_binprod.

  Section MakeDispAdj.
    Context (H : preserves_binproduct (pr1 a)).

    Let F : CC₁ -->[ a ] CC₂ := tt ,, H.

    Local Definition disp_left_adjoint_data_univ_cat_with_binprod
      : disp_left_adjoint_data a F.
    Show proof.
      refine ((tt ,, _) ,, ((tt ,, tt) ,, (tt ,, tt))).
      exact (right_adjoint_preserves_binproduct _ (left_adjoint_to_is_left_adjoint a)).

    Local Definition disp_left_adjoint_axioms_univ_cat_with_binprod
      : disp_left_adjoint_axioms a disp_left_adjoint_data_univ_cat_with_binprod.
    Show proof.
      split ; apply disp_2cells_isaprop_subbicat.

    Local Definition disp_left_adjoint_univ_cat_with_binprod
      : disp_left_adjoint a F.
    Show proof.
      simple refine (_ ,, _).
      - exact disp_left_adjoint_data_univ_cat_with_binprod.
      - exact disp_left_adjoint_axioms_univ_cat_with_binprod.

    Definition disp_adjunction_univ_cat_with_binprod
      : disp_adjunction a CC₁ CC₂.
    Show proof.
      simple refine (_ ,, _).
      - exact F.
      - exact disp_left_adjoint_univ_cat_with_binprod.
  End MakeDispAdj.

  Definition disp_adj_weq_preserves_binprod
    : disp_adjunction a CC₁ CC₂ ≃ preserves_binproduct (pr1 a).
  Show proof.
    use weqimplimpl.
    - intro aa.
      apply aa.
    - exact disp_adjunction_univ_cat_with_binprod.
    - apply isaprop_disp_adjunction_univ_cat_with_binprod.
    - apply isaprop_preserves_binproduct.
End DispAdjunctionBinproduct.

3. Adjunctions of categories with pullbacks
Section DispAdjunctionPullback.
  Context {C₁ C₂ : bicat_of_univ_cats}
          (a : adjunction C₁ C₂)
          (CC₁ : disp_bicat_pullback C₁)
          (CC₂ : disp_bicat_pullback C₂).

  Definition isaprop_disp_adjunction_univ_cat_with_pb
    : isaprop (disp_adjunction a CC₁ CC₂).
  Show proof.
    use (isaprop_total2 (_ ,, _) (λ _, _ ,, _)) ; simpl.
    - apply isapropdirprod.
      + apply isapropunit.
      + apply isaprop_preserves_pullback.
    - use (isaprop_total2 (_ ,, _) (λ _, _ ,, _)).
      + use (isaprop_total2 (_ ,, _) (λ _, _ ,, _)).
        * simpl.
          apply isapropdirprod.
          ** apply isapropunit.
          ** apply isaprop_preserves_pullback.
        * apply isapropdirprod.
          ** simpl ; apply isapropdirprod ; apply isapropunit.
          ** simpl ; apply isapropdirprod ; apply isapropunit.
      + apply isapropdirprod ; apply disp_bicat_pullback.

  Section MakeDispAdj.
    Context (H : preserves_pullback (pr1 a)).

    Let F : CC₁ -->[ a ] CC₂ := tt ,, H.

    Local Definition disp_left_adjoint_data_univ_cat_with_pb
      : disp_left_adjoint_data a F.
    Show proof.
      refine ((tt ,, _) ,, ((tt ,, tt) ,, (tt ,, tt))).
      exact (right_adjoint_preserves_pullback _ (left_adjoint_to_is_left_adjoint a)).

    Local Definition disp_left_adjoint_axioms_univ_cat_with_pb
      : disp_left_adjoint_axioms a disp_left_adjoint_data_univ_cat_with_pb.
    Show proof.
      split ; apply disp_2cells_isaprop_subbicat.

    Local Definition disp_left_adjoint_univ_cat_with_pb
      : disp_left_adjoint a F.
    Show proof.
      simple refine (_ ,, _).
      - exact disp_left_adjoint_data_univ_cat_with_pb.
      - exact disp_left_adjoint_axioms_univ_cat_with_pb.

    Definition disp_adjunction_univ_cat_with_pb
      : disp_adjunction a CC₁ CC₂.
    Show proof.
      simple refine (_ ,, _).
      - exact F.
      - exact disp_left_adjoint_univ_cat_with_pb.
  End MakeDispAdj.

  Definition disp_adj_weq_preserves_pb
    : disp_adjunction a CC₁ CC₂ ≃ preserves_pullback (pr1 a).
  Show proof.
    use weqimplimpl.
    - intro aa.
      apply aa.
    - exact disp_adjunction_univ_cat_with_pb.
    - apply isaprop_disp_adjunction_univ_cat_with_pb.
    - apply isaprop_preserves_pullback.
End DispAdjunctionPullback.

4. Adjunctions of categories with an initial object
Section DispAdjunctionInitial.
  Context {C₁ C₂ : bicat_of_univ_cats}
          (a : adjunction C₁ C₂)
          (CC₁ : disp_bicat_initial_obj C₁)
          (CC₂ : disp_bicat_initial_obj C₂).

  Definition isaprop_disp_adjunction_univ_cat_with_initial
    : isaprop (disp_adjunction a CC₁ CC₂).
  Show proof.
    use (isaprop_total2 (_ ,, _) (λ _, _ ,, _)) ; simpl.
    - apply isapropdirprod.
      + apply isapropunit.
      + apply isaprop_preserves_initial.
    - use (isaprop_total2 (_ ,, _) (λ _, _ ,, _)).
      + use (isaprop_total2 (_ ,, _) (λ _, _ ,, _)).
        * simpl.
          apply isapropdirprod.
          ** apply isapropunit.
          ** apply isaprop_preserves_initial.
        * apply isapropdirprod.
          ** simpl ; apply isapropdirprod ; apply isapropunit.
          ** simpl ; apply isapropdirprod ; apply isapropunit.
      + apply isapropdirprod ; apply disp_bicat_initial_obj.

  Section MakeDispAdj.
    Context (H : preserves_initial (pr112 a)).

    Local Definition disp_left_adjoint_univ_cat_with_initial_1cell
      : CC₁ -->[ a ] CC₂.
    Show proof.
      refine (tt ,, _).
      exact (left_adjoint_preserves_initial _ (left_adjoint_to_is_left_adjoint a)).

    Let F := disp_left_adjoint_univ_cat_with_initial_1cell.

    Local Definition disp_left_adjoint_data_univ_cat_with_initial
      : disp_left_adjoint_data a F.
    Show proof.
      refine ((tt ,, H) ,, ((tt ,, tt) ,, (tt ,, tt))).

    Local Definition disp_left_adjoint_axioms_univ_cat_with_initial
      : disp_left_adjoint_axioms a disp_left_adjoint_data_univ_cat_with_initial.
    Show proof.
      split ; apply disp_2cells_isaprop_subbicat.

    Local Definition disp_left_adjoint_univ_cat_with_initial
      : disp_left_adjoint a F.
    Show proof.
      simple refine (_ ,, _).
      - exact disp_left_adjoint_data_univ_cat_with_initial.
      - exact disp_left_adjoint_axioms_univ_cat_with_initial.

    Definition disp_adjunction_univ_cat_with_initial
      : disp_adjunction a CC₁ CC₂.
    Show proof.
      simple refine (_ ,, _).
      - exact F.
      - exact disp_left_adjoint_univ_cat_with_initial.
  End MakeDispAdj.

  Definition disp_adj_weq_preserves_initial
    : disp_adjunction a CC₁ CC₂ ≃ preserves_initial (pr112 a).
  Show proof.
    use weqimplimpl.
    - intro aa.
      apply aa.
    - exact disp_adjunction_univ_cat_with_initial.
    - apply isaprop_disp_adjunction_univ_cat_with_initial.
    - apply isaprop_preserves_initial.
End DispAdjunctionInitial.

5. Adjunctions of categories with binary coproducts
Section DispAdjunctionCoprod.
  Context {C₁ C₂ : bicat_of_univ_cats}
          (a : adjunction C₁ C₂)
          (CC₁ : disp_bicat_bincoprod C₁)
          (CC₂ : disp_bicat_bincoprod C₂).

  Definition isaprop_disp_adjunction_univ_cat_with_bincoprod
    : isaprop (disp_adjunction a CC₁ CC₂).
  Show proof.
    use (isaprop_total2 (_ ,, _) (λ _, _ ,, _)) ; simpl.
    - apply isapropdirprod.
      + apply isapropunit.
      + apply isaprop_preserves_bincoproduct.
    - use (isaprop_total2 (_ ,, _) (λ _, _ ,, _)).
      + use (isaprop_total2 (_ ,, _) (λ _, _ ,, _)).
        * simpl.
          apply isapropdirprod.
          ** apply isapropunit.
          ** apply isaprop_preserves_bincoproduct.
        * apply isapropdirprod.
          ** simpl ; apply isapropdirprod ; apply isapropunit.
          ** simpl ; apply isapropdirprod ; apply isapropunit.
      + apply isapropdirprod ; apply disp_bicat_bincoprod.

  Section MakeDispAdj.
    Context (H : preserves_bincoproduct (pr112 a)).

    Local Definition disp_left_adjoint_univ_cat_with_bincoprod_1cell
      : CC₁ -->[ a ] CC₂.
    Show proof.
      refine (tt ,, _).
      exact (left_adjoint_preserves_bincoproduct
               _
               (left_adjoint_to_is_left_adjoint a)).

    Let F := disp_left_adjoint_univ_cat_with_bincoprod_1cell.

    Local Definition disp_left_adjoint_data_univ_cat_with_bincoprod
      : disp_left_adjoint_data a F.
    Show proof.
      refine ((tt ,, H) ,, ((tt ,, tt) ,, (tt ,, tt))).

    Local Definition disp_left_adjoint_axioms_univ_cat_with_bincoprod
      : disp_left_adjoint_axioms a disp_left_adjoint_data_univ_cat_with_bincoprod.
    Show proof.
      split ; apply disp_2cells_isaprop_subbicat.

    Local Definition disp_left_adjoint_univ_cat_with_bincoprod
      : disp_left_adjoint a F.
    Show proof.
      simple refine (_ ,, _).
      - exact disp_left_adjoint_data_univ_cat_with_bincoprod.
      - exact disp_left_adjoint_axioms_univ_cat_with_bincoprod.

    Definition disp_adjunction_univ_cat_with_bincoprod
      : disp_adjunction a CC₁ CC₂.
    Show proof.
      simple refine (_ ,, _).
      - exact F.
      - exact disp_left_adjoint_univ_cat_with_bincoprod.
  End MakeDispAdj.

  Definition disp_adj_weq_preserves_bincoprod
    : disp_adjunction a CC₁ CC₂ ≃ preserves_bincoproduct (pr112 a).
  Show proof.
    use weqimplimpl.
    - intro aa.
      apply aa.
    - exact disp_adjunction_univ_cat_with_bincoprod.
    - apply isaprop_disp_adjunction_univ_cat_with_bincoprod.
    - apply isaprop_preserves_bincoproduct.
End DispAdjunctionCoprod.