proposition: Lemma mor_subcategory : forall a obp morp u, subcategory_property a obp morp -> mor (subcategory a obp morp) u = (mor a u & morp u).
proof: Proof. ir. app iff_eq; ir. assert (is_mor (subcategory a obp morp) u). app mor_is_mor. rwi is_mor_subcategory H1. xd. app is_mor_mor. uh H; ee; am. ap is_mor_mor. app subcategory_axioms. rw is_mor_subcategory. xd. app mor_is_mor. Qed.
imports: Arith ordinal nat_trans