From: "Martín Hötzel Escardó" <"escardo..."@gmail.com>
To: Homotopy Type Theory <HomotopyT...@googlegroups.com>
Subject: Questions regarding univalence as generalized extensionality
Date: Wed, 18 Oct 2017 15:58:43 -0700 (PDT) [thread overview]
Message-ID: <9ab86c8e-dc77-4332-ac6b-aabf6ce11077@googlegroups.com> (raw)
[-- Attachment #1.1: Type: text/plain, Size: 1827 bytes --]
We know, thanks to Vladimir, that univalence implies both
* FunExt: function extensionality (any two pointwise equal functions
are equal)
and
* PropExt: propositional extensionality (any two logically
equivalent propositions are equal).
These implications hold in a basic intensional Martin-Löf type theory (just
containing the ingredients needed to formulate them).
Thus, we may regard univalence as a generalized extensionality axiom for
intensional Martin-Löf theories, as has been often emphasized.
Additionally, in informal parlance, we often see propositional
extensionality equated with propositional univalence.
Let's clarify this, where we adopt X = Y as a notation for Id X Y:
* PropExt (propositional extensionality): For all propositions P and Q, we
have that
(P → Q) and (Q → P) together imply P = Q.
* PropUniv (propositional univalence): For all propositions P and Q, the
map
idtoeq_{P,Q} : P = Q → P ≃ Q
is an equivalence.
It is then clear that PropUniv → PropExt. However, the only way to get
PropUniv from PropExt that I know of requires function extensionality as an
additional assumption. Let's record this as
- PropUniv → PropExt
- FunExt → (PropExt → PropUniv).
Obvious question: does (PropExt→PropUniv) imply FunExt? I don't know.
Less obvious question: Does any of propositional univalence or
propositional extensionality imply FunExt? That is, can we "linearize" the
extensionality axioms as
UA → PropUniv → PropExt → FunExt,
and, if not, less ambitiously as UA → PropUniv → FunExt?
Even less obvious: is univalence restricted to contractible types (call it
ContrUniv) enough to get FunExt?
UA → PropUniv → ContrUniv → FunExt?
Martin
[-- Attachment #1.2: Type: text/html, Size: 2408 bytes --]
reply other threads:[~2017-10-18 22:58 UTC|newest]
Thread overview: [no followups] expand[flat|nested] mbox.gz Atom feed
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=9ab86c8e-dc77-4332-ac6b-aabf6ce11077@googlegroups.com \
--to="escardo..."@gmail.com \
--cc="HomotopyT..."@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).