proposition: Lemma comp_colimit_to_cocone_inversely : forall a b c, is_colimit a -> is_colimit b -> cosocle a = cosocle b -> cocone_target a = c -> comp c (colimit_to_cocone a b) (colimit_to_cocone b a) = id c (vertex b).
proof: Proof. ir. assert (cocone_target b = c). uf cocone_target. wr H1. am. cp H; cp H0. uh H4; uh H5; ee. uh H4; uh H5. ee. assert (composable c (colimit_to_cocone a b) (colimit_to_cocone b a)). ap show_composable. app mor_colimit_to_cocone. sy; am. sy; am. app mor_colimit_to_cocone. sy; am. rww source_colimit_to_cocone. rww target_colimit_to_cocone. sy; am. ap H8. uhg; ee. am. rw H3. rww mor_comp. ap mor_colimit_to_cocone. am. am. sy; am. sy; am. app mor_colimit_to_cocone. sy; am. rw source_colimit_to_cocone. rww target_colimit_to_cocone. am. am. sy; am. rw source_comp. rww source_colimit_to_cocone. app mor_colimit_to_cocone. sy; am. sy; am. app mor_colimit_to_cocone. sy; am. rw source_colimit_to_cocone. rww target_colimit_to_cocone. am. am. sy; am. uhg; ee. am. rw H3. ap mor_id. wr H3. ap ob_vertex. am. rw source_id. tv. wr H3; app ob_vertex. wr H3. wr cocone_compose_cocone_compose. rw cocone_compose_colimit_to_cocone. rw cocone_compose_colimit_to_cocone. rw cocone_compose_id. tv. am. am. am. sy; am. am. am. am. uhg; ee. am. app mor_colimit_to_cocone. rww source_colimit_to_cocone. rww H3. Qed.
imports: Arith limits