From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Wed, 18 Oct 2017 15:58:43 -0700 (PDT) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: <9ab86c8e-dc77-4332-ac6b-aabf6ce11077@googlegroups.com> Subject: Questions regarding univalence as generalized extensionality MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_600_1843732532.1508367523795" ------=_Part_600_1843732532.1508367523795 Content-Type: multipart/alternative; boundary="----=_Part_601_1869109894.1508367523795" ------=_Part_601_1869109894.1508367523795 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable 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=C3=B6f type theory = (just=20 containing the ingredients needed to formulate them). Thus, we may regard univalence as a generalized extensionality axiom for=20 intensional Martin-L=C3=B6f theories, as has been often emphasized. Additionally, in informal parlance, we often see propositional=20 extensionality equated with propositional univalence. Let's clarify this, where we adopt X =3D Y as a notation for Id X Y: * PropExt (propositional extensionality): For all propositions P and Q, we= =20 have that (P =E2=86=92 Q) and (Q =E2=86=92 P) together imply P =3D Q. * PropUniv (propositional univalence): For all propositions P and Q, the= =20 map=20 idtoeq_{P,Q} : P =3D Q =E2=86=92 P =E2=89=83 Q is an equivalence. It is then clear that PropUniv =E2=86=92 PropExt. However, the only way to = get=20 PropUniv from PropExt that I know of requires function extensionality as an= =20 additional assumption. Let's record this as - PropUniv =E2=86=92 PropExt - FunExt =E2=86=92 (PropExt =E2=86=92 PropUniv). =20 Obvious question: does (PropExt=E2=86=92PropUniv) imply FunExt? I don't kno= w. Less obvious question: Does any of propositional univalence or=20 propositional extensionality imply FunExt? That is, can we "linearize" the= =20 extensionality axioms as UA =E2=86=92 PropUniv =E2=86=92 PropExt =E2=86=92 FunExt, and, if not, less ambitiously as UA =E2=86=92 PropUniv =E2=86=92 FunExt? Even less obvious: is univalence restricted to contractible types (call it= =20 ContrUniv) enough to get FunExt? UA =E2=86=92 PropUniv =E2=86=92 ContrUniv =E2=86=92 FunExt? Martin ------=_Part_601_1869109894.1508367523795 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
We know, thanks to Vladimir, that univalence implies = both

=C2=A0* FunExt: function extensionality (any = two pointwise equal functions
=C2=A0 =C2=A0are equal)
<= br>
and

=C2=A0* PropExt: propositional e= xtensionality (any two logically
=C2=A0 =C2=A0equivalent proposit= ions are equal).

These implications hold in a basi= c intensional Martin-L=C3=B6f type theory (just containing the ingredients = needed to formulate them).

Thus, we may regard uni= valence as a generalized extensionality axiom for intensional Martin-L=C3= =B6f theories, as has been often emphasized.

Addit= ionally, in informal parlance, we often see propositional extensionality eq= uated with propositional univalence.

Let's cla= rify this, where we adopt X =3D Y as a notation for Id X Y:

<= /div>
=C2=A0* PropExt (propositional extensionality): For all propositi= ons P and Q, we have that

=C2=A0 =C2=A0 (P =E2=86= =92 Q) and (Q =E2=86=92 P) together imply P =3D Q.


=C2=A0* PropUniv (propositional univalence): For all propos= itions P and Q, the map=C2=A0

=C2=A0 =C2=A0 =C2=A0= idtoeq_{P,Q} : P =3D Q =E2=86=92 P =E2=89=83 Q

= =C2=A0 =C2=A0is an equivalence.

It is then clear t= hat PropUniv =E2=86=92 PropExt. However, the only way to get PropUniv from = PropExt that I know of requires function extensionality as an additional as= sumption. Let's record this as

=C2=A0 =C2=A0 -= PropUniv =E2=86=92 PropExt

=C2=A0 =C2=A0 - FunExt= =E2=86=92 (PropExt =E2=86=92 PropUniv).
=C2=A0
Obvious= question: does (PropExt=E2=86=92PropUniv) imply FunExt? I don't know.<= /div>

Less obvious question: Does any of propositional u= nivalence or propositional extensionality imply FunExt? That is, can we &qu= ot;linearize" the extensionality axioms as

= =C2=A0 =C2=A0UA =E2=86=92 PropUniv =E2=86=92 PropExt =E2=86=92 FunExt,

and, if not, less ambitiously as UA =E2=86=92 PropUniv= =E2=86=92 FunExt?

Even less obvious: is univalenc= e restricted to contractible types (call it ContrUniv) enough to get FunExt= ?

=C2=A0 =C2=A0UA =E2=86=92 PropUniv =E2=86=92 Con= trUniv =E2=86=92 FunExt?

Martin

------=_Part_601_1869109894.1508367523795-- ------=_Part_600_1843732532.1508367523795--