Re: [HoTT] computing K

[Martin Escardo <escardo...@googlemail.com>]

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
>