From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.36.78.139 with SMTP id r133mr21003732ita.4.1514398426868; Wed, 27 Dec 2017 10:13:46 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.107.136.98 with SMTP id k95ls2574115iod.16.gmail; Wed, 27 Dec 2017 10:13:46 -0800 (PST) X-Received: by 10.107.205.77 with SMTP id d74mr22031211iog.57.1514398425991; Wed, 27 Dec 2017 10:13:45 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1514398425; cv=none; d=google.com; s=arc-20160816; b=aw56/d1d0/u5QnUmpbG+xWRRwxvNfrnnHYpO31vXYGFBhTsWcmApfx6mQskey1GoSI TrRNWFucPmeGzJNxVzt5BFNd81wXsT8NMJpa3eff8KJOZc6DopJQgYRGlU/JSoxWYJ7h 6tB3CEJ3tvINLj08mDi6LVRcXTKWfl5ct4vX8WkJ4vqOFSaNPNbOJgV2rvBs6QevuL+2 8CnL4erFWlI9zduQyJIsZ8d+JCNaf4xE/USUeXCU9sr4wspBBoPq3aBrgv3BYMyztww2 3pPAYQ61Y4Y12q36jt6wZFU+MuFADksaOsonU2cny3wFD60T7GERyFyke75ZdRJ51QUS VQ0g== 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:references:in-reply-to :mime-version:dkim-signature:arc-authentication-results; bh=IugFjhg0u+wOmUuoQsdIBTCpPwEBI2qMHDkkvxy/Fbs=; b=epyB78GHAOGT20DqbBA9HcoXtLyCE6M2MLlsR8L6kS0fbYwjpKEfFKE+bs81/KZeOl wLnisWNsUkjdmarKq+sVM6P0A1uahuvPCi6guauH22eMG9uoEnpuP4Lj1D+90caVFcQ3 MUnmf0dZe4oOPy05Q00VKFOGznIn6cFu8qBI/Hcp7tC1ayvjqkbnRGwiePl17K8iqwUA iHRJmQv/TX7djsQyAd8a0VxWQcXAEAZbBMk52zNpnkjXKwqkBtR8q7IeL0qC/VzjXdiX oE46ub6LOj8I+6FdjSiYIGsdKfKWYHareInucVetim6i+s78gtpiP58SxG75Pu2acVYZ iLpg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=Oe/dQjmM; spf=pass (google.com: domain of fpvd...@gmail.com designates 2607:f8b0:4001:c06::230 as permitted sender) smtp.mailfrom=fpvd...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-io0-x230.google.com (mail-io0-x230.google.com. [2607:f8b0:4001:c06::230]) by gmr-mx.google.com with ESMTPS id 138si1251201ite.2.2017.12.27.10.13.45 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 27 Dec 2017 10:13:45 -0800 (PST) Received-SPF: pass (google.com: domain of fpvd...@gmail.com designates 2607:f8b0:4001:c06::230 as permitted sender) client-ip=2607:f8b0:4001:c06::230; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=Oe/dQjmM; spf=pass (google.com: domain of fpvd...@gmail.com designates 2607:f8b0:4001:c06::230 as permitted sender) smtp.mailfrom=fpvd...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-io0-x230.google.com with SMTP id g70so23521440ioj.6 for ; Wed, 27 Dec 2017 10:13:45 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=IugFjhg0u+wOmUuoQsdIBTCpPwEBI2qMHDkkvxy/Fbs=; b=Oe/dQjmMbmhyPd6ZOuMq4jW9uLqXl+UF/vQbJvNpwkhNUqWa8xCz/fPAGkP1FABPyS A1QoX1SfTq8xArVJ81ToxTn93vnF/ALCQA/CadO2x0kKmaIXSzBsk6atGxgxEwLDvUwJ amad/F7HxqNK7JhIYUw38BUeBs/c+AWuHhAbz6JhH9jI+BTR9FAKZckVpWdoslsj58RD NrykceSv3IXdLL2L0A7ARQAgQntr0xvC0uHlifB80BB91FcIV76JBp261MozD6D/0BE4 YsKuoiVCfCaYXr06nzhul3SI/yfFnufraVHSZN2X4TBfskhrDvEN9Z6PHpgFXFKeU4Bx BpaA== X-Gm-Message-State: AKGB3mLbPZkZNxSD5qqdMGdFCykEYsCL1HZLlob2dxVcRm49mwdBnYcc rPkJ/47V38pjMoXHW1t3qkOIYkf7b9AgkR1Jf18qyw== X-Received: by 10.107.178.143 with SMTP id b137mr36354736iof.30.1514398425631; Wed, 27 Dec 2017 10:13:45 -0800 (PST) MIME-Version: 1.0 Received: by 10.2.163.154 with HTTP; Wed, 27 Dec 2017 10:13:25 -0800 (PST) In-Reply-To: References: From: Floris van Doorn Date: Wed, 27 Dec 2017 19:13:25 +0100 Message-ID: Subject: Re: [HoTT] HoTT in Lean 3 To: Michael Shulman Cc: Homotopy Type Theory , Jeremy Avigad , Gabriel Ebner , Rob Lewis Content-Type: multipart/alternative; boundary="001a114c9d803550520561565ca2" --001a114c9d803550520561565ca2 Content-Type: text/plain; charset="UTF-8" On 18 December 2017 at 08:04, Michael Shulman wrote: > It sounds like Lean > probably doesn't have this problem, i.e. if you define an inductive > *type* then it is always a type and never turns out to be a > proposition? Exactly. If you ask an inductive type to be in Type, it will never end up in Prop. If you want an inductive type to be in Prop, then you have to tell that explicitly. You can do that for any inductive declaration, but in the cases where singleton elimination doesn't hold, the generated induction principle will only eliminate to the universe Prop. --001a114c9d803550520561565ca2 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable

= On 18 December 2017 at 08:04, Michael Shulman <shu...@sandiego.edu&g= t; wrote:
It so= unds like Lean
probably doesn't have this problem, i.e. if you define an inductive
*type* then it is always a type and never turns out to be a
proposition?

Exactly. If you ask an inducti= ve type to be in Type, it will never end up in Prop. If you want an inducti= ve type to be in Prop, then you have to tell that explicitly. You can do th= at for any inductive declaration, but in the cases where singleton eliminat= ion doesn't hold, the generated induction principle will only eliminate= to the universe Prop.
--001a114c9d803550520561565ca2--