Re: [HoTT] Equality in the Model Type Framework

[Michael Shulman <shulman@sandiego.edu>]

We are still working out the details.  Semantically, I would certainly
expect a "theory" in a DTT to be allowed to assert judgmental
equalities.  But such theories might be poorly behaved syntactically:
allowing the "user" to add judgmental equalities in a DTT tends to
break lots of nice type-theoretic properties.  I could be wrong
though, perhaps someone more knowlegeable could say more -- this isn't
really a question about our modal DTT specifically but just more
generally about what a dependently typed "theory" is.

On Mon, Jul 2, 2018 at 8:38 PM, Matt Oliveri <atmacen@gmail.com> wrote:
> 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.

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