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