Theorems · Definition · category theory

HomotopicalAlgebra.RelativeCellComplex.Cells.mk.noConfusion

{C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {J : Type w'} →
      {inst_1 : LinearOrder J} →
        {inst_2 : OrderBot J} →
          {inst_3 : SuccOrder J} →
            {inst_4 : WellFoundedLT J} →
              {α : J → Type t} →
                {A B : (j : J) → α j → C} →
                  {basicCell : (j : J) → (i : α j) → A j i ⟶ B j i} →
                    {X Y : C} →
                      {f : X ⟶ Y} →
                        {c : HomotopicalAlgebra.RelativeCellComplex basicCell f} →
                          {P : Sort u_2} →
                            {j : J} →
                              {hj : ¬IsMax j} →
                                {k : (c.attachCells j hj).ι} →
                                  {j' : J} →
                                    {hj' : ¬IsMax j'} →
                                      {k' : (c.attachCells j' hj').ι} →
                                        { j := j, hj := hj, k := k } = { j := j', hj := hj', k := k' } →
                                          (j ≍ j' → k ≍ k' → P) → P

Defined in

Mathlib.AlgebraicTopology.RelativeCellComplex.Basic

Cited by

1 results in Mathlib

Foundations

Depth 25 from the axioms · uses propext