English
There is a functor Set X ⥤ Type u which sends a subset S ⊆ X to the type S itself and sends a morphism f: S → T to the map (x,hx) ↦ (x, leOfHom f hx).
Русский
Существует функтор Set X ⥤ Type u, отправляющий подмножество S ⊆ X в сам тип S и отображение f: S → T в отображение (x,hx) ↦ (x, leOfHom f hx).
LaTeX
$$$\\mathrm{functorToTypes} : \\mathrm{Set}\,X \\;\\to\\; \\mathrm{Type}\,u\\quad\\text{с заданием }\\mathrm{obj}(S)=S,\\\\ \\mathrm{map}(f)(\\langle x, hx\\rangle)=\\langle x, \\mathrm{leOfHom}(f,hx)\\rangle.$$$
Lean4
/-- Given `X : Type u`, this the functor `Set X ⥤ Type u` which sends `A`
to its underlying type. -/
@[simps obj map]
def functorToTypes {X : Type u} : Set X ⥤ Type u where
obj S := S
map {S T} f := fun ⟨x, hx⟩ ↦ ⟨x, leOfHom f hx⟩
