|
Category
Theory
for
ZFC
in
HOL
I:
Foundations:
Design
Patterns,
Set
Theory,
Digraphs,
Semicategories
Title: |
Category Theory for ZFC in HOL I: Foundations: Design Patterns, Set Theory, Digraphs, Semicategories |
Author:
|
Mihails Milehins (user9716869 /at/ gmail /dot/ com)
|
Submission date: |
2021-09-06 |
Abstract: |
This article provides a foundational framework for the formalization
of category theory in the object logic ZFC in HOL of the formal proof
assistant Isabelle. More specifically, this article provides a
formalization of canonical set-theoretic constructions internalized in
the type V associated with the ZFC in HOL,
establishes a design pattern for the formalization of mathematical
structures using sequences and locales, and showcases the developed
infrastructure by providing formalizations of the elementary theories
of digraphs and semicategories. The methodology chosen for the
formalization of the theories of digraphs and semicategories (and
categories in future articles) rests on the ideas that were originally
expressed in the article Set-Theoretical Foundations of
Category Theory written by Solomon Feferman and Georg
Kreisel. Thus, in the context of this work, each of the aforementioned
mathematical structures is represented as a term of the type
V embedded into a stage of the von Neumann
hierarchy. |
BibTeX: |
@article{CZH_Foundations-AFP,
author = {Mihails Milehins},
title = {Category Theory for ZFC in HOL I: Foundations: Design Patterns, Set Theory, Digraphs, Semicategories},
journal = {Archive of Formal Proofs},
month = sep,
year = 2021,
note = {\url{https://isa-afp.org/entries/CZH_Foundations.html},
Formal proof development},
ISSN = {2150-914x},
}
|
License: |
BSD License |
Depends on: |
Conditional_Simplification, Intro_Dest_Elim, ZFC_in_HOL |
Used by: |
CZH_Elementary_Categories |
|