Theorems · Definition · category theory

CategoryTheory.Functor.WellOrderInductionData.Extension.noConfusionType

Sort u_1 →
  {J : Type u} →
    [inst : LinearOrder J] →
      [inst_1 : SuccOrder J] →
        {F : CategoryTheory.Functor Jᵒᵖ (Type v)} →
          {d : F.WellOrderInductionData} →
            [inst_2 : OrderBot J] →
              {val₀ : F.obj (Opposite.op ⊥)} →
                {j : J} →
                  d.Extension val₀ j →
                    {J' : Type u} →
                      [inst' : LinearOrder J'] →
                        [inst'_1 : SuccOrder J'] →
                          {F' : CategoryTheory.Functor J'ᵒᵖ (Type v)} →
                            {d' : F'.WellOrderInductionData} →
                              [inst'_2 : OrderBot J'] →
                                {val₀' : F'.obj (Opposite.op ⊥)} → {j' : J'} → d'.Extension val₀' j' → Sort u_1

Defined in

Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Cited by

0 results in Mathlib

Foundations

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

Assumes

LinearOrderSuccOrderOrderBotLinearOrderSuccOrderOrderBot