Definition get_predoublecategory_ver_unitor_coherence {C : predoublecategory} {a b c: C} (f: a -v-> b) (g: b -v-> c) : ( ((pr1 (get_ver_associator f (ver_identity b) g)) ·sqh ( (pr1 (get_ver_right_unitor f)) ·sqv (hor_sq_identity g) )) = hor_trans_id_left_sq ((hor_sq_identity f) ·sqv (pr1 (get_ver_left_unitor g)))) := (pr12 (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.