diff --git a/poly-rec.cabal b/poly-rec.cabal
--- a/poly-rec.cabal
+++ b/poly-rec.cabal
@@ -1,8 +1,8 @@
--- Initial polykheXrec.cabal generated by cabal init.  For further
+-- Initial polyrec.cabal generated by cabal init.  For further
 -- documentation, see http://haskell.org/cabal/users-guide/
 
 name:                poly-rec
-version:             0.7.0.2
+version:             0.7.0.4
 synopsis:            Polykinded extensible records
 description:         Extensible records/row polymorphism for Haskell. Fields are polykinded,
                      to statically check rich structures. This library was initially conceived
@@ -11,20 +11,21 @@
 license-file:        LICENSE
 author:              Juan García-Garland
 maintainer:          jpgarcia@fing.edu.uy
-copyright:           2020-2022, Juan García-Garland, Marcos Viera, Alberto Pardo
-category:            Data
+copyright:           2020-2023, Juan García-Garland, Marcos Viera, Alberto Pardo
+category:            Data, Dependent Types
 build-type:          Simple
 extra-source-files:  CHANGELOG.md
 cabal-version:       >=1.10
 
 library
   exposed-modules: Data.GenRec,
-                   Data.GenRec.Label,
-                   Data.GenRec.RecInstances.Record
-                   
+                   Data.Label,
+                   Data.GenRec.RecInstances.Record,
+                   Data.HList,
+                   Data.GenRec.Unordered
   -- other-modules:
   -- other-extensions:
-  build-depends:       requirements >= 0.7.0.2 && < 0.7.1,
-                       base >=4.11 && <4.18
+  build-depends:       requirements >= 0.7.0.3 && < 0.7.1,
+                       base >= 4.20 && < 4.21
   hs-source-dirs:      src
   default-language:    Haskell2010
diff --git a/src/Data/GenRec.hs b/src/Data/GenRec.hs
--- a/src/Data/GenRec.hs
+++ b/src/Data/GenRec.hs
@@ -73,7 +73,8 @@
              InstanceSigs,
              AllowAmbiguousTypes,
              TypeApplications,
-             PatternSynonyms
+             PatternSynonyms,
+             TypeFamilyDependencies
 #-}
 
 module Data.GenRec
@@ -86,7 +87,10 @@
     (.=.),
     (#),
     (.*.),
-
+    (.//),
+    (↑),
+    (⋉),
+    (.:><),
     OrdType,
     Cmp,
     ShowRec,
@@ -98,17 +102,26 @@
     OpExtend(OpExtend),
     -- extend, TODO
     OpUpdate(OpUpdate),
+    OpLJoin(OpLJoin),
+    OpLeftProj(OpLeftProj),
     update,
     emptyGenRec,
-    module Data.GenRec.Label
+    module Data.Label,
+
+    prCmp, CmpVal,
+
+    LabelsOf
   ) where
 
 import Data.Kind
 import Data.Proxy
-import Data.GenRec.Label
+import Data.Label
 import Data.Type.Require
 import Data.Type.Bool
+import Data.Type.Equality ((:~:)(Refl))
+import Unsafe.Coerce
 
+
 import Prelude hiding (lookup)
 
 import GHC.TypeLits
@@ -264,7 +277,7 @@
   req ctx (OpLookup' Proxy l (ConsRec _ r)) = ()
 
 -- | Pretty lookup
-(#) :: forall c l r ctx v. RequireR (OpLookupCall c l r) ctx v =>
+(#) :: forall c l r ctx v. RequireR (OpLookupCall c l r) v ctx =>
   Rec c r -> Label l -> v
 r # l = req (Proxy @ctx) (OpLookupCall l r)
 
@@ -452,3 +465,259 @@
     ReqR (OpLookup c l r)
   req ctx (OpLookupCall l r) =
    req (Proxy @(ShowType r ': ctx)) (OpLookup l r)
+
+
+
+-- | HasLabel
+
+type family Or (b :: Bool)(b' :: Bool) :: Bool where
+  Or False False = False
+  Or _ _ = True 
+
+type family HasLabel (l :: k) (r :: [(k,k')]) :: Bool where
+  HasLabel l '[] = False
+  HasLabel l ( '(l', v) ': r) = Or (l == l') (HasLabel l r) 
+
+-- | Left projection
+
+data OpLeftProj
+  (c  :: Type)
+  (ls :: [k])
+  (r  :: [(k, k')]) :: Type where
+  OpLeftProj :: Label ls -> Rec c r -> OpLeftProj c ls r
+
+data OpLeftProj'
+  (b :: Bool) -- label in front
+  (c :: Type)
+  (ls:: [k])
+  (r :: [(k, k')]) :: Type where
+  OpLeftProj' :: Proxy b -> Label ls -> Rec c r -> OpLeftProj' b c ls r
+
+instance
+  (Require (OpLeftProj c (l ': ls :: [k]) ('[] :: [(k,k')])) ctx
+  ) where
+  type ReqR (OpLeftProj c (l ': ls :: [k]) ('[] :: [(k,k')]))
+    = Rec c ('[] :: [(k,k')])
+  req ctx _ = EmptyRec
+
+instance
+  (Require (OpLeftProj c ('[] :: [k]) (r :: [(k,k')])) ctx
+  ) where
+  type ReqR (OpLeftProj c ('[] :: [k]) (r :: [(k,k')]))
+    = Rec c ('[] :: [(k,k')])
+  req ctx _ = EmptyRec
+
+type family InFront (l :: k) (ls::[k]) :: Bool where
+  InFront l (l ': r) = True
+  InFront _ _ = False
+
+instance
+  ( Require (OpLeftProj' (InFront l' (l ': ls)) c
+             ((l ': ls) :: [k]) ( '(l',v) ': r)) ctx
+  , ReqR (OpLeftProj c (l ': ls) ('(l', v) : r))
+  ~ ReqR (OpLeftProj' (InFront l' (l ': ls)) c (l ': ls) ('(l', v) : r))
+  )
+  => Require (OpLeftProj c ((l ': ls) :: [k]) ( '(l',v) ': r)) ctx where
+  type ReqR (OpLeftProj c ((l ': ls) :: [k]) ( '(l',v) ': r))
+    = ReqR (OpLeftProj' (InFront l' (l ': ls)) c
+            ((l ': ls) :: [k]) ('(l',v) ': r))
+  req ctx (OpLeftProj pls r) =
+     let pr = Proxy @(InFront l' (l ': ls))
+     in req ctx (OpLeftProj' pr pls r)
+
+
+type family LabelsOf (r :: [(k, k')]) :: [k] where
+  LabelsOf '[] = '[]
+  LabelsOf ( '(l, v) ': r) = l ': LabelsOf r
+
+instance
+  ( ReqR (OpLeftProj c (ls :: [k]) (r :: [(k,k')]))
+  ~ Rec c (UnWrap @k @k' (ReqR (OpLeftProj c ls r)))
+  , Require (OpLeftProj c ls r) ctx)
+  => Require (OpLeftProj' 'True c (l ': ls) ( '(l,v) ': r)) ctx where
+  type ReqR (OpLeftProj' 'True c (l ': ls) ( '(l,v) ': r))
+    = Rec c ('(l,v) ': UnWrap (ReqR (OpLeftProj c ls r)))
+  req ctx (OpLeftProj' _ pls (ConsRec lv r))
+   = ConsRec lv $ req ctx (OpLeftProj (Label @ls) r)
+
+instance
+  (Require (OpLeftProj c (l ': ls) r) ctx)
+  => Require (OpLeftProj' 'False c (l ': ls) ( '(l',v) ': r)) ctx where
+  type ReqR (OpLeftProj' 'False c (l ': ls) ( '(l',v) ': r))
+   = ReqR (OpLeftProj c (l ': ls) r)
+  req ctx (OpLeftProj' _ ls (ConsRec _ r)) = req ctx (OpLeftProj ls r)
+
+instance
+  Require (OpLeftProj' 'False c (l ': ls) ('[] :: [(k,k')]) ) ctx where
+  type ReqR (OpLeftProj' 'False c (l ': ls) ('[] :: [(k,k')]))
+   = Rec c ('[] :: [(k, k')])
+  req ctx _ = EmptyRec
+
+infixr 5 .//
+ls .// r = req emptyCtx (OpLeftProj ls r)
+
+
+-- | extend or update
+
+data OpExtUpd (c :: Type)
+              (l  :: k)
+              (v  :: k')
+              (r  :: [(k, k')]) :: Type where
+  OpExtUpd :: Label l -> WrapField c v -> Rec c r
+           -> OpExtUpd c l v r
+
+data OpExtUpd' (b :: Ordering)
+               (c :: Type)
+               (l  :: k)
+               (v  :: k')
+               (r  :: [(k, k')]) :: Type where
+  OpExtUpd' :: Proxy b -> Label l -> WrapField c v -> Rec c r
+           -> OpExtUpd' b c l v r
+
+instance Require (OpExtUpd c l v '[]) ctx where
+  type ReqR (OpExtUpd c l v '[]) = Rec c '[ '(l,v)]
+  req ctx (OpExtUpd lv vv EmptyRec) = lv .=. vv .*. EmptyRec
+
+instance
+  Require (OpExtUpd' (Cmp l l₁) c l v ( '(l₁,v₁) ': r)) ctx
+  => Require (OpExtUpd c l v ( '(l₁,v₁) ': r)) ctx where
+  type ReqR (OpExtUpd c l v ( '(l₁,v₁) ': r))
+      = ReqR (OpExtUpd' (Cmp l l₁) c l v ( '(l₁,v₁) ': r))
+  req ctx (OpExtUpd lv vv r)
+     = req ctx (OpExtUpd' @(Cmp l l₁) @_ @_ @v
+                Proxy lv vv r)
+    
+instance Require (OpExtUpd' 'EQ c l v ( '(l, v₁) ': r)) ctx where
+  type ReqR (OpExtUpd' 'EQ c l v ( '(l, v₁) ': r))
+    = Rec c ( '(l, v) ': r)
+  req ctx (OpExtUpd' _ lv vv (ConsRec _ r))
+    = ConsRec @_ @_ @v (lv .=. vv) r
+
+instance Require (OpExtUpd' 'LT c l v ( '(l₁, v₁) ': r)) ctx where
+  type ReqR (OpExtUpd' 'LT c l v ( '(l₁, v₁) ': r))
+    = Rec c ( '(l, v) ': '(l₁, v₁) ': r)
+  req ctx (OpExtUpd' _ lv vv r) = (lv .=. vv) `ConsRec` r
+
+instance
+  (Require (OpExtUpd c (l :: k) (v :: k') r) ctx,
+    ReqR (OpExtUpd c l v r)
+  ~ Rec c (UnWrap @k @k' (ReqR (OpExtUpd c l v r))))
+  =>
+  Require (OpExtUpd' 'GT c l v ( '(l₁, v₁) ': r)) ctx where
+  type ReqR (OpExtUpd' 'GT c l v ( '(l₁, v₁) ': r)) =
+    Rec c ( '(l₁, v₁) ': UnWrap (ReqR (OpExtUpd c l v r)))
+  req ctx (OpExtUpd' _ lv vv (ConsRec lv₁ r)) =
+    lv₁ `ConsRec` (req ctx (OpExtUpd @_ @_ @v lv vv r))
+
+
+r ↑ (TagField _ _ v :: TagField c l v)
+  = req emptyCtx (OpExtUpd (Label @l) v r)
+
+-- | Left join
+
+type family LJoin (rₗ :: [(k,k')]) (rᵣ :: [(k,k')]) :: [(k,k')] where
+  LJoin '[] rᵣ = rᵣ
+  LJoin rₗ '[] = rₗ
+  LJoin ( '(lₗ,vₗ) ': rₗ) ( '(lᵣ,vᵣ) ': rᵣ)
+       = If (Cmp lₗ lᵣ == 'LT)
+            ( '(lₗ,vₗ) ': LJoin rₗ ( '(lᵣ,vᵣ) ': rᵣ))
+            (If (Cmp lₗ lᵣ == 'EQ)
+                ( '(lₗ,vₗ) ': LJoin rₗ rᵣ)
+                ( '(lᵣ,vᵣ) ': LJoin ( '(lₗ,vₗ) ': rₗ) rᵣ))
+
+data OpLJoin (c  :: Type)
+             (rₗ :: [(k,k')])
+             (rᵣ :: [(k,k')]) :: Type where
+  OpLJoin :: Rec c rₗ -> Rec c rᵣ -> OpLJoin c rₗ rᵣ
+
+instance Require (OpLJoin c '[] rᵣ) ctx where
+  type ReqR (OpLJoin c '[] rᵣ) = Rec c rᵣ
+  req ctx (OpLJoin _ r) = r
+
+instance Require (OpLJoin c (x ': r_l) '[]) ctx where
+  type ReqR (OpLJoin c (x ': r_l) '[]) = Rec c (x ': r_l)
+  req ctx (OpLJoin r _) = r
+
+data OpLJoin' (b :: Ordering)
+              (c  :: Type)
+              (rₗ :: [(k,k')])
+              (rᵣ :: [(k,k')]) :: Type where
+  OpLJoin' :: Proxy b -> Rec c rₗ -> Rec c rᵣ -> OpLJoin' b c rₗ rᵣ
+
+instance (
+  Require (OpLJoin' (Cmp lₗ lᵣ) c ( '(lₗ, vₗ) ': rₗ) ( '(lᵣ, vᵣ) ': rᵣ)) ctx
+  )
+  => Require (OpLJoin c ( '(lₗ, vₗ) ': rₗ) ( '(lᵣ, vᵣ) ': rᵣ)) ctx where
+  type ReqR (OpLJoin c ( '(lₗ, vₗ) ': rₗ) ( '(lᵣ, vᵣ) ': rᵣ))
+    = ReqR (OpLJoin' (Cmp lₗ lᵣ) c ( '(lₗ, vₗ) ': rₗ) ( '(lᵣ, vᵣ) ': rᵣ))
+  req ctx (OpLJoin (ConsRec lvₗ rₗ) (ConsRec lvᵣ rᵣ))
+    = req ctx (OpLJoin' (Proxy @(Cmp lₗ lᵣ))
+               (ConsRec lvₗ rₗ) (ConsRec lvᵣ rᵣ))
+
+instance
+  (Require (OpLJoin c rₗ ( '(lᵣ,vᵣ) ': (rᵣ :: [(k,k')]))) ctx
+  , ReqR (OpLJoin c rₗ ('(lᵣ, vᵣ) : rᵣ))
+  ~ Rec c (UnWrap @k @k'(ReqR (OpLJoin c rₗ ('(lᵣ, vᵣ) : rᵣ)))))
+  =>
+  Require (OpLJoin' 'LT c ( '(lₗ, vₗ) ': rₗ) ( '(lᵣ, vᵣ) ': rᵣ)) ctx where
+  type ReqR (OpLJoin' 'LT c ( '(lₗ, vₗ) ': rₗ) ( '(lᵣ, vᵣ) ': rᵣ))
+    = Rec c ('(lₗ,vₗ) ': UnWrap (ReqR (OpLJoin c rₗ ( '(lᵣ,vᵣ) ': rᵣ))))
+  req ctx (OpLJoin' _ (ConsRec lvₗ rₗ) (ConsRec lvᵣ rᵣ))
+   = lvₗ `ConsRec` (req ctx (OpLJoin rₗ (ConsRec lvᵣ rᵣ)))
+
+instance
+  (Require (OpLJoin c ('(lₗ, vₗ) : rₗ) (rᵣ :: [(k,k')])) ctx
+  , ReqR (OpLJoin c ('(lₗ, vₗ) : rₗ) rᵣ)
+  ~ Rec c (UnWrap @k @k' (ReqR (OpLJoin c ('(lₗ, vₗ) : rₗ) rᵣ)))
+  )
+  =>
+  Require (OpLJoin' 'GT c ( '(lₗ, vₗ) ': rₗ) ( '(lᵣ, vᵣ) ': rᵣ)) ctx where
+  type ReqR (OpLJoin' 'GT c ( '(lₗ, vₗ) ': rₗ) ( '(lᵣ, vᵣ) ': rᵣ))
+    = Rec c ('(lᵣ,vᵣ) ': UnWrap (ReqR (OpLJoin c ( '(lₗ,vₗ) ': rₗ) rᵣ)))
+  req ctx (OpLJoin' _ (ConsRec lvₗ rₗ) (ConsRec lvᵣ rᵣ))
+   = lvᵣ `ConsRec` (req ctx (OpLJoin (ConsRec lvₗ rₗ) rᵣ))
+
+instance
+  (ReqR (OpLJoin c rₗ (rᵣ :: [(k,k')]))
+  ~ Rec c (UnWrap @k @k' (ReqR (OpLJoin c rₗ rᵣ))),
+  Require (OpLJoin c rₗ rᵣ) ctx)
+  => Require (OpLJoin' 'EQ c ( '(l, vₗ) ': rₗ) ( '(l, vᵣ) ': rᵣ)) ctx where
+  type ReqR (OpLJoin' 'EQ c ( '(l, vₗ) ': rₗ) ( '(l, vᵣ) ': rᵣ))
+    = Rec c ( '(l, vₗ) ': UnWrap (ReqR (OpLJoin c rₗ rᵣ)))
+  req ctx (OpLJoin' _ (ConsRec lvₗ rₗ) (ConsRec _ rᵣ))
+    = lvₗ `ConsRec` (req ctx (OpLJoin rₗ rᵣ))
+
+
+
+(⋉) :: Require (OpLJoin c rₗ rᵣ) '[] =>
+     Rec c rₗ
+     -> Rec c rᵣ -> ReqR (OpLJoin c rₗ rᵣ)
+rₗ   ⋉ rᵣ = req emptyCtx (OpLJoin rₗ rᵣ)
+rₗ .:>< rᵣ = req emptyCtx (OpLJoin rₗ rᵣ)
+
+data SComp (b :: Ordering) where
+  SEQ :: SComp 'EQ
+  SLT :: SComp 'LT
+  SGT :: SComp 'GT
+
+-- term-level comparison
+class CmpVal (l :: k)(l₁ :: k) where
+  cmpVal :: Label l -> Label l₁ -> Ordering
+
+instance (KnownSymbol l, KnownSymbol l₁) 
+  => CmpVal (l :: Symbol) (l₁ :: Symbol) where
+  cmpVal l r = compare (symbolVal l)(symbolVal r)
+
+prCmp :: CmpVal lₗ lᵣ =>
+  (TagField c lₗ vₗ) -> (TagField c lᵣ vᵣ)
+      -> SComp (Cmp lₗ lᵣ)
+prCmp (_ :: TagField c lₗ vₗ)
+      (_ :: TagField c lᵣ vᵣ)
+  = case cmpVal (Label @lₗ) (Label @lᵣ) of
+      LT -> case unsafeCoerce Refl :: Cmp lₗ lᵣ :~: 'LT of
+              Refl -> SLT
+      GT -> case unsafeCoerce Refl :: Cmp lₗ lᵣ :~: 'GT of
+              Refl -> SGT
+      EQ -> case unsafeCoerce Refl :: Cmp lₗ lᵣ :~: 'EQ of
+              Refl -> SEQ
+
diff --git a/src/Data/GenRec/Label.hs b/src/Data/GenRec/Label.hs
deleted file mode 100644
--- a/src/Data/GenRec/Label.hs
+++ /dev/null
@@ -1,29 +0,0 @@
-{-|
-Module      : Language.Grammars.AspectAG.Label
-Description : Labels (polykinded, phantom)
-Copyright   : (c) Juan García Garland, Marcos Viera 2020
-License     : GPL-3
-Maintainer  : jpgarcia@fing.edu.uy
-Stability   : experimental
-Portability : POSIX
--}
-
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE DataKinds #-}
-
-module Data.GenRec.Label where
-import Data.Proxy
-
-data Label l = Label
-
-sndLabel :: Label '(a,b) -> Label b
-sndLabel _ = undefined
-
-fstLabel :: Label '(a,b) -> Label a
-fstLabel _ = undefined
-
-labelFromType :: a -> Label a
-labelFromType _ = Label
-
-proxyToLabel :: Proxy a -> Label a
-proxyToLabel _ = Label
diff --git a/src/Data/GenRec/RecInstances/Record.hs b/src/Data/GenRec/RecInstances/Record.hs
--- a/src/Data/GenRec/RecInstances/Record.hs
+++ b/src/Data/GenRec/RecInstances/Record.hs
@@ -23,7 +23,7 @@
   (Record, Reco,
    untag, getLabel,
    (.==.), (.**.), (##),
-   emptyRecord
+   emptyRecord, Tagged (..), Tagged
   )
   where
 
@@ -31,9 +31,12 @@
 import Data.Kind
 import Data.Proxy
 import Data.GenRec
-import Data.GenRec.Label
+import Data.Label
 
+import Data.Type.Equality
+import Unsafe.Coerce
 
+
 -- | * Records
 
 -- | datatype definition
@@ -112,11 +115,6 @@
     in '{' : show lv ++ ", " ++ shr
 
 
-r =        (Label @"integer" .==. (3 :: Integer))
-     .**.  (Label @"boolean" .==. True)
-     .**.  emptyRecord
-
-
 data Mat
 type Matrix = Rec Mat :: [(Nat, [(Symbol, Type)])] -> Type
 
@@ -148,3 +146,49 @@
 -- m' =        TagField @Mat (Label @Mat) (Label @1) r
 --        .*.  TagField (Label @Mat) (Label @2) (EmptyRec :: Record ('[] :: [(Symbol, Type)]))
 --        .*.  EmptyRec
+
+rCast :: Record '[ '("int", Int)]
+rCast = castWith (sym bad) r
+ where bad :: Record '[ '("int", Int)]
+             :~: Record '[ '("boolean", Bool), '("int", Int)]
+       bad = unsafeCoerce Refl -- undefined  no funciona porque se evalúa la prueba
+
+
+r  =        (Label @"int" .==. (3 :: Int))
+      .**.  (Label @"boolean" .==. True)
+      .**.  emptyRecord
+
+
+-- r1 :: Record
+--        '[ '("boolean", Bool),
+--           '("boolean2", Bool),
+--           '("int", Int),
+--           '("int2", Int)]
+r1 =        (Label @"int" .==. (3 :: Int))
+      .**.  (Label @"boolean" .==. True)
+      .**.  (Label @"int2" .==. (5 :: Int))
+      .**.  (Label @"boolean2" .==. False)
+      .**.  emptyRecord
+
+-- r2 :: Record
+--        '[ '("char", Char),
+--           '("int", Int),
+--           '("integer", Integer),
+--           '("unit", ())]
+r2 =        (Label @"int" .==. (40 :: Int))
+      .**.  (Label @"unit" .==. ())
+      .**.  (Label @"integer" .==. (5 :: Integer))
+      .**.  (Label @"boolean" .==. False)
+      .**.  emptyRecord
+
+t3    = r1 # Label @"int"
+tTrue = r1 # Label @"boolean"
+
+r12 = r1 .:>< r2
+
+-- r12 == {boolean : True,
+--         boolean2 : False,
+--         int : 3,
+--         int2 : 5,
+--         integer : 5,
+--         unit : ()}
diff --git a/src/Data/GenRec/Unordered.hs b/src/Data/GenRec/Unordered.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/GenRec/Unordered.hs
@@ -0,0 +1,121 @@
+{-|
+Module      : Data.GenRecord.Unordered
+Description : polykinded extensible record library
+Copyright   : (c) Juan García Garland (2023)
+License     : GPL
+Maintainer  : jpgarcia@fing.edu.uy
+Stability   : experimental
+Portability : POSIX
+
+Records where labels are names (|Symbol|s) and preserve the insertion
+order (hence they are not ordered alphanumerically).
+
+We did not reuse Generic record constructs from |Data.GenRec| and
+built new definitions instead. This module is intended to mimmick
+ordinary Haskell records, while being extensive.
+
+One quirk of the definitions in this module is that we admit repeated
+labels. Ordinary lookup will get the first occurrence, but we build
+different kind of projections to get all values under a label. This
+development was first intended to represent a collection of registers
+with names and values, hence the field name.
+
+-}
+
+{-# OPTIONS_GHC -fno-warn-missing-methods #-}
+
+{-# LANGUAGE DataKinds,
+             TypeOperators,
+             PolyKinds,
+             GADTs,
+             RankNTypes,
+             StandaloneDeriving,
+             FlexibleInstances,
+             FlexibleContexts,
+             ConstraintKinds,
+             MultiParamTypeClasses,
+             FunctionalDependencies,
+             UndecidableInstances,
+             ScopedTypeVariables,
+             TypeFamilies,
+             InstanceSigs,
+             AllowAmbiguousTypes,
+             TypeApplications,
+             PatternSynonyms,
+             DataKinds, PolyKinds
+#-}
+
+module Data.GenRec.Unordered where
+import Data.Label
+import GHC.TypeLits (Symbol, symbolVal, KnownSymbol)
+import Data.Kind
+import Data.Proxy
+import Data.Type.Require
+
+import Data.GenRec (UnWrap)
+
+data Reg (l :: Symbol) v where
+  Reg :: (KnownSymbol l) => v -> Reg l v
+
+instance
+  Show v
+  =>
+  Show (Reg l v) where
+  show (Reg v) = symbolVal (Proxy @l) ++ " : " ++ show v
+
+infixr 5 :<
+data Record (r :: [(Symbol, Type)]) :: Type where
+  Empty :: Record '[] -- ^ empty record
+  (:<) :: Reg l v -> Record r -> Record ('( l, v) ': r) -- ^
+
+instance
+  Show (Record '[]) where
+  show Empty = "{}"
+
+instance
+  (Show v)
+  =>
+  Show (Record '[ '(l,v)]) where
+  show (reg :< _) = "{ " ++ show reg ++ "}"
+  
+instance
+  ( Show v
+  , Show (Record (lv ': r)))
+  =>
+  Show (Record ( '(l, v) ': lv ': r)) where
+  show (reg :< r) =  "{" ++ show reg ++ ", " ++ tail (show r)
+
+ex1 =  Reg @"x" 3.0
+    :< Reg @"y" 2.1
+    :< Reg @"z" ()
+    :< Reg @"t" 0
+    :< Empty
+
+ex2 =  Reg @"header" ()
+    :< Reg @"val" 2.1
+    :< Reg @"val" 1.1
+    :< Reg @"val" 0.0
+    :< Reg @"footer" "END"
+    :< Empty
+
+type instance UnWrap (Record l) = l
+
+data OpSnoc (l :: Symbol) (v :: Type) (r :: [(Symbol, Type)]) where
+  OpSnoc :: Reg l v -> Record r -> OpSnoc l v r
+
+instance
+  Require (OpSnoc l v '[]) ctx where
+  type ReqR (OpSnoc l v '[])
+    = Record '[ '(l, v)]
+  req ctx (OpSnoc lv _) = lv :< Empty
+
+
+instance
+  RequireR (OpSnoc l v r) (Record (UnWrap (ReqR (OpSnoc l v r)))) ctx
+  =>
+  Require (OpSnoc l v ( '(l',v') ': r)) ctx where
+  type ReqR (OpSnoc l v ( '(l',v') ': r)) =
+    Record ( '(l',v') ': UnWrap @Symbol @Type (ReqR (OpSnoc l v r)))
+  req ctx (OpSnoc lv (lv' :< r)) = lv' :< req ctx (OpSnoc lv r) 
+
+r >: lv = req (Proxy @'[]) (OpSnoc lv r)
diff --git a/src/Data/HList.hs b/src/Data/HList.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/HList.hs
@@ -0,0 +1,114 @@
+{-|
+Module      : Data.HList
+Description :
+Implementation of strongly typed heterogeneous lists.
+Copyright   : (c) Juan García Garland, 2018,2023
+License     : GPL
+Maintainer  : jpgarcia@fing.edu.uy
+Stability   : experimental
+Portability : POSIX
+|-}
+
+{-# OPTIONS_GHC -fno-warn-missing-methods,
+                -fno-warn-partial-type-signatures #-}
+
+{-# LANGUAGE DataKinds,
+             TypeOperators,
+             PolyKinds,
+             GADTs,
+             TypeInType,
+             RankNTypes,
+             StandaloneDeriving,
+             FlexibleInstances,
+             FlexibleContexts,
+             ConstraintKinds,
+             MultiParamTypeClasses,
+             FunctionalDependencies,
+             UndecidableInstances,
+             ScopedTypeVariables,
+             TypeFamilies,
+             InstanceSigs,
+             AllowAmbiguousTypes,
+             TypeApplications,
+             PatternSynonyms,
+             PartialTypeSignatures
+#-}
+
+module Data.HList where
+
+import Data.Kind
+import Data.Proxy
+import Data.Label
+import Data.Type.Bool
+import Data.Type.Equality
+
+-- |Heterogeneous lists are implemented as a GADT
+data HList (l :: [Type]) :: Type  where
+  HNil :: HList '[]
+  HCons :: x -> HList xs -> HList (x ': xs)
+
+hHead :: HList (t ': _) -> t
+hHead (HCons v _) = v
+
+
+-- | HMember is a test membership function.
+--Since we are in Haskell the value level function computes with the evidence 
+class HMember (t :: Type) (l :: [Type]) where
+  type HMemberRes t l :: Bool
+  hMember :: Label t -> HList l -> Proxy (HMemberRes t l)
+
+instance HMember t '[] where
+  type HMemberRes t '[] = 'False
+  hMember _ _ = Proxy
+
+instance HMember t (t' ': ts) where
+  type HMemberRes t (t' ': ts) = t == t' || HMemberRes t ts
+  hMember _ _ = Proxy
+
+-- | HMember' is a test membership function.
+-- But looking up in a list of Labels
+class HMember' (t :: k) (l :: [k]) where
+  type HMemberRes' t l :: Bool
+  hMember' :: f t -> LList l -> Proxy (HMemberRes' t l)
+
+instance HMember' t '[] where
+  type HMemberRes' t '[] = 'False
+  hMember' _ _ = Proxy
+
+instance HMember' t (t' ': ts) where
+  type HMemberRes' t (t' ': ts) = t == t' || HMemberRes' t ts
+  hMember' _ _ = Proxy
+
+
+-- | No other functionality is needed for AAG
+
+infixr 2 .:
+(.:) = HCons
+ε = HNil
+hn = HNil
+
+-- | a polykinded heteogeneous list of labels
+data LList (l :: [k]) :: Type where
+  LNil :: LList '[]
+  LCons :: Label h -> LList l -> LList (h ': l)
+
+infixr 2 .:.
+(.:.) = LCons
+lL = LNil
+
+lHead :: LList (t ': ts) -> Label t
+lHead _ = Label
+
+class LListFrom (l :: [k]) where
+  lListFrom :: Proxy l -> LList l
+
+instance LListFrom ('[] :: [k]) where
+  lListFrom (Proxy :: Proxy '[])= LNil
+
+instance LListFrom ts => LListFrom (t ': ts) where
+  lListFrom (Proxy :: Proxy (t ': ts))
+    = LCons Label $ lListFrom Proxy
+
+type family Snoc (l :: [k]) (v :: k) where
+  Snoc '[]       v  = '[v]
+  Snoc (x ': xs) v  = x ': Snoc xs v 
diff --git a/src/Data/Label.hs b/src/Data/Label.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Label.hs
@@ -0,0 +1,31 @@
+{-|
+Module      : Data.Label
+Description : Labels (polykinded, phantom).
+  Basically a reimplementation of Proxy,
+  where we have control over the codebase
+Copyright   : (c) Juan García Garland, Marcos Viera 2020
+License     : GPL-3
+Maintainer  : jpgarcia@fing.edu.uy
+Stability   : experimental
+Portability : POSIX
+-}
+
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE DataKinds #-}
+
+module Data.Label where
+import Data.Proxy
+
+data Label l = Label
+
+sndLabel :: Label '(a,b) -> Label b
+sndLabel _ = undefined
+
+fstLabel :: Label '(a,b) -> Label a
+fstLabel _ = undefined
+
+labelFromType :: a -> Label a
+labelFromType _ = Label
+
+proxyToLabel :: Proxy a -> Label a
+proxyToLabel _ = Label