Email Gateway (Jan 01 2024 at 23:54): Email Gateway (Jan 01 2024 at 23:54):From: Mihails Milehins <mihailsmilehins@gmail.com>
Dear All,
I would like to make several remarks about the entries CZH_* on the AFP:
I may have mentioned to several members of the community that I have an
intention to continue improving these entries and provide further material.
However, it is likely that this will not be possible. I have not been able
to find the time and/or the computational resources to continue this work
thus far, and I doubt that this will change in the foreseeable future.
Moreover, I noticed that HOTG started taking shape once again and there is
further relevant automation that became available recently [1]. From my
perspective, TG is a more natural setting for formalization of category
theory than ZFC. Furthermore, from my experience, the automation provided
in [1] could be "game changing" in the context of the formalization of
mathematics in set-theoretic foundations at large (be it ZFC or TG). This
makes it less appealing to continue the development of my own formalization
(without, at least, a significant overhaul based on [1]). Naturally, I will
try to do my best to maintain the content that has already been published
on the AFP.
While I have accrued some further material beyond what is currently in
the AFP (Freyd's General Adjoint Functor Theorem and its applications in
algebra, quotient categories, further material on dagger categories), I do
not believe that I have enough material for a conference paper on this
topic. However, if anyone from the community could agree to provide an
endorsement for a relevant subject area on Arxiv, I would like to upload a
short note about these entries. The reasons for this are two-fold:
2.1. While the scope of the formalization is quite narrow, I believe that
this may have been the first substantial formalization (in a proof
assistant) of category theory with the categories defined on the stages of
the von Neumann hierarchy, rather than the Grothendieck's universes.
2.2. The formalization largely rests on the homegrown automation
(Conditional_Simplification), which has advantages (and some disadvantages)
over the traditional classical methods (auto/force) that combine classical
reasoning and rewriting. Again, I believe that this may be the first use
case (at least in the context of Isabelle) for this type of algorithm, and
(efficiency matters aside) I found it exceptionally convenient in a
set-theoretic setting (or any setting with theorems that contain a large
number of non-trivial premises).
Of course, I would be happy to be proven wrong about either/both of the
claims above.
[1] K. Kappelmann, “Transport via Partial Galois Connections
and Equivalences,” in APLAS 2023: Programming Languages and Systems,
Taipei, Taiwan, C.-K. Hur, Ed., in Lecture Notes in Computer Science.
Singapore: Springer Nature, 2023, pp. 225–245. doi:
10.1007/978-981-99-8311-7_11.
Kind Regards,
Mihails Milehins
(he/him/his)
Last updated: Jan 04 2025 at 20:18 UTC