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

[Michael Shulman <shu...@sandiego.edu>]

I mean, it seems to me kind of like the difference between proving a
type A is contractible by

Sigma(a:A) Pi(x:A) (x=a)

and by

A x Pi(x y:A) (x=y)

i.e. not much.  But maybe I am missing something?

On Sun, Oct 15, 2017 at 7:53 AM, Michael Shulman <shu...@sandiego.edu> wrote:
> I'm not saying to do anything different mathematically, just to
> *think* about "using a partial interpretation function on prejudgments
> and showing that all derivable judgments get a meaning" as *being a
> way of* "assigning meanings to derivations and showing that distinct
> derivations of the same judgment get the same meaning".
>
> On Sun, Oct 15, 2017 at 6:57 AM, Thomas Streicher
> <stre...@mathematik.tu-darmstadt.de> wrote:
>>> > 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.
>>>
>>> Couldn't one consider the latter to be a way of doing the former?
>>
>> In principle yes but it is very laborious. First of all you have to
>> formalize derivations and do a double induction on them which I don't
>> know how to to perform.
>>
>> Thomas
>>
>> --
>> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
>> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
>> For more options, visit https://groups.google.com/d/optout.