proposition: Lemma colimit_to_cocone_refl : forall a, is_colimit a -> colimit_to_cocone a a = id (cocone_target a) (vertex a).
proof: Proof. ir. transitivity (comp (cocone_target a) (colimit_to_cocone a a) (colimit_to_cocone a a)). wr colimit_to_cocone_cocone_compose. rw cocone_compose_colimit_to_cocone. tv. lu. am. tv. lu. app cocone_composable_colimit_to_cocone. lu. tv. rww comp_colimit_to_cocone_inversely. Qed.
imports: Arith limits