proposition: Proposition bicat_to_hor_id_laws : hor_id_laws bicat_to_hor_id_data.
proof: Proof. split. - intro x ; cbn. rewrite runitor_lunitor_identity. rewrite lunitor_linvunitor. apply idpath. - intros x y z p q. induction p, q ; cbn. rewrite !id2_left, id2_right. rewrite lunitor_runitor_identity. rewrite runitor_rinvunitor. apply idpath. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Core.Setcategories UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos UniMath.CategoryTheory.TwoSidedDisplayedCats.Strictness UniMath.CategoryTheory.Categories.StandardCategories UniMath.CategoryTheory.Groupoids UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Strictness UniMath.Bicategories.Core.Univalence UniMath.Bicategories.Core.Unitors UniMath.Bicategories.Core.BicategoryLaws UniMath.Bicategories.Morphisms.Adjunctions UniMath.Bicategories.DoubleCategories.Basics.DoubleCategoryBasics UniMath.Bicategories.DoubleCategories.Core.DoubleCats UniMath.Bicategories.DoubleCategories.Core.PseudoDoubleSetCats