An E-bicategory of E-categories, exemplifying a type-theoretic approach to bicategories
Olov Wilander · 2005
Abstract. A type-theoretic formalisation of bicategories is introduced, and it is shown that small E-categories, together with their functor categories, form such an E-bicategory. This is carried out using only basic recursive definitions, in the version of predicative type theory with a hierarchy of universes implemented by Agda. This relates to earlier work by Huet and Saïbi, who constructed a large category of small categories in Coq, but with the use of inductive families. The construction presented here may be considered more natural, particularly from the point of view of higher-dimensional category theory. This paper presents a formalisation of some parts of category theory, including a first step towards higher-dimensional category theory. The formalisation is carried out in Agda, a type-theoretic framework with a hierarchy of universes implemented at Chalmers University of Technology, Gothenburg. Agda and Alfa (the version with a graphical interface) are intended to replace the earlier ALF system (see [2, 3, 11]). Further, not all features of the framework were used; restricting myself