diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,5 @@
+# Revision history for dhall-recursive-adt
+
+## 0.1.0.0 -- 2021-01-28
+
+* First version. Released on an uNsUsPeCtInG world.
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,121 @@
+Creative Commons Legal Code
+
+CC0 1.0 Universal
+
+    CREATIVE COMMONS CORPORATION IS NOT A LAW FIRM AND DOES NOT PROVIDE
+    LEGAL SERVICES. DISTRIBUTION OF THIS DOCUMENT DOES NOT CREATE AN
+    ATTORNEY-CLIENT RELATIONSHIP. CREATIVE COMMONS PROVIDES THIS
+    INFORMATION ON AN "AS-IS" BASIS. CREATIVE COMMONS MAKES NO WARRANTIES
+    REGARDING THE USE OF THIS DOCUMENT OR THE INFORMATION OR WORKS
+    PROVIDED HEREUNDER, AND DISCLAIMS LIABILITY FOR DAMAGES RESULTING FROM
+    THE USE OF THIS DOCUMENT OR THE INFORMATION OR WORKS PROVIDED
+    HEREUNDER.
+
+Statement of Purpose
+
+The laws of most jurisdictions throughout the world automatically confer
+exclusive Copyright and Related Rights (defined below) upon the creator
+and subsequent owner(s) (each and all, an "owner") of an original work of
+authorship and/or a database (each, a "Work").
+
+Certain owners wish to permanently relinquish those rights to a Work for
+the purpose of contributing to a commons of creative, cultural and
+scientific works ("Commons") that the public can reliably and without fear
+of later claims of infringement build upon, modify, incorporate in other
+works, reuse and redistribute as freely as possible in any form whatsoever
+and for any purposes, including without limitation commercial purposes.
+These owners may contribute to the Commons to promote the ideal of a free
+culture and the further production of creative, cultural and scientific
+works, or to gain reputation or greater distribution for their Work in
+part through the use and efforts of others.
+
+For these and/or other purposes and motivations, and without any
+expectation of additional consideration or compensation, the person
+associating CC0 with a Work (the "Affirmer"), to the extent that he or she
+is an owner of Copyright and Related Rights in the Work, voluntarily
+elects to apply CC0 to the Work and publicly distribute the Work under its
+terms, with knowledge of his or her Copyright and Related Rights in the
+Work and the meaning and intended legal effect of CC0 on those rights.
+
+1. Copyright and Related Rights. A Work made available under CC0 may be
+protected by copyright and related or neighboring rights ("Copyright and
+Related Rights"). Copyright and Related Rights include, but are not
+limited to, the following:
+
+  i. the right to reproduce, adapt, distribute, perform, display,
+     communicate, and translate a Work;
+ ii. moral rights retained by the original author(s) and/or performer(s);
+iii. publicity and privacy rights pertaining to a person's image or
+     likeness depicted in a Work;
+ iv. rights protecting against unfair competition in regards to a Work,
+     subject to the limitations in paragraph 4(a), below;
+  v. rights protecting the extraction, dissemination, use and reuse of data
+     in a Work;
+ vi. database rights (such as those arising under Directive 96/9/EC of the
+     European Parliament and of the Council of 11 March 1996 on the legal
+     protection of databases, and under any national implementation
+     thereof, including any amended or successor version of such
+     directive); and
+vii. other similar, equivalent or corresponding rights throughout the
+     world based on applicable law or treaty, and any national
+     implementations thereof.
+
+2. Waiver. To the greatest extent permitted by, but not in contravention
+of, applicable law, Affirmer hereby overtly, fully, permanently,
+irrevocably and unconditionally waives, abandons, and surrenders all of
+Affirmer's Copyright and Related Rights and associated claims and causes
+of action, whether now known or unknown (including existing as well as
+future claims and causes of action), in the Work (i) in all territories
+worldwide, (ii) for the maximum duration provided by applicable law or
+treaty (including future time extensions), (iii) in any current or future
+medium and for any number of copies, and (iv) for any purpose whatsoever,
+including without limitation commercial, advertising or promotional
+purposes (the "Waiver"). Affirmer makes the Waiver for the benefit of each
+member of the public at large and to the detriment of Affirmer's heirs and
+successors, fully intending that such Waiver shall not be subject to
+revocation, rescission, cancellation, termination, or any other legal or
+equitable action to disrupt the quiet enjoyment of the Work by the public
+as contemplated by Affirmer's express Statement of Purpose.
+
+3. Public License Fallback. Should any part of the Waiver for any reason
+be judged legally invalid or ineffective under applicable law, then the
+Waiver shall be preserved to the maximum extent permitted taking into
+account Affirmer's express Statement of Purpose. In addition, to the
+extent the Waiver is so judged Affirmer hereby grants to each affected
+person a royalty-free, non transferable, non sublicensable, non exclusive,
+irrevocable and unconditional license to exercise Affirmer's Copyright and
+Related Rights in the Work (i) in all territories worldwide, (ii) for the
+maximum duration provided by applicable law or treaty (including future
+time extensions), (iii) in any current or future medium and for any number
+of copies, and (iv) for any purpose whatsoever, including without
+limitation commercial, advertising or promotional purposes (the
+"License"). The License shall be deemed effective as of the date CC0 was
+applied by Affirmer to the Work. Should any part of the License for any
+reason be judged legally invalid or ineffective under applicable law, such
+partial invalidity or ineffectiveness shall not invalidate the remainder
+of the License, and in such case Affirmer hereby affirms that he or she
+will not (i) exercise any of his or her remaining Copyright and Related
+Rights in the Work or (ii) assert any associated claims and causes of
+action with respect to the Work, in either case contrary to Affirmer's
+express Statement of Purpose.
+
+4. Limitations and Disclaimers.
+
+ a. No trademark or patent rights held by Affirmer are waived, abandoned,
+    surrendered, licensed or otherwise affected by this document.
+ b. Affirmer offers the Work as-is and makes no representations or
+    warranties of any kind concerning the Work, express, implied,
+    statutory or otherwise, including without limitation warranties of
+    title, merchantability, fitness for a particular purpose, non
+    infringement, or the absence of latent or other defects, accuracy, or
+    the present or absence of errors, whether or not discoverable, all to
+    the greatest extent permissible under applicable law.
+ c. Affirmer disclaims responsibility for clearing rights of other persons
+    that may apply to the Work or any use thereof, including without
+    limitation any person's Copyright and Related Rights in the Work.
+    Further, Affirmer disclaims responsibility for obtaining any necessary
+    consents, permissions or other rights required for any use of the
+    Work.
+ d. Affirmer understands and acknowledges that Creative Commons is not a
+    party to this document and has no duty or obligation with respect to
+    this CC0 or use of the Work.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,7 @@
+# dhall-recursive-adt
+[![CI](https://github.com/amesgen/dhall-recursive-adt/workflows/CI/badge.svg)](https://github.com/amesgen/dhall-recursive-adt/actions)
+[![Hackage](https://img.shields.io/hackage/v/dhall-recursive-adt)](https://hackage.haskell.org/package/dhall-recursive-adt)
+
+Convert recursive Haskell ADTs from and to [Dhall](https://dhall-lang.org).
+
+See [the haddocks](https://hackage.haskell.org/package/dhall-recursive-adt/docs/Dhall-Deriving-Recursive.html) for documentation.
diff --git a/dhall-recursive-adt.cabal b/dhall-recursive-adt.cabal
new file mode 100644
--- /dev/null
+++ b/dhall-recursive-adt.cabal
@@ -0,0 +1,72 @@
+cabal-version: 2.4
+name: dhall-recursive-adt
+version: 0.1.0.0
+
+synopsis: Convert recursive ADTs from and to Dhall
+description:
+  Convert recursive ADTs from and to Dhall by automating derivation of @FromDhall@/@ToDhall@ as much as possible
+category: Dhall
+
+homepage: https://github.com/amesgen/dhall-recursive-adt
+bug-reports: https://github.com/amesgen/dhall-recursive-adt/issues
+license: CC0-1.0
+license-file: LICENSE
+extra-source-files: README.md
+author: amesgen
+maintainer: amesgen@amesgen.de
+extra-source-files:
+  CHANGELOG.md
+
+  test/tree.dhall
+
+source-repository head
+  location: https://github.com/amesgen/dhall-recursive-adt
+  type: git
+
+common commons
+  default-language: Haskell2010
+  ghc-options: -Wall -Wincomplete-record-updates -Wincomplete-uni-patterns -Wredundant-constraints -Wmissing-export-lists -fno-warn-name-shadowing -fhide-source-paths
+  if impl(ghc >= 8.8)
+    ghc-options: -Wmissing-deriving-strategies
+  if impl(ghc >= 8.10)
+    ghc-options: -Wunused-packages
+  default-extensions: BlockArguments ConstraintKinds DeriveAnyClass DeriveFoldable DeriveGeneric DeriveTraversable DerivingVia FlexibleContexts GeneralizedNewtypeDeriving LambdaCase ScopedTypeVariables StandaloneDeriving TypeApplications TypeFamilies OverloadedStrings
+
+library
+  import: commons
+  hs-source-dirs: src
+  exposed-modules:
+    Dhall.Deriving.Recursive
+  build-depends:
+      base >= 4.12 && < 5
+    , dhall ^>= 1.38
+    , data-fix ^>= 0.3
+    , recursion-schemes ^>= 5.2
+
+test-suite tasty
+  import: commons
+  type: exitcode-stdio-1.0
+  main-is: Tasty.hs
+  hs-source-dirs: test
+  ghc-options: -threaded -rtsopts -with-rtsopts=-N
+  build-depends:
+      base
+    , dhall-recursive-adt
+    , dhall
+    , either ^>= 5
+    , recursion-schemes
+    , tasty >= 1.3 && <= 1.5
+    , tasty-hunit ^>= 0.10
+    , tasty-hedgehog ^>= 1
+    , hedgehog ^>= 1
+
+test-suite docspec
+  import: commons
+  if impl(ghc >= 8.10)
+    ghc-options: -fno-warn-unused-packages
+  type: exitcode-stdio-1.0
+  main-is: Docspec.hs
+  hs-source-dirs: test
+  build-depends:
+      base
+    , neat-interpolation ^>= 0.5
diff --git a/src/Dhall/Deriving/Recursive.hs b/src/Dhall/Deriving/Recursive.hs
new file mode 100644
--- /dev/null
+++ b/src/Dhall/Deriving/Recursive.hs
@@ -0,0 +1,200 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+-- | Convert /recursive/ ADTs from and to Dhall with only /some/ boilerplate.
+--
+-- This module is intended to be used with
+-- [@DerivingVia@](https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#extension-DerivingVia).
+--
+-- Click "Dhall.Deriving.Recursive#example" for a compact example.
+module Dhall.Deriving.Recursive
+  ( -- * Walkthrough
+    -- $walkthrough
+
+    -- * Compact example
+    -- $example
+
+    -- * The @DerivingVia@ newtype
+    RecADT (..),
+
+    -- * Utilities
+    -- $utilities
+    RecFromDhall,
+    recAuto,
+    recAutoWith,
+    RecToDhall,
+    recInject,
+    recInjectWith,
+  )
+where
+
+import Data.Fix (Fix)
+import Data.Functor.Contravariant (contramap)
+import Data.Functor.Foldable (Base, Corecursive, Recursive, refix)
+import qualified Dhall as D
+
+-- | Intended to be used with @DerivingVia@, as explained in the module documentation.
+--
+-- [@a@]: your (recursive) ADT
+
+-- We could work without UndecidableInstances if we added a type parameter f (~ Base a).
+-- This wouldn't be a disaster, but it is a bit less convenient.
+newtype RecADT a = RecADT {unRecADT :: a}
+
+instance RecFromDhall a => D.FromDhall (RecADT a) where
+  autoWith = fmap RecADT . recAutoWith
+
+instance RecToDhall a => D.ToDhall (RecADT a) where
+  injectWith = contramap unRecADT . recInjectWith
+
+type RecFromDhall a = (D.FromDhall (Base a (D.Result (Base a))), Corecursive a)
+
+recAuto :: RecFromDhall a => D.Decoder a
+recAuto = recAutoWith D.defaultInputNormalizer
+
+recAutoWith :: forall a. RecFromDhall a => D.InputNormalizer -> D.Decoder a
+recAutoWith = fmap refix . D.autoWith @(Fix (Base a))
+
+type RecToDhall a = (D.ToDhall (Base a (D.Result (Base a))), Recursive a)
+
+recInject :: RecToDhall a => D.Encoder a
+recInject = recInjectWith D.defaultInputNormalizer
+
+recInjectWith :: forall a. RecToDhall a => D.InputNormalizer -> D.Encoder a
+recInjectWith = contramap refix . D.injectWith @(Fix (Base a))
+
+-- $setup
+--
+-- >>> import Numeric.Natural (Natural)
+-- >>> import GHC.Generics (Generic)
+-- >>> import Dhall (FromDhall, ToDhall)
+-- >>> :set -XDerivingVia
+-- >>> :set -XDeriveAnyClass
+-- >>> :set -XDeriveFunctor
+-- >>> :set -XDeriveFoldable
+-- >>> :set -XDeriveTraversable
+-- >>> :set -XDeriveGeneric
+-- >>> :set -XOverloadedStrings
+-- >>> :set -XQuasiQuotes
+-- >>> :set -XStandaloneDeriving
+-- >>> :set -XTemplateHaskell
+-- >>> :set -XTypeApplications
+-- >>> :set -XTypeFamilies
+
+-- $walkthrough
+--
+-- Out of the box, [dhall](https://hackage.haskell.org/package/dhall) can not derive 'D.FromDhall'/'D.ToDhall'
+-- for recursive ADTs like this one
+--
+-- >>> :{
+-- data Expr = Lit Natural
+--           | Add Expr Expr
+--           | Mul Expr Expr
+--  deriving stock Show
+-- :}
+--
+-- As Dhall has no recursion by design, it might be non-obvious how to encode this type in Dhall. Luckily,
+-- the Church\/Böhm-Berarducci encoding exists, which is essentially a fancy name for the Go4
+-- [Visitor pattern](https://en.wikipedia.org/wiki/Visitor_pattern), as explained in
+-- [this blog post](https://www.haskellforall.com/2021/01/the-visitor-pattern-is-essentially-same.html).
+-- Also make sure check out the
+-- [official How-to on translating recursive code to Dhall](https://docs.dhall-lang.org/howtos/How-to-translate-recursive-code-to-Dhall.html).
+--
+-- Explicitly, consider the /non-recursive/ ADT
+--
+-- >>> :{
+-- data ExprF a = LitF Natural
+--              | AddF a a
+--              | MulF a a
+-- :}
+--
+-- For any type @a@, this is a non-recursive sum type, which we can directly translate to a Dhall union type:
+--
+-- > let ExprF = λ(a : Type) → < LitF : Natural | AddF : { _1 : a, _2 : a } | MulF : { _1 : a, _2 : a } >
+--
+-- We can derive 'D.FromDhall'\/'D.ToDhall' for @ExprF a@. Let us use the default 'GHC.Generics.Generic'-powered
+-- version here, but we could also use e.g. "Dhall.Deriving" for customization (we use
+-- [@StandaloneDeriving@](https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#extension-StandaloneDeriving)
+-- here to be able to define the instances one by one).
+--
+-- >>> deriving stock    instance                Generic   (ExprF a)
+-- >>> deriving anyclass instance FromDhall a => FromDhall (ExprF a)
+-- >>> deriving anyclass instance ToDhall a   => ToDhall   (ExprF a)
+--
+-- Right now, @Expr@ and @ExprF@ are completely unrelated. The open type family 'Base' and the type classes
+-- 'Recursive' and 'Corecursive' from [recursion-schemes](https://hackage.haskell.org/package/recursion-schemes)
+-- are exactly what we need.
+--
+-- We can derive 'Recursive' and 'Corecursive' for @Expr@ as long as we derive 'GHC.Generics.Generic' for it, and
+-- define @'Base' Expr ≔ ExprF@ as well as derive 'Functor' for @ExprF@.
+--
+-- >>> import Data.Functor.Foldable (Base, Recursive, Corecursive)
+-- >>> type instance Base Expr = ExprF
+-- >>> deriving stock    instance Functor     ExprF
+-- >>> deriving stock    instance Generic     Expr
+-- >>> deriving anyclass instance Recursive   Expr
+-- >>> deriving anyclass instance Corecursive Expr
+--
+-- With this setup, we can finally derive 'D.FromDhall'\/'D.ToDhall' for @Expr@:
+--
+-- >>> deriving via RecADT Expr instance FromDhall Expr
+-- >>> deriving via RecADT Expr instance ToDhall   Expr
+--
+-- To see how this works, consider this expression representing @(1 + 2) * (3 + 4)@:
+--
+-- >>> expr = Mul (Add (Lit 1) (Lit 2)) (Add (Lit 3) (Lit 4))
+-- >>> import qualified Dhall as D
+-- >>> encodedExpr = D.embed D.inject expr
+--
+-- In Dhall, we can construct an @Expr@ like this:
+--
+-- >>> import qualified Dhall as D
+-- >>> import NeatInterpolation
+-- >>> :{
+-- dhallExpr <- D.inputExpr [trimming|
+--   let ExprF = λ(a : Type) → < LitF : Natural | AddF : { _1 : a, _2 : a } | MulF : { _1 : a, _2 : a } >
+--   let Expr  = ∀(a : Type) → (ExprF a → a) → a
+--   --
+--   let Lit : Natural → Expr     = λ(n : Natural) →
+--     λ(a : Type) → λ(make : ExprF a → a) → make ((ExprF a).LitF n)
+--   --
+--   let Add : Expr → Expr → Expr = λ(x : Expr) → λ(y : Expr) →
+--     λ(a : Type) → λ(make : ExprF a → a) → make ((ExprF a).AddF { _1 = x a make, _2 = y a make })
+--   --
+--   let Mul : Expr → Expr → Expr = λ(x : Expr) → λ(y : Expr) →
+--     λ(a : Type) → λ(make : ExprF a → a) → make ((ExprF a).MulF { _1 = x a make, _2 = y a make })
+--   --
+--   in  Mul (Add (Lit 1) (Lit 2)) (Add (Lit 3) (Lit 4))
+--   |]
+-- :}
+--
+-- In fact, we have
+--
+-- >>> import Dhall.Core (judgmentallyEqual)
+-- >>> encodedExpr `judgmentallyEqual` dhallExpr
+-- True
+-- >>> D.extract @Expr D.auto dhallExpr
+-- Success (Mul (Add (Lit 1) (Lit 2)) (Add (Lit 3) (Lit 4)))
+
+-- $example
+-- #example#
+--
+-- We can still shorten the boilerplate a bit using 'Data.Functor.Foldable.TH.makeBaseFunctor'.
+--
+-- >>> import Data.Functor.Foldable.TH (makeBaseFunctor)
+-- >>> :{
+-- data Tree a = Leaf a | Branch (Tree a) (Tree a)
+-- makeBaseFunctor ''Tree
+-- :}
+--
+-- >>> deriving stock    instance                               Generic   (TreeF a b)
+-- >>> deriving anyclass instance (FromDhall a, FromDhall b) => FromDhall (TreeF a b)
+-- >>> deriving anyclass instance (ToDhall   a, ToDhall   b) => ToDhall   (TreeF a b)
+--
+-- >>> deriving via RecADT (Tree a) instance FromDhall a => FromDhall (Tree a)
+-- >>> deriving via RecADT (Tree a) instance ToDhall   a => ToDhall   (Tree a)
+--
+-- The test suite contains an expanded example of this situation.
+
+-- $utilities
+--
+-- If you don't want to derive 'D.FromDhall'/'D.ToDhall' with @DerivingVia@, use these functions instead.
diff --git a/test/Docspec.hs b/test/Docspec.hs
new file mode 100644
--- /dev/null
+++ b/test/Docspec.hs
@@ -0,0 +1,8 @@
+module Main (main) where
+
+main :: IO ()
+main = do
+  putStrLn "This test-suite exists only to add dependencies"
+  putStrLn "To run docspecs:"
+  putStrLn "    cabal build --enable-tests"
+  putStrLn "    ./docspec.sh"
diff --git a/test/Tasty.hs b/test/Tasty.hs
new file mode 100644
--- /dev/null
+++ b/test/Tasty.hs
@@ -0,0 +1,79 @@
+module Main (main) where
+
+import Control.Monad (join)
+import Data.Coerce (coerce)
+import Data.Either.Validation (Validation (..), validationToEither)
+import Data.Functor.Foldable (Base, Corecursive, Recursive, cata)
+import qualified Dhall as D
+import qualified Dhall.Core as D
+import Dhall.Deriving.Recursive (RecADT (RecADT))
+import GHC.Generics (Generic)
+import Hedgehog
+import qualified Hedgehog.Gen as Gen
+import qualified Hedgehog.Range as Range
+import Numeric.Natural (Natural)
+import Test.Tasty
+import Test.Tasty.HUnit
+import Test.Tasty.Hedgehog
+
+data Tree a = Leaf a | Branch (Tree a) (Tree a)
+  deriving stock (Show, Eq, Generic)
+  deriving anyclass (Recursive, Corecursive)
+  deriving (D.FromDhall, D.ToDhall) via (RecADT (Tree a))
+
+type instance Base (Tree a) = TreeF a
+
+data TreeF a b = LeafF a | BranchF b b
+  deriving stock (Functor, Generic)
+  deriving anyclass (D.FromDhall, D.ToDhall)
+
+main :: IO ()
+main = do
+  let fld = ("(./test/tree.dhall)." <>)
+  dhallTree <- D.inputExpr $ fld "exampleTree"
+  dhallLeafList :: Tree Natural -> [Natural] <- D.input D.auto $ fld "leafList"
+
+  defaultMain . testGroup "tests" $
+    [ testCase "Haskell → Dhall" $
+        JExpr dhallTree @=? JExpr do D.embed D.inject haskellTree,
+      testCase "Dhall → Haskell" $
+        assertValidation haskellTree $ D.extract D.auto dhallTree,
+      testProperty "Dhall function = Haskell function" $ property do
+        t <- forAll genTree
+        dhallLeafList t === haskellLeafList t,
+      testProperty "roundtrip Haskell → Dhall → Haskell" $ property do
+        t <- forAll genTree
+        let roundtrip = D.extract D.auto . D.embed D.inject
+        t' <- evalEither . validationToEither $ roundtrip t
+        t === t',
+      testProperty "roundtrip Dhall → Haskell → Dhall" $ property do
+        t <- D.embed D.inject <$> forAll genTree
+        let roundtrip = fmap (D.embed D.inject) . D.extract (D.auto @(Tree Natural))
+        t' <- evalEither . validationToEither $ roundtrip t
+        JExpr t === JExpr t'
+    ]
+  where
+    haskellTree :: Tree Natural
+    haskellTree = Branch (Branch (Branch (Leaf 0) (Leaf 5)) (Branch (Leaf 4) (Leaf 3))) (Leaf 6)
+
+    haskellLeafList :: Tree a -> [a]
+    haskellLeafList = cata \case
+      LeafF a -> [a]
+      BranchF t t' -> t <> t'
+
+    genTree :: MonadGen m => m (Tree Natural)
+    genTree =
+      Gen.recursive
+        Gen.choice
+        [Leaf <$> Gen.integral_ (Range.linear 0 100)]
+        [join Gen.subterm2 genTree Branch]
+
+newtype JExpr s a = JExpr (D.Expr s a)
+  deriving newtype (Show)
+
+instance Eq a => Eq (JExpr s a) where
+  (==) = coerce (D.judgmentallyEqual @a @s @s)
+
+assertValidation :: (HasCallStack, Show e, Show a, Eq a) => a -> Validation e a -> Assertion
+assertValidation a (Success a') = a @=? a'
+assertValidation _ (Failure e) = assertFailure $ show e
diff --git a/test/tree.dhall b/test/tree.dhall
new file mode 100644
--- /dev/null
+++ b/test/tree.dhall
@@ -0,0 +1,43 @@
+let TreeF =
+      λ(A : Type) → λ(b : Type) → < LeafF : A | BranchF : { _1 : b, _2 : b } >
+
+let Tree = λ(A : Type) → ∀(b : Type) → (TreeF A b → b) → b
+
+let Leaf
+    : ∀(A : Type) → A → Tree A
+    = λ(A : Type) →
+      λ(a : A) →
+      λ(b : Type) →
+      λ(make : TreeF A b → b) →
+        make ((TreeF A b).LeafF a)
+
+let Branch
+    : ∀(A : Type) → Tree A → Tree A → Tree A
+    = λ(A : Type) →
+      λ(t : Tree A) →
+      λ(u : Tree A) →
+      λ(b : Type) →
+      λ(make : TreeF A b → b) →
+        make ((TreeF A b).BranchF { _1 = t b make, _2 = u b make })
+
+let leafList
+    : ∀(A : Type) → Tree A → List A
+    = λ(A : Type) →
+      λ(t : Tree A) →
+        t
+          (List A)
+          ( λ(tf : TreeF A (List A)) →
+              merge
+                { LeafF = λ(a : A) → [ a ]
+                , BranchF = λ(t : { _1 : List A, _2 : List A }) → t._1 # t._2
+                }
+                tf
+          )
+
+let l = Leaf Natural
+
+let b = Branch Natural
+
+in  { exampleTree = b (b (b (l 0) (l 5)) (b (l 4) (l 3))) (l 6)
+    , leafList = leafList Natural
+    }