Re: [HoTT] cubical type theory with UIP

[Andrea Vezzosi <sanz...@gmail.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.