Nope. Type Theory (like Matin Luff TT) describes Type Theory really well. And it is way more useful for software development than CT is. Tools like Coq, LEAN, A

Nope. Type Theory (like Matin Luff TT) describes Type Theory really well. And it is way more useful for software development than CT is. Tools like Coq, LEAN, Agda, Idris etc. are built on TT not CT.