proposition: Lemma cocone_compose_cocone_pushdown_fmor_colimit_to_cocone : cocone_compose (fmor f (colimit_to_cocone b a)) (cocone_pushdown f b) = cocone_pushdown f a.
proof: Proof. assert (lem0 : is_cocone b). cp K1. uh H; ee. lu. assert (lem1 : a = cocone_compose (colimit_to_cocone b a) b). rww cocone_compose_colimit_to_cocone. transitivity (cocone_pushdown f (cocone_compose (colimit_to_cocone b a) b)). assert (cocone_pushdown f (cocone_compose (colimit_to_cocone b a) b) = cocone_compose (fmor f (colimit_to_cocone b a)) (cocone_pushdown f b)). rw cocone_pushdown_cocone_compose. reflexivity. am. am. am. app mor_colimit_to_cocone. rww source_colimit_to_cocone. rw H. reflexivity. assert (cocone_compose (colimit_to_cocone b a) b = a). rw cocone_compose_colimit_to_cocone. tv. am. am. am. rw H. reflexivity. Qed.
imports: Arith limits