proposition: Lemma colimit_to_cocone_id : forall a b, is_colimit a -> a = b -> colimit_to_cocone a b = id (cocone_target b) (vertex b).
proof: Proof. ir. wr H0. cp H. uh H1; ee. uh H1; ee. ap H3. uhg; ee. am. ap mor_colimit_to_cocone. am. am. tv. tv. rww source_colimit_to_cocone. uhg; ee. am. ap mor_id. ap ob_vertex. am. rw source_id. tv. ap ob_vertex. am. rww cocone_compose_colimit_to_cocone. rww cocone_compose_id. Qed.
imports: Arith limits