From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.129.131.70 with SMTP id t67mr23938320ywf.28.1468952218851; Tue, 19 Jul 2016 11:16:58 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.107.1.65 with SMTP id 62ls4214336iob.45.gmail; Tue, 19 Jul 2016 11:16:58 -0700 (PDT) X-Received: by 10.66.76.66 with SMTP id i2mr32090048paw.39.1468952218281; Tue, 19 Jul 2016 11:16:58 -0700 (PDT) Return-Path: Received: from exchange.sandiego.edu ([192.195.154.6]) by gmr-mx.google.com with ESMTPS id ph9si2143779pac.1.2016.07.19.11.16.58 for (version=TLS1 cipher=ECDHE-RSA-AES128-SHA bits=128/128); Tue, 19 Jul 2016 11:16:58 -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-f52.google.com (10.0.26.240) by exchange.sandiego.edu (10.0.25.65) with Microsoft SMTP Server (TLS) id 14.3.294.0; Tue, 19 Jul 2016 11:16:57 -0700 Received: by mail-lf0-f52.google.com with SMTP id b199so21198831lfe.0 for ; Tue, 19 Jul 2016 11:16:57 -0700 (PDT) X-Gm-Message-State: ALyK8tK8kj5oH9HLNRmOaOGPVenJ9vq3v6eeghs3i9W1F3HPE4kvmoeJttbNrEgqRUcaAittyd/GGynK8XuRDg== X-Received: by 10.25.143.137 with SMTP id r131mr985206lfd.165.1468952214842; Tue, 19 Jul 2016 11:16:54 -0700 (PDT) MIME-Version: 1.0 Received: by 10.25.149.14 with HTTP; Tue, 19 Jul 2016 11:16:35 -0700 (PDT) In-Reply-To: <319FEA26-A1A5-42F2-9539-8B4635BFC016@ias.edu> References: <319FEA26-A1A5-42F2-9539-8B4635BFC016@ias.edu> From: Michael Shulman Date: Tue, 19 Jul 2016 15:16:35 -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.240] 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.