proposition: Lemma are_inverse_colimit_to_cocone : forall a b c, is_colimit a -> is_colimit b -> cosocle a = cosocle b -> cocone_target a = c -> are_inverse c (colimit_to_cocone a b) (colimit_to_cocone b a).
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. uhg; ee; try am. 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. rww target_colimit_to_cocone. rww source_colimit_to_cocone. sy; am. rw source_colimit_to_cocone. app comp_colimit_to_cocone_inversely. am. am. am. rww comp_colimit_to_cocone_inversely. rww source_colimit_to_cocone. sy; am. sy; am. Qed.
imports: Arith limits