From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) 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,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE, T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.4 Received: from mail-wm1-x33f.google.com (mail-wm1-x33f.google.com [IPv6:2a00:1450:4864:20::33f]) by inbox.vuxu.org (Postfix) with ESMTP id AA6FA24B4D for ; Mon, 12 Feb 2024 12:12:03 +0100 (CET) Received: by mail-wm1-x33f.google.com with SMTP id 5b1f17b1804b1-40fb74433ebsf20339875e9.3 for ; Mon, 12 Feb 2024 03:12:03 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1707736322; cv=pass; d=google.com; s=arc-20160816; b=CBq0QSrWAjvF4+WyaSONE/SHCF+mfvjqJn6QCo9LmeJj4bjtZqhmdmhCHGtJXL0Ptj kmnY2hiEecwUbEn9pJrdTm65hC61xeYPBjXTWDFBbIZbhyNPzgaHHttKW5vuamX9GCMZ +4QOO6jrz99ypSXKb5rHWzyGTZv4Zh/yOsocYUlFg6wIrBjL1tMaSQBMYau3ElmleWoM 30VwD6CZxb5nauZhds0Hq95gWxgAO0AnijijfNdiop+gSLwr9ueqN7O28r3RLh4+4+mz VvW8b7yT/nC/z9sjn4HAUJj+YXicmgVcKvF5K1vPE/9X4t3IzGWingl4G53DmXGcrdqM 70MQ== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:subject:from:cc:to:content-language :user-agent:mime-version:date:message-id:sender:dkim-signature :dkim-signature; bh=FtWF95LipmwNmmZ0ukdRvOjfSB3jZXTF3bs2qArjuMk=; fh=v2tKs/UNbvbznS/EJTmT/Ubg+CREpS3kikEAqEjQRLQ=; b=0tJDzS5P+lZK5jZ0X7V91LO1b++1xnKeSmEx1rF9MakgyFe3FKcRtTzg2Cwbq3IbjI 0J+c9pmVRHzY2/OPrta9QmebbIITAyUZbLsQ3eoecvJINeaR+x8V8Q35YfwgabW4rLWD ZA/53X9rni0ZNXgO/EudXdotIz55OBpaYqceL5vzskltgMLj01iuD+jGwvdciNwt2gct NfjWXOVYoESG0bWY1k9GbiGFWjpAJllk90VhRxU8VS/mJTIQzNBMtUDQjZqODu4OiXMq /k8E2Lkr02G3LWeOo6PXRIEgpugWj+etlZa/lHYhNz3UWA+3ksT0/HGiWNIZoQUpH7LG TdMw==; darn=inbox.vuxu.org ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20230601 header.b=gFSMwacj; spf=pass (google.com: domain of escardo.martin@gmail.com designates 2a00:1450:4864:20::32a as permitted sender) smtp.mailfrom=escardo.martin@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20230601; t=1707736322; x=1708341122; darn=inbox.vuxu.org; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:x-original-authentication-results :x-original-sender:subject:from:cc:to:content-language:user-agent :mime-version:date:message-id:sender:from:to:cc:subject:date :message-id:reply-to; bh=FtWF95LipmwNmmZ0ukdRvOjfSB3jZXTF3bs2qArjuMk=; b=KddKTDql2mX+qBI4zpvTagb1ekvxKaoMoouzDSYKEAXkf+jrtos310hdbLO+De/yNU +qmtGUph2KStpFXoDI3JaVzFP9XGQezivS31/vVPxogNJnbPb3DOZfLqkDbmUtSWyKOX EyE2rFJEH1RV3ymWoIwkzXdpv1XWTGkCqFkdL8o9ZrsfI8Lfd35VQXYdks+aGRLbJsTO jaqMAwzaMhN1iPDzCTOmUZG2TVW4W2CdFwKTgK43Hz5+9VcqE3fgxrdyYw22/qAS/agN wWLK+AwaKVpK5WxJ2VT9VXEPt/yv3jG/AKKkgTXcv8WicT5F+CAkT6XrxkyDd/T3CFu6 dcRA== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20230601; t=1707736322; x=1708341122; darn=inbox.vuxu.org; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:x-original-authentication-results :x-original-sender:subject:from:cc:to:content-language:user-agent :mime-version:date:message-id:from:to:cc:subject:date:message-id :reply-to; bh=FtWF95LipmwNmmZ0ukdRvOjfSB3jZXTF3bs2qArjuMk=; b=iZTqLu/BELcBGdvRdDAMebaUAU8yttCcvi5EGeC9yS1xb9fgrSCLXw92fBGtGJNUhJ mb2Z591BbWr/LN3FVIpZNu2cIlrUJ6rhhXE2Vj7+zyLsE+5o833TA17WSuNEjQkWioA3 H768QJAy3qTMpjWYAnq0ZguMFBWTHhEoTCuUxdcmwulJPMqBXsl0UuD1Cyv/6+z+SR5E thTKi4Tp1tDGIn4SWvniVWQMHtSmmdkzlroBvn/ASoHYw59q7ZJMAEWoCvHiy6NIxfOn IlckOrtJY4iW3afieAASAobLxUGLsLHzHdZ8GVbme0Ndx9oi98ZmGcKJ843tu7ZZY47F XR3Q== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1707736322; x=1708341122; h=list-unsubscribe:list-archive:list-help:list-post :x-spam-checked-in-group:list-id:mailing-list:precedence :x-original-authentication-results:x-original-sender:subject:from:cc :to:content-language:user-agent:mime-version:date:message-id :x-beenthere:x-gm-message-state:sender:from:to:cc:subject:date :message-id:reply-to; bh=FtWF95LipmwNmmZ0ukdRvOjfSB3jZXTF3bs2qArjuMk=; b=OOkWW46Z3J/QhRzL6aVntkOAk3QNKtZKChphEpNDvrptysy5PvXzpoMOGAqI5MO0mN 7TReILV2nvO8JK5Dy2CNCdsZsB+jl9TsDBHdVk5qwvWa0ODLLUuxK9KsOYg+Us/hrTKi oTAys1SBh/1osiSzZK7l0cXRkidXoqy1noa/zF130e/NUa1uAdoQ1vpY7Sv0kKg/KRds NG/a4KTv1YMvDN/Xck3CMAP2kZCRfoQWhooRfwjgQjB1iAcxGLze3ck4mDgzgcOvlIzD Y0+xcHz1Uk92k3AIImRj+UJXN3AiJHxl5B9sZesu8/o0J8MwTnDwwcppI361f4/A11Lp RYew== Sender: homotopytypetheory@googlegroups.com X-Forwarded-Encrypted: i=2; AJvYcCVSEYtNmN2ygtMXkzyTkbmFLoR0fzXs8YocMOc+PBWTVhC+5kmKV/dNWFADQGDv7wcsXXUy6zq+XFsdJSRMttYMMg== X-Gm-Message-State: AOJu0YwbGi8+hCZGvIsGKWoFGKvywbocWFDnv8kK905e7muKDwlxngh0 8aSXs0n3w5L7lte9NxWRz8WFPQpjbWK01J/M/npGrs7D8BCa3kh+ X-Google-Smtp-Source: AGHT+IEiFOEmpH0N+82ENmL1P3XYC1Rp7v3wCZMbsuNiFJ4UQ8Q5njGvRBYqKpHYEmkFhRElcARveA== X-Received: by 2002:a05:600c:3505:b0:40f:be08:9457 with SMTP id h5-20020a05600c350500b0040fbe089457mr5318616wmq.19.1707736322259; Mon, 12 Feb 2024 03:12:02 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:600c:3d8e:b0:410:eede:6b4b with SMTP id bi14-20020a05600c3d8e00b00410eede6b4bls105837wmb.2.-pod-prod-03-eu; Mon, 12 Feb 2024 03:11:59 -0800 (PST) X-Forwarded-Encrypted: i=2; AJvYcCXf+k0c8E7wBaSCw9y6blOXDpq6rWWhbPDvBjr22h+9GED2UmeV3CxcAkJZWiBNATAXMNOvvkoY70ImaG74Vbp1aGT5qNIYpG3OXg1Wyhb41dNE3g== X-Received: by 2002:a05:600c:4f85:b0:410:78fb:c00c with SMTP id n5-20020a05600c4f8500b0041078fbc00cmr5480456wmq.4.1707736319323; Mon, 12 Feb 2024 03:11:59 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1707736319; cv=none; d=google.com; s=arc-20160816; b=NEpIP+UOKj/NpmBYRt8WNvv7hvpn0uKqFsW8bUMIOKqdADau+OLQbzf3czgl1czWqa T8nRhitCggGglweiMdgyUwohuvbylmXT447RUf1OOZ6XozSuUApANUirAK++iv2QSr6P cYuSNIZUIaXyEhYHg9/DO0PlEdOooa8W5Ec0J2csFCwAujTn9eJ9sFnS8WetuYOrKxWQ Z8UdQAZ1utx2Lc8beWEP/KQYzuMgb68z6ShYNrDb9z+feWNd0+im1YGMRsswAhHOPcv6 OSJkChhy75gNveRP/dTewk31Um1PWwth3GD9NqhD/mtiF3QSZGoeKwIwS3Mh/kFPBR2X Okmw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:subject:from:cc:to:content-language :user-agent:mime-version:date:message-id:dkim-signature; bh=/OZntfJVg7RYnSY2Z0s8+R2bzP/snqtyvvdZD4k0rVg=; fh=E7VMIlfpMEYVMOIVZ73VGkwZS2HkkC/QQsMSotCKbZI=; b=NfmBI3T1MWWRL8Av59jewHr0fiWfoh2NogRUsmdKEvpIkZJg4o+e9j+MM54gwWLOFA alOo+nS25hNWf9tu92+0q19dreYIeQ7uO3OfHTTPDNlXm/J64mKOP39BWJSHAPiVpEx0 0AWo+++cx7jw9Z29T86Y7B5Lc7CpCskiOCdYap7GiTLHB4MT0k9V8K5pWtYTfreGQRkg kwTyFYMHjk9DITef7kIOc9O/ceB2GZrza89O7kB774ajnS87Qfg4EDifxgifDW+owDPP BZh5omItP9gCadQwLKhiC/3Wii0bKH8XWdpDhXkCBCLVRj5D0tCV2wjwWxV/qDdjCusW jNlw==; dara=google.com ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20230601 header.b=gFSMwacj; spf=pass (google.com: domain of escardo.martin@gmail.com designates 2a00:1450:4864:20::32a as permitted sender) smtp.mailfrom=escardo.martin@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com X-Forwarded-Encrypted: i=1; AJvYcCWQtXtYJFLU65ZOqSVe9JDshe1RH9peSGVybk1vbY6eqP6RR9uVpGpuhaqCSEh44Ov9u3Y+w8BctyQmJ4S7ql6vvFo/XWDaYYyfSMd8VFjtbbNJcg== Received: from mail-wm1-x32a.google.com (mail-wm1-x32a.google.com. [2a00:1450:4864:20::32a]) by gmr-mx.google.com with ESMTPS id cm2-20020a5d5f42000000b0033b1589d9c3si337577wrb.0.2024.02.12.03.11.59 (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 12 Feb 2024 03:11:59 -0800 (PST) Received-SPF: pass (google.com: domain of escardo.martin@gmail.com designates 2a00:1450:4864:20::32a as permitted sender) client-ip=2a00:1450:4864:20::32a; Received: by mail-wm1-x32a.google.com with SMTP id 5b1f17b1804b1-410cb9315f6so6351195e9.2; Mon, 12 Feb 2024 03:11:59 -0800 (PST) X-Forwarded-Encrypted: i=1; AJvYcCV15pYh2CB3/IdILN9v2uNZCj46aw7STN49yiWgEXC3B5IGgTsgvUBDgeTR39wtbVnnJ0RxUy4YUptzSQVPLT2VKXVhNtuUJKFWPUkGGgb3TF+Q1Q== X-Received: by 2002:a05:600c:4f0e:b0:40f:dd91:2d06 with SMTP id l14-20020a05600c4f0e00b0040fdd912d06mr4985235wmq.32.1707736318338; Mon, 12 Feb 2024 03:11:58 -0800 (PST) X-Forwarded-Encrypted: i=1; AJvYcCVrUXRMaCh2+5UjUKGtTkg0rNHjKdcjRMR7oB+vgOQr4cVhzG7WAffYncZtBpTb/dsaJFM1M5qOYTXwZWWlG52/NKQWdV5oQrcz1Jt+hLhBe1ubBh9+tkqiMG/c+kgFuwqRyiZ9g5vn2pN+XOiTIFYrcydhL0TARbpusg6ns7lWdPQ= Received: from [192.168.0.30] ([88.97.50.0]) by smtp.gmail.com with ESMTPSA id 20-20020a05600c22d400b00410ae5e443asm1173745wmg.1.2024.02.12.03.11.57 (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 12 Feb 2024 03:11:57 -0800 (PST) Message-ID: <31b22711-e7da-49e0-9738-a2571912f71c@gmail.com> Date: Mon, 12 Feb 2024 11:11:56 +0000 MIME-Version: 1.0 User-Agent: Mozilla Thunderbird Content-Language: en-GB To: constructivenews@googlegroups.com, Agda mailing list , Homotopy Type Theory Cc: Graham Hutton , "Crole, Roy L. (Dr.)" From: Martin Escardo Subject: [HoTT] MGS'2024 (Midlands Graduate School) Content-Type: text/plain; charset="UTF-8"; format=flowed X-Original-Sender: escardo.martin@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20230601 header.b=gFSMwacj; spf=pass (google.com: domain of escardo.martin@gmail.com designates 2a00:1450:4864:20::32a as permitted sender) smtp.mailfrom=escardo.martin@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=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: , https://www.cs.le.ac.uk/events/mgs2024/ The Midlands Graduate School (MGS) provides an intensive programme of lectures on the Mathematical Foundations of Computing Science. It has run annually since 1999 and has been held at either the University of Birmingham, the University of Leicester, the University of Nottingham, or at the University of Sheffield. The lectures are aimed at postgraduate/PhD students, typically in their first or second year of study for a PhD. However, the school is open to anyone who is interested in learning more about mathematical computing foundations, and all such applicants are warmly welcomed. We very much encourage students from abroad to attend, participants from industry, and many have done so in the past. Celebrating 25 Years, MGS 2024 will be held at the School of Computing and Mathematics, University of Leicester, U.K. -- 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/31b22711-e7da-49e0-9738-a2571912f71c%40gmail.com.