Library UniMath.Bicategories.BicatOfBicategory
Bicategories
Benedikt Ahrens, Marco Maggesi February 2018 *********************************************************************************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.Univalence.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.PrecategoryBinProduct.
Require Import UniMath.CategoryTheory.HorizontalComposition.
Require Import UniMath.Bicategories.WkCatEnrichment.prebicategory.
Require Import UniMath.Bicategories.WkCatEnrichment.whiskering.
Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations.
Require Import UniMath.Bicategories.WkCatEnrichment.Notations.
Local Open Scope cat.
Lemma whisker_left_left {C : prebicategory} {a b c d : C}
(f : a -1-> b) (g : b -1-> c) {h i : c -1-> d} (x : h -2-> i) :
whisker_left f (whisker_left g x) ;v; associator_2mor f g i =
associator_2mor f g h ;v; whisker_left (f ;1; g) x.
Proof.
unfold whisker_left.
etrans; [ apply associator_naturality | idtac].
apply maponpaths.
apply maponpaths_2.
exact horizontal_comp_id.
Defined.
Lemma whisker_left_right {C : prebicategory} {a b c d : C}
(f : a -1-> b) (g h : b -1-> c) (i : c -1-> d) (x : g -2-> h) :
whisker_left f (whisker_right x i) ;v; associator_2mor f h i =
associator_2mor f g i ;v; whisker_right (whisker_left f x) i.
Proof.
exact (associator_naturality (identity f) x (identity i)).
Defined.
Lemma whisker_right_right {C : prebicategory} {a b c d : C}
(f g : a -1-> b) (h : b -1-> c) (i : c -1-> d) (x : f -2-> g) :
associator_2mor f h i ;v; whisker_right (whisker_right x h) i =
whisker_right x (h ;1; i) ;v; associator_2mor g h i.
Proof.
unfold whisker_right.
etrans; [ apply pathsinv0, associator_naturality | idtac].
apply maponpaths_2, maponpaths.
exact horizontal_comp_id.
Defined.
Section unfold_data.
Variable C : prebicategory.
Definition bcat_precategory_ob_mor : precategory_ob_mor.
Proof.
∃ C. exact (λ a b, homprecat a b).
Defined.
Definition bcat_cell_struct : prebicat_2cell_struct bcat_precategory_ob_mor
:= λ (a b : C) (f g : homprecat a b), (homprecat a b) ⟦ f, g ⟧.
Definition bcat_ob_mor_cells : ∑ (C : precategory_ob_mor), prebicat_2cell_struct C.
Proof.
∃ bcat_precategory_ob_mor. exact bcat_cell_struct.
Defined.
Definition bcat_1_id_comp_cells : prebicat_1_id_comp_cells.
Proof.
use tpair.
- ∃ bcat_precategory_ob_mor.
use tpair.
+ simpl. intros. exact (identity1 _).
+ simpl. intros a b c f g. exact (compose1 f g).
- exact bcat_cell_struct.
Defined.
Definition bcat_2_id_comp_struct : prebicat_2_id_comp_struct bcat_1_id_comp_cells.
Proof.
repeat split; simpl; unfold bcat_cell_struct.
-
intros. exact (identity _).
-
intros. exact (left_unitor f).
-
intros. exact (right_unitor f).
-
intros. exact (inv_from_iso (left_unitor f)).
-
intros. exact (inv_from_iso (right_unitor f)).
-
intros. exact (inv_from_iso (associator f g h)).
-
intros. exact (associator_2mor f g h).
-
intros a b f g h x y. exact (x · y).
-
intros a b c f g1 g2 x. exact (whisker_left f x).
-
intros a b c f1 f2 g x. exact (whisker_right x g).
Defined.
Definition bcat_data : ∑ C, prebicat_2_id_comp_struct C.
Proof.
∃ bcat_1_id_comp_cells. exact bcat_2_id_comp_struct.
Defined.
Theorem bcat_laws : prebicat_laws bcat_data.
Proof.
repeat split;
unfold id2, vcomp2, runitor, lunitor, rinvunitor, linvunitor,
rassociator, lassociator, lwhisker, rwhisker;
simpl;
unfold bcat_precategory_ob_mor, bcat_cell_struct, bcat_ob_mor_cells,
bcat_1_id_comp_cells, bcat_2_id_comp_struct, bcat_data;
simpl;
first [ intros until 1 | intros ].
-
apply id_left.
-
apply id_right.
-
apply assoc.
-
apply whisker_left_id_2mor.
-
apply whisker_right_id_2mor.
-
apply pathsinv0, whisker_left_on_comp.
-
apply pathsinv0, whisker_right_on_comp.
-
apply left_unitor_naturality.
-
apply right_unitor_naturality.
-
apply whisker_left_left.
-
apply whisker_left_right.
-
apply whisker_right_right.
-
apply twomor_naturality.
-
apply (iso_inv_after_iso (left_unitor f)).
-
apply (iso_after_iso_inv (left_unitor f)).
-
apply (iso_inv_after_iso (right_unitor f)).
-
apply (iso_after_iso_inv (right_unitor f)).
-
apply (iso_inv_after_iso (associator f g h)).
-
apply (iso_after_iso_inv (associator f g h)).
-
apply pathsinv0, (triangle_axiom f g).
-
apply pathsinv0, (pentagon_axiom f g h).
Defined.
Definition bcat : prebicat := (bcat_data,, bcat_laws).
End unfold_data.