I think (1) is indeed wishful thinking.

I can disprove it assuming the following metatheoretical property. I think this property holds for book-HoTT, but I'm not sure.

If X is a HIT and p : A -> X is a path constructor of X, and if p a ≡ p a' for terms a a' : A then a ≡ a'. (Here ≡ is judgmental equality.)

I believe that similar properties are true for MLTT if p is a constructor of an inductive type.

Now let I be the interval with points 0, 1 : I and consider the following HIT:

HIT X :=

| * : X

| p : I -> * = *

| q : p(0) = refl

Note that X is the reduced suspension of the interval, which is contractible, hence in particular a set. But assuming the above metatheoretical property, X cannot have an axiom K with the definitional properties Mike described. That would mean that p(0) ≡ p(1) and hence 0 ≡ 1. But it is impossible that the two points of the interval are judgmentally equal (because you can make a function which sends them to equal, but not judgmentally equal terms, for example (Σ(X : Type), X = empty) and (Σ(X : Type), X = unit)).

Best,

Floris

On 25 April 2017 at 19:08, Michael Shulman <shu...@sandiego.edu> wrote:

Favonia, Dan Licata, and I spent a bit of time trying to answer (1)
but didn't get anywhere. I haven't thought much about (2), but I
think we were unable to think of any nontrivial types for which we
could construct a computing K inside MLTT.

On Tue, Apr 25, 2017 at 3:04 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
> Interesting. So, then, here are some questions:
>
> (1) Suppose, for given type A, a hypothetical
>
> K: (x : A) (p : x == x) -> p == refl
>
> is given, internally in a univalent type theory.
>
> Is it possible to cook-up a K' of the same type, internally in univalent
> type theory, with the definitional behaviour you require?
>
> We are looking for an endofunction of the type ((x : A) (p : x == x) -> p ==
> refl) that performs some sort of definitional improvement.
>
> We know of an instance of such a phenomenon: if a factor f':||X||->A of some
> f:X->A through |-|:X->||X|| is given, then we can find another
> *definitional* factor f':||X||->A.
>
> This is here in agda
> http://www.cs.bham.ac.uk/~mhe/truncation-and-extensionality/hsetfunext.html#15508
> and also in a paper by Nicolai, Thorsten, Thierry and myself.
>
> (2) Failing that, can we, given the same hypothetical K, cook-up a type A'
> equivalent to A (maybe A'= Sigma(x:A) (x=x)) with K' as above?
>
> (That is, maybe A itself won't provably have (1), but still will have an
> equivalent manifestation which does.)
>
> Or is this wishful thinking?
>
> Martin

>
>
> On 25/04/17 10:46, Michael Shulman wrote:
>>
>> Here is a little observation that may be of interest (thanks to
>> Favonia for bringing this question to my attention).
>>
>> The Axiom K that is provable using unrestricted Agda-style
>> pattern-matching has an extra property: it computes to refl on refl.
>> That is, if we define
>>
>> K: (A : Type) (x : A) (p : x == x) -> p == refl
>> K A x refl = refl
>>
>> then the equation "K A x refl = refl" holds definitionally. As was
>> pointed out on the Agda mailing list a while ago, this might be
>> considered a problem if one wants to extend Agda's --without-K to
>> allow unrestricted pattern-matching when the types are automatically
>> provable to be hsets, since a general hset apparently need not admit a
>> K satisfying this *definitional* behavior.
>>
>> However (this is the perhaps-new observation), in good
>> model-categorical semantics, such a "computing K" *can* be constructed
>> for any hset. Suppose we are in a model category whose cofibrations
>> are exactly the monomorphisms, like simplicial sets or any Cisinski
>> model category. If A is an hset, then the map A -> Delta^*(PA) (which
>> type theoretically is A -> Sigma(x:A) (x=x)) is a weak equivalence.
>> But it is also a split monomorphism, hence a cofibration; and thus an
>> acyclic cofibration. Therefore, we can define functions by induction
>> on loops in A that have definitionally computing behavior on refl,
>> which is exactly what unrestricted pattern-matching allows.
>>
>> Mike
>>
>
> --

> Martin Escardo
> http://www.cs.bham.ac.uk/~mhe

--
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 HomotopyTypeTheory+unsub...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.