Hmm, that’s interesting. I wasn’t aware that Set was considered part of CiC but not CoC.

]]>I was just remembering that in CiC we must stratify Type to maintain

consistency. Usually, universes or sorts of PTS are not stratified at least by

the original definition of what a PTS is in general. So this is another

difference. Just to summarize the major difference between CoC and

CiC are inductive types, an additional impredicative universe Set, and

the stratification of Type. ]]>

at the actual entry. It is correct and sorry about that.

As for your question. Mike is correct we should pin down the terminology in order to be

precise. CoC is a particular PTS with two sorts and the complete set of rules for these

two sorts. It is the strongest among the eight systems of the lambda-cube.

There is no difference between CoC and the PTS defining CoC. If by difference we

mean expressibility -- which is itself understood as provability. Now as for CiC which

as you know is the extension of CoC with inductive types and and an impredicative

universe Set in addition to Type and Prop. As of Coq 8 it is based on predicative CiC.

Now if we only remove the inductive types from CiC then we obtain CoC with Set which

is still a PTS. It is however outside the lambda-cube. PTS' may have any number

of universes as long as they are impredicative.

I hope this helps. ]]>

PTS refers to a *class of type theories*, not to any particular one. CoC can be presented as *a* PTS.

@heades in #13,

could you say more concretely what’s wrong with the entry, if anything? Where it gives that numberd item list it does refer to CiC and “with inductive types”. That seems to agree with your #13!?

I also have a general question: what is the difference between CoC and PTS? It seems to me that if I remove from CiC the inductive types I am left with just PTS. Well, and universes. Is that the difference?

]]>Yes, probably. (-:

]]>Let’s not proliferate terminology! “The CoC” is a particular type theory, with impredicative quantification. “The predicative CoC” is another one, as

is “the predicative CoiC” — the latter is roughly the one that Coq is based on. We already have general notions like “a pure type system” and

“a type theory” and “a dependent type theory” — I don’t see any need for a general notion of “a calculus of constructions”.

I think that there is more to say about CoC. Coquand's original definition was not as a pure type system. This was pointed out later. Not to mention

that CoC can also be viewed as a extension of system F-omega. Just some points that might be useful notes. ]]>

CoC is a particular pure type system which did not originally have inductive or co-inductive types.

CiC was the extension of CoC with (co)-inductive types.

ECC is the the Extended Calculus of Constructions. Coq is based on ECC. ]]>

Absolutely! (-:

Also, concerning type checking with universes, we should mention Gérard Huet’s *Extending the Calculus of Constructions with Type:Type*, which is an unpublished manuscript from 1987 that’s often referred to. But I haven’t seen it.

Where “easier” means “easier for the formal theory of the type system, but much more tedious for the actual user”. (-:

]]>Cumulativity means that $A:Type_i$ implies $A:Type_{i+1}$ (so $Type_i$ is a *subtype* of $Type_{i+1}$). In Agda, you have to use an explicit raise operator $Type_i\to Type_{i+1}$. It’s much easier not to worry about subtyping rules. With subtyping, you have to work a bit to get *principal types*. I think that was first worked out in Luo’s PhD thesis, An Extended Calculus of Constructions, and in Harper and Pollack’s Type Checking with Universes. However, I’m not an expert here, so perhaps Mike can ask someone at IAS about the precise history.

What’s the technical definition of “cumulative hierarchy”. Can a hierarchy of universes not be cumulative?

]]>@Ulrik, that’s sure a good point about “predicative CoC” including impredicative Prop! Maybe it would be better called “semipredicative”.

I don’t think I’ve heard anyone call the type theory underlying Agda anything but “the type theory underlying Agda”. (-:

]]>I agree with Mike about not proliferating terminology.

I know the Coq manual refers to the “predicative calculus of constructions” (with one impredicative sort, Prop) to distinguish it from the “impredicative calculus of constructions” (with two impredicative sorts, Prop and Set). However, I think I’m not the only one who finds that terminology confusing!

What do we then call the base of Agda? (I know, that’s a moving target!) – Last I checked, Agda had a non-cumulative hierarchy of predicative universes, and type of universe levels, rather fancy indexed induction-recursion and induction-induction, and a monadic(?) way of treating coinduction with operators ♯ and♭.

]]>Let’s not proliferate terminology! “The CoC” is a particular type theory, with impredicative quantification. “The predicative CoC” is another one, as is “the predicative CoiC” — the latter is roughly the one that Coq is based on. We already have general notions like “a pure type system” and “a type theory” and “a dependent type theory” — I don’t see any need for a general notion of “a calculus of constructions”.

]]>Okay, thanks.

I gather that one of the four (or so) “teams” at the IAS HoTT program is concerned with doing something like re-writing Coq to make it homotopy-native.

I assume that in the course of doing so, they will re-examine these notions. I assume they will come up with a ** Calculus of homotopy-inductive Constructions**, which

refines inductive types to higher inductive types;

drops the Prop-universe.

Maybe in the near future there’ll be some preliminary notes on this, and then maybe I’ll be allowed to point to it as “another CoC” without Prop-universe :-)

]]>Great.

But: can’t we allow ourselves not to demand the Prop-universe and still speak of a “calculus of constructions”?

Quite possibly when you say *a* CoC as opposed to *the* CoC! But I’m not sure how I’d define *a* CoC. I think the version with only predicative universes goes by the name of predicative type theory, but that’s also not quite a definite phrase.

Thanks! (On both accounts.)

I have changed it now as suggested in the entry.

But: can’t we allow ourselves *not* to demand the Prop-universe and still speak of a “calculus of constructions”?

Number 4 should be more precise: An impredicative universe (type of types), Prop, and a cumulative hierarchy of predicative universes (types of types), Type$_i$, on top of Prop.

Otherwise it looks fine!

]]>I have added the following paragraph to *calculus of constructions*, I’d be grateful if experts could briefly give me a sanity check that this is an accurate characterization:

]]>More in detail, the

Calculus of (co)Inductive Constructionsis

a system of natural deduction with dependent types;

with the natural-deduction rules for dependent product types specified;

and with a rule for how to introduce new such natural-deduction rules for arbitrary (co)inductive types.

and with a type of types (hierarchy).