Has anybody experience in mechanizing category theory or knows of such work?
I'm about to implement basic parts of category theory in a tactical theorem
prover based on higher order logic. I would appreciate to learn from anybody's
earlier experiences.
Thanks in advance,
Clemens
___________
Several categorical notions and results are formalized in the
Coq proof assistant, which is a tactical theorem
prover based on higher order logic.
The formalism used in Coq is the Calculus of Inductive Constructions.
For more details about Coq, see http://pauillac.inria.fr/coq
Gerard Huet and I formalized basic notions like categories, functors and
natural transformations, and proved some results like Yoneda's lemma.
This first part is described in the paper "Constructive Category Theory"
available in http://pauillac.inria.fr/bin/psearch/publioscope?huet
I pursued this axiomatisation to include a significant segment of category
theory, by defining standard constructions like limits, adjunctions, CCC...
The mechanically proved theorems include the Freyd's theorem for existence of
adjunct functor and the construction of limits from products and equalizers.
The complete axiomatisation is available with the last version of Coq
in http://pauillac.inria.fr/coq
Our goal is to develop a "readable" non-trivial (mechanically checked)
mathematics.
A new version of this axiomatisation is in development and will be
available soon.
It will improve the readability of:
- lemma statements: by using a mechanism of inheritance (a` la P. Aczel)
- proofs: by using a powerful rewriting tactics package.
The complete axiomatisation is described in a Report, in preparation.
We describe briefely the contents of the axiomatisation in the last version
of Coq.
BASIC NOTIONS
==============
RELATIONS
==========
| Relations.v : Equivalence, PER....
|
| (+ other files not used in this formalisation)
============================
SETOID ( 9 files )
=======
| Structure.v : Syntax for Records
| BasicTypes.v : Empty Type, Types of 1 and 2 elements
| Setoid.v : Setoid definition
| Single.v : Setoid with 1 element
| Map.v : Map between setoids
| MapProperty.v : Injective and surjective properties
| SetoidPROD.v : Binary product of setoids
| Setoid_prop.v : Sub-Setoids defined by comprehension
| Map2.v : Curryied binary maps between setoids
|
| STRUCTURE ( 4 files )
| ==========
| | Monoid.v : Monoid definition
| | FreeMonoid.v : Build a free monoid from a set
| | Group.v : Group Structure
| | Inverses_Group.v : The group of inverses pairs on a monoid
=========================
CATEGORY_THEORY
================
CATEGORY ( 8 files )
=========
| Category.v : Category structure
| Hom_Equality.v : Equality of 2 morphisms
| PermCat.v : The Group of permutations on an object of a Category
| ONE.v : Category 1
| SET.v : Category of Setoids
| MON.v : Category of Monoids
| Dual.v : Diual Category
| FullSubCat.v : Full Sub Category
| PROD.v : Product of Categories
|
| CONSTRUCTIONS ( 14 files )
| ==============
| | CatProperty.v : Epic, Iso, Initial...
| | SET_Terminal.v : Terminal object in SET
| | SETProperty.v : Epic, Monic in SET
| | Binary_Products.v : Binary products of objects of categories
| | SET_BinProds.v : Binary Products in SET
| | Products.v : Products of families of objects
| | Equalizers.v : Equalizers
| | SET_Equalizer.v : Equalizers in SET
| | Pullbacks.v : Pullbacks
| | SET_Pullback.v : Pullbacks in SET
| | Exponents.v : Exponents
| | SET_Exponents.v : Exponents in SET
| | CCC.v : CCC structure
| | SET_CCC.v : SET is CCC
| =======================
=========================
FUNCTOR ( 12 files )
========
| Functor.v : Functor structure
| FunctorProperty.v : Full anf faithful functors
| PROD_proj.v : Projection functors for the category AxB
| Dual_Functor.v : Dual of a functor
| FSC_inc.v : Inclusion functor for Full Sub-Category
| FunForget.v : Forgetful functor : MON -> SET
| FunFreeMon.v : Extension the free monoid construction to a functor
| HomFunctor.v : Hom-functor Hom(a,-)
| IdCAT.v : Identity functor
| CAT.v : Category of Categories
| Comma.v : Comma Category
| Comma_proj.v : Projection for Comma category
==========================
NT ( Natural Transformation 5 files )
===
| Ntransformation.v : Natural transformation structure
| HomFunctor_NT.v : Natural transformation between hom-fonctors
| NatIso.v : Natural isomorphism
| CatFunct.v : Category of fonctors
| InterChangeLaw.v : Inter change law
|
| YONEDA_LEMMA ( 4 files )
| =============
| | Ev.v : Evaluation functor
| | NatFun.v : Natfun functor
| | YonedaEmbedding.v : Yoneda Embedding
| | YonedaLemma.v : Yoneda Lemma
| ========================
==========================
LIMITS ( 14 files )
=======
| UniversalArrow.v : Unversal arrow structure
| FunForget_UA.v : Example of universal arrow
| CoUniversalArrow.v : Co-universal arrow
| Comma_UA.v : Relation between comma category and universal arrow
| Delta.v : Delta functor
| Limit.v : Limit
| Iso_Limit.v : Bijection (Cones c F) <-> Hom(c,F)
| CoLimit.v : Colimit
| Discr.v : Discrete category
| Products1.v : Products using limits
| PA.v : "Parallel Arrows" Category
| Equalizers1.v : Equalizers using limits
| PULB.v : ".<-.->" Category
| Pullbacks1.v : Pullbacks using limits
==========================
LIMIT_CONSTRUCTIONS ( 6 files )
====================
| SET_Complete.v : SET is complete
| Th_Limits.v : Limits by products and equalizers
| Pres_Limits.v : Preservation of limits
| HomFunctor_Continuous.v : Hom-foncteur Hom(a,-) is continuous
| Th_Initial.v : Existence of initial object
| Comma_Complete.v : Comma category is complete
===========================
ADJUNCTION ( 9 files )
===========
| HomFunctor2.v : Hom-fonctors Hom(F-,-) and Hom(-,G-)
| Adjunction.v : Adjunction
| Adj_UA.v : Relation between adjunctions and universal arrows
| Adjunction1.v : Other definition of adjunction
| Th_Adjoint.v : Existence of an adjoint
| Th_CoAdjoint.v : Existence of a coadjoint
| LeftAdj_Iso.v : Two left adjoints of a functor are iso
| Adj_FunFreeMon.v : FunFreeMon is the left adjoint of the forgetful functor
| Limit_Adj.v : Limits and adjunctions
|
| CCC ( 6 files )
| ====
| | FunOne.v : Functor !C : C -> 1
| | Terminal1.v : Terminal object using adjunctions
| | Diagonal.v : Diagonal functor
| | Cartesian1.v : Cartesian category using adjunctions
| | FunProd.v : Functor -xa
| | CCC1.v : CCC using adjunctions
| =======================
|
| FREYD_THEOREM (FAFT = Freyd's Adjoint Functor Theorem) ( 4 files )
| ==============
| | FAFT_SSC2.v : The Solution Set Condition
| | FAFT_Part1.v : Necessary condition
| | FAFT_Part2_Proof1.v : Sufficient condition (1st proof)
| | FAFT_Part2_Proof2.v : Sufficient condition (2nd proof)
| =======================
=========================
Amokrane Saibi
saibi@pauillac.inria.fr