Definition hcomp_bicat_laws (B : hcomp_bicat_data) : UU := (∏ (b₁ b₂ : B) (f g : hb_mor b₁ b₂) (α : hb_cell f g), hb_vcomp (hb_id2 _) α = α) × (∏ (b₁ b₂ : B) (f g : hb_mor b₁ b₂) (α : hb_cell f g), hb_vcomp α (hb_id2 _) = α) × (∏ (b₁ b₂ : B) (f₁ f₂ f₃ f₄ : hb_mor b₁ b₂) (α : hb_cell f₁ f₂) (β : hb_cell f₂ f₃) (γ : hb_cell f₃ f₄), hb_vcomp α (hb_vcomp β γ) = hb_vcomp (hb_vcomp α β) γ) × (∏ (b₁ b₂ : B) (f₁ f₂ f₃ f₄ : hb_mor b₁ b₂) (α : hb_cell f₁ f₂) (β : hb_cell f₂ f₃) (γ : hb_cell f₃ f₄), hb_vcomp (hb_vcomp α β) γ = hb_vcomp α (hb_vcomp β γ)) × (∏ (b₁ b₂ : B) (f g : hb_mor b₁ b₂), isaset (hb_cell f g)) × (∏ (b₁ b₂ b₃ : B) (f : hb_mor b₁ b₂) (g : hb_mor b₂ b₃), hb_hcomp (hb_id2 f) (hb_id2 g) = hb_id2 (hb_comp1 f g)) × (∏ (b₁ b₂ b₃ : B) (f₁ g₁ h₁ : hb_mor b₁ b₂) (f₂ g₂ h₂ : hb_mor b₂ b₃) (α₁ : hb_cell f₁ g₁) (α₂ : hb_cell f₂ g₂) (β₁ : hb_cell g₁ h₁) (β₂ : hb_cell g₂ h₂), hb_hcomp (hb_vcomp α₁ β₁) (hb_vcomp α₂ β₂) = hb_vcomp (hb_hcomp α₁ α₂) (hb_hcomp β₁ β₂)) × (∏ (a b c d : B) (f₁ f₂ : hb_mor a b) (g₁ g₂ : hb_mor b c) (h₁ h₂ : hb_mor c d) (α₁ : hb_cell f₁ f₂) (α₂ : hb_cell g₁ g₂) (α₃ : hb_cell h₁ h₂), hb_vcomp (hb_hcomp α₁ (hb_hcomp α₂ α₃)) (hb_rassoc _ _ _) = hb_vcomp (hb_rassoc _ _ _) (hb_hcomp (hb_hcomp α₁ α₂) α₃)) × (∏ (a b : B) (f₁ f₂ : hb_mor a b) (α : hb_cell f₁ f₂), hb_vcomp (hb_hcomp (hb_id2 (hb_id1 a)) α) (hb_lunit f₂) = hb_vcomp (hb_lunit f₁) α) × (∏ (a b : B) (f₁ f₂ : hb_mor a b) (α : hb_cell f₁ f₂), hb_vcomp (hb_hcomp α (hb_id2 (hb_id1 b))) (hb_runit f₂) = hb_vcomp (hb_runit f₁) α) × (∏ (b₁ b₂ b₃ b₄ : B) (f : hb_mor b₁ b₂) (g : hb_mor b₂ b₃) (h : hb_mor b₃ b₄), hb_vcomp (hb_rassoc f g h) (hb_lassoc f g h) = hb_id2 _) × (∏ (b₁ b₂ b₃ b₄ : B) (f : hb_mor b₁ b₂) (g : hb_mor b₂ b₃) (h : hb_mor b₃ b₄), hb_vcomp (hb_lassoc f g h) (hb_rassoc f g h) = hb_id2 _) × (∏ (b₁ b₂ : B) (f : hb_mor b₁ b₂), hb_vcomp (hb_lunit f) (hb_linvunit f) = hb_id2 _) × (∏ (b₁ b₂ : B) (f : hb_mor b₁ b₂), hb_vcomp (hb_linvunit f) (hb_lunit f) = hb_id2 _) × (∏ (b₁ b₂ : B) (f : hb_mor b₁ b₂), hb_vcomp (hb_runit f) (hb_rinvunit f) = hb_id2 _) × (∏ (b₁ b₂ : B) (f : hb_mor b₁ b₂), hb_vcomp (hb_rinvunit f) (hb_runit f) = hb_id2 _) × (∏ (a b c d e : B) (k : hb_mor a b) (h : hb_mor b c) (g : hb_mor c d) (f : hb_mor d e), hb_vcomp (hb_rassoc k h (hb_comp1 g f)) (hb_rassoc (hb_comp1 k h) g f) = hb_vcomp (hb_vcomp (hb_hcomp (hb_id2 k) (hb_rassoc h g f)) (hb_rassoc k (hb_comp1 h g) f)) (hb_hcomp (hb_rassoc k h g) (hb_id2 f))) × (∏ (a b c : B) (f : hb_mor a b) (g : hb_mor b c), hb_hcomp (hb_id2 f) (hb_lunit g) = hb_vcomp (hb_rassoc f (hb_id1 b) g) (hb_hcomp (hb_runit f) (hb_id2 g))).
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.Bicategories.WkCatEnrichment.prebicategory. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.BicategoryLaws.