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 is the functor Set X ⥤ Type u which sends A to its underlying type.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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