From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.0 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-ot1-x337.google.com (mail-ot1-x337.google.com [IPv6:2607:f8b0:4864:20::337]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 17763680 for ; Sun, 17 Feb 2019 12:13:24 +0000 (UTC) Received: by mail-ot1-x337.google.com with SMTP id c26sf12788045otl.19 for ; Sun, 17 Feb 2019 04:13:24 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:in-reply-to:references:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=TxRCQhl8RR/HxSG/uOKnDCQk4MaBQK/qQw0Zl68ljM8=; b=R830UIuMnAsJGPd9jxZH10XRPQT9SiZZZE3GPTYg5Pyr08OZKfWSmhrUzf+ktsxUQx ppUW5xyqnpAJTo0xIfqkd8bT5UJnOUFHj/noolNrl3R9kXK20tu6XwYdEHXncuQMVA+B 4TJsxZCL7S9AF0Wdht+qgepX1wlIXMUa4wAKf+S7zW3g5IPMPGbYBU+lps2VARsdzP/P cAf8SB0BY36ivkL+rwtbPvUZz1awGbUQLUw9dOEd6SADh2Z5NGKIpnm06HC8cK70W/7k nLAyJgwFQedPA206k3KdQbH9ohAyoE7NHOyfqDUIigDjInhh6VUSYgIs1ISyNwLpUHO9 v2CQ== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:in-reply-to:references:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=TxRCQhl8RR/HxSG/uOKnDCQk4MaBQK/qQw0Zl68ljM8=; b=lZbfCAJ2bjXE2Iu+BFWQHVYPtvpKrpk8GYzt7iBK8etO/wFGhun9rFyGnmr3sh0wLL FIGuCFsODuV51BFZ13omEnnIJ1aGJvAS+j4l29Ddqw7Y5hPLuRKHirY4x9egDK72IlGM nQk446UWtL8/Qy//2NUHqDJhjAfyW6iaOadHbrod5v93S6kZCpPwgZCml5NDDZ5QX1XB RBAzotnZ80pe3lvrYglPJlZP7/xWze2nX9hkMD+VodddxWYkBvkNe/+aT1tqTHTflq+V qJc0N4vCeGB3rpWbeMgpUZWS4vacDUY0GdfxZV7ZPCThqBh4d5NzxARfOhdWWVNxE+cY 04aQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:date:from:to:message-id:in-reply-to :references:subject:mime-version:x-original-sender:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=TxRCQhl8RR/HxSG/uOKnDCQk4MaBQK/qQw0Zl68ljM8=; b=mEgkLsCOftVJlcZ5ha1Zg5Ba1d1+pIC6OHNTiNzHnj1hdhFzqt56JLX02vjpyDGN64 ddE/ArrMIiy0MNwKbz0yZtKPpndY9z+Dt+VH8jBh5QORVI+W0sOZ/7TCZ9AaAAz3pTo3 iboYkAbpVYCZWPfJaPsY7KOGfX5HLDR0oafBx9leNxaCtq+WHjW18ARUZGh+oDAGD2/V mzr7dZNrWd6utOaKKrQ4PmDlgzFUaw/+/10L4Kqtj5Tsdh2RlqzqOqkvefT0OFw+Kq8K 68oI8WadNTejZ8xAELhoe55jtr5e2em77g2mZ8N38LtWP0BPtUlVwf6L6PI8WJq51PWg pzVw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuaIKfBfxFEo4Sg3qJGBtyeBAB2G0Fdxdaz++2CIu4Cl1D7kTHbV ybq86xW/rUKZ3RyCso+ZoWg= X-Google-Smtp-Source: AHgI3IYvyDHgsbggKGl3EM6Yy1yEwtO0HaGvcudfcIiUyTzROCy42w7TzSlJ+/ouff+gLP/Tb91Beg== X-Received: by 2002:aca:afc3:: with SMTP id y186mr172947oie.0.1550405603379; Sun, 17 Feb 2019 04:13:23 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:bbd6:: with SMTP id l205ls6279815oif.3.gmail; Sun, 17 Feb 2019 04:13:23 -0800 (PST) X-Received: by 2002:aca:afc3:: with SMTP id y186mr172943oie.0.1550405603092; Sun, 17 Feb 2019 04:13:23 -0800 (PST) Date: Sun, 17 Feb 2019 04:13:22 -0800 (PST) From: Matt Oliveri To: Homotopy Type Theory Message-Id: In-Reply-To: References: <6f42d617-be71-4ce2-89e2-8c9a27c178c9@googlegroups.com> <26028d40-d53c-48d0-a889-4b57fdb77e42@googlegroups.com> <8BC255D3-D1CB-4BC3-9EDE-342233AC177C@nottingham.ac.uk> Subject: Re: [HoTT] Re: Why do we need judgmental equality? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_258_979656347.1550405602394" X-Original-Sender: atmacen@gmail.com 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: , ------=_Part_258_979656347.1550405602394 Content-Type: multipart/alternative; boundary="----=_Part_259_962213107.1550405602394" ------=_Part_259_962213107.1550405602394 Content-Type: text/plain; charset="UTF-8" On Sunday, February 17, 2019 at 7:08:52 AM UTC-5, Matt Oliveri wrote: > > since the collection of elimination spines is countable externally. > Oh wait, I guess not. -- 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. For more options, visit https://groups.google.com/d/optout. ------=_Part_259_962213107.1550405602394 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
On Sunday, February 17, 2019 at 7:08:52 AM UTC-5, Matt Oli= veri wrote:
si= nce the collection of elimination spines is countable externally.
=

Oh wait, I guess not.

--
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.
For more options, visit http= s://groups.google.com/d/optout.
------=_Part_259_962213107.1550405602394-- ------=_Part_258_979656347.1550405602394--