I am learning the typed lambda-calculus and looking into the Calculus of Constructions. It was going well until I was slapped in the face with variations, and now I'm confused about the layout of all the different versions. As far as I can tell, the versions of basic CoC include theories with:
- Abstraction and conversion similar to pure type systems.
- Modified abstraction rule.
- Relaxed conversion rule.
- Modified abstraction rule and relaxed conversion rule.
On top of this, it seems that on top of each variation can be built a more general theory of the sort (Predicative, Extended) Calculus of (Inductive, Coinductive) Constructions (with Rewriting, with eta-reduction), where you are free to pick your choice/exclusion of parentheses. I don't know exactly which combinations are allowed, however.
Can anyone give meaning to these variations, and how I can think about them in relation to each other?