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. 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.
Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence.