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

Mihails Milehins 📧

September 6, 2021

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

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

Session CZH_Elementary_Categories

Depends on

Used by

Cite

× 
@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: