zbMATH — the first resource for mathematics

On formalization of bicategory theory. (English) Zbl 0897.18003
Gunter, Elsa L. (ed.) et al., Theorem proving in higher order logics. 10th international conference, TPHOLs ’97. Murray Hill, NJ, USA. August 19–22, 1997. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1275, 199-214 (1997).
A generalization of the Yoneda lemma to the case of bicategories is formalized directly in the extended calculus of constructions. An implementation using the proof-checker LEGO is reported, and the problems related to this implementation are discussed.
For the entire collection see [Zbl 0870.00024].
MSC:
 18D05 Double categories, $$2$$-categories, bicategories and generalizations (MSC2010) 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) 03B35 Mechanization of proofs and logical operations