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-ot1-x337.google.com (mail-ot1-x337.google.com [IPv6:2607:f8b0:4864:20::337]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id b2b3ce67 for ; Mon, 18 Feb 2019 19:22:23 +0000 (UTC) Received: by mail-ot1-x337.google.com with SMTP id k12sf15629259otk.12 for ; Mon, 18 Feb 2019 11:22:23 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1550517742; cv=pass; d=google.com; s=arc-20160816; b=xFPVqRdEFlG8Z7MHHqWAmgXsvbxdswLEkUm9AxQCUIdXRMOvvPr5rfWzLb3dzY1dMP MG5YQSDd6+GAbx3Y9j0OZmeJPpQ66oTxU0ylWU6rOUxV7SrK2hyrfaD/wi6YJATPh1rf V9lhHdjBKg3Dvv5G1ajEosOmNnsq9bk477Yemute8Edcu48EaizMGbJLaMj89u6kWoyE JH9TdEY8IcDK6lL0Uuom1duA/RxFers7YBJIB98X2qHO90Zmy3EwIsyuhOT1VcY+aw42 h+fXDDKuLMB0MkTjFhO+e3pGSuB6qdRERqmVrpR6nF1iUM+XWx1gIZHSlmsMgLFJoIqv HycQ== 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-transfer-encoding :content-id:content-language:accept-language:in-reply-to:references :message-id:date:thread-index:thread-topic:subject:cc:to:from:sender :dkim-signature; bh=XieqC5WMp/TCLMOQVr+lkAaaW7Jnv6j2pLzH5giidyw=; b=F58VbLcQ3Yyhvliz8PEzfB0wz3NPzInRbbnY2guPCUqP7UZBnP9Jp/71OVAKJkSFMV 72ASDCS6oy5Gpd1ijZliH4hKKIJzvdqRt3nUKZj7rJbLHvcR+SJII8XNGEeVmrpmFppI 5Lk1+VDk/AZ8cIZYbqgveTbSrczwg12v7NGIW87NU9FBh0XtuONUd8ynAu/wQtOI/EV0 i92o3pLO4KOdI65GSs0O723fEY1mwQgZ8AGjeTZqolPlb4V/B5ICgk+yZdX80w8xOELk LFmtTkibqcqqYZs54W0WzB1TfUsG9UEbQN57ZnXLuimhlb+pvOxTbXYLxbsv5zzJE9Ft Kltw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@wesleyan.edu header.s=selector1 header.b=iyaHu+7B; spf=pass (google.com: domain of dlicata@wesleyan.edu designates 40.107.72.138 as permitted sender) smtp.mailfrom=dlicata@wesleyan.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:from:to:cc:subject:thread-topic:thread-index:date:message-id :references:in-reply-to:accept-language:content-language:content-id :content-transfer-encoding:mime-version:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=XieqC5WMp/TCLMOQVr+lkAaaW7Jnv6j2pLzH5giidyw=; b=A4l72YU+3fuCzoRYVLA8C8NUXWAdXj7y2UlHESj+brBAWhGRA8rv3dKahXVBRkjqAe N3vxVfrA/o3x0hZfjUXbC/fCRGHamFFafouFGNnQ4ThjxVa5Ncu2tGxBOqsRi5jGDWsO a7RJLfTH6sgfRQPJrc6f+aXr3AGdnRRXvM0dbxkj5cxQJzpN3lxndMoi1doQ+lo0mtwu Frn5Zf7UIDku1lV+DRLhSmgg4UNAtDxpSwOzAZ1Q6F2gEkbpt7rMqXP30mFHKZX5V4q0 ZFEyWKMVki94YObGWgpyGEAUm+rdRiF4Ychu6QoJDlCQaIGq9KJfZfLj7bkmUIVG51zM YR8w== 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:cc:subject:thread-topic :thread-index:date:message-id:references:in-reply-to:accept-language :content-language:content-id:content-transfer-encoding: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=XieqC5WMp/TCLMOQVr+lkAaaW7Jnv6j2pLzH5giidyw=; b=t+3IVdu/9QVx+tHSwqiGqZG5PjuV6y9FgCPvgLu9r25o/EQxVfV0yDiZxZfrJujVV8 ShTBJzH1SlSiCOJjEbP8pAUPEaLjA9ictLQoJSQeMmbkqMaZ/1aL2TsaTYZTErh0pf1+ 6u2ycXWYUtF2mBuZMDJa9z7FAHJypZNaQdWjdQLFn8fw6IaWeCIKaCbHWBwP0Q9eF1uP hnLgQb+k47LGe6zjgJtiqR4kNjxnw8aHzEFAAkALqgh9XOz8GOp50Icdkoi3esuxN/4r 5qI0GXJ/zP4aBpXoy4BpK68U44eqj3Z2omRtQsBoEUhCHbi2X0gR+45Re6y9b9cUv2rA 16Fw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAua9CiovD85SmG9DgZEa91YXkWclgVhYKPj0J0NqQTCK3rrIaQif CeLAEP8+5WX/jpXGpkdtk3Q= X-Google-Smtp-Source: AHgI3IZTlZPmJRXONhyFuYh3YpxrB69fSwHTn05WePFDHGH6qWx6u4SrbXCwOMg74eFBepgrPsgUzA== X-Received: by 2002:a9d:518e:: with SMTP id y14mr239127otg.2.1550517742681; Mon, 18 Feb 2019 11:22:22 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a54:4605:: with SMTP id p5ls7993810oip.0.gmail; Mon, 18 Feb 2019 11:22:22 -0800 (PST) X-Received: by 2002:aca:1e01:: with SMTP id m1mr13448874oic.0.1550517742404; Mon, 18 Feb 2019 11:22:22 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1550517742; cv=none; d=google.com; s=arc-20160816; b=efv2pR/fZpdZEvT3gND1aVDUHp0NN9TawlRvuboz1kHhsE/WMOi6/b7ikaPtiLHRFk JICOO4Nhnc9F4r/rKZi5SRNU69NFGmvxyQlFm6GULuvHq8pn0KGbh7CrN9dQYt90QCdd kUTYN2ue8CsZ8yrOE3IgdKJlpoOOlEdyeMMpujwIZ21/fdmKMUot1FGaCTwVglaYMbNt GOmkN/HoZ0ooLyWjXBHTZNPtqv/pC4x34mubEpeq3wReG1A3d4D/8RH8nwv6H+aXMkwE 2vmckB1ffe8bojMpa3FyAKsGfcjoJS4Drk4dPdLitecqCkxWpguRBPea5oFO946hm4qb tQ2Q== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:content-transfer-encoding:content-id:content-language :accept-language:in-reply-to:references:message-id:date:thread-index :thread-topic:subject:cc:to:from:dkim-signature; bh=YYH2RhEJKmvqe/Y4+li5tAIUu8h0zU/BjyPtJ7ufjyQ=; b=zsfUogjHnn32//1PXzcmEIXx+wP+GlzW1PJxEsbNQHk3N/vm7oUBcTtSeEiu8PunMi Tuhpek2F07O0vYYGdTsOIgpB6CxOzho8Gp5CvyTXrhKVL/JpdEV8eLpCz/ig5aeWBXiO jbeLf/TErCmsc4aSm6cwfr18p/+Zplgxk/Ecq/HMM08ir9heTfEFG+3vfGMDWPfZvezg Hn3yGwr2+XbsfaB9fDJSZuiEcXizG6UMmD/Rgc7Xcg+fbnhmhD5SVgP5/a38XuwWMH+d HZagY25+vRofnjQsYII+kKbcIpcMOGRboDiTsTtDkg+mYT91CnXJXoT1i0ysikAW6otN zvVg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@wesleyan.edu header.s=selector1 header.b=iyaHu+7B; spf=pass (google.com: domain of dlicata@wesleyan.edu designates 40.107.72.138 as permitted sender) smtp.mailfrom=dlicata@wesleyan.edu Received: from NAM05-CO1-obe.outbound.protection.outlook.com (mail-eopbgr720138.outbound.protection.outlook.com. [40.107.72.138]) by gmr-mx.google.com with ESMTPS id l92si272586otc.4.2019.02.18.11.22.22 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 18 Feb 2019 11:22:22 -0800 (PST) Received-SPF: pass (google.com: domain of dlicata@wesleyan.edu designates 40.107.72.138 as permitted sender) client-ip=40.107.72.138; Received: from BN3PR04MB2195.namprd04.prod.outlook.com (10.167.4.13) by BN3PR04MB2354.namprd04.prod.outlook.com (10.174.64.147) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.1622.16; Mon, 18 Feb 2019 19:22:19 +0000 Received: from BN3PR04MB2195.namprd04.prod.outlook.com ([fe80::c5bb:40e2:9fba:ab5e]) by BN3PR04MB2195.namprd04.prod.outlook.com ([fe80::c5bb:40e2:9fba:ab5e%8]) with mapi id 15.20.1622.020; Mon, 18 Feb 2019 19:22:19 +0000 From: "Licata, Dan" To: =?utf-8?B?TWFydMOtbiBIw7Z0emVsIEVzY2FyZMOz?= CC: Homotopy Type Theory Subject: Re: [HoTT] Re: Why do we need judgmental equality? Thread-Topic: [HoTT] Re: Why do we need judgmental equality? Thread-Index: AQHUx7CdYqfVw+3Xi0mp7irBTonfqaXl73MA Date: Mon, 18 Feb 2019 19:22:19 +0000 Message-ID: References: <1a3dfba4-816a-42c3-8eea-1a2906cb1cad@googlegroups.com> <7c3967cd-6ea6-4008-908b-e80928240d66@googlegroups.com> In-Reply-To: <7c3967cd-6ea6-4008-908b-e80928240d66@googlegroups.com> Accept-Language: en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: x-originating-ip: [24.60.108.192] x-ms-publictraffictype: Email x-ms-office365-filtering-correlation-id: c162b5da-c3d1-4e37-83cc-08d695d666ba x-microsoft-antispam: BCL:0;PCL:0;RULEID:(2390118)(7020095)(4652040)(8989299)(4534185)(4627221)(201703031133081)(201702281549075)(8990200)(5600110)(711020)(4605104)(2017052603328)(7153060)(7193020);SRVR:BN3PR04MB2354; x-ms-traffictypediagnostic: BN3PR04MB2354: x-ms-exchange-purlcount: 1 x-microsoft-exchange-diagnostics: =?utf-8?B?MTtCTjNQUjA0TUIyMzU0OzIzOjhoQW5SNFVkRnpkelZCNGh6ZzhnSnRQby82?= =?utf-8?B?eVBKdmZYY1IvTmkzcWFtWG9salg4Q0o2WUtvcElEYWRmbWw5N0VldjFVb3VE?= =?utf-8?B?eitKZGNwT3QrY2NZZjlVM2ZQaWxJMElZa2lqelgrRmlFZ3cvd1ZWUy9IL0p4?= =?utf-8?B?U3RKcjZLU2RVc1J0TVdEMDROejJKRURoaTludjA1RXpIV01udHdEb1ZsZmp2?= =?utf-8?B?eThjR2FGYUJSbjJNRi9ZKzVQMmFFaUs3bnE3amcvUHhieWR1d1dsVFgwQTBS?= =?utf-8?B?VWwrbFVrV3dOd3hZV0YyMGhBVmRWT0ZjTDJYb2RRQXZDb3Y3UlNCeFE2ZERN?= =?utf-8?B?YjRQNXRZSGxpWW1LZWFwamhTSnVUOG11NndBTmlqTVRxeUVWWXVhYytOR1JT?= =?utf-8?B?cDk4V0hOOXRISEtJZTZweXNVL25aS3pISVRxQ051dGFtanlWd0czd1hhMUYy?= =?utf-8?B?ZktRVGRxRlhCaWM5M3ZYeTFYejBpaFBmc09CdVUrZEZ5cDRHSFRRdGdPa0JW?= =?utf-8?B?MUtzdTRsTHIwZ2JQZlV4TWcyK2h5d2haMXdWeU5RTDBmMkJ0T09BVVdsVDIw?= =?utf-8?B?UDJUWDJQUWdtdE50WHRCU3QzUkJLSGlZU01DTHFVVU1EbWl0MHFFMkhOdDhZ?= =?utf-8?B?aHJyUzBaeTlVTWRvdzBvQWZhdTVSSExFb3V0TGVGMEFVSVlxOTBFOE10Q0JN?= =?utf-8?B?WHFXVjRCd2YrVk9TK2Zaa3N6SDRyc3JwNUFXMXVYVDJFYzZ4Uk5PNFhtV2k5?= =?utf-8?B?bFBta2dOemtSOWxBWFMxK3pURmNVTENzZ0VNUWtPVjg3VThRZlNSb3NzTWFs?= =?utf-8?B?cEVmL3N1QzhqdUYrbDZVaW5TRkpQWWtreVdESzdkWitybHVGN01LbGRvNm1V?= =?utf-8?B?UUxyMTJ6WU1vSDNjVGlWTGd6cHFFNjJTcnVPYTd0L0xiNlBtVXJyeGRBRkxw?= =?utf-8?B?NlJQcXVvZkZ3TmZPL2QwMktkM2x2WFVJblhsT3UydDV1RHdNV2dCS2dZejh4?= =?utf-8?B?MlRnSjVUMlVoMFZNcEFNb0Flc052VS92UFc3YkNaVk41UndwSWdvNnhkWU10?= =?utf-8?B?amxRNys0dXFHZUtvR0svQktESWVVRTVkeUVYY000NThKd29sa0lYMUhRelRF?= =?utf-8?B?M2hWekpDVnpIVFhPbUFoZGVLWmRDS0V4N0JvOVZiKzdBYncxMVdMcDBwRm1C?= =?utf-8?B?TzkzS0dvU0o2VEtWRGdXRUFEZEZYa20zNzUwL3M0eHUvOEp1WVNSSkdCSmJJ?= =?utf-8?B?czZ1QzFXcWY2OHVHS0YwL3pzWi9HazJWRklIY29tQUhSMURvRnZtUjIwdTBD?= =?utf-8?B?MlNUVDZoeGt1Q3RwbWpIM29yOVhCWWtXdDVLZUlidzVTL0VNbFBSYlNoMUhk?= =?utf-8?B?SldTWWNtVjlHdDJRYy9pWml3L0x2SnAwRUpuSm9DbHd3MzhEWEhoRlQyOXBF?= =?utf-8?B?bk1VVy9YTGNLbURwampQUTZFd3hGUTNzWGwyblZNenR5VzNNb1lGMzB2VlU0?= =?utf-8?B?dm1uMGRDaCtJTjQzZ3dTcnVybkpvdUhHQmN1ZHE0RDJjKzBFN3BncU9UOE9a?= =?utf-8?B?NzhJQ08xdjhMTTFjV1lQVTkvdlErVnIyQS8rTi9rUGNLYUttMlZpWi9xWEw0?= =?utf-8?B?OUMrZ1Y5YTVITGw4WkVqZHlKM2dSVUdONU1NWlJjNGxyaEhTYlhndHJWMGN0?= =?utf-8?B?UWRycmtPbXU3TWRIOEdzdGdkbEdxL1RlQXB1UGNHZ1dLN3Y0T25UMFpydEZj?= =?utf-8?B?Y1VwSnozWENSL2phQ3pjamNpd2ZCTzNXb1E2d290d2RLeWo4NWIwWW5FaklY?= =?utf-8?B?VHRzUjdsR0lFQUlqakxocGk3eWJDTzJENlpBVXlqcWlVRnc9PQ==?= x-microsoft-antispam-prvs: x-forefront-prvs: 09525C61DB x-forefront-antispam-report: SFV:NSPM;SFS:(10019020)(39850400004)(136003)(366004)(346002)(376002)(396003)(189003)(199004)(486006)(4326008)(14444005)(66574012)(5660300002)(476003)(82746002)(305945005)(14454004)(6246003)(256004)(446003)(97736004)(11346002)(75432002)(25786009)(6486002)(6506007)(53546011)(966005)(88552002)(6512007)(76176011)(8936002)(6306002)(71200400001)(2616005)(36756003)(86362001)(102836004)(33656002)(81166006)(2906002)(81156014)(53936002)(71190400001)(186003)(786003)(316002)(99286004)(8676002)(478600001)(6436002)(105586002)(106356001)(83716004)(6916009)(229853002)(7736002)(6116002)(3846002)(68736007)(66066001)(26005);DIR:OUT;SFP:1102;SCL:1;SRVR:BN3PR04MB2354;H:BN3PR04MB2195.namprd04.prod.outlook.com;FPR:;SPF:None;LANG:en;PTR:InfoNoRecords;MX:1;A:1; received-spf: None (protection.outlook.com: wesleyan.edu does not designate permitted sender hosts) x-ms-exchange-senderadcheck: 1 x-microsoft-antispam-message-info: Fr3KFaxa4+4EskfKBN9ZWytS5tm/vYkMXTkAJ6G8Ij/szjYNlxa/b1vK6RUyUd9ZrmbVO6lpveKNs0/AWOAWZVo2DwXH10YHhumqLz/5MI5FvdBsJGOYWKRJRg8nIju/k/No/neixezFpTMVp0COfHUDxGo4BAD+eMAR/T2nwr6iFIgwOxO5Bo1Qr8MZ5qgUhnt+tMC5fGbQSqgvhlzki8KVQhjCnRkISyC63OFib/i7FZB5vaM9ORsfyf+Dwm4jfAmdwsOAA9yHcZuAf4wpavb7nnaNH4MWoegDApxEpEKD9cFzLmc+Os4Zb1fEdNnSb9Pb3J6BaXLSeyeP1TD0/QuYDpKU/f/+Nim3zVkfXkH/T86ELY3rlUF+gnQPCGBPeC9AsTKVLIAWEB4GxGM3QckblpeZO6eNO/3sT9m55fQ= Content-Type: text/plain; charset="UTF-8" Content-ID: <5588FF4918DA00459F9109C2CBF39577@namprd04.prod.outlook.com> Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-OriginatorOrg: wesleyan.edu X-MS-Exchange-CrossTenant-Network-Message-Id: c162b5da-c3d1-4e37-83cc-08d695d666ba X-MS-Exchange-CrossTenant-originalarrivaltime: 18 Feb 2019 19:22:19.7282 (UTC) X-MS-Exchange-CrossTenant-fromentityheader: Hosted X-MS-Exchange-CrossTenant-id: a9fd6c79-6d71-49f3-9111-0c8e591dc3d1 X-MS-Exchange-CrossTenant-mailboxtype: HOSTED X-MS-Exchange-Transport-CrossTenantHeadersStamped: BN3PR04MB2354 X-Original-Sender: dlicata@wesleyan.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@wesleyan.edu header.s=selector1 header.b=iyaHu+7B; spf=pass (google.com: domain of dlicata@wesleyan.edu designates 40.107.72.138 as permitted sender) smtp.mailfrom=dlicata@wesleyan.edu 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: , Hi, I=E2=80=99m confused =E2=80=94 does it even type check to ask pr=E2=82=82 = (x , y) =E2=89=A1 y ? I would expect=20 x : A y : B(x) (x,y) : =CE=A3 A B fst (x,y) : A snd (x,y) : B(fst (x,y)) so if beta for fst is weak, then pr=E2=82=82 (x , y) =E2=89=A1 transport Y (p =E2=81=BB=C2=B9) y is the best you could hope for. I.e., you have a path for the first beta, = and a path over it for the second. =20 -Dan > On Feb 18, 2019, at 12:37 PM, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 wrote: >=20 > On Friday, 8 February 2019 21:19:24 UTC, Mart=C3=ADn H=C3=B6tzel Escard= =C3=B3 wrote: > why is it claimed that definitional equalities are essential to dependen= t type theories? >=20 > I've tested what happens if we replace definitional/judgmental > equalities in MLTT by identity types, working in the fragment of Agda=20 > that only has =CE=A0 and universes (built-in) and hence my =CE=A0 has its= usual=20 > judgemental rules, including the =CE=B7 rule (but this rule could be disa= bled). >=20 > In order to switch off definitional equalities for the identity type > and =CE=A3 types, I work with them given as hypothetical arguments to a m= odule > (and no hence with no definitions): >=20 > _=E2=89=A1_ : {X : =F0=9D=93=A4} =E2=86=92 X =E2=86=92 X =E2=86=92 =F0= =9D=93=A4 -- Identity type. >=20 > refl : {X : =F0=9D=93=A4} (x : X) =E2=86=92 x =E2=89=A1 x >=20 > J : {X : =F0=9D=93=A4} (x : X) (A : (y : X) =E2=86=92 x =E2=89=A1 y =E2= =86=92 =F0=9D=93=A4) > =E2=86=92 A x (refl x) =E2=86=92 (y : X) (r : x =E2=89=A1 y) =E2=86= =92 A y r >=20 > J-comp : {X : =F0=9D=93=A4} (x : X) (A : (y : X) =E2=86=92 x =E2=89=A1 = y =E2=86=92 =F0=9D=93=A4) > =E2=86=92 (a : A x (refl x)) =E2=86=92 J x A a x (refl x) =E2= =89=A1 a >=20 > =CE=A3 : {X : =F0=9D=93=A4} =E2=86=92 (X =E2=86=92 =F0=9D=93=A4) =E2=86= =92 =F0=9D=93=A4 >=20 > _,_ : {X : =F0=9D=93=A4} {Y : X =E2=86=92 =F0=9D=93=A4} (x : X) =E2=86= =92 Y x =E2=86=92 =CE=A3 Y >=20 > =CE=A3-elim : {X : =F0=9D=93=A4} {Y : X =E2=86=92 =F0=9D=93=A4} {A : = =CE=A3 Y =E2=86=92 =F0=9D=93=A4} > =E2=86=92 ((x : X) (y : Y x) =E2=86=92 A (x , y)) > =E2=86=92 (z : =CE=A3 Y) =E2=86=92 A z >=20 > =CE=A3-comp : {X : =F0=9D=93=A4} {Y : X =E2=86=92 =F0=9D=93=A4} {A : = =CE=A3 Y =E2=86=92 =F0=9D=93=A4} > =E2=86=92 (f : (x : X) (y : Y x) =E2=86=92 A (x , y)) > =E2=86=92 (x : X) > =E2=86=92 (y : Y x) > =E2=86=92 =CE=A3-elim f (x , y) =E2=89=A1 f x y >=20 > Everything I try to do with the identity type just works, including > the more advanced things of univalent mathematics - but obviously I > haven't tried everything that can be tried. >=20 > However, although I can define both projections pr=E2=82=81 and pr=E2=82= =82 for =CE=A3, and > prove the =CE=B7-rule =CF=83 =E2=89=A1 (pr=E2=82=81 =CF=83 , pr=E2=82=82 = =CF=83), I get >=20 > p : pr=E2=82=81 (x , y) =E2=89=A1 x >=20 > but only >=20 > pr=E2=82=82 (x , y) =E2=89=A1 transport Y (p =E2=81=BB=C2=B9) y >=20 > It doesn't seem to be possible to get pr=E2=82=82 (x , y) =E2=89=A1 y wit= hout further > assumptions. But maybe I overlooked something. >=20 > One idea, which I haven't tested, is to replace =CE=A3-elim and =CE=A3-co= mp by > the the single axiom >=20 > =CE=A3-single : > {X : =F0=9D=93=A4} {Y : X =E2=86=92 =F0=9D=93=A4} (A : =CE=A3 Y =E2= =86=92 =F0=9D=93=A4) > =E2=86=92 (f : (x : X) (y : Y x) =E2=86=92 A (x , y)) > =E2=86=92 is-contr (=CE=A3 =CE=BB (g : (z : =CE=A3 Y) =E2=86=92 A z) > =E2=86=92 (x : X) (y : Y x) =E2=86=92 g (x , y) = =E2=89=A1 f x y) >=20 > I don't know whether this works. (I suspect the fact that "induction > principles =E2=89=83 contractibility of the given data with their computa= tion > rules" is valid only in the presence of definitional equalities for > the induction principle, and that the contractibility version has a > better chance to work in the absence of definitional equalities.) >=20 > One can also wonder whether the presentation taking the projections > with their computation rules as primitive, and the =CE=B7 rule would > work. But again we can define =CE=A3-elim but not =CE=A3-comp for it. >=20 > In any case, without further identities, simply replacing definitional > equalities by identity types doesn't seem to work, although I may be=20 > missing something. >=20 > Martin >=20 >=20 >=20 >=20 > --=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= email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. --=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.