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=-0.9 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-lf1-x13e.google.com (mail-lf1-x13e.google.com [IPv6:2a00:1450:4864:20::13e]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 36356f19 for ; Thu, 5 Sep 2019 07:11:02 +0000 (UTC) Received: by mail-lf1-x13e.google.com with SMTP id w193sf322429lff.3 for ; Thu, 05 Sep 2019 00:11:01 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1567667461; cv=pass; d=google.com; s=arc-20160816; b=YD/BJovHbi3jMbHpv6hERQ9zcGhvqiVPncUe5POZfYZa2QQGUzgCdVZrweIqtVd5zq 0S38hx284/iM7+m4ODndtT5gYJaI5u6HJDRnZlKnhwKwid9ENNMBMYmH9T0IMbHoSxNM B97hI2Fh4mPgMN1a5yKLxUFVTHOrP4vPPYeZzAo2VDKI0Uv8OH9M0qHlXlHIMv7WExAR UyFZsZE8qxI+D1wK+XAbY9Zq81BHJYDmbCLL4PZcxugxSfTNjBI1UHvqbLZFalf1SQ5Z Ola8J2oCvl83wpchfZM+v3IOiIaUWRA96Ng+zTykNDKs2hf0cTweoeFHU6Qi4bivIBsh VkgA== 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:mime-version:content-language :accept-language:message-id:date:thread-index:thread-topic:subject :to:from:sender:dkim-signature; bh=tiepo/04svcVBnAYg7vSOVGfxc7w1IOsKqelrxZA7oY=; b=eiBnxp2yqtonGWaYvURpSm9eMcSGHt3rR6AcJguOf7gcr+oFjAg881nGR7G4ElNWs0 MXDvc1XaffZWK5CvsVUbvIDN7D5VrWhgyZRpl7o0SQSr+EGK88b8v/yxM7SP/LltvVfO Gp6NjPZtVOzs2o719nrQ/eF+riJmVwvE7tUPNxYU85oVCtaPFr1qCXFgkcNB3n4svqvw UoReSk4tidISBkgmFoc/8U6CEb/qzxWZZ5m+m91PeORsQu/4mIiatr3LPFCoLsb4o3i7 TFvBp55uVwfJ2GfM5xFuAR+7I/qzQ5gWms6Pl4lCnRHj9kg0TYTKLBb9h0yZLQq2mwcV HB0A== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=pass (google.com: domain of palmgren@math.su.se designates 77.238.36.174 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:from:to:subject:thread-topic:thread-index:date:message-id :accept-language:content-language:mime-version:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=tiepo/04svcVBnAYg7vSOVGfxc7w1IOsKqelrxZA7oY=; b=nzZH2uaWNNDsRoZWwFk0Rg6iAEJIWLTkJiao7PEa2VnjslSIw05XYtZgegWmnhVOW1 m9WCFWXr3n/scrodOW/EI5Q7URvm09R9MH0e/ADYI86dz4YmzXDJomECC+vjGSCkPtRu GJTv4B7snCCTto2/xAcmAS+2SRCHrGv6avondMuVYS5+Eq7eW9+2nRkenIN0maWHX0I1 iibCxQK+1v4uNw9kl/V0kdBoNylPWUjw38Yo7At+jxhkucWf2sSDCDEiUZoK42e0ZyAg J8h99Xy6Je0MDIvH8mc/h1SB66WpCNqi6hxUoFPdI4s6LUVUH4QoSBg4jXUDBO2L2rin qG2A== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:from:to:subject:thread-topic:thread-index :date:message-id:accept-language:content-language:mime-version :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=tiepo/04svcVBnAYg7vSOVGfxc7w1IOsKqelrxZA7oY=; b=p9pnUe2YiNE9zXabch7goE1IXiFj6L4k1YCyiWke0178E9dta3uGdhhEVVuL6KF8vE BVujzBkcxQU++BdhRwPkX6mdHesD5/QcJzkloUeZDPvFYIhhrh+URrKSSpVomlkxNuWP DRKewaS6h+ppA+EEPhKV/jzyoxwNhonpWARKFsEIaJc6oxIdSjnR753FGMNUYsNmKDHc mmVsvejNUN57kUdBRsD4iQ2W9S/id/fB1EgI0jwj4PhziK3Sc7LrXjI9ecpB1mwGlbkd io1+ArlLWG1RosyGCddEyWpEAJOVOUXce0d+qQlovI8QJAxGZd3ag+AdWA5BUJHVYeVT k6Sw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAVwNnynQ2fr6d140FgTg9P2j9KFmoftCBaap9Bo181mJcCZNMDF WRHtArGV5/WrFx6RJUrbYZM= X-Google-Smtp-Source: APXvYqyQRWxMBEjQR+YdH5CO6zNySO+B3Co2uR8qyzISldLnfGabBLxzJmQGUqQuiFMzFfJsfcm/aA== X-Received: by 2002:a2e:95cd:: with SMTP id y13mr981795ljh.188.1567667461166; Thu, 05 Sep 2019 00:11:01 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:ac2:54aa:: with SMTP id w10ls133634lfk.10.gmail; Thu, 05 Sep 2019 00:11:00 -0700 (PDT) X-Received: by 2002:ac2:52b6:: with SMTP id r22mr1313148lfm.19.1567667460499; Thu, 05 Sep 2019 00:11:00 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1567667460; cv=none; d=google.com; s=arc-20160816; b=MLyY/KobjqmjEvWvuawO0ZibPuppQ3Lwiqbo1338nL0rG29yKoao4htRwavif/azu0 TtPayog1T6U7Oi8hrj/s0F6IOlTgK9MKgDaN/lpRHo/9KIhrD7jjnt+2l04ABR0q8k4D YXTK2aetg20oYCNfKmMt0De8NZLUaUDEqXAXyFMTkdiiQOrFqhiN3AmocHaa+tP1B+hY MIJCgt90tDUg9jHHKf1OGuamSYZ7nx3NnTg2jKa91arMz1TQq/m979nsncnLqL1BCmF7 IFZlsQjFlz87rN0oiV46M7vYDpd8PhVx3GHC9vJQoMac2SfVf6cdrDkiDTCn0CCkVVwi rZ4Q== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:content-language:accept-language:message-id:date :thread-index:thread-topic:subject:to:from; bh=pkjNGue0buDFtmdtV+4NCoAN4pCo6pocE3G2Z8vRvx8=; b=vVKJv6Sr1wgM0hMH0cBeGLSeud3fhg8ZE2/D1ZO6n4UJscwaVHsDIFTDqRTjnqAWoY QKqLQ6ZAzCUaNkcSJZMDRu60inr5XlAdQYoRtG/c3exPbjElWEZ07mYFPZ+Vjmp17Fab cF0PwuyoeOikNO6SBol1+4RJ2c5kXxVqE8XJFbwvp358IOT+9QQz03Yr48EEyJeyV4ZQ uQnRyzXSitDQiH7l/gzA/oe4+6Gb6hUgY+aZI8PTE8vblKomO0XXrpPBkTU4oSS7hFsC eam0zJV68oLsJzQdNyPOY6PD0JK1VbHCPXUclYI6utMXStusOmX9wbcuevCNPD/wXgAS rM1g== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of palmgren@math.su.se designates 77.238.36.174 as permitted sender) smtp.mailfrom=palmgren@math.su.se Received: from mail-prod-route03.it.su.se (mail-prod-route03.it.su.se. [77.238.36.174]) by gmr-mx.google.com with ESMTPS id o30si60655lfi.0.2019.09.05.00.11.00 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 05 Sep 2019 00:11:00 -0700 (PDT) Received-SPF: pass (google.com: domain of palmgren@math.su.se designates 77.238.36.174 as permitted sender) client-ip=77.238.36.174; Received: from e-mailfilter01.sunet.se (e-mailfilter01.sunet.se [IPv6:2001:6b0:8:2::201]) (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 46PBg8060pz1Fys for ; Thu, 5 Sep 2019 09:11:00 +0200 (CEST) Received: from smtp.su.se (mail-prod-smtp04.it.su.se [130.237.181.99]) by e-mailfilter01.sunet.se (8.14.4/8.14.4/Debian-8+deb8u2) with ESMTP id x857AxKA080287 (version=TLSv1/SSLv3 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NO) for ; Thu, 5 Sep 2019 09:10:59 +0200 Received: from EBOX-PROD-SRV15.win.su.se (unknown [IPv6:2001:6b0:5:1162:85f3:6da2:459d:88c7]) by smtp.su.se (Postfix) with ESMTPS id 46PBg726HVz2v5s for ; Thu, 5 Sep 2019 09:10:59 +0200 (CEST) Received: from ebox-prod-srv13.win.su.se (2001:6b0:5:1162:f071:3d85:b2d0:c2f6) by EBOX-PROD-SRV15.win.su.se (2001:6b0:5:1162:85f3:6da2:459d:88c7) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256) id 15.1.1713.5; Thu, 5 Sep 2019 09:10:59 +0200 Received: from ebox-prod-srv13.win.su.se ([fe80::f071:3d85:b2d0:c2f6]) by ebox-prod-srv13.win.su.se ([fe80::f071:3d85:b2d0:c2f6%2]) with mapi id 15.01.1713.007; Thu, 5 Sep 2019 09:10:59 +0200 From: Erik Palmgren To: "homotopytypetheory@googlegroups.com" Subject: =?UTF-8?Q?=5BHoTT=5D_New_preprint_=3A_A_model_of_Martin=2DL=C3=B6f_extensi?= =?UTF-8?Q?onal_type_theory_with_universes_formalized_in_Agda_=28=09arXiv=3A1?= =?UTF-8?Q?909=2E01414=29?= Thread-Topic: =?utf-8?B?TmV3IHByZXByaW50IDogQSBtb2RlbCBvZiBNYXJ0aW4tTMO2ZiBleHRlbnNp?= =?utf-8?B?b25hbCB0eXBlIHRoZW9yeSB3aXRoIHVuaXZlcnNlcyBmb3JtYWxpemVkIGlu?= =?utf-8?Q?_Agda_(=09arXiv:1909.01414)?= Thread-Index: AQHVY7kRsTiI+rDAAkyvuDxj9yW6cQ== Date: Thu, 5 Sep 2019 07:10:58 +0000 Message-ID: <6AC5AAA7-297B-4644-A116-4182A0FC935E@math.su.se> Accept-Language: sv-SE, en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: x-mailer: Apple Mail (2.3124) x-originating-ip: [130.237.154.251] Content-Type: multipart/alternative; boundary="_000_6AC5AAA7297B4644A1164182A0FC935Emathsuse_" MIME-Version: 1.0 X-Bayes-Prob: 0.0001 (Score 0, tokens from: outbound, outbound-su-se:default, su-se:default, base:default, @@RPTN) X-CanIt-Geo: ip=130.237.181.99; country=SE; region=Stockholm; city=Stockholm; latitude=59.3333; longitude=18.0500; http://maps.google.com/maps?q=59.3333,18.0500&z=6 X-CanItPRO-Stream: outbound-su-se:outbound (inherits from outbound-su-se:default,su-se:default,base:default) X-Canit-Stats-ID: 090VHaXW2 - 0d6e805f6382 - 20190905 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 77.238.36.174 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: , --_000_6AC5AAA7297B4644A1164182A0FC935Emathsuse_ Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable >From type theory to setoids and back Erik Palmgren (Submitted on 3 Sep 2019) A model of Martin-L=C3=B6f extensional type theory with universes is formal= ized in Agda, an interactive proof system based on Martin-L=C3=B6f intensio= nal type theory. This may be understood, we claim, as a solution to the old= problem of modelling the full extensional theory in the intensional theory= . Types are interpreted as setoids, and the model is therefore a setoid mod= el. We solve the problem of intepreting type universes by utilizing Aczel's= type of iterative sets, and show how it can be made into a setoid of small= setoids containing the necessary setoid constructions. In addition we interpret the bracket types of Awodey and Bauer. Further quo= tient types should be interpretable. Comments: 30 pages Subjects: Logic (math.LO) MSC classes: 03B15, 03B35, 03E70, 03F50 Cite as: arXiv:1909.01414 [math.LO= ] (or arXiv:1909.01414v1 [math.LO= ] for this version) https://arxiv.org/abs/1909.01414 --=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/6AC5AAA7-297B-4644-A116-4182A0FC935E%40math.su.se. --_000_6AC5AAA7297B4644A1164182A0FC935Emathsuse_ Content-Type: text/html; charset="UTF-8" Content-ID: <7AEB0CEF7F799F42B9B5F715ED2AEDC4@win.su.se> Content-Transfer-Encoding: quoted-printable


From type theory to setoids and= back

Erik Pa= lmgren
(Submitted = on 3 Sep 2019)
A model of Martin-L=C3=B6f extensional type theory with universes is formal= ized in Agda, an interactive proof system based on Martin-L=C3=B6f intensio= nal type theory. This may be understood, we claim, as a solution to the old= problem of modelling the full extensional theory in the intensional theory. Types are interpreted as setoids, and th= e model is therefore a setoid model. We solve the problem of intepreting ty= pe universes by utilizing Aczel's type of iterative sets, and show how it c= an be made into a setoid of small setoids containing the necessary setoid constructions. 
In addition we interpret the bracket types of Awodey and Bauer. Further quo= tient types should be interpretable.
Comments: 30 pages
Subjects: Logic (math.LO)
MSC classes: 03B15, 03B35, 03E70, 03F50
Cite as: arXiv:1909= .01414 [math.LO]
  (or arXiv:1909.01414v1 = [math.LO] for this version)



htt= ps://arxiv.org/abs/1909.01414

--
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://groups.google.com/d/ms= gid/HomotopyTypeTheory/6AC5AAA7-297B-4644-A116-4182A0FC935E%40math.su.se.
--_000_6AC5AAA7297B4644A1164182A0FC935Emathsuse_--