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

[Noah Snyder <nsnyder@gmail.com>]

[-- Attachment #1.1: Type: text/plain, Size: 7350 bytes --]

HoTT is NOT a specific proof assistant the way that Lean is.  Instead it’s
a different flavor of type theory which is well attuned to things that have
a homotopical flavor.  It can be implemented in various proof assistants
(Coq, Agda, Lean 2) but none of them are really fully designed for HoTT.
But the kind of practical question you’re asking depends on the
implementation.  I don’t think any of the implementations are practical in
the way that you want.  For example, I’m not aware of any kind of “tactics”
for HoTT.  The bookkeeping involved in saying that the two proofs of
Eckman-Hilton for 3-loops agree (which I could explain in one hand gesture
in person and where I understand all the relevant issues in HoTT) is very
very intimidating practically.  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.

HoTT is mostly better for math that’s explicitly homotopical.  But there
are situations in more ordinary math where you can see why it would be
useful.  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.  In
HoTT that happens automatically.  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.

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.
For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1.2: Type: text/html, Size: 9395 bytes --]

[-- Attachment #2: additivity.jpg --]
[-- Type: image/jpeg, Size: 18737 bytes --]