Theorems · Definition · category theory

PresheafOfModules.noConfusion

{P : Sort u_1} →
  {C : Type u₁} →
    {inst : CategoryTheory.Category.{v₁, u₁} C} →
      {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
        {t : PresheafOfModules R} →
          {C' : Type u₁} →
            {inst' : CategoryTheory.Category.{v₁, u₁} C'} →
              {R' : CategoryTheory.Functor C'ᵒᵖ RingCat} →
                {t' : PresheafOfModules R'} →
                  C = C' → inst ≍ inst' → R ≍ R' → t ≍ t' → PresheafOfModules.noConfusionType P t t'

Defined in

Mathlib.Algebra.Category.ModuleCat.Presheaf

Cited by

0 results in Mathlib

Foundations

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