Theorems · Definition · category theory

CategoryTheory.Localization.SmallHom

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (W : CategoryTheory.MorphismProperty C) →
      (X Y : C) → [CategoryTheory.Localization.HasSmallLocalizedHom W X Y] → Type w

The type of morphisms from X to Y in the localized category with respect to W : MorphismProperty C that is shrunk to Type w when HasSmallLocalizedHom.{w} W X Y holds.

Defined in

Mathlib.CategoryTheory.Localization.SmallHom

Cited by

24 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Localization.HasSmallLocalizedHom