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

[Michael Shulman <shu...@sandiego.edu>]

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.