On Monday, July 2, 2018 at 11:38:47 PM UTC-4, Matt Oliveri wrote:

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.

Come to think of it, this last part probably isn't right. Internal implication-like connectives generally wouldn't work with modes and substructure the way rules should.
Still wondering about equality.

--
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.