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=-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,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: from mail-il1-x138.google.com (mail-il1-x138.google.com [IPv6:2607:f8b0:4864:20::138]) by inbox.vuxu.org (Postfix) with ESMTP id BE6DB2382C for ; Thu, 11 Apr 2024 13:32:20 +0200 (CEST) Received: by mail-il1-x138.google.com with SMTP id e9e14a558f8ab-36aff59aba8sf2268675ab.2 for ; Thu, 11 Apr 2024 04:32:20 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1712835138; cv=pass; d=google.com; s=arc-20160816; b=T6Lmxd9U4bVyGPNYP7fJ94ukz1HC8MrRTfjKQzo6K+gw9Oqr2L63cXSFSkq5DaXx92 Ygwwkjp9TEufl57fdCSnVa/IWGt+BMOGVDbypgKQOLwZY0jHOKGGX0V7axUKhWEGvBi8 TIWQdzknHCg+y70jykwHuuRMsOUBhqPARPY1tXJHJhhq3cJiPQ3I3dB9VkRxAA10L5Zz EVHp5E4hv58orjiQAj96wR1liBar3yxUo7OI3e0FFnUC1JD0NiZYs2aQV7bvzHZuSKKn 9kMg2XvvyxFKM3o3VNKVabNAcIYEnKWe2IPM3qwq59GbV7iqokCjw8RDKxdGVS+A9Zr7 N4TQ== 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:to:subject:message-id:date:from :mime-version:sender:dkim-signature:dkim-signature; bh=3aM5yPnVQjKVW/yH6In9/82jv+XyVCX4IKf9jkZREWo=; fh=IndWl0NM00YWwZJniZI7yh/Q1jvDe/xTEQraYQy9DYI=; b=iLpHpTxiEHvlGJMLZvAxLOoPLbRQIaOwgK6XU7/SM55/DZXu1FSQUe9lhnrtRA0GPV g2Xu0KTOf3cu56eL3kpX/X41P77TXgPcF4NQEGuDWLUZDvcVXzbcteVgo7KUsNJLvCdZ vLXdxe8fbmXeUpq5gvhjV23fyE5ltmP2peYL3GgtFMX8UQDDm4A5TkwI9lWvh/YiVG4b GDbTlEhK4xtgzmtW6abhlicREx3Pd02xSgRXA+6yeXVKPDI6FzsFiXwbKj40wt6PRS9V Pf9g8HMRv8gKjGFbUDqN4at8IQOCruHzV3Jch54Wj5fDz6ZyfoFoe51y9xZw9Kd9YCnp Bugg==; darn=inbox.vuxu.org ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20230601 header.b=NRFnGOjw; spf=pass (google.com: domain of anstenklev@gmail.com designates 2607:f8b0:4864:20::52d as permitted sender) smtp.mailfrom=anstenklev@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=1712835138; x=1713439938; 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:to:subject:message-id:date:from:mime-version :sender:from:to:cc:subject:date:message-id:reply-to; bh=3aM5yPnVQjKVW/yH6In9/82jv+XyVCX4IKf9jkZREWo=; b=Biuj+fUkaXrykRktH36qQZqG6t0w8hm8CzVcH+oZO7tB+vZQM+TuDPqxmo6TfmJ7JM XW1ckH7DF3DjfPlzAa83p6hcY7Af2ihUPa3+GMYzx6q/wYcQH9ppKZu7m6TeF8IUcFzP Rk0Hmk/l0IccodCKNTPPha8UUtkGRno1HtUXYfWMXNsLcMPhQKCJ5gQPgQ56zq9ygCSm mO57fyVQevYuOUSYiSxCGsKRy7tgsdXIjJ6PPa+SfZ/YwFWbByhUEx+F/IwSX/8rGSpO Q3/eZGMjLsWw8gpI5Thv/RRhm245cJlkURcAix/QSwkD1M87FDaMfBd089aJHl9BDQK9 sGxg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20230601; t=1712835138; x=1713439938; 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:to:subject:message-id:date:from:mime-version:from :to:cc:subject:date:message-id:reply-to; bh=3aM5yPnVQjKVW/yH6In9/82jv+XyVCX4IKf9jkZREWo=; b=TR/XjCCGkFNtzcfypsCl8rMSYGhGPQMrOISae+85TQq+Zj6+OnkCJyYPvM6XltnvEW sq0uf4Vm7Zg0qaJghg9X/vpeTiWw1hXy1OBftNEUbuV5RJeWQaAFFKQ/pOp5rD0tYzzJ DDSbyGoQSO0AGBKLVUsPhYHrfa7YgwyGtrtw7YumfKd7936fGNONrYBJr9PoI63S3I6W i4vY//eL1wd3CvtbVGSJlk80oJwC282zPoDOq1ciffj4rBUfeAoLuuUSk1538NYuoQF5 1NmNbyUwNY4YaRAyCDPTIMrIYzrWBHx7yz5IdKM20iKMgCsj0QgKrgPG7VdemxnLIlDI rpYQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1712835138; x=1713439938; 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:to:subject :message-id:date:from:mime-version:x-beenthere:x-gm-message-state :sender:from:to:cc:subject:date:message-id:reply-to; bh=3aM5yPnVQjKVW/yH6In9/82jv+XyVCX4IKf9jkZREWo=; b=pGxZoYB3dkzBLinQDVMP2l/p+R7vcKZ6ojPAGxw+mKnhbOZ6G3o697UC3F47fpm0cU uPowBBK4svuJzPswOpSPRCil/t0JcJRAnv1aCB37z++8WpSJPYaEbzMidMFsv+8AjXJ4 ja68yLjx36RtBOPUdt6/Ci8ErZrJuiCDLrY5rS1JcJA2iB4lSgbZJQrtfnw5Anz7EggF YAWA6Nr8mxtLNCrGCgLXNzMbb9yAB/by5ymSWEAbtgyWkr9b12Ut5BfCBzVcuhOj7pxk M+Q8IIdmTMplyPE90SgHQylLyIiSwMUVS8OExw0I82mECZEHqVDB5G+qFgpuZVTBkqJr WXBg== Sender: homotopytypetheory@googlegroups.com X-Forwarded-Encrypted: i=2; AJvYcCWbRHxsQESIBIxResNU5F37aLNnaTvLu002+z5gCbW0es+0/N6IuTDXt1l3ce/YsXcZCuQnlHF1aRDS29Z6KhZrpQ== X-Gm-Message-State: AOJu0Yx6H6wyNE4FWvBFUK+TjOSiGIS9TGS4An5gEIpSVn9RWXGIuuEb hWUjhRsRU2Tr3U4AcCZ9h85pyQeVQr7ZgiS+FV1Zg/0XQIDA12UZ X-Google-Smtp-Source: AGHT+IGwD5NwwSOKhLJOT9Kc3n8pphdhSqFJLEbrDFK6EEAG8rzOf95yGhL0pP58f5GQ2wlBqxIbhg== X-Received: by 2002:a05:6e02:1a0d:b0:366:99ee:f14a with SMTP id s13-20020a056e021a0d00b0036699eef14amr6299992ild.22.1712835138530; Thu, 11 Apr 2024 04:32:18 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6e02:485:b0:368:a702:92ec with SMTP id b5-20020a056e02048500b00368a70292ecls2282918ils.2.-pod-prod-02-us; Thu, 11 Apr 2024 04:32:14 -0700 (PDT) X-Forwarded-Encrypted: i=2; AJvYcCVZclEdk+c4DOgj9ewwqJYcJTfGIQ11d+EYVdpBBe0yfeHKUVCwxYajDCADDUhZN7I6uG5a4pm65Uv+b11jXPkN4bZ+TFfl56U7xJVtKLtMD7t6rg== X-Received: by 2002:a05:6602:4187:b0:7d0:d84d:9e13 with SMTP id bx7-20020a056602418700b007d0d84d9e13mr7771070iob.19.1712835134515; Thu, 11 Apr 2024 04:32:14 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1712835134; cv=none; d=google.com; s=arc-20160816; b=ud18DkvxmmsZBEe7YrWhfpvII92W5MR6K7SS1ybuMOEp9Ji4H1FRL1BCSZnNMk/EQZ +93apnOHuxPkwmBCBRCpuEz+D7t+OnSUPyZQA4yETYukJnvkuj43Rvz75c6TTwmhpEAq 2wDGl97oqq/NBpS4FfsA+1HSxEE7wdRQUesbnD+z7tKjwsMFR1Q7IUWsYJyZdFLsUJ2i 0lYeBcOmWaVPUcUfLchIXG4JnqwonAcQpiOd39Q9Ej2p5lMbSK9fg/hYrcpEYLF2B7F0 EDCoIAF+7Xv16Ac4EQ1NeOv18ol7LoIla7mmCD8msxkefPuRdYipnWU1rGTjl03O3M5+ MqIA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:mime-version:dkim-signature; bh=B0f9NIZAbLqlLg8kjYuftndg8fgZEWsulHsbWHL5tHc=; fh=+N3AAWwzVnHONZP7nA4kwW9pQR5Tw0BhcSGYz7OcHD0=; b=diTkh398UfX4Fops8QeCryKj6TdjylhD/xMQWt2NpUWz9EVFNbRYS7ksT6ah7tm8Ua VViuz/UuyjzvnA4NJPiUWvcGBlIyOQOsZRYvs1gx22nMW36Wk9q2XiMSO1ZDTSgY1Pwy zbXWpQKDf5VwesZ8RNvr/DQ2nkaOvtKttymxqQIKyC49VC+HLJIjQR3notTlgu2cq5Qs ujna2rJLsgh2fV3Xi/6/Li/XBd7aoC2J3rHGHBbWL4SbLlA+rnpZE6vSxF8i/p5NWrta Hz1Kc7m17b3i0g5b6WBQSx+coKNxKaesbQt3mtQKgF66xSu/FAA3Pp7PoYA316joLGvg 0Gew==; dara=google.com ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20230601 header.b=NRFnGOjw; spf=pass (google.com: domain of anstenklev@gmail.com designates 2607:f8b0:4864:20::52d as permitted sender) smtp.mailfrom=anstenklev@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-pg1-x52d.google.com (mail-pg1-x52d.google.com. [2607:f8b0:4864:20::52d]) by gmr-mx.google.com with ESMTPS id e9-20020a6b7309000000b007d5eb8eb2cbsi71509ioh.1.2024.04.11.04.32.14 (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Thu, 11 Apr 2024 04:32:14 -0700 (PDT) Received-SPF: pass (google.com: domain of anstenklev@gmail.com designates 2607:f8b0:4864:20::52d as permitted sender) client-ip=2607:f8b0:4864:20::52d; Received: by mail-pg1-x52d.google.com with SMTP id 41be03b00d2f7-5dca1efad59so5558935a12.2; Thu, 11 Apr 2024 04:32:14 -0700 (PDT) X-Forwarded-Encrypted: i=1; AJvYcCXC5OLqu7IsIJeCYQO8b8slrRfuTCiTNhUxu5vKUYeeYsfxsjSPLbtZHLmaVKRoZRCvDPm/9ksJDqsbdUg0Osk182wnDGYR4O7ENVYgUoDcUSEe28zLITm559MyUXsTvCyjugZV23j5oY2C55c7hnKjrZPLYV7gTEDWhJS9w8Y= X-Received: by 2002:a17:90a:fe18:b0:2a2:a9c3:6447 with SMTP id ck24-20020a17090afe1800b002a2a9c36447mr5250952pjb.21.1712835133810; Thu, 11 Apr 2024 04:32:13 -0700 (PDT) MIME-Version: 1.0 From: =?UTF-8?Q?Ansten_M=C3=B8rch_Klev?= Date: Thu, 11 Apr 2024 13:31:47 +0200 Message-ID: Subject: [HoTT] Workshop on inductive definitions To: fom@lists.ugent.be, HomotopyTypeTheory@googlegroups.com, members-philmathpractice@googlegroups.com Content-Type: multipart/alternative; boundary="000000000000b5b64f0615d08184" X-Original-Sender: anstenklev@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20230601 header.b=NRFnGOjw; spf=pass (google.com: domain of anstenklev@gmail.com designates 2607:f8b0:4864:20::52d as permitted sender) smtp.mailfrom=anstenklev@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: , --000000000000b5b64f0615d08184 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Workshop on inductive definitions An inductively defined domain is a domain whose elements may be thought of as having been generated in a stepwise fashion. Standard examples are the natural numbers, the words over some alphabet, and the constructive ordinals. Over an inductively defined domain, functions may be defined by induction on the structure of the elements. Both forms of inductive definition are central to mathematics. In constructive mathematics, in particular, they are usually treated as primitive forms of definition. In this workshop, both conceptual and technical aspects of inductive definitions will be discussed. Hosted by the Institute of Philosophy, Czech Academy of Sciences 2-3 May Academic Conference Centre (AKC), Husova 4a, Prague, Czechia Thursday 2 May ------- 10.00 Introduction by Ansten Klev (Prague) 11.00 Peter Dybjer (Gothenburg) =E2=80=93 Inductive definitions, predicativ= ity and the Mahlo Universe 14.00 Laura Crosilla (Florence) =E2=80=93 Predicativity as invariance 15.30 Mark van Atten (Paris) =E2=80=93 Intuitionistic inductive definitions Friday 3 May ------ 9.30 Thierry Coquand (Gothenburg) =E2=80=93 Inductive definitions and const= ructive mathematics 11.00 =C3=98ystein Linnebo (Oslo) =E2=80=93 Inductive definitions and Weyl'= s notion of extensional determinateness 14.00 Ulrik Buchholtz (Nottingham) =E2=80=93 TBA 15.30 Wilfried Sieg (Pittsburgh) =E2=80=93 Methodological frames: Mathemati= cal structuralism and proof theory The workshop will be broadcast via Zoom. Write klev@flu.cas.cz for the link. The talks by Van Atten and Sieg will be exclusively via Zoom. Generously funded by a Lumina quaeruntur grant (LQ300092101) from the Czech Academy of Sciences. --=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/CAJHZuqYH4WKea9rbKzQOC6dZMhq3WJMoNfYViy2WFO-DZgJ5-w%40ma= il.gmail.com. --000000000000b5b64f0615d08184 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Workshop on inductive definitions

An in= ductively defined domain is a domain whose elements may be thought of as ha= ving been generated in a stepwise fashion. Standard examples are the natura= l numbers, the words over some alphabet, and the constructive ordinals. Ove= r an inductively defined domain, functions may be defined by induction on t= he structure of the elements. Both forms of inductive definition are centra= l to mathematics. In constructive mathematics, in particular, they are usua= lly treated as primitive forms of definition. In this workshop, both concep= tual and technical aspects of inductive definitions will be discussed.=C2= =A0

Hosted by the Institute of Philosophy, Czech Aca= demy of Sciences
2-3 May
Academic Conference Centre (AK= C), Husova 4a, Prague, Czechia

Thursday 2 May
-------
10.00 Introduction by Ansten Klev (Prague)
11.00 Peter Dybjer (Gothenburg) =E2=80=93 Inductive definitions, predicat= ivity and the Mahlo Universe

14.00 Laura Crosilla = (Florence) =E2=80=93 Predicativity as invariance
15.30 Mark van A= tten (Paris) =E2=80=93 Intuitionistic inductive definitions

<= /div>
Friday 3 May
------
9.30 Thierry Coquand (Got= henburg) =E2=80=93 Inductive definitions and constructive mathematics
=
11.00 =C3=98ystein Linnebo (Oslo) =E2=80=93 Inductive definitions and = Weyl's notion of extensional determinateness

1= 4.00 Ulrik Buchholtz (Nottingham) =E2=80=93 TBA
15.30 Wilfried Si= eg (Pittsburgh) =E2=80=93 Methodological frames: Mathematical structuralism= and proof theory

The workshop will be broadcast v= ia Zoom. Write klev@flu.cas.cz for t= he link. The talks by Van Atten and Sieg will be exclusively via Zoom.=C2= =A0

Generously funded by a Lumina quaeruntur= grant (LQ300092101) from the Czech Academy of Sciences.=C2=A0

--
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://gro= ups.google.com/d/msgid/HomotopyTypeTheory/CAJHZuqYH4WKea9rbKzQOC6dZMhq3WJMo= NfYViy2WFO-DZgJ5-w%40mail.gmail.com.
--000000000000b5b64f0615d08184--