Library UniMath.Bicategories.ComprehensionCat.SetGroupoidModel

Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Prelude.
Require Import UniMath.CategoryTheory.Core.Setcategories.
Require Import UniMath.CategoryTheory.Categories.CategoryOfSetGroupoids.
Require Import UniMath.CategoryTheory.Groupoids.
Require Import UniMath.CategoryTheory.Limits.Terminal.
Require Import UniMath.CategoryTheory.Limits.Examples.CategoryOfSetGroupoidsLimits.
Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.
Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.
Require Import UniMath.CategoryTheory.DisplayedCats.Functors.
Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations.
Require Import UniMath.CategoryTheory.DisplayedCats.Examples.SetGroupoidsIsoFib.
Require Import UniMath.CategoryTheory.DisplayedCats.Examples.SetGroupoidComprehension.
Require Import UniMath.Bicategories.ComprehensionCat.BicatOfCompCat.

1. The univalent comprehension category of setgroupoids

Definition setgroupoid_cat_with_terminal_disp_cat
  : cat_with_terminal_disp_cat.
Proof.
  use make_cat_with_terminal_disp_cat.
  - exact univalent_cat_of_setgroupoid.
  - exact terminal_obj_setgroupoid.
  - exact univalent_disp_cat_isofib.
Defined.

Definition setgroupoid_cat_with_terminal_cleaving
  : cat_with_terminal_cleaving.
Proof.
  use make_cat_with_terminal_cleaving.
  - exact setgroupoid_cat_with_terminal_disp_cat.
  - exact cleaving_disp_cat_isofib.
Defined.

Definition setgroupoid_comprehension_functor
  : comprehension_functor setgroupoid_cat_with_terminal_cleaving.
Proof.
  use make_comprehension_functor.
  - exact disp_cat_isofib_comprehension.
  - exact disp_cat_isofib_comprehension_cartesian.
Defined.

Definition setgroupoid_comp_cat
  : comp_cat.
Proof.
  use make_comp_cat.
  - exact setgroupoid_cat_with_terminal_cleaving.
  - exact setgroupoid_comprehension_functor.
Defined.

2. The univalent comprehension category of setgroupoids with split isofibrations

Definition setgroupoid_cat_split_with_terminal_disp_cat
  : cat_with_terminal_disp_cat.
Proof.
  use make_cat_with_terminal_disp_cat.
  - exact univalent_cat_of_setgroupoid.
  - exact terminal_obj_setgroupoid.
  - exact univalent_disp_cat_split_isofib.
Defined.

Definition setgroupoid_cat_split_with_terminal_cleaving
  : cat_with_terminal_cleaving.
Proof.
  use make_cat_with_terminal_cleaving.
  - exact setgroupoid_cat_split_with_terminal_disp_cat.
  - exact cleaving_disp_cat_split_isofib.
Defined.

Definition setgroupoid_split_comprehension_functor
  : comprehension_functor setgroupoid_cat_split_with_terminal_cleaving.
Proof.
  use make_comprehension_functor.
  - exact disp_cat_split_isofib_comprehension.
  - exact disp_cat_split_isofib_comprehension_cartesian.
Defined.

Definition setgroupoid_comp_cat_split
  : comp_cat.
Proof.
  use make_comp_cat.
  - exact setgroupoid_cat_split_with_terminal_cleaving.
  - exact setgroupoid_split_comprehension_functor.
Defined.