proposition: Lemma eqzmap_cone_compose : forall c z, is_cone c -> cone_source c = twoarrow_cat -> cone_composable c z -> eqzmap (cone_compose c z) = comp (cone_target c) (eqzmap c) z.
proof: Proof. ir. uf eqzmap. rw edge_cone_compose. tv. rw H0; ap ob_twoarrow_cat. am. Qed.
imports: Arith colimits little_cat fc_limits cardinal