Theorems · Definition · algebraic topology

CategoryTheory.SimplicialObject.Split.Hom.mk.noConfusion

{C : Type u_1} →
  {inst : CategoryTheory.Category.{v_1, u_1} C} →
    {S₁ S₂ : CategoryTheory.SimplicialObject.Split C} →
      {P : Sort u} →
        {F : S₁.X ⟶ S₂.X} →
          {f : (n : ℕ) → S₁.s.N n ⟶ S₂.s.N n} →
            {comm :
                autoParam
                  (∀ (n : ℕ),
                    CategoryTheory.CategoryStruct.comp (S₁.s.ι n) (F.app (Opposite.op { len := n })) =
                      CategoryTheory.CategoryStruct.comp (f n) (S₂.s.ι n))
                  CategoryTheory.SimplicialObject.Split.Hom.comm._autoParam} →
              {F' : S₁.X ⟶ S₂.X} →
                {f' : (n : ℕ) → S₁.s.N n ⟶ S₂.s.N n} →
                  {comm' :
                      autoParam
                        (∀ (n : ℕ),
                          CategoryTheory.CategoryStruct.comp (S₁.s.ι n) (F'.app (Opposite.op { len := n })) =
                            CategoryTheory.CategoryStruct.comp (f' n) (S₂.s.ι n))
                        CategoryTheory.SimplicialObject.Split.Hom.comm._autoParam} →
                    { F := F, f := f, comm := comm } = { F := F', f := f', comm := comm' } → (F ≍ F' → f ≍ f' → P) → P

Defined in

Mathlib.AlgebraicTopology.SimplicialObject.Split

Cited by

1 results in Mathlib

Foundations

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