### Abstract

This article provides a formalization of the foundations of the theory of 1-categories in the object logic ZFC in HOL of the formal proof assistant Isabelle. The article builds upon the foundations that were established in the AFP entry Category Theory for ZFC in HOL I: Foundations: Design Patterns, Set Theory, Digraphs, Semicategories.

### License

BSD License

### History

November 7, 2021
  added a definition of a dagger monoidal category (revision c9ed46c09de9)

### Topics

- Mathematics/Category theory

### Session CZH_Elementary_Categories

- CZH_ECAT_Introduction
- CZH_ECAT_Category
- CZH_ECAT_Small_Category
- CZH_ECAT_Functor
- CZH_ECAT_Small_Functor
- CZH_ECAT_NTCF
- CZH_ECAT_Small_NTCF
- CZH_ECAT_PCategory
- CZH_ECAT_Subcategory
- CZH_ECAT_Simple
- CZH_ECAT_Discrete
- CZH_ECAT_SS
- CZH_ECAT_Parallel
- CZH_ECAT_Comma
- CZH_ECAT_Rel
- CZH_ECAT_Par
- CZH_ECAT_Set
- CZH_ECAT_GRPH
- CZH_ECAT_SemiCAT
- CZH_DG_CAT
- CZH_SMC_CAT
- CZH_ECAT_CAT
- CZH_DG_FUNCT
- CZH_SMC_FUNCT
- CZH_ECAT_FUNCT
- CZH_ECAT_Hom
- CZH_ECAT_Cone
- CZH_ECAT_Small_Cone
- CZH_ECAT_Yoneda
- CZH_ECAT_Order
- CZH_ECAT_Small_Order
- CZH_ECAT_Ordinal
- CZH_ECAT_CSimplicial
- CZH_ECAT_Structure_Example
- CZH_ECAT_Conclusions

### Depends on

- Category Theory for ZFC in HOL I: Foundations: Design Patterns, Set Theory, Digraphs, Semicategories

### Used by

- Category Theory for ZFC in HOL III: Universal Constructions

### Auto-related entries

- Category Theory for ZFC in HOL III: Universal Constructions
- Soundness of the Q0 proof system for higher-order logic
- MLSS Decision Procedure
- Conditional Simplification
- Conditional Transfer Rule

## Cite

×

CZH_Elementary_Categories-AFP

    @article{CZH_Elementary_Categories-AFP,
      author  = {Mihails Milehins},
      title   = {Category Theory for ZFC in HOL II: Elementary Theory of 1-Categories},
      journal = {Archive of Formal Proofs},
      month   = {September},
      year    = {2021},
      note    = {\url{https://isa-afp.org/entries/CZH_Elementary_Categories.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