Re: [HoTT] A small observation on cumulativity and the failure of initiality

[Thomas Streicher <stre...@mathematik.tu-darmstadt.de>]

It is certainly tempting to assign meanings to derivations and then to
show that different derivations of the same judgement get assigned the
same meaning.
When writing my thesis in the second half of the 80s I found this too
difficult and instead used an a priori partial interpretation
function assigning meaning to prejudgements. It was then part of the
correctness theorem that all derivable judgements get assigned a meaning.

Most people have gone this way at least when they took pains to write
down the interpretation function at all.

BTW the above allows one to show that assigning a meaning to derivations
just depends on the judgement: one jyust has to show that the meaning
assigned to a derivation of a judgement J coincides with the meaning
assigned to J beforehand.

Thomas