Remove temp file.
Refactor Category into obj + structure.
Add global category module.
Better interface for categories.
Move trunc from IsCategory to Category.
Require IsCategory to be in scope.
Add category structure for sets.
Move hom out of IsCategory.
Being univalent is a proposition.
Fix definition of free category.
Add free categories to index.
Add non-indexed M types.