diff --git a/COPYING b/COPYING
new file mode 100644
--- /dev/null
+++ b/COPYING
@@ -0,0 +1,25 @@
+Copyright (c) 2012 Conal Elliott
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+1. Redistributions of source code must retain the above copyright
+   notice, this list of conditions and the following disclaimer.
+2. 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.
+3. The names of the authors may not be used to endorse or promote products
+   derived from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``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 AUTHORS 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.lhs b/Setup.lhs
new file mode 100644
--- /dev/null
+++ b/Setup.lhs
@@ -0,0 +1,3 @@
+#!/usr/bin/env runhaskell
+> import Distribution.Simple
+> main = defaultMain
diff --git a/ftree.cabal b/ftree.cabal
new file mode 100644
--- /dev/null
+++ b/ftree.cabal
@@ -0,0 +1,27 @@
+Name:                ftree
+Version:             0.1.2
+Cabal-Version:       >= 1.6
+Synopsis:            Depth-typed functor-based trees, both top-down and bottom-up
+Category:            Data
+Description:
+  Depth-typed functor-based trees, both top-down and bottom-up
+Author:              Conal Elliott
+Maintainer:          conal@conal.net
+Copyright:           (c) 2013 by Conal Elliott
+License:             BSD3
+License-File:        COPYING
+Stability:           experimental
+build-type:          Simple
+
+source-repository head
+  type:     git
+  location: git://github.com/conal/ftree.git
+
+Library
+  hs-Source-Dirs:      src
+  Extensions:
+  Build-Depends:       base<5, ShowF, type-unary>=0.2.12
+  Exposed-Modules:     
+                       Data.FTree.TopDown
+                       Data.FTree.BottomUp
+  ghc-options:         -Wall
diff --git a/src/Data/FTree/BottomUp.hs b/src/Data/FTree/BottomUp.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/FTree/BottomUp.hs
@@ -0,0 +1,173 @@
+{-# LANGUAGE GADTs, KindSignatures, TypeOperators, Rank2Types, DataKinds #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# OPTIONS_GHC -Wall #-}
+
+----------------------------------------------------------------------
+-- |
+-- Module      :  Data.FTree.BottomUp
+-- Copyright   :  (c) 2011 Conal Elliott
+-- 
+-- Maintainer  :  conal@conal.net
+-- Stability   :  experimental
+-- 
+-- Top-down, depth-typed functor trees.
+-- In other words, right-associated n-ary functor composition.
+-- See <http://conal.net/blog/posts/a-trie-for-length-typed-vectors/>.
+----------------------------------------------------------------------
+
+module Data.FTree.BottomUp (T(..),(:^),unL,unB,foldT,inT,inT2,inL,inB,inL2,inB2) where
+
+-- TODO: explicit exports
+
+import Prelude hiding (and)
+
+import Control.Applicative (Applicative(..),liftA2,(<$>))
+import Data.Foldable (Foldable(..),and)
+import Data.Traversable (Traversable(..))
+import Data.Monoid (Monoid(..))
+
+import TypeUnary.Nat
+
+import Text.ShowF
+
+-- References:
+--
+-- [*Applicative Programming with Effects*]: http://www.soi.city.ac.uk/~ross/papers/Applicative.html
+-- [*Semantic editor combinators*]: http://conal.net/blog/posts/semantic-editor-combinators/
+
+-- Since composition is associative, a recursive formulation might naturally fold from the left or from the right.
+-- In this module, we'll fold on the right
+-- See the module `BottomUp` for left-folded composition.
+
+--   f :^ Z   =~ Id
+--   f :^ S n =~ f :. (f :^ n)
+
+-- Writing as a GADT:
+
+data T :: (* -> *) -> * -> (* -> *) where
+  L :: a -> T f Z a
+  B :: IsNat n => T f n (f a) -> T f (S n) a
+
+type (:^) = T
+
+unL :: (f :^ Z) a -> a
+unL (L a) = a
+
+unB :: (f :^ S n) a -> (f :^ n) (f a)
+unB (B fsa) = fsa
+
+foldT :: forall f n a z. Functor f =>
+         (a -> z) -> (f a -> a) -> (f :^ n) a -> z
+foldT l b = fo
+ where
+   fo :: (f :^ m) a -> z
+   fo (L a)  = l a
+   fo (B ts) = fo (b <$> ts)
+
+-- Operate inside the representation of `f :^ n`:
+
+inT :: (a -> b)
+    -> (forall n. IsNat n => (f :^ n) (f a) -> (f :^ n) (f b))
+    -> (forall n. (f :^ n) a -> (f :^ n) b)
+inT l _ (L a ) = (L (l a ))
+inT _ b (B as) = (B (b as))
+
+inT2 :: (a -> b -> c)
+     -> (forall n. IsNat n => (f :^ n) (f a) -> (f :^ n) (f b) -> (f :^ n) (f c))
+     -> (forall n. (f :^ n) a -> (f :^ n) b -> (f :^ n) c)
+inT2 l _ (L a ) (L b ) = L (l a  b )
+inT2 _ b (B as) (B bs) = B (b as bs)
+inT2 _ _ _ _ = error "inT2: unhandled case"  -- Possible??
+
+-- Similar to `inT`, but useful when we can know whether a `L` or a `B`:
+
+inL :: (a -> b)
+        -> ((f :^ Z) a -> (f :^ Z) b)
+inL h (L a ) = L (h a )
+
+inB :: ((f :^ n) (f a) -> (f :^ n) (f b))
+        -> ((f :^ (S n)) a -> (f :^ (S n)) b)
+inB h (B as) = B (h as)
+
+inL2 :: (a -> b -> c)
+         -> ((f :^ Z) a -> (f :^ Z) b -> (f :^ Z) c)
+inL2 h (L a ) (L b ) = L (h a  b )
+
+inB2 :: ((f :^ n) (f a) -> (f :^ n) (f b) -> (f :^ n) (f c))
+         -> ((f :^ (S n)) a -> (f :^ (S n)) b -> (f :^ (S n)) c)
+inB2 h (B as) (B bs) = B (h as bs)
+
+
+instance (Functor f, ShowF f, Show a) => Show ((f :^ n) a) where show = showF
+
+instance (Functor f, ShowF f) => ShowF (f :^ n) where
+  showsPrecF p (L a ) = showsApp1   "L" p a
+  showsPrecF p (B as) = showsFComp1 "B" p as
+
+-- The Functor constructors for showing come from showsFComp1. Revisit.
+
+-- Functors compose into functors and applicatives into applicatives.
+-- (See [*Applicative Programming with Effects*] (section 5) and [*Semantic editor combinators*].)
+-- The following definitions arise from the standard instances for binary functor composition.
+
+instance Functor f => Functor (f :^ n) where
+  fmap h = inT h ((fmap.fmap) h)
+
+instance (IsNat n, Applicative f) => Applicative (f :^ n) where
+  pure = pureN nat
+  (<*>) = inT2 ($) (liftA2 (<*>))
+
+pureN :: Applicative f => Nat n -> a -> (f :^ n) a
+pureN Zero     a = L a
+pureN (Succ _) a = B ((pure . pure) a)
+
+-- More explicitly:
+
+--   pureN (Succ n) a = B ((pure . pureN n) a)
+
+-- The `Foldable` and `Traversable` classes are also closed under composition.
+
+instance (Functor f, Foldable f) => Foldable (f :^ n) where
+  fold (L a ) = a
+  fold (B as) = fold (fold <$> as)
+
+-- Alternatively, define `foldMap`:
+
+--     foldMap h (L a ) = h a
+--     foldMap h (B as) = fold (foldMap h <$> as)
+
+-- Better yet:
+
+  foldMap h (L a ) = h a
+  foldMap h (B as) = (foldMap.foldMap) h as
+
+instance Traversable f => Traversable (f :^ n) where
+  sequenceA (L qa) = L <$> qa
+  sequenceA (B as) = fmap B . sequenceA . fmap sequenceA $ as
+
+-- i.e.,
+
+--     sequenceA . L = fmap L
+-- <
+--     sequenceA . B = fmap B . sequenceA . fmap sequenceA
+
+-- We can use the `Applicative` instance in standard way to get a `Monoid` instance:
+
+instance (IsNat n, Applicative f, Monoid m) => Monoid ((f :^ n) m) where
+  mempty  = pure mempty
+  mappend = liftA2 mappend
+
+-- (To follow the general pattern exactly, replace the first two constraints with `Applicative (f :^ n)` and add `FlexibleContexts` to the module's `LANGUAGE` pragma.)
+
+
+-- Equality and ordering
+-- =====================
+
+-- Standard forms:
+
+instance (Foldable f, Applicative f, IsNat n, Eq a) => Eq ((f :^ n) a) where
+  (==) = (fmap.fmap) and (liftA2 (==))
+
+instance (Foldable f, Applicative f, IsNat n, Ord a) => Ord ((f :^ n) a) where
+  compare = (fmap.fmap) fold (liftA2 compare)
diff --git a/src/Data/FTree/TopDown.hs b/src/Data/FTree/TopDown.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/FTree/TopDown.hs
@@ -0,0 +1,172 @@
+{-# LANGUAGE GADTs, KindSignatures, TypeOperators, Rank2Types, DataKinds #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# OPTIONS_GHC -Wall #-}
+
+----------------------------------------------------------------------
+-- |
+-- Module      :  Data.FTree.TopDown
+-- Copyright   :  (c) 2011 Conal Elliott
+-- 
+-- Maintainer  :  conal@conal.net
+-- Stability   :  experimental
+-- 
+-- Top-down, depth-typed functor trees.
+-- In other words, right-associated n-ary functor composition.
+-- See <http://conal.net/blog/posts/a-trie-for-length-typed-vectors/>.
+----------------------------------------------------------------------
+
+module Data.FTree.TopDown (T(..),(:^),unL,unB,foldT,inT,inT2,inL,inB,inL2,inB2) where
+
+-- TODO: explicit exports
+
+import Prelude hiding (and)
+
+import Control.Applicative (Applicative(..),liftA2,(<$>))
+import Data.Foldable (Foldable(..),and)
+import Data.Traversable (Traversable(..))
+import Data.Monoid (Monoid(..))
+
+import TypeUnary.Nat
+
+import Text.ShowF
+
+-- References:
+--
+-- [*Applicative Programming with Effects*]: http://www.soi.city.ac.uk/~ross/papers/Applicative.html
+-- [*Semantic editor combinators*]: http://conal.net/blog/posts/semantic-editor-combinators/
+
+-- Since composition is associative, a recursive formulation might naturally fold from the left or from the right.
+-- In this module, we'll fold on the right
+-- See the module `BottomUp` for left-folded composition.
+
+--   f :^ Z   =~ Id
+--   f :^ S n =~ f :. (f :^ n)
+
+-- Writing as a GADT:
+
+data T :: (* -> *) -> * -> (* -> *) where
+  L :: a -> T f Z a
+  B :: IsNat n => f (T f n a) -> T f (S n) a
+
+type (:^) = T
+
+unL :: (f :^ Z) a -> a
+unL (L a) = a
+
+unB :: (f :^ S n) a -> f ((f :^ n) a)
+unB (B fsa) = fsa
+
+foldT :: forall f n a z. Functor f =>
+         (a -> z) -> (f z -> z) -> (f :^ n) a -> z
+foldT l b = fo
+ where
+   fo :: (f :^ m) a -> z
+   fo (L a)  = l a
+   fo (B ts) = b (fo <$> ts)
+
+-- Operate inside the representation of `f :^ n`:
+
+inT :: (a -> b)
+    -> (forall n. IsNat n => f ((f :^ n) a) -> f ((f :^ n) b))
+    -> (forall n. (f :^ n) a -> (f :^ n) b)
+inT l _ (L a ) = (L (l a ))
+inT _ b (B as) = (B (b as))
+
+inT2 :: (a -> b -> c)
+     -> (forall n. IsNat n => f ((f :^ n) a) -> f ((f :^ n) b) -> f ((f :^ n) c))
+     -> (forall n. (f :^ n) a -> (f :^ n) b -> (f :^ n) c)
+inT2 l _ (L a ) (L b ) = L (l a  b )
+inT2 _ b (B as) (B bs) = B (b as bs)
+inT2 _ _ _ _ = error "inT2: unhandled case"  -- Possible??
+
+-- Similar to `inT`, but useful when we can know whether a `L` or a `B`:
+
+inL :: (a -> b)
+        -> ((f :^ Z) a -> (f :^ Z) b)
+inL h (L a ) = L (h a )
+
+inB :: (f ((f :^ n) a) -> f ((f :^ n) b))
+        -> ((f :^ (S n)) a -> (f :^ (S n)) b)
+inB h (B as) = B (h as)
+
+inL2 :: (a -> b -> c)
+         -> ((f :^ Z) a -> (f :^ Z) b -> (f :^ Z) c)
+inL2 h (L a ) (L b ) = L (h a  b )
+
+inB2 :: (f ((f :^ n) a) -> f ((f :^ n) b) -> f ((f :^ n) c))
+         -> ((f :^ (S n)) a -> (f :^ (S n)) b -> (f :^ (S n)) c)
+inB2 h (B as) (B bs) = B (h as bs)
+
+
+instance (ShowF f, Show a) => Show ((f :^ n) a) where show = showF
+
+instance ShowF f => ShowF (f :^ n) where
+  showsPrecF p (L a ) = showsApp1  "L" p a
+  showsPrecF p (B as) = showsFApp1 "B" p as
+
+-- Functors compose into functors and applicatives into applicatives.
+-- (See [*Applicative Programming with Effects*] (section 5) and [*Semantic editor combinators*].)
+-- The following definitions arise from the standard instances for binary functor composition.
+
+instance Functor f => Functor (f :^ n) where
+  fmap h = inT h ((fmap.fmap) h)
+
+instance (IsNat n, Applicative f) => Applicative (f :^ n) where
+  pure = pureN nat
+  (<*>) = inT2 ($) (liftA2 (<*>))
+
+pureN :: Applicative f => Nat n -> a -> (f :^ n) a
+pureN Zero     a = L a
+pureN (Succ _) a = B ((pure . pure) a)
+
+-- More explicitly:
+
+--   pureN (Succ n) a = B ((pure . pureN n) a)
+
+-- The `Foldable` and `Traversable` classes are also closed under composition.
+
+instance (Functor f, Foldable f) => Foldable (f :^ n) where
+  fold (L a ) = a
+  fold (B as) = fold (fold <$> as)
+
+-- Alternatively, define `foldMap`:
+
+--     foldMap h (L a ) = h a
+--     foldMap h (B as) = fold (foldMap h <$> as)
+
+-- Better yet:
+
+  foldMap h (L a ) = h a
+  foldMap h (B as) = (foldMap.foldMap) h as
+
+
+instance Traversable f => Traversable (f :^ n) where
+  sequenceA (L qa) = L <$> qa
+  sequenceA (B as) = fmap B . sequenceA . fmap sequenceA $ as
+
+-- i.e.,
+
+--     sequenceA . L = fmap L
+-- <
+--     sequenceA . B = fmap B . sequenceA . fmap sequenceA
+
+-- We can use the `Applicative` instance in standard way to get a `Monoid` instance:
+
+instance (IsNat n, Applicative f, Monoid m) => Monoid ((f :^ n) m) where
+  mempty  = pure mempty
+  mappend = liftA2 mappend
+
+-- (To follow the general pattern exactly, replace the first two constraints with `Applicative (f :^ n)` and add `FlexibleContexts` to the module's `LANGUAGE` pragma.)
+
+
+-- Equality and ordering
+-- =====================
+
+-- Standard forms:
+
+instance (Foldable f, Applicative f, IsNat n, Eq a) => Eq ((f :^ n) a) where
+  (==) = (fmap.fmap) and (liftA2 (==))
+
+instance (Foldable f, Applicative f, IsNat n, Ord a) => Ord ((f :^ n) a) where
+  compare = (fmap.fmap) fold (liftA2 compare)