please don't ask me what a type is. i don't know how to explain and it's my number 1 source of impostor syndrome basically
Conversation
It’s kinda a hard question to answer because “what is” is a question about semantics and “a type” is a purely syntactic thing!
1
2
7
*nods* any answer that you give is either reductive or tautological
2
3
but it sucks because if you try to introduce someone to the ideas most common in type theory invariably the first question they hit you with is "what is a type"
and your options are either put your biases on full display or give them a non answer and hope they stick around
3
4
"what is art?"
was one of the first things we got into at art school and yeah it's pretty fun and hard to answer in a very satisfactory way