Email Gateway (Apr 20 2021 at 19:01): Email Gateway (Apr 20 2021 at 19:01):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]
Email Gateway (Apr 21 2021 at 10:59):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
Email Gateway (Apr 21 2021 at 11:17):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
Email Gateway (Apr 21 2021 at 18:38):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 :-).
Email Gateway (Apr 22 2021 at 09:38):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
Email Gateway (Apr 22 2021 at 09:45):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
Email Gateway (Apr 22 2021 at 12:57):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.
Email Gateway (Apr 22 2021 at 21:07):From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear Lawrence Paulson/Jason Gross/All,
Thank you for your comments.
Email Gateway (Apr 23 2021 at 01:51):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.
Email Gateway (Apr 23 2021 at 11:04):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
Email Gateway (Apr 23 2021 at 11:29):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
Email Gateway (Apr 23 2021 at 11:37):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
Email Gateway (Apr 24 2021 at 00:19):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
Email Gateway (Apr 24 2021 at 00:34):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.
Email Gateway (Apr 24 2021 at 22:41):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: Jul 15 2022 at 23:21 UTC