* cubical type theory with UIP @ 2017-07-23 22:54 Michael Shulman 2017-07-29 1:47 ` Matt Oliveri 2017-08-02 9:40 ` [HoTT] " Andrea Vezzosi 0 siblings, 2 replies; 20+ messages in thread From: Michael Shulman @ 2017-07-23 22:54 UTC (permalink / raw) To: HomotopyT...@googlegroups.com I am wondering about versions of cubical type theory with UIP. The motivation would be to have a type theory with canonicity for 1-categorical semantics that can prove both function extensionality and propositional univalence. (I am aware of Observational Type Theory, which I believe has UIP and proves function extensionality, but I don't think it proves propositional univalence -- although I would be happy to be wrong about that.) Presumably we obtain a cubical type theory that's compatible with axiomatic UIP if in CCHM cubical type theory we postulate only a single universe of propositions. But I wonder about some possible refinements, such as: 1. In this case do we still need *all* the Kan composition and gluing operations? If all types are hsets then it seems like it ought to be unnecessary to have these operations at all higher dimensions. 2. Can it be enhanced to make UIP provable, such as by adding a computing K eliminator? Mike ^ permalink raw reply [flat|nested] 20+ messages in thread
* Re: cubical type theory with UIP 2017-07-23 22:54 cubical type theory with UIP Michael Shulman @ 2017-07-29 1:47 ` Matt Oliveri 2017-07-29 2:25 ` [HoTT] " Jon Sterling 2017-07-29 6:19 ` Michael Shulman 2017-08-02 9:40 ` [HoTT] " Andrea Vezzosi 1 sibling, 2 replies; 20+ messages in thread From: Matt Oliveri @ 2017-07-29 1:47 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 1303 bytes --] I'm confused. So you want a cubical type theory with only hsets? In what sense would there be cubes, other than just points? I thoght OTT had propositional extensionality. Though maybe that's only for strict props. On Sunday, July 23, 2017 at 6:54:39 PM UTC-4, Michael Shulman wrote: > > I am wondering about versions of cubical type theory with UIP. The > motivation would be to have a type theory with canonicity for > 1-categorical semantics that can prove both function extensionality > and propositional univalence. (I am aware of Observational Type > Theory, which I believe has UIP and proves function extensionality, > but I don't think it proves propositional univalence -- although I > would be happy to be wrong about that.) > > Presumably we obtain a cubical type theory that's compatible with > axiomatic UIP if in CCHM cubical type theory we postulate only a > single universe of propositions. But I wonder about some possible > refinements, such as: > > 1. In this case do we still need *all* the Kan composition and gluing > operations? If all types are hsets then it seems like it ought to be > unnecessary to have these operations at all higher dimensions. > > 2. Can it be enhanced to make UIP provable, such as by adding a > computing K eliminator? > > Mike > [-- Attachment #1.2: Type: text/html, Size: 1521 bytes --] ^ permalink raw reply [flat|nested] 20+ messages in thread
* Re: [HoTT] Re: cubical type theory with UIP 2017-07-29 1:47 ` Matt Oliveri @ 2017-07-29 2:25 ` Jon Sterling 2017-07-29 7:29 ` Matt Oliveri 2017-07-29 6:19 ` Michael Shulman 1 sibling, 1 reply; 20+ messages in thread From: Jon Sterling @ 2017-07-29 2:25 UTC (permalink / raw) To: HomotopyTypeTheory On Fri, Jul 28, 2017, at 06:47 PM, Matt Oliveri wrote: > I'm confused. So you want a cubical type theory with only hsets? In what > sense would there be cubes, other than just points? I thoght OTT had > propositional extensionality. Though maybe that's only for strict props. I think 'propositional extensionality' in OTT was for objects which were propositions *by definition*, as opposed to h-props in HoTT (which is something that you prove about a type, and doesn't merely follow from the intension of the type). Best, Jon > > On Sunday, July 23, 2017 at 6:54:39 PM UTC-4, Michael Shulman wrote: > > > > I am wondering about versions of cubical type theory with UIP. The > > motivation would be to have a type theory with canonicity for > > 1-categorical semantics that can prove both function extensionality > > and propositional univalence. (I am aware of Observational Type > > Theory, which I believe has UIP and proves function extensionality, > > but I don't think it proves propositional univalence -- although I > > would be happy to be wrong about that.) > > > > Presumably we obtain a cubical type theory that's compatible with > > axiomatic UIP if in CCHM cubical type theory we postulate only a > > single universe of propositions. But I wonder about some possible > > refinements, such as: > > > > 1. In this case do we still need *all* the Kan composition and gluing > > operations? If all types are hsets then it seems like it ought to be > > unnecessary to have these operations at all higher dimensions. > > > > 2. Can it be enhanced to make UIP provable, such as by adding a > > computing K eliminator? > > > > Mike > > > > -- > 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 HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. ^ permalink raw reply [flat|nested] 20+ messages in thread
* Re: [HoTT] Re: cubical type theory with UIP 2017-07-29 2:25 ` [HoTT] " Jon Sterling @ 2017-07-29 7:29 ` Matt Oliveri 0 siblings, 0 replies; 20+ messages in thread From: Matt Oliveri @ 2017-07-29 7:29 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 843 bytes --] On Friday, July 28, 2017 at 10:25:44 PM UTC-4, Jonathan Sterling wrote: > > On Fri, Jul 28, 2017, at 06:47 PM, Matt Oliveri wrote: > > I'm confused. So you want a cubical type theory with only hsets? In what > > sense would there be cubes, other than just points? I thoght OTT had > > propositional extensionality. Though maybe that's only for strict props. > > I think 'propositional extensionality' in OTT was for objects which were > propositions *by definition*, as opposed to h-props in HoTT (which is > something that you prove about a type, and doesn't merely follow from > the intension of the type). > Right, that's what I meant by strict props. If so, it still seems like it should work to redefine equality for types such that hprops are quotiented based on logical equivalence, and equality of other types is left alone. [-- Attachment #1.2: Type: text/html, Size: 1050 bytes --] ^ permalink raw reply [flat|nested] 20+ messages in thread
* Re: [HoTT] Re: cubical type theory with UIP 2017-07-29 1:47 ` Matt Oliveri 2017-07-29 2:25 ` [HoTT] " Jon Sterling @ 2017-07-29 6:19 ` Michael Shulman 2017-07-29 7:23 ` Matt Oliveri 1 sibling, 1 reply; 20+ messages in thread From: Michael Shulman @ 2017-07-29 6:19 UTC (permalink / raw) To: Matt Oliveri; +Cc: Homotopy Type Theory Right: up to homotopy, all cubes would be equivalent to points (hence my question #1). On Fri, Jul 28, 2017 at 6:47 PM, Matt Oliveri <atm...@gmail.com> wrote: > I'm confused. So you want a cubical type theory with only hsets? In what > sense would there be cubes, other than just points? I thoght OTT had > propositional extensionality. Though maybe that's only for strict props. > > > On Sunday, July 23, 2017 at 6:54:39 PM UTC-4, Michael Shulman wrote: >> >> I am wondering about versions of cubical type theory with UIP. The >> motivation would be to have a type theory with canonicity for >> 1-categorical semantics that can prove both function extensionality >> and propositional univalence. (I am aware of Observational Type >> Theory, which I believe has UIP and proves function extensionality, >> but I don't think it proves propositional univalence -- although I >> would be happy to be wrong about that.) >> >> Presumably we obtain a cubical type theory that's compatible with >> axiomatic UIP if in CCHM cubical type theory we postulate only a >> single universe of propositions. But I wonder about some possible >> refinements, such as: >> >> 1. In this case do we still need *all* the Kan composition and gluing >> operations? If all types are hsets then it seems like it ought to be >> unnecessary to have these operations at all higher dimensions. >> >> 2. Can it be enhanced to make UIP provable, such as by adding a >> computing K eliminator? >> >> Mike > > -- > 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 HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. ^ permalink raw reply [flat|nested] 20+ messages in thread
* Re: [HoTT] Re: cubical type theory with UIP 2017-07-29 6:19 ` Michael Shulman @ 2017-07-29 7:23 ` Matt Oliveri 2017-07-29 8:07 ` Michael Shulman 0 siblings, 1 reply; 20+ messages in thread From: Matt Oliveri @ 2017-07-29 7:23 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 1950 bytes --] Only up to homotopy? So you still want the model to be using cubical sets? Actually, couldn't you interpret OTT into the hsets, internally to HoTT? It'd be a hassle without a real solution to the infinite coherence problem, but it should work, since the h-levels involved are bounded. On Saturday, July 29, 2017 at 2:20:06 AM UTC-4, Michael Shulman wrote: > > Right: up to homotopy, all cubes would be equivalent to points (hence > my question #1). > > On Fri, Jul 28, 2017 at 6:47 PM, Matt Oliveri <atm...@gmail.com > <javascript:>> wrote: > > I'm confused. So you want a cubical type theory with only hsets? In what > > sense would there be cubes, other than just points? I thoght OTT had > > propositional extensionality. Though maybe that's only for strict props. > > > > > > On Sunday, July 23, 2017 at 6:54:39 PM UTC-4, Michael Shulman wrote: > >> > >> I am wondering about versions of cubical type theory with UIP. The > >> motivation would be to have a type theory with canonicity for > >> 1-categorical semantics that can prove both function extensionality > >> and propositional univalence. (I am aware of Observational Type > >> Theory, which I believe has UIP and proves function extensionality, > >> but I don't think it proves propositional univalence -- although I > >> would be happy to be wrong about that.) > >> > >> Presumably we obtain a cubical type theory that's compatible with > >> axiomatic UIP if in CCHM cubical type theory we postulate only a > >> single universe of propositions. But I wonder about some possible > >> refinements, such as: > >> > >> 1. In this case do we still need *all* the Kan composition and gluing > >> operations? If all types are hsets then it seems like it ought to be > >> unnecessary to have these operations at all higher dimensions. > >> > >> 2. Can it be enhanced to make UIP provable, such as by adding a > >> computing K eliminator? > >> > >> Mike > [-- Attachment #1.2: Type: text/html, Size: 2538 bytes --] ^ permalink raw reply [flat|nested] 20+ messages in thread
* Re: [HoTT] Re: cubical type theory with UIP 2017-07-29 7:23 ` Matt Oliveri @ 2017-07-29 8:07 ` Michael Shulman 2017-07-29 10:19 ` Matt Oliveri 0 siblings, 1 reply; 20+ messages in thread From: Michael Shulman @ 2017-07-29 8:07 UTC (permalink / raw) To: Matt Oliveri; +Cc: Homotopy Type Theory As I said, > The motivation would be to have a type theory with canonicity for > 1-categorical semantics So no, I don't want "the model" to be using cubical sets, I want models in all suitable 1-categories (e.g. Pi-pretopos etc.). On Sat, Jul 29, 2017 at 12:23 AM, Matt Oliveri <atm...@gmail.com> wrote: > Only up to homotopy? So you still want the model to be using cubical sets? > Actually, couldn't you interpret OTT into the hsets, internally to HoTT? > It'd be a hassle without a real solution to the infinite coherence problem, > but it should work, since the h-levels involved are bounded. > > On Saturday, July 29, 2017 at 2:20:06 AM UTC-4, Michael Shulman wrote: >> >> Right: up to homotopy, all cubes would be equivalent to points (hence >> my question #1). >> >> On Fri, Jul 28, 2017 at 6:47 PM, Matt Oliveri <atm...@gmail.com> wrote: >> > I'm confused. So you want a cubical type theory with only hsets? In what >> > sense would there be cubes, other than just points? I thoght OTT had >> > propositional extensionality. Though maybe that's only for strict props. >> > >> > >> > On Sunday, July 23, 2017 at 6:54:39 PM UTC-4, Michael Shulman wrote: >> >> >> >> I am wondering about versions of cubical type theory with UIP. The >> >> motivation would be to have a type theory with canonicity for >> >> 1-categorical semantics that can prove both function extensionality >> >> and propositional univalence. (I am aware of Observational Type >> >> Theory, which I believe has UIP and proves function extensionality, >> >> but I don't think it proves propositional univalence -- although I >> >> would be happy to be wrong about that.) >> >> >> >> Presumably we obtain a cubical type theory that's compatible with >> >> axiomatic UIP if in CCHM cubical type theory we postulate only a >> >> single universe of propositions. But I wonder about some possible >> >> refinements, such as: >> >> >> >> 1. In this case do we still need *all* the Kan composition and gluing >> >> operations? If all types are hsets then it seems like it ought to be >> >> unnecessary to have these operations at all higher dimensions. >> >> >> >> 2. Can it be enhanced to make UIP provable, such as by adding a >> >> computing K eliminator? >> >> >> >> Mike > > -- > 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 HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. ^ permalink raw reply [flat|nested] 20+ messages in thread
* Re: [HoTT] Re: cubical type theory with UIP 2017-07-29 8:07 ` Michael Shulman @ 2017-07-29 10:19 ` Matt Oliveri 2017-07-29 11:08 ` Matt Oliveri 0 siblings, 1 reply; 20+ messages in thread From: Matt Oliveri @ 2017-07-29 10:19 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 2708 bytes --] Sorry. I got distracted because the type theory you seem to be asking for doesn't sound cubical. Like I said, I suspect OTT could handle hprop extensionality, if it doesn't already. Probably ETT could too. On Saturday, July 29, 2017 at 4:08:01 AM UTC-4, Michael Shulman wrote: > > As I said, > > > The motivation would be to have a type theory with canonicity for > > 1-categorical semantics > > So no, I don't want "the model" to be using cubical sets, I want > models in all suitable 1-categories (e.g. Pi-pretopos etc.). > > On Sat, Jul 29, 2017 at 12:23 AM, Matt Oliveri <atm...@gmail.com > <javascript:>> wrote: > > Only up to homotopy? So you still want the model to be using cubical > sets? > > Actually, couldn't you interpret OTT into the hsets, internally to HoTT? > > It'd be a hassle without a real solution to the infinite coherence > problem, > > but it should work, since the h-levels involved are bounded. > > > > On Saturday, July 29, 2017 at 2:20:06 AM UTC-4, Michael Shulman wrote: > >> > >> Right: up to homotopy, all cubes would be equivalent to points (hence > >> my question #1). > >> > >> On Fri, Jul 28, 2017 at 6:47 PM, Matt Oliveri <atm...@gmail.com> > wrote: > >> > I'm confused. So you want a cubical type theory with only hsets? In > what > >> > sense would there be cubes, other than just points? I thoght OTT had > >> > propositional extensionality. Though maybe that's only for strict > props. > >> > > >> > > >> > On Sunday, July 23, 2017 at 6:54:39 PM UTC-4, Michael Shulman wrote: > >> >> > >> >> I am wondering about versions of cubical type theory with UIP. The > >> >> motivation would be to have a type theory with canonicity for > >> >> 1-categorical semantics that can prove both function extensionality > >> >> and propositional univalence. (I am aware of Observational Type > >> >> Theory, which I believe has UIP and proves function extensionality, > >> >> but I don't think it proves propositional univalence -- although I > >> >> would be happy to be wrong about that.) > >> >> > >> >> Presumably we obtain a cubical type theory that's compatible with > >> >> axiomatic UIP if in CCHM cubical type theory we postulate only a > >> >> single universe of propositions. But I wonder about some possible > >> >> refinements, such as: > >> >> > >> >> 1. In this case do we still need *all* the Kan composition and > gluing > >> >> operations? If all types are hsets then it seems like it ought to > be > >> >> unnecessary to have these operations at all higher dimensions. > >> >> > >> >> 2. Can it be enhanced to make UIP provable, such as by adding a > >> >> computing K eliminator? > >> >> > >> >> Mike > [-- Attachment #1.2: Type: text/html, Size: 3569 bytes --] ^ permalink raw reply [flat|nested] 20+ messages in thread
* Re: [HoTT] Re: cubical type theory with UIP 2017-07-29 10:19 ` Matt Oliveri @ 2017-07-29 11:08 ` Matt Oliveri 2017-07-29 21:19 ` Michael Shulman 0 siblings, 1 reply; 20+ messages in thread From: Matt Oliveri @ 2017-07-29 11:08 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 3184 bytes --] Now I'm having second thoughts. Quotienting together hprops might make type equality computationally relevant. Not something you want with OTT's strict props or ETT's equality. Maybe 2-dimensional type theory would be good for the job. In this case the 2-cells would not be distinguishable by equality, but might still have computational content. On Saturday, July 29, 2017 at 6:19:57 AM UTC-4, Matt Oliveri wrote: > > Sorry. I got distracted because the type theory you seem to be asking for > doesn't sound cubical. Like I said, I suspect OTT could handle hprop > extensionality, if it doesn't already. Probably ETT could too. > > On Saturday, July 29, 2017 at 4:08:01 AM UTC-4, Michael Shulman wrote: >> >> As I said, >> >> > The motivation would be to have a type theory with canonicity for >> > 1-categorical semantics >> >> So no, I don't want "the model" to be using cubical sets, I want >> models in all suitable 1-categories (e.g. Pi-pretopos etc.). >> >> On Sat, Jul 29, 2017 at 12:23 AM, Matt Oliveri <atm...@gmail.com> wrote: >> > Only up to homotopy? So you still want the model to be using cubical >> sets? >> > Actually, couldn't you interpret OTT into the hsets, internally to >> HoTT? >> > It'd be a hassle without a real solution to the infinite coherence >> problem, >> > but it should work, since the h-levels involved are bounded. >> > >> > On Saturday, July 29, 2017 at 2:20:06 AM UTC-4, Michael Shulman wrote: >> >> >> >> Right: up to homotopy, all cubes would be equivalent to points (hence >> >> my question #1). >> >> >> >> On Fri, Jul 28, 2017 at 6:47 PM, Matt Oliveri <atm...@gmail.com> >> wrote: >> >> > I'm confused. So you want a cubical type theory with only hsets? In >> what >> >> > sense would there be cubes, other than just points? I thoght OTT had >> >> > propositional extensionality. Though maybe that's only for strict >> props. >> >> > >> >> > >> >> > On Sunday, July 23, 2017 at 6:54:39 PM UTC-4, Michael Shulman wrote: >> >> >> >> >> >> I am wondering about versions of cubical type theory with UIP. The >> >> >> motivation would be to have a type theory with canonicity for >> >> >> 1-categorical semantics that can prove both function extensionality >> >> >> and propositional univalence. (I am aware of Observational Type >> >> >> Theory, which I believe has UIP and proves function extensionality, >> >> >> but I don't think it proves propositional univalence -- although I >> >> >> would be happy to be wrong about that.) >> >> >> >> >> >> Presumably we obtain a cubical type theory that's compatible with >> >> >> axiomatic UIP if in CCHM cubical type theory we postulate only a >> >> >> single universe of propositions. But I wonder about some possible >> >> >> refinements, such as: >> >> >> >> >> >> 1. In this case do we still need *all* the Kan composition and >> gluing >> >> >> operations? If all types are hsets then it seems like it ought to >> be >> >> >> unnecessary to have these operations at all higher dimensions. >> >> >> >> >> >> 2. Can it be enhanced to make UIP provable, such as by adding a >> >> >> computing K eliminator? >> >> >> >> >> >> Mike >> > [-- Attachment #1.2: Type: text/html, Size: 3961 bytes --] ^ permalink raw reply [flat|nested] 20+ messages in thread
* Re: [HoTT] Re: cubical type theory with UIP 2017-07-29 11:08 ` Matt Oliveri @ 2017-07-29 21:19 ` Michael Shulman [not found] ` <8f052071-09e0-74db-13dc-7f76bc71e374@cs.bham.ac.uk> 2017-07-31 4:19 ` Matt Oliveri 0 siblings, 2 replies; 20+ messages in thread From: Michael Shulman @ 2017-07-29 21:19 UTC (permalink / raw) To: Matt Oliveri; +Cc: Homotopy Type Theory But it seems to me that cubical type theory could solve these problems in a nicer way, which is why I asked. On Sat, Jul 29, 2017 at 4:08 AM, Matt Oliveri <atm...@gmail.com> wrote: > Now I'm having second thoughts. Quotienting together hprops might make type > equality computationally relevant. Not something you want with OTT's strict > props or ETT's equality. Maybe 2-dimensional type theory would be good for > the job. In this case the 2-cells would not be distinguishable by equality, > but might still have computational content. > > > On Saturday, July 29, 2017 at 6:19:57 AM UTC-4, Matt Oliveri wrote: >> >> Sorry. I got distracted because the type theory you seem to be asking for >> doesn't sound cubical. Like I said, I suspect OTT could handle hprop >> extensionality, if it doesn't already. Probably ETT could too. >> >> On Saturday, July 29, 2017 at 4:08:01 AM UTC-4, Michael Shulman wrote: >>> >>> As I said, >>> >>> > The motivation would be to have a type theory with canonicity for >>> > 1-categorical semantics >>> >>> So no, I don't want "the model" to be using cubical sets, I want >>> models in all suitable 1-categories (e.g. Pi-pretopos etc.). >>> >>> On Sat, Jul 29, 2017 at 12:23 AM, Matt Oliveri <atm...@gmail.com> wrote: >>> > Only up to homotopy? So you still want the model to be using cubical >>> > sets? >>> > Actually, couldn't you interpret OTT into the hsets, internally to >>> > HoTT? >>> > It'd be a hassle without a real solution to the infinite coherence >>> > problem, >>> > but it should work, since the h-levels involved are bounded. >>> > >>> > On Saturday, July 29, 2017 at 2:20:06 AM UTC-4, Michael Shulman wrote: >>> >> >>> >> Right: up to homotopy, all cubes would be equivalent to points (hence >>> >> my question #1). >>> >> >>> >> On Fri, Jul 28, 2017 at 6:47 PM, Matt Oliveri <atm...@gmail.com> >>> >> wrote: >>> >> > I'm confused. So you want a cubical type theory with only hsets? In >>> >> > what >>> >> > sense would there be cubes, other than just points? I thoght OTT had >>> >> > propositional extensionality. Though maybe that's only for strict >>> >> > props. >>> >> > >>> >> > >>> >> > On Sunday, July 23, 2017 at 6:54:39 PM UTC-4, Michael Shulman wrote: >>> >> >> >>> >> >> I am wondering about versions of cubical type theory with UIP. The >>> >> >> motivation would be to have a type theory with canonicity for >>> >> >> 1-categorical semantics that can prove both function extensionality >>> >> >> and propositional univalence. (I am aware of Observational Type >>> >> >> Theory, which I believe has UIP and proves function extensionality, >>> >> >> but I don't think it proves propositional univalence -- although I >>> >> >> would be happy to be wrong about that.) >>> >> >> >>> >> >> Presumably we obtain a cubical type theory that's compatible with >>> >> >> axiomatic UIP if in CCHM cubical type theory we postulate only a >>> >> >> single universe of propositions. But I wonder about some possible >>> >> >> refinements, such as: >>> >> >> >>> >> >> 1. In this case do we still need *all* the Kan composition and >>> >> >> gluing >>> >> >> operations? If all types are hsets then it seems like it ought to >>> >> >> be >>> >> >> unnecessary to have these operations at all higher dimensions. >>> >> >> >>> >> >> 2. Can it be enhanced to make UIP provable, such as by adding a >>> >> >> computing K eliminator? >>> >> >> >>> >> >> Mike > > -- > 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 HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. ^ permalink raw reply [flat|nested] 20+ messages in thread
[parent not found: <8f052071-09e0-74db-13dc-7f76bc71e374@cs.bham.ac.uk>]
* Re: [HoTT] Re: cubical type theory with UIP [not found] ` <8f052071-09e0-74db-13dc-7f76bc71e374@cs.bham.ac.uk> @ 2017-07-31 3:49 ` Matt Oliveri 2017-07-31 15:50 ` Michael Shulman 0 siblings, 1 reply; 20+ messages in thread From: Matt Oliveri @ 2017-07-31 3:49 UTC (permalink / raw) To: Homotopy Type Theory; +Cc: Martin Escardo, Michael Shulman On Sun, Jul 30, 2017 at 4:26 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote: > I am interested in this question. > > Univalent type theory gives something we don't have in e.g. the calculus > of constructions, such as unique choice, or function extensionality or > propositional extensionality. > > A very attractive type theory, before we start to consider higher > dimensional types that are not sets, is an intensional Martin-Loef type > theory in with universes of propositions and of sets, with propositional > truncation, function extensionality, propositional extensionality, > quotients, Sigma and Exists. > > (1) What is this type theory? (Whatever it is, it is a common extension > of some spartan intensional Martin-Loef type theory and the internal > language of the free elementary topos.) > > (2) What are its models? In particular (as Mike asks), which fragment of > the cubical model does it correspond to? > > Martin I'm curious what you guys are thinking of doing with this kind of system, and why extensional equality of strict propositions is not enough. Is it just that using strict propositions is bad style for structuralists? Or maybe I just mistakenly assumed strict propositional extensionality is not enough. (Any computational content of proofs of strict propositions is not internalized. So with constructive functions, strict propositions do not provide unique choice.) > On 29/07/17 22:19, Michael Shulman wrote: >> But it seems to me that cubical type theory could solve these problems >> in a nicer way, which is why I asked. >> >> On Sat, Jul 29, 2017 at 4:08 AM, Matt Oliveri <atm...@gmail.com> wrote: >>> Now I'm having second thoughts. Quotienting together hprops might make type >>> equality computationally relevant. Not something you want with OTT's strict >>> props or ETT's equality. Maybe 2-dimensional type theory would be good for >>> the job. In this case the 2-cells would not be distinguishable by equality, >>> but might still have computational content. >>> >>> >>> On Saturday, July 29, 2017 at 6:19:57 AM UTC-4, Matt Oliveri wrote: >>>> >>>> Sorry. I got distracted because the type theory you seem to be asking for >>>> doesn't sound cubical. Like I said, I suspect OTT could handle hprop >>>> extensionality, if it doesn't already. Probably ETT could too. >>>> >>>> On Saturday, July 29, 2017 at 4:08:01 AM UTC-4, Michael Shulman wrote: >>>>> >>>>> As I said, >>>>> >>>>>> The motivation would be to have a type theory with canonicity for >>>>>> 1-categorical semantics >>>>> >>>>> So no, I don't want "the model" to be using cubical sets, I want >>>>> models in all suitable 1-categories (e.g. Pi-pretopos etc.). >>>>> >>>>> On Sat, Jul 29, 2017 at 12:23 AM, Matt Oliveri <atm...@gmail.com> wrote: >>>>>> Only up to homotopy? So you still want the model to be using cubical >>>>>> sets? >>>>>> Actually, couldn't you interpret OTT into the hsets, internally to >>>>>> HoTT? >>>>>> It'd be a hassle without a real solution to the infinite coherence >>>>>> problem, >>>>>> but it should work, since the h-levels involved are bounded. >>>>>> >>>>>> On Saturday, July 29, 2017 at 2:20:06 AM UTC-4, Michael Shulman wrote: >>>>>>> >>>>>>> Right: up to homotopy, all cubes would be equivalent to points (hence >>>>>>> my question #1). >>>>>>> >>>>>>> On Fri, Jul 28, 2017 at 6:47 PM, Matt Oliveri <atm...@gmail.com> >>>>>>> wrote: >>>>>>>> I'm confused. So you want a cubical type theory with only hsets? In >>>>>>>> what >>>>>>>> sense would there be cubes, other than just points? I thoght OTT had >>>>>>>> propositional extensionality. Though maybe that's only for strict >>>>>>>> props. >>>>>>>> >>>>>>>> >>>>>>>> On Sunday, July 23, 2017 at 6:54:39 PM UTC-4, Michael Shulman wrote: >>>>>>>>> >>>>>>>>> I am wondering about versions of cubical type theory with UIP. The >>>>>>>>> motivation would be to have a type theory with canonicity for >>>>>>>>> 1-categorical semantics that can prove both function extensionality >>>>>>>>> and propositional univalence. (I am aware of Observational Type >>>>>>>>> Theory, which I believe has UIP and proves function extensionality, >>>>>>>>> but I don't think it proves propositional univalence -- although I >>>>>>>>> would be happy to be wrong about that.) >>>>>>>>> >>>>>>>>> Presumably we obtain a cubical type theory that's compatible with >>>>>>>>> axiomatic UIP if in CCHM cubical type theory we postulate only a >>>>>>>>> single universe of propositions. But I wonder about some possible >>>>>>>>> refinements, such as: >>>>>>>>> >>>>>>>>> 1. In this case do we still need *all* the Kan composition and >>>>>>>>> gluing >>>>>>>>> operations? If all types are hsets then it seems like it ought to >>>>>>>>> be >>>>>>>>> unnecessary to have these operations at all higher dimensions. >>>>>>>>> >>>>>>>>> 2. Can it be enhanced to make UIP provable, such as by adding a >>>>>>>>> computing K eliminator? >>>>>>>>> >>>>>>>>> Mike ^ permalink raw reply [flat|nested] 20+ messages in thread
* Re: [HoTT] Re: cubical type theory with UIP 2017-07-31 3:49 ` Matt Oliveri @ 2017-07-31 15:50 ` Michael Shulman 2017-07-31 17:36 ` Matt Oliveri ` (2 more replies) 0 siblings, 3 replies; 20+ messages in thread From: Michael Shulman @ 2017-07-31 15:50 UTC (permalink / raw) To: Matt Oliveri; +Cc: Homotopy Type Theory, Martin Escardo As I've said twice already, what I want to do with this system is use it as an internal language for 1-toposes. So to me, that is the answer to Martin's question (2). I'm not quite sure what Martin means by his question (1), since he's just described a type theory, but the original question I asked was whether cubical methods can be used to describe a version of such a type theory with canonicity. Another motivation is that as far as I know, there is not a really satisfactory version of sequent calculus for first-order logic with equality (e.g. not having a fully satisfactory cut-elimination theorem). If cubical methods are a good way to treat equality "computationally", I wonder whether a "cubical sequent calculus" would be able to deal with equality better. I'm not quite sure what a "strict proposition" is, but if you mean having a type of propositions that doesn't include all of them, then the reason that's not enough for me is that frequently in univalent type theory we encounter types that we *prove* to be propositions even though they are not "given as such", such as "being contractible" and "being a proposition", and this is responsible for a significant amount of the unique flavor and usefulness of univalent type theory. For semantic reasons I wouldn't want to use intuitionistic set theory, because it doesn't naturally occur as the internal language of categories. You can perform contortions to model it therein, but that involves interpreting it into type theory rather than the other way around. I don't know what you mean by "somehow clean it up into a type system", but if you can do that cleaning up and obtain a type theory (a "formal type theory" in Bob Harper's sense, not a "computational type theory", i.e. one that is inductively generated by rules rather than assigning types to untyped terms in an "intended semantics"), then I'd like to see it. Mike On Sun, Jul 30, 2017 at 8:49 PM, Matt Oliveri <atm...@gmail.com> wrote: > On Sun, Jul 30, 2017 at 4:26 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote: >> I am interested in this question. >> >> Univalent type theory gives something we don't have in e.g. the calculus >> of constructions, such as unique choice, or function extensionality or >> propositional extensionality. >> >> A very attractive type theory, before we start to consider higher >> dimensional types that are not sets, is an intensional Martin-Loef type >> theory in with universes of propositions and of sets, with propositional >> truncation, function extensionality, propositional extensionality, >> quotients, Sigma and Exists. >> >> (1) What is this type theory? (Whatever it is, it is a common extension >> of some spartan intensional Martin-Loef type theory and the internal >> language of the free elementary topos.) >> >> (2) What are its models? In particular (as Mike asks), which fragment of >> the cubical model does it correspond to? >> >> Martin > > I'm curious what you guys are thinking of doing with this kind of > system, and why extensional equality of strict propositions is not > enough. Is it just that using strict propositions is bad style for > structuralists? Or maybe I just mistakenly assumed strict > propositional extensionality is not enough. > > (Any computational content of proofs of strict propositions is not > internalized. So with constructive functions, strict propositions do > not provide unique choice.) > >> On 29/07/17 22:19, Michael Shulman wrote: >>> But it seems to me that cubical type theory could solve these problems >>> in a nicer way, which is why I asked. >>> >>> On Sat, Jul 29, 2017 at 4:08 AM, Matt Oliveri <atm...@gmail.com> wrote: >>>> Now I'm having second thoughts. Quotienting together hprops might make type >>>> equality computationally relevant. Not something you want with OTT's strict >>>> props or ETT's equality. Maybe 2-dimensional type theory would be good for >>>> the job. In this case the 2-cells would not be distinguishable by equality, >>>> but might still have computational content. >>>> >>>> >>>> On Saturday, July 29, 2017 at 6:19:57 AM UTC-4, Matt Oliveri wrote: >>>>> >>>>> Sorry. I got distracted because the type theory you seem to be asking for >>>>> doesn't sound cubical. Like I said, I suspect OTT could handle hprop >>>>> extensionality, if it doesn't already. Probably ETT could too. >>>>> >>>>> On Saturday, July 29, 2017 at 4:08:01 AM UTC-4, Michael Shulman wrote: >>>>>> >>>>>> As I said, >>>>>> >>>>>>> The motivation would be to have a type theory with canonicity for >>>>>>> 1-categorical semantics >>>>>> >>>>>> So no, I don't want "the model" to be using cubical sets, I want >>>>>> models in all suitable 1-categories (e.g. Pi-pretopos etc.). >>>>>> >>>>>> On Sat, Jul 29, 2017 at 12:23 AM, Matt Oliveri <atm...@gmail.com> wrote: >>>>>>> Only up to homotopy? So you still want the model to be using cubical >>>>>>> sets? >>>>>>> Actually, couldn't you interpret OTT into the hsets, internally to >>>>>>> HoTT? >>>>>>> It'd be a hassle without a real solution to the infinite coherence >>>>>>> problem, >>>>>>> but it should work, since the h-levels involved are bounded. >>>>>>> >>>>>>> On Saturday, July 29, 2017 at 2:20:06 AM UTC-4, Michael Shulman wrote: >>>>>>>> >>>>>>>> Right: up to homotopy, all cubes would be equivalent to points (hence >>>>>>>> my question #1). >>>>>>>> >>>>>>>> On Fri, Jul 28, 2017 at 6:47 PM, Matt Oliveri <atm...@gmail.com> >>>>>>>> wrote: >>>>>>>>> I'm confused. So you want a cubical type theory with only hsets? In >>>>>>>>> what >>>>>>>>> sense would there be cubes, other than just points? I thoght OTT had >>>>>>>>> propositional extensionality. Though maybe that's only for strict >>>>>>>>> props. >>>>>>>>> >>>>>>>>> >>>>>>>>> On Sunday, July 23, 2017 at 6:54:39 PM UTC-4, Michael Shulman wrote: >>>>>>>>>> >>>>>>>>>> I am wondering about versions of cubical type theory with UIP. The >>>>>>>>>> motivation would be to have a type theory with canonicity for >>>>>>>>>> 1-categorical semantics that can prove both function extensionality >>>>>>>>>> and propositional univalence. (I am aware of Observational Type >>>>>>>>>> Theory, which I believe has UIP and proves function extensionality, >>>>>>>>>> but I don't think it proves propositional univalence -- although I >>>>>>>>>> would be happy to be wrong about that.) >>>>>>>>>> >>>>>>>>>> Presumably we obtain a cubical type theory that's compatible with >>>>>>>>>> axiomatic UIP if in CCHM cubical type theory we postulate only a >>>>>>>>>> single universe of propositions. But I wonder about some possible >>>>>>>>>> refinements, such as: >>>>>>>>>> >>>>>>>>>> 1. In this case do we still need *all* the Kan composition and >>>>>>>>>> gluing >>>>>>>>>> operations? If all types are hsets then it seems like it ought to >>>>>>>>>> be >>>>>>>>>> unnecessary to have these operations at all higher dimensions. >>>>>>>>>> >>>>>>>>>> 2. Can it be enhanced to make UIP provable, such as by adding a >>>>>>>>>> computing K eliminator? >>>>>>>>>> >>>>>>>>>> Mike > > -- > 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 HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. ^ permalink raw reply [flat|nested] 20+ messages in thread
* Re: [HoTT] Re: cubical type theory with UIP 2017-07-31 15:50 ` Michael Shulman @ 2017-07-31 17:36 ` Matt Oliveri 2017-08-01 9:14 ` Neelakantan Krishnaswami 2017-08-01 21:27 ` Matt Oliveri 2 siblings, 0 replies; 20+ messages in thread From: Matt Oliveri @ 2017-07-31 17:36 UTC (permalink / raw) To: Homotopy Type Theory; +Cc: m.es... [-- Attachment #1.1: Type: text/plain, Size: 7816 bytes --] Can you point me to an example of a not-fully-satisfactory cut elimination theorem for FOL= and say what's wrong with it, so I can better appreciate the problem? On Monday, July 31, 2017 at 11:51:18 AM UTC-4, Michael Shulman wrote: > > As I've said twice already, what I want to do with this system is use > it as an internal language for 1-toposes. So to me, that is the > answer to Martin's question (2). I'm not quite sure what Martin means > by his question (1), since he's just described a type theory, but the > original question I asked was whether cubical methods can be used to > describe a version of such a type theory with canonicity. > > Another motivation is that as far as I know, there is not a really > satisfactory version of sequent calculus for first-order logic with > equality (e.g. not having a fully satisfactory cut-elimination > theorem). If cubical methods are a good way to treat equality > "computationally", I wonder whether a "cubical sequent calculus" would > be able to deal with equality better. > > I'm not quite sure what a "strict proposition" is, but if you mean > having a type of propositions that doesn't include all of them, then > the reason that's not enough for me is that frequently in univalent > type theory we encounter types that we *prove* to be propositions even > though they are not "given as such", such as "being contractible" and > "being a proposition", and this is responsible for a significant > amount of the unique flavor and usefulness of univalent type theory. > > For semantic reasons I wouldn't want to use intuitionistic set theory, > because it doesn't naturally occur as the internal language of > categories. You can perform contortions to model it therein, but that > involves interpreting it into type theory rather than the other way > around. I don't know what you mean by "somehow clean it up into a > type system", but if you can do that cleaning up and obtain a type > theory (a "formal type theory" in Bob Harper's sense, not a > "computational type theory", i.e. one that is inductively generated by > rules rather than assigning types to untyped terms in an "intended > semantics"), then I'd like to see it. > > Mike > > On Sun, Jul 30, 2017 at 8:49 PM, Matt Oliveri <atm...@gmail.com > <javascript:>> wrote: > > On Sun, Jul 30, 2017 at 4:26 PM, Martin Escardo <m.e...@cs.bham.ac.uk > <javascript:>> wrote: > >> I am interested in this question. > >> > >> Univalent type theory gives something we don't have in e.g. the > calculus > >> of constructions, such as unique choice, or function extensionality or > >> propositional extensionality. > >> > >> A very attractive type theory, before we start to consider higher > >> dimensional types that are not sets, is an intensional Martin-Loef type > >> theory in with universes of propositions and of sets, with > propositional > >> truncation, function extensionality, propositional extensionality, > >> quotients, Sigma and Exists. > >> > >> (1) What is this type theory? (Whatever it is, it is a common extension > >> of some spartan intensional Martin-Loef type theory and the internal > >> language of the free elementary topos.) > >> > >> (2) What are its models? In particular (as Mike asks), which fragment > of > >> the cubical model does it correspond to? > >> > >> Martin > > > > I'm curious what you guys are thinking of doing with this kind of > > system, and why extensional equality of strict propositions is not > > enough. Is it just that using strict propositions is bad style for > > structuralists? Or maybe I just mistakenly assumed strict > > propositional extensionality is not enough. > > > > (Any computational content of proofs of strict propositions is not > > internalized. So with constructive functions, strict propositions do > > not provide unique choice.) > > > >> On 29/07/17 22:19, Michael Shulman wrote: > >>> But it seems to me that cubical type theory could solve these problems > >>> in a nicer way, which is why I asked. > >>> > >>> On Sat, Jul 29, 2017 at 4:08 AM, Matt Oliveri <atm...@gmail.com > <javascript:>> wrote: > >>>> Now I'm having second thoughts. Quotienting together hprops might > make type > >>>> equality computationally relevant. Not something you want with OTT's > strict > >>>> props or ETT's equality. Maybe 2-dimensional type theory would be > good for > >>>> the job. In this case the 2-cells would not be distinguishable by > equality, > >>>> but might still have computational content. > >>>> > >>>> > >>>> On Saturday, July 29, 2017 at 6:19:57 AM UTC-4, Matt Oliveri wrote: > >>>>> > >>>>> Sorry. I got distracted because the type theory you seem to be > asking for > >>>>> doesn't sound cubical. Like I said, I suspect OTT could handle hprop > >>>>> extensionality, if it doesn't already. Probably ETT could too. > >>>>> > >>>>> On Saturday, July 29, 2017 at 4:08:01 AM UTC-4, Michael Shulman > wrote: > >>>>>> > >>>>>> As I said, > >>>>>> > >>>>>>> The motivation would be to have a type theory with canonicity for > >>>>>>> 1-categorical semantics > >>>>>> > >>>>>> So no, I don't want "the model" to be using cubical sets, I want > >>>>>> models in all suitable 1-categories (e.g. Pi-pretopos etc.). > >>>>>> > >>>>>> On Sat, Jul 29, 2017 at 12:23 AM, Matt Oliveri <atm...@gmail.com> > wrote: > >>>>>>> Only up to homotopy? So you still want the model to be using > cubical > >>>>>>> sets? > >>>>>>> Actually, couldn't you interpret OTT into the hsets, internally to > >>>>>>> HoTT? > >>>>>>> It'd be a hassle without a real solution to the infinite coherence > >>>>>>> problem, > >>>>>>> but it should work, since the h-levels involved are bounded. > >>>>>>> > >>>>>>> On Saturday, July 29, 2017 at 2:20:06 AM UTC-4, Michael Shulman > wrote: > >>>>>>>> > >>>>>>>> Right: up to homotopy, all cubes would be equivalent to points > (hence > >>>>>>>> my question #1). > >>>>>>>> > >>>>>>>> On Fri, Jul 28, 2017 at 6:47 PM, Matt Oliveri <atm...@gmail.com> > >>>>>>>> wrote: > >>>>>>>>> I'm confused. So you want a cubical type theory with only hsets? > In > >>>>>>>>> what > >>>>>>>>> sense would there be cubes, other than just points? I thoght OTT > had > >>>>>>>>> propositional extensionality. Though maybe that's only for > strict > >>>>>>>>> props. > >>>>>>>>> > >>>>>>>>> > >>>>>>>>> On Sunday, July 23, 2017 at 6:54:39 PM UTC-4, Michael Shulman > wrote: > >>>>>>>>>> > >>>>>>>>>> I am wondering about versions of cubical type theory with UIP. > The > >>>>>>>>>> motivation would be to have a type theory with canonicity for > >>>>>>>>>> 1-categorical semantics that can prove both function > extensionality > >>>>>>>>>> and propositional univalence. (I am aware of Observational > Type > >>>>>>>>>> Theory, which I believe has UIP and proves function > extensionality, > >>>>>>>>>> but I don't think it proves propositional univalence -- > although I > >>>>>>>>>> would be happy to be wrong about that.) > >>>>>>>>>> > >>>>>>>>>> Presumably we obtain a cubical type theory that's compatible > with > >>>>>>>>>> axiomatic UIP if in CCHM cubical type theory we postulate only > a > >>>>>>>>>> single universe of propositions. But I wonder about some > possible > >>>>>>>>>> refinements, such as: > >>>>>>>>>> > >>>>>>>>>> 1. In this case do we still need *all* the Kan composition and > >>>>>>>>>> gluing > >>>>>>>>>> operations? If all types are hsets then it seems like it ought > to > >>>>>>>>>> be > >>>>>>>>>> unnecessary to have these operations at all higher dimensions. > >>>>>>>>>> > >>>>>>>>>> 2. Can it be enhanced to make UIP provable, such as by adding a > >>>>>>>>>> computing K eliminator? > >>>>>>>>>> > >>>>>>>>>> Mike > [-- Attachment #1.2: Type: text/html, Size: 10867 bytes --] ^ permalink raw reply [flat|nested] 20+ messages in thread
* Re: [HoTT] Re: cubical type theory with UIP 2017-07-31 15:50 ` Michael Shulman 2017-07-31 17:36 ` Matt Oliveri @ 2017-08-01 9:14 ` Neelakantan Krishnaswami 2017-08-01 9:20 ` Michael Shulman 2017-08-01 21:27 ` Matt Oliveri 2 siblings, 1 reply; 20+ messages in thread From: Neelakantan Krishnaswami @ 2017-08-01 9:14 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 2632 bytes --] On Monday, July 31, 2017 at 4:51:18 PM UTC+1, Michael Shulman wrote: > > Another motivation is that as far as I know, there is not a really > satisfactory version of sequent calculus for first-order logic with > equality (e.g. not having a fully satisfactory cut-elimination > theorem). If cubical methods are a good way to treat equality > "computationally", I wonder whether a "cubical sequent calculus" would > be able to deal with equality better. > Actually, there *are* good versions of sequent calculus with equality. Jean-Yves Girard and Peter Schroeder-Heister have both given the appropriate rules. So, given a language of terms with some equational theory, the right and left rules are: —————————— =R Γ ⊢ t = t ∀θ ∈ csu(s,t). θ(Γ) ⊢ Θ(C) —————————————————————————— =L Γ, s = t ⊢ C The premise of the left rule quantifies over a *complete set of unifiers* for s and t. For terms freely generated by some signature, there is a single most general unifier (if one exists), and so the left rule has at most one premise. Once you add equations then there can be more than one most general unifier -- possibly even infinite (eg, if terms are lambda-terms modulo beta/eta, as in higher-order unification). The Girard/Schroeder-Heister equality is not the same as the Martin-Lof identity type, but it gives rise to a nicer programming language than raw J does, since the left rule is invertible. Invertible left rules are what give rise to pattern matching syntax, and so languages like Agda choose a fragment where the G/SH rule and J coincide to implement pattern matching. Agda restricts pattern matching so that an identity type argument can only have a refl pattern when the two terms being equated are generated from variables and constructors. So an identity proof p : (cons x y) = (cons a b)) can be matched as refl, but an identity proof q : (append x y) = (append a b)) can't be. This restriction ensures that first-order unification suffices for the G/SH elim, and therefore to implement pattern matching. If you are very interested in this topic, Joshua Dunfield and I have a draft paper where we work out the Curry-Howard story for pattern matching with the G/SH equality (what are called GADTs by PL theorists) in gory detail: * Sound and Complete Bidirectional Typechecking for Higher-Rank Polymorphism and Indexed Types* <http://www.cl.cam.ac.uk/~nk480/gadt.pdf> -- Neel Krishnaswami nk...@cl.cam.ac.uk [-- Attachment #1.2: Type: text/html, Size: 2955 bytes --] ^ permalink raw reply [flat|nested] 20+ messages in thread
* Re: [HoTT] Re: cubical type theory with UIP 2017-08-01 9:14 ` Neelakantan Krishnaswami @ 2017-08-01 9:20 ` Michael Shulman 2017-08-01 9:34 ` James Cheney 0 siblings, 1 reply; 20+ messages in thread From: Michael Shulman @ 2017-08-01 9:20 UTC (permalink / raw) To: Neelakantan Krishnaswami; +Cc: Homotopy Type Theory Yes, I think I've seen something like this before. It may give a good programming language, but from a semantic category-theoretic perspective I don't think it's any good. Two syntactically distinct terms might still turn out to be semantically equal, so you need a left rule for equality that does more than just syntactically analyze the terms being equated. On Tue, Aug 1, 2017 at 2:14 AM, Neelakantan Krishnaswami <n.krish...@cs.bham.ac.uk> wrote: > On Monday, July 31, 2017 at 4:51:18 PM UTC+1, Michael Shulman wrote: >> >> Another motivation is that as far as I know, there is not a really >> satisfactory version of sequent calculus for first-order logic with >> equality (e.g. not having a fully satisfactory cut-elimination >> theorem). If cubical methods are a good way to treat equality >> "computationally", I wonder whether a "cubical sequent calculus" would >> be able to deal with equality better. > > > Actually, there *are* good versions of sequent calculus with > equality. Jean-Yves Girard and Peter Schroeder-Heister have both given > the appropriate rules. So, given a language of terms with some > equational theory, the right and left rules are: > > > —————————— =R > Γ ⊢ t = t > > > ∀θ ∈ csu(s,t). θ(Γ) ⊢ Θ(C) > —————————————————————————— =L > Γ, s = t ⊢ C > > The premise of the left rule quantifies over a *complete set of > unifiers* for s and t. For terms freely generated by some signature, > there is a single most general unifier (if one exists), and so the > left rule has at most one premise. Once you add equations then > there can be more than one most general unifier -- possibly even > infinite (eg, if terms are lambda-terms modulo beta/eta, as in > higher-order unification). > > The Girard/Schroeder-Heister equality is not the same as the Martin-Lof > identity type, but it gives rise to a nicer programming language than raw J > does, since the left rule is invertible. Invertible left rules are what give > rise to > pattern matching syntax, and so languages like Agda choose a fragment > where the G/SH rule and J coincide to implement pattern matching. > > Agda restricts pattern matching so that an identity type > argument can only have a refl pattern when the two terms being equated > are generated from variables and constructors. So an identity proof > p : (cons x y) = (cons a b)) can be matched as refl, but an identity > proof q : (append x y) = (append a b)) can't be. > > This restriction ensures that first-order unification suffices for the > G/SH elim, and therefore to implement pattern matching. > > If you are very interested in this topic, Joshua Dunfield and I have a draft > paper where we work out the Curry-Howard story for pattern matching > with the G/SH equality (what are called GADTs by PL theorists) in gory > detail: > > Sound and Complete Bidirectional Typechecking for Higher-Rank Polymorphism > and Indexed Types > <http://www.cl.cam.ac.uk/~nk480/gadt.pdf> > > -- > Neel Krishnaswami > nk...@cl.cam.ac.uk > > -- > 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 HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. ^ permalink raw reply [flat|nested] 20+ messages in thread
* Re: [HoTT] Re: cubical type theory with UIP 2017-08-01 9:20 ` Michael Shulman @ 2017-08-01 9:34 ` James Cheney 2017-08-01 16:26 ` Michael Shulman 0 siblings, 1 reply; 20+ messages in thread From: James Cheney @ 2017-08-01 9:34 UTC (permalink / raw) To: Michael Shulman; +Cc: Neelakantan Krishnaswami, Homotopy Type Theory [-- Attachment #1: Type: text/plain, Size: 4726 bytes --] Not sure if it's what you're looking for or if it is an example of a "not fully satisfactory" system, but Negri and von Plato's book "Structural Proof Theory" (esp. ch. 6) talks about axiomatic extensions to sequent calculi that preserve cut elimination. The main idea is to turn axioms of the form P1 & ... & Pn => Q1 | ... | Qm into right-rules of the form Q1,Gamma => Delta, ... Qm, Gamma => Delta --------------------------------------------------------------- P1,...,Pn, Gamma => Delta so that no new principal cuts are introduced. This can handle equality or other FOL axioms of the form forall X. /\_i Pi ==> \/_i Q_i where P_i and Q_i are atomic. --James On Tue, Aug 1, 2017 at 10:20 AM, Michael Shulman <shu...@sandiego.edu> wrote: > Yes, I think I've seen something like this before. It may give a good > programming language, but from a semantic category-theoretic > perspective I don't think it's any good. Two syntactically distinct > terms might still turn out to be semantically equal, so you need a > left rule for equality that does more than just syntactically analyze > the terms being equated. > > On Tue, Aug 1, 2017 at 2:14 AM, Neelakantan Krishnaswami > <n.krish...@cs.bham.ac.uk> wrote: > > On Monday, July 31, 2017 at 4:51:18 PM UTC+1, Michael Shulman wrote: > >> > >> Another motivation is that as far as I know, there is not a really > >> satisfactory version of sequent calculus for first-order logic with > >> equality (e.g. not having a fully satisfactory cut-elimination > >> theorem). If cubical methods are a good way to treat equality > >> "computationally", I wonder whether a "cubical sequent calculus" would > >> be able to deal with equality better. > > > > > > Actually, there *are* good versions of sequent calculus with > > equality. Jean-Yves Girard and Peter Schroeder-Heister have both given > > the appropriate rules. So, given a language of terms with some > > equational theory, the right and left rules are: > > > > > > —————————— =R > > Γ ⊢ t = t > > > > > > ∀θ ∈ csu(s,t). θ(Γ) ⊢ Θ(C) > > —————————————————————————— =L > > Γ, s = t ⊢ C > > > > The premise of the left rule quantifies over a *complete set of > > unifiers* for s and t. For terms freely generated by some signature, > > there is a single most general unifier (if one exists), and so the > > left rule has at most one premise. Once you add equations then > > there can be more than one most general unifier -- possibly even > > infinite (eg, if terms are lambda-terms modulo beta/eta, as in > > higher-order unification). > > > > The Girard/Schroeder-Heister equality is not the same as the Martin-Lof > > identity type, but it gives rise to a nicer programming language than > raw J > > does, since the left rule is invertible. Invertible left rules are what > give > > rise to > > pattern matching syntax, and so languages like Agda choose a fragment > > where the G/SH rule and J coincide to implement pattern matching. > > > > Agda restricts pattern matching so that an identity type > > argument can only have a refl pattern when the two terms being equated > > are generated from variables and constructors. So an identity proof > > p : (cons x y) = (cons a b)) can be matched as refl, but an identity > > proof q : (append x y) = (append a b)) can't be. > > > > This restriction ensures that first-order unification suffices for the > > G/SH elim, and therefore to implement pattern matching. > > > > If you are very interested in this topic, Joshua Dunfield and I have a > draft > > paper where we work out the Curry-Howard story for pattern matching > > with the G/SH equality (what are called GADTs by PL theorists) in gory > > detail: > > > > Sound and Complete Bidirectional Typechecking for Higher-Rank > Polymorphism > > and Indexed Types > > <http://www.cl.cam.ac.uk/~nk480/gadt.pdf> > > > > -- > > Neel Krishnaswami > > nk...@cl.cam.ac.uk > > > > -- > > 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 HomotopyTypeThe...@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 HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. > [-- Attachment #2: Type: text/html, Size: 6180 bytes --] ^ permalink raw reply [flat|nested] 20+ messages in thread
* Re: [HoTT] Re: cubical type theory with UIP 2017-08-01 9:34 ` James Cheney @ 2017-08-01 16:26 ` Michael Shulman 0 siblings, 0 replies; 20+ messages in thread From: Michael Shulman @ 2017-08-01 16:26 UTC (permalink / raw) To: James Cheney; +Cc: Neelakantan Krishnaswami, Homotopy Type Theory I think I've seen something like that too; it seems to be basically giving up on eliminating cuts involving equalities by building them into the primitive rules. I would expect equality to be one of the *logical* operations, so that we can eliminate its cuts, rather than being described by axioms as if it were part of the "theory". On Tue, Aug 1, 2017 at 2:34 AM, James Cheney <james....@gmail.com> wrote: > Not sure if it's what you're looking for or if it is an example of a "not > fully satisfactory" system, but Negri and von Plato's book "Structural Proof > Theory" (esp. ch. 6) talks about axiomatic extensions to sequent calculi > that preserve cut elimination. The main idea is to turn axioms of the form > > P1 & ... & Pn => Q1 | ... | Qm > > into right-rules of the form > > Q1,Gamma => Delta, ... Qm, Gamma => Delta > --------------------------------------------------------------- > P1,...,Pn, Gamma => Delta > > so that no new principal cuts are introduced. This can handle equality or > other FOL axioms of the form forall X. /\_i Pi ==> \/_i Q_i where P_i and > Q_i are atomic. > > --James > > > On Tue, Aug 1, 2017 at 10:20 AM, Michael Shulman <shu...@sandiego.edu> > wrote: >> >> Yes, I think I've seen something like this before. It may give a good >> programming language, but from a semantic category-theoretic >> perspective I don't think it's any good. Two syntactically distinct >> terms might still turn out to be semantically equal, so you need a >> left rule for equality that does more than just syntactically analyze >> the terms being equated. >> >> On Tue, Aug 1, 2017 at 2:14 AM, Neelakantan Krishnaswami >> <n.krish...@cs.bham.ac.uk> wrote: >> > On Monday, July 31, 2017 at 4:51:18 PM UTC+1, Michael Shulman wrote: >> >> >> >> Another motivation is that as far as I know, there is not a really >> >> satisfactory version of sequent calculus for first-order logic with >> >> equality (e.g. not having a fully satisfactory cut-elimination >> >> theorem). If cubical methods are a good way to treat equality >> >> "computationally", I wonder whether a "cubical sequent calculus" would >> >> be able to deal with equality better. >> > >> > >> > Actually, there *are* good versions of sequent calculus with >> > equality. Jean-Yves Girard and Peter Schroeder-Heister have both given >> > the appropriate rules. So, given a language of terms with some >> > equational theory, the right and left rules are: >> > >> > >> > —————————— =R >> > Γ ⊢ t = t >> > >> > >> > ∀θ ∈ csu(s,t). θ(Γ) ⊢ Θ(C) >> > —————————————————————————— =L >> > Γ, s = t ⊢ C >> > >> > The premise of the left rule quantifies over a *complete set of >> > unifiers* for s and t. For terms freely generated by some signature, >> > there is a single most general unifier (if one exists), and so the >> > left rule has at most one premise. Once you add equations then >> > there can be more than one most general unifier -- possibly even >> > infinite (eg, if terms are lambda-terms modulo beta/eta, as in >> > higher-order unification). >> > >> > The Girard/Schroeder-Heister equality is not the same as the Martin-Lof >> > identity type, but it gives rise to a nicer programming language than >> > raw J >> > does, since the left rule is invertible. Invertible left rules are what >> > give >> > rise to >> > pattern matching syntax, and so languages like Agda choose a fragment >> > where the G/SH rule and J coincide to implement pattern matching. >> > >> > Agda restricts pattern matching so that an identity type >> > argument can only have a refl pattern when the two terms being equated >> > are generated from variables and constructors. So an identity proof >> > p : (cons x y) = (cons a b)) can be matched as refl, but an identity >> > proof q : (append x y) = (append a b)) can't be. >> > >> > This restriction ensures that first-order unification suffices for the >> > G/SH elim, and therefore to implement pattern matching. >> > >> > If you are very interested in this topic, Joshua Dunfield and I have a >> > draft >> > paper where we work out the Curry-Howard story for pattern matching >> > with the G/SH equality (what are called GADTs by PL theorists) in gory >> > detail: >> > >> > Sound and Complete Bidirectional Typechecking for Higher-Rank >> > Polymorphism >> > and Indexed Types >> > <http://www.cl.cam.ac.uk/~nk480/gadt.pdf> >> > >> > -- >> > Neel Krishnaswami >> > nk...@cl.cam.ac.uk >> > >> > -- >> > 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 HomotopyTypeThe...@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 HomotopyTypeThe...@googlegroups.com. >> For more options, visit https://groups.google.com/d/optout. > > ^ permalink raw reply [flat|nested] 20+ messages in thread
* Re: [HoTT] Re: cubical type theory with UIP 2017-07-31 15:50 ` Michael Shulman 2017-07-31 17:36 ` Matt Oliveri 2017-08-01 9:14 ` Neelakantan Krishnaswami @ 2017-08-01 21:27 ` Matt Oliveri 2 siblings, 0 replies; 20+ messages in thread From: Matt Oliveri @ 2017-08-01 21:27 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 1767 bytes --] On Monday, July 31, 2017 at 11:51:18 AM UTC-4, Michael Shulman wrote: > > I'm not quite sure what a "strict proposition" is, but if you mean > having a type of propositions that doesn't include all of them, then > the reason that's not enough for me is that frequently in univalent > type theory we encounter types that we *prove* to be propositions even > though they are not "given as such", such as "being contractible" and > "being a proposition", and this is responsible for a significant > amount of the unique flavor and usefulness of univalent type theory. > > For semantic reasons I wouldn't want to use intuitionistic set theory, > because it doesn't naturally occur as the internal language of > categories. You can perform contortions to model it therein, but that > involves interpreting it into type theory rather than the other way > around. I don't know what you mean by "somehow clean it up into a > type system", but if you can do that cleaning up and obtain a type > theory (a "formal type theory" in Bob Harper's sense, not a > "computational type theory", i.e. one that is inductively generated by > rules rather than assigning types to untyped terms in an "intended > semantics"), then I'd like to see it. > I'm thinking it would look a lot like OTT, but with unique choice for strict props. Not all subsingletons are strict props, so they would not be subject to propositional extensionality. So this is apparently not what you want. However, I'm not very confident about all that. I wouldn't be that surprised if it worked out differently. (In particular, something OTT-like, but with unique choice may not even make sense.) But I don't think it'll be what you want, in any case. I've lost interest in that approach. [-- Attachment #1.2: Type: text/html, Size: 2104 bytes --] ^ permalink raw reply [flat|nested] 20+ messages in thread
* Re: [HoTT] Re: cubical type theory with UIP 2017-07-29 21:19 ` Michael Shulman [not found] ` <8f052071-09e0-74db-13dc-7f76bc71e374@cs.bham.ac.uk> @ 2017-07-31 4:19 ` Matt Oliveri 1 sibling, 0 replies; 20+ messages in thread From: Matt Oliveri @ 2017-07-31 4:19 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 4460 bytes --] Hey what about if you start with intuitionistic set theory. Use the usual encodings of Martin-Löf types. For the universe of propositions, use the subsets of your favorite singleton. You get proposition extensionality. The way functions are defined provides function extensionality and unique choice. Now consider the realizers for this system and somehow clean it up into a type system. If the realizers are sane, you should get canonicity. Does that work? It's quite different from MLTT: you don't reason about computations. (At least not using "propositions".) On Saturday, July 29, 2017 at 5:19:45 PM UTC-4, Michael Shulman wrote: > > But it seems to me that cubical type theory could solve these problems > in a nicer way, which is why I asked. > > On Sat, Jul 29, 2017 at 4:08 AM, Matt Oliveri <atm...@gmail.com > <javascript:>> wrote: > > Now I'm having second thoughts. Quotienting together hprops might make > type > > equality computationally relevant. Not something you want with OTT's > strict > > props or ETT's equality. Maybe 2-dimensional type theory would be good > for > > the job. In this case the 2-cells would not be distinguishable by > equality, > > but might still have computational content. > > > > > > On Saturday, July 29, 2017 at 6:19:57 AM UTC-4, Matt Oliveri wrote: > >> > >> Sorry. I got distracted because the type theory you seem to be asking > for > >> doesn't sound cubical. Like I said, I suspect OTT could handle hprop > >> extensionality, if it doesn't already. Probably ETT could too. > >> > >> On Saturday, July 29, 2017 at 4:08:01 AM UTC-4, Michael Shulman wrote: > >>> > >>> As I said, > >>> > >>> > The motivation would be to have a type theory with canonicity for > >>> > 1-categorical semantics > >>> > >>> So no, I don't want "the model" to be using cubical sets, I want > >>> models in all suitable 1-categories (e.g. Pi-pretopos etc.). > >>> > >>> On Sat, Jul 29, 2017 at 12:23 AM, Matt Oliveri <atm...@gmail.com> > wrote: > >>> > Only up to homotopy? So you still want the model to be using cubical > >>> > sets? > >>> > Actually, couldn't you interpret OTT into the hsets, internally to > >>> > HoTT? > >>> > It'd be a hassle without a real solution to the infinite coherence > >>> > problem, > >>> > but it should work, since the h-levels involved are bounded. > >>> > > >>> > On Saturday, July 29, 2017 at 2:20:06 AM UTC-4, Michael Shulman > wrote: > >>> >> > >>> >> Right: up to homotopy, all cubes would be equivalent to points > (hence > >>> >> my question #1). > >>> >> > >>> >> On Fri, Jul 28, 2017 at 6:47 PM, Matt Oliveri <atm...@gmail.com> > >>> >> wrote: > >>> >> > I'm confused. So you want a cubical type theory with only hsets? > In > >>> >> > what > >>> >> > sense would there be cubes, other than just points? I thoght OTT > had > >>> >> > propositional extensionality. Though maybe that's only for strict > >>> >> > props. > >>> >> > > >>> >> > > >>> >> > On Sunday, July 23, 2017 at 6:54:39 PM UTC-4, Michael Shulman > wrote: > >>> >> >> > >>> >> >> I am wondering about versions of cubical type theory with UIP. > The > >>> >> >> motivation would be to have a type theory with canonicity for > >>> >> >> 1-categorical semantics that can prove both function > extensionality > >>> >> >> and propositional univalence. (I am aware of Observational Type > >>> >> >> Theory, which I believe has UIP and proves function > extensionality, > >>> >> >> but I don't think it proves propositional univalence -- although > I > >>> >> >> would be happy to be wrong about that.) > >>> >> >> > >>> >> >> Presumably we obtain a cubical type theory that's compatible > with > >>> >> >> axiomatic UIP if in CCHM cubical type theory we postulate only a > >>> >> >> single universe of propositions. But I wonder about some > possible > >>> >> >> refinements, such as: > >>> >> >> > >>> >> >> 1. In this case do we still need *all* the Kan composition and > >>> >> >> gluing > >>> >> >> operations? If all types are hsets then it seems like it ought > to > >>> >> >> be > >>> >> >> unnecessary to have these operations at all higher dimensions. > >>> >> >> > >>> >> >> 2. Can it be enhanced to make UIP provable, such as by adding a > >>> >> >> computing K eliminator? > >>> >> >> > >>> >> >> Mike > [-- Attachment #1.2: Type: text/html, Size: 5900 bytes --] ^ permalink raw reply [flat|nested] 20+ messages in thread
* Re: [HoTT] cubical type theory with UIP 2017-07-23 22:54 cubical type theory with UIP Michael Shulman 2017-07-29 1:47 ` Matt Oliveri @ 2017-08-02 9:40 ` Andrea Vezzosi 1 sibling, 0 replies; 20+ messages in thread From: Andrea Vezzosi @ 2017-08-02 9:40 UTC (permalink / raw) To: Michael Shulman; +Cc: HomotopyT...@googlegroups.com Not really an answer, but one observation about point 2: > 2. Can it be enhanced to make UIP provable, such as by adding a > computing K eliminator? I think we would rather derive K from a computing UIP, because even the J eliminator is derived by proving that any element of (Sigma (y : A), x = y) is equal to (x , refl) by using connections (and then using comp on the obtained path). I think something along these lines should work: suppose we add a primitive UIP0 for every type A (restricting to some universe if needed) UIP0 A : (x y : A) (p : x = y) -> p = refl then "UIP0 A a b (\ i. t)" could compute by scrutinizing A: in case A is a "positive" type it would commute with introductions when a, b and t are all built with the same one; in case A is a "negative" type it would commute with the eliminations. It's quite probable that UIP0 will have to be generalized a bit to make sense for path types, just like composition generalizes transport by also having a system. This might make connections in the interval type redundant, because they wouldn't be needed for J. Best, Andrea On Mon, Jul 24, 2017 at 12:54 AM, Michael Shulman <shu...@sandiego.edu> wrote: > I am wondering about versions of cubical type theory with UIP. The > motivation would be to have a type theory with canonicity for > 1-categorical semantics that can prove both function extensionality > and propositional univalence. (I am aware of Observational Type > Theory, which I believe has UIP and proves function extensionality, > but I don't think it proves propositional univalence -- although I > would be happy to be wrong about that.) > > Presumably we obtain a cubical type theory that's compatible with > axiomatic UIP if in CCHM cubical type theory we postulate only a > single universe of propositions. But I wonder about some possible > refinements, such as: > > 1. In this case do we still need *all* the Kan composition and gluing > operations? If all types are hsets then it seems like it ought to be > unnecessary to have these operations at all higher dimensions. > > 2. Can it be enhanced to make UIP provable, such as by adding a > computing K eliminator? > > Mike > > -- > 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 HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. ^ permalink raw reply [flat|nested] 20+ messages in thread
end of thread, other threads:[~2017-08-02 9:40 UTC | newest] Thread overview: 20+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2017-07-23 22:54 cubical type theory with UIP Michael Shulman 2017-07-29 1:47 ` Matt Oliveri 2017-07-29 2:25 ` [HoTT] " Jon Sterling 2017-07-29 7:29 ` Matt Oliveri 2017-07-29 6:19 ` Michael Shulman 2017-07-29 7:23 ` Matt Oliveri 2017-07-29 8:07 ` Michael Shulman 2017-07-29 10:19 ` Matt Oliveri 2017-07-29 11:08 ` Matt Oliveri 2017-07-29 21:19 ` Michael Shulman [not found] ` <8f052071-09e0-74db-13dc-7f76bc71e374@cs.bham.ac.uk> 2017-07-31 3:49 ` Matt Oliveri 2017-07-31 15:50 ` Michael Shulman 2017-07-31 17:36 ` Matt Oliveri 2017-08-01 9:14 ` Neelakantan Krishnaswami 2017-08-01 9:20 ` Michael Shulman 2017-08-01 9:34 ` James Cheney 2017-08-01 16:26 ` Michael Shulman 2017-08-01 21:27 ` Matt Oliveri 2017-07-31 4:19 ` Matt Oliveri 2017-08-02 9:40 ` [HoTT] " Andrea Vezzosi
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).