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.