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).
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.