computing K

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

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