From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.129.32.70 with SMTP id g67mr7780319ywg.42.1513580697711; Sun, 17 Dec 2017 23:04:57 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.37.189.140 with SMTP id f12ls644123ybh.15.gmail; Sun, 17 Dec 2017 23:04:56 -0800 (PST) X-Received: by 10.129.107.214 with SMTP id g205mr8241171ywc.143.1513580696859; Sun, 17 Dec 2017 23:04:56 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1513580696; cv=none; d=google.com; s=arc-20160816; b=onYm5Fcc/G+MIdmWFx20ewzBmgV03pGoAZztq8E8cDWEHA0Hc2n+pCwkxZV3n3/eFR K9Cd8QJye1VR34mNXDJn9yYzozqGXRVO5rXHjnrpYFBr/Ok92u54WERou/olvm3qjKFM MFUtUw/9nLqqqyGZ22ngmpPjbx+PwaG/fin1R20bGM+mBrTW9rwp2FBcXR6m67wX3zbx 8kGfg0JceGAybx1yeYSW+LxQvjLvsUV7rR5Nzs2wVVJGQtuxWfNobVd1LzIi7SLQgPlD XhmwE0DEwjAkUJqM6VpJhXFvVrOhYSdIFqaOkGyLAomH7E25vXgFse9/KDkjWiqgYjjL DMPA== 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:references:in-reply-to :mime-version:dkim-signature:arc-authentication-results; bh=yn8427ioejAsRrQzapD25394BLLi3og9FyDXUHJuqEY=; b=IDg6oSzfDopRnlnxY8N1LDt5b5AAUj3Q74T3DYffJxdxtgJCzUjv+m30a+3UYCezr5 lTuDmvn5MsWEP47Rk4a8GRL2zRk+fPoRAz0HUgQcmSMWkrCRKrkBaVYtDIhAoQkwFvYH K8Jz783tG5WVxHzh2yNN+UcCZrZd7J4tM2bZ58RuPqmuD/JeRA4AINKhSUwm2042B+Nr rtY4ncU8H7LhlVTg0Gq/FSenjsKoCOaSWU/z8aaPhpXgfrFy8YWhvL2sQ8N+WfAeG7/0 AcVRCeCPgGocxvaejKQtpndc5ZpkJbuKPTXsIRlmCTYNGXwHrYrvQIjqvBq3w0LES3y4 ZyWA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=LSyrv2EN; spf=neutral (google.com: 2607:f8b0:4003:c06::22e is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-oi0-x22e.google.com (mail-oi0-x22e.google.com. [2607:f8b0:4003:c06::22e]) by gmr-mx.google.com with ESMTPS id a3si837374ybn.1.2017.12.17.23.04.56 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 17 Dec 2017 23:04:56 -0800 (PST) Received-SPF: neutral (google.com: 2607:f8b0:4003:c06::22e is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4003:c06::22e; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=LSyrv2EN; spf=neutral (google.com: 2607:f8b0:4003:c06::22e is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-oi0-x22e.google.com with SMTP id f69so9939117oig.10 for ; Sun, 17 Dec 2017 23:04:56 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=sandiego-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=yn8427ioejAsRrQzapD25394BLLi3og9FyDXUHJuqEY=; b=LSyrv2ENopx7CDnFPBC2NyJ0j4iW2U8NqJyQuTKAg7/Tkhj/5NB//uIEY1C5RCdmPO Pq3wg/qGb1Ws3otCTSfypQhN3aNoRzxXNBFE3DE2q6vwVGkxu6LSbRl7HdkdKneUxG61 KXW8lVphxyZbZlDVyYnGJYRhnUA7VvbWBHJCnEUQURcb3bUwbeIakg+w3t7+VUp3Ap77 waiP+OhVwA0cLTcQlcf33cN2qD+Iv8arjXB4LLUUzvcJVhtE3f4B7D7c7/4nBa8+lVV8 MHPVAh5ddE/kya2qF7S1yaKSXDJiUdwHfYKaLRPuyt4kFeTb5ovByulUKHaLxofzLYaU 9VRA== X-Gm-Message-State: AKGB3mJOsg1J1cdp0cTAg8GMpZagIHfW64hepKpwKlitFuMuOWnlpAy2 kJAfLJ8yLsl++muxJywM9ygCpsMoWxo= X-Received: by 10.202.75.69 with SMTP id y66mr12029848oia.242.1513580696122; Sun, 17 Dec 2017 23:04:56 -0800 (PST) Return-Path: Received: from mail-ot0-f175.google.com (mail-ot0-f175.google.com. [74.125.82.175]) by smtp.gmail.com with ESMTPSA id i128sm5505754oib.25.2017.12.17.23.04.55 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 17 Dec 2017 23:04:55 -0800 (PST) Received: by mail-ot0-f175.google.com with SMTP id n18so3253156otd.1 for ; Sun, 17 Dec 2017 23:04:55 -0800 (PST) X-Received: by 10.157.13.17 with SMTP id 17mr14869341oti.41.1513580695108; Sun, 17 Dec 2017 23:04:55 -0800 (PST) MIME-Version: 1.0 Received: by 10.157.89.169 with HTTP; Sun, 17 Dec 2017 23:04:34 -0800 (PST) In-Reply-To: References: From: Michael Shulman Date: Sun, 17 Dec 2017 23:04:34 -0800 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] HoTT in Lean 3 To: Floris van Doorn Cc: Homotopy Type Theory , Jeremy Avigad , Gabriel Ebner , Rob Lewis Content-Type: text/plain; charset="UTF-8" This is very cool! I look forward to hearing more about it. Some 5 years ago when were trying to be sure that Coq would be consistent with univalence, we also worried about singleton elimination, but in that case I think the problem was not definitional proof irrelevance (which Coq doesn't have) but the fact that Coq used to implicitly put some inductive definitions, including in particular the identity type, in Prop even when you didn't tell it to. I don't remember that we actually derived a contradiction from this, but the idea of all identity types of all types (in all universes) living in the bottom universe certainly seemed unlikely to be consistent. We fixed that with the --indices-matter flag which told Coq to put all inductive definitions in the correct universe. It sounds like Lean probably doesn't have this problem, i.e. if you define an inductive *type* then it is always a type and never turns out to be a proposition? On Sun, Dec 17, 2017 at 3:13 PM, Floris van Doorn wrote: > A followup to my previous email in another discussion (copied below). > > I said in that email that the kernel of Lean 3 is inconsistent with > univalence. While this is true, we are currently developing a HoTT library > for Lean 3 here: > https://github.com/gebner/hott3 > The logic in this library is consistent in the following sense described > below. > > In Lean you can define inductive types and inductive propositions. Most > inductive propositions can only eliminate to Prop (having them eliminate to > Type would be inconsistent with proof irrelevance). There is a rule called > singleton elimination, which allows certain propositions which are > "subsingletons" to eliminate to all types (I believe that an inductive type > is a subsingleton if it has at most one constructor, and all arguments of > that constructor are Prop-valued, but don't quote me on that). > > In the Lean 3 HoTT library Gabriel Ebner has written a program that checks > whenever you proof a theorem/definition in the HoTT library that singleton > elimination is not used. If it is used, then it raises an error (even though > the Lean kernel did accept the proof). > > We're quite certain that removing singleton elimination makes the kernel > consistent with univalence. In fact, I believe that even when assuming > `false` (which is the empty type living in Prop) we cannot construct any > data in a type from it. This allows us to write metaprograms, like tactics > and automation in Lean using Prop, while not using Prop in the HoTT-library. > > I think Lean 3 is an interesting proof assistant to work on HoTT-specific > automation, since Lean has a very strong metaprogramming language to write > tactics in the Lean language itself. It is probably not the long-term "best" > proof assistant, since its underlying type theory is not cubical (its > underlying type theory is basically the type theory of the HoTT book). Work > is in progress to port the formalizations from Lean 2 to Lean 3. > > For more information see the readme of the linked Github repository. Any > comments are welcome. > > Best, > Floris > > > > On 17 December 2017 at 23:43, Floris van Doorn wrote: >> >> Just to clear some things up in this conversation: >> >> - The Lean kernel is consistent with any form of propositional >> extensionality, as far as I know. >> - The kernel for the current version of Lean, Lean 3, is not designed for >> HoTT and inconsistent with univalence. However, it does *not* ignore any >> transport of an equality. The bottom universe in Lean is the universe of >> propositions, Prop (not to be confused with hProp). What does hold is that >> there is definitional proof irrelevance for proofs of a proposition, i.e. if >> P : Prop and p, q : P then p is definitionally equal to q. This means that >> if we have a proof p : A = A for some type A, then transporting along p is >> the identity function (because p = refl, definitionally). However, if p : A >> = B, then transporting along p is not the identity function (which would be >> type incorrect to state). >> - Lean has an evaluator in a virtual machine, which is used to evaluate >> programs and tactics efficiently outside the kernel. This evaluator is not >> trusted, and cannot be used when writing any proof in Lean. This evaluator >> removes all type information and propositions for efficiency, and can >> evaluate expressions to the wrong answer when axioms are added to the type >> theory (even if the axioms are consistent). For example, if we add the >> following lines to Ben's example >> ``` >> constant H : HProp_ext >> #eval Sig.fst (x H) >> ``` >> we see that the evaluator incorrectly evaluates this expression to tt >> (true). Needless to say, the evaluator was not designed for this, but >> instead to evaluate tactics like the following quickly. >> ``` >> if n < 1000000 then apply tactic1 else apply tactic2 >> ``` >> >> I hope this clears up any confusion. >> >> Best, >> Floris >> > -- > 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 HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout.