I watched all 5 videos a few years ago. And if I understand it correctly "Computational Type Theory" basically defines a type as describing the behaviour of a c

I watched all 5 videos a few years ago. And if I understand it correctly "Computational Type Theory" basically defines a type as describing the behaviour of a computation. Which is really interesting but kinda hard for me to wrap my arms around compared with Martin Loff type theory. It looks as if type checking will have to be done manual, using N axiomatic rules for how you can prove A from B. Is that your understanding as well? Also, there doesn't seem to be much material on Computational Type theory online. Any good references? (Except for the nuPrl book of course).