proposition: Lemma all_arrow_zero_to : forall z u, mor (function_cat z) u -> source u = (R 0) -> u = arrow_zero_to (target u).
proof: Proof. ir. ap mor_fc_extensionality. sh z. ee; try am. ap mor_fc_arrow_zero_to. wr H0. wr ob_function_cat. rww ob_source. wr ob_function_cat. rww ob_target. rww source_arrow_zero_to. rww target_arrow_zero_to. ir. rwi H0 H1. rwi zero_emptyset H1. nin H1. nin x0. Qed.
imports: Arith ordinal nat_trans