From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>

Dear All,

I noticed that the recent AFP entry on Grothendieck's Schemes (

https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2021-April/msg00016.html)

[0] also has an article associated with it (arxiv.org:

https://arxiv.org/abs/2104.09366) [1].

I hope it would not be inappropriate of me to ask a few questions about

certain elements of the content of [1] and provide several remarks on

certain aspects of the development that is described in the article.

Section 1 contains the following passage:

In particular, the present work makes a triple contribution to

Isabelle/HOL: a first building block towards a new topology library, a new

building block towards a library for abstract algebra and finally a

formalization of schemes.

Given that the information about the "new topology/abstract algebra"

libraries is now not only in the public domain, but a part of an official

publication, I would like to kindly ask the authors whether it would be

possible to provide more information about these new developments? Are the

existing HOL-Algebra/HOL-Analysis libraries meant to be refactored in a

non-backward compatible manner? Will this new development affect the

topology library that is currently a part of the main library of

Isabelle/HOL? Is this topology library also going to be

replaced/deprecated? I believe that all of the existing users of these

libraries deserve to know about their future :-).

Section 2 contains the following passage:

Even using locales, we can still go wrong. The root of the problems in

HOL-Algebra is the desire to refer to a structure such as a group with its

components using a single variable, as a record data structure. The new (at

the time) extensible records seemed perfect for the task. But they led to

some peculiarities: notably, the locale abelian_group (in Theory Ring)

which presents the odd twist of requiring a ring structure. The lack of

multiple inheritance for records seems to have required the awkward use of

the ring record for abelian groups. However, Clemens Ballarin recently

conducted an experiment [...] showing that locales, without records, allow

for a smooth handling of basic algebraic structures in Isabelle such as

monoids, groups and rings. We decided to base our formal development on

this experiment.

Furthermore, section 3 describes the "new topology library":

Our new topology library is entirely built on locales without using type

classes or type declarations (via the typedef command). In particular, our

topological spaces have explicit carrier sets as part of their data instead

of using UNIV, the set of all elements of some type, or having to define it

later as the union of all the open sets.

From these passages and the comments above, my guess is that there is an

intention to develop the new algebra/topology libraries for Isabelle/HOL

based on this pattern.

In this context, I would like to mention that, in a certain sense, I have

already achieved a certain degree success (and failures) in this direction

(and I was not the first one), albeit in connection with my work on

Types-To-Sets, and I thought that it may be relevant to share my experience

here and one of the main conclusions of my own attempts.

Generally, (what I call) the *design pattern* that was used in [2] in the

context of algebra, in my opinion, is very similar to the design pattern

that was originally proposed by Ondřej Kunčar and Andrei Popescu in their

work on Types-To-Sets [3] in the context of both algebra and topology (I am

referring, primarily, to the examples associated with the article and not

the article itself) and later developed further into a part of a small case

study by Fabian Immler and Bohua Zhan [4]. Thus, for example, the locale

for the definition of a semigroup from [4] looks like

locale semigroup_add_on_with =

fixes S::"'a set" and pls::"'a⇒'a⇒'a"

assumes add_assoc: "a ∈ S ⟹ b ∈ S ⟹ c ∈ S ⟹ pls (pls a b) c = pls a (pls

b c)"

assumes add_mem: "a ∈ S ⟹ b ∈ S ⟹ pls a b ∈ S"

I have continued this work and developed several small libraries that are

meant to showcase different design patterns that can be used for the

development of libraries in Isabelle/HOL based around the same idea in 2019

and 2020. Fundamentally, all of these libraries use a very similar design

pattern based on explicit locale parameters with explicitly fixed

carrier/underlying sets for modeling all possible mathematical structures

(I use the term mathematical structure informally). The current iteration

is available here: https://gitlab.com/user9716869/tts_examples. For

example, the definition of (e.g.) topological space in [1] is based on the

same idea as in that library (

https://mailman46.in.tum.de/pipermail/isabelle-dev/2019-April/016894.html).

Compare:

(from https://gitlab.com/user9716869/tts_examples)

locale topological_space_ow = fixes 𝔘 :: "'at set" and τ :: "'at set ⇒

bool"

assumes open_UNIV[simp, intro]: "τ 𝔘"

assumes open_Int[intro]: "⟦ S ⊆ 𝔘; T ⊆ 𝔘; τ S; τ T ⟧ ⟹ τ (S ∩ T)"

assumes open_Union[intro]: "⟦ K ⊆ Pow 𝔘; ∀S∈K. τ S ⟧ ⟹ τ (⋃K)"

(from [1])

locale topological_space = fixes S :: "'a set" and is_open :: "'a set ⇒

bool"

assumes open_space [simp, intro]: "is_open S" and open_empty [simp,

intro]: "is_open {}"

and open_imp_subset: "is_open U ⟹ U ⊆ S"

and open_inter [intro]: "⟦is_open U; is_open V⟧ ⟹ is_open (U ∩ V)"

and open_union [intro]: "⋀F::('a set) set. (⋀x. x ∈ F ⟹ is_open x) ⟹

is_open (⋃x∈F. x)"

I hope that the remarks above will suffice to give my further claims a

certain degree of credibility, as it seems that the ideas (albeit, not

entirely my own ideas) that I was trying to promote in 2019 are beginning

to be adapted by the community :-). By the way, it might be appropriate to

add references to (at least) [3], [4] and the aforementioned post by Fabian

Immler (if not my own repository), in connection with the design pattern

being used, given that it seems to be one of the matters emphasized in [1].

I would like to be very clear, however, that I have little concern about

what decision will be made with regard to this matter and this is very far

from being the main issue that I would like to discuss in this post.

I have already summarised some of my concerns about the design pattern

being used in [1] in the following post on the mailing list:

https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2019-August/msg00006.html.

However, since then, I developed further concerns about it. Unfortunately,

in my experience, using explicit parameters for the definition of

mathematical structures makes it difficult to talk about the interplay

between different structures, e.g. using tools and techniques from category

theory or similar. Furthermore, carrying around dramatically large lists of

explicitly stated parameters can become unwieldy very quickly as the

structures become more complex (see my remarks in

https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2019-August/msg00006.html

for further information).

Finally, I converged on the opinion that there has to exist a canonical

methodology for representing any mathematical structure as a term of some

type (e.g. by using product types or similar). If this is so, then why

would one wish to define such structures using explicitly stated locale

parameters?

Once again, from [1],

The new (at the time) extensible records seemed perfect for the task. But

they led to some peculiarities: notably, the locale abelian_group (in

Theory Ring) which presents the odd twist of requiring a ring structure.

My opinion is that this is the only problem of the record + locale

approach, and it is not insurmountable. That is, the problem is that the

records lack a mechanism for multiple inheritance. Perhaps, the key to its

solution lies in the following comments made by Andreas Lochbihler in reply

to one of my questions:

https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2019-August/msg00017.html.

I believe that I have already solved the crux of the problem by following

up on one of the ideas expressed in the aforementioned post by Andreas

Lochbihler and providing yet another design pattern that allows for

mimicking records with multiple inheritance. At the moment, this pattern is

quite unwieldy, but it can be fully automated, potentially (of course, this

would require a considerable amount of programming effort).

I describe it based on a close-to-minimal example that is provided as a

copy at the end of the email in Appendix A. Hopefully, with the comments in

the code, the example provides a self-sufficient explanation of the pattern

(however, this variant of the pattern is slightly outdated, as the pattern

has been slightly improved since the example was developed). As such, the

example does not showcase the use of multiple inheritance, as it would make

the example too long. However, hopefully, it should be apparent to see that

multiple inheritance is not an issue for the design pattern, as it is

possible to 'upcast' a 'multirecord' to any 'multirecord' with the 'parent

structure' with ease (of course, privately, I have already developed use

cases for the demonstration of multiple inheritance). Overall, I used this

inheritance mechanism to define (and reason about) semifunctors,

categories, functors, natural transformations, dagger

digraphs/semicategories/categories, and several other concepts, not

necessarily related to category theory (e.g. topological spaces). Moreover,

it is possible to combine the inheritance mechanism with the inheritance of

the fields of the record. This is used, for example, to ensure that a

semifunctor from one semicategory to another (stated as a locale) inherits

from the digraph homomorphism from one digraph to another in a canonical

manner.

At first sight, it may seem that using records+unrest

[message truncated]

From: Lawrence Paulson <lp15@cam.ac.uk>

The current HOL-Analysis library is huge. It has been refactored already and without doubt it will undergo further refactorings in the future. It is however in no way deprecated, nor even HOL-Algebra, although the latter deserves to be. To replace either would take an enormous amount of manpower, which we don’t have.

What we can expect to see our series of experiments trying to push the boundaries of what we can formalise, with an eye in particular to further developing this locale methodology, which seems to work so well.

Larry

From: Lawrence Paulson <lp15@cam.ac.uk>

I think the Isabelle community as a whole welcomes all demonstrations of useful methodologies for formalising mathematics. This particular paper on schemes was in response to a challenge made by Kevin Buzzard concerning the expressiveness of simple type theory. Other methodologies could be demonstrated by tackling the same example. It is indeed a long series of definitions and proofs, but now that both the paper and the formal development are available, it should be easier for other groups to give it a try. I would be happy to see improvements to our own work.

The AFP already contains many alternative formalisations of the same mathematical ideas, and there is no plan to impose any one approach.

Larry

From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>

Dear Lawrence Paulson/All,

Thank you for your replies. Also, I do apologize for starting such a long

and slightly chaotic thread yesterday. I will try to be more to the point

today.

I would like to clarify that my thread was hardly about the entire

formalization study that is presented in [1], but, primarily, about the

proposal to develop a new library for topology based on the locale +

explicit locale parameters/explicit carrier set approach. The pattern that

is proposed in [1] is the one that I advocated in the first half of 2019.

However, at the time, your reaction to this idea seemed to vary from

possibly mildly critical to tentatively inquisitive. Given that my own

experience with formal methods and Isabelle was minimal at the time, I kept

worrying about whether I am, indeed, doing something wrong and how much my

work would be criticized, if I was to make an attempt to publish it. The

only person who seemed to be mildly supportive of this idea at the time was

Fabian Immler (

https://mailman46.in.tum.de/pipermail/isabelle-dev/2019-April/016894.html):

not surprisingly, my own approach evolved from Fabian Immler and Bohua

Zhan's approach to the formalization of elements of algebra in [2] and the

examples associated with [3]. The support of Fabian Immler was sufficient

for me to continue that work. However, to this date, I had some concerns

about how it could be received, and my non-conventional approach to

topology was one. of the contributing factors. Of course, I was very

surprised to see that, in [1], nearly an entire section was dedicated to

advocating the use of what I would consider being the same pattern that

seemed to lack your support at the time of its proposal. In any case, I

welcome this event as good news, as it reinforces my self-esteem and my

belief in my own ideas :-).

From: Lawrence Paulson <lp15@cam.ac.uk>

The HOL-Analysis library already contains a substantial development of abstract topology, which I ported from HOL Light some years ago, and which has none of the limitations connected with type classes. I this version is probably no worse than one defined using locales.

But as for your own proposal in 2019, it looks like you were ahead of your time. It was not until 2020 that Clemens’ paper appeared:

Clemens Ballarin, Exploring the Structure of an Algebra Text with Locales

Journal of Automated Reasoning 64, pages 1093–1121 (2020)

This was the inspiration for our development.

Larry

From: Lawrence Paulson <lp15@cam.ac.uk>

On the topic of category theory: I know mine is a minority view, but category theorists need to come up with a consistent theory before they can expect formal reasoning in any system. Allow me to quote Pierre Cartier:

"Nowadays, one of the most interesting points in mathematics is that, although all categorical reasonings are formally contradictory, we use them and we never make a mistake. Grothendieck provided a partial solution in terms of universes but a revolution of the foundations similar to what Cauchy and Weierstrass did for analysis is still to arrive. In this respect, he was pragmatic: categories are useful and they give results so we do not have to look at subtle set theoretic questions if there is no need. Is today the moment to think about these problems? Maybe…”

Larry

From: Jason Gross <jasongross9@gmail.com>

all categorical reasonings are formally contradictory

From what I could find on Google (https://mathoverflow.net/a/23612/30462)

this is a quote from 2009, and Cartier goes on to propose formalizing

category theory in proof assistants. In fact basic category theory has

been formalized in proof assistants many times now (I've personally made or

contributed to formalizations in Coq, Agda, and Lean, and there are dozens

besides me and at least one in Isabelle/HOL (

https://mathoverflow.net/questions/152497/formalizations-of-category-theory-in-proof-assistants)).

I've found that universe polymorphism, which Cartier seems to see as a bit

of a kludge, is in fact invaluable in formalizations of category theory, so

that I can define category once and get a definition at all universe

levels, whence I can easily apply any of my constructions to the (larger)

category of (smaller) categories, in a way that's parametric over the

particular universes I'm using. (Though in fact I've heard that three

universes is generally enough: we merely need to talk about small

categories and about locally small categories, and then we can have the

locally small category of all small categories.)

Additionally, there's some recent work that gives a type theory for

oo-categories (https://arxiv.org/abs/2007.08307) which I saw a lecture on

just yesterday, which seems to me to at least be in the direction of giving

synthetic rules for category theory that don't lead to contradictions.

From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>

Dear Lawrence Paulson/Jason Gross/All,

Thank you for your comments.

From: "Eugene W. Stark" <isabelle-users@starkeffect.com>

I have been following this thread and as the author of [3-5] I would like to chime in with a comment,

for what it is worth, and also a question about the quoted text below.

My comment is that although the inability of HOL to support the formalization of "large" categories certainly

does have some implications as regards the applicability of an HOL formalization of category theory

(e.g. one cannot construct in HOL a cartesian closed category, having objects that are sets and having homs

that consist of all functions from their domain to their codomain, unless we only admit finite sets as

objects), there are many applications of category theory for which the consideration of such large categories

is not required. It just seems to be that some people are more focused on the foundational aspects of category

theory and others on applications that only need to make use of "small" categories. I tend to align more with

the latter point of view, so I have not worried so much about the foundational aspects that could not be

adequately formalized. I find that I care about having a category of all sets about as much (or as little)

as I care about having a type of all sets; mostly I don't worry about it.

My question is that I would like to understand better something that was said in the quoted text below

regarding the supposed impossibility of treating the collections of all real numbers and all complex numbers

as two distinct objects in (for example) the category Top. What I don't understand about this I don't see

what is stopping us from constructing a category, at least up to equivalence, of topological spaces whose

sets of points are bounded by some fixed cardinality. For example, both the real numbers and the complex

numbers have the cardinality of the continuum. A topological space on either of these can be represented

as a certain collection of subsets of these sets with continuum-many elements. We can then certainly form

(in HOL) a category having all such collections as its objects, and all continuous functions between such

collections as its arrows. The objects and arrows of the category would inhabit a somewhat higher type,

but there is no problem in obtaining it. Unless I am missing something basic, I don't see the difficulty

in carrying out this construction, e.g. using the formalization in [3]. So perhaps something else was meant,

in which case I would like to understand what it was.

Perhaps I have missed what was intended by the phrase "so long as real numbers and complex numbers are

modelled as two distinct types and not distinct terms of some other type". Does this mean that somehow

some particular construction of "the" real numbers and "the" complex numbers are to be given special

status, and that to be useful, a category Top of topological space would have to contain as objects the

precise results of these particular distinguished constructions, as opposed to merely having some

objects R and C for which for which the induced topologies on hom(1, R) and hom(1, C) are homeomorphic

to the spaces of real numbers, and complex numbers, respectively? I don't see why this would be of such

great importance.

From: Lawrence Paulson <lp15@cam.ac.uk>

Thanks for your comments. I look forward to seeing formalisations of schemes (and other challenging pieces of mathematics) from you and others, using a variety of techniques. Proof methodologies seem to be developing rapidly at the moment!

Larry

From: Lawrence Paulson <lp15@cam.ac.uk>

It might be worth mentioning that the AFP development ZFC_in_HOL makes progress in this direction, establishing through the typecast system that a great number of types (including real and complex) are “small”, which means they can be embedded into sets in the ZF universe. An ambitious person could do something with this.

Larry

From: Lawrence Paulson <lp15@cam.ac.uk>

I am not sure this helps, since from a set theoretic point of view, we have a proper class of one element groups, even though they are all isomorphic. The thing you want to limit is the rank of the carrier set, not the cardinality. Extremely small ranks are sufficient for doing quite large chunks of mathematics.

To the best of my knowledge, we don’t have many useful tools for reasoning in the style of category theory within higher-order logic.

Larry

From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>

Dear Eugene W. Stark/All,

Thank you for your remarks.

My criticism of Isabelle/HOL in connection with applied category theory was

twofold:

- Firstly, I claimed that the existing frameworks for doing category

theory cannot be applied to the canonical constructions conveniently (this

argument has little to do with what kind of categories we can construct in

Isabelle/HOL: I provide more details below).

- My second argument was related to the impossibility of the

construction of certain large categories.

It seems that we both agree that Isabelle/HOL's size limitations are quite

severe, although, perhaps, they do not have a significant impact on your

own work. From my perspective, this is a very strong and rather objective

argument against Isabelle/HOL (please do remember that my arguments were

aimed predominantly at the Isabelle/HOL, not any specific formalization of

category theory), merely because there exist formal systems that do not

have these limitations; at least, they are less severe to the point of

making such systems suitable for performing the vast majority of

constructions in the published literature, including almost anything that

involves reasonably large categories. From what I have seen, most commonly,

mathematics is exposed in systems that are equiconsistent with or stronger

than ZFC (more specifically, most of the mathematics in the published

literature seems to be exposed using some logic of the order higher or

equal than 1 + the axioms of ZFC or MK, or, if category theory is involved,

either TG or the one-universe axiomatization of Mac Lane, even if this is

not always stated explicitly). It seems to me then that the consistency

strength greater or equal to that of the ZFC is a prerequisite for any

formal system to be accepted as some general medium for the communication

and storage of mathematical knowledge. Whether or not a significant

fraction of the ideas that are expressed using such systems can also be

expressed in Isabelle/HOL, I find slightly irrelevant. The question comes

down to why would one wish to use Isabelle/HOL in favor of stronger systems

(at least, equiconsistent with the ZFC) that are already available.

As a side note, in my opinion, the systems like ZFC in HOL and HOTG come

closest to what is conventionally used for the exposition of mathematics.

Personally, having tried formalizing mathematics in ZFC in HOL (e.g., see

https://gitlab.com/category-theory-for-zfc-in-hol), I found that it is

almost as easy and convenient as "copying" mathematics from textbooks.

On 23 Apr 2021, Eugene W. Stark wrote

My question is that I would like to understand better something that was

said in the quoted text below

regarding the supposed impossibility of treating the collections of all

real numbers and all complex numbers

as two distinct objects in (for example) the category Top.

Perhaps I have missed what was intended by the phrase "so long as real

numbers and complex numbers are

modelled as two distinct types and not distinct terms of some other

type". Does this mean that somehow

some particular construction of "the" real numbers and "the" complex

numbers are to be given special

status...

a). My first argument was hardly concerned with the issues related to size

(this is covered by the second, more important, argument), but mere

practical convenience of using the results about specific categories

that can be exposed in Isabelle/HOL. I am inclined to tentatively give a

positive answer to the question "Does this mean that somehow some

particular construction of "the" real numbers and "the" complex numbers are

to be given special status?". At the moment, the transfer infrastructure of

Isabelle/HOL still has a number of limitations, so it is not that easy to

transfer the results automatically from, e.g., an existing type real to its

isomorphic copy embedded in some other type and vice versa. At the very

least, it requires some amount of tedious manual labor (also, if our copy

of the real numbers is no longer a type, we cannot even instantiate it as,

e.g., a canonical field from the standard library). Perhaps, in the future,

the transfer infrastructure of Isabelle/HOL will be perfected to the point

that I would no longer try to use such an argument. But this would, yet

again, require a substantial amount of labor in a different direction.

In essence, my first argument is slightly subjective and comes down to how

much one is prepared to sacrifice convenience and conventional

Isabelle/HOL's approach of treating distinct mathematical structures as

distinct types in favor of being able to apply the tools of category theory

to them. Another problem is that similar issues seem to hardly exist in

most of the other formal systems that I have tried thus far, or, somehow,

are easier to deal with, subjectively.

b). As a side remark, the chosen name of the category in my last email is

misleading, and, perhaps, led to an alternative interpretation of the

argument that I was trying to make. In my original email (

https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2021-April/msg00062.html)

I was more careful and stated "something similar to the category Top

(whatever can be achieved taking into consideration the size limitation of

Isabelle/HOL).". Indeed, I have not analyzed in detail as to how much

exactly can be done in this direction in Isabelle/HOL alone and exactly how

close we can get: perhaps, you can provide an affirmative answer to this

question.

Kind Regards,

Mikhail Chekhov

From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>

Dear Lawrence Paulson/All,

Thank you for your comments.

Indeed, one ambitious person has already tried doing something similar in

Isabelle/ZF in 2010 [1]. Indeed, in Category2, the concept of a category is

defined in arbitrary types, but it uses the type ZF for the development of

the category Set, defining all related concepts via isomorphisms. I did

modernize a large part of this development some time ago (this work is not

publicly available), adapting it to V from ZFC in HOL, but I have given up

on this approach in favor of internalizing everything in V and simply

treating HOL as (indeed) a logic, merely a better alternative to FOL (see

https://gitlab.com/category-theory-for-zfc-in-hol). Nonetheless, I still

use the mechanism that you mentioned for the transfer of some of the

relevant properties exposed in HOL to the sets in V. For example, see my

exposition of the integer/rational/real numbers and finite sequences in

https://gitlab.com/category-theory-for-zfc-in-hol/czh_sets: most of the

properties were transferred automatically using the capabilities of

transfer [2].

Kind Regards,

Mikhail Chekhov

[1] Katovsky A. Category Theory. Archive of Formal Proofs. 2010;

[2] Huffman B, Kunčar O. Lifting and Transfer: A Modular Design for

Quotients in Isabelle/HOL. In: Gonthier G, Norrish M, editors. Certified

Programs and Proofs. Heidelberg: Springer; 2013. p. 131–46.

From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>

Dear Eugene W. Stark/All,

I would like to make a minor correction and provide a couple of side

remarks for the post attached after my signature.

*Correction*

The last sentence in my post in the attachment should not contain the word

"affirmative" :-).

*Side remarks*

I would like to add a couple of further arguments for clause a), hopefully

reinforcing the arguments already provided. In Isabelle/HOL, once one

defines, for example, a type of real numbers, it is possible to instantiate

it as, e.g., a group or a topological space using type classes. Then, all

theorems about groups/topological spaces become available for this type

automatically. Ideally, in my view, an "applicable category theory"

framework would need to work exactly like this. Thus, if we have a few

specific constructions defined in Isabelle/HOL and we notice that they form

a category, we would like to simply prove the axioms of a category for

these specific constructions and get the theorems for categories for free,

instantiated for these specific constructions (this is exactly where the

desire to single out some distinguished user-defined constructions comes

from). Unfortunately, in my view, many of the typical applications for

which such a framework could be useful would have categories whose

objects/arrows span multiple types, provided that we do not attempt to move

away from the existing infrastructure that has already been developed for

Isabelle/HOL.

Yet another side remark is that it is possible to do something similar to

what I describe above in Isabelle/HOL by the exploitation of schematic

polymorphism: see the screenshot attached to this email (this also appeared

in

https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2020-July/msg00050.html)

and please ignore everything that you see there apart from the idea for the

software implementation. Unfortunately, I found this idea to be too

labor-intensive to be practical: effectively, to provide such a framework

we would need to "hard-code" all theorems (and their proofs) about

categories in Isabelle/ML.

Kind Regards,

Mikhail Chekhov

MCATS.png

Last updated: Jan 25 2022 at 01:11 UTC