Theorems · Definition · category theory

HomotopicalAlgebra.AttachCells.reindex

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {α : Type t} →
      {A B : α → C} →
        {g : (a : α) → A a ⟶ B a} →
          {X₁ X₂ : C} →
            {f : X₁ ⟶ X₂} →
              (c : HomotopicalAlgebra.AttachCells g f) → {ι' : Type w'} → ι' ≃ c.ι → HomotopicalAlgebra.AttachCells g f

This definition allows the replacement of the ι field of a AttachCells g f structure by an equivalent type.

Defined in

Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells

Cited by

9 results in Mathlib

Foundations

Depth 35 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Category