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 $[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?
What exactly is $\Tm^{V}$ 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 $\prod_{V} Tm$.
1 to 9 of 9