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-lf1-x13c.google.com (mail-lf1-x13c.google.com [IPv6:2a00:1450:4864:20::13c]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 8f8a171a for ; Sun, 17 Feb 2019 14:14:54 +0000 (UTC) Received: by mail-lf1-x13c.google.com with SMTP id y13sf1578773lfg.14 for ; Sun, 17 Feb 2019 06:14:54 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1550412894; cv=pass; d=google.com; s=arc-20160816; b=0wum+xQH+gtbHt8/eI4kMl6Juc8CWJyslY/hd/iD5VyAgQYg4dVAjpZrPwW8GphOyw XDZT/Zwznf90FZQPbUiFg83IeG62eZlTUcbFN9zbr/DhaHLaghzMy3/ZsvyC9B8Q6WgX SSBaWRcuHBYVnuk4V0DOK7OVHQDqbxo+lGp3P6N0rzokSW8GjFAl+BwV2sV3BzUSnfgw k4nhE3DQrk1pMMEmnWFutFzQ/+RvhEP/ZIeheMRoQTGopMzv109Lq04W6JcfU1h3WiYY QWj67X6zPXJqIrjMasXwTGzo9teSyreuw8CeCLftS3xDd/uZjVUjgfbVSVHbxPNFZrYU jA5A== 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:to:from:sender :dkim-signature; bh=m7O0ZHOqJjx5juZH6xvg4EHvZuv0uceIESZjRRHitO0=; b=IdOGwdznb59/pSPwFU9FQQHZ+Q/pPaGoL7QQA5ITnqwgVTPDUNFjIwVMJmoCIYgnI9 NOZb1m6QbXyEEgPnDsrkp6LgdOrswXrIYC90qHK9oAxj7MGDYsadFaL8GmRp2vPTl5Vg yWWMopLB7TRqiSWbWqyDz/9sPUuxZilhfd91bXRh1AkgKoJxU88Rm90Ej1vbN8+35pBV 7uBVOpxZA4BnjWsEi63vn20XgjUnPEAlSLJ+Oil2nEOb+eAMUyaCJl9bPjV1YY8U8LcQ akinFPwofPeKhTbGSQqecO0QfG6VCsKZWrfmaWggwLEhthdD4IarJQonRfBq5ABd4ojX waUQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@wesleyan.edu header.s=selector1 header.b=VxgS8hBv; spf=pass (google.com: domain of dlicata@wesleyan.edu designates 40.107.82.95 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: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=m7O0ZHOqJjx5juZH6xvg4EHvZuv0uceIESZjRRHitO0=; b=VQJSZ78aT8dzr42khYT+Fc6Ar9PAdXX4ACxEJ6Zr8QEiReolChR18+fOlu4s2VCpN9 jpcGOs7W84cfvWwZXi5G8Tj3tbUjd/lNjSnS7bhWVSr3VabDKOeavsZTf1K7Ev8xE32X OPMmbsTww3zN2OPo/1Pjh9g0FwXeldAdxWFpU+ToRafRsMmnXdTKfxZmwlS82HJYFHoj OHRbwfVWzCiKCwVwi68aza0bgyp+1i5JrwMf1sAF2jnlSttQkJIq0HHOPt5OOGQ9k0B+ USyqA+eZ8MdD3ajyfn1L0BazCoeng6i2+JIrbsGWPTezFLbpQZZOyytW3be4CCdpE2U0 Be3A== 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: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=m7O0ZHOqJjx5juZH6xvg4EHvZuv0uceIESZjRRHitO0=; b=qongE1ijNoruT4DVMBv9/F9cWqfkLO3LpoL9m2/UmLDIEodJ0NTjstpTEjwA47rTiT Wm9t+k2VOYYOWoQRaNSqdDps+Ia19NST5A5qTP9wpm5+oK2rLORlupptGBETIv2hF9Zw 9pJ0a4eBUtjNIIxFSYwIL3iE+L7GYw7YztVwkAe1Q5fqgeFjacVjaixYLWGTwg/fnR3Y lq8oMrWZ3OBtH0xyTLcvee5te1vxEDEftVR+4DgW/zuThZUCskY/YyGaRPCwJkrDC34J Zfpt0UZmt++3GNTABXEcAHlcEvMpuDrediONk9NGZ0yE+i1xC4Hqtsn69zLZd23htptf nWaw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAubgoZx35IFfA/pyvR1PqFrTCHjNgHJb0ap8WmWKs+f5J2DZWoVA 3uBkAxXG4wYSB+Aqw29Fy18= X-Google-Smtp-Source: AHgI3IYRJK3ibYS45cU/APUiLTs/GW+Ov1AYbp3VFrSM0lF0ipQSs3Lkb9X9a7o5nLLRHP+mJIXqoA== X-Received: by 2002:ac2:519a:: with SMTP id u26mr6254lfi.6.1550412894047; Sun, 17 Feb 2019 06:14:54 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a2e:9a18:: with SMTP id o24ls43936lji.3.gmail; Sun, 17 Feb 2019 06:14:53 -0800 (PST) X-Received: by 2002:a2e:3a08:: with SMTP id h8-v6mr1019712lja.6.1550412893337; Sun, 17 Feb 2019 06:14:53 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1550412893; cv=none; d=google.com; s=arc-20160816; b=IJilg03lzRnBCUujvIf+NA13/1fPcgMj/py1PWLs6q+BRtPD/vLwut8z1iSzESxbwP DU1Y2cR1n8zeQ2o2OBiSE3NVT0BRMH20fvrDB0QhRbvyck/aw0aSfG3QNuroh7htKgXw EjCa3MsAYKtJC6UPOU+VNGqtV2E6New2+uoEgEYYEJIgKST+GpDmCfgTiYoZVBhbEDn6 BWK1dUHcz2jF7Ys8cSLPCNTHgrk+VVjwNzQp6kdWjnXtwdOrCKAZD42tNMvYkdCcw4t8 6YPQ4qbXapHmRC5a5ZKBDOWJmAsqZhYkgUcmWkZV+y6tkhosmOBsVVlXbz3Zqx2j4qUe 4fbQ== 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:to:from:dkim-signature; bh=ztg2etMgHrv7wc3EoHYM+jEbe38uDdf07nWq6RUDW4Y=; b=yTfV5tn3C69DllJ4/6xGfmvwKLeDrDM2CZDw3sNmNs9IBlJn9snkPl0c1BigFcZPRj 40ANDy/rRQtyAQCMvceVHgD+2eZVVc1JwMDQQUHZzC+z98rG6yHUO8DjsN5CBa5/20RP w5tTtqEbohUwOYIqymuddhnB/0f8iFmYA7IinfxP8GdeKvNYLaOBmqm1SiFd9abDATvA /NOEkRoc/XTaB+af8GR3WlH1Yg1d1xqcRbahZIeElKkScWW371CTEdAxdWSWe7gDPaqx XzUqacJ4Q0NYt+yyM6qFiMrVjQEjkUoAHEjmGqhB6WTuoRkRsWKJAykJS9K9BWSiuh1p b0uw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@wesleyan.edu header.s=selector1 header.b=VxgS8hBv; spf=pass (google.com: domain of dlicata@wesleyan.edu designates 40.107.82.95 as permitted sender) smtp.mailfrom=dlicata@wesleyan.edu Received: from NAM01-SN1-obe.outbound.protection.outlook.com (mail-eopbgr820095.outbound.protection.outlook.com. [40.107.82.95]) by gmr-mx.google.com with ESMTPS id s3-v6si583840ljg.5.2019.02.17.06.14.52 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-SHA bits=128/128); Sun, 17 Feb 2019 06:14:52 -0800 (PST) Received-SPF: pass (google.com: domain of dlicata@wesleyan.edu designates 40.107.82.95 as permitted sender) client-ip=40.107.82.95; Received: from BN3PR04MB2195.namprd04.prod.outlook.com (10.167.4.13) by BN3PR04MB2308.namprd04.prod.outlook.com (10.166.73.147) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.1622.16; Sun, 17 Feb 2019 14:14:49 +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.018; Sun, 17 Feb 2019 14:14:48 +0000 From: "Licata, Dan" To: Homotopy Type Theory Subject: Re: [HoTT] A unifying cartesian cubical type theory Thread-Topic: [HoTT] A unifying cartesian cubical type theory Thread-Index: AQHUxqU9LYfzxGbfyEWWvjlH/ZJWw6XkCUWA Date: Sun, 17 Feb 2019 14:14:48 +0000 Message-ID: <96E42DDC-22B2-4B55-9A59-1A118D4C088F@wesleyan.edu> References: <6F861453-7F0E-4FD3-91B7-378B8ED25D7F@cmu.edu> <4d63c003926b2c19e530c107c5b141cd.squirrel@webmail.mathematik.tu-darmstadt.de> <20190216195136.GA11255@mathematik.tu-darmstadt.de> <20190217094330.GB3415@mathematik.tu-darmstadt.de> In-Reply-To: <20190217094330.GB3415@mathematik.tu-darmstadt.de> 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: 3e520a41-ee62-4981-43a9-08d694e246b7 x-microsoft-antispam: BCL:0;PCL:0;RULEID:(2390118)(7020095)(4652040)(8989299)(4534185)(4627221)(201703031133081)(201702281549075)(8990200)(5600110)(711020)(4605104)(2017052603328)(7153060)(7193020);SRVR:BN3PR04MB2308; x-ms-traffictypediagnostic: BN3PR04MB2308: x-microsoft-exchange-diagnostics: =?utf-8?B?MTtCTjNQUjA0TUIyMzA4OzIzOnY4U3pxcHBsUzdQbHJDRDRadlZIMGV3R3RQ?= =?utf-8?B?S0RlK0hOcHlZdDh5UzZBQ0FYM21MU0tseUY3VUpxQnJOR2NpcmNtS3JxUGdW?= =?utf-8?B?R0JjY3ZKdG5tK3NZRmZHRXRLVzVEbWdrUE0yMnhUaUVuOVpsMVVrbnFVZi91?= =?utf-8?B?UlRIeURJUm9RQkJTM1RFbmVLS1ExNWRaak1ZMDRua1NVaDArWHlsSWJFSkFv?= =?utf-8?B?VElKU01jSmpEdTM0M1draDJqZ2svUVl2aW90YkliZlVzRDlnQzhMbjV6aStY?= =?utf-8?B?MkNxSDB2K1BhRkpEcVM2V0hpR0R1anlUM1V0bVRjeTZqSi8zTlFTM0lQanh4?= =?utf-8?B?UzRyOWVONm5pQVlaS0hmODZRdEpydnBFT0trRUJrSURWNkJWNWRHSzNIajZn?= =?utf-8?B?NWxlN216TmxKMW9DYUsvS28xZWo5dFVyU1VOUitBeXRDcVoveXk0L3ZCTUc2?= =?utf-8?B?RE15bDRYWnRSbng3cmxoTW53d1QvZkg3VVI3SXMya285ZmVJWWVuUit1ZXRX?= =?utf-8?B?NDYwUDgyUTVOWUFwUnN3aHR4dnJSNWVoWC9LNFBSRzFxRzZySEJoV0xIQUpn?= =?utf-8?B?QjJ6cTNZbXRxUWRuSm0wYng4U21iVXpTWjg4bW0zc1g5ZUZjTlUzTmJYRmdZ?= =?utf-8?B?Vm9XTjRNbUZOWm9VaCsrR3plNkhuN3NZWGxvQ2wvRTFqWmZKTlVod21lSFhL?= =?utf-8?B?RlhyT3Yvdlh1cjNxWHl6T1loaXFjOFNuUlVSMWQ4b25pOVNRR3ZlQnBLZFBW?= =?utf-8?B?ZS84UTRHMnlOVnZ2ZE4xcHBHa3JxVHkwMlNlVlJnSEV0VWJsNVFxTlJPUC9J?= =?utf-8?B?S2xDQ3Fjd0hNVFJXandObDhxYTk3YUtlZW1lb2ZoejBEdjBBbXhSZVF5OURq?= =?utf-8?B?aS9WNmwyejBTZlhpMU4veHpuWTVJRnU5aTNkMHBIQ3Rjd1VVOVAwR0laTmw2?= =?utf-8?B?cEZCNUppTlpmbXZCOHk5OXpQSngwNmd6MlVLUTVYR1ZWanlOcGFsekFIWUJZ?= =?utf-8?B?YUpPbzBpK0VZQzh1TFNFZlh1dy9iOUpyNTFOSGNISnB2SU9jSDFKdkZ2cXdo?= =?utf-8?B?czBrVTNnUGVHT0Z0WUx2TUdxc3dnMmFRVjZzbGZCL1FIeUdsaTlwdnB1b2h3?= =?utf-8?B?WnR2SVNmNWxUdnIwam5zNHZkdlFNUXFvWDhpSTNEaTdHbFJ2aXFUTTNDM2w4?= =?utf-8?B?ZVYwdmVQY3ZaaUhneVhsclB3YW52dk0rVW16MS9qaFhQbkZsN0tGYVlOaVRC?= =?utf-8?B?Q011cnYyWGg1Z3o3RkE3S1BVdFl2NzFmaDl1bE13enIwN09zUStuenFUblBG?= =?utf-8?B?Mzh5bHNuVjlkTm13RnVjb0tRM2RPdkFtU3djcUx2YXFPajBCY053cVFqUnBZ?= =?utf-8?B?REI2YUt2ZFB0WVJzQUVISTNtU29jY0p2MENoM1Vlc2FPRzAwb3g3TGpYSjYw?= =?utf-8?B?OWpxSGJvdUZDSlZnSUlqTzEzWmh1VnovWmlST0dVMnFydGxHbkRRTUs2L2Z2?= =?utf-8?B?UkNQVnFGNUgxdHVRaFAydGxrYVBsTmVVNXNqTDFnNEIwbFBCUVlucnltZTFv?= =?utf-8?B?YTYyTU1tR1VXR3EvdHZCa2MvZmIrbVhPK1p5Q0ZrLythQjFBeTNBZnNicUFw?= =?utf-8?B?WG8yZFVHVXhyQ1FiK3p5MzRwRXVuQVhkdlF4Nk5VS3hLTitaM2tEdWovRThJ?= =?utf-8?Q?pDslEv0kB/fcGIOiBEPkTD9n2FAnkGSMMGa78ju?= x-microsoft-antispam-prvs: x-forefront-prvs: 0951AB0A30 x-forefront-antispam-report: SFV:NSPM;SFS:(10019020)(39850400004)(396003)(366004)(346002)(136003)(376002)(199004)(189003)(105586002)(478600001)(2906002)(33656002)(75432002)(6506007)(102836004)(36756003)(26005)(68736007)(82746002)(88552002)(316002)(256004)(786003)(186003)(97736004)(106356001)(8676002)(5660300002)(8936002)(81156014)(81166006)(14454004)(25786009)(93886005)(6246003)(53936002)(6436002)(6916009)(6486002)(3846002)(305945005)(7736002)(6512007)(6116002)(66066001)(229853002)(486006)(86362001)(76176011)(99286004)(11346002)(83716004)(71200400001)(71190400001)(476003)(2616005)(446003);DIR:OUT;SFP:1102;SCL:1;SRVR:BN3PR04MB2308;H:BN3PR04MB2195.namprd04.prod.outlook.com;FPR:;SPF:None;LANG:en;PTR:InfoNoRecords;A:1;MX: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: nkETJXZJ0Y95KOsImStTI6OBINGJ/s4QR5S4MD/m2+dKPwCT3JK7m+TiycIaAfJCrMYUsx1h6cjeEwUroPTSW2qKsC9K29GInag7+q71KV8iG7AjqaVTHjqSktHb5hRMWSg1RuniSxcmr4Xvark6Q9NEK6k4M0gQ7yrBfxizUmorNbg/nuYZDltBFh5K8JdOr0Eg+HasMvLxnrjEMu2pUNXAHz/ZKy/oX9X2MdA4Ojv34BsNgTPvMpfrtxmpKyapKdXqXj+MfMfkxmtHDZYrbNOOI97iE1MOA3W7gSFX8JgaypXfhqioUSfxmsMrUTzUMMFmEh+fqr+GgA/0IehqsK357EAHhb0yqcWmcx53Gv7g/WCUIDMeDDV5IQotk8DeiQ4vz47fVllrMmmdvKBcPgMxYdZkXxD3Q/BQelpSZHw= Content-Type: text/plain; charset="UTF-8" Content-ID: Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-OriginatorOrg: wesleyan.edu X-MS-Exchange-CrossTenant-Network-Message-Id: 3e520a41-ee62-4981-43a9-08d694e246b7 X-MS-Exchange-CrossTenant-originalarrivaltime: 17 Feb 2019 14:14:48.6977 (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: BN3PR04MB2308 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=VxgS8hBv; spf=pass (google.com: domain of dlicata@wesleyan.edu designates 40.107.82.95 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: , This is very cool! It's great to know that we can do without the diagonal cofibrations if we weaken the notion of fibration. Here's a reformulation of this Kan operation that I find intriguing:=20 in the internal language, I think Evan and Anders' definition is equivalent= to saying that A : I =E2=86=92 Set has Kan composition iff =CE=A0 r:I, the map (=CE=BB f =E2=86=92 f r) : (=CE=A0 (x : I) =E2=86= =92 A x) =E2=86=92 (A r) is an equivalence where equivalence is defined to be hfiber contractible, and contractible is defined to be "any partial element extends to a total one" (i.e. "trivial fibration") In contrast, the stricter notion, where com^r->r is strictly the identity i= s=20 A : I =E2=86=92 Set has Kan composition means=20 =CE=A0 r:I, b : A(r), the strict fiber (i.e. SFiber (f : A =E2=86=92 B) b =3D =CE=A3 a:A. f(a) =3Dstr= ictly b) of the map (=CE=BB f =E2=86=92 f r) : (=CE=A0 (x : I) =E2=86= =92 A x) =E2=86=92 (A r) is contractible Here's why: (1) The definition in Evan and Anders' note, in pseudo-internal-language notation (ignoring the boundary constraint proofs) is:=20 hasWCom : (I =E2=86=92 Set) =E2=86=92 Set=20 hasWCom A =3D (r r' : I) =E2=86=92=20 (=CE=B1 : Set) {{c=CE=B1 : Cofib =CE=B1}} (t : (x : I) =E2=86=92 =CE=B1 =E2=86=92 A x) (b : A r [ =CE=B1 =E2=86=A6 t r=CE=B1) ] ) =E2=86=92 A r' [ =CE=B1 =E2=86=A6 t r' ] hasWPath :(I =E2=86=92 Set) =E2=86=92 (wcomA : hasWCom A) =E2=86=92 Set hasWPath A wcomA =3D (r : I) =E2=86=92=20 (=CE=B1 : Set) {{c=CE=B1 : Cofib =CE=B1}} (t : (x : I) =E2=86=92 =CE=B1 =E2=86=92 A x) (b : A r [ =CE=B1 =E2=86=A6 t r) ] ) =E2=86=92 (Path (A r) (wcomA r r' =CE=B1 t b) (fst b)) [= =CE=B1 =E2=86=A6 \ _ =E2=86=92 t r' ] (i.e. the path is constantly t r' on =CE=B1) (2) If you move the r' binding inward and fuse the two functions into one, = you get=20 hasWCom : (I =E2=86=92 Set) =E2=86=92 Set=20 hasWCom A =3D (r : I) =E2=86=92=20 (=CE=B1 : Set) {{c=CE=B1 : Cofib =CE=B1}} (t : (x : I) =E2=86=92 =CE=B1 =E2=86=92 A x) (b : A r [ =CE=B1 =E2=86=A6 t r) ] ) =E2=86=92 (=CE=A3 f:((r' : I) =E2=86=92 A r'). Path (A r) (f = r) b) [ =CE=B1 =E2=86=A6 (\ r' =E2=86=92 t r' , \ _ =E2=86=92 t r= ) ] (i.e. on =CE=B1, f is t - , and the path is constant.) If we ignore the partial element stuff for a bit, that's hasWCom : (I =E2=86=92 Set) =E2=86=92 Set=20 hasWCom A =3D (r : I) =E2=86=92=20 (b : A r ) =E2=86=92 (=CE=A3 f : ((r' : I) =E2=86=92 A r'). Path (A r) (= f r) b) which is=20 apply : (r : I) =E2=86=92 ((x : I) =E2=86=92 A x) =E2=86=92 A r hasWCom : (I =E2=86=92 Set l) =E2=86=92 Set hasWCom A =3D (r : I) =E2=86=92=20 (b : A r ) =E2=86=92 HFiber (apply r) b (3) Restoring and rearranging the partial element constraint to t instead of b gives hasWCom : (I =E2=86=92 Set) =E2=86=92 Set hasWCom A =3D (r : I) =E2=86=92=20 (=CE=B1 : Set) {{c=CE=B1 : Cofib =CE=B1}} (b : A r ) (t : =CE=B1 =E2=86=92 (x : I) =E2=86=92 (A x [x =3D r =E2=86= =A6 b]) ) =E2=86=92 (HFiber (apply r) b) [ =CE=B1 =E2=86=A6 (\ r' =E2= =86=92 t r' p=CE=B1 , \ _ =E2=86=92 t r) ] which is, strangely enough, exactly the weird definition of equivalence that a group came up with at Dagstuhl while trying to optmize cubicaltt. =20 (4) Assuming using that weird definition of equivalence is not essential, we could rephrase using the hfiber-contractible definition, where contractible is defined to mean that any partial element extends to a total one:=20 -- trivial fibration: any partial element can be extended ContractibleFill : (A : Set) =E2=86=92 Set=20 ContractibleFill A =3D (=CE=B1 : Set) {{c=CE=B1 : Cofib =CE=B1}} =E2=86= =92 (t : =CE=B1 =E2=86=92 A) =E2=86=92 A [=CE=B1 =E2=86=A6 t ] isEquivFill : (A : Set) (B : Set) (f : A =E2=86=92 B) =E2=86=92 Set=20 isEquivFill A B f =3D (b : B) =E2=86=92 ContractibleFill (HFiber f b) isKan : (I =E2=86=92 Set) =E2=86=92 Set=20 isKan A =3D (r : I) =E2=86=92 isEquivFill ((x : I) =E2=86=92 A x) (A r)= (apply A r) This unwinds to almost the operation you have, except that this definition has a partial element of the whole HFiber (apply A r) b on =CE=B1, i.e. t r has a path to b, rather than being required to be strictly equal to it. =20 For the strict one, we have hasCom : (I =E2=86=92 Set l) =E2=86=92 Set=20 hasCom A =3D (r r' : I) (=CE=B1 : Set) {{_ : Cofib =CE=B1}}=20 =E2=86=92 (t : (z : I) =E2=86=92 =CE=B1 =E2=86=92 A z)=20 =E2=86=92 (b : A r [ =CE=B1 =E2=86=A6 t r ])=20 =E2=86=92 A r' [ =CE=B1 =E2=86=A6 t r' , (r =3D r') =E2=86=A6 = =E2=87=92 (fst b) ] i.e. (r : I) (=CE=B1 : Set) {{_ : Cofib =CE=B1}}=20 =E2=86=92 (t : (z : I) =E2=86=92 =CE=B1 =E2=86=92 A z)=20 =E2=86=92 (b : A r [ =CE=B1 =E2=86=A6 t r ])=20 =E2=86=92 =CE=A3 (f : (r' : I) =E2=86=92 A r')[=CE=B1 =E2=86=A6 = t]. f r =3D b)=20 i.e. (r : I) (b : A r) =E2=86=92 (=CE=B1 : Set) {{_ : Cofib =CE=B1}}=20 =E2=86=92 (t : =CE=B1 =E2=86=92 =CE=A3 f:((z : I) =E2=86=92 A z)= . f r =3D b)=20 =E2=86=92 =CE=A3 (f : (r' : I) =E2=86=92 A r')[=CE=B1 =E2=86=A6 = t]. f r =3D b i.e. (r : I) (b : A r) =E2=86=92 (=CE=B1 : Set) {{_ : Cofib =CE=B1}}=20 =E2=86=92 (t : =CE=B1 =E2=86=92 SFiber f b)=20 =E2=86=92 SFiber f b [ =CE=B1 =E2=86=A6 t ] (using uniqueness f= or =3D)=20 i.e. (r : I) (b : A r) =E2=86=92 Contractible(SFiber f b) --=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.