Re: [HoTT] computing K

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

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