@carloangiuli@mathstodon.xyz @mevenlennonbertrand@lipn.info i think type theory in the "full generality" we try to base many proof assistants on today is very complicated. i am not sure that that generality is always necessary for many common uses of the tools, and i'm interested in finding de-generalizations we can surface for those uses