From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a0c:9dea:: with SMTP id p42-v6mr3204817qvf.27.1527765001277; Thu, 31 May 2018 04:10:01 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a37:49c2:: with SMTP id w185-v6ls19892118qka.8.gmail; Thu, 31 May 2018 04:10:00 -0700 (PDT) X-Received: by 2002:a37:4a8b:: with SMTP id x133-v6mr3410025qka.39.1527765000673; Thu, 31 May 2018 04:10:00 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1527765000; cv=none; d=google.com; s=arc-20160816; b=WW72Ei18WQSKIsFggNwu5szXpXB2Sn0GlfvSDvRK/V4PU+mCch8/O2nqo4EfmOhrT0 nRBqrlfUPzJsAo7AJNoMhLIseneQvv2CJcmZiI1CoTC6AiQXGXttEQYEAxXhrQuHbxON SiRgWzS3F1KDlkbtVBNp9bnblSLzkvwZhfv0ZTXvIfO6n+hoF4hhl2DDLMlSnrBhZNUz uWyu1PlSXToB8R4exsuh3NB1hMF8zrtJrTJlIF07aiAPqi5TnBVnBDpLot+XsoswGMjt M67T2a9k5tx6ItiKSjkNs26aegFOqNKoAJSDNF738bVYt4hbfou28QNT2iOTFDNOKk64 PJ7g== 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:mime-version:dkim-signature :arc-authentication-results; bh=2nxHEVxd9NRikSdKXoGyD7A/q4M1kyIHm7cJVJiOl/M=; b=lblsZsQIcQ/B4yXL/Bl0LDHbEPrNoFLP03PS5oT2uGpgzNjjwQtVK+q+Ds++MINoyd 40TGQCGByfHTch9P9Sx74VHxk6maplt2AdnHB7gLCdaPOG7lkR1f9VTgRKh0lxeSzyGO ERR1WbmXMz0a75tM+XIXIO4iwpLrZWjQcIX4UWDEvEdAihBHpE/aixKXlJY7zfgXKAav lPNB0ICYNkvgxr2jQhxvesqBIlRp7YX2Gm4LdyNHA66VJ1VSnX4ZqDMd2DOgDuk27loa Ch4aZFfEj4fRE8fba6lzy3LNCxLikWPcy2ly+aFV/z4fjjU2LR8g67GX7vojBGrYwjyQ KBKw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=w2AVlw2n; spf=neutral (google.com: 2607:f8b0:4002:c05::232 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-yw0-x232.google.com (mail-yw0-x232.google.com. [2607:f8b0:4002:c05::232]) by gmr-mx.google.com with ESMTPS id j1-v6si1153403qkk.2.2018.05.31.04.10.00 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 31 May 2018 04:10:00 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c05::232 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4002:c05::232; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=w2AVlw2n; spf=neutral (google.com: 2607:f8b0:4002:c05::232 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-yw0-x232.google.com with SMTP id 81-v6so3415047ywb.6 for ; Thu, 31 May 2018 04:10:00 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=sandiego-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-transfer-encoding; bh=2nxHEVxd9NRikSdKXoGyD7A/q4M1kyIHm7cJVJiOl/M=; b=w2AVlw2nlE+vYScq5qHZh0zCIWpTdApOTrbQ3732XSDmc5WLm2w7sKfBUVJnEzVOMF qMulB0znXb2c/yWhwLYCFqO/kRf4jiE1NqHpHbg29qXR5qRGUX8UUeI4UQTO/R0PTQmU 4GkiroxuzHdMpddl4L0i9duWLBEiuTNEftBM7JwdjPnVcRjdDgSCik0zfUvG3d6VzEpU 44YYcndlQY2AkpJR07teGPEY4aujkVrBEwAGPSWsnyjyD8P8Frjn+DQwJ6H0LZZ5Y2Bl aa+3jjFEl1FUxBsIXoLm3qgHfb9Z/iK0AWe3YwTxbspWnB/vepJ99Gr85tU/zgq35Ju5 E+vQ== X-Gm-Message-State: ALKqPwe/T6LR52vGocGtCE3/VCF1b9WxXmyBhE5gmNM7vItif3FdPMHQ Gl7BFFtTKT5B4RaXsi0Y1wt74Lln X-Received: by 2002:a0d:e849:: with SMTP id r70-v6mr3469988ywe.482.1527765000183; Thu, 31 May 2018 04:10:00 -0700 (PDT) Return-Path: Received: from mail-yw0-f179.google.com (mail-yw0-f179.google.com. [209.85.161.179]) by smtp.gmail.com with ESMTPSA id x127-v6sm7833387ywa.19.2018.05.31.04.09.59 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 31 May 2018 04:09:59 -0700 (PDT) Received: by mail-yw0-f179.google.com with SMTP id j190-v6so6916619ywe.4 for ; Thu, 31 May 2018 04:09:59 -0700 (PDT) X-Received: by 2002:a81:38d6:: with SMTP id f205-v6mr3339516ywa.63.1527764999451; Thu, 31 May 2018 04:09:59 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:a25:d2ce:0:0:0:0:0 with HTTP; Thu, 31 May 2018 04:09:39 -0700 (PDT) In-Reply-To: <433eba9a-1d5b-43ce-a266-64d2f6b10047@googlegroups.com> References: <1527602447.1037774.1389070656.2CE32C72@webmail.messagingengine.com> <433eba9a-1d5b-43ce-a266-64d2f6b10047@googlegroups.com> From: Michael Shulman Date: Thu, 31 May 2018 04:09:39 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Re: Where is the problem with initiality? To: =?UTF-8?B?TWFydMOtbiBIw7Z0emVsIEVzY2FyZMOz?= Cc: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On Thu, May 31, 2018 at 3:48 AM, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 wrote: > Is the > study of type theories mature enough to admit a general definition of a t= ype > theory, of which the ones we are looking at are a particular case? Well, we won't know whether it is unless we try. Various of the people working on the initiality theorem are approaching it by way of formulating such definitions, either syntactically (collections of rules) or semantically (structure on a CwF). And I spoke about another class of general definitions-in-progress in my own HoTTEST talk (jww Dan Licata and Mitchell Riley).