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, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-pl1-x63a.google.com (mail-pl1-x63a.google.com [IPv6:2607:f8b0:4864:20::63a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 96357513 for ; Sun, 11 Aug 2019 12:40:03 +0000 (UTC) Received: by mail-pl1-x63a.google.com with SMTP id t2sf59847786plo.10 for ; Sun, 11 Aug 2019 05:40:03 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1565527202; cv=pass; d=google.com; s=arc-20160816; b=VuahBPpKLwO7T36UDak+a3/rl6GrGzjj4NjRhOi8IA5+lnnd1wiMaBEAz01HpFOeno ZdoBehBHEtPCgxIASy9pQZKPZwM5r4lRgo2OkWhQmSQ7CSnj848QvPGGpxSUdLaaAoxP d6vqJSCvEDqmpGnZCpwuyf/XNrMSDHaNp90xK0uBjsJ896Oj5uR7OtikybGIZc7uI6iP /r8gSzpUm9436LHlvs00ZSCo5f5GyKKZHXHx5JThRPk8mKxSh188oEAo829KYInwGFk1 BoefpQHM/ruaDAkppKYiYhAvykx71T2Gj8ycQucOllMB3OCIrQB0mdvzWcGu2Nk+v8PD DKhA== 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:cc:to:subject :message-id:date:from:in-reply-to:references:mime-version:sender :dkim-signature; bh=6LjXhE8HzYFU6mn+jFn1QICDO8LGQq0Q+SZRBx52HoE=; b=CinjFJOJ2jLf+ehCC/thUgGMcGB2qMD/Ewl/L9CiX3bnHoxtxlPr0nbFmvjUiSAU7q 1OxXmsCkvct/CuYydUZ715MJFRtEXA2ItM5jD5sU+ZwJBq4fG6CzzrTITR7VpMm0f2U4 KiAJ2OEIgmwtmh8iN/aZ7hS4V5VdywkouUzBjHONsYoHgg9VcS5sM2VjPDDwfydOhV/S 8XbhqHSa5gZlA+egFt61ZHvThXCY5Qa4CsG0mAKA7pIT0XSvHJgo/t0CsbrHnOhlct3J vKNiZeOkv0/5PkjSDxa/oX8OSzWUtFcUS4lOHSEM7vG8djAwsEqqyB0x53yUKPkbtDRq vV5Q== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=ggtGDe6o; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b32 as permitted sender) smtp.mailfrom=shulman@sandiego.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:references:in-reply-to:from:date:message-id :subject:to:cc:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=6LjXhE8HzYFU6mn+jFn1QICDO8LGQq0Q+SZRBx52HoE=; b=RayOKlxpcYChIDzOAnzElCa0XLxRCtnvhMdJzssDg28SGYsD7xeQX5cks1S0s7jPit gHFGSVp3v7uKpfLpFAf+jVg/BCI70mOFMDC4PR7t6HlBHH9haILh7c3k2RViMgZ6AGQW bKAVv3Irduh3oEQY7nSTLWz0ViYw4+YszlucQ+jPwNfYl1KGs3Jt1mjRL81DCka2EuZs DbRDhg4yHnEmI50J18Ya56FsdaJfn39aDwVLnvZglcmYMcTwSK3lhfA4O6BMWPJl9q9Q N22BJ57L30p5jkcng0Ty3TxG+tKMAMFinuQQ2swBDp5u+mEnGFFC7obuFWijehSLlwzy AT8w== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:references:in-reply-to:from :date:message-id:subject:to:cc: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=6LjXhE8HzYFU6mn+jFn1QICDO8LGQq0Q+SZRBx52HoE=; b=Lu3JZjPHR1azNqLdT3M3Z7GH3larOZOK0th/xGcvlkly3SMdr4Qh4b79H1yCl/n4XW 0Jl7Ay/SLiC836Z0MsZE3gnpsio+S99fLqIEQ2OvzLcQIE2cWrcl48kS92v89y7PxQNC A9ebWwBZYPO8xrz5C3zM1Hj7dJXmtUrkezje/UKGQB0TDCTn+PcF4heTxYFqQpMdcMtt tTR/XKOCOAU3985oKJx9LK/fZRsQVM8JHp9Nzj1wCtxc6QR+GpsltqCTaG+pqU7jqEvy mWtSOyHytC3dLKyH3ydRszo0X7ESSdHCNa+2q70r5+/6yUE5HSJh+LNgfep2z9ph2nQJ uB2A== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAVPmnPkJul7UbLOH1Exb+YOGV0k5ex3AZ05w/61yGoXCMDv2c+2 1hKgZ4WVfixBlYBV53cZNpM= X-Google-Smtp-Source: APXvYqwfOMgybqqeUFPtPabozNG/pFg1aUsNplvwqJtoqzwzp5kY1jKFAtw+j6P1mVeHae0JBZFWdw== X-Received: by 2002:a62:144b:: with SMTP id 72mr2917001pfu.42.1565527202326; Sun, 11 Aug 2019 05:40:02 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a65:6203:: with SMTP id d3ls10999234pgv.16.gmail; Sun, 11 Aug 2019 05:40:02 -0700 (PDT) X-Received: by 2002:aa7:9e9a:: with SMTP id p26mr31777468pfq.25.1565527201986; Sun, 11 Aug 2019 05:40:01 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1565527201; cv=none; d=google.com; s=arc-20160816; b=zCrYxOUXeuUJpovCDvymw055S303l/oep8W/LNdFwwNhClwNCygcpwR7UlTkt/G0ap Qxsao4z3/KvA33eHCxP6fXcmrXyDucK47DaqROLhTHJw2JIWZ93N17dQGqn4KyUjgbkf O/9fWV3a2gTf/exrK/UcjYz5jwFhln+4oBG6Nuv23wMPdvL3GgVfYirblzDxXRsGY5UX PKmpwixpJ+dH3re7dMBA5hBxf84zzLFarq+gfS74F94qfR09bo9m33Its55x848pmRrt pxh7zfSorGTtusVHV64Sp2AFsVqH4uKUfnLE6A9nckIddGb6VLly3J1zY7EfP3AsqGbk OnaQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:dkim-signature; bh=FHw3nFjYpV19frGPuPAqu1B7iaUEN1DcBHYolMQXpL8=; b=H8KD/zTpBOE6edg1cpECUFQ9FJl5PJfwwFlFdehI3XSYZUJkwWiYpPHGkyLE0B1hfc ZW/nQ+OXq7EecXMKYs80uOg4FjbnJqF3n4Qkeblzj25TSUkHvTKPt7+DZrdqdKoAZGSS vAvi2mQc8lq7oXolH3EyD5LH/nL297zOeHf578HXm8JpS3A5A8uy5ETJ9gsL6NkzlJnx OB3vhUCHVKEpf6UGLs7nTBlx3zWw+ocAVP+Ez3c86S+ULYp1dlGpPB+gQPJLlb/+XBYN 4J7Y3RnRZ3qKMsgxyFs6cHXIiIj+tSt681Qe6pt3AfHhP3eNIJSGc+8/8FGm5I7C0m9Z 17mA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=ggtGDe6o; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b32 as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yb1-xb32.google.com (mail-yb1-xb32.google.com. [2607:f8b0:4864:20::b32]) by gmr-mx.google.com with ESMTPS id b24si327383pjq.1.2019.08.11.05.40.01 for (version=TLS1_3 cipher=AEAD-AES128-GCM-SHA256 bits=128/128); Sun, 11 Aug 2019 05:40:01 -0700 (PDT) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b32 as permitted sender) client-ip=2607:f8b0:4864:20::b32; Received: by mail-yb1-xb32.google.com with SMTP id s142so7970371ybc.6 for ; Sun, 11 Aug 2019 05:40:01 -0700 (PDT) X-Received: by 2002:a25:830b:: with SMTP id s11mr19546804ybk.208.1565527201035; Sun, 11 Aug 2019 05:40:01 -0700 (PDT) Received: from mail-yb1-f180.google.com (mail-yb1-f180.google.com. [209.85.219.180]) by smtp.gmail.com with ESMTPSA id t128sm20438562ywf.32.2019.08.11.05.39.58 for (version=TLS1_3 cipher=AEAD-AES128-GCM-SHA256 bits=128/128); Sun, 11 Aug 2019 05:39:59 -0700 (PDT) Received: by mail-yb1-f180.google.com with SMTP id s142so7970332ybc.6 for ; Sun, 11 Aug 2019 05:39:58 -0700 (PDT) X-Received: by 2002:a25:4542:: with SMTP id s63mr19491031yba.395.1565527198493; Sun, 11 Aug 2019 05:39:58 -0700 (PDT) MIME-Version: 1.0 References: <9d23061c-4b7a-4d69-9c22-f28261ad3b33@googlegroups.com> <06e24c98-7409-4e75-88ee-a6e1bb891e1e@www.fastmail.com> In-Reply-To: From: Michael Shulman Date: Sun, 11 Aug 2019 08:39:46 -0400 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] New theorem prover Arend is released To: Valery Isaev Cc: Jon Sterling , "HomotopyTypeTheory@googlegroups.com" Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: shulman@sandiego.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=ggtGDe6o; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b32 as permitted sender) smtp.mailfrom=shulman@sandiego.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: , On Sun, Aug 11, 2019 at 6:47 AM Valery Isaev wrote= : > I don't remember well, but I think the idea is that you need to prove tha= t there is a trivial cofibration Eq(A,B) -> F(U^I,A,B), where the first obj= ect is the object of equivalences between A and B and the second object is = the fiber of U^I over A and B. The fact that this map is a weak equivalence= is just the univalence axiom. The problem is to show that it is a cofibrat= ion and whether this is true or not depends on the definition of Eq(A,B). I= don't actually remember whether I finished this proof. Yes, in a straightforward approach that's what you would need to prove, or more precisely that the map Eq -> U^I is a trivial cofibration in the slice over UxU (since the lifting has to be done in the universal case rather than just over each global element). Possibly you could get away with less, since you're only asking to recover the action of the given equivalence as a function (rather than the entire equivalence data). Perhaps a clever choice of fibration structure in the equivalence extension property would suffice. > Since F(A,p) is the usual (inductive) data type, you can do everything yo= u can do with other data types. In particular, since it has only one constr= uctor with one parameter A, it is easy to proof that it is equivalent to A. Okay, it sounds like you're saying that the datatype defined with \use\level is F(A,p) and the analogous one defined without \use\level is A, while both have their usual rules but are not identical. In this case you have somewhat *more* than an equivalence between F(A,p) and A, at least if all datatypes have their usual definitional computation rules, since an arbitrary type "F(A,p)" that is only *equivalent* to a datatype will only inherit a typal computation rule. It seems plausible though that one could construct universes of n-types that are strictly closed under a given datatype construction that preserves n-types (at least, assuming one can do the same for arbitrary universes). However, the documentation also suggests that \use\level can be applied to plain definitions (\func). How is F(A,p) distinguished from A in this case? --=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/CAOvivQxMwmkA0o2XBecGQaiaVFO0rjwKvZfbMqS%2Be363GJwRbA%40= mail.gmail.com.