| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
Category Theory for ZFC in HOL III: Universal Constructions
| Title: | Category Theory for ZFC in HOL III: Universal Constructions |
| Author: | Mihails Milehins (user9716869 /at/ gmail /dot/ com) |
| Submission date: | 2021-09-06 |
| 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. |
| BibTeX: |
@article{CZH_Universal_Constructions-AFP,
author = {Mihails Milehins},
title = {Category Theory for ZFC in HOL III: Universal Constructions},
journal = {Archive of Formal Proofs},
month = sep,
year = 2021,
note = {\url{https://isa-afp.org/entries/CZH_Universal_Constructions.html},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Depends on: | CZH_Elementary_Categories |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |
| Older releases: None |