From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:adf:e387:: with SMTP id e7-v6mr414915wrm.9.1528313118181; Wed, 06 Jun 2018 12:25:18 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:f617:: with SMTP id w23-v6ls531649wmc.12.canary-gmail; Wed, 06 Jun 2018 12:25:17 -0700 (PDT) X-Received: by 2002:a1c:d8d:: with SMTP id 135-v6mr378051wmn.10.1528313117236; Wed, 06 Jun 2018 12:25:17 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1528313117; cv=none; d=google.com; s=arc-20160816; b=Ao6sn6C+Os967leMpyKQg8xv3145duA3Q6AJzlcf2Xc80vb6RlPu7WG2Xwvuo8Xviq cm8GDSfS+8qjM5m9kKXMAfR6yXS02Y5lKN12oK3KMwJTF+u82dxHXYDsAxSwnLey+USO c/pRo4WvVJdd94LD95bUZnXupviQ50Nc1o1/OhEJRyPidERfyXEkv1tWJ/tl5E0GFgND hZ8VXsm7XGrQWN3VcjTrLCiqzblN0o3FLeBdBlCA0WvsjbR8kUWNJFlmlYILxF4I1I/A VF8dNvBXTeFkotnkmWbhiNTOcDygwylZF7NroXtQUfMfVLmlbs9orpun40+i0BH0Fz4u WdoA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=user-agent:in-reply-to:content-disposition:mime-version:references :message-id:subject:cc:to:from:date:dkim-signature :arc-authentication-results; bh=Cztp0Jjgm24YMQ74s/fUhpf1J2WmWtsq8SPC4YEBzwU=; b=vr6lCrIm6HhofeRQSYIbd+ShnK2Flp+YgKHJHjv9xwklPHmOJGYyQzbCyxi5fWY/Pe 87NjVOlH1b5F6Gh/EjwmfNjpVVCbEZXuI0GlP8XjbqzAz9lJ+FJ9JKxtmymAOyQ/9m2p iBkdzV3wmsSMFwxsjvqMiyFvfBr9F8BO2LBB6HVFbKEJK1YYJ8UzrWhUPrVmiJZZjhlN MswnYXLtbD5ukMqwxKKZFczFEEjMLwkIypTT3pkomR2dx/vptmXNUG/AmBFlGoWDeAjZ 5EqRtT6o5MpPP2WKr0/O1IvW3ZJMV0WCUqanaObEWAX3bNzd/9GKRm7E1/anYQXQPE1M uF2g== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=ZwJwk8y1; spf=pass (google.com: domain of rwilli...@gmail.com designates 2a00:1450:4010:c07::232 as permitted sender) smtp.mailfrom=rwilli...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-lf0-x232.google.com (mail-lf0-x232.google.com. [2a00:1450:4010:c07::232]) by gmr-mx.google.com with ESMTPS id b8-v6si959790wrn.2.2018.06.06.12.25.17 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 06 Jun 2018 12:25:17 -0700 (PDT) Received-SPF: pass (google.com: domain of rwilli...@gmail.com designates 2a00:1450:4010:c07::232 as permitted sender) client-ip=2a00:1450:4010:c07::232; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=ZwJwk8y1; spf=pass (google.com: domain of rwilli...@gmail.com designates 2a00:1450:4010:c07::232 as permitted sender) smtp.mailfrom=rwilli...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-lf0-x232.google.com with SMTP id g21-v6so8867686lfb.4 for ; Wed, 06 Jun 2018 12:25:17 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:cc:subject:message-id:references:mime-version :content-disposition:in-reply-to:user-agent; bh=Cztp0Jjgm24YMQ74s/fUhpf1J2WmWtsq8SPC4YEBzwU=; b=ZwJwk8y12xRhamWKX2vE573ndh2o8ooKhq+wyNrqE7A+i78l52t42ZmUrpbbBc7khy Sj7gIr4rWUtml/PrVwUqLy7WavFfyREANtgLT76bKfPb5U/ReC25e5InSPEGdoJuODcK L+zRdKFWefjhSliDcdgfHD8ciwq4vCGUqGsJlTmzTK3nVnXsHiEeQhRkuy/rBiSf9QvY UQRIBWJsUQsc8UvCr2b5wA3MA5d76T4sspS0mn2JRI0BgcoaTyymqvuRqZFNXo7y119v /ItNQNAK7dFcj2pcmQKNBVV7RHwxUWJR6BmIyT/bnFrtH0X6qv5B+0MwhVc2jp97S8FV hNxQ== X-Gm-Message-State: APt69E3K2sw24RHtUFD9YhBN/K5sD/P+sOAFASxyrgq28taC83DhfjUe gCSeKkGjjIdSIrzAyY9JpQal2w== X-Received: by 2002:a19:c452:: with SMTP id u79-v6mr2575929lff.5.1528313116916; Wed, 06 Jun 2018 12:25:16 -0700 (PDT) Return-Path: Received: from localhost (109.247.202.84.customer.cdi.no. [84.202.247.109]) by smtp.gmail.com with ESMTPSA id j11-v6sm3298800lja.42.2018.06.06.12.25.15 (version=TLS1_2 cipher=ECDHE-RSA-CHACHA20-POLY1305 bits=256/256); Wed, 06 Jun 2018 12:25:15 -0700 (PDT) Date: Wed, 6 Jun 2018 21:25:14 +0200 From: Richard Williamson To: Thorsten Altenkirch Cc: Andrej Bauer , Alexander Kurz , "homotopyt...@googlegroups.com" Subject: Re: [HoTT] Re: Where is the problem with initiality? Message-ID: <20180606192514.GA818@richard.richard> 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> <20180605221223.GA3309@richard.richard> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: User-Agent: Mutt/1.9.5 (2018-04-13) > Actually I am teaching Python (by choice) Nice! > And second the untyped version is only the first step before I > understand what I am doing at which point I am able to make the > concepts involved more precise. Interesting! If I understood you correctly, I would say that I program in Python in the opposite way: I always have the types in my mind, and these guide the code, even though I do not write them down explicitly. In other words, I think that I program in the way as you have in mind in the following sentence, but there are benefits (flexibility, development time, etc) to me in writing the code in Python rather than in a statically typed language. > In particular in a mathematical development I would expect that > the objects involved are understood and hence can be given a > specific type. I like the following analogy... > Actually, Python is dynamically typed, which is why I always compare it to > set theory. Python has predicates to test wether an object belongs to an > arbitrary type. This corresponds to the element relation in set theory. In > contrast, strongly typed languages don't have predicates like this because > you know statically what the type of an object is. In the same way in Type > Theory typing is static hence it doesn't make sense to have an element > relation. ...and the following is also true... > I would think that once I understand the concepts involved in my > construction I should be able to assign static types to them. That is > certainly the case in programming but even more so for mathematical > constructions. ...but I disagree with the implied conclusion that one will always wish to write down those static types. Suppose I wish to formalise a quick argument involving words in a free group for instance. Does it really matter to me whether I am actually working in a free group? Maybe any group would do for my present purposes. Indeed, maybe any monoid would do. It is going to save me a lot of time, and give more flexibility with regard to how I incorporate my argument in a larger argument later, if I can just jump in and start manipulating those words without worrying yet about what type they have, even if I have a particular type, or more than one type, in mind. One might even argue that such a view is philosophically closer to much mathematical practise, especially that influenced by category theory: we are typically concerned with the properties of an object (what we can do with it), not exactly with what it is. To misappropriate the classic slogan: if it quacks like a free group, it might as well be a free group.