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

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

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.