Library UniMath.Bicategories.DisplayedBicats.Examples.CategoriesWithStructure

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.Core.Isos.
Require Import UniMath.CategoryTheory.Core.Univalence.
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.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.
Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations.
Require Import UniMath.Bicategories.Core.Examples.BicatOfCats.
Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations.
Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence.
Require Import UniMath.Bicategories.DisplayedBicats.Examples.Sub1Cell.
Require Import UniMath.Bicategories.DisplayedBicats.Examples.Prod.

Local Open Scope cat.

1. Categories with a chosen terminal object
Definition disp_bicat_chosen_terminal_obj
  : disp_bicat bicat_of_cats.
Show proof.
  use disp_subbicat.
  - exact (λ C, Terminal (pr1 C)).
  - exact (λ C₁ C₂ T₁ T₂ F, preserves_chosen_terminal_eq F T₁ T₂).
  - exact (λ C T, identity_preserves_chosen_terminal_eq T).
  - exact (λ _ _ _ _ _ _ _ _ PF PG, composition_preserves_chosen_terminal_eq PF PG).

Definition cat_with_chosen_terminal_obj
  : bicat
  := total_bicat disp_bicat_chosen_terminal_obj.

2. Categories that have a terminal object
Definition disp_bicat_have_terminal_obj
  : disp_bicat bicat_of_cats.
Show proof.
  use disp_subbicat.
  - exact (λ C, @hasTerminal (pr1 C)).
  - exact (λ C₁ C₂ _ _ F, preserves_terminal F).
  - exact (λ C _, identity_preserves_terminal _).
  - exact (λ _ _ _ _ _ _ _ _ HF HG, composition_preserves_terminal HF HG).

Definition cat_with_terminal_obj
  : bicat
  := total_bicat disp_bicat_have_terminal_obj.

Lemma disp_2cells_is_contr_have_terminal_obj
  : disp_2cells_iscontr disp_bicat_have_terminal_obj.
Show proof.
  intro ; intros.
  exists (tt,,tt).
  intro.
  use total2_paths_f ; apply iscontrunit.

Lemma disp_2cells_is_contr_chosen_terminal_obj
  : disp_2cells_iscontr disp_bicat_chosen_terminal_obj.
Show proof.
  intro ; intros.
  exists (tt,,tt).
  intro.
  use total2_paths_f ; apply iscontrunit.

1. Categories with a chosen binary products
Definition disp_bicat_chosen_binproducts
  : disp_bicat bicat_of_cats.
Show proof.
  use disp_subbicat.
  - exact (λ C, BinProducts C).
  - exact (λ C₁ C₂ BP₁ BP₂ F, preserves_chosen_binproducts_eq F BP₁ BP₂).
  - exact (λ C T, identity_preserves_chosen_binproducts_eq T).
  - exact (λ _ _ _ _ _ _ _ _ PF PG, composition_preserves_chosen_binproducts_eq PF PG).

Definition cat_with_chosen_binproducts
  : bicat
  := total_bicat disp_bicat_chosen_binproducts.

2. Categories that have binary products
Definition disp_bicat_have_binproducts
  : disp_bicat bicat_of_cats.
Show proof.
  use disp_subbicat.
  - exact (λ C, hasBinProducts C).
  - exact (λ C₁ C₂ _ _ F, preserves_binproduct F).
  - exact (λ C _, identity_preserves_binproduct _).
  - exact (λ _ _ _ _ _ _ _ _ HF HG, composition_preserves_binproduct HF HG).

Definition cat_with_binproducts
  : bicat
  := total_bicat disp_bicat_have_binproducts.

Lemma disp_2cells_is_contr_have_binproducts
  : disp_2cells_iscontr disp_bicat_have_binproducts.
Show proof.
  intro ; intros.
  exists (tt,,tt).
  intro.
  use total2_paths_f ; apply iscontrunit.

Lemma disp_2cells_is_contr_chosen_binproducts
  : disp_2cells_iscontr disp_bicat_chosen_binproducts.
Show proof.
  intro ; intros.
  exists (tt,,tt).
  intro.
  use total2_paths_f ; apply iscontrunit.