fact: Definition get_predoublecategory_interchange_id_hor {C : predoublecategory} {a b c: C} (f: a -h-> b) (g: b -h-> c) : ver_sq_identity(f ·h g) = (ver_sq_identity f) ·sqh (ver_sq_identity g) := (pr12 (pr222 (pr222 C))) a b c f g.
imports: UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Notations UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence