Just a random thought, but one of the nice things about category theory is that you stop thinking about objects and start thinking about morphisms. Are there any type theories designed with this concept at the very forefront?
Conversation
Possibly a related question, and possibly not: are there type theories that view equalities and other relations as sort of the primitive building blocks of the type theory, and let types fall out of them, rather than sort of building them out of types?
3
1
15
Replying to
Isn’t this one of those Curry vs Church things? I always forget which is which 😂
I'm thinking that Makam seemed rather like 'building up stuff using open relations', and I think it was inspired by λProlog and Twelf? Not sure if those are similar at all to what you are interested in, although I'm guessing you might already familiar with those 😅
2