Hask (Category)

$\mathbf{Hask}$ is the category of haskell types and (total) functions). Note that $\mathbf{Hask}$ is not a real category becuase:

1. It is lazy.
2. It is not total.

Agda (Categoory)

This is closely related to the ‘category’ $\mathbf{Agda}$.

1. Agda uses intensional equality rather than extensional equality.