Author: Olov Wilander
Title: An E-bicategory of E-categories
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.