From: Nicolai Kraus <nicola...@gmail.com>
To: HomotopyTypeTheory@googlegroups.com
Subject: Re: [HoTT] Weaker forms of univalence
Date: Wed, 19 Jul 2017 19:04:13 +0100 [thread overview]
Message-ID: <b130010e-615a-9713-b129-9318ae12b2db@gmail.com> (raw)
In-Reply-To: <CAOvivQxRx8OPHV=-e_L010b3jaZZMnbaEEu2v0ZOvC2pCttHyA@mail.gmail.com>
On 19/07/17 18:19, Michael Shulman wrote:
> I am not sure about (1). It might be an open question even in the
> case when A and B are propositions.
If we restrict ourselves to the case that A and B are propositions, then
(1) (A ≃ B) -> (A = B)
is as strong as (2) / (3), since (1) then says that equality is implied
by a reflexive propositional relation and thus a proposition.
Of course this needs funext.
(Afaik (1) is often called "propositional extensionality", but we could
also just call it "univalence for propositions.)
We have once discussed on this list whether (1) is consistent with UIP
(i.e. it would be different from (2)), but we did not find an answer.
Nicolai
next prev parent reply other threads:[~2017-07-19 18:04 UTC|newest]
Thread overview: 11+ messages / expand[flat|nested] mbox.gz Atom feed top
2017-07-19 16:26 Ian Orton
2017-07-19 17:19 ` [HoTT] " Michael Shulman
2017-07-19 18:04 ` Nicolai Kraus [this message]
2017-07-20 6:56 ` Bas Spitters
2017-07-20 11:59 ` Steve Awodey
2017-07-20 17:57 ` Michael Shulman
2017-07-21 1:36 ` Matt Oliveri
2017-07-21 7:43 ` Peter LeFanu Lumsdaine
2017-07-19 17:21 ` Jason Gross
2017-07-19 17:28 ` Michael Shulman
2017-07-19 18:02 ` Jason Gross
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=b130010e-615a-9713-b129-9318ae12b2db@gmail.com \
--to="nicola..."@gmail.com \
--cc=HomotopyTypeTheory@googlegroups.com \
/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).