
Category
Theory
with
Adjunctions
and
Limits
Title: 
Category Theory with Adjunctions and Limits 
Author:

Eugene W. Stark (stark /at/ cs /dot/ stonybrook /dot/ edu)

Submission date: 
20160626 
Abstract: 
This article attempts to develop a usable framework for doing category
theory in Isabelle/HOL. Our point of view, which to some extent
differs from that of the previous AFP articles on the subject, is to
try to explore how category theory can be done efficaciously within
HOL, rather than trying to match exactly the way things are done using
a traditional approach. To this end, we define the notion of category
in an "objectfree" style, in which a category is represented by a
single partial composition operation on arrows. This way of defining
categories provides some advantages in the context of HOL, including
the ability to avoid the use of records and the possibility of
defining functors and natural transformations simply as certain
functions on arrows, rather than as composite objects. We define
various constructions associated with the basic notions, including:
dual category, product category, functor category, discrete category,
free category, functor composition, and horizontal and vertical
composite of natural transformations. A "set category" locale is
defined that axiomatizes the notion "category of all sets at a type
and all functions between them," and a fairly extensive set of
properties of set categories is derived from the locale assumptions.
The notion of a set category is used to prove the Yoneda Lemma in a
general setting of a category equipped with a "hom embedding," which
maps arrows of the category to the "universe" of the set category. We
also give a treatment of adjunctions, defining adjunctions via left
and right adjoint functors, natural bijections between homsets, and
unit and counit natural transformations, and showing the equivalence
of these definitions. We also develop the theory of limits, including
representations of functors, diagrams and cones, and diagonal
functors. We show that right adjoint functors preserve limits, and
that limits can be constructed via products and equalizers. We
characterize the conditions under which limits exist in a set
category. We also examine the case of limits in a functor category,
ultimately culminating in a proof that the Yoneda embedding preserves
limits. 
Change history: 
[20180529]:
Revised axioms for the category locale. Introduced notation for composition and "in hom".
(revision 8318366d4575)
[20200215]:
Move ConcreteCategory.thy from Bicategory to Category3 and use it systematically.
Make other minor improvements throughout.
(revision a51840d36867)

BibTeX: 
@article{Category3AFP,
author = {Eugene W. Stark},
title = {Category Theory with Adjunctions and Limits},
journal = {Archive of Formal Proofs},
month = jun,
year = 2016,
note = {\url{http://isaafp.org/entries/Category3.html},
Formal proof development},
ISSN = {2150914x},
}

License: 
BSD License 
Depends on: 
HereditarilyFinite 
Used by: 
MonoidalCategory 
Status: [ok] 
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.

