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.