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

Site Tag Cloud

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

• CommentRowNumber1.
• CommentAuthorMike Shulman
• CommentTimeOct 28th 2018

Created, mainly with stuff from the overview.

• CommentRowNumber2.
• CommentAuthorMike Shulman
• CommentTimeOct 28th 2018

• CommentRowNumber3.
• CommentAuthorMike Shulman
• CommentTimeOct 28th 2018

• CommentRowNumber4.
• CommentAuthordlicata335
• CommentTimeNov 1st 2018

To what extent is this proof of initiality intended to be constructive? I think that has some bearing on how the partial interpretations are treated. I think it should be possible to prove initiality in a constructive metalanguage, but maybe some shortcuts helpful for the intended audience are possible classically.

• CommentRowNumber5.
• CommentAuthorMike Shulman
• CommentTimeNov 1st 2018

I don’t immediately see anything that would make it nonconstructive.

• CommentRowNumber6.
• CommentAuthorMike Shulman
• CommentTimeNov 1st 2018

In particular, I think all the definitions of the partial interpretations should be expressed in purely category-theoretic language in the presheaf category $[C^{op},Set]$, which is inherently constructive, especially because the internal logic of this category is not classical. Is there something that looks nonconstructive to you?

• CommentRowNumber7.
• CommentAuthorAlizter
• CommentTimeNov 8th 2018

What exactly is $\Tm^{V}$ where $V$ is a finite set?

• CommentRowNumber8.
• CommentAuthorMike Shulman
• CommentTimeNov 8th 2018

The $V$-indexed power (for $Set$-enrichment) of the presheaf $Tm$.

• CommentRowNumber9.
• CommentAuthorMike Shulman
• CommentTimeNov 8th 2018

Otherwise known as the product of $V$ copies of $Tm$, or $\prod_{V} Tm$.