12 Sep
2010
12 Sep
'10
6:27 a.m.
Hi Toby and David, Toby Bartels <toby+categories@ugcs.caltech.edu> wrote:
The non-evil algebraic definitions of higher categories are based on dependent type theory,
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? [For admin and other information see: http://www.mta.ca/~cat-dist/ ]