Open invitation: If you are learning Agda or Martin-Löf type theory and wish to talk about it or related matters, contact me and I will try to help to the best of my ability.
5
13
79
Conversation
Do you know of any formulations of a typed lambda-I calculus (lambda calculus with no vacuous binding allowed) in Agda?
4
What do you mean by “vacuous binding”?
1
1
This Tweet is from a suspended account. Learn more
Ahh cool!
1
Yeah QTT does seem uhhh ‘relevant’ here 😁