Theorems · Definition · category theory

CompHausLike.LocallyConstant.functorToPresheaves

{P : TopCat → Prop} →
  CategoryTheory.Functor (Type (max u w)) (CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w)))

The functor from the category of sets to presheaves on CompHausLike P given by locally constant maps.

Defined in

Mathlib.Condensed.Discrete.LocallyConstant

Cited by

11 results in Mathlib

Foundations

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