From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.129.241.7 with SMTP id h7mr13029532ywm.34.1520571613768; Thu, 08 Mar 2018 21:00:13 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.13.212.209 with SMTP id w200ls352914ywd.24.gmail; Thu, 08 Mar 2018 21:00:12 -0800 (PST) X-Received: by 10.129.130.67 with SMTP id s64mr12745004ywf.145.1520571612963; Thu, 08 Mar 2018 21:00:12 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1520571612; cv=none; d=google.com; s=arc-20160816; b=LhTC5f8HyARICsDtVVxiX3g+IDokmK6L/ghTxL4tSpWl2z4TbmFY6QCabfjdEknUb/ NHGe9MPJAKhwzdUgUwVJbHUzgZ01heTiwh0WIXz0MCFe7zoJz38UNdQL0CR6xy/z2lbf sa4Q0lFlZ3DSS5LF7IcVapYYE0cEudCu3IJ11mOcLVsPNht9QpSqo6plLczzpYGsw959 X+GzLT9XzwUBOm2yWCktCuJX1omrO+UToZC3m445i7KaDpNDDoM5/lgGrZgFoiDlJNlN 7d61tJ9Sm2hzWTohXzCFQ6EL59OYk/TPU5OMsFMXS3NEZeF9ab8Gl5hedh8jYJSpTII8 mz8Q== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:mime-version:message-id:date:reply-to :user-agent:references:in-reply-to:subject:cc:to:from :arc-authentication-results; bh=iH08KwJ6pNGagjEy52NmC/H+YNJc4t1su8PDPWypCeo=; b=oOykpfDPEUIEEuKfypTNi+uYFG+eGgGoG6sokD2YlYz3IFnVI4fxDdRJdc1nHll4ZE SlKoR195GtnoZP9GfTnK0CsMdIpRep8Tq9HrS1cJ2QYBYPIg/LNJIefRNqiBBNySkz2e PE4hTA6mk1i9GPXme97vtiR+hZCaGpuGucZj+sHbHf/bIruuPWaUPCFL0FrifGp2oooV ZLzjMMIdXkGEiyKw/tFpAD3Q030d5Wmdf9Py3Dtl8FW7aGh8XLFsC723ZclS4gOvTG1Q W0cJk06AVP6z2Uv+2DWst+ci/pFk0mcBzl4oeWoO+Awde+f0Ac5zFQeJxhoGCBZpds7+ ywKg== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of ra...@retrotexts.net designates 208.113.200.129 as permitted sender) smtp.mailfrom=ra...@retrotexts.net Return-Path: Received: from homiemail-a114.g.dreamhost.com (sub5.mail.dreamhost.com. [208.113.200.129]) by gmr-mx.google.com with ESMTPS id v8si11777ywg.3.2018.03.08.21.00.12 for (version=TLS1_1 cipher=ECDHE-RSA-AES128-SHA bits=128/128); Thu, 08 Mar 2018 21:00:12 -0800 (PST) Received-SPF: pass (google.com: domain of ra...@retrotexts.net designates 208.113.200.129 as permitted sender) client-ip=208.113.200.129; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of ra...@retrotexts.net designates 208.113.200.129 as permitted sender) smtp.mailfrom=ra...@retrotexts.net Received: from homiemail-a114.g.dreamhost.com (localhost [127.0.0.1]) by homiemail-a114.g.dreamhost.com (Postfix) with ESMTP id 4A43348000A39; Thu, 8 Mar 2018 21:00:11 -0800 (PST) Received: from retrotexts.net (unknown [14.139.59.140]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) (Authenticated sender: ra...@retrotexts.net) by homiemail-a114.g.dreamhost.com (Postfix) with ESMTPSA id EFAFB48000A2F; Thu, 8 Mar 2018 21:00:10 -0800 (PST) Received: by retrotexts.net (Postfix, from userid 1000) id 00AFC2400323; Fri, 9 Mar 2018 10:30:06 +0530 (IST) From: "N. Raghavendra" To: =?utf-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= Cc: Homotopy Type Theory Subject: Re: [HoTT] Univalence from scratch In-Reply-To: <7f3c276a-2d81-4235-8f2a-c4d82ea4f827@googlegroups.com> (=?utf-8?Q?=22Mart=C3=ADn________H=C3=B6tzel_Escard=C3=B3=22's?= message of "Wed, 7 Mar 2018 13:10:53 -0800 (PST)") References: <7f3c276a-2d81-4235-8f2a-c4d82ea4f827@googlegroups.com> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.0.60 (gnu/linux) Reply-To: "N. Raghavendra" Date: Fri, 09 Mar 2018 10:30:06 +0530 Message-ID: <87woylzvvt.fsf@hri.res.in> MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable 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/