
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

Submission date: 
20210906 
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 settheoretic 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 SetTheoretical 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_FoundationsAFP,
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://isaafp.org/entries/CZH_Foundations.html},
Formal proof development},
ISSN = {2150914x},
}

License: 
BSD License 
Depends on: 
Conditional_Simplification, Intro_Dest_Elim, ZFC_in_HOL 
Used by: 
CZH_Elementary_Categories 
