proposition: Lemma colimit_preservation_invariance : is_colimit (cocone_pushdown f a).
proof: Proof. ir. ap (colimit_to_cocone_invertible_is_colimit (a:= (cocone_pushdown f a)) (b:=(cocone_pushdown f b))). am. app is_cocone_cocone_pushdown. cp K0; lu. rw K3; uf cocone_target; rww K2. rw cosocle_cocone_pushdown. rw cosocle_cocone_pushdown. rww K2. wr fmor_colimit_to_cocone. rw cocone_target_cocone_pushdown. ap invertible_fmor_ctl. am. cp K0; lu. am. am. am. am. Qed.
imports: Arith limits