From: Floris van Doorn <fpvd...@gmail.com>
To: Michael Shulman <shu...@sandiego.edu>
Cc: Martin Escardo <m.es...@cs.bham.ac.uk>,
"HomotopyT...@googlegroups.com" <homotopyt...@googlegroups.com>
Subject: Re: [HoTT] computing K
Date: Wed, 26 Apr 2017 16:40:38 -0400 [thread overview]
Message-ID: <CAAwvom=UCgQOraWQBbqr3TFOGP8DLZNXX_aQ97+sMedOoW3XXQ@mail.gmail.com> (raw)
In-Reply-To: <CAOvivQw47AYByQubyqzQ++rEgcy_cfSqun6xXucWwQiJ6z_Z0Q@mail.gmail.com>
[-- Attachment #1: Type: text/plain, Size: 4784 bytes --]
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
On 25 April 2017 at 19:08, Michael Shulman <shu...@sandiego.edu> wrote:
> 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
> >
> >
> > On 25/04/17 10:46, Michael Shulman wrote:
> >>
> >> 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
> >>
> >
> > --
> > Martin Escardo
> > http://www.cs.bham.ac.uk/~mhe
>
> --
> 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.
>
[-- Attachment #2: Type: text/html, Size: 6267 bytes --]
next prev parent reply other threads:[~2017-04-26 20:40 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 ` [HoTT] " Thomas Streicher
2017-04-25 14:10 ` 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 [this message]
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='CAAwvom=UCgQOraWQBbqr3TFOGP8DLZNXX_aQ97+sMedOoW3XXQ@mail.gmail.com' \
--to="fpvd..."@gmail.com \
--cc="homotopyt..."@googlegroups.com \
--cc="m.es..."@cs.bham.ac.uk \
--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).