proposition: Lemma invertible_cocommutation_is_colimit_cocone_pushdown : forall c, target f = c -> invertible c cocommutation = is_colimit (cocone_pushdown f a).
proof: Proof. ir. wr H. ap iff_eq; ir. wr cocone_compose_cocommutation. app is_colimit_cocone_compose. ap cocone_composable_cocommutation. rww cocone_target_b. uf cocommutation. ap invertible_colimit_to_cocone. am. am. rww cosocle_cocone_pushdown. sy; am. rww cocone_target_b. Qed.
imports: Arith limits