Theorems · Definition · category theory

CategoryTheory.Functor.CommShift.mk.noConfusion

{C : Type u_1} →
  {D : Type u_2} →
    {inst : CategoryTheory.Category.{v_1, u_1} C} →
      {inst_1 : CategoryTheory.Category.{v_2, u_2} D} →
        {F : CategoryTheory.Functor C D} →
          {A : Type u_6} →
            {inst_2 : AddMonoid A} →
              {inst_3 : CategoryTheory.HasShift C A} →
                {inst_4 : CategoryTheory.HasShift D A} →
                  {P : Sort u} →
                    {commShiftIso :
                        (a : A) → (CategoryTheory.shiftFunctor C a).comp F ≅ F.comp (CategoryTheory.shiftFunctor D a)} →
                      {commShiftIso_zero :
                          autoParam (commShiftIso 0 = CategoryTheory.Functor.CommShift.isoZero F A)
                            CategoryTheory.Functor.CommShift.commShiftIso_zero._autoParam} →
                        {commShiftIso_add :
                            autoParam
                              (∀ (a b : A),
                                commShiftIso (a + b) =
                                  CategoryTheory.Functor.CommShift.isoAdd (commShiftIso a) (commShiftIso b))
                              CategoryTheory.Functor.CommShift.commShiftIso_add._autoParam} →
                          {commShiftIso' :
                              (a : A) →
                                (CategoryTheory.shiftFunctor C a).comp F ≅ F.comp (CategoryTheory.shiftFunctor D a)} →
                            {commShiftIso_zero' :
                                autoParam (commShiftIso' 0 = CategoryTheory.Functor.CommShift.isoZero F A)
                                  CategoryTheory.Functor.CommShift.commShiftIso_zero._autoParam} →
                              {commShiftIso_add' :
                                  autoParam
                                    (∀ (a b : A),
                                      commShiftIso' (a + b) =
                                        CategoryTheory.Functor.CommShift.isoAdd (commShiftIso' a) (commShiftIso' b))
                                    CategoryTheory.Functor.CommShift.commShiftIso_add._autoParam} →
                                { commShiftIso := commShiftIso, commShiftIso_zero := commShiftIso_zero,
                                      commShiftIso_add := commShiftIso_add } =
                                    { commShiftIso := commShiftIso', commShiftIso_zero := commShiftIso_zero',
                                      commShiftIso_add := commShiftIso_add' } →
                                  (commShiftIso ≍ commShiftIso' → P) → P

Defined in

Mathlib.CategoryTheory.Shift.CommShift

Cited by

0 results in Mathlib

Foundations

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