Definition mors_to_arrow_mor {C : category} {a b x y : C} (f : a --> b) (g : x --> y) (h : a --> x) (k : b --> y) (H : h · g = f · k) : (mor_to_arrow_ob f) --> (mor_to_arrow_ob g). Proof. use tpair. - exact (make_dirprod h k). - abstract (exact H). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.SIP. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.