From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.36.85.196 with SMTP id e187mr4671104itb.2.1468956604018; Tue, 19 Jul 2016 12:30:04 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.36.73.68 with SMTP id z65ls259255ita.21.gmail; Tue, 19 Jul 2016 12:30:03 -0700 (PDT) X-Received: by 10.67.14.70 with SMTP id fe6mr33580925pad.5.1468956603199; Tue, 19 Jul 2016 12:30:03 -0700 (PDT) Return-Path: Received: from exchange.sandiego.edu ([192.195.154.6]) by gmr-mx.google.com with ESMTPS id a133si1595168pfa.0.2016.07.19.12.30.03 for (version=TLS1 cipher=ECDHE-RSA-AES128-SHA bits=128/128); Tue, 19 Jul 2016 12:30:03 -0700 (PDT) Received-SPF: neutral (google.com: 192.195.154.6 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=192.195.154.6; Authentication-Results: gmr-mx.google.com; spf=neutral (google.com: 192.195.154.6 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: from mail-lf0-f41.google.com (10.0.26.241) by exchange.sandiego.edu (10.0.25.65) with Microsoft SMTP Server (TLS) id 14.3.294.0; Tue, 19 Jul 2016 12:30:01 -0700 Received: by mail-lf0-f41.google.com with SMTP id g62so22343523lfe.3 for ; Tue, 19 Jul 2016 12:30:01 -0700 (PDT) X-Gm-Message-State: ALyK8tJZl4+pO/wGx2iTuIXhRSjJ5Jo4sTKL/CYHyerRo0fe8FAr+KJui7v/nMNwVuyTK1VvaexzH0jK0+TfjQ== X-Received: by 10.25.143.137 with SMTP id r131mr1250985lfd.165.1468956599592; Tue, 19 Jul 2016 12:29:59 -0700 (PDT) MIME-Version: 1.0 Received: by 10.25.149.14 with HTTP; Tue, 19 Jul 2016 12:29:39 -0700 (PDT) In-Reply-To: References: <319FEA26-A1A5-42F2-9539-8B4635BFC016@ias.edu> From: Michael Shulman Date: Tue, 19 Jul 2016 16:29:39 -0300 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] FOMUS slides To: Vladimir Voevodsky CC: "HomotopyT...@googlegroups.com" Content-Type: text/plain; charset="UTF-8" Return-Path: shu...@sandiego.edu X-Originating-IP: [10.0.26.241] Okay, so then suppose I have e:Id0 T A B and R:P2. What is the type of transportb0 R e? On Tue, Jul 19, 2016 at 4:28 PM, Vladimir Voevodsky wrote: > Thank you for spotting this typo. It is supposed to be P_1. I have corrected the slides. > > >> On Jul 19, 2016, at 8:16 PM, Michael Shulman wrote: >> >> Can you explain the idea on the last slide a little more? Did you >> actually mean to say that R and "transportb0 R e" both have type P2, >> or should one of them have had type P1? If the latter, then how can >> we tell what type(s) "transportb0 R e" is allowed to have based on >> knowing the types of R and e? >> >> On Tue, Jul 19, 2016 at 2:18 PM, Vladimir Voevodsky wrote: >>> Hello, >>> >>> the slides of my FOMUS talk that have started the discussion about >>> equalities are now available at my website >>> https://www.math.ias.edu/vladimir/lectures . >>> >>> Vladimir. >>> >>> -- >>> 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 HomotopyTypeThe...@googlegroups.com. >>> For more options, visit https://groups.google.com/d/optout. >> >> -- >> 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 HomotopyTypeThe...@googlegroups.com. >> For more options, visit https://groups.google.com/d/optout. > > -- > 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 HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout.