From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.1 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,FREEMAIL_FROM,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 23487 invoked from network); 25 Sep 2021 09:04:32 -0000 Received: from mail-ed1-x537.google.com (2a00:1450:4864:20::537) by inbox.vuxu.org with ESMTPUTF8; 25 Sep 2021 09:04:32 -0000 Received: by mail-ed1-x537.google.com with SMTP id o23-20020a509b17000000b003d739e2931dsf12888573edi.4 for ; Sat, 25 Sep 2021 02:04:32 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1632560670; cv=pass; d=google.com; s=arc-20160816; b=KUzqGfNG60q9+6orJWfw+njhsXq495rqQvgI1vDQGFqDM/xN1Yk8qSzoNyvzY9Sc0T qpPqa1NzXOULLdHa3f7/yyunJwk8pNn2Nh8sDA7h3Rb8SPq24RAU7PR17gJKUoWsJ9Xr sydW/gZPvEtqn7z2C1MdCZomxecVkrCEjBEaJrUaice3EqsfY9v9R5dghgw1m6hk2LmK i/f/gFXHw5WBA7NoQJeu4YPOiGYkPKZKW7w1oDntA3TC/CMEFsZlI9IzHi5fgQs1xUHE xKrmhvkatSjsfISQtenGE2HY2BtpBkbr73zwN3p0pUAY7QqALM1m2gvX+L/aRlN4NLWj BIBg== 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:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:sender:dkim-signature :dkim-signature; bh=Kx8tSb+BbNjwvY/iLG7tL6sG/7oocOV3jTla3TYjhLk=; b=kS3ulL3l5h2tuyNnQHk+5rYfHaNhYlGvPWMS9Oh4JUkIRq2cQr2pEeesljvzpmKW6n z0V0RTR7WnHXUwEhVK7j+uk+oEW1QkggGrGFdxXvxa4hbyy94KVBjfXbCc7WXTWGiZgA XTHIZzv8aXEgGmuboiJDKDKMDB++Wmn6I4riUb9dJT3J+4X6ed6XTKDa7T6ApBdSFrsq roI/yBCTFWZbigngErHCZy29g+pn46HWhMw/kQqcvGJG/DE9m1WeSiGdECcJ4couF3Jp n900OqPX9sljoNO8GbmnfXR3e2tBQbWN1HwndldgyLzVmT8nCBoEmNC+qUuo2+jAzh92 NgJA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=dhK8MW+t; spf=pass (google.com: domain of guillaume.brunerie@gmail.com designates 2a00:1450:4864:20::52f as permitted sender) smtp.mailfrom=guillaume.brunerie@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=20210112; h=sender:mime-version:references:in-reply-to:from:date:message-id :subject:to:cc:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=Kx8tSb+BbNjwvY/iLG7tL6sG/7oocOV3jTla3TYjhLk=; b=Bv3OfkjqZ1MKFhG05ub/zeTnXPx0sRYwvnQ6jE4POPqen8PDh0R1F+i2NIcKdYYqAe 0MQ86/n0eg1tjrO0owpjcQC1YWiKGuHsmV8GZFBx0AUscL4ELPJqtyhOiVAhGpLQkV4+ xBcly7tH6qtM5DcBhRLQpw9Ddq/yYD+6JEYAnq5l0MFwpx62orzwKYpsBF/tUA6NC+Yu 9+eI1kwKtAth8A4jcN11k7P0K3PoM2D4oDrR3tweUX6IWnUvhcVbN3/jQCgy9W76+jgJ 1tJgPwk45haiPH9Bf+XyLyk4PjhisaPtYiE1etATk9jyZc0VeapIDvX2or/d5YbVUnWi FkvA== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc:x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=Kx8tSb+BbNjwvY/iLG7tL6sG/7oocOV3jTla3TYjhLk=; b=Wa1ZL2jHG2DI8/gUgaaKAue6ST1s6UF9GWeOOdeX3xsbnBLyTucutcg3AZYrA2ll77 8Li33O/GTyRYsvnU+R+txEc7LLaN5vGmg7N11BKr7GUEIG8QeJtAnTI0YgHPEmmSZeES xHuWBI+L6ofO5CXlJ+ENidIJKqj+7oGpX4LHkFcGi+Bb1Zuv4+H8fMrrOQQqsK3wm7Em 5fjmm7yuKG0tlQ0O7iXq8V58tE82SqlBVDn6GQyIvADakanmrZUAr/K6UHB8BExkfSiW OMuMd+4DZCIE188zFGl3pQBCJd+0gPWRmE3W5igjoVaNf6k3xKqwsEt9+VLp1fR5MRMC x6oQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=sender:x-gm-message-state:mime-version:references:in-reply-to:from :date:message-id:subject:to:cc: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=Kx8tSb+BbNjwvY/iLG7tL6sG/7oocOV3jTla3TYjhLk=; b=Sn2+QkiNdxyNSSGxQxrHeEw8WzZ9zwVkAex/esyaZc0asZZ+H0nsO9VPDjxtJugjlN QyYrHvIhvQUEzXyEywZpL97dJ3hlg59AJ1A4tHMjRwNhlyRVImAPcqP5/5DNrHXC26DP MMPJ2en3/7gAEMcfwt9v3U7jwHgj4F9CFHBXGSfLDHM6M/Hl5GP0mq7G6weiSkTtW7Vt qN0HPiZ7HJXPpcRLEIMBZTGhpjdWkJv+UPWZw4Ng4moXnkfQN7Eg4EGOoWOsSPiKyfYh 00XmRXsiuURT8tdBCQ+xnvMRNnvAiSMFZVGXNFMCWP+NQ/m+8glTcVKhGeqI42D7joAy QaBw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM5338cuNM1PF6rdii865jFdaMkfBbC08cEtYaCeWfgYka3+tcpykX lnWFykoduJ0qrPG3W6WLI50= X-Google-Smtp-Source: ABdhPJxANkVz1m7vWxzswovwwjZXXpa+b+xLsmQ2bHxhZe8kas0rnZR3V9aOBvGO8bpSKA4+rJzfYg== X-Received: by 2002:a50:d809:: with SMTP id o9mr2062084edj.149.1632560670494; Sat, 25 Sep 2021 02:04:30 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:906:2f8a:: with SMTP id w10ls967442eji.9.gmail; Sat, 25 Sep 2021 02:04:29 -0700 (PDT) X-Received: by 2002:a17:906:7811:: with SMTP id u17mr15702923ejm.562.1632560669419; Sat, 25 Sep 2021 02:04:29 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1632560669; cv=none; d=google.com; s=arc-20160816; b=DktT4H6LdADVBofu6M5haBiFYkoXmTmVQVyhwZcRAU3uAjKzgeGNGG2lhx8CeFcI/O R2jL14o0ioKCHOeSH3rD/ovakuXHoM3xmFp//74rDYlMRfpKDljI9ymGYtOgkTnjknyi 1AtB/JPCFCRJIHeQKBTnZVJl1+xHK7EZvTLqz3lGOu0fZxm7XlOBmMZZwgv591b8Y3P9 +sZqK2p99wtc9Ca2f1z5n6xPbYw+8f/Dni4ONO9Zmdfuo6iZS1wsZVfPIR5MjCu59Rf2 x0YC45dktYC+Rufw7wGlnDyp4JvHZdABPJV49yT235dYcpDK8tearQdMEzqpn8RdxHrX VlMg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature; bh=fCrp7Ysgfw1c/Fc5fzjOVBB2tAVY6FE4MS8DBFqqkUc=; b=SwUzJRBnuJI/35hfRbL4o/hfhlST/XPFoUG0Lz3J5ZgbVMnLGZ03Uwr4X4HVvdoOSS Ito3A5O0WlGYxgCUDDYwOQxdHZ3gUZv0hYN5Mmq3Yd2OgUdenr9iaPmFUMSkkAiTptB6 Npfo2mhMIUwxNShpkrTvzjxSfOGw09mgCM5rsbYgLCsA2aRvcsKr2D+W8KPELmXp+axy X6G2ye/79BBkEoZvNp/L449Rglds9/glrX92DErBwPsNNBRb1Xq3nWAtpGYItiynzJ72 jWLqJdE2H9bIFU7z+tidBgkWU4K0rfPn4TLcuuYX7kuMAXjpUNbzTfn9z9G1lsm2CQ/u hj6g== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=dhK8MW+t; spf=pass (google.com: domain of guillaume.brunerie@gmail.com designates 2a00:1450:4864:20::52f as permitted sender) smtp.mailfrom=guillaume.brunerie@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-ed1-x52f.google.com (mail-ed1-x52f.google.com. [2a00:1450:4864:20::52f]) by gmr-mx.google.com with ESMTPS id j19si699690edp.2.2021.09.25.02.04.29 (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sat, 25 Sep 2021 02:04:29 -0700 (PDT) Received-SPF: pass (google.com: domain of guillaume.brunerie@gmail.com designates 2a00:1450:4864:20::52f as permitted sender) client-ip=2a00:1450:4864:20::52f; Received: by mail-ed1-x52f.google.com with SMTP id c21so45344226edj.0; Sat, 25 Sep 2021 02:04:29 -0700 (PDT) X-Received: by 2002:a17:906:6b93:: with SMTP id l19mr16389305ejr.26.1632560669205; Sat, 25 Sep 2021 02:04:29 -0700 (PDT) MIME-Version: 1.0 References: In-Reply-To: From: Guillaume Brunerie Date: Sat, 25 Sep 2021 11:04:17 +0200 Message-ID: Subject: Re: [HoTT] Reminder: 2 year position on HoTT and related topics in Stockholm, deadline Friday next week To: Anders Mortberg Cc: Homotopy Type Theory , types-announce@lists.seas.upenn.edu, Agda mailing list , Coq-Club Club , lean-user@googlegroups.com, constructivenews@googlegroups.com, Categories list Content-Type: multipart/alternative; boundary="000000000000c3275605ccce26cd" X-Original-Sender: guillaume.brunerie@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=dhK8MW+t; spf=pass (google.com: domain of guillaume.brunerie@gmail.com designates 2a00:1450:4864:20::52f as permitted sender) smtp.mailfrom=guillaume.brunerie@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: , --000000000000c3275605ccce26cd Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Den fre 24 sep. 2021 13:20Anders Mortberg skrev: > Dear all, > > A quick reminder of the postdoctoral position in HoTT and related topics > that I advertised a couple of weeks ago, with deadline *October 1* > (midnight Stockholm time). > > Full details and application at: > https://www.su.se/english/about-the-university/work-at-su/available-jobs?= rmpage=3Djob&rmjob=3D15797&rmlang=3DUK > > Departmental webpage: https://www.math.su.se/english/research > > Once again, please get in touch with me if you have any questions about > the position or application process! > > Best, > Anders > > > On Mon, Sep 6, 2021 at 1:43 PM Anders Mortberg > wrote: > >> Dear all, >> >> I=E2=80=99m pleased to announce that we=E2=80=99re hiring a postdoctoral= researcher in >> homotopy type theory and related topics at Stockholm University. It=E2= =80=99s a 2 >> year position, provisionally starting January 2022, in the computational >> mathematics group of the Mathematics Department. The application deadlin= e >> is 1 October. >> >> We welcome all applicants interested in working on homotopy type theory >> and related topics. Potential project topics include, but are not limite= d >> to: homotopy type theory, categorical models of type theories, cubical t= ype >> theories, implementation of proof assistants, computer formalization of >> mathematics and computer science. >> >> Full details and application at: >> https://www.su.se/english/about-the-university/work-at-su/available-jobs= ?rmpage=3Djob&rmjob=3D15797&rmlang=3DUK >> >> Departmental webpage: https://www.math.su.se/english/research >> >> Please get in touch with me if you have any questions about the position= ! >> >> Best, >> Anders >> >> -- > 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/CAMWCppmGdAQmwEc9Uw_= %2BC%3DkdZGkvjykMPQgRKChoog5UARcKNw%40mail.gmail.com > > . > --=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. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/CAFJ3QWJvJmYLSB8k-2Fm0wi41rmzGBOoMBAud%3DSN-qgQLGZVgw%40= mail.gmail.com. --000000000000c3275605ccce26cd Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable

Den fre 24 sep. 2021 13:20Anders Mortberg <andersmortberg@gmail.com> skrev:
Dea= r all,

A quick reminder of the postdoctoral positi= on in HoTT and related topics that I advertised a couple of weeks ago, with= deadline October 1 (midnight Stockholm time).


Depa= rtmental webpage: https://www.math.su.se/english/research=

Once again, please get in touch with me if you ha= ve any questions about the position or application process!

Best,
Anders
<= br>

On Mon, Sep 6, 2021 at 1:43 PM Anders Mortberg <anders.mortbe= rg@math.su.se> wrote:
Dear all,

I=E2=80=99m pleased to announce that we=E2=80=99re hiring a postdoctoral researcher in= =20 homotopy type theory and related topics at Stockholm University. It=E2=80= =99s a 2 year position, provisionally starting January 2022, in the=20 computational mathematics group of the Mathematics Department. The=20 application deadline is 1 October.

We welcome all applicants inter= ested in working on homotopy type theory and related topics. Potential project topics include, but are not limited = to: homotopy type theory, categorical models of type=20 theories, cubical type theories, implementation of proof assistants, comput= er formalization of mathematics and computer science.



<= div>Please get in touch with me if you have any questions about the positio= n!

Best,
Anders

=

--
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@googleg= roups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/Homotop= yTypeTheory/CAMWCppmGdAQmwEc9Uw_%2BC%3DkdZGkvjykMPQgRKChoog5UARcKNw%40mail.= gmail.com.

--
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://g= roups.google.com/d/msgid/HomotopyTypeTheory/CAFJ3QWJvJmYLSB8k-2Fm0wi41rmzGB= OoMBAud%3DSN-qgQLGZVgw%40mail.gmail.com.
--000000000000c3275605ccce26cd--