open import category-theory.categories
open import Agda.Primitive

variable
  l1 l2 : Level

thm : (C : Category l1 l2) → {!   !}