proposition: Lemma subcategory_inclusion_axioms : forall a b, is_subcategory a b -> Functor.axioms (Umorphism.inclusion a b).
proof: Proof. ir. uh H; ee. uhg; ee. uf inclusion. app Umorphism.create_like. rww source_inclusion. rww target_inclusion. ir. rw target_inclusion. rwi source_inclusion H6. rww fob_inclusion. au. ir. rwi source_inclusion H6. rw target_inclusion. rww fob_inclusion. rw source_inclusion. rww fmor_inclusion. sy; au. app mor_id. ir. rwi source_inclusion H6. rw target_inclusion. rww fmor_inclusion. au. ir. rwi source_inclusion H6. rww fmor_inclusion. rww fob_inclusion. rww ob_source. ir. rwi source_inclusion H6. rww fmor_inclusion. rww fob_inclusion. rww ob_target. ir. rwi source_inclusion H6. rwi source_inclusion H7. rw target_inclusion. rww fmor_inclusion. rww fmor_inclusion. rww source_inclusion. rww fmor_inclusion. sy; au. rww mor_comp. Qed.
imports: Arith ordinal nat_trans