∀ {Ω : Type w} [inst : SizeOf Ω] (obj : Set Ω) (hom : ↑obj → ↑obj → Set Ω) (id : (X : ↑obj) → ↑(hom X X))
  (comp : {X Y Z : ↑obj} → ↑(hom X Y) → ↑(hom Y Z) → ↑(hom X Z))
  (id_comp :
    autoParam (∀ {X Y : ↑obj} (f : ↑(hom X Y)), comp (id X) f = f) CategoryTheory.SmallCategoryOfSet.id_comp._autoParam)
  (comp_id :
    autoParam (∀ {X Y : ↑obj} (f : ↑(hom X Y)), comp f (id Y) = f) CategoryTheory.SmallCategoryOfSet.comp_id._autoParam)
  (assoc :
    autoParam
      (∀ {X Y Z T : ↑obj} (f : ↑(hom X Y)) (g : ↑(hom Y Z)) (h : ↑(hom Z T)), comp (comp f g) h = comp f (comp g h))
      CategoryTheory.SmallCategoryOfSet.assoc._autoParam),
  sizeOf { obj := obj, hom := hom, id := id, comp := comp, id_comp := id_comp, comp_id := comp_id, assoc := assoc } = 1