From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.202.48.6 with SMTP id w6mr8516502oiw.107.1508848854049; Tue, 24 Oct 2017 05:40:54 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.43.195 with SMTP id u61ls39688ota.1.gmail; Tue, 24 Oct 2017 05:40:53 -0700 (PDT) X-Received: by 10.157.81.50 with SMTP id c47mr9091582oth.119.1508848853224; Tue, 24 Oct 2017 05:40:53 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1508848853; cv=none; d=google.com; s=arc-20160816; b=JbS4LCND9USlF5m8BrbY8XSIhE+5UsKpPytNeDKalg9tvBazxtmYHv5RI1xKjBRYOp PIZIZs9+EM7bBaR0IzNGQUY1gPWsQnU+jxh3TISnfYji/43wCoPhP0TrDmjshuCdCqSn pTsnqLqJUALKKKdEDCTEONHPO8/P7PJzxtfwBq1UYecnAQo/FEGuMC2UEVwR1obdTUbV QMcHHVFXPXHR5zRKbKm4Nl5nyZHJZtw7B7WYoFS2j7iwG0O9b10CyQGomHDdXOhSpnqN aIcYpS/0NFylO2xoEzHeoJknoyVxOYh+6lFXNhc6kXQHvFpfLSd1JW3DMqf3m1uJVETf vUBA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :references:in-reply-to:reply-to:mime-version:dkim-signature :arc-authentication-results; bh=Rf32q81cGB7azcosoHdMs7M7DVk0THJc5ddSUg8efTI=; b=031/8BECWDSsauISwbDTltxPm9WBwxEr6OW2mYEMajHPyt1333IyL0taMybVdute/I 9gIiFc3MwxuJw+1rAXzFN4cMtD2ME7o3zIi2N5G9zQwhcI0aTacwEdbCwhYdA9NCqSmK 8LwXDxU76lmWILlVYHoflkOfi0+mr3nqOMz69fq3FveGSIEeMn3rDCjz1D7qQJHEv4kT m/WZcDvYfzvJ26FB/qQznAT0BuJM30MRdBdOYbiiY4TA0YIECABwwlarOVQGgENReFD0 tJfw/cP8fCkTXMBCCXO4oIyIvcYUvm3IK5HMUmz5Gp7TUI4Wc+eUO7eRFZWj6wOZgras spgg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=K0lH4em7; spf=pass (google.com: domain of hub...@gmail.com designates 2607:f8b0:400e:c05::234 as permitted sender) smtp.mailfrom=hub...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-pg0-x234.google.com (mail-pg0-x234.google.com. [2607:f8b0:400e:c05::234]) by gmr-mx.google.com with ESMTPS id t9si14683ote.1.2017.10.24.05.40.53 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 24 Oct 2017 05:40:53 -0700 (PDT) Received-SPF: pass (google.com: domain of hub...@gmail.com designates 2607:f8b0:400e:c05::234 as permitted sender) client-ip=2607:f8b0:400e:c05::234; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=K0lH4em7; spf=pass (google.com: domain of hub...@gmail.com designates 2607:f8b0:400e:c05::234 as permitted sender) smtp.mailfrom=hub...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-pg0-x234.google.com with SMTP id s75so14408752pgs.0 for ; Tue, 24 Oct 2017 05:40:53 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:reply-to:in-reply-to:references:from:date:message-id :subject:to:cc:content-transfer-encoding; bh=Rf32q81cGB7azcosoHdMs7M7DVk0THJc5ddSUg8efTI=; b=K0lH4em7X4fYuPYEI77XmDHAvmeiMiqnnfPdc1OQIEoF7AG5VgEl96kU9RoQCIGRz8 51PikuHbin87pyS5HJhO3BXIF4692vkeSpqWHyFZd81BOuk38vtd0WPhMaf+oXIG30BP d8MyH2ThMrqr27+BBDg1FpBKYpjodIFxSkGCRj7RaNO4c4vHDeVmG6f2x5tFakBtjfCU FsroLSMNojhDzXV9nffXVrtz3WMtxqMEfhMJaRbRkrBcJtYNO5bzmjhFQIAbzKbvFL6a kZFAo6zKmrR7U/GuclGwbzjQAVvK3BCU9/P3v3CEDWJS4gBV0pFd6vvJSyAVAC66wouj RaNw== X-Gm-Message-State: AMCzsaXsu/c4fBZsgA2ExQSIdol4f29e3f+ZhVrmAiD7ratjdjQIHhBa Dh8qY6BwscriztzPO+aTG+/rHKiuE00i9wAJNVIv1w== X-Received: by 10.99.184.25 with SMTP id p25mr14231714pge.180.1508848852759; Tue, 24 Oct 2017 05:40:52 -0700 (PDT) MIME-Version: 1.0 Received: by 10.100.160.130 with HTTP; Tue, 24 Oct 2017 05:40:52 -0700 (PDT) Reply-To: hub...@gmail.com In-Reply-To: References: From: Simon Huber Date: Tue, 24 Oct 2017 14:40:52 +0200 Message-ID: Subject: Re: [HoTT] Definition of semantic composition in CCHM cubical type theory To: jas...@cs.washington.edu Cc: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Hi Jasper, On Tue, Oct 24, 2017 at 6:10 AM, wrote: > Then down in the interpretation from syntax (bottom of p.22, top of p.23)= , > we define the interpretation of comp as > [[=CE=93; comp i A [=CF=95 =E2=86=92 u] a0]]=CF=81 =3D comp El [[=CE=93,i= :II;A]] (I, j, =CF=81=E2=80=B2 , [[=CE=93; =CF=95]]=CF=81, > [[=CE=93, =CF=95, i: II; u]]=CF=81=E2=80=B2 , [[=CE=93; a0]]=CF=81) > using =CF=81=E2=80=B2 =3D (=CF=81 s_j , i =3D j), supposedly in =CE=93(I,= j). We have =CF=81 =E2=88=88 [[=CE=93]](I) and > s_j : I, j =E2=86=92 I is the inclusion. > > I don't understand how to read =CF=81=E2=80=B2 =3D (=CF=81 s_j , i =3D j)= . Where does i come from, > and what does it mean to set =CF=81=E2=80=B2 to be a pair of =CF=81 s_j a= nd the substitution i > =3D j? I think, we have El [[=CE=93,i:II;A]] in Ty([[=CE=93,i:II]]), so w= e expect =CF=81=E2=80=B2 in > [[=CE=93,i:II]](I, i), so =CF=81=E2=80=B2 is a pair of [[=CE=93]](I, i) a= nd II(I, i), so i guess we > have =CF=81 s_j in [[=CE=93]](I, i) and i =3D j in II(I, i)? > > As I was writing this I think I made some progress, but I still don't > understand what it means to have i =3D j in II(I, i). > Does it have anything to do with the other place =CF=81=E2=80=B2 is used= , in [[=CE=93, =CF=95, i: > II; u]]=CF=81=E2=80=B2 ? You are right, this is not quite right and a typo--it should be: =CF=81' =3D (=CF=81 s_j, j). (=CF=81' should be an element of [[=CE=93, i : II]](I,j).) Cheers, Simon