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,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 14632 invoked from network); 29 Nov 2022 15:03:32 -0000 Received: from mail-il1-x13d.google.com (2607:f8b0:4864:20::13d) by inbox.vuxu.org with ESMTPUTF8; 29 Nov 2022 15:03:32 -0000 Received: by mail-il1-x13d.google.com with SMTP id s1-20020a056e021a0100b003026adad6a9sf12396672ild.18 for ; Tue, 29 Nov 2022 07:03:32 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1669734210; cv=pass; d=google.com; s=arc-20160816; b=j4IChahKeFM9zySvgIPGlnWQNr78irMIbwiAidPHETJ6ZCphd02Dw3AlpVPONlL18o BcEFF8qJTDjaY5rQOUoaYo1h+b1g4237UWCabZXHugrAkWynLUQEYCgcbxlD8Ee+ABK5 DENckW1qErPY9nU009IT4khMHIUebuEceXWXeRzoha1PWwjU0tWaxRaVc0zst6Rkm8k0 POVrthUmiUTgQBNV0/2fP84Yxr3qQp13mnxotn81iHiTBwvqOtik9Uiqkb2BL6NHPosc sg/aRCfhEYPjV9YtRVfbW1bvxPrm0y2Ilxf0GDO2fnkKFFgiobVRDeAycgAU8sHFXW1E erNA== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:to:subject:message-id:date:from :reply-to:in-reply-to:references:mime-version:sender:dkim-signature :dkim-signature; bh=EDbj3jshX8ivtou2k/RKIjrUalc5ITd7W3CJK1HgQKg=; b=rtn8s8cQ8CsE0mTQXEe9uXeY5N7DSmj7R3Aa8ALOBAVwcuTQng5zdrTUADhT2G1G4c pxShL7Ys6UJVMTNbntUKp5k8M2JV2bhPBYiREJsCr6IjOniPmscsIvK4lXDUkkKSU8oO OSohTtU+sTIKl9OokcN3QAXVm45oRpGyfqvjQuZRDQO6T6QdycNxiaMnFcWaSTcj0iqc kWeJwH7TjafY9ZtJ3pLIG9+Zaf0cV6xh3et6OzcpE0X8IvcU8FyPfynhALByq/8MSbQv y5fRq7MHEyTA5eh9tvcVZycEHMP8hmiOl4x7FiJrDOkU9CFS2f93AroDNAWGWv57d8+A wAXA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=Mm8vU0Fs; spf=pass (google.com: domain of jamievicary@gmail.com designates 2607:f8b0:4864:20::d36 as permitted sender) smtp.mailfrom=jamievicary@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=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:to:subject:message-id:date:from:reply-to :in-reply-to:references:mime-version:sender:from:to:cc:subject:date :message-id:reply-to; bh=EDbj3jshX8ivtou2k/RKIjrUalc5ITd7W3CJK1HgQKg=; b=VmBJ7+VYknNy5PyGHS+T7MF/8jOa3BwdG3lqkTcNqzzPBdxWT0+HntPnTJj+1hOdfc hltMcU8I53WBIIyMS53cR2yvgVzaYFri0fszXk6y6p5bedN0C15fCmU7RTLx7XKBKxg/ 5cyT9gYnm94QbzMljC0/j8Tq7fJVThXYiMffhWPGRDjqigYUBW+va6jrVZC0maHWxopm cRTmN90QLUa/ySiXaO5azIOzkIel/Ip8PEHxYhGB9usIgGM9vmCx99xkDZNJwyfsIkj+ ootM1PMJeTY0lvpoV4c9r7u7V1XF/zqtWTBu6t/U6agkUOMOWBtSfdYJzErMba/EANbw NjHQ== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:to:subject:message-id:date:from:reply-to :in-reply-to:references:mime-version:from:to:cc:subject:date :message-id:reply-to; bh=EDbj3jshX8ivtou2k/RKIjrUalc5ITd7W3CJK1HgQKg=; b=ARCb0ljCQUMSog53P5o5Ol2hlltL4QG3NgAZFY5AdWPaPIQo45/S4gq7vgwD8Tp2JA U1bISPsu6Ix+N9BRLHXboL2KSeNeIZEZC5HUI6RCl+Q69eX4Z2Q2x37d9K6wK3U8NI76 N0RYyHJLD7e+Mi0K0dqp23ECVvXYQXOvAG7u6mSk4CcY8oMYPiJSgWVHt7PuqzewH6vr vcMjI79/x3GtiDAoejVB8SrsmR5Rm2DBOgFTQDYk19Ftd18eRWtxdMTKHmkZrYySbQ02 hE3fkbvXcsndBMSnFSX4TThe+kCfGRPiU7eeivvxGPPEYeDYOlSgU/RTwFJlARSLzBnb qtkw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :x-spam-checked-in-group:list-id:mailing-list:precedence :x-original-authentication-results:x-original-sender:to:subject :message-id:date:from:reply-to:in-reply-to:references:mime-version :x-gm-message-state:sender:from:to:cc:subject:date:message-id :reply-to; bh=EDbj3jshX8ivtou2k/RKIjrUalc5ITd7W3CJK1HgQKg=; b=0WrfCGJnI080orRDm2ZLdj4pKkTG30tE0ljQx/vAsWI+ZVydeRJ2C/c1msecEpf5Lc 7Txx/79xZZrpDO17cNocL7jhzdbtxB+ZX1Fa0WqmPsbiwB6skqwXkdySBRdc6pyHvysO XUD0cyVuIez1Vu1iDVdkBfEf035VZRX2KTLXh2nU21h32e98HAy7mfj7e5GQghARwhHo pVb9i4jX6UQ2/BzG4lIpcxqIZ4YvAt/8TZLPVqUC755q0Fd+tzPJlhczgEAaQsnT2Bov aahICj6PPSOTbPPPxJgnsKtam92AnaTdlO08uG0JB3brJcXBNSQod/LfN8tvF5ONK0g9 xhTQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ANoB5pkSBVz0wLUil7nxHjaaReCzyj4tmQxlC0gFgw9fhb2or36mb21t lz1Wu/HhUaNsR+VSrjThtrs= X-Google-Smtp-Source: AA0mqf6+9MqbmxJ2myaA2oX3kl7Jw4aLRMnSKeCA/RlydzwpgGybHn4ou641jguaiggnKayh/yUOCw== X-Received: by 2002:a02:c918:0:b0:376:2324:bfe1 with SMTP id t24-20020a02c918000000b003762324bfe1mr27439677jao.189.1669734210290; Tue, 29 Nov 2022 07:03:30 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a5d:9685:0:b0:6de:9e24:a442 with SMTP id m5-20020a5d9685000000b006de9e24a442ls1389138ion.9.-pod-prod-gmail; Tue, 29 Nov 2022 07:03:29 -0800 (PST) X-Received: by 2002:a05:6602:234b:b0:6db:6299:1144 with SMTP id r11-20020a056602234b00b006db62991144mr16777811iot.212.1669734208828; Tue, 29 Nov 2022 07:03:28 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1669734208; cv=none; d=google.com; s=arc-20160816; b=rKuoOdMF9Fw0NAkojXSDg1iwQ9busG3DCRL/lurzixYkOW4iIQTAhL7u8GJ8RNyxPN EhPgQovxInB7UtsE/4Cle11bxmrlePHmcTtyFSP5wJ4na88JVMXNLorE/5tBwZLa9pTw NHq9M7lihku85IlBlSgmY/CcoQcZa70M0/aA7DmbP+tyqeYhVKDDOl4/8wUCeOsYkNQ8 h87FWYnGa9Y0CnNRrm22KIdqEKukrl5kfXlWWcFFSS/A3Wv/0nn8RtL0/ZDn3zNtriAo KzHMr+t5z9ZN2zjmve7KpSZQeO0O01AejjEfBjkU2zkmr+O1GTV6s5o5mjOkcX8cwQtL XqZA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:reply-to:in-reply-to:references :mime-version:dkim-signature; bh=yuKfSV9Sz6xjyFR4cq98PXpALdjgvM9bFPYV6HXZelk=; b=KeO7VXUIPXQT6g/WAMIPg1Q4fAKoFPhKRNQtepVuQs/qwDFddF6ifqQFXYAtFu+sPg 9vtDoQ2+ndTZSnUpws9RKPBm9nBZsrSruroQ0g4Eq+TN5iDFSYK0kPKRXJ0/D7pcpg7E mrxfTVuBHjpAtWSmjwAeLS61CPlkHIVcnd04rFXHJ9grAfMb7i443xw+Wmi3OqH+lKN1 sD8K81yg4OX9KpCu8EO7HSTdAC+pdPJUEIHJq2DHecFuoZP7hnYtM+UbFf17HjF/QlfE XJhRl8+p4WP+iJH8ZIymv78B5yg3tTK4fD4u29LJ3tnjow7vIMa0VV3kB8hi4ytvibbR qPRA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=Mm8vU0Fs; spf=pass (google.com: domain of jamievicary@gmail.com designates 2607:f8b0:4864:20::d36 as permitted sender) smtp.mailfrom=jamievicary@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-io1-xd36.google.com (mail-io1-xd36.google.com. [2607:f8b0:4864:20::d36]) by gmr-mx.google.com with ESMTPS id b5-20020a02c985000000b0035a25c888bcsi894352jap.2.2022.11.29.07.03.28 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Tue, 29 Nov 2022 07:03:28 -0800 (PST) Received-SPF: pass (google.com: domain of jamievicary@gmail.com designates 2607:f8b0:4864:20::d36 as permitted sender) client-ip=2607:f8b0:4864:20::d36; Received: by mail-io1-xd36.google.com with SMTP id p193so65609iod.6 for ; Tue, 29 Nov 2022 07:03:28 -0800 (PST) X-Received: by 2002:a05:6638:418f:b0:387:9f70:be42 with SMTP id az15-20020a056638418f00b003879f70be42mr13741058jab.295.1669734208474; Tue, 29 Nov 2022 07:03:28 -0800 (PST) MIME-Version: 1.0 References: In-Reply-To: Reply-To: jamievicary@gmail.com From: Jamie Vicary Date: Tue, 29 Nov 2022 15:03:15 +0000 Message-ID: Subject: [HoTT] Cambridge 3-year postdoc position on type theory for higher categories To: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" X-Original-Sender: jamievicary@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=Mm8vU0Fs; spf=pass (google.com: domain of jamievicary@gmail.com designates 2607:f8b0:4864:20::d36 as permitted sender) smtp.mailfrom=jamievicary@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: , List-Unsubscribe: , Hi, I have a 3-year postdoctoral research position available soon in Cambridge, on type theory and higher categories. The project itself is not on HoTT, but a researcher from the HoTT community could potentially be a very good fit. The closing date for applications is 13 December, and the position is intended to start early next year, although there is some flexibility in the start date. We have a great group here with lots of category theory--related activity, and Cambridge is a fun place to live. I'd be happy to receive any informal enquiries. Best wishes, Jamie ------------- Research Assistant/Associate in Type Theory for Higher Categories (Fixed Term) https://www.jobs.cam.ac.uk/job/38441/ Fixed-term: The funds for this post are available for 3 years Start Date: 1 January 2023 (or as soon as possible thereafter) Applications are invited for a Research Assistant/Research Associate to work on computational aspects of higher category theory. In this collaborative project, we aim to develop powerful new type-theoretic tools for working with directed globular weak higher categories, such as semistrict languages, cylinder/path space constructions, tensor products, and higher transfors, in particular from the perspective of the Finster-Mimram type theory Catt (arXiv:1706.02866). The position is within Jamie Vicary's research group in the Department of Computer Science at the University of Cambridge. Part of the Cambridge Logical Structures Hub (https://www.cl.cam.ac.uk/research/clash/), this is an exciting scientific environment with many researchers working on related topics, and a vibrant seminar schedule and visitor programme. Cambridge is a beautiful city in which to live and work. The successful candidate is likely to have (or expects to soon be awarded) a PhD in Mathematics, Computer Science or a related discipline. The candidate must have research experience in the following area: - Type-theoretic models of higher category theory Experience in the following areas is desirable: - Cylinder and path space constructions - The Finster-Mimram type theory Catt - Model structures on higher categories - The Gray tensor product of higher categories - Formal proof construction in Agda or Coq - Computads for higher categories - String diagrammatic methods for higher categories For informal enquiries please contact Jamie Vicary (jamie.vicary@cl.cam.ac.uk). Please ensure you upload a covering letter explaining your suitability for the role, a curriculum vitae, and contact information of 2 references. NOTE referees may be contacted at any point of the application process. If you upload any additional documents, which have not been requested, we will not be able to consider these as part of your application. The University actively supports equality, diversity and inclusion and encourages applications from all sections of society. The University has a responsibility to ensure that all employees are eligible to live and work in the UK. -- 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/CANr23v2U5MwDNB3hVBhjgA9R%2BAJkyo2U-HWETYMkD-NBGwerJg%40mail.gmail.com.