From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:adf:c707:: with SMTP id k7-v6mr248104wrg.18.1527687018123; Wed, 30 May 2018 06:30:18 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:6e11:: with SMTP id j17-v6ls6530273wmc.10.canary-gmail; Wed, 30 May 2018 06:30:17 -0700 (PDT) X-Received: by 2002:a1c:ec42:: with SMTP id k63-v6mr201213wmh.29.1527687017274; Wed, 30 May 2018 06:30:17 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1527687017; cv=none; d=google.com; s=arc-20160816; b=SkQxEuh55TPjXNS0VoRRUZqRou0ZDdkcfEdm/7S4yOC0Iwk1IbgQ56kXu2T+dLMdqC WLDjY9DbLQYCYhZICceX7t9A7N/YBuo8ASnLTBp15Xfwrwg9j4ItoimKIGiyDXS1ywTp EUllYlLNWxnCjriPwpFvH7HsMH8YWvtde2En4Xd+xFCyNHODasSAoCcW4zfdS+4E1RDJ xzC4TqavHgV1FqfvE+WUE6y8CYhzGyujm0tUofvRpQQioVxwCK6JVO9SiIgS9FAjp3RS xPmw1h0Tbsky3nOX4J4eDvU8nzMTNe/cMSv4VZBkI7wl+wH+7e8/A68NQnCOcHpjVU/i hFOw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=date:in-reply-to:references:subject:content-transfer-encoding :mime-version:to:from:message-id:dkim-signature :arc-authentication-results; bh=zoMNKhwj1nId5feoPKrYL2g31p439umQ5tYMRUWzFmE=; b=Dcq0rnxBbmHQY1iHOVoSF7qDlTe5EVDppdNtlMOCiTPXoQ2LOlctvbz5huu/XCO7kp aPd8PfOLzbKhRRC/CiphvY4AavVy74vZ4ifm8QmYvYf+Mq2G4GkcJfnI+LOC+VRb3Joe 84JLdrx+Tky2ezRCYvMLgxNvcRpCS4w5D0wbd0JOUbB4sgut2yZdO1alKeYrBd0O2e4x QCTwG+3J4tanZ51nyMEuV0aQu29Gs4aLBM9Tr3zXBGSkheKuBIBJ0aXD1QXs420GKbcs DoBcW2h7QvnKCHy+W/91WgAXNsQUjHD25lyThGS88sScc8h/hPbZeVFMiSrT4llEe7z3 KXVw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@messagingengine.com header.s=fm2 header.b=ddObxhJS; spf=neutral (google.com: 66.111.4.25 is neither permitted nor denied by best guess record for domain of j...@jonmsterling.com) smtp.mailfrom=j...@jonmsterling.com Return-Path: Received: from out1-smtp.messagingengine.com (out1-smtp.messagingengine.com. [66.111.4.25]) by gmr-mx.google.com with ESMTPS id o4-v6si425174wrm.1.2018.05.30.06.30.16 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 30 May 2018 06:30:17 -0700 (PDT) Received-SPF: neutral (google.com: 66.111.4.25 is neither permitted nor denied by best guess record for domain of j...@jonmsterling.com) client-ip=66.111.4.25; Authentication-Results: gmr-mx.google.com; dkim=pass head...@messagingengine.com header.s=fm2 header.b=ddObxhJS; spf=neutral (google.com: 66.111.4.25 is neither permitted nor denied by best guess record for domain of j...@jonmsterling.com) smtp.mailfrom=j...@jonmsterling.com Received: from compute2.internal (compute2.nyi.internal [10.202.2.42]) by mailout.nyi.internal (Postfix) with ESMTP id E799D21E67 for ; Wed, 30 May 2018 09:30:15 -0400 (EDT) Received: from web2 ([10.202.2.212]) by compute2.internal (MEProxy); Wed, 30 May 2018 09:30:15 -0400 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d= messagingengine.com; h=content-transfer-encoding:content-type :date:from:in-reply-to:message-id:mime-version:references :subject:to:x-me-sender:x-me-sender:x-sasl-enc; s=fm2; bh=zoMNKh wj1nId5feoPKrYL2g31p439umQ5tYMRUWzFmE=; b=ddObxhJSxdAtvsPbj7yD/Q Mvul7VBuJFIk2B50R4DKQAj/s1JlfeO6ASCUCT+Vre2bVajII281+eDWxo8ux4vO G2ntMIjtw6zrj49iEoGrT+HuhZs98hYjXgQRZJi4n2XVaLPQbhO9myjKqtbLF8/Z lC57ojnG0K0nmHUdPwie4akYJV2neBEEKAp4mIg5b73vecfg3O87m20gaCDKcRba k4ZK0n2mFLHM8TLpcPBZoLZmJDFRplCsxAXRGPZUvmDhDeKj7JUQwCUBR5f0ZY/3 PtabFMzm9TIoTmcA1vDc3KX3WJmcK7ydvY+e6if9RXGB6iMzxsRn2u7vCenldK+A == X-ME-Proxy: X-ME-Proxy: X-ME-Proxy: X-ME-Proxy: X-ME-Proxy: X-ME-Proxy: X-ME-Sender: Received: by mailuser.nyi.internal (Postfix, from userid 99) id 898AA621DC; Wed, 30 May 2018 09:30:15 -0400 (EDT) Message-Id: <1527687015.373472.1390433112.7C19BE52@webmail.messagingengine.com> From: Jon Sterling To: HomotopyTypeTheory@googlegroups.com MIME-Version: 1.0 Content-Transfer-Encoding: 7bit Content-Type: text/plain; charset="utf-8" X-Mailer: MessagingEngine.com Webmail Interface - ajax-397f98d6 Subject: Re: [HoTT] Re: Where is the problem with initiality? References: <06B9C5AB-C7CB-4CB5-B951-64E0C4180AD9@exmail.nottingham.ac.uk> <20180530093331.GA28365@mathematik.tu-darmstadt.de> <5559377C-94C9-422E-BBF7-A07AFA4B7D04@exmail.nottingham.ac.uk> <3D1D292E-1EFF-4EA2-8233-B55FDA5CE8A5@gmail.com> In-Reply-To: <3D1D292E-1EFF-4EA2-8233-B55FDA5CE8A5@gmail.com> Date: Wed, 30 May 2018 06:30:15 -0700 I fear that this veers off topic---but let me say that this is hardly a serious problem for structural / typed foundations, considering the fact that you can always embed an untyped mathematical universe into a typed one in an easy way (for instance, using Aczel's interpretation of constructive set theory into type theory), whereas it is much harder to move in the other direction without inheriting the pathologies of set theory. With that said, maybe we can get back to the original question. Where really is the problem with initiality? As Thomas said, the problem surely does not at all lie in the difference between "human syntax" and syntax based on categorical gadgets (it's easy to see that these are the same). Returning to Thomas's email about M_a and M_s (lindenbaum-tarski model), it sounds as if the problem has almost nothing to do with initiality at all, if the hard part is really to show that M_s is a model at all. Am I misunderstanding Thomas's email? On Wed, May 30, 2018, at 3:53 AM, Alexander Kurz wrote: > > > > On 30 May 2018, at 10:37, Thorsten Altenkirch wrote: > > > > On 30/05/2018, 10:33, "Thomas Streicher" wrote: > > > > That categorical syntax and ordinary syntax are isomorphic is just a > > purely syntactic result allowing one to replace correct algebraic > > syntax by one more accessible for the human mind. > > > > For the human mind accustomed to the separation of collections and predicates as present in conventional Mathematics. > > I think the problem is not just one of being accustomed or not. > > It is crucial that informal mathematics is untyped. The untypedness is > what makes it flexible enough for practical purposes. Formalising > mathematics in a proof assistant is hard work. And to a large extent > this is due to the fact that everything has to be typed. > > If we ever want to get mathematicians to use proof assistants as > casually as they use latex, the problem of untyped vs typed mathematics > needs to be solved. > > Alexander > > > > > > > > > > > > > > > This message and any attachment are intended solely for the addressee > > and may contain confidential information. If you have received this > > message in error, please contact the sender and delete the email and > > attachment. > > > > Any views or opinions expressed by the author of this email do not > > necessarily reflect the views of the University of Nottingham. Email > > communications with the University of Nottingham may be monitored > > where permitted by law. > > > > > > > > > > -- > > 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.