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

Mihails Milehins

6 September 2021

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.
BSD License

Depends On

Used by

Topics

Related Entries

Theories

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{http://isa-afp.org/entries/CZH_Elementary_Categories.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
Download