Re: [HoTT] Equality in the Model Type Framework

[Matt Oliveri <atmacen@gmail.com>]

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

On Wednesday, July 4, 2018 at 12:50:03 AM UTC-4, Michael Shulman wrote:
>
> We are still working out the details.


I'm looking forward to more 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.


Basically; yeah.

In more detail, your approach seems to have three stages:
1) specify a mode theory
2) specify a theory in the resulting doctrine
3) use it

I figured the user could only add judgmental equalities in stage (2). The 
equations in stage (1) seem like something else (usually "WLOGed" away in 
the syntax), and the equations in stage (3) are typal equality.

I was guessing/hoping that the nice syntactic properties would only cover 
the type system corresponding to the doctrine, and not cover the additional 
constants and equations added in stage (2).

Dan already pointed out in his third Hausdorff talk that MLTT doesn't have 
the subformula property. So it sure looks like user-specified constants and 
equations at stage (2) rules that out. My impression was that you should 
not expect the subformula property in a theory with logical strength.

Arbitrary equations rules out normalization too, because they could add 
equality reflection. Although I don't recommend it, it should be possible 
to impose a restricted way of adding equations, so that the system remains 
normalizing. Justifying such a framework would be tricky without putting an 
upper bound on the proof-theoretic strength of the normalization 
metatheorem.

With equality reflection, the operational semantics and judgmental equality 
become separate. Computational type theory is a way of getting a lot of 
flexibility for equations while keeping canonicity. (Strong normalization 
is not available.) Judgmental equality of t and t' in type T means that 
computations t and t' implement the same element of T. But it seems like 
that would be a big detour for you.

Really though, I don't think the nice syntactic properties should be a 
concern when designing the *categorical* semantics of a full blown 
dependent type theory. That's why I was hoping they would only pertain to 
the bare doctrine.

this isn't 
> really a question about our modal DTT specifically but just more 
> generally about what a dependently typed "theory" is.
>

Wait a minute. Looking back at your "What Is an n-Theory?" post, you were 
thinking of things like HoTT and cubical type theory as doctrines. I don't 
understand how this fits with the modal type framework. A mode theory will 
not be enough to specify that kind of doctrine, will it? And if those are 
doctrines, why do theories also get judgmental equations? What are theories 
used for?

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