cubical type theory with UIP

cubical type theory with UIP

[Michael Shulman]

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

Re: cubical type theory with UIP

[Matt Oliveri]

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

Re: [HoTT] Re: cubical type theory with UIP

[Jon Sterling]

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.

Re: [HoTT] Re: cubical type theory with UIP

[Matt Oliveri]

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

Re: [HoTT] Re: cubical type theory with UIP

[Michael Shulman]

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.

Re: [HoTT] Re: cubical type theory with UIP

[Matt Oliveri]

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

Re: [HoTT] Re: cubical type theory with UIP

[Michael Shulman]

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.

Re: [HoTT] Re: cubical type theory with UIP

[Matt Oliveri]

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

Re: [HoTT] Re: cubical type theory with UIP

[Matt Oliveri]

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

Re: [HoTT] Re: cubical type theory with UIP

[Michael Shulman]

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.

Re: [HoTT] Re: cubical type theory with UIP

[Matt Oliveri]

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

Re: [HoTT] Re: cubical type theory with UIP

[Michael Shulman]

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.

Re: [HoTT] Re: cubical type theory with UIP

[Matt Oliveri]

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

Re: [HoTT] Re: cubical type theory with UIP

[Neelakantan Krishnaswami]

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

Re: [HoTT] Re: cubical type theory with UIP

[Michael Shulman]

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.

Re: [HoTT] Re: cubical type theory with UIP

[James Cheney]

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

Re: [HoTT] Re: cubical type theory with UIP

[Michael Shulman]

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

Re: [HoTT] Re: cubical type theory with UIP

[Matt Oliveri]

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

Re: [HoTT] Re: cubical type theory with UIP

[Matt Oliveri]

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

Re: [HoTT] cubical type theory with UIP

[Andrea Vezzosi]

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.