Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
From: Nicolas Alexander Schmidt <zero@fromzerotoinfinity.xyz>
To: Kevin Buzzard <kevin.m.buzzard@gmail.com>
Cc: Homotopy Type Theory <HomotopyTypeTheory@googlegroups.com>
Subject: Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'?
Date: Wed, 27 Nov 2019 21:21:53 +0100	[thread overview]
Message-ID: <c25dfb49-6b6e-d926-f8c3-4c590ca6f507@fromzerotoinfinity.xyz> (raw)
In-Reply-To: <CAH52Xb2AoMWBeCCJ5B8=Dfa8UgmO1vbWf7a=dvfRqTFTdu61qA@mail.gmail.com>

Thank you Kevin, for taking the time to write this very detailed response.

After taking a look at your original approach and the improved one of
your student, I am under the impression that the difficulties you
encountered actually had little to do with the proof assistant you were
working in. Perhaps this impression is just uninformed, and e.g. in a
system based on cubical type theory these problems would disappear. Of
course, the only way to tell is to go ahead and formalize this result in
such a system.

But to me it seems that the "commutative diagram hell" you faced really
stems from an issue that already exists within mathematics, namely the
two conflicting viewpoints on localization: viewing it as a property
(the honest viewpoint) or viewing it as an operation (the convenient
illusion). As far as I understood, in your original approach you proved
the "standard affine covering lemma"
(https://stacks.math.columbia.edu/tag/00EJ) under the operational
viewpoint, making it nontrivial to apply this lemma to "nonstandard"
localizations, whereas your student proved the lemma under the property
viewpoint, i.e. for "all" localizations at the same time.

To a "proper" mathematician this distinction must seem silly, and if he
doesn't outright dismiss it as fruitless philosophical nonsense, he will
most likely claim that one can safely pretend it doesn't exist due to
"existence of canonical isomorphisms yada yada yada".

And yet, even the (presumably "proper") author(s) of
https://stacks.math.columbia.edu/tag/01HR somehow felt the need to
justify the application of lemma 10.23.1 with a sentence like

    "[...] and hence we can rewrite this sequence as the sequence [...]",

which seems to admit the issue. Thus instead of pathologies, one may
view the difficulties arising in formalization as merely pointing out
existing gaps in the proper mathematician's operational theory, that he
can in principle fill out all the details in his proofs to arbitrary
precision.


This problem and its solution remind me of something I encountered a few
years ago, when I tried to convince myself of the well-known fact that
the abstract braid group

    B(W) := < T_w for w \in W  |  \ell(w) + \ell(w') = \ell(ww') 
\Rightarrow T_w T_{w'} = T_{ww'} >

attached to a finite reflection group W can be viewed as the fundamental
group of its complexified hyperplane complement X. My ambition was only
to explicitly construct the map

\rho: B(W) --> \pi_1(X,x_0),

but even that turned out to be more difficult than expected.

The first naive attempt---of writing down explicit representative paths
in the classes \rho(T_w) and proving that these satisfy the "braid
relations" up to homotopy---was completely impractical. In fact, even
writing down representative paths seemed not merely difficult but
hopeless. Eventually I realized that the solution is to attach to a
generator T_w not a representative (operational viewpoint) but a
canonical subspace of the path-space (property viewpoint), showing that
the latter is contractible and that the collection of these subspaces
satisfy the braid relations (in the obvious sense). After that
realization, everything was completely straightforward.


--

Nicolas


Am 24.11.19 um 19:11 schrieb Kevin Buzzard:
>
>     Kevin, I would like to second Michael's interest in seeing these 20
>     commutative diagrams. Moreover, I'd also be very interested in seeing
>     your "spaghetti code" (quote from the slides of your Big Proof
>     talk): it
>     seems it should be informative to see where your initial approach went
>     wrong, and how much these problems and their solution had anything
>     to do
>     at all with the formal system you were working in. Are your original
>     files perhaps available somewhere?
>
>
> Sorry for the delay.
>
> My original repo with a "bad" theorem is here:
>
> https://github.com/kbuzzard/lean-stacks-project
>
> The bad theorem is this:
>
> https://stacks.math.columbia.edu/tag/00EJ
>
> The problem is that the rings denoted R_{f_i} (localisations of rings)
> are typically defined to mathematicians as "this explicit construction
> here" as opposed to "the unique up to unique isomorphism ring having
> some explicit property" and, as a mathematician, I formalised (or more
> precisely got Imperial College maths undergraduates Chris Hughes and
> Kenny Lau to formalise) the explicit construction of the localisation
> and then the explicit theorem as stated in the stacks project, not
> understanding at the time that this would lead to trouble. When I came
> to apply it, I ran into the issue that on this page
>
> https://stacks.math.columbia.edu/tag/01HR
>
> we have the quote: "If f, g in R are such that D(f)=D(g), then by
> Lemma 26.5.1 there are canonical maps M_f->M_g and M_g->M_f which are
> mutually inverse. Hence [we can regard M_f and M_g as equal]".
>
> This is a typical mathematician's usage of the word "canonical" -- it
> means "I give you my mathematician's guarantee that I will never do
> anything to M_f which won't work in exactly the same way as M_g so you
> can replace one by the other and I won't mind".
>
> As I explained earlier, by the time I noticed this subtlety it was too
> late, and this led to this horrorshow:
>
> https://github.com/kbuzzard/lean-stacks-project/blob/7c2438e441547da6a5786a9a427fd78cbc407fa9/src/canonical_isomorphism_nonsense.lean#L268
>
> plus the lines following, all of which is applied here
>
> https://github.com/kbuzzard/lean-stacks-project/blob/595aa1d6c5ce5a6fa0259c5a0a2226a91b07d96e/src/tag01HR.lean#L208
>
> . That last link is justifying a whole bunch of rewrites along
> canonical isomorphisms. These were the general lemmas I needed to
> prove that if A -> B was a map, and if A was canonically isomorphic to
> A' and if B was canonically isomorphic to B' and A' -> B' was the
> corresponding map, then the image of A was canonically isomorphic to
> the image of A' etc, all in some very specific situation where
> "canonically isomorphic" was typically replaced by "unique isomorphism
> satisfying this list of properties". Note that this is crappy old code
> written by me when I had no idea what I was doing. One very
> interesting twist was this: the universal property of localisation for
> the localised ring R_f is a statement which says that under certain
> circumstances there is a unique ring homomorphism from R_f; however in
> https://stacks.math.columbia.edu/tag/00EJ the map beta in the
> statement of the lemma is *not* a ring homomorphism and so a naive
> application the universal property was actually *not enough*! One has
> to reformulate the lemma in terms of equalisers of ring homomorphisms
> and remove mention of beta. None of this is mentioned in the stacks
> project website because we are covered by the fact that everything is
> "canonical" so it's all bound to work -- and actually this is *true*
> -- we are very good at using this black magic word.
>
> All of this is fixed in Ramon Mir's MSc project
>
> https://github.com/ramonfmir/lean-scheme
>
> and the explanations of how it was fixed are in his write-up here
>
> https://www.imperial.ac.uk/media/imperial-college/faculty-of-engineering/computing/public/1819-ug-projects/Fernandez-I-MirR-Schemes-in-Lean.pdf
>
> Briefly, one crucial input was that the localisation map R -> R_f
> could be characterised up to unique isomorphism in the category of
> R-algebras by something far more concrete than the universal property,
> and Ramon used this instead.
>
> In HoTT one might naively say that these problems would not arise
> because isomorphic things are equal. However my *current* opinion is
> that it is not as easy as this, because I believe that the correct
> "axiom" is that "canonically" isomorphic objects are equal and that
> the HoTT axiom is too strong. I developed some rather primitive tools
> to rewrite certain statements along certain kinds of isomorphisms with
> some naturality properties, and mathematicians would be happy with
> these ideas. I can quite believe that if you stick to homotopy types
> with the model in your mind as being topological spaces up to homotopy
> then the HoTT axiom is perfect. However there are things other than
> topological spaces in mathematics, for example commutative rings, and
> in my mind the HoTT axiom just looks weird and wrong in ring theory,
> and I expect it to backfire when HoTT people start doing some serious
> ring theory. I might be wrong. Part of me hopes I'm wrong, in fact.
> But this will remain my opinion until someone comes along and
> formalises the definition of a scheme in one of the HoTT theories and
> proves the "theorem" that an affine scheme is a scheme (I write
> "theorem" in quotes because it is a construction, not a theorem). I
> had the pleasure of meeting Thorsten Altenkirch earlier this week and
> I asked him why this had not been done yet, and he told me that they
> were just waiting for the right person to come along and do it. A year
> or so ago I was of the opinion that more mathematicians should be
> using Lean but now I have come to the conclusion that actually more
> mathematicians should be engaging with *all* of the theorem provers,
> so we can find out which provers are the most appropriate for which
> areas. By "mathematicians" here I really mean my ugly phrase "proper
> mathematicians", i.e. people doing algebra/number
> theory/geometry/topology etc, people who have absolutely no idea what
> a type is and would even struggle to list the axioms of set theory.
> These people with their "canonical" constructions (a phrase which has
> no meaning) are the problem, and they're very hard to reach because
> currently these systems offer them nothing they need. I wrote a silly game
>
> http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/
>
> to help my 1st years revise for my exam (and the game takes things
> much further than the contents of the course), and I'm writing a real
> number game too, to help my 1st years revise analysis for their
> January exam. It would not be hard to write analogous such games in
> one of the HoTT theories, I would imagine.
>
> From what I have seen, it seems to me that Isabelle is a fabulous tool
> for classical analysis, Coq is great for finite group theory, the
> Kepler conjecture is proved in other HOL systems, and the HoTT systems
> are great for the theory of topological spaces up to homotopy. But
> number theory has been around for millennia and unfortunately uses
> analysis, group theory and topological spaces, and I want one system
> which can do all of them. I think that we can only find out the
> limitations of these systems by doing a whole bunch of "proper
> mathematics" in all of them. I think it's appalling that none of them
> can even *state* the Hodge conjecture, for example. For me, that is a
> very simple reason for a "proper mathematician" to immediately reject
> all of them in 2019. But I digress.
>
> Kevin
>
>
>
>     --
>
>     Nicolas
>
>
>
>
>     -- 
>     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
>     <mailto:HomotopyTypeTheory%2Bunsubscribe@googlegroups.com>.
>     To view this discussion on the web visit
>     https://groups.google.com/d/msgid/HomotopyTypeTheory/bc1a186e-4d33-0296-4b1b-b09ee8188037%40fromzerotoinfinity.xyz.
>

-- 
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/c25dfb49-6b6e-d926-f8c3-4c590ca6f507%40fromzerotoinfinity.xyz.

  parent reply	other threads:[~2019-11-27 20:22 UTC|newest]

Thread overview: 32+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2019-10-27 14:41 Nicolas Alexander Schmidt
2019-10-27 17:22 ` Bas Spitters
2019-11-03 11:38   ` Bas Spitters
2019-11-03 11:52     ` David Roberts
2019-11-03 19:13       ` Michael Shulman
2019-11-03 19:45         ` Valery Isaev
2019-11-03 22:23           ` Martín Hötzel Escardó
2019-11-04 23:20             ` Nicolas Alexander Schmidt
2019-11-24 18:11               ` Kevin Buzzard
2019-11-26  0:25                 ` Michael Shulman
2019-11-26  8:08                   ` Ulrik Buchholtz
2019-11-26 19:14                   ` Martín Hötzel Escardó
2019-11-26 19:53                     ` Kevin Buzzard
2019-11-26 20:40                       ` Martín Hötzel Escardó
2019-11-26 22:18                       ` Michael Shulman
2019-11-27  0:16                         ` Joyal, André
2019-11-27  2:28                           ` Stefan Monnier
2019-11-27  1:41                         ` Daniel R. Grayson
2019-11-27  8:22                         ` N. Raghavendra
2019-11-27 10:12                     ` Thorsten Altenkirch
2019-11-27 16:37                       ` Michael Shulman
2019-11-27 20:21                 ` Nicolas Alexander Schmidt [this message]
2019-11-04 18:42         ` Kevin Buzzard
2019-11-04 21:10           ` Michael Shulman
2019-11-04 23:26           ` David Roberts
2019-11-05 15:43           ` Daniel R. Grayson
2019-11-05 20:29             ` Yuhao Huang
2019-11-06 23:59               ` Daniel R. Grayson
2019-11-05 23:14           ` Martín Hötzel Escardó
2019-11-06  0:06             ` Stefan Monnier
2019-11-11 18:26               ` Licata, Dan
2019-11-03  7:29 ` Michael Shulman

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=c25dfb49-6b6e-d926-f8c3-4c590ca6f507@fromzerotoinfinity.xyz \
    --to=zero@fromzerotoinfinity.xyz \
    --cc=HomotopyTypeTheory@googlegroups.com \
    --cc=kevin.m.buzzard@gmail.com \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).