Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
From: Thomas Streicher <stre...@mathematik.tu-darmstadt.de>
To: Michael Shulman <shu...@sandiego.edu>
Cc: "HomotopyT...@googlegroups.com" <homotopyt...@googlegroups.com>
Subject: Re: [HoTT] computing K
Date: Tue, 25 Apr 2017 15:17:43 +0200	[thread overview]
Message-ID: <20170425131743.GB30195@mathematik.tu-darmstadt.de> (raw)
In-Reply-To: <CAOvivQy_324YDSgS=+J9DSqG113pgbJ5EvUPq=W8XT3Scc++jQ@mail.gmail.com>

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
> 

  reply	other threads:[~2017-04-25 13:17 UTC|newest]

Thread overview: 7+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2017-04-25  9:46 Michael Shulman
2017-04-25 13:17 ` Thomas Streicher [this message]
2017-04-25 14:10   ` [HoTT] " Favonia
2017-04-25 22:05 ` Martin Escardo
     [not found] ` <f9cd4d85-a186-f228-cdc2-75ea4e434e0e@cs.bham.ac.uk>
2017-04-25 23:08   ` Michael Shulman
2017-04-26 20:40     ` Floris van Doorn
2017-04-26 21:33       ` Floris van Doorn

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=20170425131743.GB30195@mathematik.tu-darmstadt.de \
    --to="stre..."@mathematik.tu-darmstadt.de \
    --cc="homotopyt..."@googlegroups.com \
    --cc="shu..."@sandiego.edu \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).