### 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.

### License

BSD License

### Topics

- Mathematics/Category theory
- Logic/Set theory

### Session CZH_Foundations

- CZH_Sets_MIF
- CZH_Utilities
- CZH_Introduction
- CZH_Sets_Introduction
- CZH_Sets_Sets
- CZH_Sets_Nat
- CZH_Sets_BRelations
- CZH_Sets_IF
- CZH_Sets_Equipollence
- CZH_Sets_Cardinality
- CZH_Sets_Ordinals
- CZH_Sets_FSequences
- CZH_Sets_FBRelations
- CZH_Sets_VNHS
- CZH_Sets_NOP
- HOL_CContinuum
- CZH_Sets_ZQR
- CZH_EX_Replacement
- CZH_EX_TS
- CZH_EX_Algebra
- CZH_Sets_Conclusions
- CZH_DG_Introduction
- CZH_DG_Digraph
- CZH_DG_Small_Digraph
- CZH_DG_DGHM
- CZH_DG_Small_DGHM
- CZH_DG_TDGHM
- CZH_DG_Small_TDGHM
- CZH_DG_PDigraph
- CZH_DG_Subdigraph
- CZH_DG_Simple
- CZH_DG_GRPH
- CZH_DG_Rel
- CZH_DG_Par
- CZH_DG_Set
- CZH_DG_Conclusions
- CZH_SMC_Introduction
- CZH_SMC_Semicategory
- CZH_SMC_Small_Semicategory
- CZH_SMC_Semifunctor
- CZH_SMC_Small_Semifunctor
- CZH_SMC_NTSMCF
- CZH_SMC_Small_NTSMCF
- CZH_SMC_PSemicategory
- CZH_SMC_Subsemicategory
- CZH_SMC_Simple
- CZH_SMC_Rel
- CZH_SMC_Par
- CZH_SMC_Set
- CZH_SMC_GRPH
- CZH_DG_SemiCAT
- CZH_SMC_SemiCAT
- CZH_SMC_Conclusions

### Depends on

- Conditional Simplification
- IDE: Introduction, Destruction, Elimination
- Zermelo Fraenkel Set Theory in Higher-Order Logic

### Used by

- Category Theory for ZFC in HOL II: Elementary Theory of 1-Categories

### Auto-related entries

- Category Theory for ZFC in HOL II: Elementary Theory of 1-Categories
- Category Theory for ZFC in HOL III: Universal Constructions
- Conditional Transfer Rule

## Cite

×

CZH_Foundations-AFP

    @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   = {September},
      year    = {2021},
      note    = {\url{https://isa-afp.org/entries/CZH_Foundations.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Oct 5, 2021 : Isabelle2021
- Sep 14, 2021 : Isabelle2021