fact: Definition prebicat_2_id_comp_struct (C : prebicat_1_id_comp_cells) : UU := (∏ (a b : C) (f : C⟦a, b⟧), f ==> f) × (∏ (a b : C) (f : C⟦a, b⟧), identity _ · f ==> f) × (∏ (a b : C) (f : C⟦a, b⟧), f · identity _ ==> f) × (∏ (a b : C) (f : C⟦a, b⟧), identity _ · f <== f) × (∏ (a b : C) (f : C⟦a, b⟧), f · identity _ <== f) × (∏ (a b c d : C) (f : C⟦a, b⟧) (g : C⟦b, c⟧) (h : C⟦c, d⟧), (f · g) · h ==> f · (g · h)) × (∏ (a b c d : C) (f : C⟦a, b⟧) (g : C⟦b, c⟧) (h : C⟦c, d⟧), f · (g · h) ==> (f · g) · h) × (∏ (a b : C) (f g h : C⟦a, b⟧), f ==> g -> g ==> h -> f ==> h) × (∏ (a b c : C) (f : C⟦a, b⟧) (g1 g2 : C⟦b, c⟧), g1 ==> g2 → f · g1 ==> f · g2) × (∏ (a b c : C) (f1 f2 : C⟦a, b⟧) (g : C⟦b, c⟧), f1 ==> f2 → f1 · g ==> f2 · g).
imports: UniMath.Tactics.EnsureStructuredProofs UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.PrecategoryBinProduct