The Tao of Types
April 17, 2025 | Section: Notes
Simple Types Before exploring dependent types with all its beautiful complexities we’ll take a look at something simpler, appropriately named simple types, starting with the most fundamental type of all, the functon type $\_\to\_$. One issue with simple types is that it is not clear what to start with. We’ll generalize this with constructions which work for any type, called $\textsf{Set}$ in Agda. That is, we will use polymorphic constructions without introducing a formal account for polymorphism which we will do later once we have dependent types in our arsenal. Examples of polymorphic constructions are identity $\textsf{id}$ and composition $\_ \circ \_$ which give us a first taste of category theory.