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.