[HoTT] Equality in the Model Type Framework

[Matt Oliveri <atmacen@gmail.com>]

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

I saw Dan Licata's Hausdorf talks about the framework for modal type 
systems that he, Mike Shulman, and Mitchell Riley are working on.

As I understand it, a "mode theory" in this framework specifies a 
judgmental structure, and the bold F and U type constructors provide 
certain type constructors for each judgmental structure generically. The 
resulting type systems correspond to certain doctrines, and each system can 
be used to specify theories for structured categories of the corresponding 
doctrine.

Neat. Except... theories usually involve equality. What equality is this, 
on the type theory side? In the case of simple type systems, I guess it can 
only be judgmental equality. But what about with dependent type systems? 
What's the plan?

If dependently-typed theories could use judgmental equality in axioms, and 
if one universe (without type constructors) was added to the framework, it 
seems like each mode theory would yield a system analogous to Martin-Löf's 
logical framework (MLLF), so a full constructive type theory could be 
specified at the theory level. This sounds nice.

-- 
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: 1627 bytes --]