The functor from Set X to types

Given X : Type u, we define the functor Set.functorToTypes : Set X ⥤ Type u which sends A : Set X to its underlying type.

def Set.functorToTypes {X : Type u} : CategoryTheory.Functor (Set X) (Type u)

Given X : Type u, this the functor Set X ⥤ Type u which sends A to its underlying type.

Equations

• Set.functorToTypes = { obj := fun (S : Set X) => ↑S, map := fun {S T : Set X} (f : S ⟶ T) (x : ↑S) => match x with | ⟨x, hx⟩ => ⟨x, ⋯⟩, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem Set.functorToTypes_map {X : Type u} {S T : Set X} (f : S ⟶ T) (x✝ : ↑S) : functorToTypes.map f x✝ = match x✝ with | ⟨x, hx⟩ => ⟨x, ⋯⟩

@[simp]

theorem Set.functorToTypes_obj {X : Type u} (S : Set X) : functorToTypes.obj S = ↑S