Discussion of Homotopy Type Theory and Univalent Foundations
 help / Atom feed
From: Jason Gross <jasongross9@gmail.com>
To: Vladimir Voevodsky <vladimir@ias.edu>
Cc: Peter LeFanu Lumsdaine <p.l.lumsdaine@gmail.com>,
	Thierry Coquand <Thierry.Coquand@cse.gu.se>,
	 "HomotopyTypeTheory@googlegroups.com"
	<HomotopyTypeTheory@googlegroups.com>
Subject: Re: [HoTT] Definitions of equivalence satisfying judgmental/strict groupoid laws?
Date: Fri, 16 Aug 2019 17:14:19 -0700
Message-ID: <CAKObCao60=RFWY=Cn0BTV9bWcRCQXRSqOjvCYbS37mHOeJ0Yqg@mail.gmail.com> (raw)
In-Reply-To: <435F59BF-DD90-43E0-926A-D197D38B94B4@ias.edu>

[-- Attachment #1: Type: text/plain, Size: 2719 bytes --]

Resurrecting this thread from many years ago, because I was thinking about
it again recently, it seems to me that although { f &
isTrackedByRelEquiv(f) } satisfies the rule sym (sym e) = e judgmentally,
it doesn't satisfy the rule that sym id = id judgmentally.  (In particular,
I am not sure what relational equivalence to use for the identity
equivalence which does not change judgmentally when I flip the order of its
arguments.)  Is there a version of equivalence which simultaneously
satisfies that the inverse of the identity is judgmentally the identity,
and that inverting an equivalence twice judgmentally gives you what you
started with?

-Jason

On Thu, Nov 13, 2014 at 12:59 PM Vladimir Voevodsky <vladimir@ias.edu>
wrote:

> In general no. But their model is essentially syntactic and more or less
> complete. Or, to be more precise, I would expect it to
> be more or less complete.
>
> V.
>
>
> On Nov 13, 2014, at 9:55 PM, Peter LeFanu Lumsdaine <
> p.l.lumsdaine@gmail.com> wrote:
>
> On Thu, Nov 13, 2014 at 12:04 PM, Vladimir Voevodsky <vladimir@ias.edu>
> wrote:
>
>> The question is about how you interpret this operation for the univalent
>> universe. If there is an interpretation of such an operation then there is
>> a way to define equivalences between types in an involutionary way.
>>
>
> I don’t follow why this should be the case.  This shows that there is some
> notion of equivalence *in the model* (i.e. constructed in the meta-theory)
> which is strictly involutive.  But there is no reason that this notion need
> be definable in the syntax of the object theory, is there?
>
> –p.
>
> --
> 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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
>
>
> --
> 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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
>

-- 
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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAKObCao60%3DRFWY%3DCn0BTV9bWcRCQXRSqOjvCYbS37mHOeJ0Yqg%40mail.gmail.com.

[-- Attachment #2: Type: text/html, Size: 4424 bytes --]

       reply index

Thread overview: 2+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
     [not found] <CAKObCarykcu9p=1VB5YkBPjm3sVzKk9DO9oNYBFthr-jWOGptw@mail.gmail.com>
     [not found] ` <50f257f8-f6a0-410e-9f32-512ebcef1e05@googlegroups.com>
     [not found]   ` <CAOvivQw2sDUx+TVp3RSEL2kFdLzyharBXA-zwB3=o9820NUsnA@mail.gmail.com>
     [not found]     ` <CAAkwb-=sivUFQ5TRCohcykU2Tg49mE38h-6Q-7zUHUaJ5eXMhg@mail.gmail.com>
     [not found]       ` <CAOvivQxmb-gC8gFhVtDnOwxtcYTDH1tXv3B47fpfVwJxtOdgvQ@mail.gmail.com>
     [not found]         ` <CAAkwb-nq7Y142fbiEeC1MQ4n-H66xBc0NaycK2-=nObxbutjXA@mail.gmail.com>
     [not found]           ` <CAGqv1ODSYp-R2W1xvZeP8m04JO_CSbS8ZePL9+cu=mdXQXZRjQ@mail.gmail.com>
     [not found]             ` <CAAkwb-kwaAWfd27doQ6VbMm85Lbs6=Y8p_MCSQc6r0K6_RLyBw@mail.gmail.com>
     [not found]               ` <68F509C8-C1BC-40B9-BE23-B930C801AF1D@ias.edu>
     [not found]                 ` <BD2EF3CB-2A9C-4A7D-9C39-94B25A95DB4B@chalmers.se>
     [not found]                   ` <4957EC32-97FE-4383-AA07-C1ADF4EAF243@ias.edu>
     [not found]                     ` <CAAkwb-n85XxXVNB-V8OdH73qzPgFa50XiNGMbRjASTcLZ_BVRw@mail.gmail.com>
     [not found]                       ` <435F59BF-DD90-43E0-926A-D197D38B94B4@ias.edu>
2019-08-17  0:14                         ` Jason Gross [this message]
2019-09-12  1:45                           ` Martín Hötzel Escardó

Reply instructions:

You may reply publically 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='CAKObCao60=RFWY=Cn0BTV9bWcRCQXRSqOjvCYbS37mHOeJ0Yqg@mail.gmail.com' \
    --to=jasongross9@gmail.com \
    --cc=HomotopyTypeTheory@googlegroups.com \
    --cc=Thierry.Coquand@cse.gu.se \
    --cc=p.l.lumsdaine@gmail.com \
    --cc=vladimir@ias.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

Discussion of Homotopy Type Theory and Univalent Foundations

Archives are clonable: git clone --mirror http://inbox.vuxu.org/hott

Newsgroup available over NNTP:
	nntp://inbox.vuxu.org/vuxu.archive.hott


AGPL code for this site: git clone https://public-inbox.org/ public-inbox