3.5. The category of types🔗

If u is a universe, Type u (which is the type of types in the universe u) is a category: we may call it the category of types. In set-theoretical foundations, this would be called "the category of sets".

If f : X ⟶ Y is a morphism in the category of types, one may evaluate it at x : X:

If X and Y are types, the type of morphisms X ⟶ Y in the category of types is not definitionally equal to the type X → Y of functions from X to Y. In order to define a morphism, we use a constructor that we access using the notation ↾ (typed as \uprightharpoon). The map x ↦ x ^ 2 from ℕ to ℕ, as a morphism in the category of types, can be defined as: