Theorems · Theorem · category theory

TopCat.Presheaf.toTypes_isSheaf

∀ (X : TopCat) (T : ↑X → Type u_1), (X.presheafToTypes T).IsSheaf

We show that the presheaf of functions to a type T (no continuity assumptions, just plain functions) form a sheaf. In fact, the proof is identical when we do this for dependent functions to a type family T, so we do the more general case.

Defined in

Mathlib.Topology.Sheaves.SheafOfFunctions

Cited by

1 results in Mathlib

Foundations

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