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-sop.cabal b/defun-sop.cabal
new file mode 100644
--- /dev/null
+++ b/defun-sop.cabal
@@ -0,0 +1,50 @@
+cabal-version:   2.4
+name:            defun-sop
+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: lists
+description:
+  This package provides term definitions for type families in "DeFun.List"
+  using 'NP' type from @sop-core@ package.
+
+source-repository head
+  type:     git
+  location: https://github.com/phadej/defun.git
+  subdir:   defun-sop
+
+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:   Data.SOP.NP.DeFun
+  build-depends:
+    , base        ^>=4.16.3.0 || ^>=4.17.2.0 || ^>=4.18.0.0 || ^>=4.19.0.0
+    , defun-core  ^>=0.1
+    , sop-core    ^>=0.5.0.2
+
+  x-docspec-options: -XDataKinds -XGADTs -XStandaloneDeriving
diff --git a/src/Data/SOP/NP/DeFun.hs b/src/Data/SOP/NP/DeFun.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/SOP/NP/DeFun.hs
@@ -0,0 +1,206 @@
+{-# LANGUAGE Trustworthy #-}
+-- |
+--
+-- This module is designed to imported qualified:
+--
+-- @
+-- import qualified Data.SOP.NP.DeFun as NP
+-- @
+--
+module Data.SOP.NP.DeFun (
+    -- * Append
+    Append, AppendSym, AppendSym1,
+    append, appendSym, appendSym1,
+    -- * Map
+    Map, MapSym, MapSym1,
+    map, mapSym, mapSym1,
+    -- * Concat
+    Concat, ConcatSym,
+    concat, concatSym,
+    -- * ConcatMap
+    ConcatMap, ConcatMapSym, ConcatMapSym1,
+    concatMap, concatMapSym, concatMapSym1,
+    -- * Map2
+    Map2, Map2Sym, Map2Sym1, Map2Sym2,
+    map2, map2Sym, map2Sym1, map2Sym2,
+    -- * Sequence
+    Sequence, SequenceSym,
+    sequence, sequenceSym,
+    -- * Foldr
+    Foldr, FoldrSym, FoldrSym1, FoldrSym2,
+    foldr, foldrSym, foldrSym1, foldrSym2,
+    -- * Foldl
+    Foldl, FoldlSym, FoldlSym1, FoldlSym2,
+    foldl, foldlSym, foldlSym1, foldlSym2,
+    -- * ZipWith
+    ZipWith, ZipWithSym, ZipWithSym1, ZipWithSym2,
+    zipWith, zipWithSym, zipWithSym1, zipWithSym2,
+    -- * Reverse
+    Reverse, ReverseSym,
+    reverse, reverseSym,
+) where
+
+import DeFun.List
+
+import Data.SOP.NP (NP (..))
+
+import DeFun.Core
+import DeFun.Function
+
+-- $setup
+-- >>> import Prelude (Char, Maybe (..), Show)
+-- >>> import Numeric.Natural (Natural)
+-- >>> import Data.SOP.NP (NP (..))
+-- >>> import DeFun.Core
+-- >>> :set -dppr-cols9999
+--
+-- >>> data Nat = Z | S Nat
+-- >>> data SNat (n :: Nat) where { SZ :: SNat Z; SS :: SNat n -> SNat (S n) }
+-- >>> deriving instance Show (SNat n)
+
+-------------------------------------------------------------------------------
+-- Append
+-------------------------------------------------------------------------------
+
+append :: NP a xs -> NP a ys -> NP a (Append xs ys)
+append Nil       ys = ys
+append (x :* xs) ys = x :* append xs ys
+
+appendSym :: Lam2 (NP a) (NP a) (NP a) AppendSym
+appendSym = Lam appendSym1
+
+appendSym1 :: NP a xs -> Lam (NP a) (NP a) (AppendSym1 xs)
+appendSym1 xs = Lam (append xs)
+
+-------------------------------------------------------------------------------
+-- Map
+-------------------------------------------------------------------------------
+
+map :: Lam a b f -> NP a xs -> NP b (Map f xs)
+map _ Nil       = Nil
+map f (x :* xs) = f @@ x :* map f xs
+
+mapSym :: Lam (a :~> b) (Lam (NP a) (NP b)) MapSym
+mapSym = Lam mapSym1
+
+mapSym1 :: Lam a b f -> Lam (NP a) (NP b) (MapSym1 f)
+mapSym1 f = Lam (map f)
+
+-------------------------------------------------------------------------------
+-- Concat
+-------------------------------------------------------------------------------
+
+concat :: NP (NP a) xss -> NP a (Concat xss)
+concat Nil         = Nil
+concat (xs :* xss) = append xs (concat xss)
+
+concatSym :: Lam (NP (NP a)) (NP a) ConcatSym
+concatSym = Lam concat
+
+-------------------------------------------------------------------------------
+-- ConcatMap
+-------------------------------------------------------------------------------
+
+concatMap :: Lam a (NP b) f -> NP a xs -> NP b (ConcatMap f xs)
+concatMap _ Nil       = Nil
+concatMap f (x :* xs) = append (f @@ x) (concatMap f xs)
+
+concatMapSym :: Lam2 (a :~> NP b) (NP a) (NP b) ConcatMapSym
+concatMapSym = Lam concatMapSym1
+
+concatMapSym1 :: Lam a (NP b) f -> Lam (NP a) (NP b) (ConcatMapSym1 f)
+concatMapSym1 f = Lam (concatMap f)
+
+-------------------------------------------------------------------------------
+-- Map2
+-------------------------------------------------------------------------------
+
+map2 :: Lam2 a b c f -> NP a xs -> NP b ys -> NP c (Map2 f xs ys)
+map2 f xs ys = concatMap (compSym2 (flipSym2 mapSym ys) f) xs
+
+map2Sym :: Lam3 (a :~> b :~> c) (NP a) (NP b) (NP c) Map2Sym
+map2Sym = Lam map2Sym1
+
+map2Sym1 :: Lam2 a b c f -> Lam2 (NP a) (NP b) (NP c) (Map2Sym1 f)
+map2Sym1 f = Lam (map2Sym2 f)
+
+map2Sym2 :: Lam2 a b c f -> NP a xs -> Lam (NP b) (NP c) (Map2Sym2 f xs)
+map2Sym2 f xs = Lam (map2 f xs)
+
+-------------------------------------------------------------------------------
+-- Sequence
+-------------------------------------------------------------------------------
+
+sequence :: NP (NP a) xss -> NP (NP a) (Sequence xss)
+sequence Nil         = Nil :* Nil
+sequence (xs :* xss) = map2 (con2 (:*)) xs (sequence xss)
+
+sequenceSym :: Lam (NP (NP a)) (NP (NP a)) SequenceSym
+sequenceSym = Lam sequence
+
+-------------------------------------------------------------------------------
+-- Foldr
+-------------------------------------------------------------------------------
+
+foldr :: Lam2 a b b f -> b x -> NP a ys -> b (Foldr f x ys)
+foldr _ z Nil       = z
+foldr f z (x :* xs) = f @@ x @@ (foldr f z xs)
+
+foldrSym :: Lam3 (a :~> b :~> b) b (NP a) b FoldrSym
+foldrSym = Lam foldrSym1
+
+foldrSym1 :: Lam2 a b b f -> Lam2 b (NP a) b (FoldrSym1 f)
+foldrSym1 f = Lam (foldrSym2 f)
+
+foldrSym2 :: Lam2 a b b f -> b x -> Lam (NP a) b (FoldrSym2 f x)
+foldrSym2 f z = Lam (foldr f z)
+
+-------------------------------------------------------------------------------
+-- Foldl
+-------------------------------------------------------------------------------
+
+foldl :: Lam2 b a b f -> b x -> NP a ys -> b (Foldl f x ys)
+foldl _ z Nil       = z
+foldl f z (x :* xs) = foldl f (f @@ z @@ x) xs
+
+foldlSym :: Lam3 (b :~> a :~> b) b (NP a) b FoldlSym
+foldlSym = Lam foldlSym1
+
+foldlSym1 :: Lam2 b a b f -> Lam2 b (NP a) b (FoldlSym1 f)
+foldlSym1 f = Lam (foldlSym2 f)
+
+foldlSym2 :: Lam2 b a b f -> b x -> Lam (NP a) b (FoldlSym2 f x)
+foldlSym2 f z = Lam (foldl f z)
+
+-------------------------------------------------------------------------------
+-- ZipWith
+-------------------------------------------------------------------------------
+
+zipWith :: Lam2 a b c f -> NP a xs -> NP b ys -> NP c (ZipWith f xs ys)
+zipWith _ Nil       _         = Nil
+zipWith _ (_ :* _)  Nil       = Nil
+zipWith f (x :* xs) (y :* ys) = f @@ x @@ y :* zipWith f xs ys
+
+zipWithSym :: Lam3 (a :~> b :~> c) (NP a) (NP b) (NP c) ZipWithSym
+zipWithSym = Lam zipWithSym1
+
+zipWithSym1 :: Lam2 a b c f -> Lam2 (NP a) (NP b) (NP c) (ZipWithSym1 f)
+zipWithSym1 f = Lam (zipWithSym2 f)
+
+zipWithSym2 :: Lam2 a b c f -> NP a xs -> Lam (NP b) (NP c) (ZipWithSym2 f xs)
+zipWithSym2 f xs = Lam (zipWith f xs)
+
+-------------------------------------------------------------------------------
+-- Reverse
+-------------------------------------------------------------------------------
+
+-- |
+--
+-- >>> reverse (SZ :* SS SZ :* SS (SS SZ) :* Nil)
+-- SS (SS SZ) :* SS SZ :* SZ :* Nil
+--
+reverse :: NP a xs -> NP a (Reverse xs)
+reverse = foldl (flipSym1 (con2 (:*))) Nil
+
+reverseSym :: Lam (NP a) (NP a) ReverseSym
+reverseSym = Lam reverse