From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.55.23.165 with SMTP id 37mr19943205qkx.18.1520578940813; Thu, 08 Mar 2018 23:02:20 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.200.40.247 with SMTP id j52ls3570817qtj.9.gmail; Thu, 08 Mar 2018 23:02:20 -0800 (PST) X-Received: by 10.200.50.204 with SMTP id a12mr20735877qtb.39.1520578940157; Thu, 08 Mar 2018 23:02:20 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1520578940; cv=none; d=google.com; s=arc-20160816; b=q8gNHqnPdf0fjk0A4OR3OUKyO/IftOM942T8g62BUOqr2BUVhTDue2mAn0kXEgtO+k Nc5ns5JH0ru0IerafcFLtIaoXaceGoWFDKc9KOQob6mXzR8+DGkEqO+DCPt8faAEOqHG bN+2j+edTi/G2V2nRxQlizmspXvZL2t6xHlxxy+gcbQoH6EKp6jWSu2to+kWX1MoXnxB ToeLJTXB9AGFSGxGsftz4JjdSoo9GY2sVkkHCIM0SO08AQtIFwczyO2iRnMaUe0Vc/ok saZQSC9nqDFeqEu2cVHG9tuxiKWt8ewupEEeUgX8rrwPFn6mWkcIUovK//17oG8KTuMi HRAQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature:arc-authentication-results; bh=SsQ8Ln1bPOz+M1EqTslszxqSVoh7/xODWgqPjYMZ4tE=; b=zMJKKlKkHY0UWwogRXwkMsz6v800dXNlWO1LwDU+lyFGtP8KNiPSQ4Mkn/eK8WJ/fI rSgTEAkSTmfa8dT8FHNCvkWHpAH9QDPRttGRWvO5cMjTWc4g6ef6bol0PhKxhxXHbRds zSkgb8b8+OdnVv3bBKorcz1zXOouV4Kb0oDb73EGXRB5mnuzwCqdPJLv/GepbydIVg7B 3SUk4eRC+pQTu2j3o2QcoAepyi5YWVZSHokifyPXeqOUmLN3OB31M4MHNklTzfaXiv+L 5jLtlIIgTWTC2S9LRvH4ca+65SvJ0i24wOnhSPiye1jj13ypy4W7yJYZiz46qkzGZtZh 77hA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=ZgyXe3J7; spf=pass (google.com: domain of jason...@gmail.com designates 2607:f8b0:400d:c0d::234 as permitted sender) smtp.mailfrom=jason...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-qt0-x234.google.com (mail-qt0-x234.google.com. [2607:f8b0:400d:c0d::234]) by gmr-mx.google.com with ESMTPS id m16si30833qtn.0.2018.03.08.23.02.20 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 08 Mar 2018 23:02:20 -0800 (PST) Received-SPF: pass (google.com: domain of jason...@gmail.com designates 2607:f8b0:400d:c0d::234 as permitted sender) client-ip=2607:f8b0:400d:c0d::234; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=ZgyXe3J7; spf=pass (google.com: domain of jason...@gmail.com designates 2607:f8b0:400d:c0d::234 as permitted sender) smtp.mailfrom=jason...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-qt0-x234.google.com with SMTP id l25so9694498qtj.1 for ; Thu, 08 Mar 2018 23:02:20 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc; bh=SsQ8Ln1bPOz+M1EqTslszxqSVoh7/xODWgqPjYMZ4tE=; b=ZgyXe3J7a40Dwf3NFOSIEiktspYmShN7KYlmTGnVFx13BrLw4kFar5o6gaM7n+FaFe Uu71Ry9/sU5jnAaJifdLm2kyzKlfMWDZrmO908f+ZfTUUX12rqNqPJdfRQ/suOw62chE P9oojqzhquQuO+Dugv6Nn1b0CjTlIjS0m51+8qJSBvqFQOe+VeC0aWrLG+6Rsvc/OR4m uGITnS+5o2aZu4LYl5K8nAB2U208QRBFGrKVPTIifBlucYksELxRqFaca/PRhqVlXHid VK+Rug8wqajROa+wwFqnzBSu/n53KU/DpB4B+FlD+zwkMN49xWzQYxxv0wingr7Hkh5r Cjjg== X-Gm-Message-State: AElRT7EuBvXguplIWFl3lMQgNrq8CVQgcM7b2++MlVGy8e9YQfJZOndn htNCAKhlJXG/MiumDAL2vBd2cVHaY/3oJRtBZysEpw== X-Received: by 10.200.80.78 with SMTP id h14mr43743253qtm.211.1520578939782; Thu, 08 Mar 2018 23:02:19 -0800 (PST) MIME-Version: 1.0 References: <7f3c276a-2d81-4235-8f2a-c4d82ea4f827@googlegroups.com> <87woylzvvt.fsf@hri.res.in> In-Reply-To: <87woylzvvt.fsf@hri.res.in> From: Jason Gross Date: Fri, 09 Mar 2018 07:02:08 +0000 Message-ID: Subject: Re: [HoTT] Univalence from scratch To: "N. Raghavendra" Cc: =?UTF-8?B?TWFydMOtbiBIw7Z0emVsIEVzY2FyZMOz?= , Homotopy Type Theory Content-Type: multipart/alternative; boundary="f4f5e8097a988f08f10566f55f4e" --f4f5e8097a988f08f10566f55f4e Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Raghu, perhaps you want Set Universe Polymorphism. Definition univalence@{U U'} : Type@{U'} :=3D forall X Y : Type@{U}, ... or alternatively Universe U. Definition univalence :=3D forall X Y : Type@{U}, ... ? On Fri, Mar 9, 2018 at 12:00 AM N. Raghavendra wrote: > At 2018-03-07T13:10:53-08:00, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 wrote: > > > This also has an ancillary Agda file with univalence defined from > > scratch (without the use of any library at all). Perhaps somebody > > should add a Coq "version from scratch" of this. > > I have kept my attempt at a Coq version at > > http://www.retrotexts.net/just-univalence/toc.html > > However, I don't know how to define the univalence of a universe in Coq, > that is, I don't know what to write for foo and bar in > > Definition univalence (U : foo) : bar :=3D baz. > > Remarks are welcome. > > Raghu. > > -- > N. Raghavendra , http://www.retrotexts.net/ > Harish-Chandra Research Institute, http://www.hri.res.in/ > > -- > 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 HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. > --f4f5e8097a988f08f10566f55f4e Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Raghu, perhaps you want
= =C2=A0 Set Universe Polymorphism.
=C2=A0 Definition univalence@{U = U'} : Type@{U'} :=3D forall X Y : Type@{U}, ...
or alterna= tively
=C2=A0 Universe U.
=C2=A0 Definition univalence := =3D forall X Y : Type@{U}, ...
?

On Fri, Mar 9, 2018 at 12:00 AM N. Raghavendra <ra...@hri.res.in> wrote:
At 2018-03-07T13:10:53-08:00, Mart=C3=ADn H=C3= =B6tzel Escard=C3=B3 wrote:

> This also has an ancillary Agda file with univalence defined from
> scratch (without the use of any library at all). Perhaps somebody
> should add a Coq "version from scratch" of this.

I have kept my attempt at a Coq version at

=C2=A0 http://www.retrotexts.net/just-univalence= /toc.html

However, I don't know how to define the univalence of a universe in Coq= ,
that is, I don't know what to write for foo and bar in

=C2=A0 Definition univalence (U : foo) : bar :=3D baz.

Remarks are welcome.

Raghu.

--
N. Raghavendra <ra= ...@hri.res.in>, http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTypeThe...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
--f4f5e8097a988f08f10566f55f4e--