a bit more polymorphism.

Author: Gregory Malecha

theories/Core/Any.v

@@ -2,12 +2,11 @@ Set Implicit Arguments.
 Set Strict Implicit.
 
 (** This class should be used when no requirements are needed **)
-Class Any (T : Type) : Type.
+Polymorphic Class Any (T : Type) : Type.
 
-Global Instance Any_a (T : Type) : Any T.
+Global Polymorphic Instance Any_a (T : Type) : Any T.
 
-
-Definition RESOLVE (T : Type) : Type := T.
+Polymorphic Definition RESOLVE (T : Type) : Type := T.
 
 Existing Class RESOLVE.
 

theories/Structures/Functor.v

@@ -3,28 +3,25 @@ Require Import ExtLib.Core.Any.
 Set Implicit Arguments.
 Set Strict Implicit.
 
-Section functor.
-  Variable F : Type -> Type.
+Polymorphic Class Functor (F : Type@{d} -> Type) : Type :=
+{ fmap : forall {A B : Type@{d}}, (A -> B) -> F A -> F B }.
 
-  Class Functor : Type :=
-  { fmap : forall A B, (A -> B) -> F A -> F B }.
+Polymorphic Definition ID {T : Type@{d}} (f : T -> T) : Prop :=
+  forall x, f x = x.
 
-  Definition ID {T : Type} (f : T -> T) : Prop :=
-    forall x, f x = x.
+Polymorphic Class PFunctor (F : Type@{d} -> Type) : Type :=
+{ FunP : Type@{d} -> Type
+; pfmap : forall {A B : Type@{d}} {P : FunP B}, (A -> B) -> F A -> F B
+}.
 
-  Class PFunctor : Type :=
-  { FunP : Type -> Type
-  ; pfmap : forall {A B} {P : FunP B}, (A -> B) -> F A -> F B
-  }.
+Existing Class FunP.
+Hint Extern 0 (@FunP _ _ _) => progress (simpl FunP) : typeclass_instances.
 
-  Existing Class FunP.
-  Hint Extern 0 (@FunP _ _ _) => progress (simpl FunP) : typeclass_instances.
-
-  Global Instance PFunctor_From_Functor (F : Functor) : PFunctor :=
-  { FunP := Any
-  ; pfmap := fun _ _ _ f x => fmap f x
-  }.
-End functor.
+Global Polymorphic Instance PFunctor_From_Functor
+       (F : Type@{d} -> Type) (FunF : Functor F) : PFunctor F :=
+{ FunP := Any
+; pfmap := fun _ _ _ f x => fmap f x
+}.
 
 Module FunctorNotation.
   Notation "f <$> x" := (@pfmap _ _ _ _ _ f x) (at level 51, right associativity).