Theorems · Theorem · category theory

CategoryTheory.equivYoneda_hom_app_hom_apply_hom_apply

∀ (S : CategoryTheory.Functor Type uᵒᵖ (Type u))
  (hs : CategoryTheory.Presheaf.IsSheaf CategoryTheory.typesGrothendieckTopology S) (X : Type uᵒᵖ)
  (x : S.obj (Opposite.op (Opposite.unop X))) (x_1 : Opposite.unop X),
  (CategoryTheory.ConcreteCategory.hom
        ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.equivYoneda S hs).hom.app X)) x))
      x_1 =
    (CategoryTheory.ConcreteCategory.hom (S.map (TypeCat.ofHom fun x => x_1).op)) x

Defined in

Mathlib.CategoryTheory.Sites.Types

Cited by

0 results in Mathlib

Foundations

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