fact: Definition hcomp_bicat_data : UU := ∑ (ob : UU) (mor : ob → ob → UU) (cell : ∏ (x y : ob), mor x y → mor x y → UU) (id1 : ∏ (x : ob), mor x x) (comp1 : ∏ (x y z : ob), mor x y → mor y z → mor x z), (∏ (x y : ob) (f : mor x y), cell _ _ f f) × (∏ (x y : ob) (f g h : mor x y), cell _ _ f g → cell _ _ g h → cell _ _ f h) × (∏ (x y : ob) (f : mor x y), cell _ _ (comp1 _ _ _ f (id1 y)) f) × (∏ (x y : ob) (f : mor x y), cell _ _ f (comp1 _ _ _ f (id1 y))) × (∏ (x y : ob) (f : mor x y), cell _ _ (comp1 _ _ _ (id1 x) f) f) × (∏ (x y : ob) (f : mor x y), cell _ _ f (comp1 _ _ _ (id1 x) f)) × (∏ (w x y z : ob) (f : mor w x) (g : mor x y) (h : mor y z), cell _ _ (comp1 _ _ _ (comp1 _ _ _ f g) h) (comp1 _ _ _ f (comp1 _ _ _ g h))) × (∏ (w x y z : ob) (f : mor w x) (g : mor x y) (h : mor y z), cell _ _ (comp1 _ _ _ f (comp1 _ _ _ g h)) (comp1 _ _ _ (comp1 _ _ _ f g) h)) × (∏ (x y z : ob) (f₁ f₂ : mor x y) (g₁ g₂ : mor y z), cell _ _ f₁ f₂ → cell _ _ g₁ g₂ → cell _ _ (comp1 _ _ _ f₁ g₁) (comp1 _ _ _ f₂ g₂)).
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.PrecategoryBinProduct UniMath.Bicategories.WkCatEnrichment.prebicategory UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.BicategoryLaws