Category of categories

[barrettj12]

I thought I'd like to add the category of (small) categories to Categories/Instances. Most of the work was already done elsewhere, but I ran into a roadblock trying to prove

C D : Category ℓ ℓ'
    ⊢ isSet (Functor C D)

I don't think I know enough (cubical) type theory to know whether this is even true, let alone write a proof in Agda. Maybe someone with more expertise can help.

[felixwellen]

I don't expect it to be true, since there is no requirement on D to have a 0-type of objects. That's not a recipe for a counterexample, since the type of functors is some Sigma-type based on that. If you want to treat Categories as 0-type based structures, you could ask D to be a 0-type for your construction. Then you should get a 0-type of functors. However, that would mean, that you forget natural transformations and consider naturally isomorphic functors as something completely different.

But in some way you have to do somehting forgetful, if you want to have 'the' 1-category of small 1-categories (since, naturally, I would say it is a 2-category).

Another way would be to ask for all the small categories to be univalent, then (not completely sure here...) you would get a 1-type of functors. And you could truncate that to get a 0-type (with all operations and laws you need).

[barrettj12]

Hmmm. I think I'll just make it a Precategory then. If anyone ends up needing a category of categories later, they can think more about what is required for the homs to be sets.

[mortberg]

Name change suggestion