Definition prebicat_laws (C : prebicat_data) : 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) (f g : C⟦a, b⟧) (x : f ==> g), (identity _ ◃ x) • lunitor g = lunitor f • x) × (∏ (a b : C) (f g : C⟦a, b⟧) (x : f ==> g), (x ▹ identity _) • runitor g = runitor f • x) × (∏ (a b c d : C) (f : C⟦a, b⟧) (g : C⟦b, c⟧) (h i : c --> d) (x : h ==> i), f ◃ (g ◃ x) • lassociator _ _ _ = lassociator _ _ _ • (f · g ◃ x)) × (∏ (a b c d : C) (f : C⟦a, b⟧) (g h : C⟦b, c⟧) (i : c --> d) (x : g ==> h), (f ◃ (x ▹ i)) • lassociator _ _ _ = lassociator _ _ _ • ((f ◃ x) ▹ i)) × (∏ (a b c d : C) (f g : C⟦a, b⟧) (h : C⟦b, c⟧) (i : c --> d) (x : f ==> g), lassociator _ _ _ • ((x ▹ h) ▹ i) = (x ▹ h · i) • lassociator _ _ _) × (∏ (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 : C⟦a, b⟧), lunitor f • linvunitor _ = id2 _) × (∏ (a b : C) (f : C⟦a, b⟧), linvunitor f • lunitor _ = id2 _) × (∏ (a b : C) (f : C⟦a, b⟧), runitor f • rinvunitor _ = id2 _) × (∏ (a b : C) (f : C⟦a, b⟧), rinvunitor f • runitor _ = id2 _) × (∏ (a b c d : C) (f : C⟦a, b⟧) (g : C⟦b, c⟧) (h : c --> d), lassociator f g h • rassociator _ _ _ = id2 _) × (∏ (a b c d : C) (f : C⟦a, b⟧) (g : C⟦b, c⟧) (h : c --> d), rassociator f g h • lassociator _ _ _ = id2 _) × (∏ (a b c : C) (f : C⟦a, b⟧) (g : C⟦b, c⟧), lassociator _ _ _ • (runitor f ▹ g) = f ◃ lunitor g) × (∏ (a b c d e: C) (f : C⟦a, b⟧) (g : C⟦b, c⟧) (h : c --> d) (i : C⟦d, e⟧), (f ◃ lassociator g h i) • lassociator _ _ _ • (lassociator _ _ _ ▹ i) = lassociator f g _ • lassociator _ _ _).
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.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.PrecategoryBinProduct.