Re: [HoTT] doing "all of pure mathematics" in type theory

[Bas Spitters <b.a.w.spitters@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 14134 bytes --]

There has been progress in making a cleaner interface with the standard Coq
tactics. (Some abstractions were broken at the ocaml level)
I'm hopeful that this can be lead to a clean connection between the HoTT
library and more of the Coq developments in the not too distant future.
As it exists in agda now.

IIUC, UniMath does not allow any of the standard library or it's tactics,
or even record types, since Vladimir wanted to have a very tight connection
between type theory and it's semantics in simplicial sets. So, I don't
expect them to connect to other developments, but I could be wrong.

About the bundled/unbundled issue, which also exists in Coq, there's some
recent progress "frame type theory" which should be applicable to both Coq
and lean:
 http://www.ii.uib.no/~bezem/abstracts/TYPES_2019_paper_51

Coming back to Kevin's question, yes, HoTT (plus classical logic for sets),
seems to be the most natural foundation for mathematics as is currently
published in the Annals.

On Sat, May 25, 2019 at 6:42 PM Noah Snyder <nsnyder@gmail.com> wrote:

> UniMath vs HoTT wasn’t exactly my point, UniMath = Book-HoTT is of a
> category from “Coq with the indices-matter option plus the HoTT library."
> “Coq with the indices-matter option plus the HoTT library" is of the same
> category as "Lean plus the math library" and then it makes sense to compare
> how practically useful they are for math.
>
> Here it's important to note that most advanced things that you can do in
> Coq are broken by using the "indices-matter" option and relatedly not using
> the built-in type Prop.  Quoting from https://arxiv.org/abs/1610.04591
> "This small change makes the whole standard library unusable, and many
> tactics stop working, too.  The solution was rather drastic: we ripped out
> the standard library and replaced it with a minimal core that is sufficient
> for the basic tactics to work."
>
> (In particular, I was in error in my previous email, *some* tactics are
> available in Coq+indices-matter+HoTT, but not many of the more advanced
> ones, and to my knowledge, not tactics needed for complicated homotopical
> calculations.)
>
> I should say I've never used Coq, just Agda.  (When I was using Agda the
> situation was even worse, things like pattern matching secretly assumed k
> even if you used the without-k option, and HITs were put in by a hack that
> wasn't totally clear if it worked, etc.)  So I'm likely wrong in some
> places above.
>
> So I think from a practical point of view, “Coq with the indices-matter
> option plus the HoTT library" is well behind ordinary Coq (and also Lean)
> for doing ordinary mathematics.  However, if and when it does catch up some
> of the pain points involving transporting from my previous email should go
> away automatically.  (Side comment: once you start talking about
> transporting stuff related to categories across equivalences of categories
> it's only going to get more painful in ordinary type theory, but will
> remain easy in HoTT approaches.)
>
> Best,
>
> Noah
>
> p.s. Installed Lean last week.  Looking forward to using it next year when
> Scott and I are both at MSRI.
>
> On Sat, May 25, 2019 at 11:36 AM Kevin Buzzard <kevin.m.buzzard@gmail.com>
> wrote:
>
>> Hi Noah. Thank you for pointing out the category error. It seems to me
>> that sometimes when I say "HoTT" I should be saying, for example, "UniMath".
>>
>> Tactics in Lean are absolutely crucial for library development. Coq has
>> some really powerful tactics, right? UniMath can use those tactics,
>> presumably?
>>
>> I understand that UniMath, as implemented in Coq, takes Coq and adds some
>> "rules" of the form "you can't use this functionality" and also adds at
>> least one new axiom (univalence).
>>
>> On Sat, 25 May 2019 at 15:50, Noah Snyder <nsnyder@gmail.com> wrote:
>>
>>> I’d also imagine that a “practical” implementation would likely have
>>> some kind of “two-level” type theory where you can use types that behave
>>> classically when that’s better and HoTT types when that’s better.
>>>
>>
>> But plain Coq has such types, right?
>>
>> OK so this has all been extremely informative. There are other provers
>> being developed which will implement some flavour of HoTT more
>> "faithfully", and it might be easier to develop maths libraries in such
>> provers.
>>
>> For example, if G and H are isomorphic groups and you want to translate a
>>> theorem or construction across the isomorphism.  In ordinary type theory
>>> this is going to involve annoying book-keeping which it seems like you’d
>>> have to do separately for each kind of mathematical object.
>>>
>>
>> Yes. This is a pain point in Lean. It's a particularly nasty one too, as
>> far as mathematicians are concerned, because when you tell a mathematician
>> "well this ring R is Cohen-Macauley, and here's a ring S which is
>> isomorphic to R, but we cannot immediately deduce in Lean that S is
>> Cohen-Macauley" then they begin to question what kind of crazy system you
>> are using which cannot deduce this immediately. As an interesting
>> experiment, find your favourite mathematician, preferably one who does not
>> know what a Cohen-Macauley ring is, and ask them whether they think it will
>> be true that if R and S are isomorphic rings and R is Cohen-Macauley then S
>> is too. They will be very confident that this is true, even if they do not
>> know the definition; standard mathematical definitions are
>> isomorphism-invariant. This is part of our code of conduct, in fact.
>>
>> However in Lean I believe that the current plan is to try and make a
>> tactic which will resolve this issue. This has not yet been done, and as
>> far as I can see this is a place where UniMath is a more natural fit for
>> "the way mathematicians think". However now I've looked over what has
>> currently been formalised in UniMath I am wondering whether there are pain
>> points for it, which Lean manages to get over more easily. That is somehow
>> where I'm coming from.
>>
>>
>>>  For example, say you have a theorem about bimodules over semisimple
>>> rings whose proof starts “wlog, by Artin-Wedderburn, we can assume both
>>> algebras are multimatrix algebras over division rings.”  Is that step
>>> something you’d be able to deal with easily in Lean?  If not, that’s
>>> somewhere that down the line HoTT might make things more practical.
>>>
>>
>> This is a great example! To be honest I am slightly confused about why we
>> are not running into this sort of thing already. As far as I can see this
>> would be a great test case for the (still very much under development)
>> transport tactic. Maybe we don't have enough classification theorems. I
>> think that our hope in general is that this sort of issue can be solved
>> with automation.
>>
>> Kevin
>>
>>
>>
>>> But mostly I just want to say you’re making a category error in your
>>> question.  HoTT is an abstract type theory, not a proof assistant.
>>>
>>> Best,
>>>
>>> Noah
>>>
>>> On Sat, May 25, 2019 at 9:34 AM Juan Ospina <jospina65@gmail.com> wrote:
>>>
>>>> On page 117 of https://arxiv.org/pdf/1808.10690.pdf appears the
>>>> "additivity axiom".  Please let me know if the following formulation of the
>>>> such axiom is correct:
>>>>
>>>> [image: additivity.jpg]
>>>>
>>>>
>>>>
>>>> On Saturday, May 25, 2019 at 5:22:41 AM UTC-5, awodey wrote:
>>>>>
>>>>> A useful example for you might be Floris van Doorn’s formalization of
>>>>> the Atiyah-Hirzebruch and Serre spectral sequences for cohomology
>>>>> in HoTT using Lean:
>>>>>
>>>>>  https://arxiv.org/abs/1808.10690
>>>>>
>>>>> Regards,
>>>>>
>>>>> Steve
>>>>>
>>>>> > On May 25, 2019, at 12:12 PM, Kevin Buzzard <kevin....@gmail.com>
>>>>> wrote:
>>>>> >
>>>>> > Hi from a Lean user.
>>>>> >
>>>>> > As many people here will know, Tom Hales' formal abstracts project
>>>>> https://formalabstracts.github.io/ wants to formalise many of the
>>>>> statements of modern pure mathematics in Lean. One could ask more generally
>>>>> about a project of formalising many of the statements of modern pure
>>>>> mathematics in an arbitrary system, such as HoTT. I know enough about the
>>>>> formalisation process to know that whatever system one chooses, there will
>>>>> be pain points, because some mathematical ideas fit more readily into some
>>>>> foundational systems than others.
>>>>> >
>>>>> > I have seen enough of Lean to become convinced that the pain points
>>>>> would be surmountable in Lean. I have seen enough of Isabelle/HOL to become
>>>>> skeptical about the idea that it would be suitable for all of modern pure
>>>>> mathematics, although it is clearly suitable for some of it; however it
>>>>> seems that simple type theory struggles to handle things like tensor
>>>>> products of sheaves of modules on a scheme, because sheaves are dependent
>>>>> types and it seems that one cannot use Isabelle's typeclass system to
>>>>> handle the rings showing up in a sheaf of rings.
>>>>> >
>>>>> > I have very little experience with HoTT. I have heard that the fact
>>>>> that "all constructions must be isomorphism-invariant" is both a blessing
>>>>> and a curse. However I would like to know more details. I am speaking at
>>>>> the Big Proof conference in Edinburgh this coming Wednesday on the pain
>>>>> points involved with formalising mathematical objects in dependent type
>>>>> theory and during the preparation of my talk I began to wonder what the
>>>>> analogous picture was with HoTT.
>>>>> >
>>>>> > Everyone will have a different interpretation of "modern pure
>>>>> mathematics" so to fix our ideas, let me say that for the purposes of this
>>>>> discussion, "modern pure mathematics" means the statements of the theorems
>>>>> publishsed by the Annals of Mathematics over the last few years, so for
>>>>> example I am talking about formalising statements of theorems involving
>>>>> L-functions of abelian varieties over number fields, Hodge theory,
>>>>> cohomology of algebraic varieties, Hecke algebras of symmetric groups,
>>>>> Ricci flow and the like; one can see titles and more at
>>>>> http://annals.math.princeton.edu/2019/189-3 . Classical logic and the
>>>>> axiom of choice are absolutely essential -- I am only interested in the
>>>>> hard-core "classical mathematician" stance of the way mathematics works,
>>>>> and what it is.
>>>>> >
>>>>> > If this is not the right forum for this question, I would be happily
>>>>> directed to somewhere more suitable. After spending 10 minutes failing to
>>>>> get onto ##hott on freenode ("you need to be identified with services") I
>>>>> decided it was easier just to ask here. If people want to chat directly I
>>>>> am usually around at https://leanprover.zulipchat.com/ (registration
>>>>> required, full names are usually used, I'll start a HoTT thread in
>>>>> #mathematics).
>>>>> >
>>>>> > Kevin Buzzard
>>>>> >
>>>>> > --
>>>>> > 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.
>>>>> > To view this discussion on the web visit
>>>>> https://groups.google.com/d/msgid/HomotopyTypeTheory/a57315f6-cbd6-41a5-a3b7-b585e33375d4%40googlegroups.com.
>>>>>
>>>>> > For more options, visit https://groups.google.com/d/optout.
>>>>>
>>>>> --
>>>> 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.
>>>> To view this discussion on the web visit
>>>> https://groups.google.com/d/msgid/HomotopyTypeTheory/18681ec4-dc8d-42eb-b42b-b9a9f639d89e%40googlegroups.com
>>>> <https://groups.google.com/d/msgid/HomotopyTypeTheory/18681ec4-dc8d-42eb-b42b-b9a9f639d89e%40googlegroups.com?utm_medium=email&utm_source=footer>
>>>> .
>>>> For more options, visit https://groups.google.com/d/optout.
>>>>
>>> --
>>> 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.
>>>
>> To view this discussion on the web visit
>>> https://groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg4dyjZHueTPQEYKQaojSw6SDKNUC8y49JHMoR9oTQOmMw%40mail.gmail.com
>>> <https://groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg4dyjZHueTPQEYKQaojSw6SDKNUC8y49JHMoR9oTQOmMw%40mail.gmail.com?utm_medium=email&utm_source=footer>
>>> .
>>
>>
>>> For more options, visit https://groups.google.com/d/optout.
>>>
>> --
> 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.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg7LAv8A%2BoXRLhsN3O7uXCh3D%2BSfBSsr-hmwRsr1iwztPg%40mail.gmail.com
> <https://groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg7LAv8A%2BoXRLhsN3O7uXCh3D%2BSfBSsr-hmwRsr1iwztPg%40mail.gmail.com?utm_medium=email&utm_source=footer>
> .
> For more options, visit https://groups.google.com/d/optout.
>

-- 
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.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOoPQuTNxVJ5%2B1Xotk3wzCgaW0C4wcxOdkpHANbOYdK5rCRkiA%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.

[-- Attachment #2: Type: text/html, Size: 18925 bytes --]