proposition: Lemma fmor_colimit_to_cocone : fmor f (colimit_to_cocone b a) = colimit_to_cocone (cocone_pushdown f b) (cocone_pushdown f a).
proof: Proof. cp K4. uh H; ee. uh H; ee. assert (is_cocone b). cp K1. uh H2; ee; lu. assert (is_coversal b). cp K1; lu. ap H1. uhg; ee. app is_cocone_cocone_pushdown. rww cocone_target_cocone_pushdown. app mor_fmor. rw K3. app mor_colimit_to_cocone. rww source_fmor. rww vertex_cocone_pushdown. rww source_colimit_to_cocone. rw K3; app mor_colimit_to_cocone. uhg; ee. app is_cocone_cocone_pushdown. rww cocone_target_cocone_pushdown. ap mor_colimit_to_cocone. ap is_cocone_cocone_pushdown. am. am. rw K3. uf cocone_target. rww K2. am. rww cosocle_cocone_pushdown. rw cosocle_cocone_pushdown. rww K2. rww cocone_target_cocone_pushdown. rw source_colimit_to_cocone. tv. app is_cocone_cocone_pushdown. rw K3; uf cocone_target; rww K2. am. rww cosocle_cocone_pushdown. rw cosocle_cocone_pushdown. rww K2. rw cocone_compose_cocone_pushdown_fmor_colimit_to_cocone. sy; rw cocone_compose_colimit_to_cocone. tv. app is_cocone_cocone_pushdown. rw K3; uf cocone_target; rww K2. am. rw cosocle_cocone_pushdown. rw cosocle_cocone_pushdown. rww K2. Qed.
imports: Arith limits