Category Theory for ZFC in HOL III: Universal Constructions

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

The article provides a formalization of elements of the theory of universal constructions for 1-categories (such as limits, adjoints and Kan extensions) in the object logic ZFC in HOL of the formal proof assistant Isabelle. The article builds upon the foundations established in the AFP entry Category Theory for ZFC in HOL II: Elementary Theory of 1-Categories.

License

BSD License

History

May 16, 2022
creation and preservation of limits (revision 68412a363595)

Topics

Session CZH_Universal_Constructions

Depends on

Cite

× 
@article{CZH_Universal_Constructions-AFP,
  author  = {Mihails Milehins},
  title   = {Category Theory for ZFC in HOL III: Universal Constructions},
  journal = {Archive of Formal Proofs},
  month   = {September},
  year    = {2021},
  note    = {\url{https://isa-afp.org/entries/CZH_Universal_Constructions.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: