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,T_KAM_HTML_FONT_INVALID autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-oi1-x237.google.com (mail-oi1-x237.google.com [IPv6:2607:f8b0:4864:20::237]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id a8d75be0 for ; Fri, 1 Mar 2019 09:17:27 +0000 (UTC) Received: by mail-oi1-x237.google.com with SMTP id l198sf10282509oib.1 for ; Fri, 01 Mar 2019 01:17:27 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=cLUrNxl6iBHF43VMSABrugOpb3xdoXYxPabB0RzU2vc=; b=cw8XlkesP58J+3FLNFO+atWsuJumP2iEKGiBSilOsPsyeMHPo2HQ7VKkTRbBvpvK1H WzNrGjBBAphruXu1ZsJ0yFwG+P7/JyqWb67YUsJl0Eu/njySiPWVnaLk3oech4FJfqgl vZRUbYp14cM5UD3MJ+uftd7cGi2DJ2dYA9UOOBw++g/JcN4x793t9eqjEA0rCXaXk/SR wxyR82+1a2c4wHYYmrkyVcE8l/Xb7kz22TrF4NaCpOv6YAGvphDH8btZZhn4QCopZANB HKjsGUxb0pQQ7vtCPWHug0cKf8OnlZnBk2gLCcOEVPT20D+pYzV4dXqpjUxppNhYe/dn vnBg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:subject:mime-version:x-original-sender :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=cLUrNxl6iBHF43VMSABrugOpb3xdoXYxPabB0RzU2vc=; b=GwocOSxhONeAIFx6XnsEb1g+aUus4glc/UKOEv+14iewVquBZFz/jc86/WaZJQTRCB R/9woFDkZjqS4VpL9k3nmDdQyTTcYsFYLaBNX8CS6SHD9QLbfADhsoR45PuGnGW6Yr95 yYxuECYTW5mwVqlH3lfmlPMbiHArddpEL+uo5JfR5Rh/0uYKP9PfS+LXMAr9zvcjtkVK E+HIG/2dcyQQqS6BaDyzQPG7IceOlcuEK2t3SixV3wCnTabpxTzw4A1XX3gHhKrLb993 MgaB5NU6tIVXjiMtwCxpOjWE8oLLK5L+kTD/r1J++bUV1TwIAHCB8SS97vJI2RyYuRWM N6Uw== 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: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=cLUrNxl6iBHF43VMSABrugOpb3xdoXYxPabB0RzU2vc=; b=W8DbpgGQP7W4B4Wk33K/cZr7yOaLh1gQC5O/ycYOVQ2u+6y96p0yc73OnBLkmMpXCt z/fVox8MKS0HEvyQlsQTrNXFsMlFsWHCWKq5pvSTomazcmBHrGOG3QySr7cumhEl3LoM GHt0+moHeX81q14IKsd2b8NwQpciiaJ2ImbMC8Xm2HK7Ha9MDgxzCX+udLar8TFmv7eC P51eWSEvg2U6ZubuSFFg9xKW1pmnhFcSUnU1c4b5il6pJi34+h/eOHgHruH+oRh/fJGR 0RNGPrP+ZjiCLhn8E53oj7VIQnL3QMJujd357kB+ctDS9e/kyb0/299yRDi+RaFpmMFg p9oA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAX7kD8DBzSBxiKTX79XYP071Zf/qhneA1ECXrLUnVOdM9Izi9PF 1sE6nCYu3VyzXbo3Z8TUnL4= X-Google-Smtp-Source: APXvYqxezjDoCzNETpLdWLlMMZm7BkNo/sETW31UVEeRERXPt/Yfv0BCpQeLBw7y0cbqpwcQx/2lHw== X-Received: by 2002:a9d:73c2:: with SMTP id m2mr2770886otk.91.1551431845783; Fri, 01 Mar 2019 01:17:25 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:62c:: with SMTP id 41ls3936745otn.2.gmail; Fri, 01 Mar 2019 01:17:25 -0800 (PST) X-Received: by 2002:a9d:4c85:: with SMTP id m5mr2675914otf.367.1551431844976; Fri, 01 Mar 2019 01:17:24 -0800 (PST) Date: Fri, 1 Mar 2019 01:17:24 -0800 (PST) From: Marco Maggesi To: Homotopy Type Theory Message-Id: Subject: [HoTT] Funding available for Second School and Workshop on Univalent Mathematics, Birmingham (UK), April 1-5 MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_155_1012388142.1551431844335" X-Original-Sender: marco.maggesi@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_155_1012388142.1551431844335 Content-Type: multipart/alternative; boundary="----=_Part_156_1244540083.1551431844336" ------=_Part_156_1244540083.1551431844336 Content-Type: text/plain; charset="UTF-8" Dear all, Funding is available for participation in 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) Details of the event are given below. Participants ("trainees") eligible to be reimbursed: Trainees must be engaged in an official research programme as a PhD Student or postdoctoral fellow or can be employed by, or affiliated to, an institution, organisation or legal entity which has within its remit a clear association with performing research. Trainees eligible for reimbursement: 1. Trainees from COST Full Members / COST Cooperating Member. 2. Trainees from Approved NNC Institutions. 3. Trainees from Approved European RTD Organisations. COST member countries are listed on https://www.cost.eu/who-we-are/members/member-states-2/ The precise conditions for funding by COST are given in Section 6 of https://www.cost.eu/wp-content/uploads/2018/10/20180501-Vademecum2.pdf Overview ======== 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 computer proof assistant Coq. In this school and workshop, we aim to introduce newcomers to the ideas of Univalent Foundations and mathematics therein, and to formalizing mathematics in a computer proof assistant based on Univalent Foundations. Format ======= We will have two tracks: - Beginners track - Advanced track: suitable for participants with some experience in Univalent Foundations and the proof assistant Coq. In the beginners track, you will receive an introduction to Univalent Foundations and to mathematics in those foundations, by leading experts in the field. In the accompanying problem sessions, you will formalize pieces of univalent mathematics in the UniMath library. In the advanced track, you will work, in a small group, on formalizing a specific topic in UniMath, guided by an expert in univalent mathematics. Your code will become part of the UniMath library. Application and funding ======================= For information on how to participate, please visit https://unimath.github.io/bham2019. Funding will be given out on a `first come first served` basis. Related events =========== The 6th Workshop on Formal Topology (http://www.cs.bham.ac.uk/~sjv/6WFTop/) and the Midlands Graduate School (http://events.cs.bham.ac.uk/mgs2019/) are going to take place in the two weeks following the School and Workshop on Univalent Foundations. -- 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. For more options, visit https://groups.google.com/d/optout. ------=_Part_156_1244540083.1551431844336 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable

Dear all,


Fundin= g is available for participation in the


Second Sch= ool and Workshop on Univalent Mathematics,


to be h= eld at the University of Birmingham (UK), April 1-5, 2019

= (https://unimath.github.= io/bham2019)


Details of the event ar= e given below.


Participants ("trainees") = eligible to be reimbursed:


Trainees must be engaged= in an official research programme as a PhD Student or postdoctoral fellow = or can be employed by, or affiliated to, an institution, organisation or le= gal entity which has within its remit a clear association with performing r= esearch. Trainees eligible for reimbursement:

1. Tra= inees from COST Full Members / COST Cooperating Member.

2. Trainees from Approved NNC Institutions.

3. Tra= inees from Approved European RTD Organisations.

COST me= mber countries are listed on https://www.cost.eu/w= ho-we-are/members/member-states-2/

The precise cond= itions for funding by COST are given in Section 6 of https://www.cost.eu/wp-content/uploads/2018/10/20180501-V= ademecum2.pdf




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 o= f

Univalent Foundations, a new approach to foundations = of mathematics

based on ideas from homotopy theory, suc= h 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

= computer proof assistant Coq.


In this school an= d workshop, we aim to introduce newcomers to the ideas

= of Univalent Foundations and mathematics therein, and to formalizing=

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 pa= rticipants with some experience in

Univalent Foundation= s and the proof assistant Coq.


In the beginners tra= ck, you will receive an introduction to Univalent

Found= ations and to mathematics in those foundations, by leading experts

in the field. In the accompanying problem sessions, you will fo= rmalize

pieces of univalent mathematics in the UniMath = library.

In the advanced track, you will work, in a sma= ll group, on formalizing a

specific topic in UniMath, g= uided by an expert in univalent mathematics.

Your code = will become part of the UniMath library.


Applicatio= n 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 t= o participate, please visit

https://unimath.github.io/bham2019.

Funding will be given out on a `first come first served` basis.=


Related events

=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D

The 6th Workshop on Formal Topology (http://www.cs.bham.ac.uk/~sjv/6WFTop= /) and the Midlands Graduate School (http://events.cs.bham.ac.uk/mgs2019/= HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit http= s://groups.google.com/d/optout.
------=_Part_156_1244540083.1551431844336-- ------=_Part_155_1012388142.1551431844335--