Theorems · Inductive type · category theory

HomotopicalAlgebra.AttachCells

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {α : Type t} →
      {A B : α → C} → ((a : α) → A a ⟶ B a) → {X₁ X₂ : C} → (X₁ ⟶ X₂) → Type (max (max (max t u) v) (w + 1))

Given a family of morphisms g a : A a ⟶ B a and a morphism f : X₁ ⟶ X₂, this structure contains the data and properties which expresses that X₂ is obtained from X₁ by attaching cells of the form g a.

Defined in

Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells

Cited by

32 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

CategoryTheory.Category