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.