I idly wonder why you used the scarey quotes in "algebraic" data types?

@KonstantinSolomatov, did you end up finding "Inductively defined types" online? If you hit this problem, you can often ask for a draft from one of the authors.

The only thing I've seen is Unison unisonweb.org/2017-10-13/scala-world.html

I wonder if the futurama projections technique could be used to speed up the interpreter, effectively ending up with a compiler?

Thanks for answering! I'm glad I asked otherwise I would have gotten the idea that CoC was better than M-L's ITT. I have roughly followed all the advice given in the answer you mention -- but I could do much better at understanding it all :). UTT is Luo's UTT. I'm pretty sure it stands for Unified Type Theory. The reference is always his book "Computation and Reasoning". I've been wondering whether to buy that one...

I'm trying to get my head around type theory. I'm wondering, given CoC is better than M-L's ITT, is it necessary to go back to understand M-L's work at all? i.e. can I get a good grasp of type theory by understanding merely CoC? Where does UTT fit into this? Idris uses something like UTT and I think Agda does too.

A pdf version of the paper mentioned by @cody: cs.ru.nl/~herman/PUBS/CC_CHiso.pdf

and yet free objects are, in a sense, generated from the axioms. Free theorems are generated (as you say "follow automatically") from the type signature.