# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorUrs
• CommentTimeOct 4th 2012
• (edited Oct 4th 2012)

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 Constructions is

1. a system of natural deduction with dependent types;

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

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

4. and with a type of types (hierarchy).

• CommentRowNumber2.
• CommentAuthorUlrik
• CommentTimeOct 4th 2012

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!

• CommentRowNumber3.
• CommentAuthorUrs
• CommentTimeOct 4th 2012
• (edited Oct 4th 2012)

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”?

• CommentRowNumber4.
• CommentAuthorUlrik
• CommentTimeOct 4th 2012

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.

• CommentRowNumber5.
• CommentAuthorUrs
• CommentTimeOct 4th 2012
• (edited Oct 4th 2012)

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

1. refines inductive types to higher inductive types;

2. 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 :-)

• CommentRowNumber6.
• CommentAuthorMike Shulman
• CommentTimeOct 5th 2012

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”.

• CommentRowNumber7.
• CommentAuthorUlrik
• CommentTimeOct 5th 2012

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♭.

• CommentRowNumber8.
• CommentAuthorMike Shulman
• CommentTimeOct 5th 2012

@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”. (-:

• CommentRowNumber9.
• CommentAuthorUrs
• CommentTimeOct 5th 2012

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

• CommentRowNumber10.
• CommentAuthorUlrik
• CommentTimeOct 5th 2012
• (edited Oct 5th 2012)

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.

• CommentRowNumber11.
• CommentAuthorMike Shulman
• CommentTimeOct 5th 2012

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

• CommentRowNumber12.
• CommentAuthorUlrik
• CommentTimeOct 5th 2012

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.

• CommentRowNumber13.
• CommentTimeOct 6th 2012
I don't think number three above is quite right.

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.
• CommentRowNumber14.
• CommentTimeOct 6th 2012
Mike you were saying:

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.
• CommentRowNumber15.
• CommentTimeOct 6th 2012
In response to my previous response. I may have misunderstood what you meant by "general notion."
• CommentRowNumber16.
• CommentAuthorMike Shulman
• CommentTimeOct 6th 2012

Yes, probably. (-:

• CommentRowNumber17.
• CommentAuthorUrs
• CommentTimeOct 6th 2012
• (edited Oct 6th 2012)

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?

• CommentRowNumber18.
• CommentAuthorMike Shulman
• CommentTimeOct 6th 2012

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

• CommentRowNumber19.
• CommentTimeOct 6th 2012
Urs, Sorry, you are right. I miss read the first post of this discussion and I didn't look
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.
• CommentRowNumber20.
• CommentTimeOct 6th 2012
One small last remark. I wasn't being all that precise in my last paragraph.

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.
• CommentRowNumber21.
• CommentAuthorMike Shulman
• CommentTimeOct 6th 2012

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