debug module

docs/TypeLevel.md

@@ -0,0 +1,67 @@
+Type Level
+==========
+
+```haskell
+data Coercion (a :: k) (b :: k) where
+  Coercion :: forall (k :: BOX) (a :: k) (b :: k).  Coercible a b => Coercion a b
+```
+
+```haskell
+coerceWith :: Coercion a b -> a -> b
+```
+
+#### Empty
+
+```haskell
+data Void
+```
+
+```haskell
+absurd :: Void -> a
+```
+
+```haskell
+vacuous :: Functor f => f Void -> f a
+```
+
+#### Proxy
+
+```haskell
+data Proxy (t :: k) = Proxy
+```
+
+#### Symbol
+
+* symbolVal
+* someSymbolVal
+
+#### Nat
+
+* natVal
+* someNatVal
+
+#### Type Equality
+
+```haskell
+(:~:) :: k -> k -> *
+```
+
+```haskell
+(==) :: k -> k -> Bool
+```
+
+```haskell
+sym :: a :~: b -> b :~: a
+```
+
+```haskell
+trans :: a :~: b -> b :~: c -> a :~: c
+```
+
+```haskell
+castWith :: a :~: b -> a -> b
+```
+
+```haskell
+gcastWith :: a :~: b -> ((a ~ b) => r) -> r
+```