| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
Category Theory
| Title: | Category Theory |
| Author: | Alexander Katovsky (apk32 /at/ cam /dot/ ac /dot/ uk) |
| Submission date: | 2010-06-20 |
| Abstract: | This article presents a development of Category Theory in Isabelle/HOL. A Category is defined using records and locales. Functors and Natural Transformations are also defined. The main result that has been formalized is that the Yoneda functor is a full and faithful embedding. We also formalize the completeness of many sorted monadic equational logic. Extensive use is made of the HOLZF theory in both cases. For an informal description see here [pdf]. |
| BibTeX: |
@article{Category2-AFP,
author = {Alexander Katovsky},
title = {Category Theory},
journal = {Archive of Formal Proofs},
month = jun,
year = 2010,
note = {\url{http://isa-afp.org/entries/Category2.shtml},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Status: [skipped] | This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |
Older releases:
|