From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.0 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,HTML_MESSAGE,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 23276 invoked from network); 8 Oct 2022 23:42:01 -0000 Received: from mail-yb1-xb3b.google.com (2607:f8b0:4864:20::b3b) by inbox.vuxu.org with ESMTPUTF8; 8 Oct 2022 23:42:01 -0000 Received: by mail-yb1-xb3b.google.com with SMTP id e15-20020a25370f000000b006be3091eee2sf8007916yba.10 for ; Sat, 08 Oct 2022 16:42:01 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1665272520; cv=pass; d=google.com; s=arc-20160816; b=ipAFnVXO8c5GkN85aEYpxihSJRnQflSKajUwrzrq9AD7avyDbgabUdQBU+NKdJylOz JManzCjoyYpbEYY4yPYUl942owaskxdkIx3fzYYZVR7VNiiWFe7uVT9FyyWR1MUW0YRQ cde9SyBuLLBPFAEOpkxQTUfFabgh+rNsGYvPxOX2YFs9R8wc5RRXsEP1UE0R3D9RIb8S sNSFCy+qhYJR2A9m6DpuDxUna53nK0S2PPROuBsm47TjoZ764reuZiYrEP1UC8MoZUR+ 4nEuWJAS5gmLuayateYR1xZAweaSIdJmu+v5yi6ZgC+Fg5MA3t1IHadrSSukAIzokuqm llEg== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:sender:dkim-signature; bh=oLKhA4/lR/GF/NFwIQrGpcWQ+VlMFcXl6LyLjriGFjI=; b=bsEmIk2PedVZybpwlzv/MSL20621zCXa3aR1SiDasWWCQtXhgtmqcRavUXPTXgmPwd UNUI+LWLUyJg3SIvVW/iuyHL+Bc2Pe5Pqy3Dqa3balG4rDAwqWTGMrr9y3LKm9akZ2Cy F6qrCM8PyKk/Mh+rR0skrayK/gLqNUqvkjCY06CMJfumSq6LUbBqRknGSTqY4XwQNZe0 al+41CeWBBQl9LwNuu1xFV37QXAPAmjWlSQsnW7RTGh+L2PukjVA5U/Hz00itt0mnF0d 5Rm1YUZA+Z0Lweqs9boVRJIMmyRJEzK+83yThaC5tMbrd+Z65UiMkHgjkoP3/zQ79HnC emHQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego.edu header.s=google header.b=SZk81pcZ; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::1036 as permitted sender) smtp.mailfrom=shulman@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20210112; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:cc:to:subject:message-id:date:from:in-reply-to :references:mime-version:sender:from:to:cc:subject:date:message-id :reply-to; bh=oLKhA4/lR/GF/NFwIQrGpcWQ+VlMFcXl6LyLjriGFjI=; b=eOOrh7L8s7shy6AQXu5TVTHjg+6e05hhGY1FB8nXsQFR3Q2C6w3sBGtdwnRcZTNIER a6KgQLGJmxeMqFSz2xARNW+m0f13YNQiUlJXSvA5cSU//dSXtdzYSOavpS/CBhZ3+QQa uks9oE/P8QM4dcfwjns7QQ1sNsWSH6aJLfHX4rV2HyyFpupz9aDIW/uVaEGMYiSmBAub PWd+1w0lJrPYtc6RfxIRRnCapGqs8tNkkvlFlyHPndMOGlBtaDGZz++Y5Q1lZUiWUP30 N80+yUhynLUNIW1GaDdq68ViJ8+mNZxPTrVfwKFP7aFLeaQbFqX3csT88lCmMMu+BLkO fzGA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :x-spam-checked-in-group:list-id:mailing-list:precedence :x-original-authentication-results:x-original-sender:cc:to:subject :message-id:date:from:in-reply-to:references:mime-version :x-gm-message-state:sender:from:to:cc:subject:date:message-id :reply-to; bh=oLKhA4/lR/GF/NFwIQrGpcWQ+VlMFcXl6LyLjriGFjI=; b=WyDnuVOp529dYUmHuKJ/7Pwq3BRo2qX/nMdoqq6comEp3ha5aXbCxhOJrKsqhlA1eM F+t0PrrtQmySPBo1Zpml09MApbBTp305XumtGbGuSweEYqUNo3cJFmfwKPJgZvD53uQp noNXDFKvGFbinRj+CtEGsfjLoWGCigEL6kJue0vD+HVn/+doIseBFrOrDygapGdmn+c+ rFtbk4Wae2BdtWkmuc34l3cfIRn8A098WikFeJCordSiopiHWnkE6V4ot3XfEBPC6ZNA LMr9qKmTG5BxSmdgRoloIbBgxTRoSFXkpjHU/qveoiUsmOvGK2WNmv5/PfMY1z9O5LUg nkEg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ACrzQf1YS0ilXAnutymjczvVkRMDKQWGbVlfvbEPvt5r+sUUruRTFfyH 9Rxy46RaMsGfJXx1x9BEF/k= X-Google-Smtp-Source: AMsMyM4CFk+sAUHnPfdabP5T9WlZffpB+bXllpM9icxYDbTVbJXJ11lqYlYie8O6Ls2ub6KjFD86VA== X-Received: by 2002:a81:3884:0:b0:360:7830:f09f with SMTP id f126-20020a813884000000b003607830f09fmr4312963ywa.159.1665272519965; Sat, 08 Oct 2022 16:41:59 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a81:480c:0:b0:345:895d:35eb with SMTP id v12-20020a81480c000000b00345895d35ebls3257324ywa.2.-pod-prod-gmail; Sat, 08 Oct 2022 16:41:58 -0700 (PDT) X-Received: by 2002:a0d:ef84:0:b0:352:9e0d:a596 with SMTP id y126-20020a0def84000000b003529e0da596mr10493357ywe.347.1665272518612; Sat, 08 Oct 2022 16:41:58 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1665272518; cv=none; d=google.com; s=arc-20160816; b=Wj0x9p4nhED/giPBfzv3RDkyl0GIipBDoy/ngTqsI5h9CVVCF4l2+bRAPrlbI/5G69 Nfx9nB1GoVM1/SujuFTNpi5cpBb4HVA8TmWsQzbiPyJdx+LjsNUhrlUudsTmQsj81mK1 mtgthCggOJja2KRzG9IooeR24cUIXzcGqztSLUwJUjrcQCTaF+Xj/Dbdepf+L5A4ndwh cdfZ+clqE1KEoU2PxNGCX1yTRP9/3lZFMI1MSBDIcmrYckn9dY4p20CInKNW+G05Mw2X l4r3rxkitV8xvDlLVksF0RecHyudCxCXIc+e18r1MNf59QLZv/dCz36FikQZmsI4PlZf s9KA== 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; bh=m4rRa7EO6uPb9QsBE/nWl+3/1JSPdwY37Sm8IjjUzwg=; b=K0EvhGtQCgawHyn9dFx+n8cUyow0zsCrzPq8D5E7bbgm/LeymH7SjDTnu5LZlhljcc 7kvr9CZym90ZVC3ExP9ZCuwI/N5aP2/M5OWKap8M8Gx+pC5zz6wqXFt2HZtsoSp6u6Ye EkaVzOdjPgX63+lwsYXpQT7nl0RjqWuG7u4M1t3sMYriG2xkudw1ncfxd4OBReWxQAYS WGU32Y/5g7YFhaiE9MzmP4Z832EUyyfYmjKtWy4gbVsPPUM07tFrhkKaLvX9Z0V+mTCU CLG8myOqvX3bFWoiKgL9Qbb5EdFsFXmQreZXUUgVfqxqKmL6RpJ5L7nugXPL2Aj77GyW S/1g== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego.edu header.s=google header.b=SZk81pcZ; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::1036 as permitted sender) smtp.mailfrom=shulman@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu Received: from mail-pj1-x1036.google.com (mail-pj1-x1036.google.com. [2607:f8b0:4864:20::1036]) by gmr-mx.google.com with ESMTPS id a80-20020a25ca53000000b006bc9a3ce6e4si333436ybg.3.2022.10.08.16.41.58 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sat, 08 Oct 2022 16:41:58 -0700 (PDT) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::1036 as permitted sender) client-ip=2607:f8b0:4864:20::1036; Received: by mail-pj1-x1036.google.com with SMTP id g8-20020a17090a128800b0020c79f987ceso2427778pja.5 for ; Sat, 08 Oct 2022 16:41:58 -0700 (PDT) X-Received: by 2002:a17:90b:4f8a:b0:20c:9d98:13d1 with SMTP id qe10-20020a17090b4f8a00b0020c9d9813d1mr5707533pjb.245.1665272517772; Sat, 08 Oct 2022 16:41:57 -0700 (PDT) MIME-Version: 1.0 References: <3ff0b19b-0db2-4b63-b75d-3da9101a2f96n@googlegroups.com> In-Reply-To: <3ff0b19b-0db2-4b63-b75d-3da9101a2f96n@googlegroups.com> From: Michael Shulman Date: Sat, 8 Oct 2022 16:41:46 -0700 Message-ID: Subject: Re: [HoTT] Identity types of types, and univalence for the entire type theory To: Madeleine Birchfield Cc: Homotopy Type Theory Content-Type: multipart/alternative; boundary="000000000000e0670f05ea8e783d" X-Original-Sender: shulman@sandiego.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@sandiego.edu header.s=google header.b=SZk81pcZ; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::1036 as permitted sender) smtp.mailfrom=shulman@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , List-Unsubscribe: , --000000000000e0670f05ea8e783d Content-Type: text/plain; charset="UTF-8" It's tempting to think that one can define univalence without universes, but I don't think this rule makes sense: On Sat, Oct 8, 2022 at 6:59 AM Madeleine Birchfield < madeleinebirchfield@gmail.com> wrote: > The elimination rule says that given a judgment 'A type' in context Gamma, > a judgment 'B type' in context Gamma, a judgment 'C(p) type' in the context > 'Gamma, p : A = B', and a judgment 't:C(refl_A)' in the context 'Gamma', > one could form the conclusion 'J(t, p): C(p)' in the context 'Gamma' In the ordinary Id-elimination rule, the motive C has to be defined in the context of two *variable* elements of the type and an equality between them, not two *specific* elements. In particular, if A and B are specific types, then it doesn't make sense to substitute refl_A for p in C, because you can't substitute A for B. You can only substitute for a variable. I think in order to do something like this, you have to augment type theory by some kind of "polymorphism" that will allow you to hypothesize a "type variable" in the context. -- 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CADYavpwW0jL-EER%2BK3t7qs4_RegaB0CkZz6seMpRBw2SHGsr-Q%40mail.gmail.com. --000000000000e0670f05ea8e783d Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
It's tempting to think that one can define univalence = without universes, but I don't think this rule makes sense:

On Sat, Oct 8,= 2022 at 6:59 AM Madeleine Birchfield <madeleinebirchfield@gmail.com> wrote:
The elimination rule says that given a judgment 'A type' in context Ga= mma, a judgment 'B type' in context Gamma, a judgment 'C(p) type'= in the=20 context 'Gamma, p : A =3D B', and a judgment 't:C(refl_A)' = in the context=20 'Gamma', one could form the conclusion 'J(t, p): C(p)' in t= he context=20 'Gamma'

In the ordinary Id-eliminat= ion=20 rule, the motive C has to be defined in the context of two *variable*=20 elements of the type and an equality between them, not two *specific*=20 elements.=C2=A0 In particular, if A and B are specific types, then it doesn= 't make sense to substitute refl_A for p in C, because you can't=20 substitute A for B.=C2=A0 You can only substitute for a variable.

I think in order to do something like this, you have to augment type=20 theory by some kind of "polymorphism" that will allow you to hypo= thesize a "type variable" in the context.


=

--
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 = HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://g= roups.google.com/d/msgid/HomotopyTypeTheory/CADYavpwW0jL-EER%2BK3t7qs4_Rega= B0CkZz6seMpRBw2SHGsr-Q%40mail.gmail.com.
--000000000000e0670f05ea8e783d--