Library UniMath.CategoryTheory.Core.TwoCategories
Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Setcategories.
Require Import UniMath.CategoryTheory.Core.Univalence.
Local Open Scope cat.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Setcategories.
Require Import UniMath.CategoryTheory.Core.Univalence.
Local Open Scope cat.
Definition two_cat_data
: UU
:= ∑ (C : precategory_data)
(cells_C : ∏ (x y : C), x --> y → x --> y → UU),
(∏ (x y : C) (f : x --> y), cells_C _ _ f f)
× (∏ (x y : C) (f g h : x --> y),
cells_C _ _ f g → cells_C _ _ g h → cells_C _ _ f h)
× (∏ (x y z : C)
(f : x --> y)
(g1 g2 : y --> z),
cells_C _ _ g1 g2 → cells_C _ _ (f · g1) (f · g2))
× (∏ (x y z : C)
(f1 f2 : x --> y)
(g : y --> z),
cells_C _ _ f1 f2 → cells_C _ _ (f1 · g) (f2 · g)).
Definition make_two_cat_data
(C : precategory_data)
(cellsC : ∏ (x y : C), x --> y → x --> y → UU)
(id : ∏ (x y : C) (f : x --> y), cellsC _ _ f f)
(vC : ∏ (x y : C)
(f g h : x --> y),
cellsC _ _ f g → cellsC _ _ g h → cellsC _ _ f h)
(lW : ∏ (x y z : C)
(f : x --> y)
(g1 g2 : y --> z),
cellsC _ _ g1 g2 → cellsC _ _ (f · g1) (f · g2))
(rW : ∏ (x y z : C)
(f1 f2 : x --> y)
(g : y --> z),
cellsC _ _ f1 f2 → cellsC _ _ (f1 · g) (f2 · g))
: two_cat_data
:= C ,, cellsC ,, id ,, vC ,, lW ,, rW.
Coercion precategory_from_two_cat_data (C : two_cat_data)
: precategory_data
:= pr1 C.
Definition two_cat_cells
(C : two_cat_data)
{a b : C}
(f g : C⟦a, b⟧)
: UU
:= pr12 C a b f g.
Local Notation "f '==>' g" := (two_cat_cells _ f g) (at level 60).
Local Notation "f '<==' g" := (two_cat_cells _ g f) (at level 60, only parsing).
: UU
:= ∑ (C : precategory_data)
(cells_C : ∏ (x y : C), x --> y → x --> y → UU),
(∏ (x y : C) (f : x --> y), cells_C _ _ f f)
× (∏ (x y : C) (f g h : x --> y),
cells_C _ _ f g → cells_C _ _ g h → cells_C _ _ f h)
× (∏ (x y z : C)
(f : x --> y)
(g1 g2 : y --> z),
cells_C _ _ g1 g2 → cells_C _ _ (f · g1) (f · g2))
× (∏ (x y z : C)
(f1 f2 : x --> y)
(g : y --> z),
cells_C _ _ f1 f2 → cells_C _ _ (f1 · g) (f2 · g)).
Definition make_two_cat_data
(C : precategory_data)
(cellsC : ∏ (x y : C), x --> y → x --> y → UU)
(id : ∏ (x y : C) (f : x --> y), cellsC _ _ f f)
(vC : ∏ (x y : C)
(f g h : x --> y),
cellsC _ _ f g → cellsC _ _ g h → cellsC _ _ f h)
(lW : ∏ (x y z : C)
(f : x --> y)
(g1 g2 : y --> z),
cellsC _ _ g1 g2 → cellsC _ _ (f · g1) (f · g2))
(rW : ∏ (x y z : C)
(f1 f2 : x --> y)
(g : y --> z),
cellsC _ _ f1 f2 → cellsC _ _ (f1 · g) (f2 · g))
: two_cat_data
:= C ,, cellsC ,, id ,, vC ,, lW ,, rW.
Coercion precategory_from_two_cat_data (C : two_cat_data)
: precategory_data
:= pr1 C.
Definition two_cat_cells
(C : two_cat_data)
{a b : C}
(f g : C⟦a, b⟧)
: UU
:= pr12 C a b f g.
Local Notation "f '==>' g" := (two_cat_cells _ f g) (at level 60).
Local Notation "f '<==' g" := (two_cat_cells _ g f) (at level 60, only parsing).
Definition id2 {C : two_cat_data} {a b : C} (f : C⟦a, b⟧) : f ==> f
:= pr122 C a b f.
Definition vcomp2 {C : two_cat_data} {a b : C} {f g h : C⟦a, b⟧}
: f ==> g → g ==> h → f ==> h
:= λ x y, pr1 (pr222 C) _ _ _ _ _ x y.
Definition lwhisker {C : two_cat_data} {a b c : C} (f : C⟦a, b⟧) {g1 g2 : C⟦b, c⟧}
: g1 ==> g2 → f · g1 ==> f · g2
:= λ x, pr12 (pr222 C) _ _ _ _ _ _ x.
Definition rwhisker {C : two_cat_data} {a b c : C} {f1 f2 : C⟦a, b⟧} (g : C⟦b, c⟧)
: f1 ==> f2 → f1 · g ==> f2 · g
:= λ x, pr22 (pr222 C) _ _ _ _ _ _ x.
Local Notation "x • y" := (vcomp2 x y) (at level 60).
Local Notation "f ◃ x" := (lwhisker f x) (at level 60). Local Notation "y ▹ g" := (rwhisker g y) (at level 60).
Definition hcomp {C : two_cat_data} {a b c : C} {f1 f2 : C⟦a, b⟧} {g1 g2 : C⟦b, c⟧}
: f1 ==> f2 -> g1 ==> g2 -> f1 · g1 ==> f2 · g2
:= λ x y, (x ▹ g1) • (f2 ◃ y).
Definition hcomp' {C : two_cat_data} {a b c : C} {f1 f2 : C⟦a, b⟧} {g1 g2 : C⟦b, c⟧}
: f1 ==> f2 -> g1 ==> g2 -> f1 · g1 ==> f2 · g2
:= λ x y, (f1 ◃ y) • (x ▹ g2).
Local Notation "x ⋆ y" := (hcomp x y) (at level 50, left associativity).
Definition idto2mor
{C : two_cat_data}
{x y : C}
{f g : x --> y}
(p : f = g)
: f ==> g.
Show proof.
:= pr122 C a b f.
Definition vcomp2 {C : two_cat_data} {a b : C} {f g h : C⟦a, b⟧}
: f ==> g → g ==> h → f ==> h
:= λ x y, pr1 (pr222 C) _ _ _ _ _ x y.
Definition lwhisker {C : two_cat_data} {a b c : C} (f : C⟦a, b⟧) {g1 g2 : C⟦b, c⟧}
: g1 ==> g2 → f · g1 ==> f · g2
:= λ x, pr12 (pr222 C) _ _ _ _ _ _ x.
Definition rwhisker {C : two_cat_data} {a b c : C} {f1 f2 : C⟦a, b⟧} (g : C⟦b, c⟧)
: f1 ==> f2 → f1 · g ==> f2 · g
:= λ x, pr22 (pr222 C) _ _ _ _ _ _ x.
Local Notation "x • y" := (vcomp2 x y) (at level 60).
Local Notation "f ◃ x" := (lwhisker f x) (at level 60). Local Notation "y ▹ g" := (rwhisker g y) (at level 60).
Definition hcomp {C : two_cat_data} {a b c : C} {f1 f2 : C⟦a, b⟧} {g1 g2 : C⟦b, c⟧}
: f1 ==> f2 -> g1 ==> g2 -> f1 · g1 ==> f2 · g2
:= λ x y, (x ▹ g1) • (f2 ◃ y).
Definition hcomp' {C : two_cat_data} {a b c : C} {f1 f2 : C⟦a, b⟧} {g1 g2 : C⟦b, c⟧}
: f1 ==> f2 -> g1 ==> g2 -> f1 · g1 ==> f2 · g2
:= λ x y, (f1 ◃ y) • (x ▹ g2).
Local Notation "x ⋆ y" := (hcomp x y) (at level 50, left associativity).
Definition idto2mor
{C : two_cat_data}
{x y : C}
{f g : x --> y}
(p : f = g)
: f ==> g.
Show proof.
3. Laws
The numbers in the following laws refer to the list of axioms given in ncatlab
(Section "Definition / Details")
https://ncatlab.org/nlab/show/bicategorydetailedDefn
version of October 7, 2015 10:35:36
Definition two_cat_category
: UU
:= ∑ (C : two_cat_data), is_precategory C × has_homsets C.
Definition make_two_cat_category
(C : two_cat_data)
(HC₁ : is_precategory C)
(HC₂ : has_homsets C)
: two_cat_category
:= C ,, HC₁ ,, HC₂.
Definition category_from_two_cat_data (C : two_cat_category)
: category.
Show proof.
Coercion category_from_two_cat_data : two_cat_category >-> category.
Definition two_cat_laws (C : two_cat_category)
: UU
:=
1a id2_left
1b id2_right
2 vassocr
(∏ (a b : C) (f g h k : C⟦a, b⟧) (x : f ==> g) (y : g ==> h) (z : h ==> k),
x • (y • z) = (x • y) • z)
×
x • (y • z) = (x • y) • z)
×
3a lwhisker_id2
3b id2_rwhisker
4 lwhisker_vcomp
(∏ (a b c : C) (f : C⟦a, b⟧) (g h i : C⟦b, c⟧) (x : g ==> h) (y : h ==> i),
(f ◃ x) • (f ◃ y) = f ◃ (x • y))
×
(f ◃ x) • (f ◃ y) = f ◃ (x • y))
×
5 rwhisker_vcomp
(∏ (a b c : C) (f g h : C⟦a, b⟧) (i : C⟦b, c⟧) (x : f ==> g) (y : g ==> h),
(x ▹ i) • (y ▹ i) = (x • y) ▹ i)
×
(x ▹ i) • (y ▹ i) = (x • y) ▹ i)
×
6 vcomp_whisker
(∏ (a b c : C) (f g : C⟦a, b⟧) (h i : C⟦b, c⟧) (x : f ==> g) (y : h ==> i),
(x ▹ h) • (g ◃ y) = (f ◃ y) • (x ▹ i))
×
(x ▹ h) • (g ◃ y) = (f ◃ y) • (x ▹ i))
×
7 naturality of left whiskering
(∏ (a b : C) (f g : C⟦a, b⟧) (x : f ==> g),
(identity a ◃ x) • idto2mor (id_left g) = idto2mor (id_left f) • x)
×
(identity a ◃ x) • idto2mor (id_left g) = idto2mor (id_left f) • x)
×
8 naturality of right whiskering
(∏ (a b : C) (f g : C⟦a, b⟧) (x : f ==> g),
(x ▹ identity b) • idto2mor (id_right g) = idto2mor (id_right f) • x)
×
(x ▹ identity b) • idto2mor (id_right g) = idto2mor (id_right f) • x)
×
9 left whisker of left whisker
(∏ (a b c d : C) (f : C⟦a, b⟧) (g : C⟦b, c⟧) (h i : C⟦c, d⟧) (x : h ==> i),
(f ◃ (g ◃ x)) • idto2mor (assoc f g i) = idto2mor (assoc f g h) • (f · g ◃ x))
×
(f ◃ (g ◃ x)) • idto2mor (assoc f g i) = idto2mor (assoc f g h) • (f · g ◃ x))
×
10 right whisker of left whisker
(∏ (a b c d : C) (f : C⟦a, b⟧) (g h : C⟦b, c⟧) (i : C⟦c, d⟧) (x : g ==> h),
(f ◃ (x ▹ i) • idto2mor (assoc f h i) = idto2mor (assoc f g i) • ((f ◃ x) ▹ i)))
×
(f ◃ (x ▹ i) • idto2mor (assoc f h i) = idto2mor (assoc f g i) • ((f ◃ x) ▹ i)))
×
11 right whisker of right whisker
(∏ (a b c d : C) (f g : C⟦a, b⟧) (h : C⟦b, c⟧) (i : C⟦c, d⟧) (x : f ==> g),
idto2mor (assoc f h i) • (x ▹ h ▹ i) = (x ▹ h · i) • idto2mor (assoc g h i)).
Definition two_precat : UU := ∑ C : two_cat_category, two_cat_laws C.
Definition make_two_precat
(C : two_cat_category)
(HC : two_cat_laws C)
: two_precat
:= C ,, HC.
Coercion two_cat_category_from_two_cat (C : two_precat)
: two_cat_category
:= pr1 C.
Coercion two_cat_laws_from_two_cat (C : two_precat)
: two_cat_laws C
:= pr2 C.
idto2mor (assoc f h i) • (x ▹ h ▹ i) = (x ▹ h · i) • idto2mor (assoc g h i)).
Definition two_precat : UU := ∑ C : two_cat_category, two_cat_laws C.
Definition make_two_precat
(C : two_cat_category)
(HC : two_cat_laws C)
: two_precat
:= C ,, HC.
Coercion two_cat_category_from_two_cat (C : two_precat)
: two_cat_category
:= pr1 C.
Coercion two_cat_laws_from_two_cat (C : two_precat)
: two_cat_laws C
:= pr2 C.
Definition two_cat_lunitor
{C : two_precat}
{x y : C}
(f : x --> y)
: identity _ · f ==> f
:= idto2mor (id_left f).
Definition two_cat_linvunitor
{C : two_precat}
{x y : C}
(f : x --> y)
: f ==> identity _ · f
:= idto2mor (!(id_left f)).
Definition two_cat_runitor
{C : two_precat}
{x y : C}
(f : x --> y)
: f · identity _ ==> f
:= idto2mor (id_right f).
Definition two_cat_rinvunitor
{C : two_precat}
{x y : C}
(f : x --> y)
: f ==> f · identity _
:= idto2mor (!(id_right f)).
Definition two_cat_lassociator
{C : two_precat}
{w x y z : C}
(f : w --> x)
(g : x --> y)
(h : y --> z)
: f · (g · h) ==> (f · g) · h
:= idto2mor (assoc f g h).
Definition two_cat_rassociator
{C : two_precat}
{w x y z : C}
(f : w --> x)
(g : x --> y)
(h : y --> z)
: (f · g) · h ==> f · (g · h)
:= idto2mor (!(assoc f g h)).
Section two_cat_law_projections.
Context {C : two_precat}.
{C : two_precat}
{x y : C}
(f : x --> y)
: identity _ · f ==> f
:= idto2mor (id_left f).
Definition two_cat_linvunitor
{C : two_precat}
{x y : C}
(f : x --> y)
: f ==> identity _ · f
:= idto2mor (!(id_left f)).
Definition two_cat_runitor
{C : two_precat}
{x y : C}
(f : x --> y)
: f · identity _ ==> f
:= idto2mor (id_right f).
Definition two_cat_rinvunitor
{C : two_precat}
{x y : C}
(f : x --> y)
: f ==> f · identity _
:= idto2mor (!(id_right f)).
Definition two_cat_lassociator
{C : two_precat}
{w x y z : C}
(f : w --> x)
(g : x --> y)
(h : y --> z)
: f · (g · h) ==> (f · g) · h
:= idto2mor (assoc f g h).
Definition two_cat_rassociator
{C : two_precat}
{w x y z : C}
(f : w --> x)
(g : x --> y)
(h : y --> z)
: (f · g) · h ==> f · (g · h)
:= idto2mor (!(assoc f g h)).
Section two_cat_law_projections.
Context {C : two_precat}.
1a id2_left
Definition id2_left {a b : C} {f g : C⟦a, b⟧} (x : f ==> g)
: id2 f • x = x
:= pr1 (pr2 C) _ _ _ _ x.
: id2 f • x = x
:= pr1 (pr2 C) _ _ _ _ x.
1b id2_right
Definition id2_right {a b : C} {f g : C⟦a, b⟧} (x : f ==> g)
: x • id2 g = x
:= pr1 (pr2 (pr2 C)) _ _ _ _ x.
: x • id2 g = x
:= pr1 (pr2 (pr2 C)) _ _ _ _ x.
2 vassocr
Definition vassocr {a b : C} {f g h k : C⟦a, b⟧}
(x : f ==> g) (y : g ==> h) (z : h ==> k)
: x • (y • z) = (x • y) • z
:= pr1 (pr2 (pr2 (pr2 C))) _ _ _ _ _ _ x y z.
Definition vassocl {a b : C} {f g h k : C⟦a, b⟧}
(x : f ==> g) (y : g ==> h) (z : h ==> k)
: (x • y) • z = x • (y • z)
:= !(vassocr _ _ _).
(x : f ==> g) (y : g ==> h) (z : h ==> k)
: x • (y • z) = (x • y) • z
:= pr1 (pr2 (pr2 (pr2 C))) _ _ _ _ _ _ x y z.
Definition vassocl {a b : C} {f g h k : C⟦a, b⟧}
(x : f ==> g) (y : g ==> h) (z : h ==> k)
: (x • y) • z = x • (y • z)
:= !(vassocr _ _ _).
3a lwhisker_id2
Definition lwhisker_id2 {a b c : C} (f : C⟦a, b⟧) (g : C⟦b, c⟧)
: f ◃ id2 g = id2 _
:= pr1 (pr2 (pr2 (pr2 (pr2 C)))) _ _ _ f g.
: f ◃ id2 g = id2 _
:= pr1 (pr2 (pr2 (pr2 (pr2 C)))) _ _ _ f g.
3b id2_rwhisker
Definition id2_rwhisker {a b c : C} (f : C⟦a, b⟧) (g : C⟦b, c⟧)
: id2 f ▹ g = id2 _
:= pr1 (pr2 (pr2 (pr2 (pr2 (pr2 C))))) _ _ _ f g.
: id2 f ▹ g = id2 _
:= pr1 (pr2 (pr2 (pr2 (pr2 (pr2 C))))) _ _ _ f g.
4 lwhisker_vcomp
Definition lwhisker_vcomp {a b c : C} (f : C⟦a, b⟧) {g h i : C⟦b, c⟧}
(x : g ==> h) (y : h ==> i)
: (f ◃ x) • (f ◃ y) = f ◃ (x • y)
:= pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 C)))))) _ _ _ f _ _ _ x y.
(x : g ==> h) (y : h ==> i)
: (f ◃ x) • (f ◃ y) = f ◃ (x • y)
:= pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 C)))))) _ _ _ f _ _ _ x y.
5 rwhisker_vcomp
Definition rwhisker_vcomp {a b c : C} {f g h : C⟦a, b⟧}
(i : C⟦b, c⟧) (x : f ==> g) (y : g ==> h)
: (x ▹ i) • (y ▹ i) = (x • y) ▹ i
:= pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 C))))))) _ _ _ _ _ _ i x y.
(i : C⟦b, c⟧) (x : f ==> g) (y : g ==> h)
: (x ▹ i) • (y ▹ i) = (x • y) ▹ i
:= pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 C))))))) _ _ _ _ _ _ i x y.
6 vcomp_whisker
Definition vcomp_whisker {a b c : C} {f g : C⟦a, b⟧} {h i : C⟦b, c⟧}
(x : f ==> g) (y : h ==> i)
: (x ▹ h) • (g ◃ y) = (f ◃ y) • (x ▹ i)
:= pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 C)))))))) _ _ _ _ _ _ i x y.
(x : f ==> g) (y : h ==> i)
: (x ▹ h) • (g ◃ y) = (f ◃ y) • (x ▹ i)
:= pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 C)))))))) _ _ _ _ _ _ i x y.
7 vcomp_lunitor
Definition vcomp_lunitor {a b : C} {f g : C⟦a, b⟧} (x : f ==> g)
: (identity a ◃ x) • two_cat_lunitor g = two_cat_lunitor f • x
:= pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 C))))))))) _ _ _ _ x.
: (identity a ◃ x) • two_cat_lunitor g = two_cat_lunitor f • x
:= pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 C))))))))) _ _ _ _ x.
8 vcomp_runitor
Definition vcomp_runitor {a b : C} {f g : C⟦a, b⟧} (x : f ==> g)
: (x ▹ identity b) • two_cat_runitor g = two_cat_runitor f • x
:= pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 C)))))))))) _ _ _ _ x.
: (x ▹ identity b) • two_cat_runitor g = two_cat_runitor f • x
:= pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 C)))))))))) _ _ _ _ x.
9 lwhisker_lwhisker
Definition lwhisker_lwhisker {a b c d : C} (f : C⟦a, b⟧) (g : C⟦b, c⟧) {h i : C⟦c, d⟧} (x : h ==> i)
: (f ◃ (g ◃ x)) • two_cat_lassociator f g i = two_cat_lassociator f g h • (f · g ◃ x)
:= pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 C))))))))))) _ _ _ _ _ _ _ _ x.
: (f ◃ (g ◃ x)) • two_cat_lassociator f g i = two_cat_lassociator f g h • (f · g ◃ x)
:= pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 C))))))))))) _ _ _ _ _ _ _ _ x.
10 rwhisker_lwhisker
Definition rwhisker_lwhisker {a b c d : C} (f : C⟦a, b⟧) {g h : C⟦b, c⟧} (i : C⟦c, d⟧) (x : g ==> h)
: (f ◃ (x ▹ i) • two_cat_lassociator f h i = two_cat_lassociator f g i • ((f ◃ x) ▹ i))
:= pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 C)))))))))))) _ _ _ _ _ _ _ _ x.
: (f ◃ (x ▹ i) • two_cat_lassociator f h i = two_cat_lassociator f g i • ((f ◃ x) ▹ i))
:= pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 C)))))))))))) _ _ _ _ _ _ _ _ x.
11 rwhisker_rwhisker
Definition rwhisker_rwhisker {a b c d : C} {f g : C⟦a, b⟧} (h : C⟦b, c⟧) (i : C⟦c, d⟧) (x : f ==> g)
: two_cat_lassociator f h i • (x ▹ h ▹ i) = (x ▹ h · i) • two_cat_lassociator g h i
:= pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 C)))))))))))) _ _ _ _ _ _ _ _ x.
End two_cat_law_projections.
: two_cat_lassociator f h i • (x ▹ h ▹ i) = (x ▹ h · i) • two_cat_lassociator g h i
:= pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 C)))))))))))) _ _ _ _ _ _ _ _ x.
End two_cat_law_projections.
Definition isaset_cells (C : two_precat) : UU
:= ∏ (a b : C) (f g : a --> b), isaset (f ==> g).
Definition two_cat : UU
:= ∑ C : two_precat, isaset_cells C.
Definition make_two_cat
(C : two_precat)
(HC : isaset_cells C)
: two_cat
:= C ,, HC.
Coercion two_cat_to_two_precat
(C : two_cat)
: two_precat
:= pr1 C.
Proposition isaset_two_cat_cells
{C : two_cat}
{a b : C}
(f g : a --> b)
: isaset (f ==> g).
Show proof.
Definition isaprop_two_cat_laws
(C : two_cat)
: isaprop (two_cat_laws C).
Show proof.
:= ∏ (a b : C) (f g : a --> b), isaset (f ==> g).
Definition two_cat : UU
:= ∑ C : two_precat, isaset_cells C.
Definition make_two_cat
(C : two_precat)
(HC : isaset_cells C)
: two_cat
:= C ,, HC.
Coercion two_cat_to_two_precat
(C : two_cat)
: two_precat
:= pr1 C.
Proposition isaset_two_cat_cells
{C : two_cat}
{a b : C}
(f g : a --> b)
: isaset (f ==> g).
Show proof.
Definition isaprop_two_cat_laws
(C : two_cat)
: isaprop (two_cat_laws C).
Show proof.
Section IdTo2MorLaws.
Context {C : two_precat}.
Definition idto2mor_id
{x y : C}
{f : x --> y}
(p : f = f)
: idto2mor p = id2 _.
Show proof.
Definition idto2mor_comp
{x y : C}
{f g h : x --> y}
(p : f = g)
(q : g = h)
: idto2mor p • idto2mor q = idto2mor (p @ q).
Show proof.
Definition idto2mor_lwhisker
{x y z : C}
(f : x --> y)
{g h : y --> z}
(p : g = h)
: f ◃ idto2mor p
=
idto2mor (maponpaths (λ q, f · q) p).
Show proof.
Definition idto2mor_rwhisker
{x y z : C}
{f g : x --> y}
(h : y --> z)
(p : f = g)
: idto2mor p ▹ h
=
idto2mor (maponpaths (λ q, q · h) p).
Show proof.
Definition two_cat_lunitor_linvunitor
{x y : C}
(f : x --> y)
: two_cat_lunitor f • two_cat_linvunitor f = id2 _.
Show proof.
Definition two_cat_linvunitor_lunitor
{x y : C}
(f : x --> y)
: two_cat_linvunitor f • two_cat_lunitor f = id2 _.
Show proof.
Definition two_cat_runitor_rinvunitor
{x y : C}
(f : x --> y)
: two_cat_runitor f • two_cat_rinvunitor f = id2 _.
Show proof.
Definition two_cat_rinvunitor_runitor
{x y : C}
(f : x --> y)
: two_cat_rinvunitor f • two_cat_runitor f = id2 _.
Show proof.
Definition two_cat_lassociator_rassociator
{w x y z : C}
(f : w --> x)
(g : x --> y)
(h : y --> z)
: two_cat_lassociator f g h • two_cat_rassociator f g h = id2 _.
Show proof.
Definition two_cat_rassociator_lassociator
{w x y z : C}
(f : w --> x)
(g : x --> y)
(h : y --> z)
: two_cat_rassociator f g h • two_cat_lassociator f g h = id2 _.
Show proof.
Definition id1_lwhisker {a b : C} {f g : C⟦a, b⟧} (x : f ==> g)
: (identity a ◃ x) = two_cat_lunitor f • x • two_cat_linvunitor g.
Show proof.
Definition rwhisker_id1 {a b : C} {f g : C⟦a, b⟧} (x : f ==> g)
: (x ▹ identity b) = two_cat_runitor f • x • two_cat_rinvunitor g.
Show proof.
Definition lwhisker_lwhisker_mor
{a b c d : C}
(f : a --> b)
(g : b --> c)
{h i : c --> d}
(τ : h ==> i)
: f ◃ (g ◃ τ)
=
two_cat_lassociator _ _ _
• (f · g ◃ τ)
• two_cat_rassociator _ _ _.
Show proof.
Definition lwhisker_comp_mor
{a b c d : C}
(f : a --> b)
(g : b --> c)
{h i : c --> d}
(τ : h ==> i)
: f · g ◃ τ
=
two_cat_rassociator _ _ _
• (f ◃ (g ◃ τ))
• two_cat_lassociator _ _ _.
Show proof.
Definition rwhisker_lwhisker_mor
{a b c d : C}
(f : a --> b)
{g h : b --> c}
(τ : g ==> h)
(i : c --> d)
: f ◃ (τ ▹ i)
=
two_cat_lassociator _ _ _
• ((f ◃ τ) ▹ i)
• two_cat_rassociator _ _ _.
Show proof.
Definition lwhisker_rwhisker_mor
{a b c d : C}
(f : a --> b)
{g h : b --> c}
(τ : g ==> h)
(i : c --> d)
: (f ◃ τ) ▹ i
=
two_cat_rassociator _ _ _
• (f ◃ (τ ▹ i))
• two_cat_lassociator _ _ _.
Show proof.
Definition rwhisker_rwhisker_mor
{a b c d : C}
{f g : a --> b}
(τ : f ==> g)
(h : b --> c)
(i : c --> d)
: τ ▹ h ▹ i
=
two_cat_rassociator _ _ _
• (τ ▹ h · i)
• two_cat_lassociator _ _ _.
Show proof.
Definition rwhisker_comp_mor
{a b c d : C}
{f g : a --> b}
(τ : f ==> g)
(h : b --> c)
(i : c --> d)
: τ ▹ h · i
=
two_cat_lassociator _ _ _
• (τ ▹ h ▹ i)
• two_cat_rassociator _ _ _.
Show proof.
Proposition idto2mor_left
{a b : C}
{f f' g : a --> b}
(p p' : f = f')
{τ τ' : f' ==> g}
(r : τ = τ')
: idto2mor p • τ
=
idto2mor p' • τ'.
Show proof.
Proposition idto2mor_right
{a b : C}
{f g g' : a --> b}
(p p' : g = g')
{τ τ' : f ==> g}
(r : τ = τ')
: τ • idto2mor p
=
τ' • idto2mor p'.
Show proof.
Definition arr_idto2mor_eq
{a b : C}
{f f' g g' : a --> b}
(p p' : f = f')
{τ τ' : f' ==> g}
(q q' : g = g')
(r : τ = τ')
: idto2mor p • τ • idto2mor q
=
idto2mor p' • τ' • idto2mor q'.
Show proof.
Definition arr_idto2mor_eq2
{a b : C}
{f f' g g' h h' : a --> b}
(p p' : f = f')
{τ τ' : f' ==> g}
(q q' : g = g')
{θ θ' : g' ==> h}
(r r' : h = h')
(H₁ : τ = τ')
(H₂ : θ = θ')
: idto2mor p • τ • idto2mor q • θ • idto2mor r
=
idto2mor p' • τ' • idto2mor q' • θ' • idto2mor r'.
Show proof.
Definition arr_idto2mor_eq3
{a b : C}
{f f' g g' h h' k k' : a --> b}
(p p' : f = f')
{τ τ' : f' ==> g}
(q q' : g = g')
{θ θ' : g' ==> h}
(r r' : h = h')
{ξ ξ' : h' ==> k}
(s s' : k = k')
(H₁ : τ = τ')
(H₂ : θ = θ')
(H₃ : ξ = ξ')
: idto2mor p • τ • idto2mor q • θ • idto2mor r • ξ • idto2mor s
=
idto2mor p' • τ' • idto2mor q' • θ' • idto2mor r' • ξ' • idto2mor s'.
Show proof.
Context {C : two_precat}.
Definition idto2mor_id
{x y : C}
{f : x --> y}
(p : f = f)
: idto2mor p = id2 _.
Show proof.
Definition idto2mor_comp
{x y : C}
{f g h : x --> y}
(p : f = g)
(q : g = h)
: idto2mor p • idto2mor q = idto2mor (p @ q).
Show proof.
Definition idto2mor_lwhisker
{x y z : C}
(f : x --> y)
{g h : y --> z}
(p : g = h)
: f ◃ idto2mor p
=
idto2mor (maponpaths (λ q, f · q) p).
Show proof.
Definition idto2mor_rwhisker
{x y z : C}
{f g : x --> y}
(h : y --> z)
(p : f = g)
: idto2mor p ▹ h
=
idto2mor (maponpaths (λ q, q · h) p).
Show proof.
Definition two_cat_lunitor_linvunitor
{x y : C}
(f : x --> y)
: two_cat_lunitor f • two_cat_linvunitor f = id2 _.
Show proof.
unfold two_cat_lunitor, two_cat_linvunitor.
rewrite idto2mor_comp.
rewrite pathsinv0r.
apply idpath.
rewrite idto2mor_comp.
rewrite pathsinv0r.
apply idpath.
Definition two_cat_linvunitor_lunitor
{x y : C}
(f : x --> y)
: two_cat_linvunitor f • two_cat_lunitor f = id2 _.
Show proof.
unfold two_cat_lunitor, two_cat_linvunitor.
rewrite idto2mor_comp.
rewrite pathsinv0l.
apply idpath.
rewrite idto2mor_comp.
rewrite pathsinv0l.
apply idpath.
Definition two_cat_runitor_rinvunitor
{x y : C}
(f : x --> y)
: two_cat_runitor f • two_cat_rinvunitor f = id2 _.
Show proof.
unfold two_cat_runitor, two_cat_rinvunitor.
rewrite idto2mor_comp.
rewrite pathsinv0r.
apply idpath.
rewrite idto2mor_comp.
rewrite pathsinv0r.
apply idpath.
Definition two_cat_rinvunitor_runitor
{x y : C}
(f : x --> y)
: two_cat_rinvunitor f • two_cat_runitor f = id2 _.
Show proof.
unfold two_cat_runitor, two_cat_rinvunitor.
rewrite idto2mor_comp.
rewrite pathsinv0l.
apply idpath.
rewrite idto2mor_comp.
rewrite pathsinv0l.
apply idpath.
Definition two_cat_lassociator_rassociator
{w x y z : C}
(f : w --> x)
(g : x --> y)
(h : y --> z)
: two_cat_lassociator f g h • two_cat_rassociator f g h = id2 _.
Show proof.
unfold two_cat_lassociator, two_cat_rassociator.
rewrite idto2mor_comp.
rewrite pathsinv0r.
apply idpath.
rewrite idto2mor_comp.
rewrite pathsinv0r.
apply idpath.
Definition two_cat_rassociator_lassociator
{w x y z : C}
(f : w --> x)
(g : x --> y)
(h : y --> z)
: two_cat_rassociator f g h • two_cat_lassociator f g h = id2 _.
Show proof.
unfold two_cat_lassociator, two_cat_rassociator.
rewrite idto2mor_comp.
rewrite pathsinv0l.
apply idpath.
rewrite idto2mor_comp.
rewrite pathsinv0l.
apply idpath.
Definition id1_lwhisker {a b : C} {f g : C⟦a, b⟧} (x : f ==> g)
: (identity a ◃ x) = two_cat_lunitor f • x • two_cat_linvunitor g.
Show proof.
rewrite <- vcomp_lunitor.
rewrite !vassocl.
rewrite two_cat_lunitor_linvunitor.
rewrite id2_right.
apply idpath.
rewrite !vassocl.
rewrite two_cat_lunitor_linvunitor.
rewrite id2_right.
apply idpath.
Definition rwhisker_id1 {a b : C} {f g : C⟦a, b⟧} (x : f ==> g)
: (x ▹ identity b) = two_cat_runitor f • x • two_cat_rinvunitor g.
Show proof.
rewrite <- vcomp_runitor.
rewrite !vassocl.
rewrite two_cat_runitor_rinvunitor.
rewrite id2_right.
apply idpath.
rewrite !vassocl.
rewrite two_cat_runitor_rinvunitor.
rewrite id2_right.
apply idpath.
Definition lwhisker_lwhisker_mor
{a b c d : C}
(f : a --> b)
(g : b --> c)
{h i : c --> d}
(τ : h ==> i)
: f ◃ (g ◃ τ)
=
two_cat_lassociator _ _ _
• (f · g ◃ τ)
• two_cat_rassociator _ _ _.
Show proof.
rewrite <- lwhisker_lwhisker.
rewrite !vassocl.
rewrite two_cat_lassociator_rassociator.
rewrite id2_right.
apply idpath.
rewrite !vassocl.
rewrite two_cat_lassociator_rassociator.
rewrite id2_right.
apply idpath.
Definition lwhisker_comp_mor
{a b c d : C}
(f : a --> b)
(g : b --> c)
{h i : c --> d}
(τ : h ==> i)
: f · g ◃ τ
=
two_cat_rassociator _ _ _
• (f ◃ (g ◃ τ))
• two_cat_lassociator _ _ _.
Show proof.
rewrite !vassocl.
refine (!_).
etrans.
{
apply maponpaths.
apply lwhisker_lwhisker.
}
rewrite !vassocr.
rewrite two_cat_rassociator_lassociator.
rewrite id2_left.
apply idpath.
refine (!_).
etrans.
{
apply maponpaths.
apply lwhisker_lwhisker.
}
rewrite !vassocr.
rewrite two_cat_rassociator_lassociator.
rewrite id2_left.
apply idpath.
Definition rwhisker_lwhisker_mor
{a b c d : C}
(f : a --> b)
{g h : b --> c}
(τ : g ==> h)
(i : c --> d)
: f ◃ (τ ▹ i)
=
two_cat_lassociator _ _ _
• ((f ◃ τ) ▹ i)
• two_cat_rassociator _ _ _.
Show proof.
rewrite <- rwhisker_lwhisker.
rewrite !vassocl.
rewrite two_cat_lassociator_rassociator.
rewrite id2_right.
apply idpath.
rewrite !vassocl.
rewrite two_cat_lassociator_rassociator.
rewrite id2_right.
apply idpath.
Definition lwhisker_rwhisker_mor
{a b c d : C}
(f : a --> b)
{g h : b --> c}
(τ : g ==> h)
(i : c --> d)
: (f ◃ τ) ▹ i
=
two_cat_rassociator _ _ _
• (f ◃ (τ ▹ i))
• two_cat_lassociator _ _ _.
Show proof.
rewrite !vassocl.
refine (!_).
etrans.
{
apply maponpaths.
apply rwhisker_lwhisker.
}
rewrite !vassocr.
rewrite two_cat_rassociator_lassociator.
rewrite id2_left.
apply idpath.
refine (!_).
etrans.
{
apply maponpaths.
apply rwhisker_lwhisker.
}
rewrite !vassocr.
rewrite two_cat_rassociator_lassociator.
rewrite id2_left.
apply idpath.
Definition rwhisker_rwhisker_mor
{a b c d : C}
{f g : a --> b}
(τ : f ==> g)
(h : b --> c)
(i : c --> d)
: τ ▹ h ▹ i
=
two_cat_rassociator _ _ _
• (τ ▹ h · i)
• two_cat_lassociator _ _ _.
Show proof.
rewrite !vassocl.
refine (!_).
etrans.
{
apply maponpaths.
refine (!_).
apply rwhisker_rwhisker.
}
rewrite !vassocr.
rewrite two_cat_rassociator_lassociator.
rewrite id2_left.
apply idpath.
refine (!_).
etrans.
{
apply maponpaths.
refine (!_).
apply rwhisker_rwhisker.
}
rewrite !vassocr.
rewrite two_cat_rassociator_lassociator.
rewrite id2_left.
apply idpath.
Definition rwhisker_comp_mor
{a b c d : C}
{f g : a --> b}
(τ : f ==> g)
(h : b --> c)
(i : c --> d)
: τ ▹ h · i
=
two_cat_lassociator _ _ _
• (τ ▹ h ▹ i)
• two_cat_rassociator _ _ _.
Show proof.
rewrite rwhisker_rwhisker.
rewrite !vassocl.
rewrite two_cat_lassociator_rassociator.
rewrite id2_right.
apply idpath.
rewrite !vassocl.
rewrite two_cat_lassociator_rassociator.
rewrite id2_right.
apply idpath.
Proposition idto2mor_left
{a b : C}
{f f' g : a --> b}
(p p' : f = f')
{τ τ' : f' ==> g}
(r : τ = τ')
: idto2mor p • τ
=
idto2mor p' • τ'.
Show proof.
Proposition idto2mor_right
{a b : C}
{f g g' : a --> b}
(p p' : g = g')
{τ τ' : f ==> g}
(r : τ = τ')
: τ • idto2mor p
=
τ' • idto2mor p'.
Show proof.
Definition arr_idto2mor_eq
{a b : C}
{f f' g g' : a --> b}
(p p' : f = f')
{τ τ' : f' ==> g}
(q q' : g = g')
(r : τ = τ')
: idto2mor p • τ • idto2mor q
=
idto2mor p' • τ' • idto2mor q'.
Show proof.
assert (p = p') as s.
{
apply homset_property.
}
induction s.
assert (q = q') as s.
{
apply homset_property.
}
induction s.
induction r.
apply idpath.
{
apply homset_property.
}
induction s.
assert (q = q') as s.
{
apply homset_property.
}
induction s.
induction r.
apply idpath.
Definition arr_idto2mor_eq2
{a b : C}
{f f' g g' h h' : a --> b}
(p p' : f = f')
{τ τ' : f' ==> g}
(q q' : g = g')
{θ θ' : g' ==> h}
(r r' : h = h')
(H₁ : τ = τ')
(H₂ : θ = θ')
: idto2mor p • τ • idto2mor q • θ • idto2mor r
=
idto2mor p' • τ' • idto2mor q' • θ' • idto2mor r'.
Show proof.
induction H₁, H₂.
use idto2mor_right.
apply maponpaths_2.
use idto2mor_right.
apply maponpaths_2.
apply maponpaths.
apply (homset_property C).
use idto2mor_right.
apply maponpaths_2.
use idto2mor_right.
apply maponpaths_2.
apply maponpaths.
apply (homset_property C).
Definition arr_idto2mor_eq3
{a b : C}
{f f' g g' h h' k k' : a --> b}
(p p' : f = f')
{τ τ' : f' ==> g}
(q q' : g = g')
{θ θ' : g' ==> h}
(r r' : h = h')
{ξ ξ' : h' ==> k}
(s s' : k = k')
(H₁ : τ = τ')
(H₂ : θ = θ')
(H₃ : ξ = ξ')
: idto2mor p • τ • idto2mor q • θ • idto2mor r • ξ • idto2mor s
=
idto2mor p' • τ' • idto2mor q' • θ' • idto2mor r' • ξ' • idto2mor s'.
Show proof.
induction H₁, H₂, H₃.
use idto2mor_right.
apply maponpaths_2.
use idto2mor_right.
apply maponpaths_2.
use idto2mor_right.
apply maponpaths_2.
apply maponpaths.
apply (homset_property C).
End IdTo2MorLaws.use idto2mor_right.
apply maponpaths_2.
use idto2mor_right.
apply maponpaths_2.
use idto2mor_right.
apply maponpaths_2.
apply maponpaths.
apply (homset_property C).
Definition is_two_setcat
(C : two_cat)
: UU
:= isaset C.
Definition two_setcat
: UU
:= ∑ (C : two_cat), is_two_setcat C.
Definition make_two_setcat
(C : two_cat)
(HC : is_two_setcat C)
: two_setcat
:= C ,, HC.
Coercion two_setcat_to_two_cat
(C : two_setcat)
: two_cat
:= pr1 C.
Proposition is_two_setcat_two_setcat
(C : two_setcat)
: isaset C.
Show proof.
Proposition is_setcategory_two_setcat
(C : two_setcat)
: is_setcategory C.
Show proof.
(C : two_cat)
: UU
:= isaset C.
Definition two_setcat
: UU
:= ∑ (C : two_cat), is_two_setcat C.
Definition make_two_setcat
(C : two_cat)
(HC : is_two_setcat C)
: two_setcat
:= C ,, HC.
Coercion two_setcat_to_two_cat
(C : two_setcat)
: two_cat
:= pr1 C.
Proposition is_two_setcat_two_setcat
(C : two_setcat)
: isaset C.
Show proof.
Proposition is_setcategory_two_setcat
(C : two_setcat)
: is_setcategory C.
Show proof.
Definition univalent_two_cat
: UU
:= ∑ (C : two_cat), is_univalent (category_from_two_cat_data C).
Definition make_univalent_two_cat
(C : two_cat)
(HC : is_univalent (category_from_two_cat_data C))
: univalent_two_cat
:= C ,, HC.
Coercion univalent_two_cat_to_two_cat
(C : univalent_two_cat)
: two_cat
:= pr1 C.
Proposition is_univalent_univalent_two_cat
(C : univalent_two_cat)
: is_univalent (category_from_two_cat_data C).
Show proof.
: UU
:= ∑ (C : two_cat), is_univalent (category_from_two_cat_data C).
Definition make_univalent_two_cat
(C : two_cat)
(HC : is_univalent (category_from_two_cat_data C))
: univalent_two_cat
:= C ,, HC.
Coercion univalent_two_cat_to_two_cat
(C : univalent_two_cat)
: two_cat
:= pr1 C.
Proposition is_univalent_univalent_two_cat
(C : univalent_two_cat)
: is_univalent (category_from_two_cat_data C).
Show proof.
Definition hom_precat_ob_mor
{C : two_cat}
(x y : C)
: precategory_ob_mor.
Show proof.
Definition hom_precat_data
{C : two_cat}
(x y : C)
: precategory_data.
Show proof.
Proposition hom_precat_laws
{C : two_cat}
(x y : C)
: is_precategory (hom_precat_data x y).
Show proof.
Definition hom_precat
{C : two_cat}
(x y : C)
: precategory.
Show proof.
Definition hom_cat
{C : two_cat}
(x y : C)
: category.
Show proof.
Definition locally_univalent_two_cat
(C : two_cat)
: UU
:= ∏ (x y : C), is_univalent (hom_cat x y).
Module Notations.
Notation "f '==>' g" := (two_cat_cells _ f g) (at level 60).
Notation "f '<==' g" := (two_cat_cells _ g f) (at level 60, only parsing).
Notation "x • y" := (vcomp2 x y) (at level 60).
Notation "f ◃ x" := (lwhisker f x) (at level 60). Notation "y ▹ g" := (rwhisker g y) (at level 60). Notation "x ⋆ y" := (hcomp x y) (at level 50, left associativity).
End Notations.
{C : two_cat}
(x y : C)
: precategory_ob_mor.
Show proof.
Definition hom_precat_data
{C : two_cat}
(x y : C)
: precategory_data.
Show proof.
use make_precategory_data.
- exact (hom_precat_ob_mor x y).
- exact (λ (f : x --> y), id2 f).
- exact (λ (f g h : x --> y) (τ : f ==> g) (θ : g ==> h), τ • θ).
- exact (hom_precat_ob_mor x y).
- exact (λ (f : x --> y), id2 f).
- exact (λ (f g h : x --> y) (τ : f ==> g) (θ : g ==> h), τ • θ).
Proposition hom_precat_laws
{C : two_cat}
(x y : C)
: is_precategory (hom_precat_data x y).
Show proof.
use is_precategory_one_assoc_to_two.
repeat split ; cbn.
- intros f g τ.
apply id2_left.
- intros f g τ.
apply id2_right.
- intros f g h k τ₁ τ₂ τ₃.
apply vassocr.
repeat split ; cbn.
- intros f g τ.
apply id2_left.
- intros f g τ.
apply id2_right.
- intros f g h k τ₁ τ₂ τ₃.
apply vassocr.
Definition hom_precat
{C : two_cat}
(x y : C)
: precategory.
Show proof.
Definition hom_cat
{C : two_cat}
(x y : C)
: category.
Show proof.
Definition locally_univalent_two_cat
(C : two_cat)
: UU
:= ∏ (x y : C), is_univalent (hom_cat x y).
Module Notations.
Notation "f '==>' g" := (two_cat_cells _ f g) (at level 60).
Notation "f '<==' g" := (two_cat_cells _ g f) (at level 60, only parsing).
Notation "x • y" := (vcomp2 x y) (at level 60).
Notation "f ◃ x" := (lwhisker f x) (at level 60). Notation "y ▹ g" := (rwhisker g y) (at level 60). Notation "x ⋆ y" := (hcomp x y) (at level 50, left associativity).
End Notations.