Theorems · Definition · category theory

CategoryTheory.SmallObject.SuccStruct.Iteration.mk.noConfusion

{C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {J : Type w} →
      {Φ : CategoryTheory.SmallObject.SuccStruct C} →
        {inst_1 : LinearOrder J} →
          {inst_2 : SuccOrder J} →
            {inst_3 : OrderBot J} →
              {inst_4 : CategoryTheory.Limits.HasIterationOfShape J C} →
                {inst_5 : WellFoundedLT J} →
                  {j : J} →
                    {P : Sort u_1} →
                      {F : CategoryTheory.Functor (↑(Set.Iic j)) C} →
                        {obj_bot : F.obj ⟨⊥, ⋯⟩ = Φ.X₀} →
                          {arrowSucc_eq :
                              ∀ (i : J) (hi : i < j),
                                CategoryTheory.SmallObject.SuccStruct.arrowSucc F i hi = Φ.toSuccArrow (F.obj ⟨i, ⋯⟩)} →
                            {arrowMap_limit :
                                ∀ (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j) (k : J) (hk : k < i),
                                  CategoryTheory.SmallObject.SuccStruct.arrowMap F k i ⋯ hij =
                                    CategoryTheory.SmallObject.SuccStruct.arrowι
                                      (CategoryTheory.SmallObject.restrictionLT F hij) hi k hk} →
                              {F' : CategoryTheory.Functor (↑(Set.Iic j)) C} →
                                {obj_bot' : F'.obj ⟨⊥, ⋯⟩ = Φ.X₀} →
                                  {arrowSucc_eq' :
                                      ∀ (i : J) (hi : i < j),
                                        CategoryTheory.SmallObject.SuccStruct.arrowSucc F' i hi =
                                          Φ.toSuccArrow (F'.obj ⟨i, ⋯⟩)} →
                                    {arrowMap_limit' :
                                        ∀ (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j) (k : J) (hk : k < i),
                                          CategoryTheory.SmallObject.SuccStruct.arrowMap F' k i ⋯ hij =
                                            CategoryTheory.SmallObject.SuccStruct.arrowι
                                              (CategoryTheory.SmallObject.restrictionLT F' hij) hi k hk} →
                                      { F := F, obj_bot := obj_bot, arrowSucc_eq := arrowSucc_eq,
                                            arrowMap_limit := arrowMap_limit } =
                                          { F := F', obj_bot := obj_bot', arrowSucc_eq := arrowSucc_eq',
                                            arrowMap_limit := arrowMap_limit' } →
                                        (F ≍ F' → P) → P

Defined in

Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Cited by

1 results in Mathlib

Foundations

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