From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Fri, 8 Dec 2017 16:27:15 -0800 (PST) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: In-Reply-To: <86619505-c082-4c11-8d5d-9159e1b351ec@googlegroups.com> References: <29b10ce3-682b-437b-bd45-fdf7b2763cec@googlegroups.com> <6570d6a7-2d41-475e-aa7f-b9dc318e74a6@googlegroups.com> <86619505-c082-4c11-8d5d-9159e1b351ec@googlegroups.com> Subject: Re: [HoTT] Yet another characterization of univalence MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_6781_1513252073.1512779236071" ------=_Part_6781_1513252073.1512779236071 Content-Type: multipart/alternative; boundary="----=_Part_6782_183215237.1512779236072" ------=_Part_6782_183215237.1512779236072 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable On Friday, 1 December 2017 14:53:25 UTC, Mart=C3=ADn H=C3=B6tzel Escard=C3= =B3 wrote: > > > OK. Here is a further weakening of the hypotheses. It suffices to have > funext (again) and that the map > > idtofun{B}{C} : A=3DB =E2=86=92 (A=E2=86=92B) > > is left-cancellable (that is, idtofun p =3D idtofun q =E2=86=92 p=3Dq). > > Univalence gives that this is an embedding, which is stronger than > saying that it is left-cancellable. And also K gives that this is an > embedding. > > I've written this down here in Agda=20 : http://www.cs.bham.ac.uk/~mhe/yoneda/yoneda.html (updating a 2015 development) * This is self-contained (doesn't use any library). * A main feature is that instead of J (or pattern maching on refl), this= =20 uses the Yoneda machinery everywhere instead (regretably with just one=20 exception (I'd be grateful for suggestions of how to get rid of this use of= =20 J)). A syntactical novelty is a new notation for universes in Agda closer to the= =20 notation in the HoTT book for informal mathematics in type theory. This=20 could be further improved by making it built-in in Agda (as explained in=20 the imported NonStandardUniverseNotation.lagda), but probably it is good=20 enough without any modification to Agda. Martin =20 ------=_Part_6782_183215237.1512779236072 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
On Friday, 1 December 2017 14:53:25 UTC, Mart=C3=ADn H=C3= =B6tzel Escard=C3=B3 wrote:

=C2=A0OK. Here is a further weakening of= the hypotheses. It suffices to have
funext (again) and that the = map

=C2=A0 =C2=A0 idtofun{B}{C} : A=3DB =E2=86=92 = (A=E2=86=92B)

is left-cancellable (that is, idtofu= n p =3D idtofun q =E2=86=92 p=3Dq).

Univalence giv= es that this is an embedding, which is stronger than
saying that = it is left-cancellable. And also K gives that this is an
embeddin= g.


I've writ= ten this down here in Agda :=C2=A0=C2=A0http://www.cs.bham.ac.uk/~mhe/yoned= a/yoneda.html

(updating a 2015 development)
<= div>
=C2=A0 * This is self-contained (doesn't use any lib= rary).
=C2=A0 * A main feature is that instead of J (or pattern m= aching on refl), this uses the Yoneda machinery everywhere instead (regreta= bly with just one exception (I'd be grateful for suggestions of how to = get rid of this use of J)).

A syntactical novelty = is a new notation for universes in Agda closer to the notation in the HoTT = book for informal mathematics in type theory. This could be further improve= d by making it built-in in Agda (as explained in the imported NonStandardUn= iverseNotation.lagda), but probably it is good enough without any modificat= ion to Agda.

Martin

=C2= =A0=C2=A0
------=_Part_6782_183215237.1512779236072-- ------=_Part_6781_1513252073.1512779236071--