proposition: Lemma mor_cocommutation : mor (target f) cocommutation.
proof: Proof. uf cocommutation. ap mor_colimit_to_cocone. app is_cocone_cocone_pushdown. am. rww cosocle_cocone_pushdown. rww cocone_target_b. Qed.
imports: Arith limits