Let's talk about ✨function types✨. If A and B are types, we can form the type A -> B of functions with domain A and codomain B.
Unlike in ZF, functions in type theory are a primitive notion, not defined as functional relations. Everything in type theory has like, 1/
Conversation
Replying to
Thanks for the thread! I appreciate the links to category theory! I really struggle with it, so it's incredibly helpful to learn how you see this stuff, and how to link it to the type theory!