* [HoTT] Equality in the Model Type Framework @ 2018-07-03 3:38 Matt Oliveri 2018-07-03 16:17 ` [HoTT] " Matt Oliveri 2018-07-04 4:49 ` [HoTT] " Michael Shulman 0 siblings, 2 replies; 7+ messages in thread From: Matt Oliveri @ 2018-07-03 3:38 UTC (permalink / raw) To: Homotopy Type Theory [-- 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 --] ^ permalink raw reply [flat|nested] 7+ messages in thread
* [HoTT] Re: Equality in the Model Type Framework 2018-07-03 3:38 [HoTT] Equality in the Model Type Framework Matt Oliveri @ 2018-07-03 16:17 ` Matt Oliveri 2018-07-04 4:49 ` [HoTT] " Michael Shulman 1 sibling, 0 replies; 7+ messages in thread From: Matt Oliveri @ 2018-07-03 16:17 UTC (permalink / raw) To: Homotopy Type Theory [-- 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 --] ^ permalink raw reply [flat|nested] 7+ messages in thread
* Re: [HoTT] Equality in the Model Type Framework 2018-07-03 3:38 [HoTT] Equality in the Model Type Framework Matt Oliveri 2018-07-03 16:17 ` [HoTT] " Matt Oliveri @ 2018-07-04 4:49 ` Michael Shulman 2018-07-04 18:11 ` Matt Oliveri 1 sibling, 1 reply; 7+ messages in thread From: Michael Shulman @ 2018-07-04 4:49 UTC (permalink / raw) To: Matt Oliveri; +Cc: Homotopy Type Theory 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. ^ permalink raw reply [flat|nested] 7+ messages in thread
* Re: [HoTT] Equality in the Model Type Framework 2018-07-04 4:49 ` [HoTT] " Michael Shulman @ 2018-07-04 18:11 ` Matt Oliveri 2018-07-05 4:00 ` Michael Shulman 0 siblings, 1 reply; 7+ messages in thread From: Matt Oliveri @ 2018-07-04 18:11 UTC (permalink / raw) To: Homotopy Type Theory [-- 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 --] ^ permalink raw reply [flat|nested] 7+ messages in thread
* Re: [HoTT] Equality in the Model Type Framework 2018-07-04 18:11 ` Matt Oliveri @ 2018-07-05 4:00 ` Michael Shulman 2018-07-05 5:59 ` Matt Oliveri 0 siblings, 1 reply; 7+ messages in thread From: Michael Shulman @ 2018-07-05 4:00 UTC (permalink / raw) To: Matt Oliveri; +Cc: Homotopy Type Theory 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. ^ permalink raw reply [flat|nested] 7+ messages in thread
* Re: [HoTT] Equality in the Model Type Framework 2018-07-05 4:00 ` Michael Shulman @ 2018-07-05 5:59 ` Matt Oliveri 2018-07-05 14:31 ` Michael Shulman 0 siblings, 1 reply; 7+ messages in thread From: Matt Oliveri @ 2018-07-05 5:59 UTC (permalink / raw) To: Homotopy Type Theory [-- 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 --] ^ permalink raw reply [flat|nested] 7+ messages in thread
* Re: [HoTT] Equality in the Model Type Framework 2018-07-05 5:59 ` Matt Oliveri @ 2018-07-05 14:31 ` Michael Shulman 0 siblings, 0 replies; 7+ messages in thread From: Michael Shulman @ 2018-07-05 14:31 UTC (permalink / raw) To: Matt Oliveri; +Cc: Homotopy Type Theory 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. ^ permalink raw reply [flat|nested] 7+ messages in thread
end of thread, other threads:[~2018-07-05 14:32 UTC | newest] Thread overview: 7+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2018-07-03 3:38 [HoTT] Equality in the Model Type Framework Matt Oliveri 2018-07-03 16:17 ` [HoTT] " Matt Oliveri 2018-07-04 4:49 ` [HoTT] " Michael Shulman 2018-07-04 18:11 ` Matt Oliveri 2018-07-05 4:00 ` Michael Shulman 2018-07-05 5:59 ` Matt Oliveri 2018-07-05 14:31 ` Michael Shulman
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for NNTP newsgroup(s).