proposition: Lemma source_cocommutation : source cocommutation = vertex b.
proof: Proof. ir. uf cocommutation. rw source_colimit_to_cocone. tv. app is_cocone_cocone_pushdown. am. rww cosocle_cocone_pushdown. Qed.
imports: Arith limits