diff --git a/ChangeLog.md b/ChangeLog.md
new file mode 100644
--- /dev/null
+++ b/ChangeLog.md
@@ -0,0 +1,6 @@
+# Changelog for fcf-graphs
+
+## v0.0.1.0
+
+* `Fcf.Data.Graph` definition and basic functions.
+* `Fcf.Data.AdjacencyMap` definition.
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright Daniel Firth (c) 2021
+
+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 Daniel Firth 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/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,16 @@
+# fcf-graphs
+
+fcf-graphs mimicks
+[algebraic-graphs](https://hackage.haskell.org/package/algebraic-graphs) but
+for type level computations using
+[first-class-families](https://hackage.haskell.org/package/first-class-families).
+
+Provided are the `Graph` and `AdjacencyMap` data types, and several functions
+for each. I believe this can reach api parity with algebraic-graphs. At the
+moment, not everything is implemented, but type-level `simplify` works which is
+interesting.
+
+Note that ordering of underlying lists/maps is a bit weird so be careful. See
+the doctests for examples, and see
+[fcf-containers](https://hackage.haskell.org/package/fcf-containers) for
+reference.
diff --git a/fcf-graphs.cabal b/fcf-graphs.cabal
new file mode 100644
--- /dev/null
+++ b/fcf-graphs.cabal
@@ -0,0 +1,56 @@
+cabal-version: 1.12
+
+-- This file has been generated from package.yaml by hpack version 0.34.4.
+--
+-- see: https://github.com/sol/hpack
+
+name:           fcf-graphs
+version:        0.0.1.0
+synopsis:       Type-level version of algebraic-graphs.
+description:    Type-level version of algebraic-graphs.
+category:       Algebra, Graphs, Types
+author:         Daniel Firth
+maintainer:     dan.firth@homotopic.tech
+copyright:      Daniel Firth
+license:        MIT
+license-file:   LICENSE
+build-type:     Simple
+extra-source-files:
+    README.md
+    ChangeLog.md
+
+source-repository head
+  type: git
+  location: https://gitlab.homotopic.tech/haskell/fcf-graphs
+
+library
+  exposed-modules:
+      Fcf.Data.AdjacencyMap
+      Fcf.Data.Graph
+  other-modules:
+      Paths_fcf_graphs
+  hs-source-dirs:
+      src
+  ghc-options: -Weverything -Wno-all-missed-specialisations -Wno-missing-import-lists -Wno-implicit-prelude -Wno-monomorphism-restriction -Wno-missing-local-signatures -Wno-missing-safe-haskell-mode -Wno-prepositive-qualified-module -Wno-orphans -Wno-safe -Wno-unsafe
+  build-depends:
+      base >=4.7 && <5
+    , fcf-containers >=0.6.0
+    , first-class-families >=0.8.0
+  default-language: Haskell2010
+
+test-suite fcf-graph-test
+  type: exitcode-stdio-1.0
+  main-is: Doctest.hs
+  other-modules:
+      Paths_fcf_graphs
+  hs-source-dirs:
+      test
+  ghc-options: -Weverything -Wno-all-missed-specialisations -Wno-missing-import-lists -Wno-implicit-prelude -Wno-monomorphism-restriction -Wno-missing-local-signatures -Wno-missing-safe-haskell-mode -Wno-prepositive-qualified-module -Wno-orphans -Wno-safe -Wno-unsafe -threaded -rtsopts -with-rtsopts=-N
+  build-depends:
+      Glob
+    , base >=4.7 && <5
+    , doctest
+    , fcf-containers >=0.6.0
+    , fcf-graphs
+    , first-class-families >=0.8.0
+  default-language: Haskell2010
diff --git a/src/Fcf/Data/AdjacencyMap.hs b/src/Fcf/Data/AdjacencyMap.hs
new file mode 100644
--- /dev/null
+++ b/src/Fcf/Data/AdjacencyMap.hs
@@ -0,0 +1,279 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Fcf.Data.AdjacencyMap where
+
+import Fcf
+import Fcf.Class.Bifunctor
+import Fcf.Data.MapC (MapC (..))
+import qualified Fcf.Data.MapC as MapC
+import Fcf.Data.Nat
+import qualified Fcf.Data.Set as S
+import Fcf.Data.Symbol
+
+newtype AdjacencyMap a = AM (MapC.MapC a (S.Set a))
+
+-- | Empty
+--
+-- === __Example__
+--
+-- >>> :kind! (Eval Empty :: AdjacencyMap Nat)
+-- (Eval Empty :: AdjacencyMap Nat) :: AdjacencyMap Nat
+-- = 'AM ('MapC '[])
+data Empty :: Exp (AdjacencyMap a)
+
+type instance Eval Empty = 'AM (Eval MapC.Empty)
+
+-- | Vertex
+--
+-- === __Example__
+--
+-- >>> :kind! (Eval (Vertex 1) :: AdjacencyMap Nat)
+-- (Eval (Vertex 1) :: AdjacencyMap Nat) :: AdjacencyMap Nat
+-- = 'AM ('MapC '[ '(1, 'S.Set '[])])
+data Vertex :: a -> Exp (AdjacencyMap a)
+
+type instance Eval (Vertex a) = 'AM (Eval (MapC.Singleton a =<< S.Empty))
+
+-- | Edge
+--
+-- === __Example__
+--
+-- >>> :kind! (Eval (Edge 1 2) :: AdjacencyMap Nat)
+-- (Eval (Edge 1 2) :: AdjacencyMap Nat) :: AdjacencyMap Nat
+-- = 'AM ('MapC '[ '(1, 'S.Set '[2]), '(2, 'S.Set '[])])
+data Edge :: a -> a -> Exp (AdjacencyMap a)
+
+type instance
+  Eval (Edge x y) =
+    If
+      (Eval (TyEq x y))
+      ('AM (Eval (MapC.Singleton x =<< S.Singleton y)))
+      ('AM (Eval (MapC.FromList ['(x, Eval (S.Singleton y)), '(y, Eval S.Empty)])))
+
+-- | Overlay
+--
+-- === __Example__
+--
+-- >>> :kind! (Eval (Overlay (Eval (Vertex 1)) (Eval (Vertex 2))))
+-- (Eval (Overlay (Eval (Vertex 1)) (Eval (Vertex 2)))) :: AdjacencyMap
+--                                                           Nat
+-- = 'AM ('MapC '[ '(2, 'S.Set '[]), '(1, 'S.Set '[])])
+data Overlay :: AdjacencyMap a -> AdjacencyMap a -> Exp (AdjacencyMap a)
+
+type instance Eval (Overlay ('AM x) ('AM y)) = 'AM (Eval (UnionWith S.Union x y))
+
+-- | Connect
+--
+-- === __Example__
+--
+-- >>> :kind! (Eval (Connect (Eval (Vertex 1)) (Eval (Vertex 2))))
+-- (Eval (Connect (Eval (Vertex 1)) (Eval (Vertex 2)))) :: AdjacencyMap
+--                                                           Nat
+-- = 'AM ('MapC '[ '(1, 'S.Set '[2]), '(2, 'S.Set '[])])
+data Connect :: AdjacencyMap a -> AdjacencyMap a -> Exp (AdjacencyMap a)
+
+type instance Eval (Connect ('AM x) ('AM y)) = 'AM (Eval (UnionsWith S.Union [x, y, Eval (FromSet (ConstFn (Eval (KeysSet y))) (Eval (KeysSet x)))]))
+
+-- | IsEmpty
+--
+-- === __Example__
+--
+-- >>> :kind! (Eval (IsEmpty ('AM ('MapC '[]))))
+-- (Eval (IsEmpty ('AM ('MapC '[])))) :: Bool
+-- = 'True
+data IsEmpty :: AdjacencyMap a -> Exp Bool
+
+type instance Eval (IsEmpty ('AM x)) = Eval (MapC.Null x)
+
+-- | HasVertex
+--
+-- === __Example__
+--
+-- >>> :kind! (Eval (HasVertex 1 (Eval (Vertex 1))))
+-- (Eval (HasVertex 1 (Eval (Vertex 1)))) :: Bool
+-- = 'True
+data HasVertex :: a -> AdjacencyMap a -> Exp Bool
+
+type instance Eval (HasVertex x ('AM y)) = Eval (MapC.Member x y)
+
+-- | HasEdge
+--
+-- === __Example__
+--
+-- >>> :kind! (Eval (HasEdge 1 2 (Eval (Edge 1 2))))
+-- (Eval (HasEdge 1 2 (Eval (Edge 1 2)))) :: Bool
+-- = 'True
+data HasEdge :: a -> a -> AdjacencyMap a -> Exp Bool
+
+type instance Eval (HasEdge x y ('AM z)) = Eval (UnMaybe (Pure 'False) (S.Member y) =<< MapC.Lookup x z)
+
+-- | VertexCount
+--
+-- === __Example__
+--
+-- >>> :kind! (Eval (VertexCount (Eval (Edge 1 2))))
+-- (Eval (VertexCount (Eval (Edge 1 2)))) :: Nat
+-- = 2
+data VertexCount :: AdjacencyMap a -> Exp Nat
+
+type instance Eval (VertexCount ('AM x)) = Eval (MapC.Size x)
+
+-- | EdgeCount
+--
+-- === __Example__
+--
+-- >>> :kind! (Eval (EdgeCount (Eval (Edge 1 2))))
+-- (Eval (EdgeCount (Eval (Edge 1 2)))) :: Nat
+-- = 1
+data EdgeCount :: AdjacencyMap a -> Exp Nat
+
+type instance Eval (EdgeCount ('AM x)) = Eval (Fcf.Foldr (+) 0 =<< Map S.Size =<< MapC.Elems x)
+
+-- | VertexList
+--
+-- === __Example__
+--
+-- >>> :kind! (Eval (VertexList (Eval (Edge 1 2))))
+-- (Eval (VertexList (Eval (Edge 1 2)))) :: [Nat]
+-- = '[1, 2]
+data VertexList :: AdjacencyMap a -> Exp [a]
+
+type instance Eval (VertexList ('AM x)) = Eval (MapC.Keys x)
+
+-- | EdgeList
+--
+-- === __Example__
+--
+-- >>> :kind! (Eval (EdgeList (Eval (Connect (Eval (Vertex 1)) (Eval (Connect (Eval (Vertex 2)) (Eval (Vertex 3))))))))
+-- (Eval (EdgeList (Eval (Connect (Eval (Vertex 1)) (Eval (Connect (Eval (Vertex 2)) (Eval (Vertex 3)))))))) :: [(Nat,
+--                                                                                                                Nat)]
+-- = '[ '(1, 2), '(1, 3), '(2, 3)]
+data EdgeList :: AdjacencyMap a -> Exp [(a, a)]
+
+type instance Eval (EdgeList ('AM x)) = Eval (EComb =<< Map (Second S.ToList) =<< MapC.ToList x)
+
+data EComb :: [(x, [y])] -> Exp [(x, y)]
+
+type instance Eval (EComb '[]) = '[]
+
+type instance Eval (EComb ('(_, '[]) ': xs)) = Eval (EComb xs)
+
+type instance Eval (EComb ('(x, y ': ys) ': xs)) = '(x, y) ': Eval (EComb ('(x, ys) ': xs))
+
+-- | VertexSet
+--
+-- === __Example__
+--
+-- >>> :kind! (Eval (VertexSet (Eval (Edge 1 2))))
+-- (Eval (VertexSet (Eval (Edge 1 2)))) :: S.Set Nat
+-- = 'S.Set '[1, 2]
+data VertexSet :: AdjacencyMap a -> Exp (S.Set a)
+
+type instance Eval (VertexSet ('AM xs)) = Eval (KeysSet xs)
+
+-- | EdgeSet
+--
+-- === __Example__
+--
+-- >>> :kind! (Eval (EdgeSet (Eval (Edge 1 2))))
+-- (Eval (EdgeSet (Eval (Edge 1 2)))) :: S.Set (Nat, Nat)
+-- = 'S.Set '[ '(1, 2)]
+data EdgeSet :: AdjacencyMap a -> Exp (S.Set (a, a))
+
+type instance Eval (EdgeSet xs) = Eval (S.FromList =<< EdgeList xs)
+
+-- | AdjacencyList
+--
+-- === __Example__
+--
+-- >>> :kind! (Eval (AdjacencyList (Eval (Edge 1 2))))
+-- (Eval (AdjacencyList (Eval (Edge 1 2)))) :: [(Nat, [Nat])]
+-- = '[ '(1, '[2]), '(2, '[])]
+data AdjacencyList :: AdjacencyMap a -> Exp [(a, [a])]
+
+type instance Eval (AdjacencyList ('AM xs)) = Eval (Map (Map S.ToList) =<< MapC.ToList xs)
+
+-- | UnionWith
+--
+-- === __Example__
+--
+-- >>> :kind! (Eval (UnionWith (++) (Eval (MapC.FromList ['(5, '["a"]), '(3, '["b"])])) (Eval (MapC.FromList ['(5, '["A"]), '(7, '["C"])]))))
+-- (Eval (UnionWith (++) (Eval (MapC.FromList ['(5, '["a"]), '(3, '["b"])])) (Eval (MapC.FromList ['(5, '["A"]), '(7, '["C"])])))) :: MapC
+--                                                                                                                                      Nat
+--                                                                                                                                      [Symbol]
+-- = 'MapC '[ '(5, '["a", "A"]), '(7, '["C"]), '(3, '["b"])]
+data UnionWith :: (v -> v -> Exp v) -> MapC k v -> MapC k v -> Exp (MapC k v)
+
+type instance
+  Eval (UnionWith f ('MapC m1) m2) =
+    Eval (Fcf.Foldr (UCombW f) m2 m1)
+
+data UCombW :: (v -> v -> Exp v) -> (k, v) -> MapC k v -> Exp (MapC k v)
+
+type instance
+  Eval (UCombW f '(k, v) lst) =
+    Eval (MapC.InsertWith f k v lst)
+
+-- | UnionsWith
+--
+-- === __Example__
+--
+-- >>> :kind! (Eval (UnionsWith (++) ['MapC ['(5, '["a"]), '(3, '["b"])], 'MapC ['(5, '["A"]), '(7, '["C"])], 'MapC ['(5, '["e"]), '(7, '["o"])]]))
+-- (Eval (UnionsWith (++) ['MapC ['(5, '["a"]), '(3, '["b"])], 'MapC ['(5, '["A"]), '(7, '["C"])], 'MapC ['(5, '["e"]), '(7, '["o"])]])) :: MapC
+--                                                                                                                                            Nat
+--                                                                                                                                            [Symbol]
+-- = 'MapC '[ '(7, '["C", "o"]), '(5, '["a", "A", "e"]), '(3, '["b"])]
+data UnionsWith :: (v -> v -> Exp v) -> [MapC k v] -> Exp (MapC k v)
+
+type instance
+  Eval (UnionsWith f xs) =
+    Eval (Fcf.Foldr (UnionWith f) (Eval MapC.Empty) xs)
+
+-- | FromSet
+--
+-- === __Example__
+--
+-- >>> :kind! (Eval (FromSet ((+) 1) ('S.Set [1,2,3])))
+-- (Eval (FromSet ((+) 1) ('S.Set [1,2,3]))) :: MapC Nat Nat
+-- = 'MapC '[ '(1, 2), '(2, 3), '(3, 4)]
+data FromSet :: (k -> Exp a) -> S.Set k -> Exp (MapC k a)
+
+type instance Eval (FromSet f ('S.Set xs)) = Eval (MapC.FromList $ Eval (Map (ToSnd f) xs))
+
+-- | ToFst
+--
+-- === __Example__
+--
+-- >>> :kind! (Eval (ToFst Length ["f", "o", "o"]))
+-- (Eval (ToFst Length ["f", "o", "o"])) :: (Nat, [Symbol])
+-- = '(3, '["f", "o", "o"])
+data ToFst :: (a -> Exp b) -> a -> Exp (b, a)
+
+type instance Eval (ToFst f x) = '(Eval (f x), x)
+
+-- | ToSnd
+--
+-- === __Example__
+--
+-- >>> :kind! (Eval (ToSnd Length ["f", "o", "o"]))
+-- (Eval (ToSnd Length ["f", "o", "o"])) :: ([Symbol], Nat)
+-- = '( '["f", "o", "o"], 3)
+data ToSnd :: (a -> Exp b) -> a -> Exp (a, b)
+
+type instance Eval (ToSnd f x) = '(x, Eval (f x))
+
+-- | KeysSet
+--
+-- === __Example__
+--
+-- >>> :kind! (Eval (KeysSet ('MapC ['(5, "f"), '(3, "o")])))
+-- (Eval (KeysSet ('MapC ['(5, "f"), '(3, "o")]))) :: S.Set Nat
+-- = 'S.Set '[5, 3]
+data KeysSet :: MapC k a -> Exp (S.Set k)
+
+type instance Eval (KeysSet xs) = Eval (S.FromList =<< MapC.Keys xs)
diff --git a/src/Fcf/Data/Graph.hs b/src/Fcf/Data/Graph.hs
new file mode 100644
--- /dev/null
+++ b/src/Fcf/Data/Graph.hs
@@ -0,0 +1,186 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Fcf.Data.Graph where
+
+import Fcf hiding (Map)
+import qualified Fcf.Data.AdjacencyMap as AM
+import Fcf.Data.Nat
+import qualified Fcf.Data.Set as S
+
+data Graph a where
+  Empty :: Graph a
+  Vertex :: a -> Graph a
+  Overlay :: Graph a -> Graph a -> Graph a
+  Connect :: Graph a -> Graph a -> Graph a
+
+-- | Empty
+--
+-- === __Example__
+--
+-- >>> :kind! (Eval Empty :: Graph Nat)
+-- (Eval Empty :: Graph Nat) :: Graph Nat
+-- = 'Empty
+data Empty :: Exp (Graph a)
+
+type instance Eval Empty = 'Empty
+
+-- | Vertex
+--
+-- === __Example__
+--
+-- >>> :kind! (Eval (Vertex 1) :: Graph Nat)
+-- (Eval (Vertex 1) :: Graph Nat) :: Graph Nat
+-- = 'Vertex 1
+data Vertex :: a -> Exp (Graph a)
+
+type instance Eval (Vertex a) = 'Vertex a
+
+-- | Edge
+--
+-- === __Example__
+--
+-- >>> :kind! (Eval (Edge 1 2) :: Graph Nat)
+-- (Eval (Edge 1 2) :: Graph Nat) :: Graph Nat
+-- = 'Connect ('Vertex 1) ('Vertex 2)
+data Edge :: a -> a -> Exp (Graph a)
+
+type instance Eval (Edge x y) = 'Connect ('Vertex x) ('Vertex y)
+
+-- | Overlay
+--
+-- === __Example__
+--
+-- >>> :kind! (Eval (Overlay ('Vertex 1) ('Vertex 2)) :: Graph Nat)
+-- (Eval (Overlay ('Vertex 1) ('Vertex 2)) :: Graph Nat) :: Graph Nat
+-- = 'Overlay ('Vertex 1) ('Vertex 2)
+data Overlay :: Graph a -> Graph a -> Exp (Graph a)
+
+type instance Eval (Overlay x y) = 'Overlay x y
+
+-- | Connect
+--
+-- === __Example__
+--
+-- >>> :kind! (Eval (Connect ('Vertex 1) ('Vertex 2)) :: Graph Nat)
+-- (Eval (Connect ('Vertex 1) ('Vertex 2)) :: Graph Nat) :: Graph Nat
+-- = 'Connect ('Vertex 1) ('Vertex 2)
+data Connect :: Graph a -> Graph a -> Exp (Graph a)
+
+type instance Eval (Connect x y) = 'Connect x y
+
+-- | Map
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (Map ((+) 1) =<< Connect ('Overlay ('Vertex 1) ('Vertex 2)) ('Vertex 3))
+-- Eval (Map ((+) 1) =<< Connect ('Overlay ('Vertex 1) ('Vertex 2)) ('Vertex 3)) :: Graph
+--                                                                                    Nat
+-- = 'Connect ('Overlay ('Vertex 2) ('Vertex 3)) ('Vertex 4)
+data Map :: (a -> Exp b) -> Graph a -> Exp (Graph b)
+
+type instance Eval (Map _ 'Empty) = 'Empty
+
+type instance Eval (Map f ('Vertex a)) = 'Vertex (Eval (f $ a))
+
+type instance Eval (Map f ('Overlay x y)) = 'Overlay (Eval (Map f x)) (Eval (Map f y))
+
+type instance Eval (Map f ('Connect x y)) = 'Connect (Eval (Map f x)) (Eval (Map f y))
+
+-- | Foldg
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (FoldG (Pure 0) Pure (+) (+) =<< Connect ('Overlay ('Vertex 1) ('Vertex 2)) ('Vertex 3))
+-- Eval (FoldG (Pure 0) Pure (+) (+) =<< Connect ('Overlay ('Vertex 1) ('Vertex 2)) ('Vertex 3)) :: Nat
+-- = 6
+data FoldG :: Exp b -> (a -> Exp b) -> (b -> b -> Exp b) -> (b -> b -> Exp b) -> Graph a -> Exp b
+
+type instance Eval (FoldG e _ _ _ 'Empty) = Eval e
+
+type instance Eval (FoldG _ v _ _ ('Vertex x)) = Eval (v x)
+
+type instance Eval (FoldG e v o c ('Overlay x y)) = Eval (o (Eval (FoldG e v o c x)) (Eval (FoldG e v o c y)))
+
+type instance Eval (FoldG e v o c ('Connect x y)) = Eval (c (Eval (FoldG e v o c x)) (Eval (FoldG e v o c y)))
+
+-- | ToAdjacencyMap
+--
+-- === __Example__
+-- >>> :kind! Eval (ToAdjacencyMap (Eval (Edge 1 2)))
+-- Eval (ToAdjacencyMap (Eval (Edge 1 2))) :: AM.AdjacencyMap Nat
+-- = 'AM.AM
+--     ('Fcf.Data.MapC.MapC '[ '(1, 'S.Set '[2]), '(2, 'S.Set '[])])
+data ToAdjacencyMap :: Graph a -> Exp (AM.AdjacencyMap a)
+
+type instance Eval (ToAdjacencyMap x) = Eval (FoldG AM.Empty AM.Vertex AM.Overlay AM.Connect x)
+
+-- | EqR
+--
+-- === __Example__
+-- >>> :kind! Eval (EqR (Eval (Edge 1 3)) (Eval (Edge 1 2)))
+-- Eval (EqR (Eval (Edge 1 3)) (Eval (Edge 1 2))) :: Bool
+-- = 'False
+data EqR :: Graph a -> Graph a -> Exp Bool
+
+type instance Eval (EqR x y) = Eval (TyEq (Eval (ToAdjacencyMap x)) (Eval (ToAdjacencyMap y)))
+
+-- | Size
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (Size =<< Connect ('Overlay ('Vertex 1) ('Vertex 2)) ('Vertex 3))
+-- Eval (Size =<< Connect ('Overlay ('Vertex 1) ('Vertex 2)) ('Vertex 3)) :: Nat
+-- = 3
+data Size :: Graph a -> Exp Nat
+
+type instance Eval (Size g) = Eval (FoldG (Pure 1) (ConstFn 1) (+) (+) g)
+
+-- | HasVertex
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (HasVertex 3 =<< Connect ('Overlay ('Vertex 1) ('Vertex 2)) ('Vertex 3))
+-- Eval (HasVertex 3 =<< Connect ('Overlay ('Vertex 1) ('Vertex 2)) ('Vertex 3)) :: Bool
+-- = 'True
+data HasVertex :: a -> Graph a -> Exp Bool
+
+type instance Eval (HasVertex x g) = Eval (FoldG (Pure 'False) (TyEq x) (||) (||) g)
+
+-- | VertexSet
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (VertexSet =<< Connect ('Overlay ('Vertex 1) ('Vertex 2)) ('Vertex 3))
+-- Eval (VertexSet =<< Connect ('Overlay ('Vertex 1) ('Vertex 2)) ('Vertex 3)) :: S.Set
+--                                                                                  Nat
+-- = 'S.Set '[3, 2, 1]
+data VertexSet :: Graph a -> Exp (S.Set a)
+
+type instance Eval (VertexSet g) = Eval (FoldG S.Empty S.Singleton S.Union S.Union g)
+
+-- | Simplify
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (Simplify =<< Overlay ('Vertex 1) ('Overlay ('Vertex 2) ('Vertex 1)))
+-- Eval (Simplify =<< Overlay ('Vertex 1) ('Overlay ('Vertex 2) ('Vertex 1))) :: Graph
+--                                                                                 Nat
+-- = 'Overlay ('Vertex 2) ('Vertex 1)
+data Simplify :: Graph a -> Exp (Graph a)
+
+type instance Eval (Simplify x) = Eval (FoldG Empty Vertex (Simple Overlay) (Simple Connect) x)
+
+data Simple :: (Graph a -> Graph a -> Exp (Graph a)) -> Graph a -> Graph a -> Exp (Graph a)
+
+type instance Eval (Simple f x y) = Eval (Simple' x y (Eval (f x y)))
+
+data Simple' :: Graph a -> Graph a -> Graph a -> Exp (Graph a)
+
+type instance
+  Eval (Simple' x y z) =
+    If (Eval (EqR x z)) x (If (Eval (EqR y z)) y z)
diff --git a/test/Doctest.hs b/test/Doctest.hs
new file mode 100644
--- /dev/null
+++ b/test/Doctest.hs
@@ -0,0 +1,16 @@
+import System.FilePath.Glob (glob)
+import Test.DocTest
+
+exts :: [String]
+exts =
+  [ "-XDataKinds",
+    "-XKindSignatures",
+    "-XTypeFamilies",
+    "-XTypeOperators",
+    "-XUndecidableInstances"
+  ]
+
+main :: IO ()
+main = do
+  xs <- glob "src/**/*.hs"
+  doctest (exts ++ xs)