Definition two_cat_laws (C : two_cat_category) : UU := (∏ (a b : C) (f g : C⟦a, b⟧) (x : f ==> g), id2 f • x = x) × (∏ (a b : C) (f g : C⟦a, b⟧) (x : f ==> g), x • id2 g = x) × (∏ (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) × (∏ (a b c : C) (f : C⟦a, b⟧) (g : C⟦b, c⟧), f ◃ id2 g = id2 _) × (∏ (a b c : C) (f : C⟦a, b⟧) (g : C⟦b, c⟧), id2 f ▹ g = id2 _) × (∏ (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)) × (∏ (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) × (∏ (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)) × (∏ (a b : C) (f g : C⟦a, b⟧) (x : f ==> g), (identity a ◃ x) • idto2mor (id_left g) = idto2mor (id_left f) • x) × (∏ (a b : C) (f g : C⟦a, b⟧) (x : f ==> g), (x ▹ identity b) • idto2mor (id_right g) = idto2mor (id_right f) • x) × (∏ (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)) × (∏ (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))) × (∏ (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)).
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.