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=-0.9 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 autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-lj1-x23a.google.com (mail-lj1-x23a.google.com [IPv6:2a00:1450:4864:20::23a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 5f7fafe1 for ; Tue, 4 Dec 2018 17:05:17 +0000 (UTC) Received: by mail-lj1-x23a.google.com with SMTP id s64-v6sf4824317lje.19 for ; Tue, 04 Dec 2018 09:05:17 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1543943116; cv=pass; d=google.com; s=arc-20160816; b=QG3dWwlh77pgr4C/7H1sGY2nYD6XmNdsTdqGT1eUzEr5PUou+y8eQJP3HHPRMNcGpe QHvi7UHoRGz7SirSPdBBJx3u9FeTdsvPTFBgrks+rp5k5hnilwghxc/jAK4gbCCTuOYp pdPTlm/RB9KqSyVMJe3nnAC+jhb2XqkAJt0TlAKvoTieOLy51VznMA9aCwQfRWdNUiLp 4XrwYbW1OQgmCClFXsdQ8T79zhGuo0yhKo61buUlGAIQ07R/lbZqn64ibeUzg5WVOlcl EfOj1wOMjMddKlpMqQWi/1ex7er6AfpKwBCI2Snno4esx+F5uxMsEAggGWKpH+aOckZj UxUA== 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:content-transfer-encoding:content-language :mime-version:user-agent:date:message-id:to:subject:from:sender :dkim-signature:dkim-signature; bh=AAoDPXlXtgkCBmUSKBqcHfWi7VS9N31iz2UMYl9SCxU=; b=auGARSYX7r88Kwlio0T1GIbCcvGR9nUbB5fSqu8ZFKvoJz4tqhdMOcz22aC2yuMCk5 lasmNSv5krfyjn1/Mo/gowFuiH5HMAsVL9O5//lMArEq2rTVZRw8OFdHb/vYB5pZ688d uLwm2iyTdcKO1amJnGw4f0T1B0I8YtPiMc2Vtgg+aTK/WZFbWJkoKXA1MHF6gG6l4rik SRfJQmKb0We2A9xexNgbySVcglyTk1SgP09hPOOb4noN2tWUqhBSxLpvfULma4CUQ6Dd wMieV+gJr42i1VEtd8aiKmmxQ6OfxmhSTQWe9SUpwcpmFye0PXpYbI/kJtkT1V9tX309 ACSQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=SmLsZAD0; spf=pass (google.com: domain of benedikt.ahrens@gmail.com designates 2a00:1450:4864:20::335 as permitted sender) smtp.mailfrom=benedikt.ahrens@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=20161025; h=sender:from:subject:to:message-id:date:user-agent:mime-version :content-language:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=AAoDPXlXtgkCBmUSKBqcHfWi7VS9N31iz2UMYl9SCxU=; b=bRsphOXt/xUXlFtdHS81EAleaMB1J03pGg139TEa77Hy8lS5KfVx/9jCPSTQfXC/9R qPIxH+ofi88D0KlWW6teehlF86Qsvdprm/t0+QItwCBVb23ZsJauTB7MUyNOi7wv0+c2 5MjFEq0axYC4MbcqJwBfk2X+GI5aK+VzjAl+xuj9D8DbevCB2DnlqJLoIkIIrd0pulVo g+u6PeE/WUCDdkiCBu5ub7cQU6Ez23O9YXCLLdS8IyBuf5LoQQnbjAOoyPHKzHjrcWt7 wL2M3282PgPDqKjOks8Mmj5mhpu/71wxFzSpB/TzFBoVSx83B9p5ngv2nlaDVl5GajXI aOVQ== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=from:subject:to:message-id:date:user-agent:mime-version :content-language:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=AAoDPXlXtgkCBmUSKBqcHfWi7VS9N31iz2UMYl9SCxU=; b=rymCsQnAEBapWABm9sXTfzl/RpZOJGO7APZM4B/WvBWZCf8cEoq4R1qf+a6xAXPvlE G4o8huMXX47ujM8fYhQTzE2qbg1lnB6rsy66k7yoAobeJXWvGrPP+e8RpDdtOXkmP0Cp YFSsmFKkVsTjX/eo3JlbSoIFtmuuXf8+92Oj67fWM/vGlQWjXnk+NsHLuY8tjndYW44w gHR/4y+L3+YA1Gl9EmJeUcYb0HBptEvItCZ8vEao+rbCVJmbpyNBcqX2+U0y3N1VRe2o baX5cpDcDTOxeYfFPz2h1MDMH//ZlhQ7Xm637/Zm+v9uP73QOtRad7FVkve7agpIm1ws d/TQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:from:subject:to:message-id:date :user-agent:mime-version:content-language:content-transfer-encoding :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=AAoDPXlXtgkCBmUSKBqcHfWi7VS9N31iz2UMYl9SCxU=; b=WPWnt3f2wGaCSrPsBfwFxn7+l1zZpwMKusKM++XxeJi/L6wxxjLgcdGSnRtInUR8y3 Ast8sKYkZB1WJRh4wDxwxnSIimXlwO5fwrjs5vRiwZ5+MOn1MoXBHADVeUbkawRDK5Yl qBVAJHhVu04P3S7k8e7f3eie98dSNmxPuV4NRfUI1gcCUNVN6VDay3Rdy2f0oF4vyj8n 8s/8D9Ar0VA/eZePVprmtuNJrnLw3djLPp+VmRnq0eS1Mh09ZVKtabHk93QhDzxYRodu jz/uixDSbNQLNifreWvskq14kSjasyoVPJVbOmdqA3Zt9h5DpVgycO45yG7Q02TCKE5x hF9g== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AA+aEWYJP1Q55bDedFcm92Crky7qkePfyPiKTXMCJD0EEsOGEggnbcS6 vrH/LIWmBM8LdeZOhx+/lP0= X-Google-Smtp-Source: AFSGD/W4viyTyuDbSdgt6xY2T1muKhcSq51MoNhM+EmjHh2OeG+zNDKmjMjtL0YwWpy+r9xtIXyR+A== X-Received: by 2002:a2e:5d8f:: with SMTP id v15-v6mr151966lje.7.1543943116654; Tue, 04 Dec 2018 09:05:16 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a2e:9691:: with SMTP id q17-v6ls2423855lji.2.gmail; Tue, 04 Dec 2018 09:05:15 -0800 (PST) X-Received: by 2002:a2e:7803:: with SMTP id t3-v6mr1962690ljc.11.1543943115924; Tue, 04 Dec 2018 09:05:15 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1543943115; cv=none; d=google.com; s=arc-20160816; b=avxJfH9I4RbTUd7Wr6IrtJhealQ5lP2IhxTUEbac5x9HRFc6UIIdstEuI/+beddVxy G2Ko6yB1CySjtGFTvNo5UUbGe5ZXlBb72xjL/R+30krJP4A+fdyEHX1IN7UPzGTEd3PD 2pWPV4MXmcNUjpgfa3tnrK+NsKvPc78R+6EbBDUkNjr5LhBqM3ZR6FPHePwlURcsdZEV D+d9gKGcurrF0t+ckXKi30mcZxgFiT8DqlWVyPdeDxw94DxOPpafsi4wdHTmtn6U/gcU Uo0PH4tHiWi8x0tZp2Y8m8O0Hv8vP0x/1wocU3WJE4xsemN6IpAA4O/nHGmoWYZKoQhO Hy3g== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:content-language:mime-version:user-agent :date:message-id:to:subject:from:dkim-signature; bh=O6T9y8b6DoXm5/DNJABcUUQFnfvFUOHfR2BPgW9zqFQ=; b=v6qw8HhVp/O98nvrTwW1vcxPvTk2SEMmlcaVW7uHOy7c7CmxPKNP+CxNrp5KSVzxTy 9urUVt9zR6zKwP2GbOzbw+76w+OxkvIpxFMRGAeszJUUmonyrFw6ZdwKAwYbF3ib7vAY PqQz05yO1tvqaMPG9EDeHlMpWuae0iPcDDh/nTe0LvM5ql/+PE2hIewq2LkWA5jtEBf3 SPSQ0c4gh2KYxH3CL917aLaaNLk9zCCVTWhqHSLtPUxG3LqYoW91q6kJ3dhseMUaYFv/ vvj+uRLwq59qccQ/rog01xKG4wIUbGO4f+WDOuIQg/wLzxHO2X7EyPa5jBQcv03JlTnq EDVQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=SmLsZAD0; spf=pass (google.com: domain of benedikt.ahrens@gmail.com designates 2a00:1450:4864:20::335 as permitted sender) smtp.mailfrom=benedikt.ahrens@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-wm1-x335.google.com (mail-wm1-x335.google.com. [2a00:1450:4864:20::335]) by gmr-mx.google.com with ESMTPS id y18si715122lfe.3.2018.12.04.09.05.15 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 04 Dec 2018 09:05:15 -0800 (PST) Received-SPF: pass (google.com: domain of benedikt.ahrens@gmail.com designates 2a00:1450:4864:20::335 as permitted sender) client-ip=2a00:1450:4864:20::335; Received: by mail-wm1-x335.google.com with SMTP id y1so10345694wmi.3 for ; Tue, 04 Dec 2018 09:05:15 -0800 (PST) X-Received: by 2002:a1c:9803:: with SMTP id a3mr13536978wme.69.1543943115192; Tue, 04 Dec 2018 09:05:15 -0800 (PST) Received: from [147.188.200.206] (dynamic200-206.cs.bham.ac.uk. [147.188.200.206]) by smtp.gmail.com with ESMTPSA id c8sm12916862wrx.42.2018.12.04.09.05.14 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 04 Dec 2018 09:05:14 -0800 (PST) From: Benedikt Ahrens Subject: [HoTT] Second School and Workshop on Univalent Mathematics, Birmingham (UK), April 1-5, 2019 To: homotopytypetheory Message-ID: <53ab340b-c3b6-2a11-0ffd-afebf13b1f3c@gmail.com> Date: Tue, 4 Dec 2018 17:05:13 +0000 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:60.0) Gecko/20100101 Thunderbird/60.3.0 MIME-Version: 1.0 Content-Type: text/plain; charset="UTF-8"; format=flowed Content-Language: en-US Content-Transfer-Encoding: quoted-printable X-Original-Sender: benedikt.ahrens@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=SmLsZAD0; spf=pass (google.com: domain of benedikt.ahrens@gmail.com designates 2a00:1450:4864:20::335 as permitted sender) smtp.mailfrom=benedikt.ahrens@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: , Dear all, We are pleased to announce the Second School and Workshop on Univalent Mathematics, to be held at the University of Birmingham (UK), April 1-5, 2019 (https://unimath.github.io/bham2019) Overview =3D=3D=3D=3D=3D=3D=3D=3D Homotopy Type Theory is an emerging field of mathematics that studies a fruitful relationship between homotopy theory and (dependent) type theory. This relation plays a crucial role in Voevodsky's program of Univalent Foundations, a new approach to foundations of mathematics based on ideas from homotopy theory, such as the Univalence Principle. The UniMath library is a large repository of computer-checked mathematics, developed from the univalent viewpoint. It is based on the=20 computer proof assistant Coq. In this school and workshop, we aim to introduce newcomers to the ideas=20 of Univalent Foundations and mathematics therein, and to formalizing=20 mathematics in a computer proof assistant based on Univalent Foundations. Format =3D=3D=3D=3D=3D=3D=3D We will have two tracks: - Beginners track - Advanced track: suitable for participants with some experience in=20 Univalent Foundations and the proof assistant Coq. In the beginners track, you will receive an introduction to Univalent=20 Foundations and to mathematics in those foundations, by leading experts=20 in the field. In the accompanying problem sessions, you will formalize=20 pieces of univalent mathematics in the UniMath library. In the advanced track, you will work, in a small group, on formalizing a=20 specific topic in UniMath, guided by an expert in univalent mathematics.=20 Your code will become part of the UniMath library. Application and funding =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D For information on how to participate, please visit https://unimath.github.io/bham2019. The deadline to apply is January 15, 2019. Limited financial support is available to cover participants' travel and lodging expenses. Mentors =3D=3D=3D=3D=3D=3D Benedikt Ahrens (University of Birmingham) Thorsten Altenkirch (University of Nottingham) Langston Barrett (Galois, Inc.) Andrej Bauer (University of Ljubljana) Auke Booij (University of Birmingham) Mart=C3=ADn Escard=C3=B3 (University of Birmingham) Tom de Jong (University of Birmingham) Marco Maggesi (University of Florence) Ralph Matthes (CNRS, University Toulouse) Anders M=C3=B6rtberg (Carnegie Mellon University and University of Gothenbu= rg) Niels van der Weide (University of Nijmegen) Best regards, The organizers Benedikt Ahrens and Marco Maggesi --=20 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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.