All Questions
1
question
11
votes
1
answer
292
views
Seven Trees in One, or How to formalize the Semiring of Types?
This is somewhat conceptual beginner's question about proof assistants.
I've been re-reading the famous Seven Trees in One / Objects of categories as complex numbers. The gist: The type $T$ of binary ...