Impredicative Pearl: categories of functor

FunctorCategory.v

(***

    Impredicative Pearl.

    The file below demonstrates that it cannot be shown, in a
    predicative theory, that the functors between fixed categories
    together with natural transformations form a category. This, in
    turn, implies that one cannot prove that the categories with
    functors and natural transformations form a bicategory (unless we
    give up on the idea that the homs of bicategories are categories).

    Note that choosing sets to take their element type in [Set] and
    setting the [-impredicative-set] flag will solve this particular
    case. However, it's just pushing the issue a little further, as it
    will be impossible to show that the bifunctors form a bicategory
    (hence the bicategories a tricategory).

***)

Record Sets : Type := {
  El : Type
}.

Record Category : Type := {
  Obj : Type ;
  Hom : Obj -> Obj -> Sets
}.

Record Functor (C D:Category) : Type := {
  on_obj : Obj C -> Obj D ;
  on_hom : forall X Y, El (Hom C X Y) -> El (Hom D (on_obj X) (on_obj Y))
}.
Arguments on_obj {C D} _ _.
Arguments on_hom {C D} _ _ _ _.

Record NaturalTransformation {C D} (F G:Functor C D) : Type := {
  map : forall X, El (Hom D (on_obj F X) (on_obj G X))
}.


(*** The two definitions below are mutually inconsistent. Either of
     them can be typechecked, but not both in the same
     environment. ***)

Definition FunctorCat (C D:Category) : Category := {|
  Obj := Functor C D ;
  Hom := fun F G => {| El := NaturalTransformation F G |}
|}.

Definition CategoryOfSets : Category := {|
  Obj := Sets ;
  Hom := fun A B => {| El := El A -> El B |}
|}.

FunctorCategoryMonomorphic.v

(***

   By making the universe levels explicit, this files makes clear
   where the universe inconsistency comes from.

***)

(* Monomorphic universes *)
Definition Type1 := Type.
Definition Type2 := Type.
Definition Type3 := Type.

(* As [Obj] has type [Type1], [Category] type must be [Type2]. *)
Record Sets : Type2 := {
  El : Type1
}.

(* Categories must hence have the following signature, for there to be
   a category of sets. *)
Record Category : Type3 := {
  Obj : Type2 ;
  Hom : Obj -> Obj -> Sets
}.

(* Functors have the right type for objects *)
Record Functor (C D:Category) : Type2 := {
  on_obj : Obj C -> Obj D ;
  on_hom : forall X Y, El (Hom C X Y) -> El (Hom D (on_obj X) (on_obj Y))
}.
Arguments on_obj {C D} _ _.
Arguments on_hom {C D} _ _ _ _.

(* But NaturalTransformations cannot be a set. *)
Record NaturalTransformation {C D} (F G:Functor C D) : Type2 := {
  map : forall X, El (Hom D (on_obj F X) (on_obj G X))
}.