diff --git a/bower.json b/bower.json
index 254c21b..0341e99 100644
--- a/bower.json
+++ b/bower.json
@@ -15,5 +15,8 @@
     "test",
     "bower.json",
     "package.json"
-  ]
+  ],
+  "dependencies": {
+    "purescript-prelude": "^3.0.0"
+  }
 }
diff --git a/package.json b/package.json
index f9e9db6..6f630dc 100644
--- a/package.json
+++ b/package.json
@@ -5,8 +5,8 @@
     "build": "pulp build -- --censor-lib --strict"
   },
   "devDependencies": {
-    "pulp": "^10.0.4",
-    "purescript-psa": "^0.5.0-rc.1",
+    "pulp": "^11.0.0",
+    "purescript-psa": "^0.5.1",
     "rimraf": "^2.6.1"
   }
 }
diff --git a/src/Type/Proxy.purs b/src/Type/Proxy.purs
index 9c6079b..89cc2a7 100644
--- a/src/Type/Proxy.purs
+++ b/src/Type/Proxy.purs
@@ -48,11 +48,140 @@
 -- | ```
 module Type.Proxy where
 
+import Prelude
+
 -- | Value proxy for kind `Type` types.
 data Proxy a = Proxy
 
+derive instance eqProxy :: Eq (Proxy a)
+
+derive instance functorProxy :: Functor Proxy
+
+derive instance ordProxy :: Ord (Proxy a)
+
+instance applicativeProxy :: Applicative Proxy where
+  pure _ = Proxy
+
+instance applyProxy :: Apply Proxy where
+  apply _ _ = Proxy
+
+instance bindProxy :: Bind Proxy where
+  bind _ _ = Proxy
+
+instance booleanAlgebraProxy :: BooleanAlgebra (Proxy a)
+
+instance boundedProxy :: Bounded (Proxy a) where
+  bottom = Proxy
+  top = Proxy
+
+instance commutativeRingProxy :: CommutativeRing (Proxy a)
+
+instance discardProxy :: Discard (Proxy a) where
+  discard = bind
+
+instance heytingAlgebraProxy :: HeytingAlgebra (Proxy a) where
+  conj _ _ = Proxy
+  disj _ _ = Proxy
+  implies _ _ = Proxy
+  ff = Proxy
+  not _ = Proxy
+  tt = Proxy
+
+instance monadProxy :: Monad Proxy
+
+instance ringProxy :: Ring (Proxy a) where
+  sub _ _ = Proxy
+
+instance semigroupProxy :: Semigroup (Proxy a) where
+  append _ _ = Proxy
+
+instance semiringProxy :: Semiring (Proxy a) where
+  add _ _ = Proxy
+  mul _ _ = Proxy
+  one = Proxy
+  zero = Proxy
+
+instance showProxy :: Show (Proxy a) where
+  show _ = "Proxy"
+
 -- | Value proxy for kind `Type -> Type` types.
 data Proxy2 (a :: Type -> Type) = Proxy2
 
+derive instance eqProxy2 :: Eq (Proxy2 a)
+
+derive instance ordProxy2 :: Ord (Proxy2 a)
+
+instance booleanAlgebraProxy2 :: BooleanAlgebra (Proxy2 a)
+
+instance boundedProxy2 :: Bounded (Proxy2 a) where
+  bottom = Proxy2
+  top = Proxy2
+
+instance commutativeRingProxy2 :: CommutativeRing (Proxy2 a)
+
+instance discardProxy2 :: Discard (Proxy2 a) where
+  discard = bind
+
+instance heytingAlgebraProxy2 :: HeytingAlgebra (Proxy2 a) where
+  conj _ _ = Proxy2
+  disj _ _ = Proxy2
+  implies _ _ = Proxy2
+  ff = Proxy2
+  not _ = Proxy2
+  tt = Proxy2
+
+instance ringProxy2 :: Ring (Proxy2 a) where
+  sub _ _ = Proxy2
+
+instance semigroupProxy2 :: Semigroup (Proxy2 a) where
+  append _ _ = Proxy2
+
+instance semiringProxy2 :: Semiring (Proxy2 a) where
+  add _ _ = Proxy2
+  mul _ _ = Proxy2
+  one = Proxy2
+  zero = Proxy2
+
+instance showProxy2 :: Show (Proxy2 a) where
+  show _ = "Proxy2"
+
 -- | Value proxy for kind `Type -> Type -> Type` types.
 data Proxy3 (a :: Type -> Type -> Type) = Proxy3
+
+derive instance eqProxy3 :: Eq (Proxy3 a)
+
+derive instance ordProxy3 :: Ord (Proxy3 a)
+
+instance booleanAlgebraProxy3 :: BooleanAlgebra (Proxy3 a)
+
+instance boundedProxy3 :: Bounded (Proxy3 a) where
+  bottom = Proxy3
+  top = Proxy3
+
+instance commutativeRingProxy3 :: CommutativeRing (Proxy3 a)
+
+instance discardProxy3 :: Discard (Proxy3 a) where
+  discard = bind
+
+instance heytingAlgebraProxy3 :: HeytingAlgebra (Proxy3 a) where
+  conj _ _ = Proxy3
+  disj _ _ = Proxy3
+  implies _ _ = Proxy3
+  ff = Proxy3
+  not _ = Proxy3
+  tt = Proxy3
+
+instance ringProxy3 :: Ring (Proxy3 a) where
+  sub _ _ = Proxy3
+
+instance semigroupProxy3 :: Semigroup (Proxy3 a) where
+  append _ _ = Proxy3
+
+instance semiringProxy3 :: Semiring (Proxy3 a) where
+  add _ _ = Proxy3
+  mul _ _ = Proxy3
+  one = Proxy3
+  zero = Proxy3
+
+instance showProxy3 :: Show (Proxy3 a) where
+  show _ = "Proxy3"