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-x33b.google.com (mail-ot1-x33b.google.com [IPv6:2607:f8b0:4864:20::33b]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 35698687 for ; Tue, 4 Jun 2019 20:50:50 +0000 (UTC) Received: by mail-ot1-x33b.google.com with SMTP id v1sf9960142otj.23 for ; Tue, 04 Jun 2019 13:50:49 -0700 (PDT) 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=iRuhkx6xKGmGEnEaFXXLSoHwzcuunfwkueFZ5ncTxXo=; b=aGq2jXGq4iJvXsdxjcRaZbB4bXu8Jw+CEK7gT99xSQzAs1n1e7sIlrUZOXjJorngce XgDyp23g0dUiKv9mM4pxXzluS7nhI6SakDfwI7s19tJ3AJ9e1xKdaGHSShfTkLFHwIiR KREL+DuexfmKcZd+i6fRanoc/n8HSYsbuWjTPB6hhPFTS1MUc5v/ufh+jL/AufpheRLs hp7+madPD+Kp/SvmDsMWLNZ3x3Tt0tAWsTMfZRTyZgQ5/sJu4GGzzjwcAeZqSXDV06Cy vTJ9ZyVLLJkzQbhXK63XR3TuOjSeDcWKHISMKaO4qGguNMOWzhrHxR2qtrKTz9jLJIIe zmdA== 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=iRuhkx6xKGmGEnEaFXXLSoHwzcuunfwkueFZ5ncTxXo=; b=P3iA9ZIwsp5E6aprHVAtHx7qYxAVt/zfkmXcSsSziqvXyRrwGT2YTZgzUN00yYrxgU aVkoZGrSalJDvT93h/nD/tG7FQSeJTP1dBqgxT8u0l6HzqCemIPQyvxRzve+A86Xyg8m x4sKbY28MQ/+S+As1I5lFuas5V3MUxU17KLy2uDCi953Vb53pgI90VuK5yLM7+HwfljQ /v3yC5TY8pdP2dv++LEnWnF2+TJDrSQI8J8/bQ2TKHNkQqh90EtdH3DlWsOLbtjlfBc6 Tyci1a+5+0Ryw7Dhq2Le0vX1mIbMPDu8NeIMMySqOwWQybEg8fihNeHkJnxunSNYeZmC 4m9Q== 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=iRuhkx6xKGmGEnEaFXXLSoHwzcuunfwkueFZ5ncTxXo=; b=XR1y07KCTQf/UqqShm3CWPs9JI64cumTYvIf4bW1lfwMgfSyrSY/rM7Oa+Z8v2ZhRF tF1zucMv/m9BYPqxmxO6MUb3Zt7lIUJ3sjuB2Ki7ZZy1UxwCRxXB29R6ckQEx+s1A4Ga bJLQGtn7SIj4tcg6mE0iwopjiXYxEQ67uwYDtDi53pCVIwjQuSgOM3WxzxSWkVquGosq ciqWnoJ7MhiSyXqUltlOyf8jf3Jf8lDoQh3u3vqowgmPPiuwWh4EojxM5oLIVySrrGbL Zg1D9lVL9TWcZbp7y3T9+JiJlcFPDipVzZeJ0lJNIlr16BRxegREpoZZzW3cibTyWY/B t1dg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAXfocB8etH4wF2gavjWEGQhI5UektJXdj++UvOFAFF+yl3iS7f8 uWn8PPTVx73E0OT7HmqnFNU= X-Google-Smtp-Source: APXvYqxmZ7IDsoBN8scAlY44JKwZQYaC1mDt+OYsscWF4Gb5JeTwe71Nqq5ZOIkRp6IBw328b8xnRw== X-Received: by 2002:a9d:3de6:: with SMTP id l93mr1678017otc.51.1559681448443; Tue, 04 Jun 2019 13:50:48 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:3e45:: with SMTP id h5ls23041otg.11.gmail; Tue, 04 Jun 2019 13:50:48 -0700 (PDT) X-Received: by 2002:a05:6830:1381:: with SMTP id d1mr6739841otq.144.1559681447781; Tue, 04 Jun 2019 13:50:47 -0700 (PDT) Date: Tue, 4 Jun 2019 13:50:47 -0700 (PDT) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: <209e2262-cb8a-4b31-9b6b-44a5df0185a5@googlegroups.com> In-Reply-To: References: <18681ec4-dc8d-42eb-b42b-b9a9f639d89e@googlegroups.com> <3f6331a7-688e-570b-01d8-d02a81eac96b@inria.fr> <9232f85a-6d64-84dc-a2d0-290c0fc6e760@cse.gu.se> Subject: Re: [HoTT] doing "all of pure mathematics" in type theory MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_2484_1472067334.1559681447206" X-Original-Sender: escardo.martin@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_2484_1472067334.1559681447206 Content-Type: multipart/alternative; boundary="----=_Part_2485_43529059.1559681447206" ------=_Part_2485_43529059.1559681447206 Content-Type: text/plain; charset="UTF-8" On Sunday, 2 June 2019 18:49:30 UTC+1, Kevin Buzzard wrote: > > The thing I know for sure is > that there are modern maths undergraduates who grew up with computer > games and who find the idea of turning their example sheet questions > into levels of a computer game quite appealing. > > I am surprised that Thorsten Altenkirch didn't manifest himself at this point. He uses to say that you can't teach old dogs new tricks. I am not sure it is the computer games (it could be, and if not they could anyway help, perhaps). I think it is their open minds. Martin -- 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. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/209e2262-cb8a-4b31-9b6b-44a5df0185a5%40googlegroups.com. For more options, visit https://groups.google.com/d/optout. ------=_Part_2485_43529059.1559681447206 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable


On Sunday, 2 June 2019 18:49:30 UTC+1, Kevin Buzza= rd wrote:
The thing I know for= sure is
that there are modern maths undergraduates who grew up with computer
games and who find the idea of turning their example sheet questions
into levels of a computer game quite appealing.


I am surprised that Thorsten Alten= kirch didn't manifest himself at this point. He uses to say that you ca= n't teach old dogs new tricks.=C2=A0

I am not = sure it is the computer games (it could be, and if not they could anyway he= lp, perhaps). I think it is their open minds.

Mart= in

--
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.
To view this discussion on the web visit https://groups.google.co= m/d/msgid/HomotopyTypeTheory/209e2262-cb8a-4b31-9b6b-44a5df0185a5%40googleg= roups.com.
For more options, visit http= s://groups.google.com/d/optout.
------=_Part_2485_43529059.1559681447206-- ------=_Part_2484_1472067334.1559681447206--