diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,3 @@
+## 0.1
+
+* First version. Released on an unsuspecting world.
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2023, Oleg Grenrus
+
+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 Oleg Grenrus 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/defun.cabal b/defun.cabal
new file mode 100644
--- /dev/null
+++ b/defun.cabal
@@ -0,0 +1,85 @@
+cabal-version:   2.4
+name:            defun
+version:         0.1
+license:         BSD-3-Clause
+license-file:    LICENSE
+author:          Oleg Grenrus <oleg.grenrus@iki.fi>
+maintainer:      Oleg Grenrus <oleg.grenrus@iki.fi>
+category:        Data
+build-type:      Simple
+extra-doc-files: CHANGELOG.md
+tested-with:     GHC ==9.2.8 || ==9.4.8 || ==9.6.3 || ==9.8.1
+synopsis:        Defunctionalization helpers
+description:
+  The package @defun@ provides defunctionalization helpers, most importantly
+  type family 'DeFun.Core.App' allowing to write higher-order type families.
+  The @singletons@ package also has its own type family @Apply@,
+  but the machinery is tied to the @Sing@ / singletons.
+  .
+  Once @UnsaturatedTypeFamilies@ extension is implemented in GHC
+  ([Proposal 242](https://github.com/ghc-proposals/ghc-proposals/pull/242)),
+  this package will become more or less obsolete.
+  .
+  In particular, the @Lam@ counterpart @SLambda@ is specialized to @Sing@ arguments.
+  The @defun@'s @Lam@ is however fully general, so you can use your own singletons
+  or (importantly) singleton-like arguments.
+  .
+  The package provides few defunctionalized functions, and their term-level
+  reflections using @SBool@ and @NP@ data types from @singletons-bool@ and @sop-core@
+  packages respectively.
+  .
+  This is the "batteries-included" variant with "many" dependencies; see the
+  @defun-core@ package and other @defun-*@ dependencies if you need a more limited
+  dependency footprint.
+  .
+  The [first-class-families](https://hackage.haskell.org/package/first-class-families) package has slightly different design,
+  in particular it doesn't reuse existing (nor define) own standalone type families.
+  In @first-class-families@ everything has to be evaluated via its @Eval@ type family (which job is similar to @App@),
+  but @defun@ only makes /higher-order/ type families look different.
+  In short, ergonomics are a bit different.
+
+source-repository head
+  type:     git
+  location: https://github.com/phadej/defun.git
+  subdir:   defun
+
+common language
+  default-language:   Haskell2010
+  default-extensions:
+    DataKinds
+    EmptyCase
+    GADTs
+    KindSignatures
+    NoImplicitPrelude
+    PatternSynonyms
+    PolyKinds
+    RankNTypes
+    ScopedTypeVariables
+    StandaloneKindSignatures
+    TypeApplications
+    TypeFamilies
+    TypeOperators
+    UndecidableInstances
+    ViewPatterns
+
+library
+  import:                   language
+  hs-source-dirs:           src
+  exposed-modules:          DeFun
+  build-depends:
+    , defun-bool  >=0.1 && <0.1.1
+    , defun-core  >=0.1 && <0.1.1
+    , defun-sop   >=0.1 && <0.1.1
+
+  x-docspec-extra-packages: base
+  x-docspec-options:        -XDataKinds -XGADTs -XStandaloneDeriving
+
+test-suite defun-tests
+  import:         language
+  type:           exitcode-stdio-1.0
+  hs-source-dirs: test
+  main-is:        defun-tests.hs
+  build-depends:
+    , base <5
+    , defun
+    , sop-core
diff --git a/src/DeFun.hs b/src/DeFun.hs
new file mode 100644
--- /dev/null
+++ b/src/DeFun.hs
@@ -0,0 +1,130 @@
+{-# LANGUAGE Trustworthy #-}
+module DeFun (
+    -- * Introduction
+    -- $intro
+    --
+
+    -- * Implementation
+    module DeFun.Core,
+    module DeFun.Function,
+    module DeFun.Bool,
+    module DeFun.List,
+    module Data.SOP.NP.DeFun,
+    module SBool.DeFun,
+) where
+
+import Data.SOP.NP.DeFun
+import DeFun.Bool
+import DeFun.Core
+import DeFun.Function
+import DeFun.List
+import SBool.DeFun
+
+-- $intro
+--
+-- This package provides defunctionalization helpers to write
+-- type-level computations.
+--
+-- As [UnsaturatedTypeFamilies](https://github.com/ghc-proposals/ghc-proposals/pull/242) are not yet implemented in the GHC,
+-- we cannot define type-level type families.
+-- Or we can, but we could only apply them to type-constructors:
+--
+-- @
+-- type BadMap :: (a -> b) -> [a] -> [b]
+-- type family BadMap f xs where
+--     BadMap f '[]      = '[]
+--     BadMap f (x : xs) = f x : BadMap f xs
+-- @
+--
+-- can be only applied to type or data-constructors,
+-- i.e. @BadMap Just [1, 2, 3]@ would work, but @BadMap 'Not' [True, False]@
+-- will not.
+--
+-- The trick is to defunctionalize higher-order functions. Instead of taking
+-- a function argument, we'll take a defunctionalization /symbol/,
+-- and use 'App' type family to apply it:
+--
+-- @
+-- type Map :: (a ~> b) -> [a] -> [b]
+-- type family Map f xs where
+--     Map f '[]    = '[]
+--     Map f (x:xs) = f @@ x : Map f xs
+-- @
+--
+-- where '@@' is the application operator.
+--
+-- Now we can call @'Map' 'NotSym' [True, False]@ and it will compute.
+-- The @'Map' Just [1, 2, 3]@ wont work, we need to convert a constuctor
+-- into a symbol @'Map' (Con1 Just) [1, 2, 3]@ works.
+--
+-- Then, the @Map@ itself can be defunctionalized.
+-- We need to define two symbols, as @Map@ takes two arguments:
+--
+-- @
+-- type MapSym :: (a ~> b) ~> [a] ~> [b]
+-- data MapSym f
+-- type instance App MapSym f = MapSym1 f
+--
+-- type MapSym1  :: (a ~> b) -> [a] ~> [b]
+-- data MapSym1 f xs
+-- type instance App (MapSym1 f) xs = Map f xs
+-- @
+--
+-- So far the above is general enough, and is defined in @singletons@
+-- (sans using different names) in a similar way.
+--
+-- Another thing which we also need, is to represent the type-level computation at type level as well.
+-- The @singletons@ package uses @Sing@ type-family, that's the whole package of that package.
+--
+-- However, @Sing@ is quite resticting. For example, one natural "term-level" reflection of lists
+-- is 'Data.SOP.NP.NP' type.
+--
+-- For example given 'Append' type family, we can write a very useful 'append' function:
+--
+-- @
+-- append :: NP a xs -> NP a ys -> NP a (Append xs ys)
+-- append Nil       ys = ys
+-- append (x :* xs) ys = x :* append xs ys
+-- @
+--
+-- @singletons@ machinery doesn't help us define these.
+--
+-- Then 'Append' (and 'append') can be used as an argument (to e.g. 'Map') and 'map':
+-- we can write something like
+--
+-- @
+-- mapAppend xs yss = map (appendSym @@ xs) yss
+-- @
+--
+-- and GHC will infer the type
+--
+-- @
+-- mapAppend :: NP a xs -> NP (NP a) xss -> NP (NP a) (Map (AppendSym1 xs) xss)
+-- @
+--
+-- to that function.
+--
+-- Being able to relatively easily write functions like 'mapAppend'
+-- is the main motivation for creation of @defun@ package.
+--
+-- Another example is append to n-ary sums ('NS'):
+--
+-- @
+-- append_NS :: forall xs ys f sing. NP sing xs -> Either (NS f xs) (NS f ys) -> NS f (Append xs ys)
+-- append_NS _ (Left xs) = goLeft xs where
+--     goLeft :: NS f xs' -> NS f (Append xs' ys)
+--     goLeft (Z x) = Z x
+--     goLeft (S x) = S (goLeft x)
+-- append_NS xs (Right ys0) = goRight xs ys0 where
+--     goRight :: NP sing xs' -> NS f ys -> NS f (Append xs' ys)
+--     goRight Nil       ys = ys
+--     goRight (_ :* xs) ys = S (goRight xs ys)
+-- @
+--
+-- where we use @NP sing@ as an explicit singleton for @xs@,
+-- instead of using @SingI@ from @singletons@ or @All@ from @sop-core@.
+--
+-- In my experience, using explicit "singletons" (especially in a libraries' internal plumbing)
+-- is a lot more convenient than trying to create all required @All@ dictionaries
+-- (then you would need to write everything twice, 'Type' and 'Constraint' versions: i.e. for 'NP' and 'All', or convert back and forth between @NP (Dict c)@ and @All c@).
+--
diff --git a/test/defun-tests.hs b/test/defun-tests.hs
new file mode 100644
--- /dev/null
+++ b/test/defun-tests.hs
@@ -0,0 +1,112 @@
+module Main where
+
+import Data.SOP (NP (..), NS (..))
+import GHC.Generics ((:*:) (..))
+import Prelude (IO, putStrLn, Either (..))
+
+import qualified Prelude as P
+
+import DeFun
+
+main :: IO ()
+main = putStrLn "OK"
+
+-------------------------------------------------------------------------------
+-- mapAppend
+-------------------------------------------------------------------------------
+
+mapAppend :: NP a xs -> NP (NP a) xss -> NP (NP a) (Map (AppendSym1 xs) xss)
+mapAppend xs yss = map (appendSym @@ xs) yss
+
+-------------------------------------------------------------------------------
+-- split_NP
+-------------------------------------------------------------------------------
+
+-- | inverse of 'append'
+split_NP :: NP pa xs -> NP a (Append xs ys) -> (NP a xs, NP a ys)
+split_NP Nil       xys        = (Nil, xys)
+split_NP (_ :* ps) (x :* xys) = let (xs, ys) = split_NP ps xys in (x :* xs, ys)
+
+-------------------------------------------------------------------------------
+-- FLATTEN utils
+-------------------------------------------------------------------------------
+
+map_NS :: Lam a b f -> NS a xs -> NS b (Map f xs)
+map_NS f (Z x)  = Z (f @@ x)
+map_NS f (S xs) = S (map_NS f xs)
+
+map_NS' :: Lam (px :*: a) b f -> NP px xs -> NS a xs -> NS b (Map f xs)
+map_NS' _ Nil         x      = case x of {}
+map_NS' f (px :* _)   (Z x)  = Z (f @@ (px :*: x))
+map_NS' f (_  :* pxs) (S xs) = S (map_NS' f pxs xs)
+
+append_NS :: forall xs ys f sing. NP sing xs -> Either (NS f xs) (NS f ys) -> NS f (Append xs ys)
+append_NS _ (Left xs) = goLeft xs where
+    goLeft :: NS f xs' -> NS f (Append xs' ys)
+    goLeft (Z x) = Z x
+    goLeft (S x) = S (goLeft x)
+append_NS xs (Right ys0) = goRight xs ys0 where
+    goRight :: NP sing xs' -> NS f ys -> NS f (Append xs' ys)
+    goRight Nil        ys = ys
+    goRight (_ :* xs') ys = S (goRight xs' ys)
+
+concatMap_NS :: Lam pa (NP pb) f -> NP pa xs -> Lam a (NS b) f -> NS a xs -> NS b (ConcatMap f xs)
+concatMap_NS pf pxs f = concatMap_NS' pf pxs (Lam (\(_ :*: x) -> f @@ x))
+
+concatMap_NS' :: Lam pa (NP pb) f -> NP pa xs -> Lam (pa :*: a) (NS b) f -> NS a xs -> NS b (ConcatMap f xs)
+concatMap_NS' _  Nil         = \_ xs -> case xs of {}
+concatMap_NS' pf (px :* pxs) = concatMap_NS_aux' pf px pxs
+
+concatMap_NS_aux' :: forall a b f x xs pa pb. Lam pa (NP pb) f -> pa x -> NP pa xs -> Lam (pa :*: a) (NS b) f -> NS a (x : xs) -> NS b (ConcatMap f (x : xs))
+concatMap_NS_aux' pf px _pxs f (Z x) = append_NS
+    @_
+    @(ConcatMap f xs)
+    (pf @@ px)
+    (Left (f @@ (px :*: x)))
+concatMap_NS_aux' pf px pxs f (S xs) = append_NS
+    @_
+    @(ConcatMap f xs)
+    (pf @@ px)
+    (Right (concatMap_NS' pf pxs f xs))
+
+map2_NS :: forall a b c f xs ys pa pb pc.
+    Lam2 pa pb pc f -> NP pa xs -> NP pb ys ->
+    Lam2 a b c f -> NS a xs -> NS b ys -> NS c (Map2 f xs ys)
+map2_NS pf pxs pys f xs ys = concatMap_NS
+    (compSym2 (flipSym2 mapSym pys) pf)
+    pxs
+    (compSym2 (flipSym2 (mkLam2 map_NS) ys) f)
+    xs
+
+sequence_NSNP :: NP (NP sing) xss -> NP (NS f) xss -> NS (NP f) (Sequence xss)
+sequence_NSNP Nil         Nil         = Z Nil
+sequence_NSNP (xs :* xss) (ys :* yss) = map2_NS
+    (con2 (:*))
+    xs
+    (sequence xss)
+    (con2 (:*))
+    ys
+    (sequence_NSNP xss yss)
+
+sequence_NSNP_sym :: Lam (NP (NP sing) :*: NP (NS f)) (NS (NP f)) SequenceSym
+sequence_NSNP_sym = Lam (\(pxss :*: xss) -> sequence_NSNP pxss xss)
+
+-------------------------------------------------------------------------------
+-- FLATTEN
+-------------------------------------------------------------------------------
+
+-- given as sum-of-products of sum-of-products,
+-- we can turn it into big sum-of-products.
+
+flattenList :: [[[[k]]]] -> [[k]]
+flattenList = P.concatMap (P.map P.concat P.. P.sequence)
+
+type FLATTEN xsss = ConcatMap (CompSym2 (MapSym1 ConcatSym) SequenceSym) xsss
+
+-- This is an isomorphism.
+flatten_NSNP :: forall xssss f sing. NP (NP (NP (NP sing))) xssss -> NS (NP (NS (NP f))) xssss -> NS (NP f) (FLATTEN xssss)
+flatten_NSNP pxssss xssss = concatMap_NS'
+    (compSym2 (mapSym1 concatSym) sequenceSym)
+    pxssss
+    (compSym2 (Lam (map_NS concatSym)) sequence_NSNP_sym)
+    xssss