From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a17:902:10c:: with SMTP id 12-v6mr5828247plb.5.1520586790811; Fri, 09 Mar 2018 01:13:10 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:902:aa03:: with SMTP id be3-v6ls2726785plb.2.gmail; Fri, 09 Mar 2018 01:13:09 -0800 (PST) X-Received: by 2002:a17:902:29e3:: with SMTP id h90-v6mr5965582plb.29.1520586789769; Fri, 09 Mar 2018 01:13:09 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1520586789; cv=none; d=google.com; s=arc-20160816; b=Xfd8YKUGJTE3dClpVAuNftyNhEC97Ev6WraR+b3cgZ2eK9Oti2stAYIIluW+DQGW43 DVGgS/ce0O0JlH9gKdCVZkkNQMDT8MvqmpE5PjnKF68ANpsUmFDPjvTUXM/Q3c+al2TX vQFofCwTmuD21A1xrRI+ATx+ZvHRD/ejMClmxoY5qSFDwUslmmZ7aDEtLw5JjumpAdI5 hWT1q0jEmMcaHfOZ2Aup16M7PWp2daQYAQq801jESbdx8TkQsnClN5Y8wCHPfzVESJWd wiiW7go1gDAlC1hhDG283EFAMNKDK8CFdXWMuJ1A/5s4upIj13XluDMCaF++pICAlTar +0Pw== 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=5oDERQUchlhIiPwU9SLw0vp6mQusVRmM7c/SN6iJ+ZE=; b=hvc65Pg6awG+nx/ptHa2HfrEImDBorrlPiq1+xXS1eC3Rjywr65AjFqbORNmsM0Tvz osdulAyyGzw4WhNbFMMV4tQK5JshTZKRGM2XZtBp4welQU9cQVLuZvQnHdOHSvcD/GeI aOsKZKOQPPS8i1ch/uSfrsKB/fwOPc07R5UzYrdDsBlNX3JnzuWhQMobEME2QaE1BG6V 3HaN3tLJ0fewJ39Lews8nQZnbGgdGt1EySnI2ribQunzlG690ExTKXoW5ukrsvP5uGG5 I9qY0BcuyzxpoZnvj7O2j1Uu5091DEmhj2jf6lWUTu5/kz9TvSWH8QSCcll8w1k+R8cK c/zA== 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 e70si42525pfb.4.2018.03.09.01.13.09 for (version=TLS1_1 cipher=ECDHE-RSA-AES128-SHA bits=128/128); Fri, 09 Mar 2018 01:13:09 -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 E599148000A3A; Fri, 9 Mar 2018 01:13:08 -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 9427148000A36; Fri, 9 Mar 2018 01:13:08 -0800 (PST) Received: by retrotexts.net (Postfix, from userid 1000) id 603A4860599; Fri, 9 Mar 2018 14:43:04 +0530 (IST) From: "N. Raghavendra" To: Jason Gross Cc: =?utf-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= , Homotopy Type Theory Subject: Re: [HoTT] Univalence from scratch In-Reply-To: (Jason Gross's message of "Fri, 09 Mar 2018 07:02:08 +0000") References: <7f3c276a-2d81-4235-8f2a-c4d82ea4f827@googlegroups.com> <87woylzvvt.fsf@hri.res.in> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.0.60 (gnu/linux) Reply-To: "N. Raghavendra" Date: Fri, 09 Mar 2018 14:43:04 +0530 Message-ID: <87tvtp1ujj.fsf@hri.res.in> MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable At 2018-03-09T07:02:08Z, Jason Gross wrote: > Raghu, perhaps you want > =C2=A0 Set Universe Polymorphism. > =C2=A0 Definition univalence@{U U'} : Type@{U'} :=3D forall X Y : Type@{U= }, > ... > or alternatively > =C2=A0 Universe U. > =C2=A0 Definition univalence :=3D forall X Y : Type@{U}, ... > ? Thanks, I'll try that. At present, I am working with a specified polymorphic universe =F0=9D=95=8C, and am using Definition univalences : =F0=9D=95=8C :=3D =E2=88=8F (X Y : =F0=9D=95=8C)= , .... Raghu. --=20 N. Raghavendra , http://www.retrotexts.net/ Harish-Chandra Research Institute, http://www.hri.res.in/