From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a17:90a:558a:: with SMTP id c10mr16691917pji.53.1589119326722; Sun, 10 May 2020 07:02:06 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a63:4383:: with SMTP id q125ls2813462pga.7.gmail; Sun, 10 May 2020 07:02:05 -0700 (PDT) X-Received: by 2002:a62:1651:: with SMTP id 78mr11883564pfw.106.1589119324972; Sun, 10 May 2020 07:02:04 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1589119324; cv=none; d=google.com; s=arc-20160816; b=aWY2OY3f2gMc4KrcVAnE9D9yN1dcchtRw3QCKXvnTivjRayssa50MB8sZYhec/WCM4 muuAG/A5GtjqXMAQKwYQQzV7MVJwaolTqKeYKPaVvfSr3qSO2ZfvlX/PMrCKawsqAj/I +NAURrsO1sZOna8S/PfVy/JzoHe/cMfySmyv/z+7vXbbum1CXWIbeIfQKMmcPvyDJSok hpQZ5dmlPJeK1NERsZS51KqF2wAJLwhm23lMqTMNjve1gPe0Rgk/gv/hd00rEOPS6zj9 173bicaQtv/TKbN/umVaD9JSkoydcXV2CabNCnJd3LEqeO23/6vmdtPEuNuNqybXv6jJ 1ClQ== 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=GwAqyE6VqgNUOZweC4xqY47H5dvNPQ8Mnydx8LwE2eU=; b=Up7FY7yvZMDxzQSBkHreAjiMWrO4eqITmahWdajSVnMqAWmNR0msvp1SlP8qvg98ZD LAJQLLJ8AcHTgHx1ShswADqkxnIJ8gfg8dJh2lGVfBtw500PlpSSUOUnoFV97SzqxhTz RI353vPkqZ7WBt2tQDMJcWnUkQMBcZKPqS+TJG0+pm1WKLt48rRyES8jYatfH/hdZ6rk 0Hv/wwj/7Mkm7FacqBakX7ydMjsvkr+bIYyed3dH2auyBagjL9Dskd3b7eRAK/QN+mbt OCbEilIVQVgu8g+iZ3sxRu4gGTqSK9v/rWsLOyhRK8bzWXPCHJknu5a8QmytSoAzT3Q1 FL8Q== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=hkMixJ5I; spf=pass (google.com: domain of shu...@sandiego.edu designates 2607:f8b0:4864:20::32e as permitted sender) smtp.mailfrom=shu...@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu Return-Path: Received: from mail-ot1-x32e.google.com (mail-ot1-x32e.google.com. [2607:f8b0:4864:20::32e]) by gmr-mx.google.com with ESMTPS id u131si523341pfc.6.2020.05.10.07.02.04 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 10 May 2020 07:02:04 -0700 (PDT) Received-SPF: pass (google.com: domain of shu...@sandiego.edu designates 2607:f8b0:4864:20::32e as permitted sender) client-ip=2607:f8b0:4864:20::32e; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=hkMixJ5I; spf=pass (google.com: domain of shu...@sandiego.edu designates 2607:f8b0:4864:20::32e as permitted sender) smtp.mailfrom=shu...@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu Received: by mail-ot1-x32e.google.com with SMTP id j4so5414582otr.11 for ; Sun, 10 May 2020 07:02:04 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=sandiego-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc; bh=GwAqyE6VqgNUOZweC4xqY47H5dvNPQ8Mnydx8LwE2eU=; b=hkMixJ5I5N7R7G+hfGE8IgJ52Yu1RNyqmDcf4GYG1x3GpqLsZDMEmG1qUhPc1dxUhf R+kV2eqf+L5XknMEmYQt2ZLpCJ9ftE3CGJIviBtaAwHrPgBMGFSXTCAqpqVlJXiOiGhB sz6rAJ/iwpNTS+lgxWo2MAIPSxeP7dj2WkTG7g3pFIHH4T7XnZ0BJBjORPw/RbJWEyZf hxCqce7jB9pOYlJiI4AX/5PwWj/javRVP8+4Yave1sXr5a1DABW9f+Ll/pJP1FYNNDHs esbbH0fsAY7hbBiPRNJIA45o+TreKnKcIaPdkdzUAtgGpLijn2Vvu0ffsqPduLUMBNqx idnQ== X-Gm-Message-State: AGi0PuY1ykyy8BOW+pd6FpUQC4QZEjWDD2M7deBS9LKQyv8LdH8RPwdo duptTRurd2wfA4A/I7xzX+2cyBLTlz7S0+y8k4SdUAuZe7A5VK+cUa1DD7G/BlkULIeGahjOK3Q c1cBzSf5Wcg/ZdO6+HTuohNdh5FGJ/CymnpiOkuP/j9dUuyzD8V9koVt2nlW4zl8GAARkb1Apu7 pqlHzVWj4Y X-Received: by 2002:a9d:170e:: with SMTP id i14mr9549326ota.283.1589119323995; Sun, 10 May 2020 07:02:03 -0700 (PDT) Return-Path: Received: from mail-oi1-f180.google.com (mail-oi1-f180.google.com. [209.85.167.180]) by smtp.gmail.com with ESMTPSA id j2sm1922363ota.28.2020.05.10.07.02.03 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 10 May 2020 07:02:03 -0700 (PDT) Received: by mail-oi1-f180.google.com with SMTP id o24so12865267oic.0 for ; Sun, 10 May 2020 07:02:03 -0700 (PDT) X-Received: by 2002:aca:ea05:: with SMTP id i5mr17320229oih.44.1589119323251; Sun, 10 May 2020 07:02:03 -0700 (PDT) MIME-Version: 1.0 References: <67E9DCCA-F9CA-45B7-9AC8-E5A7E94FE9A9@nottingham.ac.uk> <20200507100930.GA9390@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F5334@Pli.gst.uqam.ca> <8C57894C7413F04A98DDF5629FEC90B1652F53A3@Pli.gst.uqam.ca> <20200508064039.GC21473@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F54CC@Pli.gst.uqam.ca> <20200509082829.GA8417@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F55C8@Pli.gst.uqam.ca> <20200509184313.GB28841@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F563A@Pli.gst.uqam.ca> <154D1B4B-6881-4269-8BA1-1CE8EBB0BE0D@nottingham.ac.uk> In-Reply-To: <154D1B4B-6881-4269-8BA1-1CE8EBB0BE0D@nottingham.ac.uk> From: Michael Shulman Date: Sun, 10 May 2020 07:01:51 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Identity versus equality To: Thorsten Altenkirch Cc: Jon Sterling , "'Martin Escardo' via Homotopy Type Theory" Content-Type: text/plain; charset="UTF-8" On Sun, May 10, 2020 at 4:46 AM Thorsten Altenkirch wrote: > Defining simplicial types isn't entirely straightforward (as you know I suppose), because Delta is not directed. We can do semi-simplicial types as a Reedy limit, i.e. an infinite Sigma type We can certainly *talk* about simplicial types in 2LTT as exofunctors from the exocategory Delta to the exocategory Type. I assume the point you're making is that we don't have a (fibrant) *type of* simplicial types, whereas we do have a fibrant type of semisimplicial types (under appropriate axioms)? > You need some extra principles, e.g. that strict Nat is fibrant or maybe better that certain coinductive types exist. Personally, I think the best axiom to use here is that exo-Nat is *cofibrant*, i.e. Pi-types with domain exo-Nat preserve fibrancy. We don't know how to model "exo-Nat is fibrant" in all higher toposes, but it's easy to interpret "exo-Nat is cofibrant" in such models, since Pi-types with domain exo-Nat are just externally-infinite products.