instIsGoodSymmOfRespectsIsoCofibrations

English

If cofibrations respect isomorphisms and C has binary coproducts, then the symmetric cylinder P.symm is Very Good.

Русский

Если кофефибрации сохраняют изоморфизмы и существуют двоичные копродукты, то симметричный цилиндр P.symm есть Very Good.

LaTeX

$$$P.symm.IsVeryGood$$$

Lean4

instance [HasBinaryCoproducts C] [CategoryWithCofibrations C] [P.IsGood] [(cofibrations C).RespectsIso] : P.symm.IsGood
    where
  cofibration_i := by
    have hi : cofibrations C P.i := by rw [← cofibration_iff]; infer_instance
    rw [P.symm_i, cofibration_iff]
    refine ((cofibrations C).arrow_mk_iso_iff ?_).2 hi
    exact Arrow.isoMk (coprod.braiding A A) (Iso.refl _)

Похожие утверждения