proposition: Lemma und_ver_cat_morphism_eq_principle {C: predoublecategory_hor_sq} {c d : und_ver_cat_ob C} (f g : und_ver_cat_ob_mor C c d) (equp: (pr1 f) = (pr1 g)) (eqdown: (pr12 f) = (pr12 g)) (eqmid: (pr22 f) = boundary_sq_transport (equp) (eqdown) (pr22 g) ) : f = g.
proof: Proof. induction f as [ f1 [ f2 sq1 ]]. induction g as [ g1 [ g2 sq2 ]]. cbn in *. induction equp. induction eqdown. apply maponpaths. apply maponpaths. exact (eqmid). Defined.
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