proposition: Lemma ob_subcategory : forall a obp morp x, subcategory_property a obp morp -> ob (subcategory a obp morp) x = (ob a x & obp x).
proof: Proof. ir. app iff_eq; ir. assert (is_ob (subcategory a obp morp) x). app ob_is_ob. rwi is_ob_subcategory H1. xd. app is_ob_ob. uh H; ee; am. ap is_ob_ob. app subcategory_axioms. rw is_ob_subcategory. xd. app ob_is_ob. Qed.
imports: Arith ordinal nat_trans