proposition: Lemma target_cocommutation : target cocommutation = fob f (vertex a).
proof: Proof. uf cocommutation. rw target_colimit_to_cocone. rww vertex_cocone_pushdown. app is_cocone_cocone_pushdown. am. rww cosocle_cocone_pushdown. Qed.
imports: Arith limits