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

[Andrew Polonsky <andrew....@gmail.com>]

[-- Attachment #1.1: Type: text/plain, Size: 1068 bytes --]


>
> Equalities in the set theoretic translation of Type Theory are accidents 
> of implementation choices. Making them the guideline for the design of Type 
> Theory seems to to put the cart in front of the horse.
>

No.

The fact that equalities corresponding to beta reduction, etc. are 
validated is not "an accident of implementation choices".

It is a consequences of the fact that standard type constructors (function 
space, products, ...) are interpreted by their native meaning in the 
meta-level.

For example, if the metatheory is again type theory, and interpretation is 
done by recursion over the universes of object types, reifying all type 
constructors by themselves (like in an inductive-recursive universe), then 
all conversions in the object language will again be valid in the 
metatheory, and coherence issues won't arise.

I suspect that (sufficiently split) categorical models could also be 
presented this way, but it might be less natural because equality of types 
would then have to refer to (actual) equality of objects.

Cheers,
Andrew

[-- Attachment #1.2: Type: text/html, Size: 1483 bytes --]