Theorems · Definition · category theory

SheafOfModules.Hom.mk.noConfusion

{C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        {X Y : SheafOfModules R} →
          {P : Sort u_1} → {val val' : X.val ⟶ Y.val} → { val := val } = { val := val' } → (val ≍ val' → P) → P

Defined in

Mathlib.Algebra.Category.ModuleCat.Sheaf

Cited by

1 results in Mathlib

Foundations

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