# 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

added to pure type system in the Idea-section the statement

In other words a pure type system is

1. a system of natural deduction

2. with dependent types

3. and with the dependent product type formation rule.

and to the Related concepts-Section the paragraph

Adding to a pure type sytstem

1. rules for introduing inductive types

2. possibly a type of types hierarchy

makes it a calculus of inductive constructions.

Finally I added to the References-section a pointer to these slides

• CommentRowNumber2.
• CommentAuthorMike Shulman
• CommentTimeOct 5th 2012

I think CiC is a particular pure type system; your phrasing sounds like it is a class of them.

• CommentRowNumber3.
• CommentAuthorUrs
• CommentTimeOct 5th 2012

Okay.

Can you maybe help me understand what these 8 different pure type systems in the cube are? I don’t understand the notation when it comes to discussion of that.

• CommentRowNumber4.
• CommentAuthorMike Shulman
• CommentTimeOct 5th 2012

The notational names for those things like $\lambda_\to$ are ad hoc, I wouldn’t pay them too much mind.

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

What I don’t understand is what $(\ast,\Box)$ and $(\Box, \Box)$ and so on means.

• CommentRowNumber6.
• CommentAuthorMike Shulman
• CommentTimeOct 5th 2012

They’re specifying the relevant set $R$ of “relations” as described in the “Definition” section.

• CommentRowNumber7.
• CommentAuthorUrs
• CommentTimeOct 5th 2012
• (edited Oct 5th 2012)

Gee, I still don’t get it. Not only that I don’t understand the message, but I cannot even recognize a message.

Is “$\Box$” the name of some generic set? Could I write “$X$” instead of “$\Box$”? Why do we suddenly use geometric figures instead of variables? Is “$\ast$” also any set? It’s not meant to be singleton set?

Then: what does it mean to say that “$(*,\Box)$” is a relation? Which relation is this supposed to denote? On which set? And how am I supposed to think of it in words? Which role does that relation play?

Gee, I must be missing something really basic here. That feels weird.

• CommentRowNumber8.
• CommentAuthorUrs
• CommentTimeOct 5th 2012
• (edited Oct 5th 2012)

Ah, I am making progress. $S$ is the set with one or two or three elements, right?

There are a bunch of curly brackets missing in the entry, could that be?

• CommentRowNumber9.
• CommentAuthorMike Shulman
• CommentTimeOct 5th 2012

If putting curly brackets in would help, please do.

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

Okay, here I am, at past 2:00 in the morning, editing an entry that I couldn’t parse a minute ago. :-)

Right after where the triples appear, I am adding the folllowing remark. Give me a sanity check:

Remark. These relations will appear in the type formation rule for dependent product types below. They will say that for a type of sort $s_2$ depending on a type of sort $s_1$ its dependent product type has sort $s_3$.

• CommentRowNumber11.
• CommentAuthorUrs
• CommentTimeOct 5th 2012
• (edited Oct 5th 2012)

Does this here parse for you:

symbol actual value
$S =$ $\{\ast, \square\}$
$A =$ $\{(\ast : \square)\}$
$R =$ $\{(\ast, \ast), (\ast, \square), (\square, \ast), (\square, \square)\}$

?

I am now doing the other tables accordingly. Hope that’s right.

• CommentRowNumber12.
• CommentAuthorUrs
• CommentTimeOct 5th 2012
• (edited Oct 5th 2012)

Checking if I am following:

For the case of the PTS that is the CoC (the yes, yes, yes, yes-case :-) we have

• $\ast = Prop$

• $\Box = Type$

is that right?

• CommentRowNumber13.
• CommentAuthorMike Shulman
• CommentTimeOct 5th 2012

Yes, I think all of that is right. Sorry, I didn’t realize how opaque the previous entry was! Your added remark after the definition of the “relations” is I think greatly helpful (I fixed a typo).

• CommentRowNumber14.
• CommentAuthorUrs
• CommentTimeOct 5th 2012

Okay, thanks.

I have added a remark in a new subsection to make the special case of the CoC more explicit.

• CommentRowNumber15.
• CommentAuthorJonasFrey
• CommentTimeMay 1st 2015

Hi, I’ve been looking into pure type systems in the last week, and I also had a look on the nlab page. According to the nlab, a pure type system is a triple (S,A,R) of a set S of “sorts”, a set A of axioms, and a set R of “relations”.

However, I think the elements of R are called “rules”, not “relations” in the literature that I know. Is there a reason why they are called “relations” here or is it by mistake? If nobody objects I can change it.

• CommentRowNumber16.
• CommentAuthorMike Shulman
• CommentTimeAug 5th 2015

Belatedly: thanks Jonas!

I added to pure type system a remark that they can be augmented with a cumulativity relation between sorts, and a reference.

Anonymous

• CommentRowNumber18.
• CommentAuthoratmacen
• CommentTimeApr 9th 2019

Changing the metavariable names in the idea section to use $b:B$ rather than $B:C$. The latter isn’t following any convention I’ve seen.