Definition three_mor_mor12 {C : category} {xxx yyy : three C} (fff : xxx --> yyy) : (three_mor12 xxx) --> (three_mor12 yyy). Proof. use mors_to_arrow_mor. - exact (three_mor11 fff). - exact (three_mor22 fff). - abstract ( exact (pathsinv0 (pr2 (three_mor_comm fff))) ). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.Arrow.