Library UniMath.Bicategories.Colimits.Examples.DisplayMapSliceColimits
Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.Bicategories.Core.Bicat.
Import Bicat.Notations.
Require Import UniMath.Bicategories.Core.Invertible_2cells.
Require Import UniMath.Bicategories.Core.BicategoryLaws.
Require Import UniMath.Bicategories.Core.Unitors.
Require Import UniMath.Bicategories.DisplayedBicats.DispBicat.
Require Import UniMath.Bicategories.DisplayedBicats.Examples.DisplayMapBicatSlice.
Require Import UniMath.Bicategories.Colimits.Initial.
Require Import UniMath.Bicategories.Logic.DisplayMapBicat.
Local Open Scope cat.
Section ArrowSubbicatInitial.
Context {B : bicat}
(I : biinitial_obj B)
(D : arrow_subbicat B)
(b : B)
(HD : arrow_subbicat_biinitial I D).
Definition disp_map_slice_biinitial_obj
: disp_map_slice_bicat D b.
Show proof.
Definition disp_map_slice_biinitial_1cell_property
: biinitial_1cell_property disp_map_slice_biinitial_obj.
Show proof.
Definition disp_map_slice_biinitial_2cell_property
(h : disp_map_slice_bicat D b)
: biinitial_2cell_property disp_map_slice_biinitial_obj h.
Show proof.
Definition disp_map_slice_biinitial_eq_property
(h : disp_map_slice_bicat D b)
: biinitial_eq_property disp_map_slice_biinitial_obj h.
Show proof.
Definition disp_map_slice_biinitial
: biinitial_obj (disp_map_slice_bicat D b).
Show proof.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.Bicategories.Core.Bicat.
Import Bicat.Notations.
Require Import UniMath.Bicategories.Core.Invertible_2cells.
Require Import UniMath.Bicategories.Core.BicategoryLaws.
Require Import UniMath.Bicategories.Core.Unitors.
Require Import UniMath.Bicategories.DisplayedBicats.DispBicat.
Require Import UniMath.Bicategories.DisplayedBicats.Examples.DisplayMapBicatSlice.
Require Import UniMath.Bicategories.Colimits.Initial.
Require Import UniMath.Bicategories.Logic.DisplayMapBicat.
Local Open Scope cat.
Section ArrowSubbicatInitial.
Context {B : bicat}
(I : biinitial_obj B)
(D : arrow_subbicat B)
(b : B)
(HD : arrow_subbicat_biinitial I D).
Definition disp_map_slice_biinitial_obj
: disp_map_slice_bicat D b.
Show proof.
simple refine (_ ,, _ ,, _).
- exact (pr1 I).
- exact (is_biinitial_1cell_property (pr2 I) b).
- exact (pr1 HD b).
- exact (pr1 I).
- exact (is_biinitial_1cell_property (pr2 I) b).
- exact (pr1 HD b).
Definition disp_map_slice_biinitial_1cell_property
: biinitial_1cell_property disp_map_slice_biinitial_obj.
Show proof.
intros h.
simple refine (_ ,, _ ,, _).
- exact (is_biinitial_1cell_property (pr2 I) (pr1 h)).
- exact (pr2 HD _ _ (pr12 h)).
- use make_invertible_2cell ; cbn.
+ apply (is_biinitial_2cell_property (pr2 I)).
+ use make_is_invertible_2cell.
* apply (is_biinitial_2cell_property (pr2 I)).
* apply (is_biinitial_eq_property (pr2 I)).
* apply (is_biinitial_eq_property (pr2 I)).
simple refine (_ ,, _ ,, _).
- exact (is_biinitial_1cell_property (pr2 I) (pr1 h)).
- exact (pr2 HD _ _ (pr12 h)).
- use make_invertible_2cell ; cbn.
+ apply (is_biinitial_2cell_property (pr2 I)).
+ use make_is_invertible_2cell.
* apply (is_biinitial_2cell_property (pr2 I)).
* apply (is_biinitial_eq_property (pr2 I)).
* apply (is_biinitial_eq_property (pr2 I)).
Definition disp_map_slice_biinitial_2cell_property
(h : disp_map_slice_bicat D b)
: biinitial_2cell_property disp_map_slice_biinitial_obj h.
Show proof.
intros α β.
simple refine (_ ,, _).
- apply (is_biinitial_2cell_property (pr2 I)).
- apply (is_biinitial_eq_property (pr2 I)).
simple refine (_ ,, _).
- apply (is_biinitial_2cell_property (pr2 I)).
- apply (is_biinitial_eq_property (pr2 I)).
Definition disp_map_slice_biinitial_eq_property
(h : disp_map_slice_bicat D b)
: biinitial_eq_property disp_map_slice_biinitial_obj h.
Show proof.
Definition disp_map_slice_biinitial
: biinitial_obj (disp_map_slice_bicat D b).
Show proof.
simple refine (_ ,, _).
- exact disp_map_slice_biinitial_obj.
- use make_is_biinitial.
+ exact disp_map_slice_biinitial_1cell_property.
+ exact disp_map_slice_biinitial_2cell_property.
+ exact disp_map_slice_biinitial_eq_property.
End ArrowSubbicatInitial.- exact disp_map_slice_biinitial_obj.
- use make_is_biinitial.
+ exact disp_map_slice_biinitial_1cell_property.
+ exact disp_map_slice_biinitial_2cell_property.
+ exact disp_map_slice_biinitial_eq_property.