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

On Tue, Apr 25, 2017 at 9:17 AM Thomas Streicher <
stre...@mathematik.tu-darmstadt.de> wrote:

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