Re: Evil in bicategories

[Toby Bartels <toby+categories@ugcs.caltech.edu>]

David Leduc wrote:

>You both mention a definition of higher categories based on dependent
>type theory.
>Where does it appear?
>I cannot find such definition in the guide book by Cheng and Lauda.
>Can/has it be implemented in a proof assistant like Coq?

Most authors (including Cheng and Lauda) don't get into
the logical details of what is and is not evil,
so they don't discuss how it works in dependent type theory.
Nevertheless, any definition of bicategory that runs like this:
*  a collection of objects;
*  for each pair of objects, a collection of morphisms;
*  etc
is written the language of dependent type theory.

You can see examples at http://ncatlab.org/nlab/show/bicategory
(the brief definition is perfectly explicit in this way,
although it does not include all of the details;
the detailed definition leaves the declarations of some variables implicit,
although you could always stick their definitions up front,
making it a complete and perfectly explict dependent-type definition).

Actually, talking about bicategories is a red herring;
all of the issues come up already for categories.
You might as well have asked, in your original post,
why we know that the source and target of (h o g) o f and h o (g o f)
are equal when stating the associativity law in the definition of a category.
The answer is the same: when stating the associativity law,
you begin with objects W,X,Y,Z and go on from there.

I haven't seen a definition of bicategories in Coq,
but certainly the explicit definition on the nLab could be done in Coq.
But as I said, the issues already arise for ordinary categories.
For a definition of these in Coq, see http://coq.inria.fr/contribs/ConCaT.html
with http://coq.inria.fr/contribs/ConCaT.CATEGORY_THEORY.CATEGORY.Category.html
as the file that contains the definition of category itself.
(Although Coq has equality at all types, and so can express evil,
this equality is never used except within a given hom-set,
as you can see in that file and also in the other files there.)


--Toby


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]