diff --git a/ChangeLog.md b/ChangeLog.md
new file mode 100644
--- /dev/null
+++ b/ChangeLog.md
@@ -0,0 +1,17 @@
+# Changelog for recursion-schemes-ix
+
+## 0.0.1.0
+
+Initial release
+
+Multiple last-minute changes:
+
+* Switched from `singletons` to `singlethongs`
+  - `singletons` has unnecessary dependencies, and is unable to compile
+    with the current `ghcjs` version.
+* Removed QuantifiedConstraints extension usage throughout
+  - Allowed the removal of UndecidableInstances in most files
+* Added the `ITraversable` class and monadic recursion-schemes
+  - TODO: determine if `IFunctor` should just be removed,
+    ie. determine if there are any `IFunctor`s that are not `ITraversable`
+
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright Skye Soss (c) 2020
+
+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 Author name here 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/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,38 @@
+
+# recursion-schemes-ix
+
+## Recursion schemes over indexed datatypes
+
+Heavily inspired by `multirec`, this library uses `PolyKinds`
+and `SingI` constraints to achieve the same dependent typing as `multirec`.
+
+This library defines the `IFunctor` typeclass and recursion-schemes
+on `IFunctor`s.
+
+Goals:
+* Minimal dependencies
+  - This library depends only on `singlethongs`, which in turn only depends
+    on `template-haskell`. As a result, it should be easy to include in
+    any project
+* GHCJS compatibility
+  - This package is used in a compiler that I want to be able to run in the
+    browser
+* Ease of use
+  - Once everything is set-up, writing a recursion-scheme should not be
+    overly complex (looking at you, `mulrirec`)
+
+Non-Goals:
+* Eliminating boilerplate
+  - This library requires hand-written `IShow`, `IRead`, `IEq`, `IOrd`, `ITraversable` instances.
+    I also recommend writing pattern synonyms to remove the `IFix` constructor.
+    Writing these can be a pain, but its only required once for the main data structure,
+    and one `IFunctor` instance whenever you write a dependent recursion-scheme.
+* Speed
+  - The code in the library mimics the `recurion-schemes` library almost directly,
+    simply lifting everything up from `*` to `k -> *`. In a future release,
+    `INLINE` pragmas will be added and possibly benchmarked.
+
+## Documentation
+
+Not written, but haddocks on the github user site.
+
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/recursion-schemes-ix.cabal b/recursion-schemes-ix.cabal
new file mode 100644
--- /dev/null
+++ b/recursion-schemes-ix.cabal
@@ -0,0 +1,71 @@
+cabal-version: 1.12
+
+-- This file has been generated from package.yaml by hpack version 0.31.2.
+--
+-- see: https://github.com/sol/hpack
+--
+-- hash: 20ec8e090059628c63cb93a58e4d0b51b601fbc74c1e66720dfae9482192e98b
+
+name:           recursion-schemes-ix
+version:        0.1.0.0
+synopsis:       Recursion schemes over indexed Functors
+description:    Please see the README on GitHub at <https://github.com/Skyb0rg007/recursion-schemes-ix#readme>
+category:       Data
+stability:      alpha
+homepage:       https://github.com/Skyb0rg007/recursion-schemes-ix#readme
+bug-reports:    https://github.com/Skyb0rg007/recursion-schemes-ix/issues
+author:         Skye Soss
+maintainer:     skyler.soss@gmail.com
+copyright:      2020 Skye Soss
+license:        BSD3
+license-file:   LICENSE
+tested-with:    GHC == 8.6.5 , GHC == 8.8.3 , GHC == 8.10.1 , GHCJS == 8.6.0.1
+build-type:     Simple
+extra-source-files:
+    README.md
+    ChangeLog.md
+
+source-repository head
+  type: git
+  location: https://github.com/Skyb0rg007/recursion-schemes-ix
+
+library
+  exposed-modules:
+      Data.IComonad
+      Data.IFunction
+      Data.IFunctor
+      Data.IFunctor.Classes
+      Data.IFunctor.Foldable
+      Data.IFunctor.ICofree
+      Data.IFunctor.IFree
+      Data.IFunctor.IIdentity
+      Data.IMonad
+      Data.ITraversable
+  other-modules:
+      Paths_recursion_schemes_ix
+  hs-source-dirs:
+      src
+  build-depends:
+      base >=4.12 && <4.15
+    , singlethongs ==0.1
+  default-language: Haskell2010
+
+test-suite recursion-schemes-ix-test
+  type: exitcode-stdio-1.0
+  main-is: Spec.hs
+  other-modules:
+      FibSpec
+      GRINSpec
+      Paths_recursion_schemes_ix
+  hs-source-dirs:
+      test
+  ghc-options: -threaded -rtsopts -with-rtsopts=-N
+  build-depends:
+      QuickCheck
+    , base >=4.12 && <4.15
+    , containers
+    , hspec
+    , mtl
+    , recursion-schemes-ix
+    , singlethongs ==0.1
+  default-language: Haskell2010
diff --git a/src/Data/IComonad.hs b/src/Data/IComonad.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/IComonad.hs
@@ -0,0 +1,28 @@
+{-# LANGUAGE PolyKinds     #-}
+{-# LANGUAGE RankNTypes    #-}
+{-# LANGUAGE TypeOperators #-}
+
+{-# OPTIONS_GHC -Wall -Wno-name-shadowing #-}
+
+module Data.IComonad
+    ( IComonad (..)
+    -- * Re-exports
+    , module Data.IFunctor
+    ) where
+
+import           Data.Functor.Product (Product (Pair))
+import           Data.IFunctor        (IFunctor (imap), type (~~>))
+
+-- | Comonoid in the category of dependent endofunctors
+class IFunctor f => IComonad f where
+    iextract :: f a ~~> a
+    iduplicate :: f a ~~> f (f a)
+    iduplicate = iextend id
+    iextend :: (f a ~~> b) -> (f a ~~> f b)
+    iextend f = imap f . iduplicate
+    {-# MINIMAL iextract, (iduplicate | iextend) #-}
+
+instance IComonad (Product a) where
+    iextract (Pair _ b) = b
+    iduplicate (Pair a b) = Pair a (Pair a b)
+
diff --git a/src/Data/IFunction.hs b/src/Data/IFunction.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/IFunction.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE PolyKinds     #-}
+{-# LANGUAGE RankNTypes    #-}
+{-# LANGUAGE TypeOperators #-}
+
+{-# OPTIONS_GHC -Wall -Wno-name-shadowing #-}
+
+module Data.IFunction
+    ( type (~~>)
+    ) where
+
+import           Singlethongs (SingI)
+
+infixr 4 ~~>
+
+-- | Indexed function type
+type a ~~> b = forall ix. SingI ix => a ix -> b ix
+
diff --git a/src/Data/IFunctor.hs b/src/Data/IFunctor.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/IFunctor.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE PolyKinds     #-}
+{-# LANGUAGE RankNTypes    #-}
+{-# LANGUAGE TypeOperators #-}
+
+{-# OPTIONS_GHC -Wall -Wno-name-shadowing #-}
+
+module Data.IFunctor
+    ( IFunctor (..)
+    -- * Re-exports
+    , module Data.IFunction
+    ) where
+
+import           Data.Functor.Product (Product (Pair))
+import           Data.Functor.Sum     (Sum (InL, InR))
+import           Data.IFunction       (type (~~>))
+
+-- | Functor in the category of dependent types
+class IFunctor f where
+    imap :: (a ~~> b) -> (f a ~~> f b)
+
+instance IFunctor (Sum a) where
+    imap _ (InL x) = InL x
+    imap f (InR x) = InR (f x)
+
+instance IFunctor (Product a) where
+    imap f (Pair a b) = Pair a (f b)
+
diff --git a/src/Data/IFunctor/Classes.hs b/src/Data/IFunctor/Classes.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/IFunctor/Classes.hs
@@ -0,0 +1,142 @@
+{-# LANGUAGE PolyKinds  #-}
+{-# LANGUAGE RankNTypes #-}
+
+{-# OPTIONS_GHC -Wall -Wno-name-shadowing #-}
+
+module Data.IFunctor.Classes
+    (
+    -- * Indexed Show
+      IShow (..)
+    , IShow2 (..)
+    , ishowsPrec1
+    , ishow1
+    -- * Indexed Read
+    , IRead (..)
+    , IRead2 (..)
+    , ireadPrec1
+    , ireadsPrec1
+    -- * Indexed Eq
+    , IEq (..)
+    , IEq2 (..)
+    , ieq1
+    -- * Indexed Ord
+    , IOrd (..)
+    , IOrd2 (..)
+    , icompare1
+    ) where
+
+import           Data.Functor.Product (Product (..))
+import           Data.Functor.Sum     (Sum (..))
+import           Singlethongs         (SingI)
+import           Text.Read
+
+class IShow f where
+    ishowsPrec :: SingI ix => (forall ix. SingI ix => Int -> a ix -> ShowS) -> Int -> f a ix -> ShowS
+    ishowsPrec sp _ x s = ishow sp x ++ s
+    ishow :: SingI ix => (forall ix. SingI ix => Int -> a ix -> ShowS) -> f a ix -> String
+    ishow sp x = ishowsPrec sp 0 x ""
+    {-# MINIMAL ishowsPrec | ishow #-}
+
+class IShow2 a where
+    ishowsPrec2 :: SingI ix => Int -> a ix -> ShowS
+    ishowsPrec2 _ x s = ishow2 x ++ s
+    ishow2 :: SingI ix => a ix -> String
+    ishow2 x = ishowsPrec2 0 x ""
+    {-# MINIMAL ishowsPrec2 | ishow2 #-}
+
+ishowsPrec1 :: (IShow f, IShow2 a, SingI ix) => Int -> f a ix -> ShowS
+ishowsPrec1 = ishowsPrec ishowsPrec2
+
+ishow1 :: (IShow f, IShow2 a, SingI ix) => f a ix -> String
+ishow1 = ishow ishowsPrec2
+
+class IRead f where
+    ireadPrec :: SingI ix => (forall ix. SingI ix => ReadPrec (a ix)) -> ReadPrec (f a ix)
+    ireadPrec rp = readS_to_Prec $ ireadsPrec (readPrec_to_S rp)
+    ireadsPrec :: SingI ix => (forall ix. SingI ix => Int -> ReadS (a ix)) -> Int -> ReadS (f a ix)
+    ireadsPrec rp = readPrec_to_S $ ireadPrec (readS_to_Prec rp)
+    {-# MINIMAL ireadPrec | ireadsPrec #-}
+
+class IRead2 a where
+    ireadPrec2 :: SingI ix => ReadPrec (a ix)
+    ireadPrec2 = readS_to_Prec $ ireadsPrec2
+    ireadsPrec2 :: SingI ix => Int -> ReadS (a ix)
+    ireadsPrec2 = readPrec_to_S $ ireadPrec2
+    {-# MINIMAL ireadPrec2 | ireadsPrec2 #-}
+
+ireadPrec1 :: (IRead f, IRead2 a, SingI ix) => ReadPrec (f a ix)
+ireadPrec1 = ireadPrec ireadPrec2
+
+ireadsPrec1 :: (IRead f, IRead2 a, SingI ix) => Int -> ReadS (f a ix)
+ireadsPrec1 = ireadsPrec ireadsPrec2
+
+class IEq f where
+    ieq :: SingI ix => (forall ix. SingI ix => a ix -> a ix -> Bool) -> f a ix -> f a ix -> Bool
+
+class IEq2 a where
+    ieq2 :: SingI ix => a ix -> a ix -> Bool
+
+ieq1 :: (IEq f, IEq2 a, SingI ix) => f a ix -> f a ix -> Bool
+ieq1 = ieq ieq2
+
+class IEq f => IOrd f where
+    icompare :: SingI ix => (forall ix. SingI ix => a ix -> a ix -> Ordering) -> f a ix -> f a ix -> Ordering
+
+class IEq2 a => IOrd2 a where
+    icompare2 :: SingI ix => a ix -> a ix -> Ordering
+
+icompare1 :: (IOrd f, IOrd2 a, SingI ix) => f a ix -> f a ix -> Ordering
+icompare1 = icompare icompare2
+
+-- * base instances
+
+-- Sum
+instance IShow2 a => IShow (Sum a) where
+    ishowsPrec _ p (InL x) = showParen (p > 10) $
+        showString "InL " . ishowsPrec2 11 x
+    ishowsPrec sp p (InR x) = showParen (p > 10) $
+        showString "InR " . sp 11 x
+
+instance IRead2 a => IRead (Sum a) where
+    ireadPrec rp = parens $
+        (prec 10 $ do
+            Ident "InL" <- lexP
+            x <- step ireadPrec2
+            pure $ InL x
+        )
+        +++
+        (prec 10 $ do
+            Ident "InR" <- lexP
+            x <- step rp
+            pure $ InR x
+        )
+
+instance IEq2 a => IEq (Sum a) where
+    ieq _  (InL x) (InL y) = ieq2 x y
+    ieq eq (InR x) (InR y) = eq x y
+    ieq _ _ _              = False
+
+instance IOrd2 a => IOrd (Sum a) where
+    icompare _ (InL x) (InL y)    = icompare2 x y
+    icompare comp (InR x) (InR y) = comp x y
+    icompare _ (InL _) (InR _)    = LT
+    icompare _ (InR _) (InL _)    = GT
+
+-- Product
+instance IShow2 a => IShow (Product a) where
+    ishowsPrec sp p (Pair a b) = showParen (p > 10) $
+        showString "Pair " . ishowsPrec2 11 a . showString " " . sp 11 b
+
+instance IRead2 a => IRead (Product a) where
+    ireadPrec rp = parens $ prec 10 $ do
+        Ident "Pair" <- lexP
+        x <- step ireadPrec2
+        y <- step rp
+        pure $ Pair x y
+
+instance IEq2 a => IEq (Product a) where
+    ieq eq (Pair a b) (Pair a' b') = ieq2 a a' && eq b b'
+
+instance IOrd2 a => IOrd (Product a) where
+    icompare comp (Pair a b) (Pair a' b') = icompare2 a a' <> comp b b'
+
diff --git a/src/Data/IFunctor/Foldable.hs b/src/Data/IFunctor/Foldable.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/IFunctor/Foldable.hs
@@ -0,0 +1,408 @@
+{-# LANGUAGE DataKinds            #-}
+{-# LANGUAGE DeriveDataTypeable   #-}
+{-# LANGUAGE DeriveGeneric        #-}
+{-# LANGUAGE LambdaCase           #-}
+{-# LANGUAGE PolyKinds            #-}
+{-# LANGUAGE RankNTypes           #-}
+{-# LANGUAGE ScopedTypeVariables  #-}
+{-# LANGUAGE TypeOperators        #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+{-# OPTIONS_GHC -Wall -Wno-name-shadowing #-}
+
+module Data.IFunctor.Foldable
+    (
+    -- * Fixpoint for indexed types
+      IFix (..)
+    -- * Morphisms
+    -- * Constructive morphisms
+    , cata
+    , prepro
+    , para
+    , zygo
+    , histo
+    -- * Destructive morphisms
+    , ana
+    , postpro
+    , apo
+    , gapo
+    , futu
+    -- * Combined morphisms
+    , hylo
+    , dyna
+    , chrono
+    , meta
+    , elgot
+    , coelgot
+    -- * Monadic morphisms
+    , cataM
+    , paraM
+    , anaM
+    , apoM
+    , hyloM
+    , dynaM
+    -- * Distribution Laws
+    , DistLaw
+    -- * Constructive distribution laws
+    , distCata
+    , distPara
+    , distZygo
+    , distHisto
+    -- * Destructive distribution laws
+    , distAna
+    , distApo
+    , distGApo
+    , distFutu
+    -- * Generalized morphisms
+    , gfold
+    , gunfold
+    , ghylo
+    , gprepro
+    , gpostpro
+    -- * Generalized monadic morphisms
+    , gfoldM
+    , gunfoldM
+    , ghyloM
+    -- * Re-exports
+    , module Data.Functor.Const
+    , module Data.Functor.Product
+    , module Data.Functor.Sum
+    , module Data.IComonad
+    , module Data.IFunction
+    , module Data.IFunctor
+    , module Data.IFunctor.Classes
+    , module Data.IFunctor.ICofree
+    , module Data.IFunctor.IFree
+    , module Data.IFunctor.IIdentity
+    , module Data.IMonad
+    , module Data.ITraversable
+    , module Singlethongs
+    ) where
+
+import           Control.Monad           ((<=<))
+import           Data.Functor.Const      (Const (..))
+import           Data.Functor.Product    (Product (..))
+import           Data.Functor.Sum        (Sum (..))
+import           Data.IComonad           (IComonad (..))
+import           Data.IFunction          (type (~~>))
+import           Data.IFunctor           (IFunctor (..))
+import           Data.IFunctor.Classes
+import           Data.IFunctor.ICofree   (ICofree (..))
+import           Data.IFunctor.IFree     (IFree (..))
+import           Data.IFunctor.IIdentity (IIdentity (..))
+import           Data.IMonad             (IMonad (..))
+import           Data.ITraversable       (ITraversable (..), imapDefault)
+import           Data.Typeable           (Typeable)
+import           GHC.Generics            (Generic, Generic1)
+import           Singlethongs            (SingI (sing))
+import           Text.Read
+
+-- | Fixpoint type
+newtype IFix f ix = IFix { unIFix :: f (IFix f) ix }
+    deriving (Typeable, Generic, Generic1)
+
+instance (IShow f, SingI ix) => Show (IFix f ix) where
+    showsPrec p (IFix x) = showParen (p > 10) $
+        showString "IFix " .  ishowsPrec showsPrec 11 x
+
+instance (IRead f, SingI ix) => Read (IFix f ix) where
+    readPrec = parens $ prec 10 $ do
+        Ident "IFix" <- lexP
+        x <- step $ ireadPrec readPrec
+        pure $ IFix x
+
+instance (IEq f, SingI ix) => Eq (IFix f ix) where
+    IFix x == IFix y = ieq (==) x y
+
+instance (IOrd f, SingI ix) => Ord (IFix f ix) where
+    IFix x `compare` IFix y = icompare compare x y
+
+-- * Morphisms
+
+-- | Catamorphism, ie. fold
+cata :: IFunctor f
+     => (f a ~~> a)
+     -> (IFix f ~~> a)
+cata f = gfold distCata (f . imap runIIdentity)
+
+-- | Fokkinga's prepromorphism
+prepro :: IFunctor f
+       => (forall b. f b ~~> f b)
+       -> (f a ~~> a)
+       -> (IFix f ~~> a)
+prepro e f = gprepro distCata e (f . imap runIIdentity)
+
+-- | Paramorphism
+para :: IFunctor f
+     => (f (Product (IFix f) a) ~~> a)
+     -> (IFix f ~~> a)
+para = gfold distPara
+
+-- | Zygomorphism
+zygo :: IFunctor f
+     => (f b ~~> b)
+     -> (f (Product b a) ~~> a)
+     -> (IFix f ~~> a)
+zygo f = gfold (distZygo f)
+
+-- | Histomorphism
+histo :: IFunctor f
+      => (f (ICofree f a) ~~> a)
+      -> (IFix f ~~> a)
+histo = gfold distHisto
+
+-- | Anamorphism, ie. unfold
+ana :: IFunctor f
+    => (a ~~> f a)
+    -> (a ~~> IFix f)
+ana g = gunfold distAna (imap IIdentity . g)
+
+-- | Fokkinga's postpromorphism
+postpro :: IFunctor f
+        => (forall b. f b ~~> f b)
+        -> (a ~~> f a)
+        -> (a ~~> IFix f)
+postpro e g = gpostpro distAna e (imap IIdentity . g)
+
+-- | Apomorphism
+apo :: IFunctor f
+    => (a ~~> f (Sum (IFix f) a))
+    -> (a ~~> IFix f)
+apo = gunfold distApo
+
+-- | GApomorphism
+gapo :: IFunctor f
+     => (b ~~> f b)
+     -> (a ~~> f (Sum b a))
+     -> (a ~~> IFix f)
+gapo f = gunfold (distGApo f)
+
+-- | Futumorphism
+futu :: IFunctor f
+     => (a ~~> f (IFree f a))
+     -> (a ~~> IFix f)
+futu = gunfold distFutu
+
+-- | Hylomorphism, fold then unfold
+hylo :: IFunctor f
+     => (f b ~~> b)
+     -> (a ~~> f a)
+     -> (a ~~> b)
+hylo f g = ghylo distCata distAna (f . imap runIIdentity) (imap IIdentity . g)
+
+-- | Dynamorphism
+dyna :: IFunctor f
+     => (f (ICofree f b) ~~> b)
+     -> (a ~~> f a)
+     -> (a ~~> b)
+dyna f g = ghylo distHisto distAna f (imap IIdentity . g)
+
+-- | Chronomorphism
+chrono :: IFunctor f
+       => (f (ICofree f b) ~~> b)
+       -> (a ~~> f (IFree f a))
+       -> (a ~~> b)
+chrono = ghylo distHisto distFutu
+
+-- | Metamorphism
+-- TODO: ensure only 1 pass over structure
+meta :: (IFunctor f, IFunctor g)
+     => (f a ~~> a)
+     -> (a ~~> b)
+     -> (b ~~> g b)
+     -> (IFix f ~~> IFix g)
+meta f e g = ana g . e . cata f
+
+-- * Elgot algebras
+
+elgot :: forall f a b. IFunctor f
+      => (f a ~~> a)
+      -> (b ~~> Sum a (f b))
+      -> (b ~~> a)
+elgot phi psi = h
+    where
+        h :: b ~~> a
+        h = (id `sum` (phi . imap h)) . psi
+        sum :: forall a b c. (a ~~> c) -> (b ~~> c) -> (Sum a b ~~> c)
+        sum f _ (InL x) = f x
+        sum _ g (InR x) = g x
+
+coelgot :: forall f a b. IFunctor f
+        => (Product a (f b) ~~> b)
+        -> (a ~~> f a)
+        -> (a ~~> b)
+coelgot phi psi = h
+    where
+        h :: a ~~> b
+        h = phi . (id `product` (imap h . psi))
+        product :: forall a b c. (a ~~> b) -> (a ~~> c) -> (a ~~> Product b c)
+        product f g x = Pair (f x) (g x)
+
+
+-- * Monadic morphisms
+
+-- | Monadic catamorphism
+cataM :: (ITraversable f, Monad m)
+      => (forall ix. SingI ix => f a ix -> m (a ix))
+      -> (forall ix. SingI ix => IFix f ix -> m (a ix))
+cataM f = gfoldM distCata (f . imap runIIdentity)
+
+-- | Monadic Paramorphism
+paraM :: (ITraversable f, Monad m)
+      => (forall ix. SingI ix => f (Product (IFix f) a) ix -> m (a ix))
+      -> (forall ix. SingI ix => IFix f ix -> m (a ix))
+paraM = gfoldM distPara
+
+-- | Monadic anamorphism
+anaM :: (ITraversable f, Monad m)
+     => (forall ix. SingI ix => a ix -> m (f a ix))
+     -> (forall ix. SingI ix => a ix -> m (IFix f ix))
+anaM g = gunfoldM distAna (fmap (imap IIdentity) . g)
+
+-- | Monadic apomorphism
+apoM :: (ITraversable f, Monad m)
+     => (forall ix. SingI ix => a ix -> m (f (Sum (IFix f) a) ix))
+     -> (forall ix. SingI ix => a ix -> m (IFix f ix))
+apoM = gunfoldM distApo
+
+-- | Monadic hylomorphism
+hyloM :: (ITraversable f, Monad m)
+     => (forall ix. SingI ix => f b ix -> m (b ix))
+     -> (forall ix. SingI ix => a ix -> m (f a ix))
+     -> (forall ix. SingI ix => a ix -> m (b ix))
+hyloM f g = ghyloM distCata distAna (f . imap runIIdentity) (fmap (imap IIdentity) . g)
+
+-- | Monadic dynamorphism
+dynaM :: (ITraversable f, Monad m)
+      => (forall ix. SingI ix => f (ICofree f b) ix -> m (b ix))
+      -> (forall ix. SingI ix => a ix -> m (f a ix))
+      -> (forall ix. SingI ix => a ix -> m (b ix))
+dynaM f g = ghyloM distHisto distAna f (fmap (imap IIdentity) . g)
+
+-- * Distribution laws
+
+-- | Type of distribution laws
+-- A Constructive morphism means the second part is a 'IComonad'
+-- A Destructive morphism means the first part is an 'IMonad'
+type DistLaw f g = forall a. f (g a) ~~> g (f a)
+
+-- * Constructive distribution laws
+
+distCata :: IFunctor f => DistLaw f IIdentity
+distCata = IIdentity . imap runIIdentity
+
+distPara :: IFunctor f => DistLaw f (Product (IFix f))
+distPara = distZygo IFix
+
+distZygo :: IFunctor f => (f b ~~> b) -> DistLaw f (Product b)
+distZygo g m = Pair (g (imap (\(Pair a _) -> a) m)) (imap (\(Pair _ b) -> b) m)
+
+distHisto :: IFunctor f => DistLaw f (ICofree f)
+distHisto x = imap (\(a ::< _) -> a) x ::< imap (\(_ ::< x) -> distHisto x) x
+
+-- * Destructive distribution laws
+
+distAna :: IFunctor f => DistLaw IIdentity f
+distAna = imap IIdentity . runIIdentity
+
+distApo :: IFunctor f => DistLaw (Sum (IFix f)) f
+distApo = distGApo unIFix
+
+distGApo :: IFunctor f => (b ~~> f b) -> DistLaw (Sum b) f
+distGApo f (InL x) = imap InL $ f x
+distGApo _ (InR x) = imap InR x
+
+distFutu :: IFunctor f => DistLaw (IFree f) f
+distFutu (IPure x) = imap IPure x
+distFutu (IFree x) = imap (IFree . distFutu) x
+
+-- * Generalized combinators
+
+-- | Generalized fold
+gfold :: forall f w a. (IFunctor f, IComonad w)
+      => DistLaw f w
+      -> (f (w a) ~~> a)
+      -> (IFix f ~~> a)
+gfold k g = g . iextract . c
+    where
+        c :: IFix f ~~> w (f (w a))
+        c = k . imap (iduplicate . imap g . c) . unIFix
+
+-- | Generalized unfold
+gunfold :: forall f m a. (IFunctor f, IMonad m)
+        => DistLaw m f
+        -> (a ~~> f (m a))
+        -> (a ~~> IFix f)
+gunfold k f = a . ipure . f
+    where
+        a :: m (f (m a)) ~~> IFix f
+        a = IFix . imap (a . imap f . ijoin) . k
+
+-- | Generalized hylomorphism
+ghylo :: forall f w m a b. (IFunctor f, IComonad w, IMonad m)
+      => DistLaw f w
+      -> DistLaw m f
+      -> f (w b) ~~> b
+      -> a ~~> f (m a)
+      -> a ~~> b
+ghylo w m f g = iextract . h . ipure
+    where
+        h :: m a ~~> w b
+        h = imap f . w . imap (iduplicate . h . ijoin) . m . imap g
+
+-- | Generalized monadic fold
+gfoldM :: forall f w m a. (ITraversable f, ITraversable w, IComonad w, Monad m)
+       => DistLaw f w
+       -> (forall ix. SingI ix => f (w a) ix -> m (a ix))
+       -> (forall ix. SingI ix => IFix f ix -> m (a ix))
+gfoldM k g = g . iextract <=< c
+    where
+        c :: forall ix. SingI ix => IFix f ix -> m (w (f (w a)) ix)
+        c = fmap k . itraverse (fmap iduplicate . itraverse g <=< c) . unIFix
+
+-- | Generalized monadic unfold
+gunfoldM :: forall f m a x. (ITraversable f, ITraversable m, IMonad m, Monad x)
+         => DistLaw m f
+         -> (forall ix. SingI ix => a ix -> x (f (m a) ix))
+         -> (forall ix. SingI ix => a ix -> x (IFix f ix))
+gunfoldM k f = a . ipure <=< f
+    where
+        a :: SingI ix => m (f (m a)) ix -> x (IFix f ix)
+        a = fmap IFix . itraverse (a <=< itraverse f . ijoin) . k
+
+-- | Generalized monadic hylomorphism
+ghyloM :: forall f w m a b x. (ITraversable f, ITraversable w, ITraversable m, IComonad w, IMonad m, Monad x)
+       => DistLaw f w
+       -> DistLaw m f
+       -> (forall ix. SingI ix => f (w b) ix -> x (b ix))
+       -> (forall ix. SingI ix => a ix -> x (f (m a) ix))
+       -> (forall ix. SingI ix => a ix -> x (b ix))
+ghyloM w m f g = fmap iextract . h . ipure
+    where
+        h :: SingI ix => m a ix -> x (w b ix)
+        h = itraverse f <=< fmap w . itraverse (fmap iduplicate . h . ijoin) . m <=< itraverse g
+
+-- | Generalized prepromorphism
+gprepro :: forall f w a. (IFunctor f, IComonad w)
+        => DistLaw f w
+        -> (forall c. f c ~~> f c)
+        -> (f (w a) ~~> a)
+        -> (IFix f ~~> a)
+gprepro k e f = iextract . c
+    where
+        c :: IFix f ~~> w a
+        c = imap f . k . imap (iduplicate . c . cata (IFix . e)) . unIFix
+
+-- | Generalized postpromorphism
+gpostpro :: forall f m a. (IFunctor f, IMonad m)
+         => DistLaw m f
+         -> (forall c. f c ~~> f c)
+         -> (a ~~> f (m a))
+         -> (a ~~> IFix f)
+gpostpro k e g = a . ipure
+    where
+        a :: m a ~~> IFix f
+        a = IFix . imap (cata (IFix . e) . a . ijoin) . k . imap g
+
+
+
diff --git a/src/Data/IFunctor/ICofree.hs b/src/Data/IFunctor/ICofree.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/IFunctor/ICofree.hs
@@ -0,0 +1,68 @@
+{-# LANGUAGE DeriveDataTypeable    #-}
+{-# LANGUAGE DeriveGeneric         #-}
+{-# LANGUAGE PolyKinds             #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE UndecidableInstances  #-}
+
+{-# OPTIONS_GHC -Wall -Wno-name-shadowing #-}
+
+module Data.IFunctor.ICofree
+    ( ICofree (..)
+    ) where
+
+import           Data.IComonad         (IComonad (..))
+import           Data.IFunctor         (IFunctor (..))
+import           Data.IFunctor.Classes
+import           Data.ITraversable     (ITraversable (..))
+import           Data.Typeable         (Typeable)
+import           GHC.Generics          (Generic, Generic1)
+import           Singlethongs          (SingI)
+import           Text.Read
+
+infixr 5 ::<
+
+-- | Cofree IComonad
+data ICofree f a ix = a ix ::< f (ICofree f a) ix
+    deriving (Typeable, Generic, Generic1)
+
+instance IFunctor f => IFunctor (ICofree f) where
+    imap f (a ::< x) = f a ::< imap (imap f) x
+
+instance ITraversable f => ITraversable (ICofree f) where
+    itraverse f (a ::< x) = (::<) <$> f a <*> itraverse (itraverse f) x
+
+instance IFunctor f => IComonad (ICofree f) where
+    iextract (a ::< _) = a
+    iduplicate (a ::< x) = (a ::< x) ::< imap iduplicate x
+    iextend f (a ::< x) = f (a ::< x) ::< imap (iextend f) x
+
+instance IShow f => IShow (ICofree f) where
+    ishowsPrec sp p (a ::< x) = showParen (p > 5) $
+        sp 6 a . showString " ::< " . ishowsPrec (ishowsPrec sp) 6 x
+
+instance IRead f => IRead (ICofree f) where
+    ireadPrec rp = parens $ prec 5 $ do
+        a <- step rp
+        Symbol "::<" <- lexP
+        x <- step (ireadPrec (ireadPrec rp))
+        pure (a ::< x)
+
+instance IEq f => IEq (ICofree f) where
+    ieq eq (a ::< x) (a' ::< x') = eq a a' && ieq (ieq eq) x x'
+
+instance IOrd f => IOrd (ICofree f) where
+    icompare comp (a ::< x) (a' ::< x') = comp a a' <> icompare (icompare comp) x x'
+
+instance (IShow f, IShow2 a, SingI ix) => Show (ICofree f a ix) where
+    showsPrec = ishowsPrec1
+
+instance (IRead f, IRead2 a, SingI ix) => Read (ICofree f a ix) where
+    readPrec = ireadPrec1
+
+instance (IEq f, IEq2 a, SingI ix) => Eq (ICofree f a ix) where
+    (==) = ieq1
+
+instance (IOrd f, IOrd2 a, SingI ix) => Ord (ICofree f a ix) where
+    compare = icompare1
diff --git a/src/Data/IFunctor/IFree.hs b/src/Data/IFunctor/IFree.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/IFunctor/IFree.hs
@@ -0,0 +1,87 @@
+{-# LANGUAGE DeriveDataTypeable    #-}
+{-# LANGUAGE DeriveGeneric         #-}
+{-# LANGUAGE PolyKinds             #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE UndecidableInstances  #-}
+
+{-# OPTIONS_GHC -Wall -Wno-name-shadowing #-}
+
+module Data.IFunctor.IFree
+    ( IFree (..)
+    ) where
+
+import           Data.IFunctor         (IFunctor (..))
+import           Data.IFunctor.Classes
+import           Data.IMonad           (IMonad (..))
+import           Data.ITraversable     (ITraversable (..))
+import           Data.Typeable         (Typeable)
+import           GHC.Generics          (Generic, Generic1)
+import           Singlethongs          (SingI)
+import           Text.Read
+
+-- | Free IMonad
+data IFree f a ix = IPure (a ix)
+    | IFree (f (IFree f a) ix)
+    deriving (Typeable, Generic, Generic1)
+
+instance IFunctor f => IFunctor (IFree f) where
+    imap f (IPure x) = IPure (f x)
+    imap f (IFree x) = IFree (imap (imap f) x)
+
+instance ITraversable f => ITraversable (IFree f) where
+    itraverse f (IPure x) = IPure <$> f x
+    itraverse f (IFree x) = IFree <$> itraverse (itraverse f) x
+
+instance IFunctor f => IMonad (IFree f) where
+    ipure = IPure
+    ijoin (IPure x) = x
+    ijoin (IFree x) = IFree $ imap ijoin x
+    ibind f (IPure x) = f x
+    ibind f (IFree x) = IFree $ imap (ibind f) x
+
+instance IShow f => IShow (IFree f) where
+    ishowsPrec sp p (IPure x) = showParen (p > 10) $
+        showString "IPure " . sp 11 x
+    ishowsPrec sp p (IFree x) = showParen (p > 10) $
+        showString "IFree " . (ishowsPrec (ishowsPrec sp)) 11 x
+
+instance IRead f => IRead (IFree f) where
+    ireadPrec rp = parens $
+        (prec 10 $ do
+            Ident "IPure" <- lexP
+            x <- step rp
+            pure $ IPure x
+        )
+        +++
+        (prec 10 $ do
+            Ident "IFree" <- lexP
+            x <- step (ireadPrec (ireadPrec rp))
+            pure $ IFree x
+        )
+
+instance IEq f => IEq (IFree f) where
+    ieq eq (IPure x) (IPure y) = eq x y
+    ieq eq (IFree x) (IFree y) = ieq (ieq eq) x y
+    ieq _ _ _                  = False
+
+instance IOrd f => IOrd (IFree f) where
+    icompare comp (IPure x) (IPure y) = comp x y
+    icompare comp (IFree x) (IFree y) = icompare (icompare comp) x y
+    icompare _ (IPure _) (IFree _)    = LT
+    icompare _ (IFree _) (IPure _)    = GT
+
+instance (IShow f, IShow2 a, SingI ix) => Show (IFree f a ix) where
+    showsPrec = ishowsPrec1
+
+instance (IRead f, IRead2 a, SingI ix) => Read (IFree f a ix) where
+    readPrec = ireadPrec1
+
+instance (IEq f, IEq2 a, SingI ix) => Eq (IFree f a ix) where
+    (==) = ieq1
+
+instance (IOrd f, IOrd2 a, SingI ix) => Ord (IFree f a ix) where
+    compare = icompare1
+
+
diff --git a/src/Data/IFunctor/IIdentity.hs b/src/Data/IFunctor/IIdentity.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/IFunctor/IIdentity.hs
@@ -0,0 +1,72 @@
+{-# LANGUAGE DeriveDataTypeable    #-}
+{-# LANGUAGE DeriveGeneric         #-}
+{-# LANGUAGE PolyKinds             #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE TypeOperators         #-}
+
+{-# OPTIONS_GHC -Wall -Wno-name-shadowing #-}
+
+module Data.IFunctor.IIdentity
+    ( IIdentity (IIdentity, runIIdentity)
+    ) where
+
+import           Data.Data             (Data)
+import           Data.Function         (on)
+import           Data.IComonad         (IComonad (..))
+import           Data.IFunctor         (IFunctor (..))
+import           Data.IFunctor.Classes
+import           Data.IMonad           (IMonad (..))
+import           Data.ITraversable     (ITraversable (..))
+import           Data.Typeable         (Typeable)
+import           GHC.Generics          (Generic, Generic1)
+import           Singlethongs          (SingI)
+import           Text.Read
+
+data IIdentity f ix = IIdentity
+    { runIIdentity :: f ix
+    }
+    deriving (Typeable, Data, Generic, Generic1)
+
+instance IFunctor IIdentity where
+    imap f = IIdentity . f . runIIdentity
+
+instance IMonad IIdentity where
+    ipure = IIdentity
+    ijoin = runIIdentity
+
+instance IComonad IIdentity where
+    iextract = runIIdentity
+    iduplicate = IIdentity
+
+instance ITraversable IIdentity where
+    itraverse f = fmap IIdentity . f . runIIdentity
+
+instance IShow IIdentity where
+    ishowsPrec sp p (IIdentity x) = showParen (p > 10) $
+        showString "IIdentity " . sp p x
+
+instance IRead IIdentity where
+    ireadPrec rp = parens $ prec 10 $ do
+        Ident "IIdentity" <- lexP
+        x <- step rp
+        pure $ IIdentity x
+
+instance IEq IIdentity where
+    ieq eq = eq `on` runIIdentity
+
+instance IOrd IIdentity where
+    icompare comp = comp `on` runIIdentity
+
+instance (IShow2 f, SingI ix) => Show (IIdentity f ix) where
+    showsPrec = ishowsPrec1
+
+instance (IRead2 f, SingI ix) => Read (IIdentity f ix) where
+    readPrec = ireadPrec1
+
+instance (IEq2 f, SingI ix) => Eq (IIdentity f ix) where
+    (==) = ieq1
+
+instance (IOrd2 f, SingI ix) => Ord (IIdentity f ix) where
+    compare = icompare1
+
diff --git a/src/Data/IMonad.hs b/src/Data/IMonad.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/IMonad.hs
@@ -0,0 +1,28 @@
+{-# LANGUAGE PolyKinds     #-}
+{-# LANGUAGE RankNTypes    #-}
+{-# LANGUAGE TypeOperators #-}
+
+{-# OPTIONS_GHC -Wall -Wno-name-shadowing #-}
+
+module Data.IMonad
+    ( IMonad (..)
+    -- * Re-exports
+    , module Data.IFunctor
+    ) where
+
+import           Data.Functor.Sum (Sum (InL, InR))
+import           Data.IFunctor    (IFunctor (imap), type (~~>))
+
+class IFunctor f => IMonad f where
+    ipure :: a ~~> f a
+    ijoin :: f (f a) ~~> f a
+    ijoin = ibind id
+    ibind :: (a ~~> f b) -> (f a ~~> f b)
+    ibind f = ijoin . imap f
+    {-# MINIMAL ipure, (ijoin | ibind) #-}
+
+instance IMonad (Sum a) where
+    ipure = InR
+    ijoin (InL x) = InL x
+    ijoin (InR x) = x
+
diff --git a/src/Data/ITraversable.hs b/src/Data/ITraversable.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/ITraversable.hs
@@ -0,0 +1,38 @@
+{-# LANGUAGE PolyKinds     #-}
+{-# LANGUAGE RankNTypes    #-}
+{-# LANGUAGE TypeOperators #-}
+
+{-# OPTIONS_GHC -Wall -Wno-name-shadowing #-}
+
+module Data.ITraversable
+    ( ITraversable (..)
+    , imapDefault
+    -- * Re-exports
+    , module Data.IFunctor
+    ) where
+
+import           Data.Functor.Identity (Identity (Identity, runIdentity))
+import           Data.Functor.Product  (Product (Pair))
+import           Data.Functor.Sum      (Sum (InL, InR))
+import           Data.IFunctor
+import           Singlethongs          (SingI)
+
+class IFunctor f => ITraversable f where
+    itraverse :: (Applicative m, SingI ix)
+              => (forall ix. SingI ix => a ix -> m (b ix))
+              -> f a ix
+              -> m (f b ix)
+
+-- | Default 'imap' for deriving 'IFunctor'
+imapDefault :: ITraversable f
+            => (a ~~> b)
+            -> (f a ~~> f b)
+imapDefault f = runIdentity . itraverse (Identity . f)
+
+instance ITraversable (Sum a) where
+    itraverse _ (InL x) = pure $ InL x
+    itraverse f (InR x) = InR <$> f x
+
+instance ITraversable (Product a) where
+    itraverse f (Pair a b) = Pair a <$> f b
+
diff --git a/test/FibSpec.hs b/test/FibSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/FibSpec.hs
@@ -0,0 +1,71 @@
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE DeriveDataTypeable    #-}
+{-# LANGUAGE DeriveGeneric         #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE InstanceSigs          #-}
+{-# LANGUAGE KindSignatures        #-}
+{-# LANGUAGE LambdaCase            #-}
+{-# LANGUAGE NoStarIsType          #-}
+{-# LANGUAGE PatternSynonyms       #-}
+{-# LANGUAGE PolyKinds             #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE StandaloneDeriving    #-}
+{-# LANGUAGE TemplateHaskell       #-}
+{-# LANGUAGE TypeApplications      #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE TypeOperators         #-}
+
+module FibSpec (main, spec) where
+
+import           Data.IFunctor.Foldable
+import           Data.Kind               (Type)
+import           Singlethongs
+import           Test.Hspec
+import           Test.QuickCheck
+
+data PeanoIdx = PeanoIdx
+singlethongs ''PeanoIdx
+
+main :: IO ()
+main = hspec spec
+
+spec :: Spec
+spec =
+    describe "fib using 'dyna'" $ do
+        it "fibs" $
+            map fib [1 .. 8]
+            `shouldBe`
+            [1, 1, 2, 3, 5, 8, 13, 21]
+
+fib :: Integer -> Integer
+fib = getConst . fib' . Const
+    where
+        fib' :: Const Integer 'PeanoIdx -> Const Integer 'PeanoIdx
+        fib' = dyna folder builder
+        folder :: forall ix. SingI ix
+               => PeanoF (ICofree PeanoF (Const Integer)) ix
+               -> Const Integer ix
+        folder OneF                            = 1
+        folder (SuccF (_ ::< OneF))            = 1
+        folder (SuccF (a ::< SuccF (b ::< _))) = a + b
+        builder :: forall ix. SingI ix
+                => Const Integer ix
+                -> PeanoF (Const Integer) ix
+        builder n =
+          case sing :: Sing ix of
+            SPeanoIdx ->
+              if n <= 1
+                then OneF
+                else SuccF (n - 1)
+
+data PeanoF f ix where
+    OneF  :: PeanoF f 'PeanoIdx
+    SuccF :: f 'PeanoIdx -> PeanoF f 'PeanoIdx
+
+instance IFunctor PeanoF where
+    imap _ OneF      = OneF
+    imap f (SuccF x) = SuccF (f x)
+
+
diff --git a/test/GRINSpec.hs b/test/GRINSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/GRINSpec.hs
@@ -0,0 +1,243 @@
+{-# LANGUAGE DataKinds           #-}
+{-# LANGUAGE GADTs               #-}
+{-# LANGUAGE InstanceSigs        #-}
+{-# LANGUAGE LambdaCase          #-}
+{-# LANGUAGE PolyKinds           #-}
+{-# LANGUAGE RankNTypes          #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell     #-}
+{-# LANGUAGE TypeApplications    #-}
+{-# LANGUAGE TypeFamilies        #-}
+{-# LANGUAGE TypeOperators       #-}
+
+module GRINSpec (main, spec) where
+
+import           Control.Monad.State
+import           Data.IFunctor.Foldable
+import           Data.Map               (Map)
+import qualified Data.Map               as Map
+import           Data.Set               (Set)
+import qualified Data.Set               as Set
+import           Singlethongs
+import           Test.Hspec
+import           Test.QuickCheck
+import           Text.Show              (showListWith)
+
+data ASTIdx = Exp | SimpleExp | Alt | Program | Def
+singlethongs ''ASTIdx
+
+main :: IO ()
+main = hspec spec
+
+spec :: Spec
+spec = do
+    describe "lorem ipsum" $ do
+        it "asdf" $
+            1 `shouldBe` 1
+    describe "Show instance for IFix" $ do
+        it "is correct" $
+            show (IFix $ ProgramF [] [IFix $ DefF "foo" [] $ IFix $ ESimpleF $ IFix $ SReturnF $ VSimple $ SVVar "x"])
+            `shouldBe`
+            "IFix (ProgramF [] [IFix (DefF \"foo\" [] (IFix (ESimpleF (IFix (SReturnF (VSimple (SVVar \"x\")))))))])"
+
+type Name = String
+
+data External = External
+    { externalName      :: Name
+    , externalEffectful :: Bool
+    -- other fields elided
+    }
+    deriving (Show, Read, Eq, Ord)
+
+data Lit = LInt Int
+    | LBool Bool
+    deriving (Show, Read, Eq, Ord)
+
+data Val = VTag Name [SimpleVal]
+    | VSimple SimpleVal
+    deriving (Show, Read, Eq, Ord)
+
+data SimpleVal = SVLit Lit
+    | SVVar Name
+    deriving (Show, Read, Eq, Ord)
+
+data LPat = LPTag Name [Name]
+    | LPUnit
+    deriving (Show, Read, Eq, Ord)
+
+data CPat = CPTag Name [Name]
+    | CPLit Lit
+    | CPDefault
+    deriving (Show, Read, Eq, Ord)
+
+{- Original GRIN datatype
+
+data 'Exp
+  = Program     [External] [Def]
+  | Def         Name [Name] 'Exp
+  -- 'Exp
+  | EBind       SimpleExp LPat 'Exp
+  | ECase       Val [Alt]
+  -- Simple 'Exp
+  | SApp        Name [SimpleVal]
+  | SReturn     Val
+  | SStore      Val
+  | SFetch      Name
+  | SUpdate     Name Val
+  | SBlock      'Exp
+  -- Alt
+  | Alt CPat 'Exp
+
+type SimpleExp = 'Exp
+type Alt = 'Exp
+type Def = 'Exp
+type Program = 'Exp
+
+-}
+
+{- What it really should be
+
+data Program = Program [External] [Def]
+
+data Def = Def Name [Name] 'Exp
+
+data 'Exp
+    = EBind SimpleExp LPat 'Exp
+    | ECase Val [Alt]
+    | ESimple SimpleExp
+
+data SimpleExp
+    = SApp Name [SimpleVal]
+    | SReturn Val
+    | SStore Val
+    | SFetch Name
+    | SUpdate Name Val
+    -- | SBlock 'Exp
+
+data Alt = Alt CPat 'Exp
+
+-}
+
+-- recursion-schemes-ix version
+
+data AST (f :: ASTIdx -> *) (ix :: ASTIdx) where
+    -- Program
+    ProgramF :: [External] -> [f 'Def] -> AST f 'Program
+    -- Def
+    DefF :: Name -> [Name] -> f 'Exp -> AST f 'Def
+    -- Exp
+    EBindF :: f 'SimpleExp -> LPat -> f 'Exp -> AST f 'Exp
+    ECaseF :: Val -> [f 'Alt] -> AST f 'Exp
+    ESimpleF :: f 'SimpleExp -> AST f 'Exp
+    -- SimpleExp
+    SAppF :: Name -> [SimpleVal] -> AST f 'SimpleExp
+    SReturnF :: Val -> AST f 'SimpleExp
+    SStoreF :: Val -> AST f 'SimpleExp
+    SFetchF :: Name -> AST f 'SimpleExp
+    SUpdateF :: Name -> Val -> AST f 'SimpleExp
+    -- Alt
+    AltF :: CPat -> f 'Exp -> AST f 'Alt
+
+type Program   = IFix AST 'Program
+type Def       = IFix AST 'Def
+type Exp       = IFix AST 'Exp
+type SimpleExp = IFix AST 'SimpleExp
+type Alt       = IFix AST 'Alt
+
+instance IFunctor AST where
+    imap = imapDefault
+
+instance ITraversable AST where
+    itraverse :: forall ix a b m. (Applicative m, SingI ix)
+              => (forall ix. SingI ix => a ix -> m (b ix))
+              -> AST a ix
+              -> m (AST b ix)
+    itraverse f =
+      case sing :: Sing ix of
+        SProgram -> \case
+          ProgramF externs defs -> ProgramF externs <$> traverse (f @'Def) defs
+        SDef -> \case
+          DefF fn args body -> DefF fn args <$> f @'Exp body
+        SExp -> \case
+          EBindF e1 pat e2 -> EBindF <$> f @'SimpleExp e1 <*> pure pat <*> f @'Exp e2
+          ECaseF x alts -> ECaseF x <$> (traverse (f @'Alt) alts)
+          ESimpleF e -> ESimpleF <$> f @'SimpleExp e
+        SSimpleExp -> \case
+          SAppF fn args -> pure $ SAppF fn args
+          SReturnF x -> pure $ SReturnF x
+          SStoreF x -> pure $ SStoreF x
+          SFetchF l -> pure $ SFetchF l
+          SUpdateF l x -> pure $ SUpdateF l x
+        SAlt -> \case
+          AltF cpat e -> AltF cpat <$> f @'Exp e
+
+instance IShow AST where
+    ishowsPrec :: forall ix a. SingI ix
+               => (forall ix. SingI ix => Int -> a ix -> ShowS)
+               -> Int
+               -> AST a ix
+               -> ShowS
+    ishowsPrec sp p =
+      case sing :: Sing ix of
+        SProgram -> \case
+          ProgramF externs defs -> showParen (p > 10) $
+            showString "ProgramF " . showsPrec 11 externs . showString " " . showListWith (sp 0) defs
+        SDef -> \case
+          DefF fn args body -> showParen (p > 10) $
+            showString "DefF " . showsPrec 11 fn . showString " " . showsPrec 11 args . showString " " . sp 11 body
+        SExp -> \case
+          EBindF e1 pat e2 -> showParen (p > 10) $
+            showString "EBindF " . sp 11 e1 . showString " " . showsPrec 11 pat . showString " " . sp 11 e2
+          ECaseF x alts -> showParen (p > 10) $
+            showString "ECaseF " . showsPrec 11 x . showString " " . showListWith (sp 0) alts
+          ESimpleF e -> showParen (p > 10) $
+            showString "ESimpleF " . sp 11 e
+        SSimpleExp -> \case
+          SAppF fn args -> showParen (p > 10) $
+            showString "SAppF " . showsPrec 11 fn . showString " " . showsPrec 11 args
+          SReturnF x -> showParen (p > 10) $
+            showString "SReturnF " . showsPrec 11 x
+          SStoreF x -> showParen (p > 10) $
+            showString "SStoreF " . showsPrec 11 x
+          SFetchF x -> showParen (p > 10) $
+            showString "SFetchF " . showsPrec 11 x
+          SUpdateF x y -> showParen (p > 10) $
+            showString "SUpdateF " . showsPrec 11 x . showString " " . showsPrec 11 y
+        SAlt -> \case
+          AltF cpat e -> showParen (p > 10) $
+            showString "AltF " . showsPrec 11 cpat . showString " " . sp 11 e
+
+data FunNames (ix :: ASTIdx) where
+    FNProgram :: { getFunNamesProgram :: Set Name } -> FunNames 'Program
+    FNDef :: { getFunNamesDef :: Name } -> FunNames 'Def
+    FNOther :: FunNames ix
+
+funnames :: Program -> Set Name
+funnames = getFunNamesProgram . cata alg
+    where
+        alg :: forall ix. SingI ix
+            => AST FunNames ix
+            -> FunNames ix
+        alg =
+          case sing :: Sing ix of
+            SProgram -> \case
+              ProgramF _ defs -> FNProgram $ Set.fromList $ getFunNamesDef <$> defs
+            SDef -> \case
+              DefF f _ _ -> FNDef f
+            _ -> \case
+                _ -> FNOther
+
+-- type SSAM = State (Set Name, Int)
+
+-- ssa :: IFix AST 'Exp -> IFix AST 'Exp
+-- ssa e = flip evalState (mempty, 1) $
+       -- getConst (cata folder e)
+    -- >> anaM unfolder (Const (mempty, e))
+    -- where
+        -- folder :: AST (Const (SSAM ())) ~~> Const (SSAM ())
+        -- folder = undefined
+        -- unfolder :: forall ix. SingI ix
+                 -- => Const (Map Name Int, IFix AST 'Exp) ix
+                 -- -> SSAM (AST (Const (Map Name Int, IFix AST 'Exp)) ix)
+        -- unfolder = undefined
+
diff --git a/test/Spec.hs b/test/Spec.hs
new file mode 100644
--- /dev/null
+++ b/test/Spec.hs
@@ -0,0 +1,15 @@
+module Main (main) where
+
+import Test.Hspec
+import Test.QuickCheck
+import qualified FibSpec
+import qualified GRINSpec
+
+main :: IO ()
+main = hspec spec
+
+spec :: Spec
+spec = do
+    describe "FibSpec"  FibSpec.spec
+    describe "GRINSpec" GRINSpec.spec
+