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=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, 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-pg1-x537.google.com (mail-pg1-x537.google.com [IPv6:2607:f8b0:4864:20::537]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 2515c92b for ; Sat, 10 Aug 2019 12:25:28 +0000 (UTC) Received: by mail-pg1-x537.google.com with SMTP id a9sf583698pga.16 for ; Sat, 10 Aug 2019 05:25:28 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1565439927; cv=pass; d=google.com; s=arc-20160816; b=fL0PQXEAa0y6uwHb6sDMBNET1Tb8TdHVB2YEz6FL6CcHnmR9qOCou9kyETdp64dCie 2SKmPMvP2DnrB8efUmGTQNHyrX4ognvNTN36LeHg6ZVBjjimxVd4XvnjClFmmdcTC8qy qSrUQTm1w8vrFfVMdxmNUyjjRk/dQN4uaw2s6zbq3/Ha5TEgpHMPKrA6Yi4yYDd4EGuJ KHXFJv/rhqh//1mtuWy/vdp/aJrGdor90WB7FnSQR21V8xOmsyt+sr+XN9/fhxzI3/rn 3/NgWhMOqOfChxER0Q/lV0WQSFKxWAImvBvCj9Q+B+0SXb6CeJUMY6AB30/TWMnTFItf q/rg== 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:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:sender:dkim-signature :dkim-signature; bh=k1C68esYdQHFPP7g5KpSeAb4mcKAG95MlULVphdkv1Y=; b=zA2YtTJNAfqnv/PHMdgLN7Q/eSxEPLnEY+WQ1bKxDj/AypHrDs4UqRHYUPY7NwHLqh 69caeNqpf1FPsNZJ0834z2XrLtOc0z6ouLMStkrHjF1Oaj7rqiuY+NI76VzSVSQwAg6B LnMlftkiHTcGtJ23YyBT9f/SmP+EIcH4m2o9+CK5YgLng5XN7BJiINS6rbDSEo/5YcbL /H2kQLKQVuC5XxcET5u0zV+CV68/AgtLgLfeBB5BB7H+kD14d0OluHp34ArQ0itUn52J qjGp85Q37H3gxclNm6VuE0HB1TjK9d9vpTftJzveBHacG8rr89LaL4Szrg+troZM2GMD GuSg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=mkuwSi1O; spf=pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4864:20::332 as permitted sender) smtp.mailfrom=valery.isaev@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com 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:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=k1C68esYdQHFPP7g5KpSeAb4mcKAG95MlULVphdkv1Y=; b=ohoJsUp5NLkaFFg2jbV+xyE/cvTZdmdSy2xl07zdnuCMC0HW7GwGkrWbC47axZy5S7 7AqRxqFiFV4OwvzS5m1lbL2a2fIbwz800cp1aozUfiw7o2+dCQogPJqyU2JgkT/gWny2 1UQyAlkt0CFV5mUPSttLtxDjXCvqFnsuwBzLJ1RnhpwifHWYVm9fgIPkyL/STL/2Smoy hbl8SWmSRwjPxGuDPvG+Q/E+gAE8+gj0NGRQtnagU2Adj/CJg4uWkKAB8zWOxqjAnzP8 BodT35zaGyhiZtgYt5Sp/drQuZCVLi98TINEebeewFcTHrgFjIpqqKN7q4K2bHJgV3pS TycQ== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc:x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=k1C68esYdQHFPP7g5KpSeAb4mcKAG95MlULVphdkv1Y=; b=PEa7lyvpOlNVltIUtQTR8eXTj71omwgNrIdcFpIeXjTqCHDIxrgmTb92VSTPZBkpb7 /iChmjHWxCFOeNsiKSnYDBj0pbyi8cH+ppz3eoECr5f00gaKklkCuOqdp80BPayYAUro IkxcVYTCBMml7bQntI5mN4RBaYImcJA1i2uP5E1DoyKo41r43cvV0LZgZVJ4VimU0veq pGJyCIh4nqVTNPIuAfniLpaA5R4bGfiiWnW9xv85uGs2EBEajBR7OdP2FJgY9TEvaYSn ITsJMIMgz7iMc0s/esl49w932Vx7QfjKfsAd7rBQhCZEd4Txugf7SEIWKGRHz2DJcEhP muKQ== 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: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=k1C68esYdQHFPP7g5KpSeAb4mcKAG95MlULVphdkv1Y=; b=kqEnKmasTmeLGb1DkI1ycINOzi2zrWAEsJFlrw4CGwpbkMNBTCCE4AftcxrnQ2OkWH J5+56wXVFUFhux1x7fWDoT/cwX3ebuyig+eCdWf1Yn79Qtzqb4uXx+S+qGgJI2Nfd+uI THIZhnwbTIrTPpX72fZlsxR2kDWPhGZ9d/hXU/ZhKBwayLSk37I+yGX9kOW6IsVoHQSn TFfWXXC7U1yLdGwo/kFarb6vwrZuWPyu2WNh3zURSbkA0TlM+Sa9vccHglLDri8lHXhW NqZg2LEMs2ATbJ4NzDhyFUAvAPqucMvsT+8kt37P+03T/EDKn38co2/8HMqyZFFB/olt qyQA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAV4gt386SSzufFxA4YcnI8FtYYLIyuY6t7/wkk/YxlF+MoHTbAE OoqhPMSsWsAFhV5egtLaRvc= X-Google-Smtp-Source: APXvYqwn1UFOQNx9f0w3xPTbio3/GXc0Gd/mshUVjcQuaT/P8tfbooPsvJ6zVgR7KuHxBJJPXXKgHw== X-Received: by 2002:a65:6104:: with SMTP id z4mr21321907pgu.27.1565439927433; Sat, 10 Aug 2019 05:25:27 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:902:7081:: with SMTP id z1ls552632plk.16.gmail; Sat, 10 Aug 2019 05:25:27 -0700 (PDT) X-Received: by 2002:a17:90a:2846:: with SMTP id p6mr3364261pjf.101.1565439927077; Sat, 10 Aug 2019 05:25:27 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1565439927; cv=none; d=google.com; s=arc-20160816; b=ybrfN3b1lWTdt28jCSkWBwJh/3lAe8lYnYFe3MFPFttQuWH9+7Geuyv93TfrUFDs4P yF73J6yowqL/UgS4Z3J6Hw2x/NeXc8c6MB7h03oKExOcCUJxr4HxMxzM3u4NefQ6+9cD 0uuX5zg+0I/D9itoyzBm4f6my0rc8Tjf4kvAYSW1hf8ILFMQrIHiNp5ithpI3N/XSnYZ zajrTbr2un0TPw6YYRLRSoCnwDYSBg0rQoiEpyVGkxU09FJBEmsWs16ZnsQNj/MO6oT2 cbIRr6Zp6Jc6obVQW7Egh/VkqRgPPwegNjCX9bvZxUCKwH4fhtagcVPJBOdoOnMu2nUW HW5g== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature; bh=gOyvbXW0gCLDKpxzGV+rPS8uWk1nErBOMFtACHPijNk=; b=LocxHJ4rroXYCSn+TCOQ5Kv/s0XknQnHI14kKEM1lOLMI1Hst4Fdm3lPR1cNRRm7yw IhOAI2s5CvVdJvtmb/aKGdfKxmJrMzd0OrqwCBCBuDypqqv1aNlFMAtlKxk6Yh0u8Cx6 Ws8SNq6IVhCIYVv06jYB8k/QE951exfzuQ+hcdwCrcDguNmjCnhnhH5TMGQASIcMhM8L hyOwhotvpW40I1As7kjqNCvB2162ZSf6ikVxBrHrP4Oj83s/oqd2MvjcOyfurwDxCo64 MoXvfPjx+r0vxnJClZ5aBokEwD+Eka8nAfQHVmnSc9Yb00M0XyJ1p2G9n9oKS1N5Z6v/ E7oQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=mkuwSi1O; spf=pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4864:20::332 as permitted sender) smtp.mailfrom=valery.isaev@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-ot1-x332.google.com (mail-ot1-x332.google.com. [2607:f8b0:4864:20::332]) by gmr-mx.google.com with ESMTPS id d9si94237plj.5.2019.08.10.05.25.27 for (version=TLS1_3 cipher=AEAD-AES128-GCM-SHA256 bits=128/128); Sat, 10 Aug 2019 05:25:27 -0700 (PDT) Received-SPF: pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4864:20::332 as permitted sender) client-ip=2607:f8b0:4864:20::332; Received: by mail-ot1-x332.google.com with SMTP id q20so142858863otl.0 for ; Sat, 10 Aug 2019 05:25:27 -0700 (PDT) X-Received: by 2002:a02:4005:: with SMTP id n5mr28723209jaa.73.1565439926602; Sat, 10 Aug 2019 05:25:26 -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: Valery Isaev Date: Sat, 10 Aug 2019 15:24:50 +0300 Message-ID: Subject: Re: [HoTT] New theorem prover Arend is released To: Michael Shulman Cc: Jon Sterling , "HomotopyTypeTheory@googlegroups.com" Content-Type: multipart/alternative; boundary="000000000000be1080058fc2622b" X-Original-Sender: valery.isaev@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=mkuwSi1O; spf=pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4864:20::332 as permitted sender) smtp.mailfrom=valery.isaev@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com 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: , --000000000000be1080058fc2622b Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable The document is slightly outdated. We do not have the rule iso A B (=CE=BBx= =E2=87=92 x) (=CE=BBx =E2=87=92 x) idp idp i =E2=87=92=CE=B2 A in the actual implementat= ion since univalence is true even without it. This rule has another problem. It seems that the theory as presented in the document introduces a *quasi*-equivalence between A =3D B and Equiv A B, which means that there are some true statements which are not provable in it. The theory without this rule should be completely equivalent to the ordinary HoTT, even though I cannot prove this yet. Regards, Valery Isaev =D1=81=D0=B1, 10 =D0=B0=D0=B2=D0=B3. 2019 =D0=B3. =D0=B2 12:42, Michael Shu= lman : > There is a bit more subtlety here than is evident from the brief > description, since everything has to happen in an arbitrary slice > category of the model category. But although the slices of a > cartesian model category are not in general again cartesian, they are > enriched model categories over the base, and so I think I agree that > this works since I lives in the base. > > However, section 2.2 of https://valis.github.io/doc.pdf also appears > to assert that an equivalence can be made into a line in the universe > for which coercing along the line is *definitionally* equal to the > action of the given equivalence, and such that the line associated to > the identity equivalence is definitionally constant. The latter seems > like it might be obtainable by a lifting property, but I don't > immediately see how to obtain the former in a model category? > --=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/CAA520ftTacC4iegu2UM887nbyJWQTByMKhrcsftKPXCadH06kQ%40ma= il.gmail.com. --000000000000be1080058fc2622b Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
The document is slightly outdated. We do not have the= rule=C2=A0iso A B (=CE=BBx =E2=87=92 x) (=CE=BBx =E2=87=92 x) idp idp i = =E2=87=92=CE=B2 A in the actual implementation since univalence is true eve= n without it. This rule has another problem. It seems that the theory as pr= esented in the document introduces a quasi-equivalence between A =3D= B and Equiv A B, which means that there are some true statements which are= not provable in it. The theory without this rule should be completely equi= valent to the ordinary HoTT, even though I cannot prove this yet.

Regards,
Valery Isaev


=D1=81=D0=B1, 10 =D0=B0=D0=B2=D0=B3. 2019 =D0=B3. =D0=B2= 12:42, Michael Shulman <shulman@sandiego.edu>:
There is a bit more subtlety here than is evident= from the brief
description, since everything has to happen in an arbitrary slice
category of the model category.=C2=A0 But although the slices of a
cartesian model category are not in general again cartesian, they are
enriched model categories over the base, and so I think I agree that
this works since I lives in the base.

However, section 2.2 of https://valis.github.io/doc.pdf also appe= ars
to assert that an equivalence can be made into a line in the universe
for which coercing along the line is *definitionally* equal to the
action of the given equivalence, and such that the line associated to
the identity equivalence is definitionally constant.=C2=A0 The latter seems=
like it might be obtainable by a lifting property, but I don't
immediately see how to obtain the former in a model category?

--
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://gro= ups.google.com/d/msgid/HomotopyTypeTheory/CAA520ftTacC4iegu2UM887nbyJWQTByM= KhrcsftKPXCadH06kQ%40mail.gmail.com.
--000000000000be1080058fc2622b--