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

- Mathematics/Category theory

### Session CZH_Universal_Constructions

- CZH_UCAT_Introduction
- CZH_UCAT_Universal
- CZH_UCAT_Limit
- CZH_UCAT_Limit_IT
- CZH_UCAT_Limit_Product
- CZH_UCAT_Limit_Pullback
- CZH_UCAT_Limit_Equalizer
- CZH_UCAT_Pointed
- CZH_UCAT_Representable
- CZH_UCAT_Complete
- CZH_UCAT_Comma
- CZH_UCAT_Set
- CZH_UCAT_Adjoints
- CZH_UCAT_Kan
- CZH_UCAT_PWKan
- CZH_UCAT_PWKan_Example
- CZH_UCAT_Conclusions

### Depends on

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

### Auto-related entries

- Category Theory for ZFC in HOL I: Foundations: Design Patterns, Set Theory, Digraphs, Semicategories
- Conditional Simplification
- Conditional Transfer Rule
- IDE: Introduction, Destruction, Elimination

## Cite

×

CZH_Universal_Constructions-AFP

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

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