computing K

[Michael Shulman]

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

[Thomas Streicher]

In lccc's (actually finite limits cats) there is no problem to have K.
But K allows one to prove UIP which is in contradiction with UA. So we
can't have K in all model cat's modelling intensioal TT.

Thomas

[Favonia]

I believe Mike is talking about a restricted version of K which only applies to types satisfying UIP, not all types. The question is whether a "weak" K which might not compute can be "strictified" to another K which does, at least in good models. By the way, my question about the restricted K was due to Jesper's attempt to have Agda automatically detect types that admit K (now temporarily disabled). -Favonia

--
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.

[Michael Shulman]

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

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

[Floris van Doorn]

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

--
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.

[Floris van Doorn]

Disregard previous email. I misread Mike's proposed computing K (I thought it was refl on all loops).

To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.

[Martin Escardo]

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: