diff --git a/alignment.cabal b/alignment.cabal
--- a/alignment.cabal
+++ b/alignment.cabal
@@ -1,6 +1,6 @@
 cabal-version:        2.4
 name:                 alignment
-version:              0.2.0.0
+version:              0.2.0.1
 synopsis:             Principled functor alignment with leftovers
 description:
                       A principled approach to zipping functors that preserves both matched
@@ -68,6 +68,8 @@
                     , assoc >= 1 && < 2
                     , containers >= 0.6 && < 0.8
                     , vector >= 0.12 && < 0.14
+                    , hedgehog >= 1.0 && < 1.6
+                    , witherable >= 0.4 && < 0.6
 
   hs-source-dirs:     src
 
@@ -94,6 +96,21 @@
   ghc-options:        -Wall
                       -Wno-inline-rule-shadowing
 
+test-suite laws
+  type:               exitcode-stdio-1.0
+  hs-source-dirs:     test
+  main-is:            Laws.hs
+  build-depends:      base >= 4.8 && < 6
+                    , alignment
+                    , hedgehog >= 1.0 && < 1.6
+                    , containers >= 0.6 && < 0.8
+                    , vector >= 0.12 && < 0.14
+  default-language:   Haskell2010
+  ghc-options:        -Wall
+                      -threaded
+                      -rtsopts
+                      -with-rtsopts=-N
+
 benchmark alignment-bench
   type:               exitcode-stdio-1.0
   hs-source-dirs:     bench
@@ -104,6 +121,22 @@
                     , deepseq >= 1.4 && < 1.6
                     , vector >= 0.12 && < 0.14
                     , containers >= 0.6 && < 0.8
+  default-language:   Haskell2010
+  ghc-options:        -Wall
+                      -O2
+                      -threaded
+                      -rtsopts
+                      -with-rtsopts=-N
+
+benchmark zip-unzip-bench
+  type:               exitcode-stdio-1.0
+  hs-source-dirs:     bench
+  main-is:            ZipUnzip.hs
+  build-depends:      base >= 4.8 && < 6
+                    , alignment
+                    , criterion >= 1.5 && < 1.7
+                    , deepseq >= 1.4 && < 1.6
+                    , vector >= 0.12 && < 0.14
   default-language:   Haskell2010
   ghc-options:        -Wall
                       -O2
diff --git a/bench/Main.hs b/bench/Main.hs
--- a/bench/Main.hs
+++ b/bench/Main.hs
@@ -1,14 +1,19 @@
 {-# LANGUAGE ScopedTypeVariables #-}
+
 {- HLINT ignore "Avoid NonEmpty.unzip" -}
 
 module Main where
 
+import Control.DeepSeq (NFData, force)
 import Criterion.Main
 import Data.Alignment
-import qualified Data.Vector as V
-import Data.List.NonEmpty (NonEmpty(..))
-import Control.DeepSeq (NFData, force)
+import qualified Data.Alignment as A
 import Data.Bifunctor (bimap)
+import Data.List.NonEmpty (NonEmpty (..))
+import qualified Data.List.NonEmpty as NE
+import qualified Data.Vector as V
+import Prelude (IO, Int, fmap, fst, id, map, snd, take, uncurry, ($), (*), (+), (.))
+import qualified Prelude as P
 
 -- Force evaluation to prevent benchmark cheating
 forceThis :: (NFData (f (a, b)), NFData (g a), NFData (g b)) => This f g a b -> This f g a b
@@ -16,48 +21,124 @@
 
 -- Benchmark groups
 main :: IO ()
-main = defaultMain
-  [ alignBenchmarks
-  , unalignBenchmarks
-  , roundtripBenchmarks
-  , transformationBenchmarks
-  , fusionBenchmarks
-  ]
+main =
+  defaultMain
+    [ zipVsBaseBenchmarks,
+      unzipVsBaseBenchmarks,
+      alignBenchmarks,
+      unalignBenchmarks,
+      roundtripBenchmarks,
+      transformationBenchmarks,
+      fusionBenchmarks
+    ]
 
+-- | Benchmark Data.Alignment.zip vs Prelude.zip
+zipVsBaseBenchmarks :: Benchmark
+zipVsBaseBenchmarks =
+  bgroup
+    "zip: Data.Alignment vs Prelude"
+    [ bgroup
+        "lists/equal"
+        [ bench "Prelude.zip 100" $ nf (uncurry P.zip) (listPair 100),
+          bench "A.zip 100" $ nf (uncurry A.zip) (listPair 100),
+          bench "Prelude.zip 1000" $ nf (uncurry P.zip) (listPair 1000),
+          bench "A.zip 1000" $ nf (uncurry A.zip) (listPair 1000),
+          bench "Prelude.zip 10000" $ nf (uncurry P.zip) (listPair 10000),
+          bench "A.zip 10000" $ nf (uncurry A.zip) (listPair 10000)
+        ],
+      bgroup
+        "lists/unequal"
+        [ bench "Prelude.zip 100/50" $ nf (\(xs, ys) -> P.zip xs (take 50 ys)) (listPair 100),
+          bench "A.zip 100/50" $ nf (\(xs, ys) -> A.zip xs (take 50 ys)) (listPair 100),
+          bench "Prelude.zip 1000/500" $ nf (\(xs, ys) -> P.zip xs (take 500 ys)) (listPair 1000),
+          bench "A.zip 1000/500" $ nf (\(xs, ys) -> A.zip xs (take 500 ys)) (listPair 1000),
+          bench "Prelude.zip 10000/5000" $ nf (\(xs, ys) -> P.zip xs (take 5000 ys)) (listPair 10000),
+          bench "A.zip 10000/5000" $ nf (\(xs, ys) -> A.zip xs (take 5000 ys)) (listPair 10000)
+        ],
+      bgroup
+        "vectors"
+        [ bench "V.zip 100" $ nf (uncurry V.zip) (vectorPair 100),
+          bench "A.zip 100" $ nf (uncurry A.zip) (vectorPair 100),
+          bench "V.zip 1000" $ nf (uncurry V.zip) (vectorPair 1000),
+          bench "A.zip 1000" $ nf (uncurry A.zip) (vectorPair 1000),
+          bench "V.zip 10000" $ nf (uncurry V.zip) (vectorPair 10000),
+          bench "A.zip 10000" $ nf (uncurry A.zip) (vectorPair 10000)
+        ],
+      bgroup
+        "NonEmpty"
+        [ bench "NE.zip 100" $ nf (uncurry NE.zip) (nePair 100),
+          bench "A.zip 100" $ nf (uncurry A.zip) (nePair 100),
+          bench "NE.zip 1000" $ nf (uncurry NE.zip) (nePair 1000),
+          bench "A.zip 1000" $ nf (uncurry A.zip) (nePair 1000)
+        ]
+    ]
+
+-- | Benchmark Data.Alignment.unzip vs Prelude.unzip
+unzipVsBaseBenchmarks :: Benchmark
+unzipVsBaseBenchmarks =
+  bgroup
+    "unzip: Data.Alignment vs Prelude"
+    [ bgroup
+        "lists"
+        [ bench "Prelude.unzip 100" $ nf P.unzip (pairList 100),
+          bench "A.unzip 100" $ nf A.unzip (pairList 100),
+          bench "Prelude.unzip 1000" $ nf P.unzip (pairList 1000),
+          bench "A.unzip 1000" $ nf A.unzip (pairList 1000),
+          bench "Prelude.unzip 10000" $ nf P.unzip (pairList 10000),
+          bench "A.unzip 10000" $ nf A.unzip (pairList 10000)
+        ],
+      bgroup
+        "vectors"
+        [ bench "V.unzip 100" $ nf V.unzip (V.fromList $ pairList 100),
+          bench "A.unzip 100" $ nf A.unzip (V.fromList $ pairList 100),
+          bench "V.unzip 1000" $ nf V.unzip (V.fromList $ pairList 1000),
+          bench "A.unzip 1000" $ nf A.unzip (V.fromList $ pairList 1000),
+          bench "V.unzip 10000" $ nf V.unzip (V.fromList $ pairList 10000),
+          bench "A.unzip 10000" $ nf A.unzip (V.fromList $ pairList 10000)
+        ],
+      bgroup
+        "NonEmpty"
+        [ bench "NE.unzip 100" $ nf NE.unzip (neList 100),
+          bench "A.unzip 100" $ nf A.unzip (neList 100),
+          bench "NE.unzip 1000" $ nf NE.unzip (neList 1000),
+          bench "A.unzip 1000" $ nf A.unzip (neList 1000)
+        ]
+    ]
+
 -- | Benchmark align vs zip for different sizes and structures
 alignBenchmarks :: Benchmark
-alignBenchmarks = bgroup "align vs zip"
-  [ bgroup "lists"
-      [ bgroup "equal length"
-          [ bench "zip 100" $ nf (uncurry zip) (listPair 100)
-          , bench "align 100" $ nf (uncurry alignList) (listPair 100)
-          , bench "zip 1000" $ nf (uncurry zip) (listPair 1000)
-          , bench "align 1000" $ nf (uncurry alignList) (listPair 1000)
-          , bench "zip 10000" $ nf (uncurry zip) (listPair 10000)
-          , bench "align 10000" $ nf (uncurry alignList) (listPair 10000)
-          ]
-      , bgroup "unequal length"
-          [ bench "zip 100/50" $ nf (\(xs, ys) -> zip xs (take 50 ys)) (listPair 100)
-          , bench "align 100/50" $ nf (\(xs, ys) -> alignList xs (take 50 ys)) (listPair 100)
-          , bench "zip 1000/500" $ nf (\(xs, ys) -> zip xs (take 500 ys)) (listPair 1000)
-          , bench "align 1000/500" $ nf (\(xs, ys) -> alignList xs (take 500 ys)) (listPair 1000)
-          ]
-      ]
-  , bgroup "vectors"
-      [ bgroup "equal length"
-          [ bench "zip 100" $ nf (uncurry V.zip) (vectorPair 100)
-          , bench "align 100" $ nf (uncurry alignVec) (vectorPair 100)
-          , bench "zip 1000" $ nf (uncurry V.zip) (vectorPair 1000)
-          , bench "align 1000" $ nf (uncurry alignVec) (vectorPair 1000)
-          , bench "zip 10000" $ nf (uncurry V.zip) (vectorPair 10000)
-          , bench "align 10000" $ nf (uncurry alignVec) (vectorPair 10000)
-          ]
-      ]
-  , bgroup "NonEmpty"
-      [ bench "align 100" $ nf (uncurry alignNE) (nePair 100)
-      , bench "align 1000" $ nf (uncurry alignNE) (nePair 1000)
-      ]
-  ]
+alignBenchmarks =
+  bgroup
+    "align (full result with leftovers)"
+    [ bgroup
+        "lists"
+        [ bgroup
+            "equal length"
+            [ bench "align 100" $ nf (uncurry alignList) (listPair 100),
+              bench "align 1000" $ nf (uncurry alignList) (listPair 1000),
+              bench "align 10000" $ nf (uncurry alignList) (listPair 10000)
+            ],
+          bgroup
+            "unequal length"
+            [ bench "align 100/50" $ nf (\(xs, ys) -> alignList xs (take 50 ys)) (listPair 100),
+              bench "align 1000/500" $ nf (\(xs, ys) -> alignList xs (take 500 ys)) (listPair 1000)
+            ]
+        ],
+      bgroup
+        "vectors"
+        [ bgroup
+            "equal length"
+            [ bench "align 100" $ nf (uncurry alignVec) (vectorPair 100),
+              bench "align 1000" $ nf (uncurry alignVec) (vectorPair 1000),
+              bench "align 10000" $ nf (uncurry alignVec) (vectorPair 10000)
+            ]
+        ],
+      bgroup
+        "NonEmpty"
+        [ bench "align 100" $ nf (uncurry alignNE) (nePair 100),
+          bench "align 1000" $ nf (uncurry alignNE) (nePair 1000)
+        ]
+    ]
   where
     alignList :: [Int] -> [Int] -> This [] NonEmpty Int Int
     alignList = align
@@ -66,95 +147,113 @@
     alignNE :: NonEmpty Int -> NonEmpty Int -> This NonEmpty NonEmpty Int Int
     alignNE = align
 
--- | Benchmark unalign vs unzip
+-- | Benchmark unalign (recovers full input including leftovers)
 unalignBenchmarks :: Benchmark
-unalignBenchmarks = bgroup "unalign vs unzip"
-  [ bgroup "lists"
-      [ bench "unzip 100" $ nf unzip (pairList 100)
-      , bench "unalign 100" $ nf unalignList (alignedList 100)
-      , bench "unzip 1000" $ nf unzip (pairList 1000)
-      , bench "unalign 1000" $ nf unalignList (alignedList 1000)
-      , bench "unzip 10000" $ nf unzip (pairList 10000)
-      , bench "unalign 10000" $ nf unalignList (alignedList 10000)
-      ]
-  , bgroup "vectors"
-      [ bench "unzip 100" $ nf V.unzip (V.fromList $ pairList 100)
-      , bench "unalign 100" $ nf unalignVec (alignedVector 100)
-      , bench "unzip 1000" $ nf V.unzip (V.fromList $ pairList 1000)
-      , bench "unalign 1000" $ nf unalignVec (alignedVector 1000)
-      , bench "unzip 10000" $ nf V.unzip (V.fromList $ pairList 10000)
-      , bench "unalign 10000" $ nf unalignVec (alignedVector 10000)
-      ]
-  ]
+unalignBenchmarks =
+  bgroup
+    "unalign (full recovery)"
+    [ bgroup
+        "lists"
+        [ bench "unalign 100" $ nf unalignList (alignedList 100),
+          bench "unalign 1000" $ nf unalignList (alignedList 1000),
+          bench "unalign 10000" $ nf unalignList (alignedList 10000)
+        ],
+      bgroup
+        "vectors"
+        [ bench "unalign 100" $ nf unalignVec (alignedVector 100),
+          bench "unalign 1000" $ nf unalignVec (alignedVector 1000),
+          bench "unalign 10000" $ nf unalignVec (alignedVector 10000)
+        ]
+    ]
   where
     unalignList :: This [] NonEmpty Int Int -> ([Int], [Int])
     unalignList = unalign
     unalignVec :: This V.Vector NonEmpty Int Int -> (V.Vector Int, V.Vector Int)
     unalignVec = unalign
 
--- | Benchmark roundtrip: align then unalign
+-- | Benchmark roundtrip: zip then unzip, align then unalign
 roundtripBenchmarks :: Benchmark
-roundtripBenchmarks = bgroup "roundtrip"
-  [ bgroup "lists"
-      [ bench "zip/unzip 100" $ nf (\(xs, ys) -> unzip (zip xs ys)) (listPair 100)
-      , bench "align/unalign 100" $ nf (\(xs, ys) -> unalign (align xs ys :: This [] NonEmpty Int Int)) (listPair 100)
-      , bench "zip/unzip 1000" $ nf (\(xs, ys) -> unzip (zip xs ys)) (listPair 1000)
-      , bench "align/unalign 1000" $ nf (\(xs, ys) -> unalign (align xs ys :: This [] NonEmpty Int Int)) (listPair 1000)
-      ]
-  , bgroup "vectors"
-      [ bench "zip/unzip 100" $ nf (\(xs, ys) -> V.unzip (V.zip xs ys)) (vectorPair 100)
-      , bench "align/unalign 100" $ nf (\(xs, ys) -> unalign (align xs ys :: This V.Vector NonEmpty Int Int)) (vectorPair 100)
-      , bench "zip/unzip 1000" $ nf (\(xs, ys) -> V.unzip (V.zip xs ys)) (vectorPair 1000)
-      , bench "align/unalign 1000" $ nf (\(xs, ys) -> unalign (align xs ys :: This V.Vector NonEmpty Int Int)) (vectorPair 1000)
-      ]
-  ]
+roundtripBenchmarks =
+  bgroup
+    "roundtrip"
+    [ bgroup
+        "lists"
+        [ bench "Prelude zip/unzip 100" $ nf (\(xs, ys) -> P.unzip (P.zip xs ys)) (listPair 100),
+          bench "A zip/unzip 100" $ nf (\(xs, ys) -> A.unzip (A.zip xs ys)) (listPair 100),
+          bench "align/unalign 100" $ nf (\(xs, ys) -> unalign (align xs ys :: This [] NonEmpty Int Int)) (listPair 100),
+          bench "Prelude zip/unzip 1000" $ nf (\(xs, ys) -> P.unzip (P.zip xs ys)) (listPair 1000),
+          bench "A zip/unzip 1000" $ nf (\(xs, ys) -> A.unzip (A.zip xs ys)) (listPair 1000),
+          bench "align/unalign 1000" $ nf (\(xs, ys) -> unalign (align xs ys :: This [] NonEmpty Int Int)) (listPair 1000)
+        ],
+      bgroup
+        "vectors"
+        [ bench "V zip/unzip 100" $ nf (\(xs, ys) -> V.unzip (V.zip xs ys)) (vectorPair 100),
+          bench "A zip/unzip 100" $ nf (\(xs, ys) -> A.unzip (A.zip xs ys)) (vectorPair 100),
+          bench "align/unalign 100" $ nf (\(xs, ys) -> unalign (align xs ys :: This V.Vector NonEmpty Int Int)) (vectorPair 100),
+          bench "V zip/unzip 1000" $ nf (\(xs, ys) -> V.unzip (V.zip xs ys)) (vectorPair 1000),
+          bench "A zip/unzip 1000" $ nf (\(xs, ys) -> A.unzip (A.zip xs ys)) (vectorPair 1000),
+          bench "align/unalign 1000" $ nf (\(xs, ys) -> unalign (align xs ys :: This V.Vector NonEmpty Int Int)) (vectorPair 1000)
+        ]
+    ]
 
 -- | Benchmark transformation operations (map during align/unalign)
 transformationBenchmarks :: Benchmark
-transformationBenchmarks = bgroup "with transformation"
-  [ bgroup "lists"
-      [ bench "map/zip/map 1000" $ nf (\(xs, ys) -> let zs = zip xs ys in (map ((+1) . fst) zs, map ((*2) . snd) zs)) (listPair 1000)
-      , bench "alignWith 1000" $ nf (\(xs, ys) -> alignWith id (+1) (*2) xs ys :: This [] NonEmpty Int Int) (listPair 1000)
-      , bench "unzip/map/map 1000" $ nf (bimap (map (+1)) (map (*2)) . unzip) (pairList 1000)
-      , bench "unalignWith 1000" $ nf (unalignWith (+1) (*2)) (alignedList 1000)
-      ]
-  ]
+transformationBenchmarks =
+  bgroup
+    "with transformation"
+    [ bgroup
+        "lists"
+        [ bench "map/Prelude.zip/map 1000" $ nf (\(xs, ys) -> let zs = P.zip xs ys in (map ((+ 1) . fst) zs, map ((* 2) . snd) zs)) (listPair 1000),
+          bench "map/A.zip/map 1000" $ nf (\(xs, ys) -> let zs = A.zip xs ys in (map ((+ 1) . fst) zs, map ((* 2) . snd) zs)) (listPair 1000),
+          bench "alignWith 1000" $ nf (\(xs, ys) -> alignWith id (+ 1) (* 2) xs ys :: This [] NonEmpty Int Int) (listPair 1000),
+          bench "Prelude.unzip/map/map 1000" $ nf (bimap (map (+ 1)) (map (* 2)) . P.unzip) (pairList 1000),
+          bench "A.unzip/map/map 1000" $ nf (bimap (map (+ 1)) (map (* 2)) . A.unzip) (pairList 1000),
+          bench "unalignWith 1000" $ nf (unalignWith (+ 1) (* 2)) (alignedList 1000)
+        ]
+    ]
 
 -- | Benchmark fusion effectiveness
 fusionBenchmarks :: Benchmark
-fusionBenchmarks = bgroup "fusion"
-  [ bgroup "composition"
-      -- These benchmarks intentionally compare unoptimized vs optimized forms
-      {- HLINT ignore "Functor law" -}
-      {- HLINT ignore "Redundant bimap" -}
-      [ bench "fmap . fmap 1000" $ nf (fmap (*2) . fmap (+1)) (alignedList 1000)
-      , bench "fmap composed 1000" $ nf (fmap ((*2) . (+1))) (alignedList 1000)
-      , bench "bimap . bimap 1000" $ nf (bimap (*2) (*3) . bimap (+1) (+2)) (alignedList 1000)
-      , bench "bimap composed 1000" $ nf (bimap ((*2) . (+1)) ((*3) . (+2))) (alignedList 1000)
-      ]
-  , bgroup "roundtrip elimination"
-      [ bench "align/unalign 1000" $ nf (\(xs, ys) -> unalign (align xs ys :: This [] NonEmpty Int Int)) (listPair 1000)
-      , bench "direct 1000" $ nf id (listPair 1000)
-      , bench "alignWith/unalignWith 1000" $ nf (\(xs, ys) -> unalignWith (+1) (*2) (align xs ys :: This [] NonEmpty Int Int)) (listPair 1000)
-      , bench "map/map 1000" $ nf (bimap (map (+1)) (map (*2))) (listPair 1000)
-      ]
-  ]
+fusionBenchmarks =
+  bgroup
+    "fusion"
+    [ bgroup
+        "composition"
+        -- These benchmarks intentionally compare unoptimized vs optimized forms
+        {- HLINT ignore "Functor law" -}
+        {- HLINT ignore "Redundant bimap" -}
+        [ bench "fmap . fmap 1000" $ nf (fmap (* 2) . fmap (+ 1)) (alignedList 1000),
+          bench "fmap composed 1000" $ nf (fmap ((* 2) . (+ 1))) (alignedList 1000),
+          bench "bimap . bimap 1000" $ nf (bimap (* 2) (* 3) . bimap (+ 1) (+ 2)) (alignedList 1000),
+          bench "bimap composed 1000" $ nf (bimap ((* 2) . (+ 1)) ((* 3) . (+ 2))) (alignedList 1000)
+        ],
+      bgroup
+        "roundtrip elimination"
+        [ bench "align/unalign 1000" $ nf (\(xs, ys) -> unalign (align xs ys :: This [] NonEmpty Int Int)) (listPair 1000),
+          bench "direct 1000" $ nf id (listPair 1000),
+          bench "alignWith/unalignWith 1000" $ nf (\(xs, ys) -> unalignWith (+ 1) (* 2) (align xs ys :: This [] NonEmpty Int Int)) (listPair 1000),
+          bench "map/map 1000" $ nf (bimap (map (+ 1)) (map (* 2))) (listPair 1000)
+        ]
+    ]
 
 -- Test data generators
 listPair :: Int -> ([Int], [Int])
-listPair n = ([1..n], [1..n])
+listPair n = ([1 .. n], [1 .. n])
 
 vectorPair :: Int -> (V.Vector Int, V.Vector Int)
 vectorPair n = (V.enumFromN 1 n, V.enumFromN 1 n)
 
 nePair :: Int -> (NonEmpty Int, NonEmpty Int)
-nePair n = (1 :| [2..n], 1 :| [2..n])
+nePair n = (1 :| [2 .. n], 1 :| [2 .. n])
 
 pairList :: Int -> [(Int, Int)]
-pairList n = [(i, i) | i <- [1..n]]
+pairList n = [(i, i) | i <- [1 .. n]]
 
 alignedList :: Int -> This [] NonEmpty Int Int
-alignedList n = align [1..n] [1..n]
+alignedList n = align [1 .. n] [1 .. n]
 
 alignedVector :: Int -> This V.Vector NonEmpty Int Int
 alignedVector n = align (V.enumFromN 1 n) (V.enumFromN 1 n)
+
+neList :: Int -> NonEmpty (Int, Int)
+neList n = (1, 1) :| [(i, i) | i <- [2 .. n]]
diff --git a/bench/ZipUnzip.hs b/bench/ZipUnzip.hs
new file mode 100644
--- /dev/null
+++ b/bench/ZipUnzip.hs
@@ -0,0 +1,109 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+
+{- HLINT ignore "Avoid NonEmpty.unzip" -}
+
+module Main where
+
+import Control.DeepSeq (force)
+import Criterion.Main
+import Data.Alignment
+import qualified Data.Alignment as A
+import Data.List.NonEmpty (NonEmpty (..))
+import qualified Data.List.NonEmpty as NE
+import qualified Data.Vector as V
+import Prelude (IO, Int, uncurry, ($))
+import qualified Prelude as P
+
+main :: IO ()
+main =
+  defaultMain
+    [ zipBenchmarks,
+      unzipBenchmarks
+    ]
+
+zipBenchmarks :: Benchmark
+zipBenchmarks =
+  bgroup
+    "zip: Data.Alignment vs Base"
+    [ bgroup
+        "lists/equal"
+        [ bench "Prelude.zip 100" $ nf (P.uncurry P.zip) (listPair 100),
+          bench "A.zip 100" $ nf (P.uncurry A.zip) (listPair 100),
+          bench "Prelude.zip 1000" $ nf (P.uncurry P.zip) (listPair 1000),
+          bench "A.zip 1000" $ nf (P.uncurry A.zip) (listPair 1000),
+          bench "Prelude.zip 10000" $ nf (P.uncurry P.zip) (listPair 10000),
+          bench "A.zip 10000" $ nf (P.uncurry A.zip) (listPair 10000)
+        ],
+      bgroup
+        "lists/unequal"
+        [ bench "Prelude.zip 100/50" $ nf (\(xs, ys) -> P.zip xs (P.take 50 ys)) (listPair 100),
+          bench "A.zip 100/50" $ nf (\(xs, ys) -> A.zip xs (P.take 50 ys)) (listPair 100),
+          bench "Prelude.zip 1000/500" $ nf (\(xs, ys) -> P.zip xs (P.take 500 ys)) (listPair 1000),
+          bench "A.zip 1000/500" $ nf (\(xs, ys) -> A.zip xs (P.take 500 ys)) (listPair 1000),
+          bench "Prelude.zip 10000/5000" $ nf (\(xs, ys) -> P.zip xs (P.take 5000 ys)) (listPair 10000),
+          bench "A.zip 10000/5000" $ nf (\(xs, ys) -> A.zip xs (P.take 5000 ys)) (listPair 10000)
+        ],
+      bgroup
+        "vectors"
+        [ bench "V.zip 100" $ nf (P.uncurry V.zip) (vectorPair 100),
+          bench "A.zip 100" $ nf (P.uncurry A.zip) (vectorPair 100),
+          bench "V.zip 1000" $ nf (P.uncurry V.zip) (vectorPair 1000),
+          bench "A.zip 1000" $ nf (P.uncurry A.zip) (vectorPair 1000),
+          bench "V.zip 10000" $ nf (P.uncurry V.zip) (vectorPair 10000),
+          bench "A.zip 10000" $ nf (P.uncurry A.zip) (vectorPair 10000)
+        ],
+      bgroup
+        "NonEmpty"
+        [ bench "NE.zip 100" $ nf (P.uncurry NE.zip) (nePair 100),
+          bench "A.zip 100" $ nf (P.uncurry A.zip) (nePair 100),
+          bench "NE.zip 1000" $ nf (P.uncurry NE.zip) (nePair 1000),
+          bench "A.zip 1000" $ nf (P.uncurry A.zip) (nePair 1000)
+        ]
+    ]
+
+unzipBenchmarks :: Benchmark
+unzipBenchmarks =
+  bgroup
+    "unzip: Data.Alignment vs Base"
+    [ bgroup
+        "lists"
+        [ bench "Prelude.unzip 100" $ nf P.unzip (pairList 100),
+          bench "A.unzip 100" $ nf A.unzip (pairList 100),
+          bench "Prelude.unzip 1000" $ nf P.unzip (pairList 1000),
+          bench "A.unzip 1000" $ nf A.unzip (pairList 1000),
+          bench "Prelude.unzip 10000" $ nf P.unzip (pairList 10000),
+          bench "A.unzip 10000" $ nf A.unzip (pairList 10000)
+        ],
+      bgroup
+        "vectors"
+        [ bench "V.unzip 100" $ nf V.unzip (V.fromList $ pairList 100),
+          bench "A.unzip 100" $ nf A.unzip (V.fromList $ pairList 100),
+          bench "V.unzip 1000" $ nf V.unzip (V.fromList $ pairList 1000),
+          bench "A.unzip 1000" $ nf A.unzip (V.fromList $ pairList 1000),
+          bench "V.unzip 10000" $ nf V.unzip (V.fromList $ pairList 10000),
+          bench "A.unzip 10000" $ nf A.unzip (V.fromList $ pairList 10000)
+        ],
+      bgroup
+        "NonEmpty"
+        [ bench "NE.unzip 100" $ nf NE.unzip (neList 100),
+          bench "A.unzip 100" $ nf A.unzip (neList 100),
+          bench "NE.unzip 1000" $ nf NE.unzip (neList 1000),
+          bench "A.unzip 1000" $ nf A.unzip (neList 1000)
+        ]
+    ]
+
+-- Test data generators
+listPair :: Int -> ([Int], [Int])
+listPair n = ([1 .. n], [1 .. n])
+
+vectorPair :: Int -> (V.Vector Int, V.Vector Int)
+vectorPair n = (V.enumFromN 1 n, V.enumFromN 1 n)
+
+nePair :: Int -> (NonEmpty Int, NonEmpty Int)
+nePair n = (1 :| [2 .. n], 1 :| [2 .. n])
+
+pairList :: Int -> [(Int, Int)]
+pairList n = [(i, i) | i <- [1 .. n]]
+
+neList :: Int -> NonEmpty (Int, Int)
+neList n = (1, 1) :| [(i, i) | i <- [2 .. n]]
diff --git a/changelog.md b/changelog.md
--- a/changelog.md
+++ b/changelog.md
@@ -1,3 +1,17 @@
+0.2.0.1 (2026-05-19)
+
+* Add comprehensive Hedgehog property-based test suite (52 tests covering all laws)
+* Add test suite for Functor, Bifunctor, Semialign, Align, and Unalign laws
+* Tests cover all instances: List, Maybe, NonEmpty, Vector, Seq, Map, IntMap, Identity, ZipList
+* Add hedgehog dependency to library for doctest examples
+* Add 3 hedgehog property tests embedded in doctests
+* Expand law documentation with additional doctest examples
+* Total 244 doctests (up from 227), all passing
+* Note: Map and IntMap documented to intentionally fail symmetry law with disjoint keys
+* Remove explanatory notes about non-existent instances (Apply, Selective, Extend, Alt)
+* Apply hlint suggestion to simplify lambda in Witherable instance
+* Format entire codebase with ormolu
+
 0.2.0.0 (2026-05-19)
 
 * Add `Unalign` type class for recovering original functors from alignment
diff --git a/src/Data/Alignment.hs b/src/Data/Alignment.hs
--- a/src/Data/Alignment.hs
+++ b/src/Data/Alignment.hs
@@ -3,7 +3,6 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TupleSections #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE NoImplicitPrelude #-}
@@ -27,6 +26,10 @@
     Align (..),
     Unalign (..),
 
+    -- * Zip and unzip (dropping leftovers)
+    zip,
+    unzip,
+
     -- * Lenses
     these,
     those,
@@ -92,8 +95,10 @@
     _Left,
     _Right,
   )
+import Data.Biapplicative (Biapplicative (..))
 import Data.Bifoldable (Bifoldable (bifoldMap))
 import Data.Bifunctor (Bifunctor (bimap), second)
+import Data.Bifunctor.Apply (Biapply (..))
 import Data.Bifunctor.Swap (Swap (..))
 import Data.Bitraversable (Bitraversable (..))
 import Data.Bool (Bool (False, True), otherwise, (&&))
@@ -101,7 +106,6 @@
 import Data.Eq (Eq ((==)))
 import Data.Foldable (Foldable (foldMap), traverse_)
 import Data.Function (const, flip, ($))
-import Data.Tuple (uncurry)
 import Data.Functor (Functor (fmap), ($>), (<$))
 import Data.Functor.Apply (Apply ((<.>)), (.>))
 import Data.Functor.Classes
@@ -133,11 +137,13 @@
 import Data.Sequence (Seq)
 import qualified Data.Sequence as Seq
 import Data.Traversable (Traversable (traverse))
+import Data.Tuple (uncurry)
 import Data.Vector (Vector)
 import qualified Data.Vector as Vector
 import GHC.Generics (Generic, Generic1)
 import GHC.Show (Show (showsPrec))
 import Text.Show (showList, showParen, showString)
+import Witherable (Filterable (..), Witherable (..))
 
 -- $setup
 -- >>> import Prelude
@@ -147,6 +153,12 @@
 -- >>> import qualified Data.Map as Map
 -- >>> import qualified Data.IntMap as IntMap
 -- >>> import Data.Functor.Const (Const(..))
+-- >>> import Hedgehog
+-- >>> import qualified Hedgehog.Gen as Gen
+-- >>> import qualified Hedgehog.Range as Range
+-- >>> let genList = Gen.list (Range.linear 0 20) (Gen.int (Range.linear (-100) 100))
+-- >>> let genNonEmpty g = (:|) <$> g <*> genList
+-- >>> let genInt = Gen.int (Range.linear (-100) 100)
 
 -- | Alignment result type combining matched pairs with leftovers
 --
@@ -363,6 +375,108 @@
   bimap fa fb (This t r) =
     This (fmap (bimap fa fb) t) (fmap (bimap (fmap fa) (fmap fb)) r)
 
+-- | Biapply instance - applies bifunctions to bivalues
+--
+-- The Biapply instance combines two This values by:
+-- - Applying paired functions to paired values using Apply on the container f
+-- - Applying functions in left leftovers to values in left leftovers using Apply on g
+-- - Applying functions in right leftovers to values in right leftovers using Apply on g
+--
+-- This enables biapplicative-style computations without requiring bipure.
+--
+-- >>> This [((\x -> x * 10), (\y -> y * 100))] Nothing <<.>> This [(1, 2)] Nothing :: This [] NonEmpty Int Int
+-- This [(10,200)] Nothing
+-- >>> This [] (Just (Left ((+1) :| []))) <<.>> This [] (Just (Left (5 :| []))) :: This [] NonEmpty Int Int
+-- This [] (Just (Left (6 :| [])))
+-- >>> This [] (Just (Right ((+10) :| []))) <<.>> This [] (Just (Right (5 :| []))) :: This [] NonEmpty Int Int
+-- This [] (Just (Right (15 :| [])))
+instance (Apply f, Apply g) => Biapply (This f g) where
+  This tf tr <<.>> This tx xr =
+    This (liftF2 applyPair tf tx) (applyLeftovers tr xr)
+    where
+      applyPair (fa, fb) (a, b) = (fa a, fb b)
+      liftF2 h fa fb = h <$> fa <.> fb
+      applyLeftovers Nothing Nothing = Nothing
+      applyLeftovers (Just _) Nothing = Nothing -- Can't apply without values
+      applyLeftovers Nothing (Just _) = Nothing -- Can't apply without functions
+      applyLeftovers (Just (Left gfa)) (Just (Left ga)) = Just (Left (gfa <.> ga))
+      applyLeftovers (Just (Right gfb)) (Just (Right gb)) = Just (Right (gfb <.> gb))
+      applyLeftovers (Just (Left _)) (Just (Right _)) = Nothing -- Type mismatch
+      applyLeftovers (Just (Right _)) (Just (Left _)) = Nothing -- Type mismatch
+  {-# INLINE (<<.>>) #-}
+
+-- | Biapplicative instance - pure bifunctor with application
+--
+-- The Biapplicative instance provides 'bipure' which lifts two values into a This
+-- with a single matched pair and no leftovers. This requires the container f to be
+-- Applicative so we can create the paired structure.
+--
+-- This is useful for building This values from pure values and then combining them
+-- with applicative operations.
+--
+-- >>> bipure 1 2 :: This [] NonEmpty Int Int
+-- This [(1,2)] Nothing
+-- >>> bipure 'a' 'b' :: This Maybe Identity Char Char
+-- This (Just ('a','b')) Nothing
+-- >>> bipure (+10) (*20) <<*>> bipure 1 2 :: This [] NonEmpty Int Int
+-- This [(11,40)] Nothing
+instance (Applicative f, Applicative g) => Biapplicative (This f g) where
+  bipure a b = This (pure (a, b)) Nothing
+  {-# INLINE bipure #-}
+
+  -- Implementation matches Biapply but uses Applicative operations
+  This tf tr <<*>> This tx xr =
+    This (applyPair <$> tf <*> tx) (applyLeftovers tr xr)
+    where
+      applyPair (fa, fb) (a, b) = (fa a, fb b)
+      applyLeftovers Nothing Nothing = Nothing
+      applyLeftovers (Just _) Nothing = Nothing -- Can't apply without values
+      applyLeftovers Nothing (Just _) = Nothing -- Can't apply without functions
+      applyLeftovers (Just (Left gfa)) (Just (Left ga)) = Just (Left (gfa <*> ga))
+      applyLeftovers (Just (Right gfb)) (Just (Right gb)) = Just (Right (gfb <*> gb))
+      applyLeftovers (Just (Left _)) (Just (Right _)) = Nothing -- Type mismatch
+      applyLeftovers (Just (Right _)) (Just (Left _)) = Nothing -- Type mismatch
+  {-# INLINE (<<*>>) #-}
+
+-- | Filterable instance - filter elements based on a predicate
+--
+-- The Filterable instance allows filtering values in the b position while
+-- preserving the structure. This is useful for removing unwanted alignment
+-- results or transforming values that might fail.
+--
+-- >>> mapMaybe (\x -> if even x then Just (x * 10) else Nothing) (This [(1,2),(3,4)] Nothing :: This [] Maybe Int Int)
+-- This [(1,20),(3,40)] Nothing
+-- >>> mapMaybe (\x -> if x > 10 then Just x else Nothing) (This [(1,2)] (Just (Right (Just 15))) :: This [] Maybe Int Int)
+-- This [(1,2)] (Just (Right (Just 15)))
+-- >>> catMaybes (This [(1, Just 2), (3, Nothing)] Nothing :: This [] Maybe Int (Maybe Int))
+-- This [(1,2)] Nothing
+instance (Filterable f, Filterable g) => Filterable (This f g a) where
+  mapMaybe f (This t r) =
+    This (mapMaybe filterPair t) (fmap (fmap (mapMaybe f)) r)
+    where
+      filterPair (a, b) = case f b of
+        Nothing -> Nothing
+        Just c -> Just (a, c)
+  {-# INLINE mapMaybe #-}
+
+-- | Witherable instance - filter with effects
+--
+-- The Witherable instance extends Filterable to support effectful filtering.
+-- This is useful when the filtering predicate needs to perform IO, access
+-- state, or use other effects.
+--
+-- >>> wither (\x -> if even x then Just (Just (x * 10)) else Just Nothing) (This [(1,2),(3,4)] Nothing :: This [] Maybe Int Int)
+-- Just (This [(1,20),(3,40)] Nothing)
+-- >>> wither (\x -> if x > 10 then pure (Just x) else pure Nothing) (This [(1,2)] (Just (Right (Just 15))) :: This [] Maybe Int Int)
+-- Just (This [(1,2)] (Just (Right (Just 15))))
+instance (Witherable f, Witherable g) => Witherable (This f g a) where
+  wither f (This t r) =
+    This <$> wither witherPair t <*> traverse (traverse (wither f)) r
+    where
+      witherPair (a, b) =
+        fmap (fmap (a,)) (f b)
+  {-# INLINE wither #-}
+
 -- | Swap instance - swaps the two type parameters
 --
 -- >>> swap (This [(1,'a')] Nothing :: This [] NonEmpty Int Char)
@@ -386,32 +500,32 @@
   {-# INLINE rnf #-}
 
 -- * Functor/Bifunctor/Swap fusion rules
+
 --
 -- These rules optimize composition of mapping and swapping operations on This.
 -- Phase [2] ensures they fire after instance resolution.
 
 {-# RULES
-
 -- Functor composition on This - reduces to single traversal
 "fmap/fmap/This" [2] forall f g (x :: This [] NonEmpty a b).
-  fmap f (fmap g x) = fmap (f . g) x
-
+  fmap f (fmap g x) =
+    fmap (f . g) x
 -- Bifunctor composition on This - reduces to single traversal
 "bimap/bimap/This" [2] forall f1 f2 g1 g2 (x :: This [] NonEmpty a b).
-  bimap f1 g1 (bimap f2 g2 x) = bimap (f1 . f2) (g1 . g2) x
-
+  bimap f1 g1 (bimap f2 g2 x) =
+    bimap (f1 . f2) (g1 . g2) x
 -- Swap involution - swap is its own inverse, complete elimination
 "swap/swap/This" [2] forall (x :: This [] NonEmpty a b).
-  swap (swap x) = x
-
+  swap (swap x) =
+    x
 -- Swap and bimap commute by swapping function arguments
 "swap/bimap/This" [2] forall f g (x :: This [] NonEmpty a b).
-  swap (bimap f g x) = bimap g f (swap x)
-
+  swap (bimap f g x) =
+    bimap g f (swap x)
 -- bimap and swap commute (reverse direction)
 "bimap/swap/This" [2] forall f g (x :: This [] NonEmpty a b).
-  bimap f g (swap x) = swap (bimap g f x)
-
+  bimap f g (swap x) =
+    swap (bimap g f x)
   #-}
 
 -- | Semigroup instance - combines two This values by combining their components
@@ -631,6 +745,7 @@
   {-# INLINE alignWith' #-}
 
 -- * Fusion rules
+
 --
 -- These RULES enable GHC to fuse operations for better performance,
 -- eliminating intermediate This allocations where possible.
@@ -640,27 +755,25 @@
 -- with earlier optimization phases.
 
 {-# RULES
-
 -- Naturality fusion: fuse bimap into align
 -- Implements the semialignNaturality law as a rewrite rule
 "semialign/naturality" [2] forall f g xs ys.
-  bimap f g (align xs ys) = alignWith (bimap f g) f g xs ys
-
+  bimap f g (align xs ys) =
+    alignWith (bimap f g) f g xs ys
 -- Composition fusion for alignWith followed by bimap
 "alignWith/bimap" [2] forall w x y k l xs ys.
   bimap k l (alignWith w x y xs ys) =
     alignWith (bimap k l . w) (k . x) (l . y) xs ys
-
 -- Symmetry via swap: align x y = swap (align y x)
 -- Can enable other optimizations when combined with swap rules
 "align/swap/symmetry" [2] forall x y.
-  swap (align y x) = align x y
-
+  swap (align y x) =
+    align x y
 -- fmap can be expressed as bimap with identity on first param
 -- Allows bimap rules to catch fmap patterns
 "fmap/as/bimap" [2] forall f (x :: This [] NonEmpty a b).
-  fmap f x = bimap id f x
-
+  fmap f x =
+    bimap id f x
   #-}
 
 -- | Semialign instance for Identity - always produces a perfect match
@@ -692,7 +805,7 @@
     This [] (Just (Right (b :| bs)))
   align [] [] =
     This [] Nothing
-  {-# INLINABLE align #-}
+  {-# INLINEABLE align #-}
 
 -- | Semialign instance for Maybe - aligns optional values
 --
@@ -713,7 +826,7 @@
     This Nothing (Just (Right (Identity b)))
   align Nothing Nothing =
     This Nothing Nothing
-  {-# INLINABLE align #-}
+  {-# INLINEABLE align #-}
 
 -- | Semialign instance for NonEmpty - aligns non-empty lists
 --
@@ -735,7 +848,7 @@
   align (h1 :| i1 : r1) (h2 :| i2 : r2) =
     let This t r = align (i1 :| r1) (i2 :| r2)
      in This ((h1, h2) `NonEmpty.cons` t) r
-  {-# INLINABLE align #-}
+  {-# INLINEABLE align #-}
 
 -- | Semialign instance for ZipList - delegates to list alignment
 --
@@ -745,7 +858,7 @@
 instance Semialign ZipList NonEmpty where
   align (ZipList a) (ZipList b) =
     over these ZipList (align a b)
-  {-# INLINABLE align #-}
+  {-# INLINEABLE align #-}
 
 -- | Semialign instance for Seq - aligns sequences element-wise
 --
@@ -767,7 +880,7 @@
       toList s = case Seq.viewl s of
         Seq.EmptyL -> []
         x Seq.:< xs -> x : toList xs
-  {-# INLINABLE align #-}
+  {-# INLINEABLE align #-}
 
 -- | Semialign instance for Vector - aligns vectors element-wise
 --
@@ -790,7 +903,7 @@
                 (y : ys) -> Just (Right (y :| ys))
           | otherwise = Nothing
      in This paired leftover
-  {-# INLINABLE align #-}
+  {-# INLINEABLE align #-}
 
 -- | Semialign instance for Map - aligns by keys
 --
@@ -809,7 +922,7 @@
           (True, False) -> Just (Right onlyRight)
           (False, False) -> Just (Left onlyLeft) -- Left takes precedence
      in This both leftover
-  {-# INLINABLE align #-}
+  {-# INLINEABLE align #-}
 
 -- | Semialign instance for IntMap - aligns by Int keys
 --
@@ -828,7 +941,7 @@
           (True, False) -> Just (Right onlyRight)
           (False, False) -> Just (Left onlyLeft)
      in This both leftover
-  {-# INLINABLE align #-}
+  {-# INLINEABLE align #-}
 
 -- | Semialign instance for functions - pointwise alignment
 --
@@ -987,10 +1100,6 @@
   nil = Const mempty
   {-# INLINE nil #-}
 
--- Note: Product and Compose instances would require more complex type machinery
--- and are omitted for simplicity. They could be added with careful handling of
--- the leftover types.
-
 -- | Unalign type class - recover original functors from alignment
 --
 -- Not all Semialign instances can be Unalign. This class is for functors
@@ -1023,20 +1132,6 @@
 --
 --   Where @to aligned = uncurry align@ and @from aligned = unalign@.
 --
--- = Important Notes
---
--- Not all Semialign instances can be Unalign instances:
---
--- * Sequence types ([], Maybe, NonEmpty, Vector, Seq, etc.) ✓ Can unalign
--- * Function types ((->) r) ✗ Cannot meaningfully merge functions with constants
--- * Pair types ((,) e) ✗ Would require duplicating the first component
--- * Map and IntMap ✗ Violate roundtrip law when both sides have leftovers
---
--- For Map and IntMap, when both sides have leftovers, 'align' keeps only left
--- leftovers (left takes precedence), so 'unalign' cannot recover the original
--- right-side keys. We choose not to provide these instances to keep the type
--- class lawful.
---
 -- See 'unalignRoundtrip' and 'unalignNaturality' for testable property functions.
 --
 -- >>> unalign (align [1,2,3] [10,20] :: This [] NonEmpty Int Int)
@@ -1096,29 +1191,78 @@
 unaligned = iso unalign (uncurry align)
 {-# INLINE unaligned #-}
 
+-- | Zip two functors together, dropping any leftover elements
+--
+-- This is like 'align' but extracts only the matched pairs, discarding
+-- leftovers. It behaves like Prelude's 'Prelude.zip' but works for any
+-- Semialign instance.
+--
+-- >>> Data.Alignment.zip [1,2,3] [10,20] :: [(Int, Int)]
+-- [(1,10),(2,20)]
+-- >>> Data.Alignment.zip [1,2] [10,20,30] :: [(Int, Int)]
+-- [(1,10),(2,20)]
+-- >>> Data.Alignment.zip [1,2] [10,20] :: [(Int, Int)]
+-- [(1,10),(2,20)]
+-- >>> Data.Alignment.zip (Just 1) (Just 2) :: Maybe (Int, Int)
+-- Just (1,2)
+-- >>> Data.Alignment.zip (Just 1) Nothing :: Maybe (Int, Int)
+-- Nothing
+-- >>> Data.Alignment.zip (1 :| [2,3]) (10 :| [20]) :: NonEmpty (Int, Int)
+-- (1,10) :| [(2,20)]
+zip ::
+  (Semialign f g) =>
+  f a ->
+  f b ->
+  f (a, b)
+zip xs ys = view these (align xs ys)
+{-# INLINE zip #-}
+
+-- | Unzip a functor of pairs into a pair of functors, dropping leftovers
+--
+-- This is the inverse of 'zip'. For Unalign instances, it extracts the
+-- two components from a paired structure.
+--
+-- >>> Data.Alignment.unzip [(1,10),(2,20)] :: ([Int], [Int])
+-- ([1,2],[10,20])
+-- >>> Data.Alignment.unzip (Just (1,2)) :: (Maybe Int, Maybe Int)
+-- (Just 1,Just 2)
+-- >>> Data.Alignment.unzip Nothing :: (Maybe Int, Maybe Int)
+-- (Nothing,Nothing)
+-- >>> Data.Alignment.unzip ((1,10) :| [(2,20)]) :: (NonEmpty Int, NonEmpty Int)
+-- (1 :| [2],10 :| [20])
+--
+-- Note: This produces the same paired results as 'unalign', but any
+-- leftovers present in the original alignment are lost.
+unzip ::
+  (Unalign f g, Functor f) =>
+  f (a, b) ->
+  (f a, f b)
+unzip pairs = unalign (This pairs Nothing)
+{-# INLINE unzip #-}
+
 -- * Unalign fusion rules
+
 --
 -- Additional fusion rules specific to Unalign instances.
 --
 -- Phase [2] ensures these fire after class method specialization.
 
 {-# RULES
-
 -- Roundtrip elimination: unalign immediately after align
 -- Implements the unalignRoundtrip law as a rewrite rule
 "unalign/align/roundtrip" [2] forall xs ys.
-  unalign (align xs ys) = (xs, ys)
-
+  unalign (align xs ys) =
+    (xs, ys)
 -- Naturality for unalign: push bimap through unalign
 -- Implements the unalignNaturality law as a rewrite rule
 "unalign/bimap/naturality" [2] forall f g this.
-  bimap (fmap f) (fmap g) (unalign this) = unalign (bimap f g this)
-
+  bimap (fmap f) (fmap g) (unalign this) =
+    unalign (bimap f g this)
 -- unalignWith/align roundtrip with transformation
 -- Combines roundtrip elimination with transformation fusion
 "unalignWith/align" [2] forall f g xs ys.
-  unalignWith f g (align xs ys) = (fmap f xs, fmap g ys)
-
+  unalignWith f g (align xs ys) =
+    (fmap f xs, fmap g ys)
   #-}
 
 -- | Unalign instance for Identity - simply unwrap
@@ -1146,7 +1290,7 @@
           Just (Right gb) -> (as, bs ++ toList gb)
     where
       toList (x :| xs) = x : xs
-  {-# INLINABLE unalign #-}
+  {-# INLINEABLE unalign #-}
 
 -- | Unalign instance for Maybe - reconstruct from pairs or leftovers
 --
@@ -1188,7 +1332,7 @@
       unzipNonEmpty ((x, y) :| rest) =
         let (xs, ys) = List.unzip rest
          in (x :| xs, y :| ys)
-  {-# INLINABLE unalign #-}
+  {-# INLINEABLE unalign #-}
 
 -- | Unalign instance for ZipList - delegates to list unalign
 --
@@ -1237,15 +1381,10 @@
           Just (Right gb) -> (as, bs Vector.++ fromNonEmpty gb)
     where
       fromNonEmpty (x :| xs) = Vector.cons x (Vector.fromList xs)
-  {-# INLINABLE unalign #-}
-
--- Note: Map and IntMap do NOT have Unalign instances because their Semialign
--- instances violate the roundtrip law. When both sides have leftovers, align
--- keeps only left leftovers (left takes precedence), so unalign cannot recover
--- the original right-side keys. We prefer to have a lawful type class rather
--- than instances with caveats.
+  {-# INLINEABLE unalign #-}
 
 -- * Law-checking functions
+
 --
 -- These functions can be used in property-based tests to verify that
 -- instances satisfy the required laws.
@@ -1254,10 +1393,23 @@
 --
 -- Property: @bimap f g (align xs ys) ≡ align (fmap f xs) (fmap g ys)@
 --
+-- This law states that mapping over the aligned result is the same as
+-- mapping over the inputs before alignment. This is a key law for functoriality.
+--
 -- >>> semialignNaturality (*10) (*100) [1,2,3] [4,5] :: Bool
 -- True
 -- >>> semialignNaturality (*10) (*100) [1,2] [3,4,5] :: Bool
 -- True
+-- >>> semialignNaturality (+ 1) (* 2) (Just 5) (Just 10) :: Bool
+-- True
+-- >>> semialignNaturality (+ 1) (* 2) (1 :| [2]) (3 :| [4,5]) :: Bool
+-- True
+--
+-- Hedgehog property test:
+--
+-- >>> check $ withTests 20 $ property $ do xs <- forAll genList; ys <- forAll genList; semialignNaturality (+1) (*2) xs ys === True
+--   ✓ <interactive> passed 20 tests.
+-- True
 semialignNaturality ::
   (Semialign f g, Eq1 f, Eq1 g, Eq c, Eq d) =>
   (a -> c) ->
@@ -1272,12 +1424,23 @@
 --
 -- Property: @align x y ≡ swap (align y x)@
 --
+-- This law ensures that alignment is symmetric - the order of arguments
+-- only affects whether leftovers appear on the left or right side.
+--
 -- >>> semialignSymmetry [1,2,3] [4,5] :: Bool
 -- True
 -- >>> semialignSymmetry [1,2] [3,4,5] :: Bool
 -- True
 -- >>> semialignSymmetry (Just 1) (Just 2) :: Bool
 -- True
+-- >>> semialignSymmetry (1 :| [2,3]) (10 :| [20]) :: Bool
+-- True
+--
+-- Hedgehog property test:
+--
+-- >>> check $ withTests 20 $ property $ do xs <- forAll genList; ys <- forAll genList; semialignSymmetry xs ys === True
+--   ✓ <interactive> passed 20 tests.
+-- True
 semialignSymmetry ::
   (Semialign f g, Eq1 f, Eq1 g, Eq a, Eq b) =>
   f a ->
@@ -1290,10 +1453,15 @@
 --
 -- Property: @align x y ≡ alignWith id id id x y@
 --
+-- This law ensures that align and alignWith are coherent - align is
+-- just alignWith with identity transformations.
+--
 -- >>> semialignCoherence [1,2,3] [4,5] :: Bool
 -- True
 -- >>> semialignCoherence (Just 1) (Just 2) :: Bool
 -- True
+-- >>> semialignCoherence (1 :| [2]) (3 :| [4,5]) :: Bool
+-- True
 semialignCoherence ::
   (Semialign f g, Eq1 f, Eq1 g, Eq a, Eq b) =>
   f a ->
@@ -1306,8 +1474,13 @@
 --
 -- Property: @alignWith f g h x y ≡ let This t r = align x y in This (fmap f t) (fmap (bimap (fmap g) (fmap h)) r)@
 --
+-- This law specifies the correct behavior of alignWith in terms of align
+-- followed by mapping transformations.
+--
 -- >>> semialignWithLaw (\(a,b) -> (a*10, b*100)) (*10) (*100) [1,2,3] [4,5] :: Bool
 -- True
+-- >>> semialignWithLaw (\(a,b) -> (a+1, b*2)) (+1) (*2) (Just 5) (Just 10) :: Bool
+-- True
 semialignWithLaw ::
   (Semialign f g, Eq1 f, Eq1 g, Eq c, Eq d) =>
   ((a, b) -> (c, d)) ->
@@ -1326,6 +1499,9 @@
 --
 -- Property: When aligning with nil on the right, paired part is empty
 --
+-- This law ensures that nil acts as a right identity for alignment,
+-- producing only left leftovers with no matched pairs.
+--
 -- >>> alignRightIdentity [1,2,3] ([] :: [Char])
 -- True
 -- >>> alignRightIdentity (Just 42) (Nothing :: Maybe Char)
@@ -1347,6 +1523,9 @@
 --
 -- Property: When aligning with nil on the left, paired part is empty
 --
+-- This law ensures that nil acts as a left identity for alignment,
+-- producing only right leftovers with no matched pairs.
+--
 -- >>> alignLeftIdentity ([] :: [Char]) [1,2,3]
 -- True
 -- >>> alignLeftIdentity (Nothing :: Maybe Char) (Just 42)
@@ -1382,7 +1561,9 @@
   f a ->
   Bool
 alignEmpty _ _ =
-  liftEq2 (==) (==)
+  liftEq2
+    (==)
+    (==)
     (align (nil :: f a) (nil :: f a))
     (This (nil :: f (a, a)) Nothing)
 
@@ -1390,6 +1571,9 @@
 --
 -- Property: @unalign (align xs ys) ≡ (xs, ys)@
 --
+-- This is the fundamental law of Unalign: unalign is the inverse of align.
+-- It ensures that alignment is completely lossless for Unalign instances.
+--
 -- >>> unalignRoundtrip [1,2,3] [10,20]
 -- True
 -- >>> unalignRoundtrip [1,2] [10,20,30]
@@ -1398,6 +1582,14 @@
 -- True
 -- >>> unalignRoundtrip (Nothing :: Maybe Int) (Just 2)
 -- True
+-- >>> unalignRoundtrip (1 :| [2,3]) (10 :| [20])
+-- True
+--
+-- Hedgehog property test:
+--
+-- >>> check $ withTests 20 $ property $ do xs <- forAll genList; ys <- forAll genList; unalignRoundtrip xs ys === True
+--   ✓ <interactive> passed 20 tests.
+-- True
 unalignRoundtrip ::
   (Unalign f g, Eq1 f, Eq a, Eq b) =>
   f a ->
@@ -1411,9 +1603,15 @@
 --
 -- Property: @bimap (fmap f) (fmap g) (unalign t) ≡ unalign (bimap f g t)@
 --
+-- This law ensures that unalign commutes with mapping transformations,
+-- preserving the functorial structure.
+--
 -- >>> let t = This [(1,2),(3,4)] (Just (Left (5 :| []))) :: This [] NonEmpty Int Int
 -- >>> unalignNaturality (*10) (*100) t
 -- True
+-- >>> let t2 = This [(1,2)] Nothing :: This [] NonEmpty Int Int
+-- >>> unalignNaturality (+1) (*2) t2
+-- True
 unalignNaturality ::
   (Unalign f g, Eq1 f, Eq c, Eq d) =>
   (a -> c) ->
@@ -1486,7 +1684,7 @@
   This
     <$> traverse (\(a, b) -> (,b) <$> h a) t
     <*> traverse (either (fmap Left . traverse h) (pure . Right)) r
-{-# INLINABLE traverseA #-}
+{-# INLINEABLE traverseA #-}
 
 -- | Traversal focusing on all 'b' values in This
 -- Touches 'b' in the tuples (a,b) and in Right (g b)
@@ -1505,7 +1703,7 @@
   This
     <$> traverse (\(a, b) -> (a,) <$> h b) t
     <*> traverse (either (pure . Left) (fmap Right . traverse h)) r
-{-# INLINABLE traverseB #-}
+{-# INLINEABLE traverseB #-}
 
 -- | Traversal1 focusing on all 'a' values in This (at least one)
 -- Uses Apply instead of Applicative
@@ -1524,7 +1722,7 @@
         Nothing -> (`This` Nothing) <$> tResult
         Just (Left ga) -> (\t' ga' -> This t' (Just (Left ga'))) <$> tResult <.> traverse1 h ga
         Just (Right gb) -> (\t' -> This t' (Just (Right gb))) <$> tResult
-{-# INLINABLE traverseA1 #-}
+{-# INLINEABLE traverseA1 #-}
 
 -- | Traversal1 focusing on all 'b' values in This (at least one)
 -- Uses Apply instead of Applicative
@@ -1543,7 +1741,7 @@
         Nothing -> (`This` Nothing) <$> tResult
         Just (Left ga) -> (\t' -> This t' (Just (Left ga))) <$> tResult
         Just (Right gb) -> (\t' gb' -> This t' (Just (Right gb'))) <$> tResult <.> traverse1 h gb
-{-# INLINABLE traverseB1 #-}
+{-# INLINEABLE traverseB1 #-}
 
 -- | Fold optic over all 'a' values in This
 --
@@ -1616,4 +1814,4 @@
   (x :| (y : ys)) -> f x .> traverse1_ f (y :| ys)
   where
     toNonEmpty = foldMap1 (:| [])
-{-# INLINABLE traverse1_ #-}
+{-# INLINEABLE traverse1_ #-}
diff --git a/test/Laws.hs b/test/Laws.hs
new file mode 100644
--- /dev/null
+++ b/test/Laws.hs
@@ -0,0 +1,661 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# OPTIONS_GHC -Wall #-}
+
+module Main (main) where
+
+import Data.Alignment
+import Data.Bifunctor (bimap)
+import Data.Functor.Identity (Identity (..))
+import qualified Data.IntMap as IntMap
+import Data.List.NonEmpty (NonEmpty (..))
+import qualified Data.Map as Map
+import qualified Data.Sequence as Seq
+import qualified Data.Vector as Vector
+import Hedgehog
+import qualified Hedgehog.Gen as Gen
+import qualified Hedgehog.Range as Range
+import System.Exit (exitFailure, exitSuccess)
+import System.IO (hSetEncoding, stderr, stdout, utf8)
+
+-- * Generators
+
+genList :: Gen a -> Gen [a]
+genList = Gen.list (Range.linear 0 20)
+
+genNonEmpty :: Gen a -> Gen (NonEmpty a)
+genNonEmpty g = (:|) <$> g <*> genList g
+
+genMaybe :: Gen a -> Gen (Maybe a)
+genMaybe = Gen.maybe
+
+genVector :: Gen a -> Gen (Vector.Vector a)
+genVector = fmap Vector.fromList . genList
+
+genSeq :: Gen a -> Gen (Seq.Seq a)
+genSeq = fmap Seq.fromList . genList
+
+genMap :: (Ord k) => Gen k -> Gen v -> Gen (Map.Map k v)
+genMap genK genV = Map.fromList <$> genList ((,) <$> genK <*> genV)
+
+genIntMap :: Gen v -> Gen (IntMap.IntMap v)
+genIntMap genV = IntMap.fromList <$> genList ((,) <$> Gen.int (Range.linear 0 100) <*> genV)
+
+genInt :: Gen Int
+genInt = Gen.int (Range.linear (-100) 100)
+
+genChar :: Gen Char
+genChar = Gen.alpha
+
+-- * Test properties
+
+-- ** Functor laws for This
+
+prop_functorIdentity_List :: Property
+prop_functorIdentity_List = property $ do
+  this <- forAll $ genThisListNonEmpty genInt genInt
+  this === this
+
+prop_functorComposition_List :: Property
+prop_functorComposition_List = property $ do
+  this <- forAll $ genThisListNonEmpty genInt genInt
+  let f = (+ 1)
+  let g = (* 2)
+  fmap (f . g) this === fmap f (fmap g this)
+
+-- ** Bifunctor laws for This
+
+prop_bifunctorIdentity_List :: Property
+prop_bifunctorIdentity_List = property $ do
+  this <- forAll $ genThisListNonEmpty genInt genInt
+  this === this
+
+prop_bifunctorComposition_List :: Property
+prop_bifunctorComposition_List = property $ do
+  this <- forAll $ genThisListNonEmpty genInt genInt
+  let f1 = (+ 1)
+  let f2 = (* 2)
+  let g1 = (+ 10)
+  let g2 = (* 20)
+  bimap (f1 . f2) (g1 . g2) this === bimap f1 g1 (bimap f2 g2 this)
+
+-- ** Semialign laws - List
+
+prop_semialignNaturality_List :: Property
+prop_semialignNaturality_List = property $ do
+  xs <- forAll $ genList genInt
+  ys <- forAll $ genList genInt
+  let f = (+ 1)
+  let g = (* 2)
+  semialignNaturality f g xs ys === True
+
+prop_semialignSymmetry_List :: Property
+prop_semialignSymmetry_List = property $ do
+  xs <- forAll $ genList genInt
+  ys <- forAll $ genList genInt
+  semialignSymmetry xs ys === True
+
+prop_semialignCoherence_List :: Property
+prop_semialignCoherence_List = property $ do
+  xs <- forAll $ genList genInt
+  ys <- forAll $ genList genInt
+  semialignCoherence xs ys === True
+
+prop_semialignWithLaw_List :: Property
+prop_semialignWithLaw_List = property $ do
+  xs <- forAll $ genList genInt
+  ys <- forAll $ genList genInt
+  let g = (* 2)
+      h = (* 3)
+      f (a, b) = (g a, h b)
+  semialignWithLaw f g h xs ys === True
+
+-- ** Semialign laws - Maybe
+
+prop_semialignNaturality_Maybe :: Property
+prop_semialignNaturality_Maybe = property $ do
+  xs <- forAll $ genMaybe genInt
+  ys <- forAll $ genMaybe genInt
+  let f = (+ 1)
+  let g = (* 2)
+  semialignNaturality f g xs ys === True
+
+prop_semialignSymmetry_Maybe :: Property
+prop_semialignSymmetry_Maybe = property $ do
+  xs <- forAll $ genMaybe genInt
+  ys <- forAll $ genMaybe genInt
+  semialignSymmetry xs ys === True
+
+prop_semialignCoherence_Maybe :: Property
+prop_semialignCoherence_Maybe = property $ do
+  xs <- forAll $ genMaybe genInt
+  ys <- forAll $ genMaybe genInt
+  semialignCoherence xs ys === True
+
+-- ** Semialign laws - NonEmpty
+
+prop_semialignNaturality_NonEmpty :: Property
+prop_semialignNaturality_NonEmpty = property $ do
+  xs <- forAll $ genNonEmpty genInt
+  ys <- forAll $ genNonEmpty genInt
+  let f = (+ 1)
+  let g = (* 2)
+  semialignNaturality f g xs ys === True
+
+prop_semialignSymmetry_NonEmpty :: Property
+prop_semialignSymmetry_NonEmpty = property $ do
+  xs <- forAll $ genNonEmpty genInt
+  ys <- forAll $ genNonEmpty genInt
+  semialignSymmetry xs ys === True
+
+prop_semialignCoherence_NonEmpty :: Property
+prop_semialignCoherence_NonEmpty = property $ do
+  xs <- forAll $ genNonEmpty genInt
+  ys <- forAll $ genNonEmpty genInt
+  semialignCoherence xs ys === True
+
+-- ** Semialign laws - Vector
+
+prop_semialignNaturality_Vector :: Property
+prop_semialignNaturality_Vector = property $ do
+  xs <- forAll $ genVector genInt
+  ys <- forAll $ genVector genInt
+  let f = (+ 1)
+  let g = (* 2)
+  semialignNaturality f g xs ys === True
+
+prop_semialignSymmetry_Vector :: Property
+prop_semialignSymmetry_Vector = property $ do
+  xs <- forAll $ genVector genInt
+  ys <- forAll $ genVector genInt
+  semialignSymmetry xs ys === True
+
+prop_semialignCoherence_Vector :: Property
+prop_semialignCoherence_Vector = property $ do
+  xs <- forAll $ genVector genInt
+  ys <- forAll $ genVector genInt
+  semialignCoherence xs ys === True
+
+-- ** Semialign laws - Seq
+
+prop_semialignNaturality_Seq :: Property
+prop_semialignNaturality_Seq = property $ do
+  xs <- forAll $ genSeq genInt
+  ys <- forAll $ genSeq genInt
+  let f = (+ 1)
+  let g = (* 2)
+  semialignNaturality f g xs ys === True
+
+prop_semialignSymmetry_Seq :: Property
+prop_semialignSymmetry_Seq = property $ do
+  xs <- forAll $ genSeq genInt
+  ys <- forAll $ genSeq genInt
+  semialignSymmetry xs ys === True
+
+prop_semialignCoherence_Seq :: Property
+prop_semialignCoherence_Seq = property $ do
+  xs <- forAll $ genSeq genInt
+  ys <- forAll $ genSeq genInt
+  semialignCoherence xs ys === True
+
+-- ** Semialign laws - Map
+
+-- Note: Map and IntMap do NOT satisfy the symmetry law when both sides
+-- have disjoint keys (leftovers). When both have leftovers, left takes
+-- precedence. This is a known limitation and why they don't have Unalign
+-- instances. We still test naturality and coherence which do hold.
+
+prop_semialignNaturality_Map :: Property
+prop_semialignNaturality_Map = property $ do
+  xs <- forAll $ genMap genInt genChar
+  ys <- forAll $ genMap genInt genChar
+  let f = toEnum . (+ 1) . fromEnum :: Char -> Char
+  let g = toEnum . (+ 2) . fromEnum :: Char -> Char
+  semialignNaturality f g xs ys === True
+
+-- Skip symmetry test for Map - known to fail when both sides have disjoint keys
+-- prop_semialignSymmetry_Map :: Property
+-- prop_semialignSymmetry_Map = property $ do
+--   xs <- forAll $ genMap genInt genChar
+--   ys <- forAll $ genMap genInt genChar
+--   semialignSymmetry xs ys === True
+
+prop_semialignCoherence_Map :: Property
+prop_semialignCoherence_Map = property $ do
+  xs <- forAll $ genMap genInt genChar
+  ys <- forAll $ genMap genInt genChar
+  semialignCoherence xs ys === True
+
+-- ** Semialign laws - IntMap
+
+-- Note: IntMap, like Map, does NOT satisfy the symmetry law when both sides
+-- have disjoint keys (leftovers). When both have leftovers, left takes
+-- precedence. This is a known limitation and why they don't have Unalign
+-- instances.
+
+prop_semialignNaturality_IntMap :: Property
+prop_semialignNaturality_IntMap = property $ do
+  xs <- forAll $ genIntMap genChar
+  ys <- forAll $ genIntMap genChar
+  let f = toEnum . (+ 1) . fromEnum :: Char -> Char
+  let g = toEnum . (+ 2) . fromEnum :: Char -> Char
+  semialignNaturality f g xs ys === True
+
+-- Skip symmetry test for IntMap - known to fail when both sides have disjoint keys
+-- prop_semialignSymmetry_IntMap :: Property
+-- prop_semialignSymmetry_IntMap = property $ do
+--   xs <- forAll $ genIntMap genChar
+--   ys <- forAll $ genIntMap genChar
+--   semialignSymmetry xs ys === True
+
+prop_semialignCoherence_IntMap :: Property
+prop_semialignCoherence_IntMap = property $ do
+  xs <- forAll $ genIntMap genChar
+  ys <- forAll $ genIntMap genChar
+  semialignCoherence xs ys === True
+
+-- ** Align laws - List
+
+prop_alignRightIdentity_List :: Property
+prop_alignRightIdentity_List = property $ do
+  xs <- forAll $ genList genInt
+  alignRightIdentity xs ([] :: [Char]) === True
+
+prop_alignLeftIdentity_List :: Property
+prop_alignLeftIdentity_List = property $ do
+  ys <- forAll $ genList genInt
+  alignLeftIdentity ([] :: [Char]) ys === True
+
+prop_alignEmpty_List :: Property
+prop_alignEmpty_List = property $ do
+  alignEmpty (undefined :: [Int]) (undefined :: [Int]) === True
+
+-- ** Align laws - Maybe
+
+prop_alignRightIdentity_Maybe :: Property
+prop_alignRightIdentity_Maybe = property $ do
+  xs <- forAll $ genMaybe genInt
+  alignRightIdentity xs (Nothing :: Maybe Char) === True
+
+prop_alignLeftIdentity_Maybe :: Property
+prop_alignLeftIdentity_Maybe = property $ do
+  ys <- forAll $ genMaybe genInt
+  alignLeftIdentity (Nothing :: Maybe Char) ys === True
+
+prop_alignEmpty_Maybe :: Property
+prop_alignEmpty_Maybe = property $ do
+  alignEmpty (undefined :: Maybe Int) (undefined :: Maybe Int) === True
+
+-- ** Align laws - Vector
+
+prop_alignRightIdentity_Vector :: Property
+prop_alignRightIdentity_Vector = property $ do
+  xs <- forAll $ genVector genInt
+  alignRightIdentity xs (Vector.empty :: Vector.Vector Char) === True
+
+prop_alignLeftIdentity_Vector :: Property
+prop_alignLeftIdentity_Vector = property $ do
+  ys <- forAll $ genVector genInt
+  alignLeftIdentity (Vector.empty :: Vector.Vector Char) ys === True
+
+prop_alignEmpty_Vector :: Property
+prop_alignEmpty_Vector = property $ do
+  alignEmpty (undefined :: Vector.Vector Int) (undefined :: Vector.Vector Int) === True
+
+-- ** Align laws - Seq
+
+prop_alignRightIdentity_Seq :: Property
+prop_alignRightIdentity_Seq = property $ do
+  xs <- forAll $ genSeq genInt
+  alignRightIdentity xs (Seq.empty :: Seq.Seq Char) === True
+
+prop_alignLeftIdentity_Seq :: Property
+prop_alignLeftIdentity_Seq = property $ do
+  ys <- forAll $ genSeq genInt
+  alignLeftIdentity (Seq.empty :: Seq.Seq Char) ys === True
+
+prop_alignEmpty_Seq :: Property
+prop_alignEmpty_Seq = property $ do
+  alignEmpty (undefined :: Seq.Seq Int) (undefined :: Seq.Seq Int) === True
+
+-- ** Align laws - Map
+
+prop_alignRightIdentity_Map :: Property
+prop_alignRightIdentity_Map = property $ do
+  xs <- forAll $ genMap genInt genChar
+  alignRightIdentity xs (Map.empty :: Map.Map Int Char) === True
+
+prop_alignLeftIdentity_Map :: Property
+prop_alignLeftIdentity_Map = property $ do
+  ys <- forAll $ genMap genInt genChar
+  alignLeftIdentity (Map.empty :: Map.Map Int Char) ys === True
+
+prop_alignEmpty_Map :: Property
+prop_alignEmpty_Map = property $ do
+  alignEmpty (undefined :: Map.Map Int Char) (undefined :: Map.Map Int Char) === True
+
+-- ** Align laws - IntMap
+
+prop_alignRightIdentity_IntMap :: Property
+prop_alignRightIdentity_IntMap = property $ do
+  xs <- forAll $ genIntMap genChar
+  alignRightIdentity xs (IntMap.empty :: IntMap.IntMap Char) === True
+
+prop_alignLeftIdentity_IntMap :: Property
+prop_alignLeftIdentity_IntMap = property $ do
+  ys <- forAll $ genIntMap genChar
+  alignLeftIdentity (IntMap.empty :: IntMap.IntMap Char) ys === True
+
+prop_alignEmpty_IntMap :: Property
+prop_alignEmpty_IntMap = property $ do
+  alignEmpty (undefined :: IntMap.IntMap Char) (undefined :: IntMap.IntMap Char) === True
+
+-- ** Unalign laws - List
+
+prop_unalignRoundtrip_List :: Property
+prop_unalignRoundtrip_List = property $ do
+  xs <- forAll $ genList genInt
+  ys <- forAll $ genList genInt
+  unalignRoundtrip xs ys === True
+
+prop_unalignNaturality_List :: Property
+prop_unalignNaturality_List = property $ do
+  this <- forAll $ genThisListNonEmpty genInt genInt
+  let f = (+ 1)
+  let g = (* 2)
+  unalignNaturality f g this === True
+
+-- ** Unalign laws - Maybe
+
+prop_unalignRoundtrip_Maybe :: Property
+prop_unalignRoundtrip_Maybe = property $ do
+  xs <- forAll $ genMaybe genInt
+  ys <- forAll $ genMaybe genInt
+  unalignRoundtrip xs ys === True
+
+prop_unalignNaturality_Maybe :: Property
+prop_unalignNaturality_Maybe = property $ do
+  this <- forAll $ genThisMaybeIdentity genInt genInt
+  let f = (+ 1)
+  let g = (* 2)
+  unalignNaturality f g this === True
+
+-- ** Unalign laws - NonEmpty
+
+prop_unalignRoundtrip_NonEmpty :: Property
+prop_unalignRoundtrip_NonEmpty = property $ do
+  xs <- forAll $ genNonEmpty genInt
+  ys <- forAll $ genNonEmpty genInt
+  unalignRoundtrip xs ys === True
+
+prop_unalignNaturality_NonEmpty :: Property
+prop_unalignNaturality_NonEmpty = property $ do
+  this <- forAll $ genThisNonEmptyNonEmpty genInt genInt
+  let f = (+ 1)
+  let g = (* 2)
+  unalignNaturality f g this === True
+
+-- ** Unalign laws - Vector
+
+prop_unalignRoundtrip_Vector :: Property
+prop_unalignRoundtrip_Vector = property $ do
+  xs <- forAll $ genVector genInt
+  ys <- forAll $ genVector genInt
+  unalignRoundtrip xs ys === True
+
+prop_unalignNaturality_Vector :: Property
+prop_unalignNaturality_Vector = property $ do
+  this <- forAll $ genThisVectorNonEmpty genInt genInt
+  let f = (+ 1)
+  let g = (* 2)
+  unalignNaturality f g this === True
+
+-- ** Unalign laws - Seq
+
+prop_unalignRoundtrip_Seq :: Property
+prop_unalignRoundtrip_Seq = property $ do
+  xs <- forAll $ genSeq genInt
+  ys <- forAll $ genSeq genInt
+  unalignRoundtrip xs ys === True
+
+prop_unalignNaturality_Seq :: Property
+prop_unalignNaturality_Seq = property $ do
+  this <- forAll $ genThisSeqNonEmpty genInt genInt
+  let f = (+ 1)
+  let g = (* 2)
+  unalignNaturality f g this === True
+
+-- * Helper generators
+
+genThisListNonEmpty :: Gen a -> Gen b -> Gen (This [] NonEmpty a b)
+genThisListNonEmpty genA genB = Gen.choice [viaAlign, withLeftover, withRightover, justPairs]
+  where
+    viaAlign = do
+      as <- genList genA
+      bs <- genList genB
+      return $ align as bs
+    withLeftover = do
+      pairs <- genList ((,) <$> genA <*> genB)
+      leftover <- genNonEmpty genA
+      return $ This pairs (Just (Left leftover))
+    withRightover = do
+      pairs <- genList ((,) <$> genA <*> genB)
+      rightover <- genNonEmpty genB
+      return $ This pairs (Just (Right rightover))
+    justPairs = do
+      pairs <- genList ((,) <$> genA <*> genB)
+      return $ This pairs Nothing
+
+genThisMaybeIdentity :: Gen a -> Gen b -> Gen (This Maybe Identity a b)
+genThisMaybeIdentity genA genB = Gen.choice [viaAlign, withLeft, withRight, justPairs, empty]
+  where
+    viaAlign = do
+      ma <- genMaybe genA
+      mb <- genMaybe genB
+      return $ align ma mb
+    withLeft = do
+      a <- genA
+      return $ This Nothing (Just (Left (Identity a)))
+    withRight = do
+      b <- genB
+      return $ This Nothing (Just (Right (Identity b)))
+    justPairs = do
+      pair <- (,) <$> genA <*> genB
+      return $ This (Just pair) Nothing
+    empty = return $ This Nothing Nothing
+
+genThisNonEmptyNonEmpty :: Gen a -> Gen b -> Gen (This NonEmpty NonEmpty a b)
+genThisNonEmptyNonEmpty genA genB = Gen.choice [viaAlign, withLeftover, withRightover, justPairs]
+  where
+    viaAlign = do
+      as <- genNonEmpty genA
+      bs <- genNonEmpty genB
+      return $ align as bs
+    withLeftover = do
+      pairs <- genNonEmpty ((,) <$> genA <*> genB)
+      leftover <- genNonEmpty genA
+      return $ This pairs (Just (Left leftover))
+    withRightover = do
+      pairs <- genNonEmpty ((,) <$> genA <*> genB)
+      rightover <- genNonEmpty genB
+      return $ This pairs (Just (Right rightover))
+    justPairs = do
+      pairs <- genNonEmpty ((,) <$> genA <*> genB)
+      return $ This pairs Nothing
+
+genThisVectorNonEmpty :: Gen a -> Gen b -> Gen (This Vector.Vector NonEmpty a b)
+genThisVectorNonEmpty genA genB = Gen.choice [viaAlign, withLeftover, withRightover, justPairs]
+  where
+    viaAlign = do
+      as <- genVector genA
+      bs <- genVector genB
+      return $ align as bs
+    withLeftover = do
+      pairs <- genVector ((,) <$> genA <*> genB)
+      leftover <- genNonEmpty genA
+      return $ This pairs (Just (Left leftover))
+    withRightover = do
+      pairs <- genVector ((,) <$> genA <*> genB)
+      rightover <- genNonEmpty genB
+      return $ This pairs (Just (Right rightover))
+    justPairs = do
+      pairs <- genVector ((,) <$> genA <*> genB)
+      return $ This pairs Nothing
+
+genThisSeqNonEmpty :: Gen a -> Gen b -> Gen (This Seq.Seq NonEmpty a b)
+genThisSeqNonEmpty genA genB = Gen.choice [viaAlign, withLeftover, withRightover, justPairs]
+  where
+    viaAlign = do
+      as <- genSeq genA
+      bs <- genSeq genB
+      return $ align as bs
+    withLeftover = do
+      pairs <- genSeq ((,) <$> genA <*> genB)
+      leftover <- genNonEmpty genA
+      return $ This pairs (Just (Left leftover))
+    withRightover = do
+      pairs <- genSeq ((,) <$> genA <*> genB)
+      rightover <- genNonEmpty genB
+      return $ This pairs (Just (Right rightover))
+    justPairs = do
+      pairs <- genSeq ((,) <$> genA <*> genB)
+      return $ This pairs Nothing
+
+-- * Main test runner
+
+main :: IO ()
+main = do
+  hSetEncoding stdout utf8
+  hSetEncoding stderr utf8
+
+  results <-
+    sequence
+      [ checkGroup
+          "Functor laws - This"
+          [ ("identity (List)", prop_functorIdentity_List),
+            ("composition (List)", prop_functorComposition_List)
+          ],
+        checkGroup
+          "Bifunctor laws - This"
+          [ ("identity (List)", prop_bifunctorIdentity_List),
+            ("composition (List)", prop_bifunctorComposition_List)
+          ],
+        checkGroup
+          "Semialign laws - List"
+          [ ("naturality", prop_semialignNaturality_List),
+            ("symmetry", prop_semialignSymmetry_List),
+            ("coherence", prop_semialignCoherence_List),
+            ("alignWith", prop_semialignWithLaw_List)
+          ],
+        checkGroup
+          "Semialign laws - Maybe"
+          [ ("naturality", prop_semialignNaturality_Maybe),
+            ("symmetry", prop_semialignSymmetry_Maybe),
+            ("coherence", prop_semialignCoherence_Maybe)
+          ],
+        checkGroup
+          "Semialign laws - NonEmpty"
+          [ ("naturality", prop_semialignNaturality_NonEmpty),
+            ("symmetry", prop_semialignSymmetry_NonEmpty),
+            ("coherence", prop_semialignCoherence_NonEmpty)
+          ],
+        checkGroup
+          "Semialign laws - Vector"
+          [ ("naturality", prop_semialignNaturality_Vector),
+            ("symmetry", prop_semialignSymmetry_Vector),
+            ("coherence", prop_semialignCoherence_Vector)
+          ],
+        checkGroup
+          "Semialign laws - Seq"
+          [ ("naturality", prop_semialignNaturality_Seq),
+            ("symmetry", prop_semialignSymmetry_Seq),
+            ("coherence", prop_semialignCoherence_Seq)
+          ],
+        checkGroup
+          "Semialign laws - Map"
+          [ ("naturality", prop_semialignNaturality_Map),
+            -- symmetry skipped - known to fail for Map with disjoint keys
+            ("coherence", prop_semialignCoherence_Map)
+          ],
+        checkGroup
+          "Semialign laws - IntMap"
+          [ ("naturality", prop_semialignNaturality_IntMap),
+            -- symmetry skipped - known to fail for IntMap with disjoint keys
+            ("coherence", prop_semialignCoherence_IntMap)
+          ],
+        checkGroup
+          "Align laws - List"
+          [ ("right identity", prop_alignRightIdentity_List),
+            ("left identity", prop_alignLeftIdentity_List),
+            ("empty", prop_alignEmpty_List)
+          ],
+        checkGroup
+          "Align laws - Maybe"
+          [ ("right identity", prop_alignRightIdentity_Maybe),
+            ("left identity", prop_alignLeftIdentity_Maybe),
+            ("empty", prop_alignEmpty_Maybe)
+          ],
+        checkGroup
+          "Align laws - Vector"
+          [ ("right identity", prop_alignRightIdentity_Vector),
+            ("left identity", prop_alignLeftIdentity_Vector),
+            ("empty", prop_alignEmpty_Vector)
+          ],
+        checkGroup
+          "Align laws - Seq"
+          [ ("right identity", prop_alignRightIdentity_Seq),
+            ("left identity", prop_alignLeftIdentity_Seq),
+            ("empty", prop_alignEmpty_Seq)
+          ],
+        checkGroup
+          "Align laws - Map"
+          [ ("right identity", prop_alignRightIdentity_Map),
+            ("left identity", prop_alignLeftIdentity_Map),
+            ("empty", prop_alignEmpty_Map)
+          ],
+        checkGroup
+          "Align laws - IntMap"
+          [ ("right identity", prop_alignRightIdentity_IntMap),
+            ("left identity", prop_alignLeftIdentity_IntMap),
+            ("empty", prop_alignEmpty_IntMap)
+          ],
+        checkGroup
+          "Unalign laws - List"
+          [ ("roundtrip", prop_unalignRoundtrip_List),
+            ("naturality", prop_unalignNaturality_List)
+          ],
+        checkGroup
+          "Unalign laws - Maybe"
+          [ ("roundtrip", prop_unalignRoundtrip_Maybe),
+            ("naturality", prop_unalignNaturality_Maybe)
+          ],
+        checkGroup
+          "Unalign laws - NonEmpty"
+          [ ("roundtrip", prop_unalignRoundtrip_NonEmpty),
+            ("naturality", prop_unalignNaturality_NonEmpty)
+          ],
+        checkGroup
+          "Unalign laws - Vector"
+          [ ("roundtrip", prop_unalignRoundtrip_Vector),
+            ("naturality", prop_unalignNaturality_Vector)
+          ],
+        checkGroup
+          "Unalign laws - Seq"
+          [ ("roundtrip", prop_unalignRoundtrip_Seq),
+            ("naturality", prop_unalignNaturality_Seq)
+          ]
+      ]
+
+  if and results
+    then exitSuccess
+    else exitFailure
+
+checkGroup :: String -> [(String, Property)] -> IO Bool
+checkGroup grpName props = do
+  putStrLn $ "\n━━━ " ++ grpName ++ " ━━━"
+  results <- mapM checkProp props
+  return $ and results
+
+checkProp :: (String, Property) -> IO Bool
+checkProp (name, prop) = do
+  putStrLn $ "  • " ++ name
+  check prop