Re: [HoTT] Equality in the Model Type Framework

[Matt Oliveri <atmacen@gmail.com>]

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

On Thursday, July 5, 2018 at 12:00:25 AM UTC-4, Michael Shulman wrote:
>
> So the things that a theory is "allowed to do" are a 
> subset of the things a doctrine is "allowed to do", but what gets 
> excluded is the "stuff" at the categorical top dimension, not the 
> "properties" (equations) at the categorical bottom dimension.
>

So on the syntactic side, this is saying that theories can't add constants 
or equations to the mode theory? (Like flat and idempotence of flat.)

I believe intensional MLTT, at least, should be described by the 
> "tautological" or "simplest possible" mode theory with just one 
> comprehension-category mode and enough of the relevant F- and U-types, 
> including "indexed F-types" that specialize to Id-types.


Would this support W types in the doctrine? Universes? Do universes somehow 
pop up out of the new U types, or are they special?

-- 
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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

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