diff --git a/Free/Type b/Free/Type
new file mode 100644
index 0000000..3f37842
--- /dev/null
+++ b/Free/Type
@@ -0,0 +1 @@
+λ(f : Type → Type) → λ(a : Type) → ∀(r : Type) → (a → r) → (f r → r) → r
diff --git a/Free/applicative b/Free/applicative
new file mode 100644
index 0000000..7196cb4
--- /dev/null
+++ b/Free/applicative
@@ -0,0 +1,23 @@
+    let Applicative =
+          https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Applicative/Type
+    
+in    λ(f : Type → Type)
+    →     { ap =
+                λ(a : Type)
+              → λ(b : Type)
+              → λ(mf : ./Type f (a → b))
+              → λ(mx : ./Type f a)
+              → λ(r : Type)
+              → λ(kp : b → r)
+              → λ(kf : f r → r)
+              → mf r (λ(ff : a → b) → mx r (λ(xx : a) → kp (ff xx)) kf) kf
+          , pure =
+                λ(a : Type)
+              → λ(x : a)
+              → λ(r : Type)
+              → λ(kp : a → r)
+              → λ(kf : f r → r)
+              → kp x
+          }
+        ∧ ./functor f
+      : Applicative (./Type f)
diff --git a/Free/foldFree b/Free/foldFree
new file mode 100644
index 0000000..14f68f8
--- /dev/null
+++ b/Free/foldFree
@@ -0,0 +1,22 @@
+    let Monad =
+          https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Monad/Type
+
+in  let Monad/package =
+          https://raw.githubusercontent.com/FormationAI/dhall-bhat/6f66fc588c9d49a662794a32b29962341c373eb4/Monad/package.dhall
+    
+in    λ(f : Type → Type)
+    → λ(g : Type → Type)
+    → λ(monad : Monad g)
+    → λ(a : Type)
+    → λ(n : ∀(x : Type) → f x → g x)
+    → (./recursive f a).cata
+      (g a)
+      (   λ(free : ./../FreeF/Type f a (g a))
+        → merge
+          { Pure =
+              monad.pure a
+          , Free =
+              λ(q : f (g a)) → (Monad/package g monad).join a (n (g a) q)
+          }
+          free
+      )
diff --git a/Free/foldable b/Free/foldable
new file mode 100644
index 0000000..a4595ed
--- /dev/null
+++ b/Free/foldable
@@ -0,0 +1,33 @@
+    let Foldable =
+          https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Foldable/Type
+
+in  let Function/category =
+          https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Function/category
+    
+in    λ(F : Type → Type)
+    → λ(foldable : Foldable F)
+    →   { fold =
+              λ(a : Type)
+            → λ(ts : ./Type F a)
+            → λ(b : Type)
+            → λ(f : a → b → b)
+            → (./recursive F a).cata
+              (b → b)
+              (   λ(x : ./../FreeF/Type F a (b → b))
+                → merge
+                  { Pure =
+                      λ(x : a) → f x
+                  , Free =
+                        λ(x : F (b → b))
+                      → foldable.fold
+                        (b → b)
+                        x
+                        (b → b)
+                        (Function/category.compose b b b)
+                        (Function/category.identity b)
+                  }
+                  x
+              )
+              ts
+        }
+      : Foldable (./Type F)
diff --git a/Free/fromMu b/Free/fromMu
new file mode 100644
index 0000000..e8bbd5f
--- /dev/null
+++ b/Free/fromMu
@@ -0,0 +1,9 @@
+let FreeF = ./../FreeF/Type
+
+in    λ(f : Type → Type)
+    → λ(a : Type)
+    → λ(m : ./../Mu/Type (FreeF f a))
+    → λ(r : Type)
+    → λ(kp : a → r)
+    → λ(kf : f r → r)
+    → m r (λ(free : FreeF f a r) → merge { Pure = kp, Free = kf } free)
diff --git a/Free/functor b/Free/functor
new file mode 100644
index 0000000..9d8f685
--- /dev/null
+++ b/Free/functor
@@ -0,0 +1,15 @@
+    let Functor =
+          https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Functor/Type
+
+in    λ(F : Type → Type)
+    →   { map =
+              λ(a : Type)
+            → λ(b : Type)
+            → λ(f : a → b)
+            → λ(m : ./Type F a)
+            → λ(r : Type)
+            → λ(kp : b → r)
+            → λ(kf : F r → r)
+            → m r (λ(x : a) → kp (f x)) kf
+        }
+      : Functor (./Type F)
diff --git a/Free/hoist b/Free/hoist
new file mode 100644
index 0000000..d4a0685
--- /dev/null
+++ b/Free/hoist
@@ -0,0 +1,9 @@
+  λ(f : Type → Type)
+→ λ(g : Type → Type)
+→ λ(a : Type)
+→ λ(n : ∀(x : Type) → f x → g x)
+→ λ(m : ./Type f a)
+→ λ(r : Type)
+→ λ(kp : a → r)
+→ λ(kf : g r → r)
+→ m r kp (λ(q : f r) → kf (n r q))
diff --git a/Free/iter b/Free/iter
new file mode 100644
index 0000000..d38e56a
--- /dev/null
+++ b/Free/iter
@@ -0,0 +1,5 @@
+  λ(f : Type → Type)
+→ λ(a : Type)
+→ λ(phi : f a → a)
+→ λ(m : ./Type f a)
+→ m a (λ(x : a) → x) phi
diff --git a/Free/iterA b/Free/iterA
new file mode 100644
index 0000000..c52752d
--- /dev/null
+++ b/Free/iterA
@@ -0,0 +1,10 @@
+   let Applicative =
+         https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Applicative/Type
+
+in    λ(f : Type → Type)
+    → λ(g : Type → Type)
+    → λ(applicative : Applicative g)
+    → λ(a : Type)
+    → λ(phi : f (g a) → g a)
+    → λ(m : ./Type f a)
+    → m (g a) (applicative.pure a) phi
diff --git a/Free/liftF b/Free/liftF
new file mode 100644
index 0000000..2bf16c8
--- /dev/null
+++ b/Free/liftF
@@ -0,0 +1,11 @@
+   let Functor =
+         https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Functor/Type
+
+in    λ(f : Type → Type)
+    → λ(functor : Functor f)
+    → λ(a : Type)
+    → λ(x : f a)
+    → λ(r : Type)
+    → λ(kp : a → r)
+    → λ(kf : f r → r)
+    → kf (functor.map a r kp x)
diff --git a/Free/monad b/Free/monad
new file mode 100644
index 0000000..32b8655
--- /dev/null
+++ b/Free/monad
@@ -0,0 +1,16 @@
+    let Monad =
+          https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Monad/Type
+    
+in    λ(f : Type → Type)
+    →     { bind =
+                λ(a : Type)
+              → λ(b : Type)
+              → λ(m : ./Type f a)
+              → λ(g : a → ./Type f b)
+              → λ(r : Type)
+              → λ(kp : b → r)
+              → λ(kf : f r → r)
+              → m r (λ(x : a) → g x r kp kf) kf
+          }
+        ∧ ./applicative f
+      : Monad (./Type f)
diff --git a/Free/package.dhall b/Free/package.dhall
new file mode 100644
index 0000000..f586d8c
--- /dev/null
+++ b/Free/package.dhall
@@ -0,0 +1,19 @@
+  λ(f : Type → Type)
+→   { iter =
+        ./iter f
+    , iterA =
+        ./iterA f
+    , retract =
+        ./retract f
+    , wrap =
+        ./wrap f
+    , liftF =
+        ./liftF f
+    , foldFree =
+        ./foldFree f
+    , toMu =
+        ./toMu f
+    , fromMu =
+        ./fromMu f
+    }
+  ∧ ./monad f ⫽ ./transformer
diff --git a/Free/recursive b/Free/recursive
new file mode 100644
index 0000000..a4889f2
--- /dev/null
+++ b/Free/recursive
@@ -0,0 +1,13 @@
+  λ(f : Type → Type)
+→ λ(a : Type)
+→     let FreeF = ./../FreeF/Type f a
+  
+  in  let Mu/recursive = ./../Mu/recursive FreeF
+  
+  in    { cata =
+              λ(b : Type)
+            → λ(alg : ./../algebra FreeF b)
+            → λ(fa : ./Type f a)
+            → Mu/recursive.cata b alg (./toMu f a fa)
+        }
+      : ./../Recursive/Type (./Type f a) FreeF
diff --git a/Free/retract b/Free/retract
new file mode 100644
index 0000000..3addc68
--- /dev/null
+++ b/Free/retract
@@ -0,0 +1,7 @@
+    let Monad =
+          https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Monad/Type
+
+in    λ(f : Type → Type)
+    → λ(monad : Monad f)
+    → λ(a : Type)
+    → ./foldFree f f monad a (λ(b : Type) → λ(x : f b) → x)
diff --git a/Free/steppable b/Free/steppable
new file mode 100644
index 0000000..add2717
--- /dev/null
+++ b/Free/steppable
@@ -0,0 +1,33 @@
+    let Functor =
+          https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Functor/Type
+
+in    λ(f : Type → Type)
+    → λ(functor : Functor f)
+    → λ(a : Type)
+    →     let Free = ./Type f a
+      
+      in  let FreeF = ./../FreeF/Type f a
+
+      in  let FreeF/functor = ./../FreeF/functor f functor a
+
+      in  let MuFree = ./../Mu/Type FreeF
+
+      in  let Mu/steppable = ./../Mu/steppable FreeF FreeF/functor
+
+      in  let toMu = ./toMu f a
+
+      in  let fromMu = ./fromMu f a
+      
+      in    { embed =
+                  λ(fm : FreeF Free)
+                → fromMu
+                  (Mu/steppable.embed (FreeF/functor.map Free MuFree toMu fm))
+            , project =
+                  λ(fm : Free)
+                → FreeF/functor.map
+                  MuFree
+                  Free
+                  fromMu
+                  (Mu/steppable.project (toMu fm))
+            }
+          : ./../Steppable/Type Free FreeF
diff --git a/Free/toMu b/Free/toMu
new file mode 100644
index 0000000..2226095
--- /dev/null
+++ b/Free/toMu
@@ -0,0 +1,8 @@
+  λ(F : Type → Type)
+→ λ(a : Type)
+→ λ(m : ./Type F a)
+→ λ(r : Type)
+→ let FreeF = ./../FreeF/Type F a r
+  
+  in    λ(f : FreeF → r)
+      → m r (λ(x : a) → f (FreeF.Pure x)) (λ(x : F r) → f (FreeF.Free x))
diff --git a/Free/transformer b/Free/transformer
new file mode 100644
index 0000000..0238d36
--- /dev/null
+++ b/Free/transformer
@@ -0,0 +1,16 @@
+    let Monad =
+          https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Monad/Type
+
+in  let Transformer =
+          https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Transformer/Type
+
+in  let extractFunctor =
+          https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Monad/extractFunctor
+    
+in    { lift =
+            λ(m : Type → Type)
+          → λ(monad : Monad m)
+          → λ(a : Type)
+          → ./liftF m (extractFunctor m monad) a
+      }
+    : Transformer ./Type
diff --git a/Free/traversable b/Free/traversable
new file mode 100644
index 0000000..a5e27a9
--- /dev/null
+++ b/Free/traversable
@@ -0,0 +1,47 @@
+    let Applicative =
+          https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Applicative/Type
+
+in  let Traversable =
+          https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Traversable/Type
+
+in  let extractFoldable =
+          https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Traversable/extractFoldable
+
+in  let extractFunctor =
+          https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Traversable/extractFunctor
+
+in  let sequence =
+          https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Traversable/sequence
+
+in    λ(F : Type → Type)
+    → λ(traversable : Traversable F)
+    →     { traverse =
+                λ(G : Type → Type)
+              → λ(applicative : Applicative G)
+              → λ(a : Type)
+              → λ(b : Type)
+              → λ(f : a → G b)
+              → (./recursive F a).cata
+                (G (./Type F b))
+                (   λ(x : ./../FreeF/Type F a (G (./Type F b)))
+                  → merge
+                    { Pure =
+                          λ(x : a)
+                        → applicative.map
+                          b
+                          (./Type F b)
+                          ((./applicative F).pure b)
+                          (f x)
+                    , Free =
+                          λ(x : F (G (./Type F b)))
+                        → applicative.map
+                          (F (./Type F b))
+                          (./Type F b)
+                          (./wrap F b (extractFunctor F traversable))
+                          (sequence F traversable G applicative (./Type F b) x)
+                    }
+                    x
+                )
+          }
+        ∧ ./foldable F (extractFoldable F traversable) ⫽ ./functor F
+      : Traversable (./Type F)
diff --git a/Free/wrap b/Free/wrap
new file mode 100644
index 0000000..4ce1dfc
--- /dev/null
+++ b/Free/wrap
@@ -0,0 +1,11 @@
+   let Functor =
+         https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Functor/Type
+
+in    λ(f : Type → Type)
+    → λ(a : Type)
+    → λ(functor : Functor f)
+    → λ(x : f (./Type f a))
+    → λ(r : Type)
+    → λ(kp : a → r)
+    → λ(kf : f r → r)
+    → kf (functor.map (./Type f a) r (λ(m : ./Type f a) → m r kp kf) x)
diff --git a/FreeF/Type b/FreeF/Type
new file mode 100644
index 0000000..953f49d
--- /dev/null
+++ b/FreeF/Type
@@ -0,0 +1 @@
+λ(f : Type → Type) → λ(a : Type) → λ(b : Type) → < Pure : a | Free : f b >
diff --git a/FreeF/bifunctor b/FreeF/bifunctor
new file mode 100644
index 0000000..747a3bf
--- /dev/null
+++ b/FreeF/bifunctor
@@ -0,0 +1,25 @@
+    let Bifunctor =
+          https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Bifunctor/Type
+
+in  let Functor =
+          https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Functor/Type
+    
+in    λ(F : Type → Type)
+    → λ(functor : Functor F)
+    →   { bimap =
+              λ(a : Type)
+            → λ(b : Type)
+            → λ(c : Type)
+            → λ(d : Type)
+            → λ(f : a → c)
+            → λ(g : b → d)
+            → λ(m : ./Type F a b)
+            → merge
+              { Pure =
+                  λ(x : a) → (./Type F c d).Pure (f x)
+              , Free =
+                  λ(x : F b) → (./Type F c d).Free (functor.map b d g x)
+              }
+              m
+        }
+      : Bifunctor (./Type F)
diff --git a/FreeF/foldable b/FreeF/foldable
new file mode 100644
index 0000000..dffcbf9
--- /dev/null
+++ b/FreeF/foldable
@@ -0,0 +1,21 @@
+    let Foldable =
+          https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Foldable/Type
+
+in    λ(F : Type → Type)
+    → λ(foldable : Foldable F)
+    → λ(c : Type)
+    →   { fold =
+              λ(a : Type)
+            → λ(ts : ./Type F c a)
+            → λ(b : Type)
+            → λ(f : a → b → b)
+            → λ(z : b)
+            → merge
+              { Pure =
+                  λ(x : c) → z
+              , Free =
+                  λ(x : F a) → foldable.fold a x b f z
+              }
+              ts
+        }
+      : Foldable (./Type F c)
diff --git a/FreeF/functor b/FreeF/functor
new file mode 100644
index 0000000..5668dca
--- /dev/null
+++ b/FreeF/functor
@@ -0,0 +1,11 @@
+    let Functor =
+          https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Functor/Type
+    
+in  let second =
+          https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Bifunctor/second
+   
+in    λ(F : Type → Type)
+    → λ(functor : Functor F)
+    → λ(c : Type)
+    →   { map = second (./Type F) (./bifunctor F functor) c }
+      : Functor (./Type F c)
diff --git a/FreeF/traversable b/FreeF/traversable
new file mode 100644
index 0000000..6c1094b
--- /dev/null
+++ b/FreeF/traversable
@@ -0,0 +1,40 @@
+    let Applicative =
+          https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Applicative/Type
+
+in  let Traversable =
+          https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Traversable/Type
+
+in  let extractFoldable =
+          https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Traversable/extractFoldable
+
+in  let extractFunctor =
+          https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Traversable/extractFunctor
+
+in    λ(F : Type → Type)
+    → λ(traversable : Traversable F)
+    → λ(c : Type)
+    →     { traverse =
+                λ(G : Type → Type)
+              → λ(applicative : Applicative G)
+              → λ(a : Type)
+              → λ(b : Type)
+              → λ(f : a → G b)
+              → λ(ts : ./Type F c a)
+              → let FreeF = ./Type F c b
+
+                in  merge
+                    { Pure =
+                        λ(x : c) → applicative.pure FreeF (FreeF.Pure x)
+                    , Free =
+                          λ(x : F a)
+                        → applicative.map
+                          (F b)
+                          FreeF
+                          FreeF.Free
+                          (traversable.traverse G applicative a b f x)
+                    }
+                    ts
+          }
+        ∧   ./foldable F (extractFoldable F traversable) c
+          ⫽ ./functor F (extractFunctor F traversable) c
+      : Traversable (./Type F c)