[HoTT] Equality in the Model Type Framework

[HoTT] Equality in the Model Type Framework

[Matt Oliveri]

[-- 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 --]

[HoTT] Re: Equality in the Model Type Framework

[Matt Oliveri]

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

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.

[-- Attachment #1.2: Type: text/html, Size: 1298 bytes --]

Re: [HoTT] Equality in the Model Type Framework

[Michael Shulman]

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.

Re: [HoTT] Equality in the Model Type Framework

[Matt Oliveri]

[-- 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 --]

Re: [HoTT] Equality in the Model Type Framework

[Michael Shulman]

On Wed, Jul 4, 2018 at 11:11 AM, Matt Oliveri <atmacen@gmail.com> wrote:
> 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.

Right.  I would figure that nice syntactic properties usually only
apply to the initial/empty theory in a given doctrine, or perhaps more
generally to "free theories" i.e. without added judgmental equations.

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

Roughly speaking, a doctrine specifies the "kinds of types" available
and how they relate (the judgmental structure), the operations
available on such types (type formers), the structure possessed by
these operations (term formers, intro/elim/etc.), and the laws
satisfied by that structure (computation beta/eta rules).  A theory in
that doctrine asserts the existence of particular types (you could
call them "nullary type formers"), structure possessed by types
(perhaps the particular ones you added, or perhaps ones constructed
using the doctrine operations), and axioms satisfied by that
structure.  So the things that a theory is "allowed to do" are a
subset of the things a doctrine is "allowed to do", but what gets
excluded is the "stuff" at the categorical top dimension, not the
"properties" (equations) at the categorical bottom dimension.  A
theory has to have equations (consider the theory of groups, for
instance, which has axioms for associativity and so on).

Our mode theories do not purport to describe *all* possible doctrines,
only a particularly simple and well-behaved class of them.  That said,
I believe intensional MLTT, at least, should be described by the
"tautological" or "simplest possible" mode theory with just one
comprehension-category mode and enough of the relevant F- and U-types,
including "indexed F-types" that specialize to Id-types.  Axioms like
funext and univalence could then be added in a particular theory.  The
judgmental/dependency structure of cubical TT should also be
describable by a suitably flexible version of our mode theories
(although we might not include that much generality in our first paper
on dependent modal type theory), with one mode for interval variables,
another dependent on it for face formulas, and a third
comprehension-category mode dependent on them for types.  The rest of
cubical TT is special, though.

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

Re: [HoTT] Equality in the Model Type Framework

[Matt Oliveri]

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

On Thursday, July 5, 2018 at 12:00:25 AM UTC-4, Michael Shulman wrote:
>
> So the things that a theory is "allowed to do" are a 
> subset of the things a doctrine is "allowed to do", but what gets 
> excluded is the "stuff" at the categorical top dimension, not the 
> "properties" (equations) at the categorical bottom dimension.
>

So on the syntactic side, this is saying that theories can't add constants 
or equations to the mode theory? (Like flat and idempotence of flat.)

I believe intensional MLTT, at least, should be described by the 
> "tautological" or "simplest possible" mode theory with just one 
> comprehension-category mode and enough of the relevant F- and U-types, 
> including "indexed F-types" that specialize to Id-types.


Would this support W types in the doctrine? Universes? Do universes somehow 
pop up out of the new U types, or are they special?

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

Re: [HoTT] Equality in the Model Type Framework

[Michael Shulman]

On Wed, Jul 4, 2018 at 10:59 PM, Matt Oliveri <atmacen@gmail.com> wrote:
> So on the syntactic side, this is saying that theories can't add constants
> or equations to the mode theory? (Like flat and idempotence of flat.)

Yes.

> Would this support W types in the doctrine?

It's possible that there is a notion of "recursive F-type" that would
include W-types, but we haven't really worked that out yet.

> Universes? Do universes somehow
> pop up out of the new U types, or are they special?

I think universes are special.  In particular, they don't have a
universal property.

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