diff --git a/requirements.cabal b/requirements.cabal
--- a/requirements.cabal
+++ b/requirements.cabal
@@ -2,7 +2,7 @@
 -- documentation, see http://haskell.org/cabal/users-guide/
 
 name:                requirements
-version:             0.7.0.1
+version:             0.7.0.2
 synopsis:            Abstraction to manage user defined Type Errors
 description:         requirements is a framework to build user-defined type errors.
                      Users condense the arguments of functions that can raise a
@@ -21,8 +21,21 @@
 
 library
   exposed-modules:     Data.Type.Require
-  other-modules:       Figures, Vector
-  -- other-extensions:
+  --other-modules:       Figures, Vector
+  other-extensions:  UndecidableInstances  
+                  ,  MultiParamTypeClasses 
+                  ,  FlexibleContexts      
+                  ,  ConstraintKinds       
+                  ,  FlexibleInstances     
+                  ,  TypeOperators         
+                  ,  TypeFamilies          
+                  ,  DataKinds             
+                  ,  PolyKinds             
+                  ,  KindSignatures        
+                  ,  GADTs                 
+                  ,  TypeApplications      
+                  ,  ScopedTypeVariables   
+
   build-depends:       base >=4.12 && <4.18
   hs-source-dirs:      src
   default-language:    Haskell2010
diff --git a/src/Data/Type/Require.hs b/src/Data/Type/Require.hs
--- a/src/Data/Type/Require.hs
+++ b/src/Data/Type/Require.hs
@@ -163,8 +163,7 @@
 
 type family IsEmptyCtx (ms :: [ErrorMessage]) :: Bool where
   IsEmptyCtx '[] = True
-  IsEmptyCtx (m ': ms) = False -- IsEmptyMsg m && IsEmptyCtx ms
-  IsEmptyCtx _ = True
+  IsEmptyCtx (m ': ms) = False
 
 type family IsEmptyMsg (m :: ErrorMessage) :: Bool where
   IsEmptyMsg (Text "") = True
@@ -172,9 +171,9 @@
   IsEmptyMsg other = False
 
 -- -- | Formatting of context printing.
-type family ShowCTX (ctx :: k)  :: ErrorMessage where
-  ShowCTX ('[] :: [ErrorMessage]) = Text ""
-  ShowCTX ((m :: ErrorMessage) ': (ms :: [ErrorMessage])) = m :$$: ShowCTX ms
+type family ShowCTX (ctx :: [ErrorMessage])  :: ErrorMessage where
+  ShowCTX ((m :: ErrorMessage) ': (ms :: [ErrorMessage]))
+    = m :$$: ShowCTX ms
   ShowCTX (m :: [ErrorMessage]) = Text ""
 
   
@@ -216,15 +215,15 @@
 
 
 
-data Exp (a :: k) where Exp :: a -> Exp a
+data Exp (a :: Type) where Exp :: a -> Exp a
 type family Eval (exp :: Type) :: k
 
-data CondEq (a ::k) (b :: k) where
+data CondEq (a ::Type) (b :: Type) where
   CondEq :: a -> b -> CondEq a b
-data RequireEqResF (a ::k) (b :: k) where
+data RequireEqResF (a :: Type) (b :: Type) where
   RequireEqResF :: a -> b -> RequireEqResF a b
 
-data EqMsg (a::k)(b::k) where EqMsg :: a -> b -> EqMsg a b
+data EqMsg (a::Type)(b::Type) where EqMsg :: a -> b -> EqMsg a b
 type instance Eval (EqMsg t1 t2) =
     (Text "\nEQMSG" :<>: ShowTE t1
                        :<>: Text "\n/= " :<>: ShowTE t2)
@@ -234,12 +233,11 @@
   (ctx :: [ErrorMessage]) :: Constraint
 type instance RequireEqWithMsg t t' f ctx =
   (AssertEq' t t' f ctx, t ~ t')
-   --If (t `Equal` t') (()::Constraint) (Require (OpError (Eval (f t t'))) ctx))
-type family AssertEq' (t1 :: k)(t2 :: k) (f :: k -> k -> Type) ctx :: Constraint
+type family AssertEq' (t1 :: k)(t2 :: k)
+                      (f :: k -> k -> Type) ctx :: Constraint
   where
   AssertEq' a a f ctx = ()
-  AssertEq' a b f ctx = Require (OpError (Eval (f a b))
-                                ) ctx
+  AssertEq' a b f ctx = Require (OpError (Eval (f a b))) ctx
 
 -- Exported operators.
 
@@ -261,7 +259,7 @@
     (Require (OpError (Text "\n   " :<>: ShowTE t1
                        :<>: Text "\n/= " :<>: ShowTE t2)) ctx)
 
-type family Equal (a :: k) (b :: k') :: Bool where
+type family Equal (a :: k) (b :: k) :: Bool where
   Equal a a = True
   Equal a b = False
 
@@ -272,7 +270,6 @@
 
 appendCtx :: Proxy ctx -> Proxy ctx' -> Proxy (ctx :++ ctx')
 appendCtx Proxy Proxy = Proxy
-
 
 type family (:++) xs ys where
   '[] :++ ys = ys
diff --git a/src/Figures.lhs b/src/Figures.lhs
deleted file mode 100644
--- a/src/Figures.lhs
+++ /dev/null
@@ -1,151 +0,0 @@
-> {-# LANGUAGE FlexibleContexts #-}
-> {-# LANGUAGE DataKinds #-}
-> {-# LANGUAGE TypeOperators #-}
-> {-# LANGUAGE FlexibleInstances #-}
-> {-# LANGUAGE GADTs #-}
-> {-# LANGUAGE UndecidableInstances #-}
-> {-# LANGUAGE TypeFamilies #-}
-> {-# LANGUAGE MultiParamTypeClasses #-}
-> {-# LANGUAGE TypeApplications #-}
-> {-# LANGUAGE ScopedTypeVariables #-}
-> {-# LANGUAGE AllowAmbiguousTypes #-}
-> {-# OPTIONS -Wno-missing-methods #-}
-
-> module Figures where
-
-> import Data.Type.Require
-> import GHC.TypeLits
-> import Data.Type.Bool
-> import Data.Type.Equality
-> import Data.Proxy
-
-> data Color = RGB Nat Nat Nat
-
-> type instance Equ (RGB r g b) (RGB r' g' b')
->   = r == r' && g == g' && b == b'
-
-> data Dim = R2 | R3
-> type instance ShowTE R2 = Text "R2"
-> type instance ShowTE R3 = Text "R3"
-
-> data family Figure (d :: Dim) (c :: Color)
-
-
-> data instance Figure R2 c
->   = Circle Double Double Double -- center, radius? not important
-
-> data instance Figure R3 c
->   = Sphere Double Double Double Double
-
-
-> combine :: Figure d c -> Figure d c -> Figure d c
-> combine f g = undefined
-
-combine (Circle 1 1 1) (Sphere 1 1 1 1) ->
-
-• Couldn't match type ‘'R3’ with ‘'R2’
-  Expected type: Figure 'R2 c
-  Actual type: Figure 'R3 c
-
-
-> data OpEqDim  (d :: Dim)  (d' :: Dim)
-> data OpEqDim' (b :: Bool) (d :: Dim)   (d' :: Dim)
-> data OpEqCol  (c :: Color) (c' :: Color)
-> data OpEqCol' (b :: Bool) (c :: Color) (c' :: Color)
-
-> data OpCombine d d' c c' where
->   OpCombine :: Figure d c -> Figure d' c' -> OpCombine d d' c c'
-
-> instance
->   ( Require (OpEqDim d d') ctx
->   , Require (OpEqCol c c') ctx
->   )
->   =>
->   Require (OpCombine d d' c c') ctx where
->   type ReqR (OpCombine d d' c c') =
->     Figure d c
->   req ctx (OpCombine f g) =
->     undefined
-
-> instance
->   (Require (OpEqDim' (d == d') d d')) ctx
->   =>
->   Require (OpEqDim d d') ctx where
->   type ReqR (OpEqDim d d') = ReqR (OpEqDim' (d == d') d d')
-
-> instance Require (OpEqDim' 'True  d d') ctx where {}
-
-> instance
->   Require (OpError
->   (Text "Dimensional error:" :$$: Text "cannot combine figure of dimension "
->   :<>: ShowTE d :<>: Text " and dimension " :<>: ShowTE d')) ctx
->   => Require (OpEqDim' 'False d d') ctx
-
-
-> instance
->   (Require (OpEqCol' (Equ c c') c c')) ctx
->   =>
->   Require (OpEqCol c c') ctx where
->   type ReqR (OpEqCol c c') = ReqR (OpEqCol' (Equ c c') c c')
-
-> instance Require (OpEqCol' 'True  c c') ctx where {}
-
-
-an sloppy error:
-
-> instance
->   Require (OpError
->   (Text "Error, combined images must be of the same color")) ctx
->   => Require (OpEqCol' 'False c c') ctx
-
-
-> combine' f f' = req (Proxy @( '[ Text "combining"] )) (OpCombine f f')
-
-combine' (Circle 1 1 1) (Sphere 1 1 1 1) ->
-
-• Error: Dimensional error:
-         cannot combine figure of dimension R2 and dimension R3
-  trace: combining..
-
-
-
-combine' (Circle 1 1 1 :: Figure R2 (RGB 1 1 1))
-         (Circle 1 1 1 :: Figure R2 (RGB 1 1 2)) ->
-
-• Error: Error, combined images must be of the same color
-  trace: combining..
-
-> f1 = (Circle 2 2 2 :: Figure R2 (RGB 1 1 1))
-> f2 = (Sphere 2 2 2 2:: Figure R3 (RGB 1 1 1))
-
-> f = CFigure $ \Proxy  -> f1
-> f' = CFigure $ \Proxy -> f2
-
-> f'' = traceFig
->    (\(_ :: Proxy (Text "tracefig!!!!!" : ctx)) -> Proxy :: Proxy ctx ) $ f'
-
-> tr = traceFig
->    (\(_ :: Proxy (ctx)) -> Proxy :: Proxy (Text "tracefig!!!!!" : ctx) )
-
-> data CFigure d c (ctx :: [ErrorMessage])
->  = CFigure {mkCFig :: Proxy ctx -> Figure d c}
-
-
-> combine''
->   :: (Require (OpEqDim' (d == d') d d') (Text "lalo" :ctx),
->       Require (OpEqCol' (Equ c c') c c') (Text "lalo" : ctx)) =>
->      CFigure d c ctx -> CFigure d' c' ctx -> CFigure d c ctx
-> combine'' (CFigure f1) (CFigure f2)
->   = CFigure $ \(a :: Proxy ctx) ->
->           req (Proxy :: Proxy (Text "lalo" : ctx))
->               (OpCombine (f1 a) (f2 a))
-
-
-> traceFig :: (Proxy ctx' -> Proxy ctx) -> CFigure d c ctx -> CFigure d c ctx'
-> traceFig fctx (CFigure f) = CFigure $ f . fctx
-
-
-
-Error:
-
- > g = combine'' (tr $ tr f) (tr $ tr f'') -- (tr $ tr $ tr $ combine'' f f) f''
diff --git a/src/Vector.lhs b/src/Vector.lhs
deleted file mode 100644
--- a/src/Vector.lhs
+++ /dev/null
@@ -1,150 +0,0 @@
-
-> {-# LANGUAGE UndecidableInstances  #-}
-> {-# LANGUAGE MultiParamTypeClasses #-}
-> {-# LANGUAGE FlexibleContexts      #-}
-> {-# LANGUAGE ConstraintKinds       #-}
-> {-# LANGUAGE FlexibleInstances     #-}
-> {-# LANGUAGE TypeOperators         #-}
-> {-# LANGUAGE TypeFamilies          #-}
-> {-# LANGUAGE DataKinds             #-}
-> {-# LANGUAGE PolyKinds             #-}
-> {-# LANGUAGE KindSignatures        #-}
-> {-# LANGUAGE GADTs                 #-}
-> {-# LANGUAGE TypeApplications      #-}
-> {-# LANGUAGE ScopedTypeVariables   #-}
-
-> module Vector where
-
-> import Data.Kind
-> import Data.Proxy
-> import GHC.TypeLits (Symbol, ErrorMessage(..))
-
-> import Data.Type.Bool
-> import Data.Type.Equality
-> import Data.Type.Require
-
-Firstly, we define size-indexed vectors, the stapple example of a
-dependent Haskell type.
-
-> data Nat = Z | S Nat
-> type family Lt (m :: Nat) (n :: Nat) :: Bool where
->   Lt Z     (S n) = True
->   Lt _      Z    = False
->   Lt (S m) (S n) = Lt m n
-
-> infixr 3 :< 
-
-> data Vec (n :: Nat) (a :: Type) :: Type where
->   VNil :: Vec Z a
->   (:<) :: a -> Vec n a -> Vec (S n) a
-
-And singletons for natutals:
-
-> data SNat (n :: Nat) where
->   SZ :: SNat Z
->   SS :: SNat n -> SNat (S n)
-
-With this we can implement a get function, that takes the element in a
-given index of the vector. There are many ways to do that in a safe
-way:
-
- * use a value of type 'Fin n' as the input for the index.
-
-< get :: Fin n -> Vec n a -> a
-
- * use 'SNat' but also define a GADT 'Lt :: Nat -> Nat -> Type' that
-   encodes a proof that the index is smaller than the vector size.
-
-< get :: SNat n -> Lt n m -> Vec m a -> a
-
- * use a 'SNat', with no proof argument, and let index overflows to be
-   ill-typed. Since this is Haskell all type information is static,
-   meaning that we will know at compile time if the index is out of
-   bound.
-
-< get :: SNat n -> Vec m a -> a
-
-In the latter approach is where |Require| fits. The require
-infrastructure allows us to have nice type errors when an out of bound
-lookup occurs, instead of something like 'no instance for ..'
-
-We introduce an /operation/ for the vector, the get operation. This
-is a product datatype having all information we need: an index and
-vector:
-
-> data OpGet (n :: Nat) (k :: Nat) (a :: Type) :: Type  where
->    OpGet :: SNat n -> Vec k a -> OpGet n k a
-
-This operation /requires/ some properties about its arguments, in this
-case, that the index given is less than vector's length. A well-typed
-lookup will satisfy the constraint 'Require (OpGet n k a)'
-
-We will decide according on the result of '(Lt n k)' . Since
-typeclass resolution does not backtrack we need to have all
-informartion on the head of the instance. This is a well known
-trick. We build a wrapper where the first Boolean argument will
-contain the result of the comparisson:
-
-> data OpGet' (cmp :: Bool) (n :: Nat) (k :: Nat) (a :: Type) :: Type where
->    OpGet' :: Proxy cmp -> SNat n -> Vec k a -> OpGet' cmp n k a
-
-Then, the wrapper instance:
-
-> instance
->   Require (OpGet' (Lt n k) n k a) ctx
->   =>
->   Require (OpGet n k a) ctx where
->   type ReqR (OpGet n k a) =
->     ReqR (OpGet' (Lt n k) n k a)
->   req proxy (OpGet (n :: SNat n) (v :: Vec k a)) =
->     req proxy (OpGet' (Proxy @ (Lt n k)) n v)
-
-Now we program the good cases:
-
-> instance
->   Require (OpGet' 'True Z k a) ctx where
->   type ReqR (OpGet' 'True Z k a) = a
->   req _ (OpGet' _ SZ (a :< _)) = a
-
-> instance
->   Require (OpGet n k a) ctx
->   => 
->   Require (OpGet' 'True (S n) (S k) a) ctx where
->   type ReqR (OpGet' 'True (S n) (S k) a) =
->     ReqR (OpGet n k a)
->   req ctx (OpGet' _ (SS n) (_ :< as)) = req ctx (OpGet n as)
- 
-
-Finally, when (Lt n k ~ 'False) we have an ill-typed get
-operation.  We build a |Require| instance for the |OpError|
-operation. When defining it, we have in scope 'n', 'k', and 'a',
-everything needed to write a good type error using 'GHC.TypeLits'
-infraestructure.
-
-
-> instance
->   Require (OpError
->     (Text "Type error!, index out of bound:" :$$:
->     Text "Trying to lookup the " :<>: ShowTE n :<>: Text "th index" :$$:
->     Text "in a vector of size " :<>: ShowTE k
->     )
->           ) ctx
->   =>
->   Require (OpGet' False n k a) ctx where
->   type ReqR (OpGet' False n k a) = OpError (Text "lala")
->   req = error "unreachable"
-
-> get n v = req (Proxy @ '[Text "getting"]) (OpGet n v)
-
-
-> vecEx = 'a' :< 'b' :< 'c' :< 'd' :< VNil
-> a = get SZ vecEx
-> c = get (SS $ SS SZ) vecEx
-
-< e = get (SS $ SS $ SS $ SS SZ) vecEx
-
---> 
-  • Error: Type error!, index out of bound:
-           Trying to lookup the ShowTE ('S ('S ('S ('S 'Z))))th index
-           in a vector of size ShowTE ('S ('S ('S ('S 'Z))))
-    trace: getting