diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2018, Alejandro Serrano
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Alejandro Serrano nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/kind-generics-deriving.cabal b/kind-generics-deriving.cabal
new file mode 100644
--- /dev/null
+++ b/kind-generics-deriving.cabal
@@ -0,0 +1,37 @@
+cabal-version:       >=1.10
+name:                kind-generics-deriving
+version:             0.3.0.0
+synopsis:            Generic programming in GHC style for arbitrary kinds and GADTs.
+description:         This package provides automatic derivation for a wide range of classes using `kind-generics`.
+-- bug-reports:
+license:             BSD3
+license-file:        LICENSE
+author:              Alejandro Serrano
+maintainer:          trupill@gmail.com
+-- copyright:
+category:            Data
+build-type:          Simple
+
+source-repository head
+  type:     git
+  location: https://gitlab.com/trupill/kind-generics.git
+
+library
+  exposed-modules:     Generics.Kind.Derive.Eq,
+                       Generics.Kind.Derive.EqTwoParams,
+                       Generics.Kind.Derive.FunctorPosition,
+                       Generics.Kind.Derive.FunctorOne,
+                       Generics.Kind.Derive.Traversable,
+                       Generics.Kind.Derive.KFunctor,
+                       Generics.Kind.Derive.Json,
+                       Generics.Kind.Derive.Examples
+  -- other-modules:
+  -- other-extensions:
+  build-depends:       base >= 4.12 && < 5
+                     , kind-apply
+                     , kind-generics >= 0.5
+                     , first-class-families >= 0.8 && < 0.9
+                     , aeson
+  hs-source-dirs:      src
+  default-language:    Haskell2010
+  ghc-options:         -Wall -fprint-explicit-kinds
diff --git a/src/Generics/Kind/Derive/Eq.hs b/src/Generics/Kind/Derive/Eq.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/Kind/Derive/Eq.hs
@@ -0,0 +1,58 @@
+{-# language AllowAmbiguousTypes   #-}
+{-# language ConstraintKinds       #-}
+{-# language DataKinds             #-}
+{-# language FlexibleContexts      #-}
+{-# language FlexibleInstances     #-}
+{-# language MultiParamTypeClasses #-}
+{-# language PolyKinds             #-}
+{-# language QuantifiedConstraints #-}
+{-# language ScopedTypeVariables   #-}
+{-# language TypeApplications      #-}
+{-# language TypeFamilies          #-}
+{-# language TypeOperators         #-}
+{-# language UndecidableInstances  #-}
+module Generics.Kind.Derive.Eq where
+
+import           Data.Kind
+import           GHC.TypeLits
+import           Generics.Kind
+
+geq' :: forall t. (GenericK t, GEq (RepK t), ReqsEq (RepK t) 'LoT0)
+     => t -> t -> Bool
+geq' x y = geq (fromK @_ @t @'LoT0 x) (fromK @_ @t @'LoT0 y)
+
+class GEq (f :: LoT k -> Type) where
+  type family ReqsEq f (tys :: LoT k) :: Constraint
+  geq :: ReqsEq f tys => f tys -> f tys -> Bool
+
+instance GEq U1 where
+  type ReqsEq U1 tys = ()
+  geq U1 U1 = True
+
+instance GEq f => GEq (M1 i c f) where
+  type ReqsEq (M1 i c f) tys = ReqsEq f tys
+  geq (M1 x) (M1 y) = geq x y
+
+instance (GEq f, GEq g) => GEq (f :+: g) where
+  type ReqsEq (f :+: g) tys = (ReqsEq f tys, ReqsEq g tys)
+  geq (L1 x) (L1 y) = geq x y
+  geq (R1 x) (R1 y) = geq x y
+  geq _      _      = False
+
+instance (GEq f, GEq g) => GEq (f :*: g) where
+  type ReqsEq (f :*: g) tys = (ReqsEq f tys, ReqsEq g tys)
+  geq (x1 :*: x2) (y1 :*: y2) = geq x1 y1 && geq x2 y2
+
+instance GEq (Field t) where
+  type ReqsEq (Field t) tys = Eq (Interpret t tys)
+  geq (Field x) (Field y) = x == y
+
+instance GEq f => GEq (c :=>: f) where
+  type ReqsEq (c :=>: f) tys = ReqsEq f tys
+  -- really we want          = Interpret c tys => GEq f tys
+  geq (SuchThat x) (SuchThat y) = geq x y
+
+instance TypeError ('Text "Existentials are not supported")
+         => GEq (Exists k f) where
+  type ReqsEq (Exists k f) tys = TypeError ('Text "Existentials are not supported")
+  geq = undefined
diff --git a/src/Generics/Kind/Derive/EqTwoParams.hs b/src/Generics/Kind/Derive/EqTwoParams.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/Kind/Derive/EqTwoParams.hs
@@ -0,0 +1,57 @@
+{-# language AllowAmbiguousTypes   #-}
+{-# language DataKinds             #-}
+{-# language FlexibleContexts      #-}
+{-# language FlexibleInstances     #-}
+{-# language MultiParamTypeClasses #-}
+{-# language PolyKinds             #-}
+{-# language QuantifiedConstraints #-}
+{-# language ScopedTypeVariables   #-}
+{-# language TypeApplications      #-}
+{-# language TypeFamilies          #-}
+{-# language TypeOperators         #-}
+{-# language UndecidableInstances  #-}
+module Generics.Kind.Derive.EqTwoParams where
+
+import           Data.Kind
+import           Generics.Kind
+
+geq2' :: forall t. (GenericK t, GEq2 (RepK t) 'LoT0 'LoT0)
+      => t -> t -> Bool
+geq2' x y = geq2 (fromK @_ @t @'LoT0 x) (fromK @_ @t @'LoT0 y)
+
+class GEq2 (f :: LoT k -> Type) (xs :: LoT k) (ys :: LoT k) where
+  geq2 :: f xs -> f ys -> Bool
+
+instance GEq2 U1 xs ys where
+  geq2 U1 U1 = True
+
+instance (GEq2 f xs ys) => GEq2 (M1 i c f) xs ys where
+  geq2 (M1 x) (M1 y) = geq2 x y
+
+instance (GEq2 f xs ys, GEq2 g xs ys) => GEq2 (f :+: g) xs ys where
+  geq2 (L1 x) (L1 y) = geq2 x y
+  geq2 (R1 x) (R1 y) = geq2 x y
+  geq2 _      _      = False
+
+instance (GEq2 f xs ys, GEq2 g xs ys) => GEq2 (f :*: g) xs ys where
+  geq2 (x1 :*: x2) (y1 :*: y2) = geq2 x1 y1 && geq2 x2 y2
+
+instance (Interpret t xs ~ Interpret t ys, Eq (Interpret t xs)) => GEq2 (Field t) xs ys where
+  geq2 (Field x) (Field y) = x == y
+
+instance ((Interpret c xs, Interpret c ys) => GEq2 f xs ys)
+         => GEq2 (c :=>: f) xs ys where
+  geq2 (SuchThat x) (SuchThat y) = geq2 x y
+
+instance (forall x y. GEq2 f (x ':&&: xs) (y ':&&: ys))
+         => GEq2 (Exists k f) xs ys where
+  geq2 (Exists x) (Exists y) = geq2 x y
+
+{-
+instance (forall x y. GEq2 f (x ':&&: xs) (y ':&&: ys))
+         => GEq2 (ERefl f) xs ys where
+  geq2 (ERefl (x :: f (x :&&: xs))) (ERefl (y :: f (y :&&: ys)))
+    = case eqTypeRep (typeRep @x) (typeRep @y) of
+        Nothing    -> False
+        Just HRefl -> geq2 x y
+-}
diff --git a/src/Generics/Kind/Derive/Examples.hs b/src/Generics/Kind/Derive/Examples.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/Kind/Derive/Examples.hs
@@ -0,0 +1,75 @@
+{-# OPTIONS_GHC -fno-warn-orphans  #-}
+{-# language DataKinds             #-}
+{-# language FlexibleInstances     #-}
+{-# language MultiParamTypeClasses #-}
+{-# language ScopedTypeVariables   #-}
+{-# language TypeOperators         #-}
+module Generics.Kind.Derive.Examples where
+
+import           Data.Aeson                           (FromJSON (..), ToJSON (..))
+import           Data.PolyKinded.Functor
+import           Data.Traversable                     (foldMapDefault)
+
+import           Generics.Kind
+import           Generics.Kind.Derive.Eq
+import           Generics.Kind.Derive.FunctorOne
+import           Generics.Kind.Derive.FunctorPosition
+import           Generics.Kind.Derive.Json
+import           Generics.Kind.Derive.KFunctor
+import           Generics.Kind.Derive.Traversable
+import           Generics.Kind.Examples
+
+-- Maybe
+instance KFunctor Maybe '[ 'Co ] (a ':&&: 'LoT0) (b ':&&: 'LoT0) where
+  kfmap = kfmapDefault
+
+-- Tree
+instance Eq a => Eq (Tree a) where
+  (==) = geq'
+instance ToJSON a => ToJSON (Tree a) where
+  toJSON = gtoJSON'
+instance FromJSON a => FromJSON (Tree a) where
+  parseJSON = gfromJSON'
+instance KFunctor Tree '[ 'Co ] (a ':&&: 'LoT0) (b ':&&: 'LoT0) where
+  kfmap = kfmapDefault
+instance Functor Tree where
+  -- fmap = fmapDefault
+  fmap = fmapDefaultOne
+instance Foldable Tree where
+  foldMap = foldMapDefault
+instance Traversable Tree where
+  traverse = traverseDefault
+
+-- TTY (from https://gitlab.com/trupill/kind-generics/issues/3)
+instance Eq (TTY m a) where
+  (==) = geq'
+instance ToJSON (TTY m a) where
+  toJSON = gtoJSON'
+{-
+instance FromJSON (TTY m a) where
+  parseJSON = gfromJSON'
+
+Fails with:
+• Couldn't match type ‘a’ with ‘()’ arising from a use of ‘gfromJSON'’
+-}
+
+fmapEither :: (a -> b) -> Either e a -> Either e b
+fmapEither = fmapDefault'
+
+-- WeirdTree
+instance Show b => KFunctor WeirdTree '[ 'Co ] (a ':&&: 'LoT0) (b ':&&: 'LoT0) where
+  kfmap = kfmapDefault
+
+-- WeirdTree with reflected existentials
+-- instance (Eq a) => Eq (WeirdTreeR a) where
+  -- (==) = geq'
+
+instance Functor (SimpleIndex a) where
+  fmap = fmapDefault
+instance Foldable (SimpleIndex a) where
+  foldMap = foldMapDefault
+instance Traversable (SimpleIndex a) where
+  traverse = traverseDefault
+
+instance EFunctor f => Functor (Hkd f) where
+  fmap = fmapDefaultOne
diff --git a/src/Generics/Kind/Derive/FunctorOne.hs b/src/Generics/Kind/Derive/FunctorOne.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/Kind/Derive/FunctorOne.hs
@@ -0,0 +1,101 @@
+{-# language AllowAmbiguousTypes   #-}
+{-# language ConstraintKinds       #-}
+{-# language DataKinds             #-}
+{-# language FlexibleContexts      #-}
+{-# language FlexibleInstances     #-}
+{-# language MultiParamTypeClasses #-}
+{-# language PolyKinds             #-}
+{-# language QuantifiedConstraints #-}
+{-# language ScopedTypeVariables   #-}
+{-# language TemplateHaskell       #-}
+{-# language TypeApplications      #-}
+{-# language TypeFamilies          #-}
+{-# language TypeOperators         #-}
+{-# language UndecidableInstances  #-}
+module Generics.Kind.Derive.FunctorOne where
+
+import           Data.Kind
+import           Data.Proxy
+import           Generics.Kind
+import qualified Fcf.Core as Fcf
+import           Fcf.Combinators (Pure, Pure1, type (<=<))
+
+fmapDefaultOne :: (GenericK f,
+                   GenericK f,
+                   GFunctorOne (RepK f),
+                   Reqs (RepK f) a b)
+                => (a -> b) -> f a -> f b
+fmapDefaultOne f = toK . gfmapo f . fromK
+
+class GFunctorOne (f :: LoT (Type -> Type) -> Type) where
+  type family Reqs f a b :: Constraint
+  gfmapo :: Reqs f a b => (a -> b) -> f (LoT1 a) -> f (LoT1 b)
+
+gfmapo' :: forall a b f. (GFunctorOne f, Reqs f a b)
+        => (a -> b) -> f (LoT1 a) -> f (LoT1 b)
+gfmapo' = gfmapo
+
+
+instance GFunctorOne U1 where
+  type Reqs U1 a b = ()
+  gfmapo _ U1 = U1
+
+instance GFunctorOne f => GFunctorOne (M1 i c f) where
+  type Reqs (M1 i c f) a b = Reqs f a b
+  gfmapo v (M1 x) = M1 (gfmapo v x)
+
+instance (GFunctorOne f, GFunctorOne g)
+         => GFunctorOne (f :+: g) where
+  type Reqs (f :+: g) a b = (Reqs f a b, Reqs g a b)
+  gfmapo v (L1 x) = L1 (gfmapo v x)
+  gfmapo v (R1 x) = R1 (gfmapo v x)
+
+instance (GFunctorOne f, GFunctorOne g)
+         => GFunctorOne (f :*: g) where
+  type Reqs (f :*: g) a b = (Reqs f a b, Reqs g a b)
+  gfmapo v (x :*: y) = gfmapo v x :*: gfmapo v y
+
+instance GFunctorOne f => GFunctorOne (c :=>: f) where
+  type Reqs (c :=>: f) a b = (Interpret c (LoT1 b), Reqs f a b)
+  -- actually you want     = Interpret c (LoT1 a) => (Interpret c (LoT1 b), Reqs f a b)
+  gfmapo v (SuchThat x) = SuchThat (gfmapo v x)
+
+class GFunctorOneArg (t :: Atom (Type -> Type) Type) where
+  gfmapof :: Proxy t -> (a -> b)
+          -> Interpret t (LoT1 a) -> Interpret t (LoT1 b)
+
+instance GFunctorOneArg t => GFunctorOne (Field t) where
+  type Reqs (Field t) a b = (() :: Constraint)
+  gfmapo v (Field x) = Field (gfmapof (Proxy @t) v x)
+
+-- A constant
+instance GFunctorOneArg ('Kon t) where
+  gfmapof _ _ x = x
+-- The type variable itself
+instance GFunctorOneArg Var0 where
+  gfmapof _ f x = f x
+-- Going through functor
+instance forall f x.
+         (Functor f, GFunctorOneArg x)
+         => GFunctorOneArg (f :$: x) where
+  gfmapof _ f x = fmap (gfmapof (Proxy @x) f) x
+
+-- Support for Hkd, defunctionalized variant, simplfiied GenericK instance.
+instance EFunctor f => GFunctorOneArg (Eval (Kon f :@: Var0)) where
+  gfmapof _ f x = emap @f f x
+
+-- Unary first-class family as a functor.
+class EFunctor (f :: Type -> Fcf.Exp Type) where
+  emap :: (a -> b) -> Fcf.Eval (f a) -> Fcf.Eval (f b)
+
+-- The functor "x" (identity functor).
+instance EFunctor Pure where
+  emap = id
+
+-- The functor "f x", for any Functor f
+instance Functor f => EFunctor (Pure1 f) where
+  emap = fmap
+
+-- Composition of functors
+instance (EFunctor t, EFunctor u) => EFunctor (t <=< u) where
+  emap = emap @t . emap @u
diff --git a/src/Generics/Kind/Derive/FunctorPosition.hs b/src/Generics/Kind/Derive/FunctorPosition.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/Kind/Derive/FunctorPosition.hs
@@ -0,0 +1,130 @@
+{-# language AllowAmbiguousTypes   #-}
+{-# language DataKinds             #-}
+{-# language FlexibleContexts      #-}
+{-# language FlexibleInstances     #-}
+{-# language MultiParamTypeClasses #-}
+{-# language PolyKinds             #-}
+{-# language QuantifiedConstraints #-}
+{-# language ScopedTypeVariables   #-}
+{-# language TypeApplications      #-}
+{-# language TypeFamilies          #-}
+{-# language TypeOperators         #-}
+{-# language UndecidableInstances  #-}
+module Generics.Kind.Derive.FunctorPosition where
+
+import           Data.Kind
+import           GHC.TypeLits
+import           Generics.Kind
+
+fmapDefaultPos :: forall v f as bs.
+                  (GenericK f, GenericK f,
+                   GFunctorPos (RepK f) v as bs)
+               => (Interpret ('Var v) as -> Interpret ('Var v) bs)
+               -> f :@@: as -> f :@@: bs
+fmapDefaultPos f = toK @_ @f @bs . gfmapp @_ @(RepK f) @v @as @bs f . fromK @_ @f @as
+
+fmapDefault :: forall f a b. (GenericK f, GenericK f,
+               GFunctorPos (RepK f) 'VZ (LoT1 a) (LoT1 b))
+            => (a -> b) -> f a -> f b
+fmapDefault = fmapDefaultPos @'VZ @f @(LoT1 a) @(LoT1 b)
+
+bimapDefault :: forall f a c b d.
+                (GenericK f, GenericK f, GenericK f,
+                 GFunctorPos (RepK f) 'VZ       (LoT2 a d) (LoT2 c d),
+                 GFunctorPos (RepK f) ('VS 'VZ) (LoT2 a b) (LoT2 a d))
+             => (a -> c) -> (b -> d) -> f a b -> f c d
+bimapDefault f g = fmapDefaultPos @'VZ       @f @(LoT2 a d) @(LoT2 c d) f
+                 . fmapDefaultPos @('VS 'VZ) @f @(LoT2 a b) @(LoT2 a d) g
+
+class GFunctorPos (f :: LoT k -> Type) (v :: TyVar k Type)
+                  (as :: LoT k) (bs :: LoT k) where
+  gfmapp :: (Interpret ('Var v) as -> Interpret ('Var v) bs)
+         -> f as -> f bs
+
+instance GFunctorPos U1 v as bs where
+  gfmapp _ U1 = U1
+
+instance forall f v as bs i c. GFunctorPos f v as bs
+         => GFunctorPos (M1 i c f) v as bs where
+  gfmapp v (M1 x) = M1 (gfmapp @_ @f @v @as @bs v x)
+
+instance forall f g v as bs. (GFunctorPos f v as bs, GFunctorPos g v as bs)
+         => GFunctorPos (f :+: g) v as bs where
+  gfmapp v (L1 x) = L1 (gfmapp @_ @f @v @as @bs v x)
+  gfmapp v (R1 x) = R1 (gfmapp @_ @g @v @as @bs v x)
+
+instance forall f g v as bs. (GFunctorPos f v as bs, GFunctorPos g v as bs)
+         => GFunctorPos (f :*: g) v as bs where
+  gfmapp v (x :*: y) = gfmapp @_ @f @v @as @bs v x :*: gfmapp @_ @g @v @as @bs v y
+
+instance forall c f v as bs z.
+         (Interpret c as => GFunctorPos f v as bs, z ~ Interpret c bs, Interpret c as => z)
+         => GFunctorPos (c :=>: f) v as bs where
+  gfmapp v (SuchThat x) = SuchThat (gfmapp @_ @f @v @as @bs v x)
+
+instance forall k f v as bs.
+         (forall (t :: k). GFunctorPos f ('VS v) (t ':&&: as) (t ':&&: bs))
+         => GFunctorPos (Exists k f) v as bs where
+  gfmapp v (Exists (x :: f (t ':&&: x)))
+    = Exists (gfmapp @_ @f @('VS v) @(t ':&&: x) @(t ':&&: _) v x)
+
+instance forall t v as bs. GFunctorArgPos t v as bs (ContainsTyVar v t)
+         => GFunctorPos (Field t) v as bs where
+  gfmapp v (Field x) = Field (gfmappf @_ @t @v @as @bs @(ContainsTyVar v t) v x)
+
+class GFunctorArgPos (t :: Atom d Type) (v :: TyVar d Type)
+                     (as :: LoT d) (bs :: LoT d)
+                     (p :: Bool) where
+  gfmappf :: (Interpret ('Var v) as -> Interpret ('Var v) bs)
+          -> Interpret t as -> Interpret t bs
+
+instance (Interpret t as ~ Interpret t bs) => GFunctorArgPos t v as bs 'False where
+  gfmappf _ = id
+
+instance TypeError ('Text "Should never get here")
+         => GFunctorArgPos ('Kon t) v as bs whatever where
+  gfmappf _ = id
+
+instance ( Functor (Interpret f as), Interpret f as ~ Interpret f bs
+         , GFunctorArgPos x v as bs (ContainsTyVar v x) )
+         => GFunctorArgPos (f ':@: x) v as bs 'True where
+  gfmappf f x = fmap (gfmappf @_ @x @v @as @bs @(ContainsTyVar v x) f) x
+
+-- We found the same variable
+instance GFunctorArgPos ('Var 'VZ) 'VZ (a ':&&: as) (b ':&&: bs) 'True where
+  gfmappf f x = f x
+-- We need to keep looking
+instance forall d (v :: TyVar d Type) n r as s bs isthere.
+         GFunctorArgPos ('Var v) n as bs isthere
+         => GFunctorArgPos ('Var ('VS v)) ('VS n) (r ':&&: as) (s ':&&: bs) isthere where
+  gfmappf f x = gfmappf @d @('Var v) @n @as @bs @isthere f x
+-- If we arrive to another we do not want, keep it as it is
+instance TypeError ('Text "Should never get here")
+         => GFunctorArgPos ('Var 'VZ) ('VS n) (r ':&&: as) (r ':&&: bs) 'True where
+  gfmappf _ = id
+instance TypeError ('Text "Should never get here")
+         => GFunctorArgPos ('Var ('VS n)) 'VZ (r ':&&: 'LoT0) (r ':&&: 'LoT0) 'True where
+  gfmappf _ = id
+
+-- Alternative implementation
+{-
+type family EqualTyVar (v :: TyVar d Type) (w :: TyVar d Type) :: Bool where
+  EqualTyVar v v = True
+  EqualTyVar v w = False
+
+class GFunctorVarPos (v :: TyVar d Type) (w :: TyVar d Type)
+                     (as :: LoT d) (bs :: LoT d)
+                     (equal :: Bool) where
+  gfmappv :: (Interpret (Var w) as -> Interpret (Var w) bs)
+          -> Interpret (Var v) as -> Interpret (Var v) bs
+
+instance v ~ w => GFunctorVarPos v w as bs True where
+  gfmappv f = f
+instance (Interpret (Var v) as ~ Interpret (Var v) bs)
+        => GFunctorVarPos v w as bs False where
+  gfmappv _ = id
+
+instance forall v w as bs. GFunctorVarPos v w as bs (EqualTyVar v w)
+         => GFunctorArgPos (Var v) w as bs True where
+  gfmappf = gfmappv @_ @v @w @as @bs @(EqualTyVar v w)
+-}
diff --git a/src/Generics/Kind/Derive/Json.hs b/src/Generics/Kind/Derive/Json.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/Kind/Derive/Json.hs
@@ -0,0 +1,105 @@
+{-# language DataKinds             #-}
+{-# language FlexibleContexts      #-}
+{-# language FlexibleInstances     #-}
+{-# language GADTs                 #-}
+{-# language MultiParamTypeClasses #-}
+{-# language PartialTypeSignatures #-}
+{-# language PolyKinds             #-}
+{-# language QuantifiedConstraints #-}
+{-# language ScopedTypeVariables   #-}
+{-# language TypeApplications      #-}
+{-# language TypeFamilies          #-}
+{-# language TypeOperators         #-}
+{-# language UndecidableInstances  #-}
+module Generics.Kind.Derive.Json where
+
+import           Control.Applicative
+import           Control.Monad
+import           Data.Aeson
+import           Data.Aeson.Types
+import           Data.Kind
+import           Data.Proxy
+import           GHC.Generics        (Meta (..))
+import           GHC.TypeLits
+import           Generics.Kind
+
+gtoJSON' :: forall t. (GenericK t, GToJSONK (RepK t) 'LoT0)
+         => t -> Value
+gtoJSON' x = gtoJSON (fromK @_ @t @'LoT0 x)
+
+gfromJSON' :: forall t. (GenericK t, GFromJSONK (RepK t) 'LoT0)
+           => Value -> Parser t
+gfromJSON' v = fmap (toK @_ @t @'LoT0) (gfromJSON v)
+
+class GToJSONK (f :: LoT k -> Type) (x :: LoT k) where
+  gtoJSON :: f x -> Value
+class GFromJSONK (f :: LoT k -> Type) (x :: LoT k) where
+  gfromJSON :: Value -> Parser (f x)
+
+instance ToJSON (Interpret t x)
+         => GToJSONK (Field t) x where
+  gtoJSON (Field t) = toJSON t
+instance FromJSON (Interpret t x)
+         => GFromJSONK (Field t) x where
+  gfromJSON = fmap Field . parseJSON
+
+instance GToJSONK U1 x where
+  gtoJSON U1 = Null
+instance GFromJSONK U1 x where
+  gfromJSON Null = pure U1
+  gfromJSON _    = empty
+
+instance (GToJSONK f x, GToJSONK g x)
+         => GToJSONK (f :+: g) x where
+  gtoJSON (L1 f) = gtoJSON f
+  gtoJSON (R1 g) = gtoJSON g
+instance (GFromJSONK f x, GFromJSONK g x)
+         => GFromJSONK (f :+: g) x where
+  gfromJSON v = (L1 <$> gfromJSON v) <|> (R1 <$> gfromJSON v)
+
+instance (GToJSONK f x, GToJSONK g x)
+         => GToJSONK (f :*: g) x where
+  gtoJSON (f :*: g) = toJSON (gtoJSON f, gtoJSON g)
+instance (GFromJSONK f x, GFromJSONK g x)
+         => GFromJSONK (f :*: g) x where
+  gfromJSON v = do (f, g) <- parseJSON v
+                   (:*:) <$> gfromJSON f <*> gfromJSON g
+
+instance forall name f x i fx st.
+         (GToJSONK f x, KnownSymbol name)
+         => GToJSONK (M1 i ('MetaCons name fx st) f) x where
+  gtoJSON (M1 f) = toJSON (symbolVal $ Proxy @name, gtoJSON f)
+instance forall name f x i fx st.
+         (GFromJSONK f x, KnownSymbol name)
+         => GFromJSONK (M1 i ('MetaCons name fx st) f) x where
+  gfromJSON v = do (name, f) <- parseJSON v
+                   guard $ name == symbolVal (Proxy @name)
+                   M1 <$> gfromJSON f
+
+instance GToJSONK f x
+         => GToJSONK (M1 i ('MetaData _1 _2 _3 _4) f) x where
+  gtoJSON (M1 f) = gtoJSON f
+instance GFromJSONK f x
+         => GFromJSONK (M1 i ('MetaData _1 _2 _3 _4) f) x where
+  gfromJSON = fmap M1 . gfromJSON
+
+instance GToJSONK f x
+         => GToJSONK (M1 i ('MetaSel _1 _2 _3 _4) f) x where
+  gtoJSON (M1 f) = gtoJSON f
+instance GFromJSONK f x
+         => GFromJSONK (M1 i ('MetaSel _1 _2 _3 _4) f) x where
+  gfromJSON = fmap M1 . gfromJSON
+
+instance (Interpret c x => GToJSONK f x)
+         => GToJSONK (c :=>: f) x where
+  gtoJSON (SuchThat f) = gtoJSON f
+instance (Interpret c x, GFromJSONK f x)
+         => GFromJSONK (c :=>: f) x where
+  gfromJSON = fmap SuchThat . gfromJSON
+
+instance (forall t. GToJSONK f (t ':&&: x))
+         => GToJSONK (Exists k f) x where
+  gtoJSON (Exists x) = gtoJSON x
+instance (forall t. GFromJSONK f (t ':&&: x))
+         => GFromJSONK (Exists k f) x where
+  gfromJSON = fmap Exists . gfromJSON
diff --git a/src/Generics/Kind/Derive/KFunctor.hs b/src/Generics/Kind/Derive/KFunctor.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/Kind/Derive/KFunctor.hs
@@ -0,0 +1,115 @@
+{-# language AllowAmbiguousTypes   #-}
+{-# language DataKinds             #-}
+{-# language FlexibleContexts      #-}
+{-# language FlexibleInstances     #-}
+{-# language GADTs                 #-}
+{-# language MultiParamTypeClasses #-}
+{-# language PolyKinds             #-}
+{-# language QuantifiedConstraints #-}
+{-# language RankNTypes            #-}
+{-# language ScopedTypeVariables   #-}
+{-# language TypeApplications      #-}
+{-# language TypeFamilies          #-}
+{-# language TypeOperators         #-}
+{-# language UndecidableInstances  #-}
+module Generics.Kind.Derive.KFunctor where
+
+import           Data.Kind
+import           Data.PolyKinded.Functor
+import           Data.Proxy
+
+import           Generics.Kind
+
+kfmapDefault :: forall k (f :: k) v as bs. (GenericK f, GenericK f, GFunctor (RepK f) v as bs)
+             => Mappings v as bs -> f :@@: as -> f :@@: bs
+kfmapDefault v = toK @k @f @bs . gfmap v . fromK @k @f @as
+
+fmapDefault' :: forall (f :: Type -> Type) a b.
+                (GenericK f, GenericK f,
+                 GFunctor (RepK f) '[ 'Co ] (a ':&&: 'LoT0) (b ':&&: 'LoT0))
+              => (a -> b) -> f a -> f b
+fmapDefault' f = kfmapDefault (f :^: M0 :: Mappings '[ 'Co ] (a ':&&: 'LoT0) (b ':&&: 'LoT0))
+
+class GFunctor (f :: LoT k -> Type) (v :: Variances) (as :: LoT k) (bs :: LoT k) where
+  gfmap :: Mappings v as bs -> f as -> f bs
+
+instance GFunctor U1 v as bs where
+  gfmap _ U1 = U1
+
+instance GFunctor f v as bs => GFunctor (M1 i c f) v as bs where
+  gfmap v (M1 x) = M1 (gfmap v x)
+
+instance (GFunctor f v as bs, GFunctor g v as bs)
+         => GFunctor (f :+: g) v as bs where
+  gfmap v (L1 x) = L1 (gfmap v x)
+  gfmap v (R1 x) = R1 (gfmap v x)
+
+instance (GFunctor f v as bs, GFunctor g v as bs)
+         => GFunctor (f :*: g) v as bs where
+  gfmap v (x :*: y) = gfmap v x :*: gfmap v y
+
+instance (Interpret c as => GFunctor f v as bs, {- Ty c as => -} Interpret c bs)
+         => GFunctor (c :=>: f) v as bs where
+  gfmap v (SuchThat x) = SuchThat (gfmap v x)
+
+instance forall f v as bs.
+         (forall (t :: Type). GFunctor f ('Co ': v) (t ':&&: as) (t ':&&: bs))
+         => GFunctor (Exists Type f) v as bs where
+  gfmap v (Exists (x :: f (t ':&&: x)))
+    = Exists (gfmap ((id :^: v) :: Mappings ('Co ': v) (t ':&&: as) (t ':&&: bs)) x)
+
+class GFunctorArg (t :: Atom d Type)
+                  (v :: Variances) (intended :: Variance)
+                  (as :: LoT d) (bs :: LoT d) where
+  gfmapf :: Proxy t -> Proxy intended
+         -> Mappings v as bs
+         -> Mapping intended (Interpret t as) (Interpret t bs)
+
+instance forall t v as bs. GFunctorArg t v 'Co as bs
+         => GFunctor (Field t) v as bs where
+  gfmap v (Field x) = Field (gfmapf (Proxy @t) (Proxy @'Co) v x)
+
+instance GFunctorArg ('Kon t) v 'Co as bs where
+  gfmapf _ _ _ = id
+instance GFunctorArg ('Kon t) v 'Contra as bs where
+  gfmapf _ _ _ = id
+
+instance forall d (f :: Atom (Type -> d) Type) v (as :: LoT d) (bs :: LoT d).
+         (forall (t :: Type). GFunctorArg f ('Co ': v) 'Co (t ':&&: as) (t ':&&: bs))
+         => GFunctorArg ('ForAll f) v 'Co as bs where
+  gfmapf _ _ v x = fromWrappedI $ go $ toWrappedI x
+    where
+      go :: forall (t :: Type). WrappedI f (t ':&&: as) -> WrappedI f (t ':&&: bs)
+      go (WrapI p) = WrapI (gfmapf @(Type -> d) @f @('Co ': v) @'Co @(t ':&&: as) @(t ':&&: bs)
+                           Proxy Proxy (id :^: v) p)
+
+instance GFunctorArg ('Var 'VZ) (r ': v) r (a ':&&: as) (b ':&&: bs) where
+  gfmapf _ _ (f :^: _) = f
+
+instance forall vr pre v intended a as b bs.
+         GFunctorArg ('Var vr) v intended as bs
+         => GFunctorArg ('Var ('VS vr)) (pre ': v) intended (a ':&&: as) (b ':&&: bs) where
+  gfmapf _ _ (_ :^: rest) = gfmapf (Proxy @('Var vr)) (Proxy @intended) rest
+
+instance forall f x v v1 as bs.
+         (KFunctor f '[v1] (Interpret x as ':&&: 'LoT0) (Interpret x bs ':&&: 'LoT0),
+          GFunctorArg x v v1 as bs)
+         => GFunctorArg (f :$: x) v 'Co as bs where
+  gfmapf _ _ v = kfmap (gfmapf (Proxy @x) (Proxy @v1) v :^: M0)
+
+instance forall f x y v v1 v2 as bs.
+         (KFunctor f '[v1, v2] (Interpret x as ':&&: Interpret y as ':&&: 'LoT0)
+                               (Interpret x bs ':&&: Interpret y bs ':&&: 'LoT0),
+          GFunctorArg x v v1 as bs, GFunctorArg y v v2 as bs)
+         => GFunctorArg (f :$: x ':@: y) v 'Co as bs where
+  gfmapf _ _ v = kfmap (gfmapf (Proxy @x) (Proxy @v1) v :^:
+                        gfmapf (Proxy @y) (Proxy @v2) v :^: M0)
+
+instance forall f x y z v v1 v2 v3 as bs.
+         (KFunctor f '[v1, v2, v3] (Interpret x as ':&&: Interpret y as ':&&: Interpret z as ':&&: 'LoT0)
+                                   (Interpret x bs ':&&: Interpret y bs ':&&: Interpret z bs ':&&: 'LoT0),
+          GFunctorArg x v v1 as bs, GFunctorArg y v v2 as bs, GFunctorArg z v v3 as bs)
+         => GFunctorArg (f :$: x ':@: y ':@: z) v 'Co as bs where
+  gfmapf _ _ v = kfmap (gfmapf (Proxy @x) (Proxy @v1) v :^:
+                        gfmapf (Proxy @y) (Proxy @v2) v :^:
+                        gfmapf (Proxy @z) (Proxy @v3) v :^: M0)
diff --git a/src/Generics/Kind/Derive/Traversable.hs b/src/Generics/Kind/Derive/Traversable.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/Kind/Derive/Traversable.hs
@@ -0,0 +1,99 @@
+{-# language AllowAmbiguousTypes   #-}
+{-# language DataKinds             #-}
+{-# language FlexibleContexts      #-}
+{-# language FlexibleInstances     #-}
+{-# language MultiParamTypeClasses #-}
+{-# language PolyKinds             #-}
+{-# language QuantifiedConstraints #-}
+{-# language ScopedTypeVariables   #-}
+{-# language TypeApplications      #-}
+{-# language TypeFamilies          #-}
+{-# language TypeOperators         #-}
+{-# language UndecidableInstances  #-}
+module Generics.Kind.Derive.Traversable where
+
+import           Data.Kind
+import           GHC.TypeLits
+import           Generics.Kind
+
+traverseDefaultPos :: forall v f as bs g.
+                      (GenericK f, GenericK f,
+                       GTraversable (RepK f) v as bs,
+                       Applicative g)
+                   => (Interpret ('Var v) as -> g (Interpret ('Var v) bs))
+                   -> f :@@: as -> g (f :@@: bs)
+traverseDefaultPos f = fmap (toK @_ @f @bs) . gtraverse @_ @(RepK f) @v @as @bs f . fromK @_ @f @as
+
+traverseDefault :: forall f a b g. (GenericK f, GenericK f,
+                   GTraversable (RepK f) 'VZ (LoT1 a) (LoT1 b), Applicative g)
+                => (a -> g b) -> f a -> g (f b)
+traverseDefault = traverseDefaultPos @'VZ @f @(LoT1 a) @(LoT1 b)
+
+class GTraversable (f :: LoT k -> Type) (v :: TyVar k Type)
+                   (as :: LoT k) (bs :: LoT k) where
+  gtraverse :: Applicative g
+            => (Interpret ('Var v) as -> g (Interpret ('Var v) bs))
+            -> f as -> g (f bs)
+
+instance GTraversable U1 v as bs where
+  gtraverse _ U1 = pure U1
+
+instance forall f v as bs i c. GTraversable f v as bs
+         => GTraversable (M1 i c f) v as bs where
+  gtraverse v (M1 x) = M1 <$> gtraverse @_ @f @v @as @bs v x
+
+instance forall f g v as bs. (GTraversable f v as bs, GTraversable g v as bs)
+         => GTraversable (f :+: g) v as bs where
+  gtraverse v (L1 x) = L1 <$> gtraverse @_ @f @v @as @bs v x
+  gtraverse v (R1 x) = R1 <$> gtraverse @_ @g @v @as @bs v x
+
+instance forall f g v as bs. (GTraversable f v as bs, GTraversable g v as bs)
+         => GTraversable (f :*: g) v as bs where
+  gtraverse v (x :*: y) = (:*:) <$> gtraverse @_ @f @v @as @bs v x
+                                <*> gtraverse @_ @g @v @as @bs v y
+
+instance forall c f v as bs z.
+         (Interpret c as => GTraversable f v as bs, z ~ Interpret c bs, Interpret c as => z)
+         => GTraversable (c :=>: f) v as bs where
+  gtraverse v (SuchThat x) = SuchThat <$> gtraverse @_ @f @v @as @bs v x
+
+instance forall k f v as bs.
+         (forall (t :: k). GTraversable f ('VS v) (t ':&&: as) (t ':&&: bs))
+         => GTraversable (Exists k f) v as bs where
+  gtraverse v (Exists (x :: f (t ':&&: x)))
+    = Exists <$> gtraverse @_ @f @('VS v) @(t ':&&: x) @(t ':&&: _) v x
+
+instance forall t v as bs. GTraversableArg t v as bs (ContainsTyVar v t)
+         => GTraversable (Field t) v as bs where
+  gtraverse v (Field x) = Field <$> gtraversef @_ @t @v @as @bs @(ContainsTyVar v t) v x
+
+class GTraversableArg (t :: Atom d Type) (v :: TyVar d Type)
+                      (as :: LoT d) (bs :: LoT d) (p :: Bool) where
+  gtraversef :: Applicative g
+             => (Interpret ('Var v) as -> g (Interpret ('Var v) bs))
+             -> Interpret t as -> g (Interpret t bs)
+
+instance (Interpret t as ~ Interpret t bs) => GTraversableArg t v as bs 'False where
+  gtraversef _ = pure
+
+instance TypeError ('Text "Should never get here")
+         => GTraversableArg ('Kon t) v as bs whatever where
+  gtraversef _ = pure
+
+instance ( Traversable (Interpret f as), Interpret f as ~ Interpret f bs
+         , GTraversableArg x v as bs (ContainsTyVar v x))
+         => GTraversableArg (f ':@: x) v as bs 'True where
+  gtraversef f x = traverse (gtraversef @_ @x @v @as @bs @(ContainsTyVar v x) f) x
+
+-- We found the same variable
+instance GTraversableArg ('Var 'VZ) 'VZ (a ':&&: as) (b ':&&: bs) 'True where
+  gtraversef f x = f x
+-- We need to keep looking
+instance forall d (v :: TyVar d Type) n r as s bs isthere.
+         GTraversableArg ('Var v) n as bs isthere
+         => GTraversableArg ('Var ('VS v)) ('VS n) (r ':&&: as) (s ':&&: bs) isthere where
+  gtraversef f x = gtraversef @d @('Var v) @n @as @bs @isthere f x
+-- If we arrive to another we do not want, keep it as it is
+instance TypeError ('Text "Should never get here")
+         => GTraversableArg ('Var 'VZ) ('VS n) (r ':&&: as) (r ':&&: bs) 'True where
+  gtraversef _ = pure