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

[Matt Oliveri <atm...@gmail.com>]

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