@chrisamaphone@hci.social Btw, my take on this -- and on the original case -- is just that it's a human question of what concepts we can wrap our heads around despite being formally incredibly complicated. Obviously that varies by person and by experience, but I actually worry that formalization allows us to get too far ahead of our skis sometimes. I also *do* think dependent type theory is very complicated, although I also think there are many principles at work that compress it considerably. And for what it's worth, inductive schemas and pattern matching scare me most of all! I was just asking Mario and @mevenlennonbertrand@lipn.info about them last week...