`split` fails with `Error: Refiner was given an argument "@SpecializedFunctor (* Set NaturalTransformation.283 Top.112 Top.113 *) (CardinalityRepresentative O) (NatCategory (* NaturalTransformation.283 *) O) objC C" of type "Type (* max(Set, Nat about coq HOT 19 CLOSED

    Set Printing All.
    Goal (@eq
     (@SpecializedFunctor (CardinalityRepresentative (S O))
        (NatCategory (S O)) (CardinalityRepresentative (S O))
        (NatCategory (S O)))
     (@ComposeFunctors (CardinalityRepresentative (S O))
        (NatCategory (S O))
        (@SpecializedFunctor (CardinalityRepresentative O)
           (NatCategory O) objC C)
        (@FunctorCategory (CardinalityRepresentative O)
           (NatCategory O) objC C) (CardinalityRepresentative (S O))
        (NatCategory (S O)) ExponentialLaw0Functor
        ExponentialLaw0Functor_Inverse)
     (@IdentityFunctor (CardinalityRepresentative (S O)) (NatCategory (S O)))).
    generalize ExponentialLaw0Functor. (* Toplevel input, characters 0-33:
Error: Illegal application (Type Error):
The term "SpecializedFunctor" of type
 "forall (objC : Type) (_ : SpecializedCategory objC)
    (objD : Set) (_ : SpecializedCategory objD), Type"
cannot be applied to the terms
 "@SpecializedFunctor (CardinalityRepresentative O) (NatCategory O) objC C"
   : "Type"
 "@FunctorCategory (CardinalityRepresentative O) (NatCategory O) objC C"
   : "SpecializedCategory
        (@SpecializedFunctor (CardinalityRepresentative O)
           (NatCategory O) objC C)"
 "CardinalityRepresentative (S O)" : "Set"
 "NatCategory (S O)"
   : "SpecializedCategory (CardinalityRepresentative (S O))"
The 1st term has type "Type" which should be coercible to
"Type". *)

    Set Printing All.
    Goal True.
    assert (@eq
     (@SpecializedFunctor (CardinalityRepresentative (S O))
        (NatCategory (S O)) (CardinalityRepresentative (S O))
        (NatCategory (S O)))
     (@ComposeFunctors (CardinalityRepresentative (S O))
        (NatCategory (S O))
        (@SpecializedFunctor (CardinalityRepresentative O)
           (NatCategory O) objC C)
        (@FunctorCategory (CardinalityRepresentative O)
           (NatCategory O) objC C) (CardinalityRepresentative (S O))
        (NatCategory (S O)) ExponentialLaw0Functor
        ExponentialLaw0Functor_Inverse)
     (@IdentityFunctor (CardinalityRepresentative (S O)) (NatCategory (S O)))).
    generalize ExponentialLaw0Functor.

Delimit Scope object_scope with object.
Delimit Scope morphism_scope with morphism.
Delimit Scope category_scope with category.
Delimit Scope functor_scope with functor.

Set Implicit Arguments.

Generalizable All Variables.

Polymorphic Record SpecializedCategory (obj : Type) := Build_SpecializedCategory' {
  Object :> _ := obj;
  Morphism' : obj -> obj -> Type;

  Identity' : forall o, Morphism' o o;
  Compose' : forall s d d', Morphism' d d' -> Morphism' s d -> Morphism' s d';

  Associativity' : forall o1 o2 o3 o4 (m1 : Morphism' o1 o2) (m2 : Morphism' o2 o3) (m3 : Morphism' o3 o4),
    Compose' (Compose' m3 m2) m1 = Compose' m3 (Compose' m2 m1);
  (* ask for [eq_sym (Associativity' ...)], so that C^{op}^{op} is convertible with C *)
  Associativity'_sym : forall o1 o2 o3 o4 (m1 : Morphism' o1 o2) (m2 : Morphism' o2 o3) (m3 : Morphism' o3 o4),
    Compose' m3 (Compose' m2 m1) = Compose' (Compose' m3 m2) m1;
  LeftIdentity' : forall a b (f : Morphism' a b), Compose' (Identity' b) f = f;
  RightIdentity' : forall a b (f : Morphism' a b), Compose' f (Identity' a) = f
}.

Bind Scope category_scope with SpecializedCategory.
Bind Scope object_scope with Object.
Bind Scope morphism_scope with Morphism'.

Arguments Object {obj%type} C%category : rename.
Arguments Identity' {obj%type} C%category o%object : rename.
Arguments Compose' {obj%type} C%category s%object d%object d'%object m1%morphism m2%morphism : rename.

(* create a hint db for all category theory things *)
Create HintDb category discriminated.
(* create a hint db for morphisms in categories *)
Create HintDb morphism discriminated.

Section SpecializedCategoryInterface.
  Polymorphic Definition Build_SpecializedCategory (obj : Type)
    (Morphism' : obj -> obj -> Type)
    (Identity' : forall o : obj, Morphism' o o)
    (Compose' : forall s d d' : obj, Morphism' d d' -> Morphism' s d -> Morphism' s d')
    (Associativity' : forall (o1 o2 o3 o4 : obj) (m1 : Morphism' o1 o2) (m2 : Morphism' o2 o3) (m3 : Morphism' o3 o4),
      Compose' o1 o2 o4 (Compose' o2 o3 o4 m3 m2) m1 = Compose' o1 o3 o4 m3 (Compose' o1 o2 o3 m2 m1))
    (LeftIdentity' : forall (a b : obj) (f : Morphism' a b), Compose' a b b (Identity' b) f = f)
    (RightIdentity' : forall (a b : obj) (f : Morphism' a b), Compose' a a b f (Identity' a) = f) :
    @SpecializedCategory obj
    := @Build_SpecializedCategory' obj
    Morphism'
    Identity' Compose'
    Associativity'
    (fun _ _ _ _ _ _ _ => eq_sym (Associativity' _ _ _ _ _ _ _))
    LeftIdentity'
    RightIdentity'.

  Context `(C : @SpecializedCategory obj).

  Polymorphic Definition Morphism : forall s d : C, _ := Eval cbv beta delta [Morphism'] in C.(Morphism').

  Bind Scope morphism_scope with Morphism.

  Polymorphic Definition Identity : forall o : C, Morphism o o := Eval cbv beta delta [Identity'] in C.(Identity').
  Polymorphic Definition Compose : forall {s d d' : C} (m : Morphism d d') (m0 : Morphism s d), Morphism s d' := Eval cbv beta delta [Compose'] in C.(Compose').
  Polymorphic Definition Associativity : forall (o1 o2 o3 o4 : C) (m1 : Morphism o1 o2) (m2 : Morphism o2 o3) (m3 : Morphism o3 o4),
    Compose (Compose m3 m2) m1 = Compose m3 (Compose m2 m1)
    := C.(Associativity').
  Polymorphic Definition LeftIdentity : forall (a b : C) (f : Morphism a b),
    Compose (Identity b) f = f
    := C.(LeftIdentity').
  Polymorphic Definition RightIdentity : forall (a b : C) (f : Morphism a b),
    Compose f (Identity a) = f
    := C.(RightIdentity').
End SpecializedCategoryInterface.

Bind Scope morphism_scope with Morphism.

Arguments Object {obj} C : rename, simpl never.
Arguments Morphism {obj} C s d : rename, simpl nomatch.
Arguments Compose {obj} [C s d d'] m m0 : simpl nomatch.
Arguments Identity {obj} [C] o : simpl nomatch.

Global Opaque Associativity LeftIdentity RightIdentity.

Hint Resolve @LeftIdentity @RightIdentity @Associativity : category.
Hint Rewrite @LeftIdentity @RightIdentity : category.


Section SpecializedFunctor.
  Context `(C : @SpecializedCategory objC).
  Context `(D : @SpecializedCategory objD).

  Polymorphic Record SpecializedFunctor := {
    ObjectOf' : objC -> objD;
    MorphismOf' : forall s d, C.(Morphism') s d -> D.(Morphism') (ObjectOf' s) (ObjectOf' d);
    FCompositionOf' : forall s d d' (m1 : C.(Morphism') s d) (m2: C.(Morphism') d d'),
      MorphismOf' _ _ (C.(Compose') _ _ _ m2 m1) = D.(Compose') _ _ _ (MorphismOf' _ _ m2) (MorphismOf' _ _ m1);
    FIdentityOf' : forall o, MorphismOf' _ _ (C.(Identity') o) = D.(Identity') (ObjectOf' o)
  }.
End SpecializedFunctor.

Bind Scope functor_scope with SpecializedFunctor.

Create HintDb functor discriminated.

Section FunctorInterface.
  Context `(C : @SpecializedCategory objC).
  Context `(D : @SpecializedCategory objD).

  Variable F : SpecializedFunctor C D.

  Polymorphic Definition ObjectOf : C -> D := Eval cbv beta delta [ObjectOf'] in F.(ObjectOf'). (* [forall], so we can name it in [Arguments] *)
  Polymorphic Definition MorphismOf : forall {s d : C} (m : C.(Morphism) s d), D.(Morphism) (ObjectOf s) (ObjectOf d)
    := Eval cbv beta delta [MorphismOf'] in F.(MorphismOf').
  Polymorphic Definition FCompositionOf : forall (s d d' : C) (m1 : C.(Morphism) s d) (m2 : C.(Morphism) d d'),
    MorphismOf (Compose m2 m1) = Compose (MorphismOf m2) (MorphismOf m1)
    := F.(FCompositionOf').
  Polymorphic Definition FIdentityOf : forall (o : C), MorphismOf (Identity o) = Identity (ObjectOf o)
    := F.(FIdentityOf').
End FunctorInterface.

Global Coercion ObjectOf : SpecializedFunctor >-> Funclass.

Hint Resolve @FCompositionOf @FIdentityOf @FCompositionOf' @FIdentityOf' : functor.
Hint Rewrite @FIdentityOf @FIdentityOf' : functor.


Section FunctorComposition.
  Context `(B : @SpecializedCategory objB).
  Context `(C : @SpecializedCategory objC).
  Context `(D : @SpecializedCategory objD).
  Context `(E : @SpecializedCategory objE).

  Hint Rewrite @FCompositionOf : functor.

  Polymorphic Definition ComposeFunctors (G : SpecializedFunctor D E) (F : SpecializedFunctor C D) : SpecializedFunctor C E.
    refine {| ObjectOf' := (fun c => G (F c));
      MorphismOf' := (fun _ _ m => G.(MorphismOf) (F.(MorphismOf) m))
    |};
    abstract (
        intros; autorewrite with functor; reflexivity
      ).
  Defined.
End FunctorComposition.

Definition Cat0 : SpecializedCategory Empty_set.
  refine {|
      Morphism' := fun s d : Empty_set => s = d;
      Identity' := fun o : Empty_set => eq_refl;
      Compose' := fun (s d d' : Empty_set) (H : d = d') (H0 : s = d) =>
                    eq_trans H0 H |};
  admit.
Defined.

Set Printing All.
Set Printing Universes.

Lemma foo objC (C : @SpecializedCategory objC) (C0 : SpecializedCategory (SpecializedFunctor Cat0 C)) (x : SpecializedFunctor Cat0 Cat0) : forall (y : SpecializedFunctor C0 Cat0) z, (ComposeFunctors y z = x).
  intro.

Set Implicit Arguments.

Polymorphic Record Category (obj : Type) :=
  {
    Morphism : obj -> obj -> Type;
    Identity : forall o, Morphism o o
  }.

Polymorphic Record Functor objC (C :Category objC) objD (D : Category objD) :=
  {
    ObjectOf :> objC -> objD;
    MorphismOf : forall s d, C.(Morphism) s d -> D.(Morphism) (ObjectOf s) (ObjectOf d);
    FIdentityOf : forall o, MorphismOf _ _ (C.(Identity) o) = D.(Identity) (ObjectOf o)
  }.

Create HintDb functor discriminated.

Hint Rewrite @FIdentityOf : functor.

Polymorphic Definition ComposeFunctors objC C objD D objE E (G : @Functor objD D objE E) (F : @Functor objC C objD D) : Functor C E.
refine {| ObjectOf := (fun c => G (F c));
          MorphismOf := (fun _ _ m => G.(MorphismOf) _ _ (F.(MorphismOf) _ _ m))
       |};
  intros; autorewrite with functor; reflexivity.
Defined.

Definition Cat0 : Category Empty_set.
  refine {|
      Morphism := fun s d : Empty_set => s = d;
      Identity := fun o : Empty_set => eq_refl
    |};
  admit.
Defined.

Set Printing All.
Set Printing Universes.

Lemma foo objC (C : @Category objC) (C0 : Category (Functor Cat0 C)) (x : Functor Cat0 Cat0) : forall (y : Functor C0 Cat0) z, (ComposeFunctors y z = x).
  intro.

Set Implicit Arguments.

Polymorphic Record Category (obj : Type) :=
  {
    Morphism : obj -> obj -> Type;

    Identity : forall o, Morphism o o;
    Compose : forall s d d2, Morphism d d2 -> Morphism s d -> Morphism s d2;

    LeftIdentity : forall a b (f : Morphism a b), Compose (Identity b) f = f
  }.

Polymorphic Record Functor objC (C : Category objC) objD (D : Category objD) :=
  {
    ObjectOf : objC -> objD;
    MorphismOf : forall s d, C.(Morphism) s d -> D.(Morphism) (ObjectOf s) (ObjectOf d)
  }.

Create HintDb morphism discriminated.

Polymorphic Hint Resolve @LeftIdentity : morphism.

Polymorphic Definition ProductCategory objC (C : Category objC) objD (D : Category objD) : @Category (objC * objD)%type.
  refine {|
      Morphism := (fun s d => (C.(Morphism) (fst s) (fst d) * D.(Morphism) (snd s) (snd d))%type);
      Identity := (fun o => (Identity _ (fst o), Identity _ (snd o)));
      Compose := (fun (s d d2 : (objC * objD)%type) m2 m1 => (C.(Compose) _ _ _ (fst m2) (fst m1), D.(Compose) _ _ _ (snd m2) (snd m1)))
    |};
  intros; apply injective_projections; simpl; auto with morphism. (* Replacing [auto with morphism] with [apply @LeftIdentity] removes the error *)
Defined.

Polymorphic Definition Cat0 : Category Empty_set.
  refine {|
      Morphism := fun s d : Empty_set => s = d;
      Identity := fun o : Empty_set => eq_refl;
      Compose := fun s d d2 m0 m1 => eq_trans m1 m0
    |};
  admit.
Defined.

Set Printing All.
Set Printing Universes.
Polymorphic Definition ProductLaw0Functor (objC : Type) (C : Category objC) : Functor (ProductCategory C Cat0) Cat0.
refine (Build_Functor (ProductCategory C Cat0) Cat0 _ _). (* Toplevel input, characters 15-71:
Error: Refiner was given an argument
 "prod (* Top.2289 Top.2289 *) objC Empty_set" of type
"Type (* Top.2289 *)" instead of "Set". *)
econstructor. (* Toplevel input, characters 0-12:
Error: No applicable tactic.
*)

Polymorphic Lemma foo {obj : Type} : 1 = 1.
trivial.
Qed.

Polymorphic Hint Resolve foo. (* success *)
Polymorphic Hint Rewrite @foo. (* Success *)
Polymorphic Hint Resolve @foo. (* Error: @foo is a term and cannot be made a polymorphic hint, only global references can be polymorphic hints. *)
Polymorphic Hint Rewrite foo. (* Error: Cannot infer the implicit parameter obj of foo. *)