proposition: Lemma comp_inclusion_cat : forall z u v, mor (inclusion_cat z) u -> mor (inclusion_cat z) v -> source u = target v -> comp (inclusion_cat z) u v = fa_inclusion (source v) (target u).
proof: Proof. ir. ap inclusion_cat_mor_extens. rww source_comp. rww source_fa_inclusion. rww target_comp. rww target_fa_inclusion. sh z. ee. rww mor_comp. rw mor_inclusion_cat. ee. rw source_fa_inclusion. wr ob_inclusion_cat. rww ob_source. rw target_fa_inclusion. wr ob_inclusion_cat. rww ob_target. uhg. ee. rw source_fa_inclusion. rw target_fa_inclusion. app inclusion_cat_sub_trans. sh z; ee; try am. rw source_fa_inclusion. rww target_fa_inclusion. Qed.
imports: Arith ordinal nat_trans