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.1 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-lj1-x237.google.com (mail-lj1-x237.google.com [IPv6:2a00:1450:4864:20::237]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 6acea292 for ; Sat, 2 Mar 2019 21:33:37 +0000 (UTC) Received: by mail-lj1-x237.google.com with SMTP id u13sf255046ljj.13 for ; Sat, 02 Mar 2019 13:33:37 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1551562416; cv=pass; d=google.com; s=arc-20160816; b=OF13VqucUBkAzeuO6iw55XRKIjhMvXJT9SdVwlkedi4k3P8yGhs7iBnBv+uHAXzLcI Ra2ytRMo6aRMZXJMr7NynbjJgG0BI4+IXjbSLsmqnRLo1Zbxi1L8wOpxTD3Y52UQ4JGh QrcX8AJ7tYsLT4XN/FNDRfd1yXrFjBvAGvysRadl4dbD1jWjpWxbo/FjxCzXDb9kRaUi g3rAj+d/UYCyII8eyyAXfv06fQxc3og6RGuBWApNIc9CW0IH98QXZlGsLLdw+F++2mFv Ab8k/lC6xjSZRfbL3Ka27d1s1m8go2g4FNNoEe3BpScKJyF5gUqNt5zGZTwN1ZwzaQXM lU6w== 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:subject:from:to:sender :dkim-signature; bh=GXlQB61mE8OaOHEhRh1X6yxCL7WhFzdYeqaOZoU7MXI=; b=tYyTk+AA5q8VRZYrCsKS/i6rD9i6QEzZZfeEBk4l9edS29ccn+Hnjaop5r9yhxTa3v EydReFXNivIvqv2lm0qJ7rOv1bwTxz+1PnW4+fF82mn4jvcBFefXQe15U/UuqmPkJhW4 NoHW+gWFzh2iGgORLtI33pjjamDJN9LKpiBoxgtYwv2hvQwH8DuS7VON1ueJg1CJ44Mo bXyUN7qWFORHgJBbqVyQ7uvCT5KPGm7pqQ77zWChQeW588ujuK4VYaL9WOaW+7Zj0jGf C3JlFRvPY+wug3nO9ZKRK/EY2NZihfq25YhRk5dXifF3BfyqfxCaIUI05Th7B/iDTWQ7 5uWQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=pass (google.com: domain of palmgren@math.su.se designates 2001:6b0:5:1213:250:56ff:fe94:7fa1 as permitted sender) smtp.mailfrom=palmgren@math.su.se DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:to:from:subject: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=GXlQB61mE8OaOHEhRh1X6yxCL7WhFzdYeqaOZoU7MXI=; b=nYerI7vhlBBjU5nQhBgFkFGLCctzNjEVp01DRPFDLglM/z+G3pTdcq6ByFV+UoE0oU Mqb+17/gwv0DI3W535RghrHaKsy7pPQHSpPsRehXx5FGj7V+STEcXpfsCA6/9w2gjHfA cu9bbEXMLDkYaSewUGlvs2rMujFwSv63R8oJ7jXSbiMomZ8WvwBbPnJuM8hiW1YQb5AM Zzez2hKQfncYDvkXDuJ6qaXjAblqjHi2dt7nikx1//g67W2M/WsuPpV6njx7wQqXQW2z eLaFvggg9K8spmINf3gpYgA3vZawBeSpBy4AeN5iwWQ9f24ClR1RHGnjyrF/WvH9dKKi Nt3g== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:to:from:subject: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=GXlQB61mE8OaOHEhRh1X6yxCL7WhFzdYeqaOZoU7MXI=; b=MtUMp6Hg4C//wsmCmGIVcwi1RmyTitgvpdPO5jub73Wqa7m8QWFEjv9r/wu+Z4rIl0 aYdPn/EJZaU29Pc8kdVYQITOQiroNNAr/v55Ds2iFJR5QFyHegCs6SAW2WjtFdn43NXG ZTdFzMk7btC5iSoFUyOU5ABFFGKRx2DmWvM0GCiTTIGhusaAKFt43Hp6g5y/uLfL0fwN r+nB9dB+jDVv0mSuQKbMhnrC+QhGpqOmCSzCqct98foq0QcRmH/WBheG6XKqAA+rWCRk p51mtctb7Jiqp4qzgWmUVr0KJy6iW3fs2h3t8KRje2jj6srFspzf5GUwnGqx42B1NzRp jiPw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAUWBJGwSqw1teX9dZ76NIybYv5g23U6BCboyvOmNcv6l1bJkagb 0Q0MLQm3P4JNlDsSpNJLK8c= X-Google-Smtp-Source: APXvYqztXa7xB1YOcazikoT7TjdOy/e6bFNhu9PuJ+A6iaxYHl8diTrhniG3Jd/NyDjmJUlSX+lM4Q== X-Received: by 2002:a2e:5bd8:: with SMTP id m85mr6505210lje.1.1551562416336; Sat, 02 Mar 2019 13:33:36 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a19:c3c6:: with SMTP id t189ls1093013lff.3.gmail; Sat, 02 Mar 2019 13:33:35 -0800 (PST) X-Received: by 2002:ac2:43d7:: with SMTP id u23mr382539lfl.12.1551562415628; Sat, 02 Mar 2019 13:33:35 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1551562415; cv=none; d=google.com; s=arc-20160816; b=eYLJmQleXqo0YcxAU6d6K+BauvFhySKJBzwnZwe8DXGhbH6xkKp6DRcED+rNGrNfZx F7snfec95d4ibFHuv5bKHamNumk1yEfdLUvrGi6humxcJOdfBBU6bneRv7eJwNqXjx4E Sza4XoLA5t/5TH2mtWfVO5Mu3ALve4kVHjKKiM9Mr7xvWILaVRsLXuulYIhm27tzgkd5 sE1OCZ3PBJtACGBWalmperPlQjupQUBwbw4svjgwfH0ELzBGjDacJ26L80ws/OMeU5sn yYbIqmcXMPCb3K3ouifOUzvAVU7gq4UwJqH92VKu2/+3cOj4R97bv4+/zB+CBp2c1D9A 4fFg== 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:subject:from:to; bh=BGBHqjN4RnVvYHSQ8BL14kn6NzT9PL9jzYNAUOIBwc4=; b=ZrFAdBG7e8/EsvoDDRu+uwl/huu6bMMvua0U+UsHBbDC94DzApqUcLt9MP0E2voioK qaf01IsaVOwHTYS0Y+dC+Ttr/WTrHhRIXWVD+/6In6prGRXWjDL+bTDDu56BzzU/xOJ2 aDlkN/19V0Ef4cPFrSanr263OXOGaYAzww9cQ736lROlQiiFGgTk4nuhNpRD2r+V6pmo OCKdBXGraa4gYgIyXm2MJJce3VK9PYV68T3kDwl8UNGFReo0ppuiKkk4lTvm107v7mcY 3hVcef/OXpH/HTPl+T0gTrAcp2PM9Z2WJGAL7KiOB1qDuMeBZ5lppimUlvG7ydL5Dj9P v+oQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of palmgren@math.su.se designates 2001:6b0:5:1213:250:56ff:fe94:7fa1 as permitted sender) smtp.mailfrom=palmgren@math.su.se Received: from mail-prod-route03.it.su.se (mail-prod-route03.it.su.se. [2001:6b0:5:1213:250:56ff:fe94:7fa1]) by gmr-mx.google.com with ESMTPS id a6si90967lfl.2.2019.03.02.13.33.35 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 02 Mar 2019 13:33:35 -0800 (PST) Received-SPF: pass (google.com: domain of palmgren@math.su.se designates 2001:6b0:5:1213:250:56ff:fe94:7fa1 as permitted sender) client-ip=2001:6b0:5:1213:250:56ff:fe94:7fa1; Received: from e-mailfilter02.sunet.se (e-mailfilter02.sunet.se [IPv6:2001:6b0:8:2::202]) (using TLSv1.2 with cipher ECDHE-RSA-AES128-GCM-SHA256 (128/128 bits)) (No client certificate requested) by mail-prod-route03.it.su.se (Postfix) with ESMTPS id 44Bffk6zxzzxc5; Sat, 2 Mar 2019 22:33:34 +0100 (CET) Received: from smtp.su.se (mail-prod-smtp04.it.su.se [IPv6:2001:6b0:5:132:250:56ff:fe94:2456]) by e-mailfilter02.sunet.se (8.14.4/8.14.4/Debian-8+deb8u2) with ESMTP id x22LXYOd192341 (version=TLSv1/SSLv3 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NO); Sat, 2 Mar 2019 22:33:34 +0100 Received: from Eriks-Palmgrens-MacBook-Air.local (c80-216-86-31.bredband.comhem.se [80.216.86.31]) (Authenticated sender: epalm) by smtp.su.se (Postfix) with ESMTPSA id 44Bffj6VQCz2tqQ; Sat, 2 Mar 2019 22:33:33 +0100 (CET) To: "constructivenews@googlegroups.com" , homotopytypetheory , Agda List From: Erik Palmgren Subject: =?UTF-8?Q?=5BHoTT=5D_A_setoid_model_of_extensional_Martin=2DL=C3=B6f_typ?= =?UTF-8?Q?e_theory_in_Agda?= Message-ID: <7149be09-1441-875f-b27d-47bd9feaf963@math.su.se> Date: Sat, 2 Mar 2019 22:33:33 +0100 User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.10; rv:60.0) Gecko/20100101 Thunderbird/60.5.1 MIME-Version: 1.0 Content-Type: text/plain; charset="UTF-8"; format=flowed Content-Language: sv Content-Transfer-Encoding: quoted-printable X-Bayes-Prob: 0.0001 (Score 0, tokens from: outbound, outbound-su-se:default, su-se:default, base:default, @@RPTN) X-CanIt-Geo: ip=2001:6b0:5:132:250:56ff:fe94:2456; country=SE; region=Stockholm; city=Stockholm; latitude=59.3600; longitude=18.0009; http://maps.google.com/maps?q=59.3600,18.0009&z=6 X-CanItPRO-Stream: outbound-su-se:outbound (inherits from outbound-su-se:default,su-se:default,base:default) X-Canit-Stats-ID: 0aXH9xycr - b5dfb4ee6929 - 20190302 X-CanIt-Archive-Cluster: PfMRe/vJWMiXwM2YIH5BVExnUnw X-Scanned-By: CanIt (www . roaringpenguin . com) X-Original-Sender: palmgren@math.su.se X-Original-Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of palmgren@math.su.se designates 2001:6b0:5:1213:250:56ff:fe94:7fa1 as permitted sender) smtp.mailfrom=palmgren@math.su.se 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, you may be interested in this development. It has been presented (in=20 preliminary form) at seminars at HIM Bonn, G=C3=B6teborg and Stockholm duri= ng=20 2018. "A setoid model of extensional Martin-L=C3=B6f type theory in Agda" Erik Palmgren Abstract. We present details of an Agda formalization of a setoid model of Martin-L=C3=B6f type theory with Pi, Sigma, extensional identity types, natural numbers and an infinite hiearchy of universe =C3=A0 la Russell. A= =20 crucial ingredient is the use of Aczel's type V of iterative sets as an=20 extensional universe of setoids, which allows for a well-behaved=20 interpretation of type equality. (Not mentioned in the talks: There is also a formalized set-theoretic=20 model of the calculus of constructions in Coq by Bruno Barras which=20 however use classical logic.) The the following link contains the Agda development (surely in need of=20 some cleaning up): http://staff.math.su.se/palmgren/From-type-theory-to-setoids-and-back.zip The README file should tell where to start. A write up of this is being prepared. Comments are welcome. Erik Palmgren --=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.