Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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.
I don’t immediately see anything that would make it nonconstructive.
In particular, I think all the definitions of the partial interpretations should be expressed in purely category-theoretic language in the presheaf category [Cop,Set], which is inherently constructive, especially because the internal logic of this category is not classical. Is there something that looks nonconstructive to you?
What exactly is TmV where V is a finite set?
The V-indexed power (for Set-enrichment) of the presheaf Tm.
Otherwise known as the product of V copies of Tm, or ∏VTm.
1 to 9 of 9