Definition get_predoublecategory_interchange_id_ver {C : predoublecategory} {a b c: C} (f: a -v-> b) (g: b -v-> c) : (hor_sq_identity f) ·sqv (hor_sq_identity g) =hor_sq_identity(f ·v g) := (pr122 (pr222 (pr222 C))) a b c f g.
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.