proposition: Lemma comp_umorphism_cat : forall z u v, mor (umorphism_cat z) u -> mor (umorphism_cat z) v -> source u = target v -> comp (umorphism_cat z) u v = Umorphism.compose u v.
proof: Proof. ir. uf umorphism_cat. rw comp_from_arrows. tv. app mor_is_mor. app mor_is_mor. am. Qed.
imports: Arith ordinal nat_trans