diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2,6 +2,83 @@
 
 ## Upcoming
 
+## 0.2.0.0 -- 2026-07-26
+* Expand GHC support through 9.12. Bump nixpkgs, Cabal, and CI tooling.
+* Replace the `Makefile` with a `justfile`, including release commands.
+* Add a public `kindly-functors:laws` sublibrary of `hedgehog-classes` `Laws`
+  for the functor classes: identity and composition for `map1`/`map2`, one
+  bundle per variance, plus `Kindly.Rank2.Laws` for the rank-2 `bmap`/`bmap2`
+  functors. The test suite law-checks them across the structural and
+  generic-representation instances.
+* Replace the ~60 empty per-type `MapArg1`/`MapArg2`/`MapArg3` instances with
+  three blanket instances in `Kindly.Class`, keyed on the functor's domain
+  category. A `CategoricalFunctor` instance no longer needs a paired `MapArgN`
+  instance. No public API change.
+* Fill out the `Type -> Type` instance coverage in `Kindly.Functor`: the
+  `transformers` stack (`ReaderT`, `StateT`, `WriterT` (Lazy/Strict/CPS),
+  `ExceptT`, `MaybeT`, `IdentityT`, `ContT`, `RWST` (Lazy/Strict/CPS),
+  `AccumT`, `SelectT`, `Backwards`, `Reverse`, `Constant`, `Lift`),
+  partially-applied profunctors (`Star`, `Costar`, `Forget`), `semigroupoids`
+  (`WrappedApplicative`, `MaybeApply`, `Static`), `These1`, `Generically1`
+  (base >= 4.17), and the remaining non-phantom `Contravariant` types from
+  base (`Comparison`, `Equivalence`, `Op`). Adds a direct `transformers`
+  dependency.
+* Add instances for the `bifunctors` package (new dependency): `Flip`, `Clown`,
+  `Joker`, `Product`, `Sum`, `Tannen`, `Biff`, and `WrappedBifunctor`, each
+  with its partial application in `Kindly.Functor`.
+* Add profunctor (`Dom = Op`) instances for `Star`, `Costar`, `Forget`,
+  `Kleisli`, and `WrappedArrow`, and a `profunctorLaws` bundle to the laws
+  sublibrary. `Kleisli`, `Star`, and `Forget` need no `Monad`/`Functor`
+  constraint for `map2`, unlike their Hask `Profunctor` instances.
+* Add profunctor instances for `Procompose`, `Rift`, `Yoneda`, `Coyoneda`,
+  and `Cayley`, with their partial applications in `Kindly.Functor`.
+* Add profunctor instances for the `Tambara`/`Pastro` families (plain and
+  `Sum`), `Closure`, `Environment`, `FreeTraversing`, `CofreeTraversing`,
+  `FreeMapping`, and `CofreeMapping`, with their partial applications in
+  `Kindly.Functor`. This completes coverage of the `profunctors` package.
+* Add instances for `Tagged` (new `tagged` dependency): covariant in its last
+  argument, profunctorial (phantom) in its first.
+* Add a bifunctor instance for `Op`: covariant in its first argument with
+  contravariant partial applications, i.e. `Bifunctor (->) Op Op`. Hask's
+  `Bifunctor` and `Profunctor` cannot express this. Add
+  `observedBifunctorLaws` for law-testing such instances.
+* Add instances for `Fix` (bifunctors), `Constant` at two arguments, and
+  `Dual` (semigroupoids). Add trifunctor instances for `Forget` and `K1`,
+  and an `observedTrifunctorLaws` bundle for `map3`.
+* Add instances for `containers` (new dependency): `Map k`, `IntMap`, `Seq`,
+  `ViewL`, `ViewR`, `Tree`, and `SCC`.
+* Generalize `invmap` to functors of any variance and add `mapIso`, both backed
+  by a new `LiftIso` class in `Kindly.Class` that reflects a `(->)` isomorphism
+  into an arbitrary category. `invmap` and `mapIso` now resolve for covariant
+  and contravariant functors, not just invariant ones, dropping the leg the
+  functor cannot use. The domain category is fixed by the functor argument, so
+  existing invariant call sites are unchanged. Add `liftIsoLaws` and
+  `mapIsoLaws` bundles to the laws sublibrary. `LiftIso` instances cover `(->)`,
+  `Op`, `Iso (->)`, and the Kleisli categories `Star f` and `Kleisli f` (for
+  `Monad f`). `Star Maybe` is the domain of a `Filterable` functor.
+* Add `bimapIso` and `trimapIso`, the bifunctor and trifunctor analogs of
+  `mapIso`. Each maps a `(->)` isomorphism through every position of a
+  bifunctor/trifunctor regardless of that position's variance, taking one `Iso`
+  per position and reflecting it into that position's category with `liftIso`.
+  Add `bimapIsoLaws` and `trimapIsoLaws` bundles to the laws sublibrary.
+  Re-export `Iso` from `Kindly.Functor`, `Kindly.Bifunctor`, `Kindly.Trifunctor`,
+  and `Kindly` so callers of `mapIso`/`bimapIso`/`trimapIso` can build
+  isomorphisms without importing `Data.Isomorphism` directly.
+* Give `CategoricalFunctor`'s `map` a generic default backed by `kind-generics`,
+  so a datatype with a `GenericK` instance (from `deriveGenericK`) gets a
+  `CategoricalFunctor` instance from an empty body carrying only its `Dom` and
+  `Cod`. The default reads variance off the field structure and dispatches on the
+  instance's categories: covariant (`Dom = (->)`), contravariant (`Op`), and
+  invariant (`Iso (->)`) single-parameter functors, and two- and three-parameter
+  functors (bifunctors, profunctors, trifunctors) in any per-argument combination
+  of those variances. A covariant or contravariant instance of the wrong sign is
+  a compile error rather than a wrong answer. Adds a `kind-generics` dependency.
+* Export the `deriving via` adapters `FromFunctor` and `FromContra` from
+  `Kindly.Functor`, and `FromBifunctor` and `FromProfunctor` from
+  `Kindly.Bifunctor`. A type with an existing base
+  `Functor`/`Contravariant`/`Bifunctor`/`Profunctor` instance can derive its
+  `CategoricalFunctor` instance through the matching adapter.
+
 ## 0.1.0.1 -- 2024-02-04
 
 * Initial Release.
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,25 +1,15 @@
 Kindly Functors
 ===============
 
-🚨 **WORK IN PROGRESS** 🚨
-
-[![kindly-functors::CI](https://github.com/solomon-b/kindly-functors/actions/workflows/nix.yml/badge.svg)](https://github.com/solomon-b/kindly-functors/actions/workflows/nix.yml)
-[![kindly-functors::CI](https://github.com/solomon-b/kindly-functors/actions/workflows/cabal.yml/badge.svg)](https://github.com/solomon-b/kindly-functors/actions/workflows/cabal.yml)
+[![nix:build](https://github.com/solomon-b/kindly-functors/actions/workflows/nix.yml/badge.svg?branch=main)](https://github.com/solomon-b/kindly-functors/actions/workflows/nix.yml)
+[![cabal:build](https://github.com/solomon-b/kindly-functors/actions/workflows/cabal.yml/badge.svg?branch=main)](https://github.com/solomon-b/kindly-functors/actions/workflows/cabal.yml)
 
 
 A category polymorphic `Functor` typeclass based on the work of [IcelandJack](https://www.reddit.com/r/haskell/comments/eoo16m/base_category_polymorphic_functor_and_functorof/?utm_source=reddit&utm_medium=usertext&utm_name=haskell&utm_content=t1_khkwtph) and [Ed Kmett](https://gist.github.com/ekmett/b26363fc0f38777a637d) allowing you to pick out arbitrary kinds and variances for your functors.
 
 This library offers direct access to the `FunctorOf` and `Functor` classes defined in the above work but also a slightly more familiar API for one, two, and three parameter functors.
-```haskell
-type Functor f = FunctorOf (->) (->)
-type Contravariant f = FunctorOf Op (->)
-type Invariant f = FunctorOf (<->) (->)
-type Filterable f = FunctorOf (Star Maybe) (->)
-type Bifunctor p = FunctorOf (->) (Nat (->) (->))
-type Profunctor p = FunctorOf Op (Nat (->) (->))
-type Trifunctor p = FunctorOf cat1 (Nat cat2 (Nat cat3 cat4))
-```
 
+# High Level Interface
 `fmap`, `bimap`, `lmap`, and `rmap` have been made polymorphic over variances:
 ```
 > fmap show (Identity True)
@@ -50,10 +40,134 @@
 ("True","False","()")
 ```
 
-# How does this work?
+# Deriving your own instances
 
-The above functions are all just instantions of `map1`, `map2`, and `map3`:
+`map` has a generic default backed by [`kind-generics`](https://hackage.haskell.org/package/kind-generics). Give your type a `GenericK` instance with `deriveGenericK`, then write a `CategoricalFunctor` instance with an empty body that supplies only `Dom` and `Cod`:
+
+```haskell
+{-# LANGUAGE TemplateHaskell #-}
+
+import Kindly
+
+data Pair a = Pair a a deriving Show
+$(deriveGenericK ''Pair)
+
+instance CategoricalFunctor Pair where
+  type Dom Pair = (->)
+  type Cod Pair = (->)
 ```
+```
+> fmap (+1) (Pair 1 2)
+Pair 2 3
+```
+
+The default reads each argument's variance off the field structure, so a contravariant type only differs in its `Dom`:
+
+```haskell
+newtype Pred a = Pred { runPred :: a -> Bool }
+$(deriveGenericK ''Pred)
+
+instance CategoricalFunctor Pred where
+  type Dom Pred = Op
+  type Cod Pred = (->)
+```
+```
+> runPred (contramap length (Pred even)) [1,2,3]
+False
+```
+
+The declared variance is checked against the fields. Writing `Dom Pred = (->)` here is a compile error rather than a wrong answer, because `a` occurs in a negative position. This covers covariant (`(->)`), contravariant (`Op`), and invariant (`Iso (->)`) single-parameter functors, and two- and three-parameter functors in any per-argument mix of those variances. It does not cover non-`(->)` domains (e.g. `Star Maybe`), rank-2 functors, constructors carrying constraints or existentials, or a recursive field whose head has no base `Functor`.
+
+If your type already has a `base` `Functor`, `Contravariant`, `Bifunctor`, or `Profunctor` instance, skip the generics and derive the matching `CategoricalFunctor` through one of the `From*` adapters with `DerivingVia`. Import `Kindly` qualified here so its own `Functor` does not clash with the one you are deriving:
+
+```haskell
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE DerivingVia #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+import Kindly qualified as K
+
+data Tree a = Leaf a | Node (Tree a) (Tree a)
+  deriving (Show, Functor)
+
+deriving via (K.FromFunctor Tree) instance K.CategoricalFunctor Tree
+```
+```
+> K.fmap (+1) (Node (Leaf 1) (Leaf 2))
+Node (Leaf 2) (Leaf 3)
+```
+
+`FromContra`, `FromBifunctor`, and `FromProfunctor` (the last two in `Kindly.Bifunctor`) do the same for `Contravariant`, `Bifunctor`, and `Profunctor` instances.
+
+# Isomorphism mapping
+
+`invmap` threads a type isomorphism through a functor of any variance, keeping whichever leg that variance can use:
+
+```haskell
+invmap :: (Functor cat f, LiftIso cat) => (a -> b) -> (b -> a) -> f a -> f b
+```
+```
+> runIdentity (invmap show (read @Int) (Identity 5))
+"5"
+
+> getPredicate (invmap show (read @Int) (Predicate even)) "4"
+True
+```
+
+The covariant call keeps the forward function. The contravariant call keeps the backward one. So `invmap` resolves for covariant and contravariant functors, not only invariant ones. `mapIso` is the same operation taking a packaged `Iso (->)`, and `bimapIso` / `trimapIso` map one `Iso` through each position of a bifunctor / trifunctor regardless of that position's variance.
+
+# Rank-2 functors
+
+`Kindly.Rank2` covers types whose parameters are themselves functors (higher-kinded data). `bmap1`, `bmap2`, and `bmap3` pick which functor parameter to map, counting from the right to match `map1` / `map2` / `map3`:
+
+```haskell
+import Kindly
+
+data Schema f = Schema (f Int) (f Bool)
+
+instance CategoricalFunctor Schema where
+  type Dom Schema = (->) ~> (->)
+  type Cod Schema = (->)
+  map (Nat nat) (Schema a b) = Schema (nat a) (nat b)
+```
+```
+> bmap1 maybeToList (Schema (Just 1) Nothing)
+Schema [1] []
+```
+
+`bcontramap1` / `binvmap1` (and their `2` / `3` variants) do the same for a parameter the type is contravariant or invariant in.
+
+# Lower Level Interface
+
+The above functions are all just aliases for the `MapArg1`, `MapArg2`, and `MapArg3` interfaces:
+```haskell
+-- NOTE: These these classes are labeled from right to left:
+
+class (FunctorOf cat1 (->) p) => MapArg1 cat1 p | p -> cat1 where
+  map1 :: (a `cat1` b) -> p a -> p b
+  map1 = map
+
+class (FunctorOf cat1 (cat2 ~> (->)) p, forall x. MapArg1 cat2 (p x)) => MapArg2 cat1 cat2 p | p -> cat2 cat2 where
+  map2 :: (a `cat1` b) -> forall x. p a x -> p b x
+  map2 = runNat . map
+
+class (FunctorOf cat1 (cat2 ~> cat3 ~> (->)) p, forall x. MapArg2 cat2 cat3 (p x)) => MapArg3 cat1 cat2 cat3 p | p -> cat1 cat2 cat3 where
+  map3 :: (a `cat1` b) -> forall x y. p a x y -> p b x y
+  map3 f = runNat (runNat (map f))
+
+type Functor :: (Type -> Type -> Type) -> (Type -> Type) -> Constraint
+type Functor cat p = (MapArg1 cat p)
+
+type Bifunctor :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> (Type -> Type -> Type) -> Constraint
+type Bifunctor cat1 cat2 p = (MapArg2 cat1 cat2 p, forall x. MapArg1 cat2 (p x))
+
+type Trifunctor :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> (Type -> Type -> Type) -> (Type -> Type -> Type -> Type) -> Constraint
+type Trifunctor cat1 cat2 cat3 p = (MapArg3 cat3 cat2 cat1 p, forall x. MapArg2 cat2 cat1 (p x), forall x y. MapArg1 cat1 (p x y))
+```
+
+`map1`, `map2`, and `map3` can be used directly:
+```
 > map1 show (True, False, ())
 (True,False,"()")
 
@@ -67,33 +181,88 @@
 ("True",False,())
 ```
 
-Becareful when using these directly as GHC might pick out a surprising instance:
+But be careful when using these directly as GHC might pick out a surprising instance:
 ```
 > map2 show (Left True)
 Left "True"
 ```
 
-These functions themselves are a frontend for `map` from the (kindly) `Functor` class:
+# How does this actually work?
 
+`MapArg1`, `MapArg2`, and `MapArg3` are in fact just a frontend for yet another class called `CategoricalFunctor`:
 ```haskell
-type Functor :: (from -> to) -> Constraint
-class (Category (Dom f), Category (Cod f)) => Functor (f :: from -> to) where
+type CategoricalFunctor :: (from -> to) -> Constraint
+class (Category (Dom f), Category (Cod f)) => CategoricalFunctor (f :: from -> to) where
   type Dom f :: from -> from -> Type
   type Cod f :: to -> to -> Type
 
   map :: Dom f a b -> Cod f (f a) (f b)
+```
 
--- NOTE: These these classes are labeled from right to left:
-k
-class (FunctorOf cat (->) p) => MapArg1 cat p | p -> cat where
-  map1 :: (a `cat` b) -> p a -> p b
-  map1 = map
+This class describes a `Functor` just like the ordinary `base`
+`Functor` class but with the key difference that it is polymorphic
+over the source and target categories of the functor.
 
-class (FunctorOf cat1 (cat2 ~> (->)) p) => MapArg2 cat1 cat2 p | p -> cat2 cat2 where
-  map2 :: (a `cat1` b) -> forall x. p a x -> p b x
-  map2 = runNat . map
+`Dom f` (domain) is the source category and `Cod f` (co-domain) is the
+target category.
 
-class (FunctorOf cat1 (cat2 ~> cat3 ~> (->)) p) => MapArg3 cat1 cat2 cat3 p | p -> cat1 cat2 cat3 where
-  map3 :: (a `cat1` b) -> forall x y. p a x y -> p b x y
-  map3 f = runNat (runNat (map f))
+This means that you can instantiate `CategoricalFunctor` with
+Covariant (`->`), Contravariant (`Op`), Invariant (via `Iso`),
+`Kleisli`, or any product of the above by using a functor category
+(via `~>`).
+
+A helpful tool for working with `CategoricalFunctor` is the `FunctorOf` class:
+
+```haskell
+type FunctorOf :: Cat from -> Cat to -> (from -> to) -> Constraint
+class (CategoricalFunctor f, dom ~ Dom f, cod ~ Cod f) => FunctorOf dom cod f
+
+instance (CategoricalFunctor f, dom ~ Dom f, cod ~ Cod f) => FunctorOf dom cod f
 ```
+
+`FunctorOf` gives an easy way of aliasing `CategoricalFunctor`
+instances which target specific categories and parameters. We use
+`FunctorOf` to implement the outer `MapArg*` interface.
+
+```haskell
+type Functor f = FunctorOf (->) (->)
+type Contravariant f = FunctorOf Op (->)
+type Invariant f = FunctorOf (<->) (->)
+type Filterable f = FunctorOf (Star Maybe) (->)
+type Bifunctor p = FunctorOf (->) (Nat (->) (->))
+type Profunctor p = FunctorOf Op (Nat (->) (->))
+type Trifunctor p = FunctorOf cat1 (Nat cat2 (Nat cat3 cat4))
+```
+
+In the case of Functors kinds greater then `Type -> Type` the above
+aliases are a little deceptive.
+
+For example, to replace the typeclass we all know as `Bifunctor` one
+would need both the `Functor f` and `Bifunctor f` aliases from the
+above list. This is because each of these aliases picks out a specific
+single parameter and sets its variance.
+
+The `MapArg*` classes and higher level interface was built to smooth
+over this issue at the cost of less granular control.
+
+# Included instances
+
+The library comes with instances for a lot of standard types: the `transformers` monad-transformer stack, the `profunctors` hierarchy (`Star`, `Costar`, `Forget`, the `Tambara` / `Pastro` families, and more), the `bifunctors` wrappers (`Flip`, `Clown`, `Joker`, `Product`, `Sum`, `Tannen`, `Biff`), several `containers` types (`Map`, `IntMap`, `Seq`, `Tree`, `SCC`), and the contravariant types from `base`. See `CHANGELOG.md` for the full list.
+
+# Testing with the laws sublibrary
+
+`kindly-functors:laws` is a public sublibrary of [`hedgehog-classes`](https://hackage.haskell.org/package/hedgehog-classes) `Laws`, so you can law-test your own instances the way you would test `Functor` or `Monoid`. Depend on it:
+
+```
+build-depends: kindly-functors:laws
+```
+
+```haskell
+import Kindly.Functor.Laws (functorLaws)
+import Hedgehog.Classes (lawsCheck)
+
+main :: IO Bool
+main = lawsCheck (functorLaws genMyFunctor)
+```
+
+Each bundle states identity and composition for one variance: `functorLaws` at `(->)`, `contravariantFunctorLaws` at `Op`, `invariantFunctorLaws` at `Iso (->)`, with `bifunctorLaws` and `profunctorLaws` also covering `map2`. `mapIsoLaws`, `bimapIsoLaws`, and `trimapIsoLaws` check the isomorphism-mapping functions, and `Kindly.Rank2.Laws` supplies the rank-2 bundles. Covariant functors are compared with `Eq`. Contravariant and invariant functors are observed through a caller-supplied function, since they usually have no `Eq` or `Show`.
diff --git a/kindly-functors.cabal b/kindly-functors.cabal
--- a/kindly-functors.cabal
+++ b/kindly-functors.cabal
@@ -1,7 +1,7 @@
 cabal-version:   3.4
 name:            kindly-functors
 category:        Control, Categories
-version:         0.1.0.1
+version:         0.2.0.0
 synopsis:        A category polymorphic `Functor` typeclass
 description:     A category polymorphic `Functor` typeclass.
 homepage:        https://www.github.com/solomon-b/kindly-functors
@@ -17,8 +17,15 @@
 tested-with:     GHC == 9.0.2,
                  GHC == 9.2.8,
                  GHC == 9.4.8,
-                 GHC == 9.6.3,
+                 GHC == 9.6.7,
+                 GHC == 9.8.4,
+                 GHC == 9.10.3,
+                 GHC == 9.12.4,
 
+source-repository head
+    type:     git
+    location: https://github.com/solomon-b/kindly-functors.git
+
 --------------------------------------------------------------------------------
 
 common warnings
@@ -38,6 +45,7 @@
     GeneralizedNewtypeDeriving
     ImportQualifiedPost
     InstanceSigs
+    LambdaCase
     MultiParamTypeClasses
     NoImplicitPrelude
     PolyKinds
@@ -61,30 +69,65 @@
       Kindly.Class
       Kindly.Bifunctor
       Kindly.Functor
-      Kindly.Iso
       Kindly.Rank2
       Kindly.Trifunctor
     build-depends:
-      base > 4 && < 5,
+      base >= 4 && < 5,
+      bifunctors                    >= 5.6 && < 5.7,
+      containers                    >= 0.6 && < 0.9,
+      kind-generics                 >= 0.5 && < 0.6,
+      kind-generics-th              >= 0.2.3 && < 0.3,
       mtl                           >= 2.2.2 && < 2.4,
       profunctors                   >= 5.6.2 && < 5.7,
       semigroupoids                 >= 6.0.0 && < 6.1,
+      tagged                        >= 0.8 && < 0.9,
       these                         >= 1.2 && < 1.3,
-      witherable                    >= 0.4.2 && < 0.5,
+      transformers                  >= 0.5.6 && < 0.7,
+      witherable                    >= 0.4.2 && < 0.6,
     hs-source-dirs:   src
     default-language: Haskell2010
 
 --------------------------------------------------------------------------------
 
+library laws
+    import:           common-extensions, warnings
+    visibility:       public
+    hs-source-dirs:   laws
+    exposed-modules:
+      Kindly.Functor.Laws
+      Kindly.Rank2.Laws
+    build-depends:
+      base >= 4 && < 5,
+      kindly-functors,
+      semigroupoids                 >= 6.0.0 && < 6.1,
+      hedgehog                      >= 1.4 && < 1.6,
+      hedgehog-classes              >= 0.2 && < 0.3,
+    default-language: Haskell2010
+
+--------------------------------------------------------------------------------
+
 test-suite kindly-functors-test
     import:           warnings
     default-language: Haskell2010
-    -- other-modules:
-    -- other-extensions:
+    other-modules:    GenericSpec
+                      LawsSpec
+                      Rank2LawsSpec
     type:             exitcode-stdio-1.0
     hs-source-dirs:   test
     main-is:          Main.hs
     build-depends:
-        base > 4 && < 5,
+        base >= 4 && < 5,
+        bifunctors                    >= 5.6 && < 5.7,
+        containers                    >= 0.6 && < 0.9,
         hspec,
-        kindly-functors
+        hedgehog                      >= 1.4 && < 1.6,
+        hedgehog-classes              >= 0.2 && < 0.3,
+        kind-generics                 >= 0.5 && < 0.6,
+        kind-generics-th              >= 0.2.3 && < 0.3,
+        kindly-functors,
+        kindly-functors:laws,
+        profunctors                   >= 5.6.2 && < 5.7,
+        semigroupoids                 >= 6.0.0 && < 6.1,
+        tagged                        >= 0.8 && < 0.9,
+        these                         >= 1.2 && < 1.3,
+        transformers                  >= 0.5.6 && < 0.7
diff --git a/laws/Kindly/Functor/Laws.hs b/laws/Kindly/Functor/Laws.hs
new file mode 100644
--- /dev/null
+++ b/laws/Kindly/Functor/Laws.hs
@@ -0,0 +1,573 @@
+{-# LANGUAGE ImpredicativeTypes #-}
+
+-- | @hedgehog-classes@ 'Laws' for this library's category-polymorphic functor
+-- classes. A consumer can law-test their own 'CategoricalFunctor', 'MapArg1',
+-- and 'MapArg2' instances the way they test 'Functor' or 'Monoid'.
+--
+-- > import Kindly.Functor.Laws (functorLaws)
+-- > import Hedgehog.Classes (lawsCheck)
+-- >
+-- > main :: IO Bool
+-- > main = lawsCheck (functorLaws genMyFunctor)
+--
+-- One bundle per variance, each stating the same two laws. Identity
+-- (@'map1' 'id' = 'id'@) and composition
+-- (@'map1' (f '.' g) = 'map1' f '.' 'map1' g@), with @'id'@ and @('.')@ in the
+-- functor's /domain/ 'Category'. 'functorLaws' works at @('->')@ (covariant),
+-- 'contravariantFunctorLaws' at @'Op'@, 'invariantFunctorLaws' at
+-- @'Iso' ('->')@. 'bifunctorLaws' and 'profunctorLaws' also cover @'map2'@,
+-- at the @('->')@ and 'Op' domains respectively. 'mapIsoLaws' checks
+-- @'Kindly.Functor.mapIso'@, which maps an isomorphism through a functor of any
+-- variance, so one bundle serves all three domains. 'bimapIsoLaws' and
+-- 'trimapIsoLaws' do the same for @'Kindly.Bifunctor.bimapIso'@ and
+-- @'Kindly.Trifunctor.trimapIso'@, checking functoriality in every 'Iso'
+-- position. 'liftIsoLaws' checks 'liftIso' itself at any target category,
+-- covering the 'LiftIso' instances no exported functor witnesses (e.g.
+-- @Star f@ and @Kleisli m@).
+--
+-- The bundles are separate functions because the comparison differs. Covariant
+-- functors compare directly with 'Eq'. Contravariant and invariant functors
+-- usually have no 'Eq' or 'Show', so they are checked extensionally through a
+-- caller-supplied @obs :: f 'Int' -> 'Int' -> r@ that observes both sides at the
+-- 'Int' witness.
+--
+-- The rank-2 generator @forall x. 'Gen' x -> 'Gen' (f x)@ lets a covariant law
+-- instantiate @f@ at whichever element type it needs.
+module Kindly.Functor.Laws
+  ( -- * Covariant functors
+    functorLaws,
+
+    -- * Contravariant functors
+    contravariantFunctorLaws,
+
+    -- * Invariant functors
+    invariantFunctorLaws,
+
+    -- * Isomorphism mapping (any variance)
+    liftIsoLaws,
+    mapIsoLaws,
+
+    -- * Covariant bifunctors
+    bifunctorLaws,
+    observedBifunctorLaws,
+    bimapIsoLaws,
+
+    -- * Profunctors
+    profunctorLaws,
+
+    -- * Trifunctors
+    observedTrifunctorLaws,
+    trimapIsoLaws,
+  )
+where
+
+--------------------------------------------------------------------------------
+
+import Control.Category (Category (id, (.)))
+import Data.Functor.Contravariant (Op (..))
+import Data.Isomorphism (Iso (..))
+import Hedgehog (Gen, Property, forAll, forAllWith, property, (===))
+import Hedgehog.Classes (Laws (..))
+import Hedgehog.Gen qualified as Gen
+import Hedgehog.Range qualified as Range
+import Kindly.Bifunctor (Bifunctor, bimapIso)
+import Kindly.Class (LiftIso, MapArg1, MapArg2, MapArg3, liftIso, map1, map2, map3)
+import Kindly.Functor (mapIso)
+import Kindly.Trifunctor (Trifunctor, trimapIso)
+import Prelude hiding (id, (.))
+
+--------------------------------------------------------------------------------
+
+-- | The element type the laws are witnessed at.
+genInt :: Gen Int
+genInt = Gen.int (Range.linear (-100) 100)
+
+--------------------------------------------------------------------------------
+-- Covariant
+
+-- | The functor laws for a /covariant/ functor's @'map1'@ (domain @('->')@),
+-- compared with 'Eq'.
+functorLaws ::
+  forall f.
+  ( MapArg1 (->) f,
+    forall x. (Eq x) => Eq (f x),
+    forall x. (Show x) => Show (f x)
+  ) =>
+  (forall x. Gen x -> Gen (f x)) ->
+  Laws
+functorLaws genF =
+  Laws
+    "Functor"
+    [ ("Identity", covariantIdentity genF),
+      ("Composition", covariantComposition genF)
+    ]
+
+covariantIdentity ::
+  forall f.
+  ( MapArg1 (->) f,
+    forall x. (Eq x) => Eq (f x),
+    forall x. (Show x) => Show (f x)
+  ) =>
+  (forall x. Gen x -> Gen (f x)) ->
+  Property
+covariantIdentity genF = property $ do
+  fa <- forAll (genF genInt)
+  map1 (id :: Int -> Int) fa === fa
+
+covariantComposition ::
+  forall f.
+  ( MapArg1 (->) f,
+    forall x. (Eq x) => Eq (f x),
+    forall x. (Show x) => Show (f x)
+  ) =>
+  (forall x. Gen x -> Gen (f x)) ->
+  Property
+covariantComposition genF = property $ do
+  fa <- forAll (genF genInt)
+  let g = (+ 1) :: Int -> Int
+      h = (* 2) :: Int -> Int
+  map1 (g . h) fa === map1 g (map1 h fa)
+
+--------------------------------------------------------------------------------
+-- Contravariant
+
+-- | The functor laws for a /contravariant/ functor's @'map1'@ (domain 'Op'),
+-- observed through @obs@ since such functors are not 'Eq' or 'Show'.
+contravariantFunctorLaws ::
+  forall f r.
+  (MapArg1 Op f, Eq r, Show r) =>
+  Gen (f Int) ->
+  (f Int -> Int -> r) ->
+  Laws
+contravariantFunctorLaws genF obs =
+  Laws
+    "Functor (contravariant)"
+    [ ("Identity", contravariantIdentity genF obs),
+      ("Composition", contravariantComposition genF obs)
+    ]
+
+contravariantIdentity ::
+  forall f r.
+  (MapArg1 Op f, Eq r, Show r) =>
+  Gen (f Int) ->
+  (f Int -> Int -> r) ->
+  Property
+contravariantIdentity genF obs = property $ do
+  fa <- forAllWith (const "<opaque>") genF
+  a <- forAll genInt
+  obs (map1 (id :: Op Int Int) fa) a === obs fa a
+
+contravariantComposition ::
+  forall f r.
+  (MapArg1 Op f, Eq r, Show r) =>
+  Gen (f Int) ->
+  (f Int -> Int -> r) ->
+  Property
+contravariantComposition genF obs = property $ do
+  fa <- forAllWith (const "<opaque>") genF
+  a <- forAll genInt
+  let g = Op (+ 1) :: Op Int Int
+      h = Op (* 2) :: Op Int Int
+  obs (map1 (g . h) fa) a === obs (map1 g (map1 h fa)) a
+
+--------------------------------------------------------------------------------
+-- Invariant
+
+-- | The functor laws for an /invariant/ functor's @'map1'@ (domain
+-- @'Iso' ('->')@), observed through @obs@.
+invariantFunctorLaws ::
+  forall f r.
+  (MapArg1 (Iso (->)) f, Eq r, Show r) =>
+  Gen (f Int) ->
+  (f Int -> Int -> r) ->
+  Laws
+invariantFunctorLaws genF obs =
+  Laws
+    "Functor (invariant)"
+    [ ("Identity", invariantIdentity genF obs),
+      ("Composition", invariantComposition genF obs)
+    ]
+
+invariantIdentity ::
+  forall f r.
+  (MapArg1 (Iso (->)) f, Eq r, Show r) =>
+  Gen (f Int) ->
+  (f Int -> Int -> r) ->
+  Property
+invariantIdentity genF obs = property $ do
+  fa <- forAllWith (const "<opaque>") genF
+  a <- forAll genInt
+  obs (map1 (id :: Iso (->) Int Int) fa) a === obs fa a
+
+invariantComposition ::
+  forall f r.
+  (MapArg1 (Iso (->)) f, Eq r, Show r) =>
+  Gen (f Int) ->
+  (f Int -> Int -> r) ->
+  Property
+invariantComposition genF obs = property $ do
+  fa <- forAllWith (const "<opaque>") genF
+  a <- forAll genInt
+  let g = Iso (+ 1) (subtract 1) :: Iso (->) Int Int
+      h = Iso (* 2) (`div` 2) :: Iso (->) Int Int
+  obs (map1 (g . h) fa) a === obs (map1 g (map1 h fa)) a
+
+--------------------------------------------------------------------------------
+-- Isomorphism mapping (any variance)
+
+-- | The functor laws for 'liftIso', the identity-on-objects functor from the
+-- @'Iso' ('->')@ groupoid into a target category @cat@. Identity
+-- (@'liftIso' 'id' = 'id'@) and composition
+-- (@'liftIso' (i '.' j) = 'liftIso' i '.' 'liftIso' j@), with @'id'@ and @('.')@
+-- on the left in @'Iso' ('->')@ and on the right in @cat@. A @cat a b@ morphism
+-- is usually neither 'Eq' nor 'Show', so it is observed through @obs@ at the
+-- 'Int' witness. The target @cat@ is recovered from @obs@, so this bundle covers
+-- every 'LiftIso' instance, including those no exported functor witnesses.
+liftIsoLaws ::
+  forall cat r.
+  (LiftIso cat, Eq r, Show r) =>
+  (cat Int Int -> Int -> r) ->
+  Laws
+liftIsoLaws obs =
+  Laws
+    "liftIso"
+    [ ("Identity", liftIsoIdentity obs),
+      ("Composition", liftIsoComposition obs)
+    ]
+
+liftIsoIdentity ::
+  forall cat r.
+  (LiftIso cat, Eq r, Show r) =>
+  (cat Int Int -> Int -> r) ->
+  Property
+liftIsoIdentity obs = property $ do
+  a <- forAll genInt
+  obs (liftIso (id :: Iso (->) Int Int)) a === obs (id :: cat Int Int) a
+
+liftIsoComposition ::
+  forall cat r.
+  (LiftIso cat, Eq r, Show r) =>
+  (cat Int Int -> Int -> r) ->
+  Property
+liftIsoComposition obs = property $ do
+  a <- forAll genInt
+  let i = Iso (+ 1) (subtract 1) :: Iso (->) Int Int
+      j = Iso (* 2) (`div` 2) :: Iso (->) Int Int
+  obs (liftIso (i . j)) a === obs (liftIso i . liftIso j) a
+
+-- | The functor laws stated through @'mapIso'@, which maps a @('->')@
+-- isomorphism through a functor of /any/ variance. Identity
+-- (@'mapIso' 'id' = 'id'@) and composition
+-- (@'mapIso' (i '.' j) = 'mapIso' i '.' 'mapIso' j@), with @'id'@ and @('.')@ in
+-- the @'Iso' ('->')@ groupoid, observed through @obs@. The functor's domain
+-- category is recovered from @f@, so one bundle covers covariant, contravariant,
+-- and invariant functors.
+mapIsoLaws ::
+  forall cat f r.
+  (MapArg1 cat f, LiftIso cat, Eq r, Show r) =>
+  Gen (f Int) ->
+  (f Int -> Int -> r) ->
+  Laws
+mapIsoLaws genF obs =
+  Laws
+    "mapIso"
+    [ ("Identity", mapIsoIdentity genF obs),
+      ("Composition", mapIsoComposition genF obs)
+    ]
+
+mapIsoIdentity ::
+  forall cat f r.
+  (MapArg1 cat f, LiftIso cat, Eq r, Show r) =>
+  Gen (f Int) ->
+  (f Int -> Int -> r) ->
+  Property
+mapIsoIdentity genF obs = property $ do
+  fa <- forAllWith (const "<opaque>") genF
+  a <- forAll genInt
+  obs (mapIso (id :: Iso (->) Int Int) fa) a === obs fa a
+
+mapIsoComposition ::
+  forall cat f r.
+  (MapArg1 cat f, LiftIso cat, Eq r, Show r) =>
+  Gen (f Int) ->
+  (f Int -> Int -> r) ->
+  Property
+mapIsoComposition genF obs = property $ do
+  fa <- forAllWith (const "<opaque>") genF
+  a <- forAll genInt
+  let i = Iso (+ 1) (subtract 1) :: Iso (->) Int Int
+      j = Iso (* 2) (`div` 2) :: Iso (->) Int Int
+  obs (mapIso (i . j) fa) a === obs (mapIso i (mapIso j fa)) a
+
+--------------------------------------------------------------------------------
+-- Covariant bifunctor
+
+-- | The functor laws for a covariant bifunctor's @'map2'@ (its first argument),
+-- compared with 'Eq'.
+bifunctorLaws ::
+  forall p.
+  ( MapArg2 (->) (->) p,
+    forall a b. (Eq a, Eq b) => Eq (p a b),
+    forall a b. (Show a, Show b) => Show (p a b)
+  ) =>
+  (forall a b. Gen a -> Gen b -> Gen (p a b)) ->
+  Laws
+bifunctorLaws genP =
+  Laws
+    "Bifunctor"
+    [ ("map2 Identity", bifunctorIdentity genP),
+      ("map2 Composition", bifunctorComposition genP)
+    ]
+
+bifunctorIdentity ::
+  forall p.
+  ( MapArg2 (->) (->) p,
+    forall a b. (Eq a, Eq b) => Eq (p a b),
+    forall a b. (Show a, Show b) => Show (p a b)
+  ) =>
+  (forall a b. Gen a -> Gen b -> Gen (p a b)) ->
+  Property
+bifunctorIdentity genP = property $ do
+  p <- forAll (genP genInt genInt)
+  map2 (id :: Int -> Int) p === p
+
+bifunctorComposition ::
+  forall p.
+  ( MapArg2 (->) (->) p,
+    forall a b. (Eq a, Eq b) => Eq (p a b),
+    forall a b. (Show a, Show b) => Show (p a b)
+  ) =>
+  (forall a b. Gen a -> Gen b -> Gen (p a b)) ->
+  Property
+bifunctorComposition genP = property $ do
+  p <- forAll (genP genInt genInt)
+  let g = (+ 1) :: Int -> Int
+      h = (* 2) :: Int -> Int
+  map2 (g . h) p === map2 g (map2 h p)
+
+-- | The functor laws for a covariant @'map2'@ whose inner category is not
+-- @('->')@ (e.g. t'Op', where @'MapArg2' ('->') 'Op' 'Op'@ holds), observed
+-- through @obs@ since such bifunctors are function-shaped.
+observedBifunctorLaws ::
+  forall cat2 p r.
+  (MapArg2 (->) cat2 p, Eq r, Show r) =>
+  Gen (p Int Int) ->
+  (p Int Int -> Int -> r) ->
+  Laws
+observedBifunctorLaws genP obs =
+  Laws
+    "Bifunctor (observed)"
+    [ ("map2 Identity", observedBifunctorIdentity genP obs),
+      ("map2 Composition", observedBifunctorComposition genP obs)
+    ]
+
+observedBifunctorIdentity ::
+  forall cat2 p r.
+  (MapArg2 (->) cat2 p, Eq r, Show r) =>
+  Gen (p Int Int) ->
+  (p Int Int -> Int -> r) ->
+  Property
+observedBifunctorIdentity genP obs = property $ do
+  p <- forAllWith (const "<opaque>") genP
+  a <- forAll genInt
+  obs (map2 (id :: Int -> Int) p) a === obs p a
+
+observedBifunctorComposition ::
+  forall cat2 p r.
+  (MapArg2 (->) cat2 p, Eq r, Show r) =>
+  Gen (p Int Int) ->
+  (p Int Int -> Int -> r) ->
+  Property
+observedBifunctorComposition genP obs = property $ do
+  p <- forAllWith (const "<opaque>") genP
+  a <- forAll genInt
+  let g = (+ 1) :: Int -> Int
+      h = (* 2) :: Int -> Int
+  obs (map2 (g . h) p) a === obs (map2 g (map2 h p)) a
+
+--------------------------------------------------------------------------------
+-- Bifunctor isomorphism mapping (any variance)
+
+-- | The functor laws stated through @'Kindly.Bifunctor.bimapIso'@, which maps a
+-- @('->')@ isomorphism through each position of a bifunctor of /any/ variance.
+-- Identity (@'bimapIso' 'id' 'id' = 'id'@) and composition
+-- (@'bimapIso' (i '.' i') (j '.' j') = 'bimapIso' i j '.' 'bimapIso' i' j'@),
+-- with @'id'@ and @('.')@ in the @'Iso' ('->')@ groupoid, observed through
+-- @obs@. Each position's category is recovered from @p@, so one bundle covers
+-- every combination of variances.
+bimapIsoLaws ::
+  forall cat1 cat2 p r.
+  (Bifunctor cat1 cat2 p, LiftIso cat1, LiftIso cat2, Eq r, Show r) =>
+  Gen (p Int Int) ->
+  (p Int Int -> Int -> r) ->
+  Laws
+bimapIsoLaws genP obs =
+  Laws
+    "bimapIso"
+    [ ("Identity", bimapIsoIdentity genP obs),
+      ("Composition", bimapIsoComposition genP obs)
+    ]
+
+bimapIsoIdentity ::
+  forall cat1 cat2 p r.
+  (Bifunctor cat1 cat2 p, LiftIso cat1, LiftIso cat2, Eq r, Show r) =>
+  Gen (p Int Int) ->
+  (p Int Int -> Int -> r) ->
+  Property
+bimapIsoIdentity genP obs = property $ do
+  p <- forAllWith (const "<opaque>") genP
+  a <- forAll genInt
+  obs (bimapIso (id :: Iso (->) Int Int) (id :: Iso (->) Int Int) p) a === obs p a
+
+bimapIsoComposition ::
+  forall cat1 cat2 p r.
+  (Bifunctor cat1 cat2 p, LiftIso cat1, LiftIso cat2, Eq r, Show r) =>
+  Gen (p Int Int) ->
+  (p Int Int -> Int -> r) ->
+  Property
+bimapIsoComposition genP obs = property $ do
+  p <- forAllWith (const "<opaque>") genP
+  a <- forAll genInt
+  let i1 = Iso (+ 1) (subtract 1) :: Iso (->) Int Int
+      i2 = Iso (* 2) (`div` 2) :: Iso (->) Int Int
+      j1 = Iso (+ 3) (subtract 3) :: Iso (->) Int Int
+      j2 = Iso (* 5) (`div` 5) :: Iso (->) Int Int
+  obs (bimapIso (i1 . i2) (j1 . j2) p) a === obs (bimapIso i1 j1 (bimapIso i2 j2 p)) a
+
+--------------------------------------------------------------------------------
+-- Trifunctor
+
+-- | The functor laws for a covariant @'map3'@, observed through @obs@ so the
+-- bundle works for both 'Eq'-comparable trifunctors (observe with @const@)
+-- and function-shaped ones like 'Data.Profunctor.Forget'.
+observedTrifunctorLaws ::
+  forall cat2 cat3 p r.
+  (MapArg3 (->) cat2 cat3 p, Eq r, Show r) =>
+  Gen (p Int Int Int) ->
+  (p Int Int Int -> Int -> r) ->
+  Laws
+observedTrifunctorLaws genP obs =
+  Laws
+    "Trifunctor (observed)"
+    [ ("map3 Identity", observedTrifunctorIdentity genP obs),
+      ("map3 Composition", observedTrifunctorComposition genP obs)
+    ]
+
+observedTrifunctorIdentity ::
+  forall cat2 cat3 p r.
+  (MapArg3 (->) cat2 cat3 p, Eq r, Show r) =>
+  Gen (p Int Int Int) ->
+  (p Int Int Int -> Int -> r) ->
+  Property
+observedTrifunctorIdentity genP obs = property $ do
+  p <- forAllWith (const "<opaque>") genP
+  a <- forAll genInt
+  obs (map3 (id :: Int -> Int) p) a === obs p a
+
+observedTrifunctorComposition ::
+  forall cat2 cat3 p r.
+  (MapArg3 (->) cat2 cat3 p, Eq r, Show r) =>
+  Gen (p Int Int Int) ->
+  (p Int Int Int -> Int -> r) ->
+  Property
+observedTrifunctorComposition genP obs = property $ do
+  p <- forAllWith (const "<opaque>") genP
+  a <- forAll genInt
+  let g = (+ 1) :: Int -> Int
+      h = (* 2) :: Int -> Int
+  obs (map3 (g . h) p) a === obs (map3 g (map3 h p)) a
+
+--------------------------------------------------------------------------------
+-- Trifunctor isomorphism mapping (any variance)
+
+-- | The functor laws stated through @'Kindly.Trifunctor.trimapIso'@, which maps
+-- a @('->')@ isomorphism through each position of a trifunctor of /any/
+-- variance. Identity (@'trimapIso' 'id' 'id' 'id' = 'id'@) and composition
+-- (@'trimapIso' (i '.' i') (j '.' j') (k '.' k') =
+-- 'trimapIso' i j k '.' 'trimapIso' i' j' k'@), with @'id'@ and @('.')@ in the
+-- @'Iso' ('->')@ groupoid, observed through @obs@. Each position's category is
+-- recovered from @p@, so one bundle covers every combination of variances.
+trimapIsoLaws ::
+  forall cat1 cat2 cat3 p r.
+  (Trifunctor cat1 cat2 cat3 p, LiftIso cat1, LiftIso cat2, LiftIso cat3, Eq r, Show r) =>
+  Gen (p Int Int Int) ->
+  (p Int Int Int -> Int -> r) ->
+  Laws
+trimapIsoLaws genP obs =
+  Laws
+    "trimapIso"
+    [ ("Identity", trimapIsoIdentity genP obs),
+      ("Composition", trimapIsoComposition genP obs)
+    ]
+
+trimapIsoIdentity ::
+  forall cat1 cat2 cat3 p r.
+  (Trifunctor cat1 cat2 cat3 p, LiftIso cat1, LiftIso cat2, LiftIso cat3, Eq r, Show r) =>
+  Gen (p Int Int Int) ->
+  (p Int Int Int -> Int -> r) ->
+  Property
+trimapIsoIdentity genP obs = property $ do
+  p <- forAllWith (const "<opaque>") genP
+  a <- forAll genInt
+  obs (trimapIso (id :: Iso (->) Int Int) (id :: Iso (->) Int Int) (id :: Iso (->) Int Int) p) a === obs p a
+
+trimapIsoComposition ::
+  forall cat1 cat2 cat3 p r.
+  (Trifunctor cat1 cat2 cat3 p, LiftIso cat1, LiftIso cat2, LiftIso cat3, Eq r, Show r) =>
+  Gen (p Int Int Int) ->
+  (p Int Int Int -> Int -> r) ->
+  Property
+trimapIsoComposition genP obs = property $ do
+  p <- forAllWith (const "<opaque>") genP
+  a <- forAll genInt
+  let i1 = Iso (+ 1) (subtract 1) :: Iso (->) Int Int
+      i2 = Iso (* 2) (`div` 2) :: Iso (->) Int Int
+      j1 = Iso (+ 3) (subtract 3) :: Iso (->) Int Int
+      j2 = Iso (* 5) (`div` 5) :: Iso (->) Int Int
+      k1 = Iso (+ 7) (subtract 7) :: Iso (->) Int Int
+      k2 = Iso (* 11) (`div` 11) :: Iso (->) Int Int
+  obs (trimapIso (i1 . i2) (j1 . j2) (k1 . k2) p) a
+    === obs (trimapIso i1 j1 k1 (trimapIso i2 j2 k2 p)) a
+
+--------------------------------------------------------------------------------
+-- Profunctor
+
+-- | The functor laws for a /profunctor's/ @'map2'@ (domain 'Op' in its first
+-- argument), observed through @obs@ since profunctors are function-shaped and
+-- have no 'Eq' or 'Show'.
+profunctorLaws ::
+  forall p r.
+  (MapArg2 Op (->) p, Eq r, Show r) =>
+  Gen (p Int Int) ->
+  (p Int Int -> Int -> r) ->
+  Laws
+profunctorLaws genP obs =
+  Laws
+    "Profunctor"
+    [ ("map2 Identity", profunctorIdentity genP obs),
+      ("map2 Composition", profunctorComposition genP obs)
+    ]
+
+profunctorIdentity ::
+  forall p r.
+  (MapArg2 Op (->) p, Eq r, Show r) =>
+  Gen (p Int Int) ->
+  (p Int Int -> Int -> r) ->
+  Property
+profunctorIdentity genP obs = property $ do
+  p <- forAllWith (const "<opaque>") genP
+  a <- forAll genInt
+  obs (map2 (id :: Op Int Int) p) a === obs p a
+
+profunctorComposition ::
+  forall p r.
+  (MapArg2 Op (->) p, Eq r, Show r) =>
+  Gen (p Int Int) ->
+  (p Int Int -> Int -> r) ->
+  Property
+profunctorComposition genP obs = property $ do
+  p <- forAllWith (const "<opaque>") genP
+  a <- forAll genInt
+  let g = Op (+ 1) :: Op Int Int
+      h = Op (* 2) :: Op Int Int
+  obs (map2 (g . h) p) a === obs (map2 g (map2 h p)) a
diff --git a/laws/Kindly/Rank2/Laws.hs b/laws/Kindly/Rank2/Laws.hs
new file mode 100644
--- /dev/null
+++ b/laws/Kindly/Rank2/Laws.hs
@@ -0,0 +1,98 @@
+{-# LANGUAGE ImportQualifiedPost #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
+
+-- | @hedgehog-classes@ 'Laws' for the rank-2 selectors in "Kindly.Rank2".
+--
+-- Each bundle checks identity (@'map1' 'id' = 'id'@) and composition
+-- (@'map1' (n1 '.' n2) = 'map1' n1 '.' 'map1' n2@) for one selector, stated
+-- through the core map and the @Nat@ 'Cat.Category' so the sample morphisms live
+-- in the component category. One bundle per selector therefore covers every
+-- variance. Instantiate at a covariant witness for @d = (->)@, a contravariant
+-- one for @d = 'Data.Functor.Contravariant.Op'@, an invariant one for
+-- @d = 'Data.Isomorphism.Iso' (->)@. Hedgehog cannot generate natural
+-- transformations, so each is checked at a caller-chosen witness with two sample
+-- natural endo-transformations, comparing values with 'Eq'.
+module Kindly.Rank2.Laws
+  ( bmap1Laws,
+    bmap2Laws,
+    bmap3Laws,
+  )
+where
+
+--------------------------------------------------------------------------------
+
+import Control.Category qualified as Cat
+import Hedgehog (Gen, forAll, property, (===))
+import Hedgehog.Classes (Laws (..))
+import Kindly.Class (MapArg1, MapArg2, MapArg3, Nat (..), map1, map2, map3, type (~>))
+import Prelude
+
+--------------------------------------------------------------------------------
+
+bmap1Laws ::
+  forall c d b f.
+  (MapArg1 (c ~> d) b, Cat.Category c, Cat.Category d, Eq (b f), Show (b f)) =>
+  Gen (b f) ->
+  (forall x. d (f x) (f x)) ->
+  (forall x. d (f x) (f x)) ->
+  Laws
+bmap1Laws genB s1 s2 =
+  Laws
+    "bmap1"
+    [ ( "Identity",
+        property $ do
+          bf <- forAll genB
+          map1 (Cat.id :: (c ~> d) f f) bf === bf
+      ),
+      ( "Composition",
+        property $ do
+          bf <- forAll genB
+          map1 (Nat s1 Cat.. Nat s2) bf === map1 (Nat s1) (map1 (Nat s2) bf)
+      )
+    ]
+
+bmap2Laws ::
+  forall c d e b f h.
+  (MapArg2 (c ~> d) e b, Cat.Category c, Cat.Category d, Eq (b f h), Show (b f h)) =>
+  Gen (b f h) ->
+  (forall x. d (f x) (f x)) ->
+  (forall x. d (f x) (f x)) ->
+  Laws
+bmap2Laws genB s1 s2 =
+  Laws
+    "bmap2"
+    [ ( "Identity",
+        property $ do
+          bf <- forAll genB
+          map2 (Cat.id :: (c ~> d) f f) bf === bf
+      ),
+      ( "Composition",
+        property $ do
+          bf <- forAll genB
+          map2 (Nat s1 Cat.. Nat s2) bf === map2 (Nat s1) (map2 (Nat s2) bf)
+      )
+    ]
+
+bmap3Laws ::
+  forall c d e e' b f h i.
+  (MapArg3 (c ~> d) e e' b, Cat.Category c, Cat.Category d, Eq (b f h i), Show (b f h i)) =>
+  Gen (b f h i) ->
+  (forall x. d (f x) (f x)) ->
+  (forall x. d (f x) (f x)) ->
+  Laws
+bmap3Laws genB s1 s2 =
+  Laws
+    "bmap3"
+    [ ( "Identity",
+        property $ do
+          bf <- forAll genB
+          map3 (Cat.id :: (c ~> d) f f) bf === bf
+      ),
+      ( "Composition",
+        property $ do
+          bf <- forAll genB
+          map3 (Nat s1 Cat.. Nat s2) bf === map3 (Nat s1) (map3 (Nat s2) bf)
+      )
+    ]
diff --git a/src/Kindly.hs b/src/Kindly.hs
--- a/src/Kindly.hs
+++ b/src/Kindly.hs
@@ -8,6 +8,5 @@
 import Kindly.Bifunctor as M
 import Kindly.Class as M
 import Kindly.Functor as M
-import Kindly.Iso as M
 import Kindly.Rank2 as M
 import Kindly.Trifunctor as M
diff --git a/src/Kindly/Bifunctor.hs b/src/Kindly/Bifunctor.hs
--- a/src/Kindly/Bifunctor.hs
+++ b/src/Kindly/Bifunctor.hs
@@ -5,23 +5,49 @@
 module Kindly.Bifunctor
   ( Bifunctor,
     bimap,
+    bimapIso,
+    Iso (..),
     lmap,
     rmap,
+    FromBifunctor (..),
+    FromProfunctor (..),
   )
 where
 
 --------------------------------------------------------------------------------
 
+import Control.Applicative (WrappedArrow (..))
+import Control.Arrow (Arrow, Kleisli (..), arr)
 import Control.Category
 import Data.Bifunctor qualified as Hask
+import Data.Bifunctor.Biff (Biff (..))
+import Data.Bifunctor.Clown (Clown (..))
+import Data.Bifunctor.Flip (Flip (..))
+import Data.Bifunctor.Joker (Joker (..))
+import Data.Bifunctor.Product (Product (..))
+import Data.Bifunctor.Sum (Sum (..))
+import Data.Bifunctor.Tannen (Tannen (..))
+import Data.Bifunctor.Wrapped (WrappedBifunctor (..))
 import Data.Either (Either)
 import Data.Function (flip)
 import Data.Functor qualified as Hask
 import Data.Functor.Const (Const)
+import Data.Functor.Constant (Constant (..))
 import Data.Functor.Contravariant (Op (..))
+import Data.Isomorphism (Iso (..))
 import Data.Kind (Constraint, Type)
 import Data.Profunctor qualified as Hask
+import Data.Profunctor.Cayley qualified as Hask
+import Data.Profunctor.Choice qualified as Hask
+import Data.Profunctor.Closed qualified as Hask
+import Data.Profunctor.Composition qualified as Hask
+import Data.Profunctor.Mapping qualified as Hask
+import Data.Profunctor.Strong qualified as Hask
+import Data.Profunctor.Traversing qualified as Hask
+import Data.Profunctor.Yoneda qualified as Hask
 import Data.Semigroup qualified as Semigroup
+import Data.Semigroupoid.Dual (Dual (..))
+import Data.Tagged (Tagged (..))
 import Data.These (These)
 import GHC.Generics (K1)
 import Kindly.Class
@@ -39,6 +65,22 @@
 bimap :: forall cat1 cat2 p. (Bifunctor cat1 cat2 p) => forall a b a' b'. (a `cat1` a') -> (b `cat2` b') -> p a b -> p a' b'
 bimap f g = map2 f . map1 g
 
+-- | Map a @('->')@ isomorphism through each position of a 'Bifunctor',
+-- regardless of that position's variance. A bifunctor can always transport an
+-- isomorphism in either argument, so 'liftIso' reflects each iso into that
+-- position's category and drops whichever leg the category ignores. The first
+-- 'Iso' maps the first type argument, the second the second.
+--
+-- 'bimapIso' is to 'bimap' what 'Kindly.Functor.mapIso' is to
+-- 'Kindly.Functor.fmap'.
+bimapIso ::
+  (Bifunctor cat1 cat2 p, LiftIso cat1, LiftIso cat2) =>
+  Iso (->) a a' ->
+  Iso (->) b b' ->
+  p a b ->
+  p a' b'
+bimapIso i j = bimap (liftIso i) (liftIso j)
+
 -- | Lift a morphism @cat1 a b@ into a function @p a x -> p b x@.
 lmap :: (Category cat2, Bifunctor cat1 cat2 p) => (a `cat1` b) -> p a x -> p b x
 lmap = flip bimap id
@@ -49,6 +91,10 @@
 
 --------------------------------------------------------------------------------
 
+-- | A @DerivingVia@ adapter: give any base @Bifunctor@ a 'CategoricalFunctor'
+-- instance.
+--
+-- > deriving via (FromBifunctor MyType) instance CategoricalFunctor MyType
 newtype FromBifunctor f a b = FromBifunctor (f a b)
   deriving newtype (Hask.Functor, Hask.Bifunctor)
 
@@ -89,35 +135,73 @@
 
 deriving via (FromBifunctor (Const :: Type -> Type -> Type)) instance CategoricalFunctor (Const :: Type -> Type -> Type)
 
+instance CategoricalFunctor (Constant :: Type -> Type -> Type) where
+  type Dom Constant = (->)
+  type Cod Constant = (->) ~> (->)
+
+  map f = Nat (\(Constant a) -> Constant (f a))
+
 deriving via (FromBifunctor (K1 i :: Type -> Type -> Type)) instance CategoricalFunctor (K1 i :: Type -> Type -> Type)
 
---------------------------------------------------------------------------------
--- Covariant MapArg2 instances
+instance (forall x. MapArg1 (->) (p x)) => CategoricalFunctor (Flip p :: Type -> Type -> Type) where
+  type Dom (Flip p) = (->)
+  type Cod (Flip p) = (->) ~> (->)
 
-instance MapArg2 (->) (->) (,)
+  map f = Nat (\(Flip pxa) -> Flip (map1 f pxa))
 
-instance MapArg2 (->) (->) ((,,) a)
+instance (FunctorOf (->) (->) f) => CategoricalFunctor (Clown f :: Type -> Type -> Type) where
+  type Dom (Clown f) = (->)
+  type Cod (Clown f) = (->) ~> (->)
 
-instance MapArg2 (->) (->) ((,,,) a b)
+  map f = Nat (\(Clown fa) -> Clown (map f fa))
 
-instance MapArg2 (->) (->) ((,,,,) a b c)
+instance CategoricalFunctor (Joker g :: Type -> Type -> Type) where
+  type Dom (Joker g) = (->)
+  type Cod (Joker g) = (->) ~> (->)
 
-instance MapArg2 (->) (->) ((,,,,,) a b c d)
+  map _ = Nat (\(Joker gb) -> Joker gb)
 
-instance MapArg2 (->) (->) ((,,,,,,) a b c d e)
+instance (MapArg2 (->) (->) p, MapArg2 (->) (->) q) => CategoricalFunctor (Product p q) where
+  type Dom (Product p q) = (->)
+  type Cod (Product p q) = (->) ~> (->)
 
-instance MapArg2 (->) (->) Either
+  map f = Nat (\(Pair pab qab) -> Pair (map2 f pab) (map2 f qab))
 
--- instance MapArg2 (->) (->) These
+instance (MapArg2 (->) (->) p, MapArg2 (->) (->) q) => CategoricalFunctor (Sum p q) where
+  type Dom (Sum p q) = (->)
+  type Cod (Sum p q) = (->) ~> (->)
 
-instance MapArg2 (->) (->) Semigroup.Arg
+  map f =
+    Nat
+      ( \case
+          L2 pab -> L2 (map2 f pab)
+          R2 qab -> R2 (map2 f qab)
+      )
 
-instance MapArg2 (->) (->) (Const :: Type -> Type -> Type)
+instance (FunctorOf (->) (->) f, MapArg2 (->) (->) p) => CategoricalFunctor (Tannen f p) where
+  type Dom (Tannen f p) = (->)
+  type Cod (Tannen f p) = (->) ~> (->)
 
-instance MapArg2 (->) (->) (K1 i :: Type -> Type -> Type)
+  map f = Nat (\(Tannen fp) -> Tannen (map1 (map2 f) fp))
 
+instance (MapArg2 (->) (->) p, FunctorOf (->) (->) f) => CategoricalFunctor (Biff p f g :: Type -> Type -> Type) where
+  type Dom (Biff p f g) = (->)
+  type Cod (Biff p f g) = (->) ~> (->)
+
+  map f = Nat (\(Biff pfg) -> Biff (map2 (map1 f) pfg))
+
+instance (MapArg2 (->) (->) p) => CategoricalFunctor (WrappedBifunctor p) where
+  type Dom (WrappedBifunctor p) = (->)
+  type Cod (WrappedBifunctor p) = (->) ~> (->)
+
+  map f = Nat (\(WrapBifunctor pab) -> WrapBifunctor (map2 f pab))
+
 --------------------------------------------------------------------------------
 
+-- | A @DerivingVia@ adapter: give any @Profunctor@ a 'CategoricalFunctor'
+-- instance.
+--
+-- > deriving via (FromProfunctor MyType) instance CategoricalFunctor MyType
 newtype FromProfunctor f a b = FromProfunctor (f a b)
   deriving newtype (Hask.Functor, Hask.Profunctor)
 
@@ -140,11 +224,167 @@
 
 deriving via (FromProfunctor (->)) instance CategoricalFunctor (->)
 
--- TODO: Add remaining Profunctor instances
+instance CategoricalFunctor (Kleisli m) where
+  type Dom (Kleisli m) = Op
+  type Cod (Kleisli m) = (->) ~> (->)
 
+  map (Op f) = Nat (\(Kleisli g) -> Kleisli (g . f))
+
+instance CategoricalFunctor (Hask.Star f :: Type -> Type -> Type) where
+  type Dom (Hask.Star f) = Op
+  type Cod (Hask.Star f) = (->) ~> (->)
+
+  map (Op f) = Nat (\(Hask.Star g) -> Hask.Star (g . f))
+
+instance (FunctorOf (->) (->) f) => CategoricalFunctor (Hask.Costar f :: Type -> Type -> Type) where
+  type Dom (Hask.Costar f) = Op
+  type Cod (Hask.Costar f) = (->) ~> (->)
+
+  map (Op f) = Nat (\(Hask.Costar g) -> Hask.Costar (g . map f))
+
+instance CategoricalFunctor (Hask.Forget r :: Type -> Type -> Type) where
+  type Dom (Hask.Forget r) = Op
+  type Cod (Hask.Forget r) = (->) ~> (->)
+
+  map (Op f) = Nat (\(Hask.Forget g) -> Hask.Forget (g . f))
+
+instance (Arrow p) => CategoricalFunctor (WrappedArrow p) where
+  type Dom (WrappedArrow p) = Op
+  type Cod (WrappedArrow p) = (->) ~> (->)
+
+  map (Op f) = Nat (\(WrapArrow g) -> WrapArrow (g . arr f))
+
+instance (MapArg2 Op (->) q) => CategoricalFunctor (Hask.Procompose p q :: Type -> Type -> Type) where
+  type Dom (Hask.Procompose p q) = Op
+  type Cod (Hask.Procompose p q) = (->) ~> (->)
+
+  map (Op f) = Nat (\(Hask.Procompose pxc qdx) -> Hask.Procompose pxc (map2 (Op f) qdx))
+
+instance (MapArg2 Op (->) q) => CategoricalFunctor (Hask.Rift p q :: Type -> Type -> Type) where
+  type Dom (Hask.Rift p q) = Op
+  type Cod (Hask.Rift p q) = (->) ~> (->)
+
+  map (Op f) = Nat (\(Hask.Rift g) -> Hask.Rift (map2 (Op f) . g))
+
+instance CategoricalFunctor (Hask.Yoneda p) where
+  type Dom (Hask.Yoneda p) = Op
+  type Cod (Hask.Yoneda p) = (->) ~> (->)
+
+  map (Op f) = Nat (\(Hask.Yoneda g) -> Hask.Yoneda (\l r -> g (f . l) r))
+
+instance CategoricalFunctor (Hask.Coyoneda p) where
+  type Dom (Hask.Coyoneda p) = Op
+  type Cod (Hask.Coyoneda p) = (->) ~> (->)
+
+  map (Op f) = Nat (\(Hask.Coyoneda l r p) -> Hask.Coyoneda (l . f) r p)
+
+instance (FunctorOf (->) (->) f, MapArg2 Op (->) p) => CategoricalFunctor (Hask.Cayley f p) where
+  type Dom (Hask.Cayley f p) = Op
+  type Cod (Hask.Cayley f p) = (->) ~> (->)
+
+  map (Op g) = Nat (\(Hask.Cayley fp) -> Hask.Cayley (map (map2 (Op g)) fp))
+
+instance (MapArg2 Op (->) p) => CategoricalFunctor (Hask.Tambara p) where
+  type Dom (Hask.Tambara p) = Op
+  type Cod (Hask.Tambara p) = (->) ~> (->)
+
+  map (Op f) = Nat (\(Hask.Tambara t) -> Hask.Tambara (map2 (Op (\(a, c) -> (f a, c))) t))
+
+instance CategoricalFunctor (Hask.Pastro p) where
+  type Dom (Hask.Pastro p) = Op
+  type Cod (Hask.Pastro p) = (->) ~> (->)
+
+  map (Op f) = Nat (\(Hask.Pastro l m r) -> Hask.Pastro l m (r . f))
+
+instance CategoricalFunctor (Hask.Cotambara q) where
+  type Dom (Hask.Cotambara q) = Op
+  type Cod (Hask.Cotambara q) = (->) ~> (->)
+
+  map (Op f) = Nat (\(Hask.Cotambara n r) -> Hask.Cotambara n (Hask.lmap f r))
+
+instance CategoricalFunctor (Hask.Copastro p) where
+  type Dom (Hask.Copastro p) = Op
+  type Cod (Hask.Copastro p) = (->) ~> (->)
+
+  map (Op f) = Nat (\(Hask.Copastro g) -> Hask.Copastro (Hask.lmap f . g))
+
+instance (MapArg2 Op (->) p) => CategoricalFunctor (Hask.TambaraSum p) where
+  type Dom (Hask.TambaraSum p) = Op
+  type Cod (Hask.TambaraSum p) = (->) ~> (->)
+
+  map (Op f) = Nat (\(Hask.TambaraSum t) -> Hask.TambaraSum (map2 (Op (map2 f)) t))
+
+instance CategoricalFunctor (Hask.PastroSum p) where
+  type Dom (Hask.PastroSum p) = Op
+  type Cod (Hask.PastroSum p) = (->) ~> (->)
+
+  map (Op f) = Nat (\(Hask.PastroSum l m r) -> Hask.PastroSum l m (r . f))
+
+instance CategoricalFunctor (Hask.CotambaraSum q) where
+  type Dom (Hask.CotambaraSum q) = Op
+  type Cod (Hask.CotambaraSum q) = (->) ~> (->)
+
+  map (Op f) = Nat (\(Hask.CotambaraSum n r) -> Hask.CotambaraSum n (Hask.lmap f r))
+
+instance CategoricalFunctor (Hask.CopastroSum p) where
+  type Dom (Hask.CopastroSum p) = Op
+  type Cod (Hask.CopastroSum p) = (->) ~> (->)
+
+  map (Op f) = Nat (\(Hask.CopastroSum g) -> Hask.CopastroSum (Hask.lmap f . g))
+
+instance (MapArg2 Op (->) p) => CategoricalFunctor (Hask.Closure p) where
+  type Dom (Hask.Closure p) = Op
+  type Cod (Hask.Closure p) = (->) ~> (->)
+
+  map (Op f) = Nat (\(Hask.Closure t) -> Hask.Closure (map2 (Op (f .)) t))
+
+instance CategoricalFunctor (Hask.Environment p) where
+  type Dom (Hask.Environment p) = Op
+  type Cod (Hask.Environment p) = (->) ~> (->)
+
+  map (Op f) = Nat (\(Hask.Environment l m r) -> Hask.Environment l m (r . f))
+
+instance CategoricalFunctor (Hask.FreeTraversing p) where
+  type Dom (Hask.FreeTraversing p) = Op
+  type Cod (Hask.FreeTraversing p) = (->) ~> (->)
+
+  map (Op f) = Nat (\(Hask.FreeTraversing l m r) -> Hask.FreeTraversing l m (r . f))
+
+instance (MapArg2 Op (->) p) => CategoricalFunctor (Hask.CofreeTraversing p) where
+  type Dom (Hask.CofreeTraversing p) = Op
+  type Cod (Hask.CofreeTraversing p) = (->) ~> (->)
+
+  map (Op f) = Nat (\(Hask.CofreeTraversing t) -> Hask.CofreeTraversing (map2 (Op (Hask.fmap f)) t))
+
+instance CategoricalFunctor (Hask.FreeMapping p) where
+  type Dom (Hask.FreeMapping p) = Op
+  type Cod (Hask.FreeMapping p) = (->) ~> (->)
+
+  map (Op f) = Nat (\(Hask.FreeMapping l m r) -> Hask.FreeMapping l m (r . f))
+
+instance (MapArg2 Op (->) p) => CategoricalFunctor (Hask.CofreeMapping p) where
+  type Dom (Hask.CofreeMapping p) = Op
+  type Cod (Hask.CofreeMapping p) = (->) ~> (->)
+
+  map (Op f) = Nat (\(Hask.CofreeMapping t) -> Hask.CofreeMapping (map2 (Op (Hask.fmap f)) t))
+
+instance CategoricalFunctor (Tagged :: Type -> Type -> Type) where
+  type Dom Tagged = Op
+  type Cod Tagged = (->) ~> (->)
+
+  map _ = Nat (\(Tagged b) -> Tagged b)
+
 --------------------------------------------------------------------------------
--- Profunctorial MapArg2 instances
+-- Bifunctors into a non-(->) inner category
 
-instance MapArg2 Op (->) (->)
+instance CategoricalFunctor Op where
+  type Dom Op = (->)
+  type Cod Op = Op ~> (->)
 
--- TODO: Add remaining Profunctor instances
+  map f = Nat (\(Op g) -> Op (f . g))
+
+instance (forall x. MapArg1 (->) (k x)) => CategoricalFunctor (Dual k :: Type -> Type -> Type) where
+  type Dom (Dual k) = (->)
+  type Cod (Dual k) = Op ~> (->)
+
+  map f = Nat (\(Dual kba) -> Dual (map1 f kba))
diff --git a/src/Kindly/Class.hs b/src/Kindly/Class.hs
--- a/src/Kindly/Class.hs
+++ b/src/Kindly/Class.hs
@@ -1,11 +1,52 @@
-module Kindly.Class where
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE KindSignatures #-}
 
+module Kindly.Class
+  ( -- * Category-polymorphic functors
+    CategoricalFunctor (..),
+    Cat,
+    FunctorOf,
+
+    -- * Natural transformations
+    Nat (..),
+    runNat,
+    type (~>),
+
+    -- * One-, two-, and three-argument interfaces
+    MapArg1 (..),
+    MapArg2 (..),
+    MapArg3 (..),
+
+    -- * Lifting @(->)@ isomorphisms
+    LiftIso (..),
+
+    -- * Generic deriving
+    GenericK,
+    deriveGenericK,
+  )
+where
+
 --------------------------------------------------------------------------------
 
+import Control.Arrow (Kleisli (..))
 import Control.Category
+import Data.Functor.Contravariant (Op (..))
+import Data.Isomorphism (Iso (..))
 import Data.Kind (Constraint)
+import Data.Profunctor (Star (..))
 import Data.Semigroupoid (Semigroupoid (..))
-import GHC.Base (Type)
+#if MIN_VERSION_base(4,17,0)
+-- On GHC 9.4+ (@base >= 4.17@) @~@ is an ordinary type operator rather than
+-- built-in syntax, so under @NoImplicitPrelude@ it must be brought into scope.
+-- Earlier GHCs still treat @~@ as built-in syntax and do not export it.
+import Data.Type.Equality (type (~))
+#endif
+import GHC.Base (Functor (fmap), Monad, Type, pure)
+import Generics.Kind
+import Generics.Kind.TH (deriveGenericK)
+import Prelude (Bool (..))
 
 --------------------------------------------------------------------------------
 
@@ -26,7 +67,33 @@
   type Cod f :: to -> to -> Type
 
   -- | Lift a function of type @Dom f a b@ into a function of type @Cod f (f a) (f b)@.
+  --
+  -- 'map' has a generic default. A datatype with a @kind-generics@ 'GenericK'
+  -- instance (from 'deriveGenericK') gets a 'CategoricalFunctor' instance from an
+  -- empty body that gives only 'Dom' and 'Cod'. The default reads each argument's
+  -- variance off the field structure, so an instance of the wrong sign is a
+  -- compile error rather than a wrong answer.
+  --
+  -- @
+  -- data Pred a = Pred (a -> Bool)
+
+  -- $(deriveGenericK ''Pred)
+  --
+  -- instance CategoricalFunctor Pred where
+  --   type Dom Pred = Op
+  --   type Cod Pred = (->)
+  -- @
+  --
+  -- This covers covariant (@Dom = (->)@), contravariant (@Op@), and invariant
+  -- (@Iso (->)@) single-argument functors, and bifunctors, profunctors, and
+  -- trifunctors in any per-argument combination of those variances. It does not
+  -- cover non-@(->)@ domains such as @Star Maybe@ (filtering), rank-2 functors,
+  -- constructors carrying constraints or existentials, or a recursive field whose
+  -- head has no base @Functor@.
+
   map :: Dom f a b -> Cod f (f a) (f b)
+  default map :: (GMapFull (Dom f) (Cod f) f) => Dom f a b -> Cod f (f a) (f b)
+  map = gmapFull
 
 type Cat i = i -> i -> Type
 
@@ -66,8 +133,406 @@
 
 class (FunctorOf cat1 (cat2 ~> (->)) p, forall x. MapArg1 cat2 (p x)) => MapArg2 cat1 cat2 p | p -> cat2 cat2 where
   map2 :: (a `cat1` b) -> forall x. p a x -> p b x
-  map2 = runNat . map
+  map2 f = runNat (map @_ @_ @p f)
 
 class (FunctorOf cat1 (cat2 ~> cat3 ~> (->)) p, forall x. MapArg2 cat2 cat3 (p x)) => MapArg3 cat1 cat2 cat3 p | p -> cat1 cat2 cat3 where
   map3 :: (a `cat1` b) -> forall x y. p a x y -> p b x y
-  map3 f = runNat (runNat (map f))
+  map3 f = runNat (runNat (map @_ @_ @p f))
+
+--------------------------------------------------------------------------------
+
+-- | Every 'CategoricalFunctor' whose codomain is a (nested) functor category
+-- ending in @(->)@ is a @MapArgN@ via the default methods. These blanket
+-- instances mean a 'CategoricalFunctor' instance never needs a paired @MapArgN@
+-- instance. The domain category @cat1@ is recovered from @Dom p@, so one
+-- instance covers every variance (covariant @(->)@, contravariant 'Op',
+-- invariant @'Data.Isomorphism.Iso' (->)@).
+instance (CategoricalFunctor p, Cod p ~ (->), cat1 ~ Dom p) => MapArg1 cat1 p
+
+instance
+  (CategoricalFunctor p, Cod p ~ (cat2 ~> (->)), cat1 ~ Dom p, forall x. MapArg1 cat2 (p x)) =>
+  MapArg2 cat1 cat2 p
+
+instance
+  (CategoricalFunctor p, Cod p ~ (cat2 ~> cat3 ~> (->)), cat1 ~ Dom p, forall x. MapArg2 cat2 cat3 (p x)) =>
+  MapArg3 cat1 cat2 cat3 p
+
+--------------------------------------------------------------------------------
+
+-- | Lift a @('->')@ isomorphism into an arbitrary category @cat@. This is the
+-- identity-on-objects functor from the @('->')@ core groupoid (embodied by
+-- @'Iso' ('->')@) into @cat@. Objects stay put, and an isomorphism becomes a
+-- @cat@ morphism that keeps whichever leg @cat@ can use and discards the other.
+--
+-- Every category admits this functor, which is what lets a 'CategoricalFunctor'
+-- of /any/ variance map an isomorphism, whether its domain is @('->')@
+-- (covariant), 'Op' (contravariant), or @'Iso' ('->')@ (invariant). See
+-- 'Kindly.Functor.mapIso'.
+--
+-- 'liftIso' fixes its source to @'Iso' ('->')@, so @a@ and @b@ are 'Type' and
+-- the kind is @'Cat' 'Type'@. Supporting rank-2 functors (whose objects are type
+-- constructors) needs more than @PolyKinds@. There the universally available
+-- isos are natural isomorphisms, @'Iso' ((->) '~>' (->))@, not @'Iso' ('->')@,
+-- so the source groupoid has to be abstracted too, e.g. a second parameter
+-- @LiftIso src cat@ carrying the core groupoid at that kind.
+--
+-- === Laws
+--
+-- [Identity]    @'liftIso' 'id' == 'id'@
+-- [Composition] @'liftIso' (i '.' j) == 'liftIso' i '.' 'liftIso' j@
+type LiftIso :: Cat Type -> Constraint
+class (Category cat) => LiftIso cat where
+  liftIso :: Iso (->) a b -> cat a b
+
+-- | A covariant @('->')@ functor keeps the forward leg.
+instance LiftIso (->) where
+  liftIso :: Iso (->) a b -> a -> b
+  liftIso = embed
+
+-- | A contravariant 'Op' functor keeps the backward leg.
+instance LiftIso Op where
+  liftIso :: Iso (->) a b -> Op a b
+  liftIso i = Op (project i)
+
+-- | An invariant @'Iso' ('->')@ functor keeps both legs. The lift is the identity.
+instance LiftIso (Iso (->)) where
+  liftIso :: Iso (->) a b -> Iso (->) a b
+  liftIso = id
+
+-- | A @'Star' f@ Kleisli arrow keeps the forward leg, returning it in @f@ via
+-- 'pure'. Needs @'Monad' f@, matching its @'Category' ('Star' f)@ instance.
+-- @Star Maybe@ is the domain the library uses for filtering (@Filterable@)
+-- functors.
+instance (Monad f) => LiftIso (Star f) where
+  liftIso :: Iso (->) a b -> Star f a b
+  liftIso i = Star (pure . embed i)
+
+-- | A @'Kleisli' m@ arrow is @Star@ by another name (base's copy of the same
+-- @a -> m b@ type), so its lift is identical.
+instance (Monad m) => LiftIso (Kleisli m) where
+  liftIso :: Iso (->) a b -> Kleisli m a b
+  liftIso i = Kleisli (pure . embed i)
+
+--------------------------------------------------------------------------------
+-- Internals backing map's generic default (see the 'map' Haddock for the
+-- user-facing story). None of the names below are exported. The default
+-- dispatches on the instance's Dom and Cod through GMapFull, which routes to a
+-- position interpreter over the RepK.
+
+-- Covariant interpreter over a RepK, mirroring
+-- @Generics.Kind.Derive.FunctorPosition@ (reproduced to avoid depending on
+-- @kind-generics-deriving@, which pulls in @aeson@).
+class GFunctorPos (f :: LoT k -> Type) (v :: TyVar k Type) (as :: LoT k) (bs :: LoT k) where
+  gfmapp :: (Interpret ('Var v) as -> Interpret ('Var v) bs) -> f as -> f bs
+
+instance GFunctorPos U1 v as bs where
+  gfmapp _ U1 = U1
+
+instance (GFunctorPos f v as bs) => GFunctorPos (M1 i c f) v as bs where
+  gfmapp v (M1 x) = M1 (gfmapp @_ @f @v @as @bs v x)
+
+instance (GFunctorPos f v as bs, GFunctorPos g v as bs) => GFunctorPos (f :+: g) v as bs where
+  gfmapp v (L1 x) = L1 (gfmapp @_ @f @v @as @bs v x)
+  gfmapp v (R1 x) = R1 (gfmapp @_ @g @v @as @bs v x)
+
+instance (GFunctorPos f v as bs, GFunctorPos g v as bs) => GFunctorPos (f :*: g) v as bs where
+  gfmapp v (x :*: y) = gfmapp @_ @f @v @as @bs v x :*: gfmapp @_ @g @v @as @bs v y
+
+instance (GFunctorArgPos t v as bs (ContainsTyVar v t)) => GFunctorPos (Field t) v as bs where
+  gfmapp v (Field x) = Field (gfmappf @_ @t @v @as @bs @(ContainsTyVar v t) v x)
+
+class GFunctorArgPos (t :: Atom d Type) (v :: TyVar d Type) (as :: LoT d) (bs :: LoT d) (p :: Bool) where
+  gfmappf :: (Interpret ('Var v) as -> Interpret ('Var v) bs) -> Interpret t as -> Interpret t bs
+
+instance (Interpret t as ~ Interpret t bs) => GFunctorArgPos t v as bs 'False where
+  gfmappf _ = id
+
+instance
+  ( Functor (Interpret f as),
+    Interpret f as ~ Interpret f bs,
+    GFunctorArgPos x v as bs (ContainsTyVar v x)
+  ) =>
+  GFunctorArgPos (f ':@: x) v as bs 'True
+  where
+  gfmappf f = fmap (gfmappf @_ @x @v @as @bs @(ContainsTyVar v x) f)
+
+instance (w ~ v) => GFunctorArgPos ('Var w) v as bs 'True where
+  gfmappf f = f
+
+-- Contravariant interpreter. At a function field the domain is mapped by the
+-- covariant interpreter and the codomain recurses contravariantly.
+class GContraPos (f :: LoT k -> Type) (v :: TyVar k Type) (as :: LoT k) (bs :: LoT k) where
+  gcontrap :: (Interpret ('Var v) bs -> Interpret ('Var v) as) -> f as -> f bs
+
+instance GContraPos U1 v as bs where
+  gcontrap _ U1 = U1
+
+instance (GContraPos f v as bs) => GContraPos (M1 i c f) v as bs where
+  gcontrap v (M1 x) = M1 (gcontrap @_ @f @v @as @bs v x)
+
+instance (GContraPos f v as bs, GContraPos g v as bs) => GContraPos (f :+: g) v as bs where
+  gcontrap v (L1 x) = L1 (gcontrap @_ @f @v @as @bs v x)
+  gcontrap v (R1 x) = R1 (gcontrap @_ @g @v @as @bs v x)
+
+instance (GContraPos f v as bs, GContraPos g v as bs) => GContraPos (f :*: g) v as bs where
+  gcontrap v (x :*: y) = gcontrap @_ @f @v @as @bs v x :*: gcontrap @_ @g @v @as @bs v y
+
+instance (GContraArgPos t v as bs (ContainsTyVar v t)) => GContraPos (Field t) v as bs where
+  gcontrap v (Field x) = Field (gcontrapf @_ @t @v @as @bs @(ContainsTyVar v t) v x)
+
+class GContraArgPos (t :: Atom d Type) (v :: TyVar d Type) (as :: LoT d) (bs :: LoT d) (p :: Bool) where
+  gcontrapf :: (Interpret ('Var v) bs -> Interpret ('Var v) as) -> Interpret t as -> Interpret t bs
+
+instance (Interpret t as ~ Interpret t bs) => GContraArgPos t v as bs 'False where
+  gcontrapf _ = id
+
+instance
+  ( GFunctorArgPos dom v bs as (ContainsTyVar v dom),
+    GContraArgPos cod v as bs (ContainsTyVar v cod)
+  ) =>
+  GContraArgPos (('Kon (->) ':@: dom) ':@: cod) v as bs 'True
+  where
+  gcontrapf k field =
+    gcontrapf @_ @cod @v @as @bs @(ContainsTyVar v cod) k
+      . field
+      . gfmappf @_ @dom @v @bs @as @(ContainsTyVar v dom) k
+
+-- Invariant interpreter. Threads both legs of an isomorphism, swapping them at
+-- each function field.
+class GInvPos (f :: LoT k -> Type) (v :: TyVar k Type) (as :: LoT k) (bs :: LoT k) where
+  ginvp ::
+    (Interpret ('Var v) as -> Interpret ('Var v) bs) ->
+    (Interpret ('Var v) bs -> Interpret ('Var v) as) ->
+    f as ->
+    f bs
+
+instance GInvPos U1 v as bs where
+  ginvp _ _ U1 = U1
+
+instance (GInvPos f v as bs) => GInvPos (M1 i c f) v as bs where
+  ginvp fwd bwd (M1 x) = M1 (ginvp @_ @f @v @as @bs fwd bwd x)
+
+instance (GInvPos f v as bs, GInvPos g v as bs) => GInvPos (f :+: g) v as bs where
+  ginvp fwd bwd (L1 x) = L1 (ginvp @_ @f @v @as @bs fwd bwd x)
+  ginvp fwd bwd (R1 x) = R1 (ginvp @_ @g @v @as @bs fwd bwd x)
+
+instance (GInvPos f v as bs, GInvPos g v as bs) => GInvPos (f :*: g) v as bs where
+  ginvp fwd bwd (x :*: y) = ginvp @_ @f @v @as @bs fwd bwd x :*: ginvp @_ @g @v @as @bs fwd bwd y
+
+instance (GInvArgPos t v as bs (ContainsTyVar v t)) => GInvPos (Field t) v as bs where
+  ginvp fwd bwd (Field x) = Field (ginvpf @_ @t @v @as @bs @(ContainsTyVar v t) fwd bwd x)
+
+class GInvArgPos (t :: Atom d Type) (v :: TyVar d Type) (as :: LoT d) (bs :: LoT d) (p :: Bool) where
+  ginvpf ::
+    (Interpret ('Var v) as -> Interpret ('Var v) bs) ->
+    (Interpret ('Var v) bs -> Interpret ('Var v) as) ->
+    Interpret t as ->
+    Interpret t bs
+
+instance (Interpret t as ~ Interpret t bs) => GInvArgPos t v as bs 'False where
+  ginvpf _ _ = id
+
+instance (w ~ v) => GInvArgPos ('Var w) v as bs 'True where
+  ginvpf fwd _ = fwd
+
+instance
+  ( GInvArgPos dom v bs as (ContainsTyVar v dom),
+    GInvArgPos cod v as bs (ContainsTyVar v cod)
+  ) =>
+  GInvArgPos (('Kon (->) ':@: dom) ':@: cod) v as bs 'True
+  where
+  ginvpf fwd bwd field =
+    ginvpf @_ @cod @v @as @bs @(ContainsTyVar v cod) fwd bwd
+      . field
+      . ginvpf @_ @dom @v @bs @as @(ContainsTyVar v dom) bwd fwd
+
+instance
+  {-# OVERLAPPABLE #-}
+  ( Functor (Interpret f as),
+    Interpret f as ~ Interpret f bs,
+    GInvArgPos x v as bs (ContainsTyVar v x)
+  ) =>
+  GInvArgPos (f ':@: x) v as bs 'True
+  where
+  ginvpf fwd bwd = fmap (ginvpf @_ @x @v @as @bs @(ContainsTyVar v x) fwd bwd)
+
+--------------------------------------------------------------------------------
+-- The wrappers quantify the assignment internally so a plain
+-- @G...K (RepK f)@ suffices as a constraint.
+
+class GFunctorK (rep :: LoT (Type -> Type) -> Type) where
+  gfmapK :: (a -> b) -> rep (LoT1 a) -> rep (LoT1 b)
+
+instance (forall a b. GFunctorPos rep 'VZ (LoT1 a) (LoT1 b)) => GFunctorK rep where
+  gfmapK :: forall a b. (a -> b) -> rep (LoT1 a) -> rep (LoT1 b)
+  gfmapK = gfmapp @_ @rep @'VZ @(LoT1 a) @(LoT1 b)
+
+class GContraK (rep :: LoT (Type -> Type) -> Type) where
+  gcontraK :: (b -> a) -> rep (LoT1 a) -> rep (LoT1 b)
+
+instance (forall a b. GContraPos rep 'VZ (LoT1 a) (LoT1 b)) => GContraK rep where
+  gcontraK :: forall a b. (b -> a) -> rep (LoT1 a) -> rep (LoT1 b)
+  gcontraK = gcontrap @_ @rep @'VZ @(LoT1 a) @(LoT1 b)
+
+class GInvK (rep :: LoT (Type -> Type) -> Type) where
+  ginvK :: (a -> b) -> (b -> a) -> rep (LoT1 a) -> rep (LoT1 b)
+
+instance (forall a b. GInvPos rep 'VZ (LoT1 a) (LoT1 b)) => GInvK rep where
+  ginvK :: forall a b. (a -> b) -> (b -> a) -> rep (LoT1 a) -> rep (LoT1 b)
+  ginvK = ginvp @_ @rep @'VZ @(LoT1 a) @(LoT1 b)
+
+class GBiFirstK (rep :: LoT (Type -> Type -> Type) -> Type) where
+  gbiFirstK :: (a -> c) -> rep (LoT2 a n) -> rep (LoT2 c n)
+
+instance (forall a c n. GFunctorPos rep 'VZ (LoT2 a n) (LoT2 c n)) => GBiFirstK rep where
+  gbiFirstK :: forall a c n. (a -> c) -> rep (LoT2 a n) -> rep (LoT2 c n)
+  gbiFirstK = gfmapp @_ @rep @'VZ @(LoT2 a n) @(LoT2 c n)
+
+class GProFirstK (rep :: LoT (Type -> Type -> Type) -> Type) where
+  gproFirstK :: (c -> a) -> rep (LoT2 a n) -> rep (LoT2 c n)
+
+instance (forall a c n. GContraPos rep 'VZ (LoT2 a n) (LoT2 c n)) => GProFirstK rep where
+  gproFirstK :: forall a c n. (c -> a) -> rep (LoT2 a n) -> rep (LoT2 c n)
+  gproFirstK = gcontrap @_ @rep @'VZ @(LoT2 a n) @(LoT2 c n)
+
+class GBiFirstInvK (rep :: LoT (Type -> Type -> Type) -> Type) where
+  gbiFirstInvK :: (a -> c) -> (c -> a) -> rep (LoT2 a n) -> rep (LoT2 c n)
+
+instance (forall a c n. GInvPos rep 'VZ (LoT2 a n) (LoT2 c n)) => GBiFirstInvK rep where
+  gbiFirstInvK :: forall a c n. (a -> c) -> (c -> a) -> rep (LoT2 a n) -> rep (LoT2 c n)
+  gbiFirstInvK = ginvp @_ @rep @'VZ @(LoT2 a n) @(LoT2 c n)
+
+type LoT3 a b c = a :&&: b :&&: c :&&: LoT0
+
+class GTriFirstK (rep :: LoT (Type -> Type -> Type -> Type) -> Type) where
+  gtriFirstK :: (a -> b) -> rep (LoT3 a x y) -> rep (LoT3 b x y)
+
+instance (forall a b x y. GFunctorPos rep 'VZ (LoT3 a x y) (LoT3 b x y)) => GTriFirstK rep where
+  gtriFirstK :: forall a b x y. (a -> b) -> rep (LoT3 a x y) -> rep (LoT3 b x y)
+  gtriFirstK = gfmapp @_ @rep @'VZ @(LoT3 a x y) @(LoT3 b x y)
+
+class GTriProFirstK (rep :: LoT (Type -> Type -> Type -> Type) -> Type) where
+  gtriProFirstK :: (b -> a) -> rep (LoT3 a x y) -> rep (LoT3 b x y)
+
+instance (forall a b x y. GContraPos rep 'VZ (LoT3 a x y) (LoT3 b x y)) => GTriProFirstK rep where
+  gtriProFirstK :: forall a b x y. (b -> a) -> rep (LoT3 a x y) -> rep (LoT3 b x y)
+  gtriProFirstK = gcontrap @_ @rep @'VZ @(LoT3 a x y) @(LoT3 b x y)
+
+class GTriInvFirstK (rep :: LoT (Type -> Type -> Type -> Type) -> Type) where
+  gtriInvFirstK :: (a -> b) -> (b -> a) -> rep (LoT3 a x y) -> rep (LoT3 b x y)
+
+instance (forall a b x y. GInvPos rep 'VZ (LoT3 a x y) (LoT3 b x y)) => GTriInvFirstK rep where
+  gtriInvFirstK :: forall a b x y. (a -> b) -> (b -> a) -> rep (LoT3 a x y) -> rep (LoT3 b x y)
+  gtriInvFirstK = ginvp @_ @rep @'VZ @(LoT3 a x y) @(LoT3 b x y)
+
+--------------------------------------------------------------------------------
+-- One dispatch class keyed on the domain and codomain categories, so the single
+-- 'map' default covers every variance and arity below.
+
+class GMapFull (dom :: from -> from -> Type) (cod :: to -> to -> Type) (f :: from -> to) where
+  gmapFull :: dom a b -> cod (f a) (f b)
+
+-- covariant, single parameter (also the last argument of a two-parameter type)
+instance
+  (GenericK f, GFunctorK (RepK f)) =>
+  GMapFull ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type) (f :: Type -> Type)
+  where
+  gmapFull :: forall a b. (a -> b) -> f a -> f b
+  gmapFull d = toK @_ @f @(LoT1 b) . gfmapK @(RepK f) d . fromK @_ @f @(LoT1 a)
+
+-- contravariant, single parameter
+instance
+  (GenericK f, GContraK (RepK f)) =>
+  GMapFull (Op :: Type -> Type -> Type) ((->) :: Type -> Type -> Type) (f :: Type -> Type)
+  where
+  gmapFull :: forall a b. Op a b -> f a -> f b
+  gmapFull (Op k) = toK @_ @f @(LoT1 b) . gcontraK @(RepK f) k . fromK @_ @f @(LoT1 a)
+
+-- invariant, single parameter
+instance
+  (GenericK f, GInvK (RepK f)) =>
+  GMapFull (Iso (->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type) (f :: Type -> Type)
+  where
+  gmapFull :: forall a b. Iso (->) a b -> f a -> f b
+  gmapFull i = toK @_ @f @(LoT1 b) . ginvK @(RepK f) (embed i) (project i) . fromK @_ @f @(LoT1 a)
+
+-- covariant in the first of two arguments, producing a Nat. The second
+-- argument's category @cat2@ is the phantom source of the Nat and does not
+-- affect the mapping, so a single instance covers every second-argument
+-- variance.
+instance
+  (GenericK f, GBiFirstK (RepK f)) =>
+  GMapFull ((->) :: Type -> Type -> Type) (cat2 ~> (->)) (f :: Type -> Type -> Type)
+  where
+  gmapFull :: forall a c. (a -> c) -> Nat cat2 (->) (f a) (f c)
+  gmapFull h = Nat go
+    where
+      go :: forall n. f a n -> f c n
+      go = toK @_ @f @(LoT2 c n) . gbiFirstK @(RepK f) h . fromK @_ @f @(LoT2 a n)
+
+-- contravariant in the first of two arguments (a profunctor when the second is
+-- covariant), producing a Nat.
+instance
+  (GenericK f, GProFirstK (RepK f)) =>
+  GMapFull (Op :: Type -> Type -> Type) (cat2 ~> (->)) (f :: Type -> Type -> Type)
+  where
+  gmapFull :: forall a c. Op a c -> Nat cat2 (->) (f a) (f c)
+  gmapFull (Op k) = Nat go
+    where
+      go :: forall n. f a n -> f c n
+      go = toK @_ @f @(LoT2 c n) . gproFirstK @(RepK f) k . fromK @_ @f @(LoT2 a n)
+
+-- invariant in the first of two arguments, producing a Nat.
+instance
+  (GenericK f, GBiFirstInvK (RepK f)) =>
+  GMapFull (Iso (->) :: Type -> Type -> Type) (cat2 ~> (->)) (f :: Type -> Type -> Type)
+  where
+  gmapFull :: forall a c. Iso (->) a c -> Nat cat2 (->) (f a) (f c)
+  gmapFull i = Nat go
+    where
+      go :: forall n. f a n -> f c n
+      go = toK @_ @f @(LoT2 c n) . gbiFirstInvK @(RepK f) (embed i) (project i) . fromK @_ @f @(LoT2 a n)
+
+-- covariant in the first of three arguments, producing a nested Nat. As with
+-- two arguments, the trailing categories are phantom sources and one instance
+-- per first-argument variance covers every combination of the other two.
+instance
+  (GenericK f, GTriFirstK (RepK f)) =>
+  GMapFull ((->) :: Type -> Type -> Type) (cat2 ~> cat3 ~> (->)) (f :: Type -> Type -> Type -> Type)
+  where
+  gmapFull :: forall a b. (a -> b) -> Nat cat2 (cat3 ~> (->)) (f a) (f b)
+  gmapFull morph = Nat middle
+    where
+      middle :: forall x. Nat cat3 (->) (f a x) (f b x)
+      middle = Nat inner
+        where
+          inner :: forall y. f a x y -> f b x y
+          inner = toK @_ @f @(LoT3 b x y) . gtriFirstK @(RepK f) morph . fromK @_ @f @(LoT3 a x y)
+
+-- contravariant in the first of three arguments.
+instance
+  (GenericK f, GTriProFirstK (RepK f)) =>
+  GMapFull (Op :: Type -> Type -> Type) (cat2 ~> cat3 ~> (->)) (f :: Type -> Type -> Type -> Type)
+  where
+  gmapFull :: forall a b. Op a b -> Nat cat2 (cat3 ~> (->)) (f a) (f b)
+  gmapFull (Op k) = Nat middle
+    where
+      middle :: forall x. Nat cat3 (->) (f a x) (f b x)
+      middle = Nat inner
+        where
+          inner :: forall y. f a x y -> f b x y
+          inner = toK @_ @f @(LoT3 b x y) . gtriProFirstK @(RepK f) k . fromK @_ @f @(LoT3 a x y)
+
+-- invariant in the first of three arguments.
+instance
+  (GenericK f, GTriInvFirstK (RepK f)) =>
+  GMapFull (Iso (->) :: Type -> Type -> Type) (cat2 ~> cat3 ~> (->)) (f :: Type -> Type -> Type -> Type)
+  where
+  gmapFull :: forall a b. Iso (->) a b -> Nat cat2 (cat3 ~> (->)) (f a) (f b)
+  gmapFull i = Nat middle
+    where
+      middle :: forall x. Nat cat3 (->) (f a x) (f b x)
+      middle = Nat inner
+        where
+          inner :: forall y. f a x y -> f b x y
+          inner = toK @_ @f @(LoT3 b x y) . gtriInvFirstK @(RepK f) (embed i) (project i) . fromK @_ @f @(LoT3 a x y)
diff --git a/src/Kindly/Functor.hs b/src/Kindly/Functor.hs
--- a/src/Kindly/Functor.hs
+++ b/src/Kindly/Functor.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP #-}
 {-# OPTIONS_GHC -Wno-orphans #-}
 
 -- | Single Parameter Functors of arbitrary categories.
@@ -5,50 +6,105 @@
   ( Functor,
     fmap,
     contramap,
+    mapIso,
     invmap,
+    Iso (..),
     Filterable,
     mapMaybe,
     catMaybes,
     filter,
+    FromFunctor (..),
+    FromContra (..),
   )
 where
 
 --------------------------------------------------------------------------------
 
 import Control.Applicative (Const, WrappedArrow, WrappedMonad, ZipList)
+import Control.Applicative.Backwards (Backwards (..))
+import Control.Applicative.Lift (Lift (..))
 import Control.Arrow (Arrow, ArrowMonad, Kleisli (..))
 import Control.Category (Category (..))
 import Control.Exception (Handler)
 import Control.Monad (Monad)
 import Control.Monad.ST (ST)
 import Control.Monad.ST.Lazy qualified as Lazy
+import Control.Monad.Trans.Accum (AccumT (..))
+import Control.Monad.Trans.Cont (ContT (..))
+import Control.Monad.Trans.Except (ExceptT (..))
+import Control.Monad.Trans.Identity (IdentityT (..))
+import Control.Monad.Trans.Maybe (MaybeT (..))
+import Control.Monad.Trans.RWS.CPS qualified as CPS
+import Control.Monad.Trans.RWS.Lazy qualified as Lazy
+import Control.Monad.Trans.RWS.Strict qualified as Strict
+import Control.Monad.Trans.Reader (ReaderT (..))
+import Control.Monad.Trans.Select (SelectT (..))
+import Control.Monad.Trans.State.Lazy qualified as Lazy
+import Control.Monad.Trans.State.Strict qualified as Strict
+import Control.Monad.Trans.Writer.CPS qualified as CPS
+import Control.Monad.Trans.Writer.Lazy qualified as Lazy
+import Control.Monad.Trans.Writer.Strict qualified as Strict
+import Data.Bifunctor.Biff (Biff (..))
+import Data.Bifunctor.Clown (Clown (..))
+import Data.Bifunctor.Fix (Fix (..))
+import Data.Bifunctor.Flip (Flip (..))
+import Data.Bifunctor.Joker (Joker (..))
+import Data.Bifunctor.Product qualified as Bifunctor
+import Data.Bifunctor.Sum qualified as Bifunctor
+import Data.Bifunctor.Tannen (Tannen (..))
+import Data.Bifunctor.Wrapped (WrappedBifunctor (..))
 import Data.Complex (Complex)
-import Data.Either (Either)
+import Data.Either (Either (..))
 import Data.Functor qualified as Hask
+import Data.Functor.Apply (MaybeApply (..), WrappedApplicative (..))
 import Data.Functor.Compose (Compose (..))
-import Data.Functor.Contravariant (Op (..), Predicate)
+import Data.Functor.Constant (Constant)
+import Data.Functor.Contravariant (Comparison, Equivalence, Op (..), Predicate)
 import Data.Functor.Contravariant qualified as Hask
 import Data.Functor.Identity (Identity (..))
 import Data.Functor.Product (Product (..))
+import Data.Functor.Reverse (Reverse (..))
 import Data.Functor.Sum (Sum (..))
+import Data.Functor.These (These1 (..))
+import Data.Graph (SCC)
+import Data.IntMap (IntMap)
+import Data.Isomorphism
 import Data.Kind (Constraint, Type)
 import Data.List.NonEmpty (NonEmpty)
+import Data.Map (Map)
 import Data.Maybe (Maybe (..))
 import Data.Monoid qualified as Monoid
 import Data.Ord (Down)
 import Data.Profunctor qualified as Hask.Profunctor
+import Data.Profunctor.Cayley qualified as Hask.Profunctor
+import Data.Profunctor.Choice qualified as Hask.Profunctor
+import Data.Profunctor.Closed qualified as Hask.Profunctor
+import Data.Profunctor.Composition qualified as Hask.Profunctor
+import Data.Profunctor.Mapping qualified as Hask.Profunctor
+import Data.Profunctor.Strong qualified as Hask.Profunctor
+import Data.Profunctor.Traversing qualified as Hask.Profunctor
+import Data.Profunctor.Yoneda qualified as Hask.Profunctor
 import Data.Proxy (Proxy)
 import Data.Semigroup qualified as Semigroup
+import Data.Semigroupoid.Dual (Dual (..))
+import Data.Semigroupoid.Static (Static (..))
+import Data.Sequence (Seq, ViewL, ViewR)
+import Data.Tagged (Tagged)
 import Data.These (These)
+import Data.Tree (Tree)
+#if MIN_VERSION_base(4,16,0)
 import Data.Tuple (Solo)
+#endif
 import Foreign (Ptr)
 import GHC.Arr (Array)
 import GHC.Base (Char, Double, IO, Int, Word, ($))
 import GHC.Conc (STM)
 import GHC.Exts (Float)
 import GHC.Generics (K1, M1 (..), Par1, Rec1 (..), U1, URec, V1, (:*:) (..), (:+:) (..), (:.:) (..))
+#if MIN_VERSION_base(4,17,0)
+import GHC.Generics (Generic1, Generically1, Rep1)
+#endif
 import Kindly.Class
-import Kindly.Iso
 import System.Console.GetOpt (ArgDescr, ArgOrder, OptDescr)
 import Text.ParserCombinators.ReadP (ReadP)
 import Text.ParserCombinators.ReadPrec (ReadPrec)
@@ -70,25 +126,36 @@
 -- in 'Data.Functor.Contravariant.'
 --
 -- TODO: Do we keep this around? This is nice to have so that library
--- users don't have to manually pack functions in 'Op'.
+-- users don't have to manually pack functions in t'Op'.
 contramap :: (Functor Op p) => (a -> b) -> p b -> p a
 contramap = fmap . Op
 
--- | A specialization of 'fmap' for invariant functors as defined
--- in 'Data.Functor.Invariant.'
+-- | Map a @('->')@ isomorphism through a 'Functor' of /any/ variance. A functor
+-- can always transport an isomorphism. 'liftIso' reflects the iso into the
+-- functor's domain category @cat@, dropping whichever leg @cat@ ignores (the
+-- backward leg for a covariant @('->')@ functor, the forward leg for a
+-- contravariant 'Op' one, neither for an invariant @'Iso' ('->')@ one).
 --
--- TODO: Do we keep this around? This is nice to have so that library
--- users don't have to manually pack functions in 'Iso'.
-invmap :: (Functor (<->) f) => (a -> b) -> (b -> a) -> f a -> f b
-invmap f g = fmap (Iso f g)
+-- 'mapIso' generalizes 'invmap'. @'invmap' f g = 'mapIso' ('Iso' f g)@.
+mapIso :: (Functor cat f, LiftIso cat) => Iso (->) a b -> f a -> f b
+mapIso i = fmap (liftIso i)
 
+-- | Map an isomorphism through a 'Functor' of /any/ variance, generalizing the
+-- invariant-only version. The two legs are packed into an @'Iso' ('->')@ and
+-- mapped with 'mapIso', so 'invmap' now resolves for covariant and
+-- contravariant functors too, not just invariant ones. The domain category is
+-- fixed by the functor argument, so existing invariant call sites are
+-- unaffected.
+invmap :: (Functor cat f, LiftIso cat) => (a -> b) -> (b -> a) -> f a -> f b
+invmap f g = mapIso (Iso f g)
+
 -- TODO: 'Filterable' is currently unusable due to fundeps. This can
 -- be fixed by making it @FunctorOf (Hask.Star Maybe) (->) p@, but I
 -- think we can do better by switching away from associated types.
 type Filterable p = Functor (Hask.Profunctor.Star Maybe) p
 
 -- | A specialization of 'fmap' for filterable functors as defined
--- in 'Witherable'
+-- in "Witherable"
 --
 -- TODO: Do we keep this around? This is nice to have so that library
 -- users don't have to manually pack functions in 'Hask.Star'.
@@ -113,6 +180,10 @@
 
 --------------------------------------------------------------------------------
 
+-- | A @DerivingVia@ adapter: give any base @Functor@ a covariant
+-- 'CategoricalFunctor' instance (@Dom = (->)@, @Cod = (->)@).
+--
+-- > deriving via (FromFunctor MyType) instance CategoricalFunctor MyType
 newtype FromFunctor f a = FromFunctor (f a)
   deriving newtype (Hask.Functor)
 
@@ -174,7 +245,9 @@
 
 deriving via (FromFunctor Maybe) instance CategoricalFunctor Maybe
 
+#if MIN_VERSION_base(4,16,0)
 deriving via (FromFunctor Solo) instance CategoricalFunctor Solo
+#endif
 
 deriving via (FromFunctor []) instance CategoricalFunctor []
 
@@ -302,137 +375,338 @@
 
 deriving via (FromFunctor ((,,,,,,) a b c d e f)) instance CategoricalFunctor ((,,,,,,) a b c d e f)
 
---------------------------------------------------------------------------------
--- Covariant MapArg1 instances
+#if MIN_VERSION_base(4,17,0)
+deriving via (FromFunctor (Generically1 (f :: Type -> Type))) instance (Generic1 f, Hask.Functor (Rep1 f)) => CategoricalFunctor (Generically1 f)
+#endif
 
-instance MapArg1 (->) ZipList
+instance (FunctorOf (->) (->) m) => CategoricalFunctor (IdentityT m) where
+  type Dom (IdentityT m) = (->)
+  type Cod (IdentityT m) = (->)
 
-instance MapArg1 (->) Handler
+  map f (IdentityT m) = IdentityT $ map f m
 
-instance MapArg1 (->) Complex
+instance (FunctorOf (->) (->) m) => CategoricalFunctor (MaybeT m) where
+  type Dom (MaybeT m) = (->)
+  type Cod (MaybeT m) = (->)
 
-instance MapArg1 (->) Identity
+  map f (MaybeT m) = MaybeT $ map (map f) m
 
-instance MapArg1 (->) Monoid.First
+instance (FunctorOf (->) (->) m) => CategoricalFunctor (ExceptT e m) where
+  type Dom (ExceptT e m) = (->)
+  type Cod (ExceptT e m) = (->)
 
-instance MapArg1 (->) Monoid.Last
+  map f (ExceptT m) = ExceptT $ map (map f) m
 
-instance MapArg1 (->) Down
+instance (FunctorOf (->) (->) m) => CategoricalFunctor (ReaderT r m) where
+  type Dom (ReaderT r m) = (->)
+  type Cod (ReaderT r m) = (->)
 
-instance MapArg1 (->) Semigroup.First
+  map f (ReaderT g) = ReaderT $ \r -> map f (g r)
 
-instance MapArg1 (->) Semigroup.Last
+instance (FunctorOf (->) (->) m) => CategoricalFunctor (Lazy.StateT s m) where
+  type Dom (Lazy.StateT s m) = (->)
+  type Cod (Lazy.StateT s m) = (->)
 
-instance MapArg1 (->) Semigroup.Max
+  map f (Lazy.StateT g) = Lazy.StateT $ \s -> map (\(a, s') -> (f a, s')) (g s)
 
-instance MapArg1 (->) Semigroup.Min
+instance (FunctorOf (->) (->) m) => CategoricalFunctor (Strict.StateT s m) where
+  type Dom (Strict.StateT s m) = (->)
+  type Cod (Strict.StateT s m) = (->)
 
-instance MapArg1 (->) Semigroup.Dual
+  map f (Strict.StateT g) = Strict.StateT $ \s -> map (\(a, s') -> (f a, s')) (g s)
 
-instance MapArg1 (->) Semigroup.Product
+instance (FunctorOf (->) (->) m) => CategoricalFunctor (Lazy.WriterT w m) where
+  type Dom (Lazy.WriterT w m) = (->)
+  type Cod (Lazy.WriterT w m) = (->)
 
-instance MapArg1 (->) Semigroup.Sum
+  map f (Lazy.WriterT m) = Lazy.WriterT $ map (\(a, w) -> (f a, w)) m
 
-instance MapArg1 (->) NonEmpty
+instance (FunctorOf (->) (->) m) => CategoricalFunctor (Strict.WriterT w m) where
+  type Dom (Strict.WriterT w m) = (->)
+  type Cod (Strict.WriterT w m) = (->)
 
-instance MapArg1 (->) STM
+  map f (Strict.WriterT m) = Strict.WriterT $ map (\(a, w) -> (f a, w)) m
 
-instance MapArg1 (->) Par1
+deriving via (FromFunctor (CPS.WriterT w m)) instance (Hask.Functor m) => CategoricalFunctor (CPS.WriterT w m)
 
-instance MapArg1 (->) ArgDescr
+instance CategoricalFunctor (ContT r m) where
+  type Dom (ContT r m) = (->)
+  type Cod (ContT r m) = (->)
 
-instance MapArg1 (->) ArgOrder
+  map f (ContT g) = ContT $ \k -> g (k . f)
 
-instance MapArg1 (->) OptDescr
+instance (FunctorOf (->) (->) m) => CategoricalFunctor (Lazy.RWST r w s m) where
+  type Dom (Lazy.RWST r w s m) = (->)
+  type Cod (Lazy.RWST r w s m) = (->)
 
-instance MapArg1 (->) ReadP
+  map f (Lazy.RWST g) = Lazy.RWST $ \r s -> map (\(a, s', w) -> (f a, s', w)) (g r s)
 
-instance MapArg1 (->) ReadPrec
+instance (FunctorOf (->) (->) m) => CategoricalFunctor (Strict.RWST r w s m) where
+  type Dom (Strict.RWST r w s m) = (->)
+  type Cod (Strict.RWST r w s m) = (->)
 
-instance MapArg1 (->) IO
+  map f (Strict.RWST g) = Strict.RWST $ \r s -> map (\(a, s', w) -> (f a, s', w)) (g r s)
 
-instance MapArg1 (->) Maybe
+deriving via (FromFunctor (CPS.RWST r w s m)) instance (Hask.Functor m) => CategoricalFunctor (CPS.RWST r w s m)
 
-instance MapArg1 (->) Solo
+instance (FunctorOf (->) (->) m) => CategoricalFunctor (AccumT w m) where
+  type Dom (AccumT w m) = (->)
+  type Cod (AccumT w m) = (->)
 
-instance MapArg1 (->) []
+  map f (AccumT g) = AccumT $ \w -> map (\(a, w') -> (f a, w')) (g w)
 
-instance (Monad m) => MapArg1 (->) (WrappedMonad m)
+instance (FunctorOf (->) (->) m) => CategoricalFunctor (SelectT r m) where
+  type Dom (SelectT r m) = (->)
+  type Cod (SelectT r m) = (->)
 
-instance (Arrow a) => MapArg1 (->) (ArrowMonad a)
+  map f (SelectT g) = SelectT $ \k -> map f (g (k . f))
 
-instance MapArg1 (->) (Lazy.ST s)
+instance (FunctorOf (->) (->) f) => CategoricalFunctor (Backwards f) where
+  type Dom (Backwards f) = (->)
+  type Cod (Backwards f) = (->)
 
-instance MapArg1 (->) (Either a)
+  map f (Backwards m) = Backwards $ map f m
 
-instance MapArg1 (->) (Proxy :: Type -> Type)
+instance (FunctorOf (->) (->) f) => CategoricalFunctor (Reverse f) where
+  type Dom (Reverse f) = (->)
+  type Cod (Reverse f) = (->)
 
-instance MapArg1 (->) (Semigroup.Arg a)
+  map f (Reverse m) = Reverse $ map f m
 
-instance MapArg1 (->) (Array i)
+deriving via (FromFunctor (Constant a)) instance CategoricalFunctor (Constant a :: Type -> Type)
 
-instance MapArg1 (->) (U1 :: Type -> Type)
+instance (FunctorOf (->) (->) f) => CategoricalFunctor (Lift f) where
+  type Dom (Lift f) = (->)
+  type Cod (Lift f) = (->)
 
-instance MapArg1 (->) (V1 :: Type -> Type)
+  map f (Pure a) = Pure $ f a
+  map f (Other m) = Other $ map f m
 
-instance MapArg1 (->) (ST s)
+instance (FunctorOf (->) (->) f) => CategoricalFunctor (Hask.Profunctor.Star f a) where
+  type Dom (Hask.Profunctor.Star f a) = (->)
+  type Cod (Hask.Profunctor.Star f a) = (->)
 
-instance MapArg1 (->) ((,) a)
+  map f (Hask.Profunctor.Star g) = Hask.Profunctor.Star $ \x -> map f (g x)
 
-instance (Arrow a) => MapArg1 (->) (WrappedArrow a b)
+deriving via (FromFunctor (Hask.Profunctor.Costar f a)) instance CategoricalFunctor (Hask.Profunctor.Costar f a)
 
-instance (FunctorOf (->) (->) m) => MapArg1 (->) (Kleisli m a)
+deriving via (FromFunctor (Hask.Profunctor.Forget r a)) instance CategoricalFunctor (Hask.Profunctor.Forget r a :: Type -> Type)
 
-instance MapArg1 (->) (Const m :: Type -> Type)
+instance (FunctorOf (->) (->) f) => CategoricalFunctor (WrappedApplicative f) where
+  type Dom (WrappedApplicative f) = (->)
+  type Cod (WrappedApplicative f) = (->)
 
-instance (FunctorOf (->) (->) f) => MapArg1 (->) (Monoid.Ap f)
+  map f (WrapApplicative m) = WrapApplicative $ map f m
 
-instance (FunctorOf (->) (->) f) => MapArg1 (->) (Monoid.Alt f)
+instance (FunctorOf (->) (->) f) => CategoricalFunctor (MaybeApply f) where
+  type Dom (MaybeApply f) = (->)
+  type Cod (MaybeApply f) = (->)
 
-instance (FunctorOf (->) (->) f) => MapArg1 (->) (Rec1 f)
+  map f (MaybeApply (Left fa)) = MaybeApply $ Left $ map f fa
+  map f (MaybeApply (Right a)) = MaybeApply $ Right $ f a
 
-instance MapArg1 (->) (URec (Ptr ()) :: Type -> Type)
+instance (FunctorOf (->) (->) f) => CategoricalFunctor (Static f a) where
+  type Dom (Static f a) = (->)
+  type Cod (Static f a) = (->)
 
-instance MapArg1 (->) (URec Char :: Type -> Type)
+  map f (Static g) = Static $ map (f .) g
 
-instance MapArg1 (->) (URec Double :: Type -> Type)
+instance (FunctorOf (->) (->) f, FunctorOf (->) (->) g) => CategoricalFunctor (These1 f g) where
+  type Dom (These1 f g) = (->)
+  type Cod (These1 f g) = (->)
 
-instance MapArg1 (->) (URec Float :: Type -> Type)
+  map f (This1 fa) = This1 $ map f fa
+  map f (That1 ga) = That1 $ map f ga
+  map f (These1 fa ga) = These1 (map f fa) (map f ga)
 
-instance MapArg1 (->) (URec Int :: Type -> Type)
+instance (MapArg2 (->) (->) p) => CategoricalFunctor (Flip p a) where
+  type Dom (Flip p a) = (->)
+  type Cod (Flip p a) = (->)
 
-instance MapArg1 (->) (URec Word :: Type -> Type)
+  map f (Flip pba) = Flip $ map2 f pba
 
-instance MapArg1 (->) ((,,) a b)
+deriving via (FromFunctor (Clown f a)) instance CategoricalFunctor (Clown f a :: Type -> Type)
 
-instance (FunctorOf (->) (->) f, FunctorOf (->) (->) g) => MapArg1 (->) (Product f g)
+instance (FunctorOf (->) (->) g) => CategoricalFunctor (Joker g a) where
+  type Dom (Joker g a) = (->)
+  type Cod (Joker g a) = (->)
 
-instance (FunctorOf (->) (->) f, FunctorOf (->) (->) g) => MapArg1 (->) (Sum f g)
+  map f (Joker gb) = Joker $ map f gb
 
-instance (FunctorOf (->) (->) f, FunctorOf (->) (->) g) => MapArg1 (->) (f :*: g)
+instance (FunctorOf (->) (->) (p a), FunctorOf (->) (->) (q a)) => CategoricalFunctor (Bifunctor.Product p q a) where
+  type Dom (Bifunctor.Product p q a) = (->)
+  type Cod (Bifunctor.Product p q a) = (->)
 
-instance (FunctorOf (->) (->) f, FunctorOf (->) (->) g) => MapArg1 (->) (f :+: g)
+  map f (Bifunctor.Pair pab qab) = Bifunctor.Pair (map f pab) (map f qab)
 
-instance MapArg1 (->) (K1 i c :: Type -> Type)
+instance (FunctorOf (->) (->) (p a), FunctorOf (->) (->) (q a)) => CategoricalFunctor (Bifunctor.Sum p q a) where
+  type Dom (Bifunctor.Sum p q a) = (->)
+  type Cod (Bifunctor.Sum p q a) = (->)
 
-instance MapArg1 (->) ((,,,) a b c)
+  map f (Bifunctor.L2 pab) = Bifunctor.L2 $ map f pab
+  map f (Bifunctor.R2 qab) = Bifunctor.R2 $ map f qab
 
-instance MapArg1 (->) ((->) r)
+instance (FunctorOf (->) (->) f, FunctorOf (->) (->) (p a)) => CategoricalFunctor (Tannen f p a) where
+  type Dom (Tannen f p a) = (->)
+  type Cod (Tannen f p a) = (->)
 
-instance (FunctorOf (->) (->) f, FunctorOf (->) (->) g) => MapArg1 (->) (Compose f g)
+  map g (Tannen fp) = Tannen $ map (map g) fp
 
-instance (FunctorOf (->) (->) f, FunctorOf (->) (->) g) => MapArg1 (->) (f :.: g)
+instance (FunctorOf (->) (->) (p (f a)), FunctorOf (->) (->) g) => CategoricalFunctor (Biff p f g a) where
+  type Dom (Biff p f g a) = (->)
+  type Cod (Biff p f g a) = (->)
 
-instance (FunctorOf (->) (->) f) => MapArg1 (->) (M1 i c f)
+  map h (Biff pfg) = Biff $ map (map h) pfg
 
-instance MapArg1 (->) ((,,,,) a b c d)
+instance (FunctorOf (->) (->) (p a)) => CategoricalFunctor (WrappedBifunctor p a) where
+  type Dom (WrappedBifunctor p a) = (->)
+  type Cod (WrappedBifunctor p a) = (->)
 
-instance MapArg1 (->) ((,,,,,) a b c d e)
+  map f (WrapBifunctor pab) = WrapBifunctor $ map f pab
 
-instance MapArg1 (->) ((,,,,,,) a b c d e f)
+instance (forall x. MapArg1 (->) (p x)) => CategoricalFunctor (Hask.Profunctor.Procompose p q a) where
+  type Dom (Hask.Profunctor.Procompose p q a) = (->)
+  type Cod (Hask.Profunctor.Procompose p q a) = (->)
 
+  map f (Hask.Profunctor.Procompose pxc qdx) = Hask.Profunctor.Procompose (map1 f pxc) qdx
+
+instance (MapArg2 Op (->) p) => CategoricalFunctor (Hask.Profunctor.Rift p q a) where
+  type Dom (Hask.Profunctor.Rift p q a) = (->)
+  type Cod (Hask.Profunctor.Rift p q a) = (->)
+
+  map f (Hask.Profunctor.Rift g) = Hask.Profunctor.Rift $ \p -> g (map2 (Op f) p)
+
+instance CategoricalFunctor (Hask.Profunctor.Yoneda p a) where
+  type Dom (Hask.Profunctor.Yoneda p a) = (->)
+  type Cod (Hask.Profunctor.Yoneda p a) = (->)
+
+  map f (Hask.Profunctor.Yoneda g) = Hask.Profunctor.Yoneda $ \l r -> g l (r . f)
+
+instance CategoricalFunctor (Hask.Profunctor.Coyoneda p a) where
+  type Dom (Hask.Profunctor.Coyoneda p a) = (->)
+  type Cod (Hask.Profunctor.Coyoneda p a) = (->)
+
+  map f (Hask.Profunctor.Coyoneda l r p) = Hask.Profunctor.Coyoneda l (f . r) p
+
+instance (FunctorOf (->) (->) f, FunctorOf (->) (->) (p a)) => CategoricalFunctor (Hask.Profunctor.Cayley f p a) where
+  type Dom (Hask.Profunctor.Cayley f p a) = (->)
+  type Cod (Hask.Profunctor.Cayley f p a) = (->)
+
+  map g (Hask.Profunctor.Cayley fp) = Hask.Profunctor.Cayley $ map (map g) fp
+
+instance (forall x. MapArg1 (->) (p x)) => CategoricalFunctor (Hask.Profunctor.Tambara p a) where
+  type Dom (Hask.Profunctor.Tambara p a) = (->)
+  type Cod (Hask.Profunctor.Tambara p a) = (->)
+
+  map f (Hask.Profunctor.Tambara t) = Hask.Profunctor.Tambara $ map1 (\(b, c) -> (f b, c)) t
+
+instance CategoricalFunctor (Hask.Profunctor.Pastro p a) where
+  type Dom (Hask.Profunctor.Pastro p a) = (->)
+  type Cod (Hask.Profunctor.Pastro p a) = (->)
+
+  map f (Hask.Profunctor.Pastro l m r) = Hask.Profunctor.Pastro (f . l) m r
+
+instance CategoricalFunctor (Hask.Profunctor.Cotambara q a) where
+  type Dom (Hask.Profunctor.Cotambara q a) = (->)
+  type Cod (Hask.Profunctor.Cotambara q a) = (->)
+
+  map f (Hask.Profunctor.Cotambara n r) = Hask.Profunctor.Cotambara n (Hask.Profunctor.rmap f r)
+
+instance CategoricalFunctor (Hask.Profunctor.Copastro p a) where
+  type Dom (Hask.Profunctor.Copastro p a) = (->)
+  type Cod (Hask.Profunctor.Copastro p a) = (->)
+
+  map f (Hask.Profunctor.Copastro g) = Hask.Profunctor.Copastro $ \n -> Hask.Profunctor.rmap f (g n)
+
+instance (forall x. MapArg1 (->) (p x)) => CategoricalFunctor (Hask.Profunctor.TambaraSum p a) where
+  type Dom (Hask.Profunctor.TambaraSum p a) = (->)
+  type Cod (Hask.Profunctor.TambaraSum p a) = (->)
+
+  map f (Hask.Profunctor.TambaraSum t) =
+    Hask.Profunctor.TambaraSum $ map1 (\case Left b -> Left (f b); Right c -> Right c) t
+
+instance CategoricalFunctor (Hask.Profunctor.PastroSum p a) where
+  type Dom (Hask.Profunctor.PastroSum p a) = (->)
+  type Cod (Hask.Profunctor.PastroSum p a) = (->)
+
+  map f (Hask.Profunctor.PastroSum l m r) = Hask.Profunctor.PastroSum (f . l) m r
+
+instance CategoricalFunctor (Hask.Profunctor.CotambaraSum q a) where
+  type Dom (Hask.Profunctor.CotambaraSum q a) = (->)
+  type Cod (Hask.Profunctor.CotambaraSum q a) = (->)
+
+  map f (Hask.Profunctor.CotambaraSum n r) = Hask.Profunctor.CotambaraSum n (Hask.Profunctor.rmap f r)
+
+instance CategoricalFunctor (Hask.Profunctor.CopastroSum p a) where
+  type Dom (Hask.Profunctor.CopastroSum p a) = (->)
+  type Cod (Hask.Profunctor.CopastroSum p a) = (->)
+
+  map f (Hask.Profunctor.CopastroSum g) = Hask.Profunctor.CopastroSum $ \n -> Hask.Profunctor.rmap f (g n)
+
+instance (forall x. MapArg1 (->) (p x)) => CategoricalFunctor (Hask.Profunctor.Closure p a) where
+  type Dom (Hask.Profunctor.Closure p a) = (->)
+  type Cod (Hask.Profunctor.Closure p a) = (->)
+
+  map f (Hask.Profunctor.Closure t) = Hask.Profunctor.Closure $ map1 (f .) t
+
+instance CategoricalFunctor (Hask.Profunctor.Environment p a) where
+  type Dom (Hask.Profunctor.Environment p a) = (->)
+  type Cod (Hask.Profunctor.Environment p a) = (->)
+
+  map f (Hask.Profunctor.Environment l m r) = Hask.Profunctor.Environment (f . l) m r
+
+instance CategoricalFunctor (Hask.Profunctor.FreeTraversing p a) where
+  type Dom (Hask.Profunctor.FreeTraversing p a) = (->)
+  type Cod (Hask.Profunctor.FreeTraversing p a) = (->)
+
+  map f (Hask.Profunctor.FreeTraversing l m r) = Hask.Profunctor.FreeTraversing (f . l) m r
+
+instance (forall x. MapArg1 (->) (p x)) => CategoricalFunctor (Hask.Profunctor.CofreeTraversing p a) where
+  type Dom (Hask.Profunctor.CofreeTraversing p a) = (->)
+  type Cod (Hask.Profunctor.CofreeTraversing p a) = (->)
+
+  map f (Hask.Profunctor.CofreeTraversing t) = Hask.Profunctor.CofreeTraversing $ map1 (Hask.fmap f) t
+
+instance CategoricalFunctor (Hask.Profunctor.FreeMapping p a) where
+  type Dom (Hask.Profunctor.FreeMapping p a) = (->)
+  type Cod (Hask.Profunctor.FreeMapping p a) = (->)
+
+  map f (Hask.Profunctor.FreeMapping l m r) = Hask.Profunctor.FreeMapping (f . l) m r
+
+instance (forall x. MapArg1 (->) (p x)) => CategoricalFunctor (Hask.Profunctor.CofreeMapping p a) where
+  type Dom (Hask.Profunctor.CofreeMapping p a) = (->)
+  type Cod (Hask.Profunctor.CofreeMapping p a) = (->)
+
+  map f (Hask.Profunctor.CofreeMapping t) = Hask.Profunctor.CofreeMapping $ map1 (Hask.fmap f) t
+
+deriving via (FromFunctor (Tagged s)) instance CategoricalFunctor (Tagged s)
+
+instance (MapArg2 (->) (->) p) => CategoricalFunctor (Fix p) where
+  type Dom (Fix p) = (->)
+  type Cod (Fix p) = (->)
+
+  map f (In p) = In (map2 (map f) (map1 f p))
+
+deriving via (FromFunctor (Map k)) instance CategoricalFunctor (Map k)
+
+deriving via (FromFunctor IntMap) instance CategoricalFunctor IntMap
+
+deriving via (FromFunctor Seq) instance CategoricalFunctor Seq
+
+deriving via (FromFunctor ViewL) instance CategoricalFunctor ViewL
+
+deriving via (FromFunctor ViewR) instance CategoricalFunctor ViewR
+
+deriving via (FromFunctor Tree) instance CategoricalFunctor Tree
+
+deriving via (FromFunctor SCC) instance CategoricalFunctor SCC
+
 --------------------------------------------------------------------------------
 
+-- | A @DerivingVia@ adapter: give any base @Contravariant@ a contravariant
+-- 'CategoricalFunctor' instance (@Dom = Op@).
+--
+-- > deriving via (FromContra MyType) instance CategoricalFunctor MyType
 newtype FromContra f a = FromContra (f a)
   deriving newtype (Hask.Contravariant)
 
@@ -448,25 +722,26 @@
 
 deriving via (FromContra Predicate) instance CategoricalFunctor Predicate
 
--- TODO: Add remaining Contravariant instances
+deriving via (FromContra Comparison) instance CategoricalFunctor Comparison
 
---------------------------------------------------------------------------------
--- Contravariant MapArg1 instances
+deriving via (FromContra Equivalence) instance CategoricalFunctor Equivalence
 
-instance MapArg1 Op Predicate
+deriving via (FromContra (Op a)) instance CategoricalFunctor (Op a)
 
--- TODO: Add remaining Contravariant instances
+instance (MapArg2 Op (->) k) => CategoricalFunctor (Dual k a) where
+  type Dom (Dual k a) = Op
+  type Cod (Dual k a) = (->)
 
+  map (Op f) (Dual kba) = Dual (map2 (Op f) kba)
+
 --------------------------------------------------------------------------------
 
 instance CategoricalFunctor Monoid.Endo where
-  type Dom Monoid.Endo = (<->)
+  type Dom Monoid.Endo = Iso (->)
   type Cod Monoid.Endo = (->)
 
-  map :: (a <-> b) -> Monoid.Endo a -> Monoid.Endo b
-  map Iso {..} (Monoid.Endo f) = Monoid.Endo (fwd . f . bwd)
-
-instance MapArg1 (<->) Monoid.Endo
+  map :: Iso (->) a b -> Monoid.Endo a -> Monoid.Endo b
+  map Iso {..} (Monoid.Endo f) = Monoid.Endo (embed . f . project)
 
 --------------------------------------------------------------------------------
 
diff --git a/src/Kindly/Iso.hs b/src/Kindly/Iso.hs
deleted file mode 100644
--- a/src/Kindly/Iso.hs
+++ /dev/null
@@ -1,29 +0,0 @@
-module Kindly.Iso where
-
---------------------------------------------------------------------------------
-
-import Control.Category (Category (..))
-import Data.Kind (Type)
-import Kindly.Class (Cat)
-
---------------------------------------------------------------------------------
-
--- | An invertible mapping between 'a' and 'b' in category 'cat'.
---
--- === Laws
---
--- @
--- 'fwd' '.' 'bwd' ≡ 'id'
--- 'bwd' '.' 'fwd' ≡ 'id'
--- @
-data Iso cat a b = Iso {fwd :: a `cat` b, bwd :: b `cat` a}
-
-instance (Category cat) => Category (Iso cat) where
-  id :: (Category cat) => Iso cat a a
-  id = Iso id id
-
-  (.) :: Iso cat b c -> Iso cat a b -> Iso cat a c
-  Iso fwd bwd . Iso fwd' bwd' = Iso (fwd . fwd') (bwd' . bwd)
-
-type (<->) :: Cat Type
-type (<->) = Iso (->)
diff --git a/src/Kindly/Rank2.hs b/src/Kindly/Rank2.hs
--- a/src/Kindly/Rank2.hs
+++ b/src/Kindly/Rank2.hs
@@ -1,25 +1,140 @@
--- | Work in Progress.
+-- | Rank-2 functors: 'CategoricalFunctor's whose parameters are themselves
+-- functors. A type with @N@ functor parameters is an @N@-ary functor between
+-- functor categories, and 'bmap1' \/ 'bmap2' \/ 'bmap3' select which parameter
+-- to map.
+--
+-- The selectors count parameters __from the right__, matching the core
+-- 'Kindly.Class.map1' \/ 'Kindly.Class.map2' \/ 'Kindly.Class.map3'. On
+-- @b f g h@, 'bmap1' maps @h@, 'bmap2' maps @g@, and 'bmap3' maps @f@.
 module Kindly.Rank2
-  ( BFunctor,
-    bmap,
-    BFunctor2,
+  ( -- * Covariant aliases
+    FunctorB,
+    BifunctorB,
+    TrifunctorB,
+
+    -- * Selectors
+    bmap1,
     bmap2,
+    bmap3,
+
+    -- * Contravariant wrappers
+    bcontramap1,
+    bcontramap2,
+    bcontramap3,
+
+    -- * Invariant wrappers
+    binvmap1,
+    binvmap2,
+    binvmap3,
   )
 where
 
 --------------------------------------------------------------------------------
 
+import Data.Functor.Contravariant (Op (..))
+import Data.Isomorphism (Iso (..))
 import Kindly.Class
 
 --------------------------------------------------------------------------------
+-- Covariant aliases
 
-type BFunctor b = FunctorOf ((->) ~> (->)) (->) b
+-- | A rank-2 type covariant in its single functor parameter.
+type FunctorB b = MapArg1 ((->) ~> (->)) b
 
-bmap :: BFunctor b => forall f g. (forall x. f x -> g x) -> b f -> b g 
-bmap nat = map (Nat nat)
+-- | A rank-2 type covariant in both functor parameters.
+type BifunctorB b = MapArg2 ((->) ~> (->)) ((->) ~> (->)) b
 
-type BFunctor2 b = FunctorOf ((->) ~> (->) ~> (->)) (->) b
+-- | A rank-2 type covariant in all three functor parameters.
+type TrifunctorB b = MapArg3 ((->) ~> (->)) ((->) ~> (->)) ((->) ~> (->)) b
 
-bmap2 :: BFunctor2 b => forall f g. (forall x x'. f x x' -> g x x') -> b f -> b g 
-bmap2 nat = map (Nat (Nat nat))
+--------------------------------------------------------------------------------
+-- Selectors
 
+-- | Map the rightmost functor parameter of a rank-2 type.
+--
+-- For a one-parameter HKD:
+--
+-- > data Schema f = Schema (f Int) (f Bool)
+-- >
+-- > instance CategoricalFunctor Schema where
+-- >   type Dom Schema = (->) ~> (->)
+-- >   type Cod Schema = (->)
+-- >   map (Nat nat) (Schema a b) = Schema (nat a) (nat b)
+-- >
+-- > -- turn every field's @Maybe@ into a list
+-- > bmap1 maybeToList :: Schema Maybe -> Schema []
+bmap1 :: (MapArg1 (c ~> d) b) => (forall x. d (f x) (g x)) -> b f -> b g
+bmap1 n = map1 (Nat n)
+
+-- | Map the second-from-right functor parameter of a rank-2 type.
+--
+-- On a two-parameter HKD @b f g@, 'bmap1' maps @g@ (rightmost) and 'bmap2' maps
+-- @f@. Map both by nesting: @bmap2 n1 (bmap1 n2 x)@.
+bmap2 :: (MapArg2 (c ~> d) e b) => (forall x. d (f x) (g x)) -> b f h -> b g h
+bmap2 n = map2 (Nat n)
+
+-- | Map the third-from-right functor parameter of a rank-2 type.
+bmap3 :: (MapArg3 (c ~> d) e e' b) => (forall x. d (f x) (g x)) -> b f h i -> b g h i
+bmap3 n = map3 (Nat n)
+
+--------------------------------------------------------------------------------
+-- Contravariant wrappers
+
+-- | Map the rightmost parameter of a type contravariant in it.
+bcontramap1 :: (MapArg1 (c ~> Op) b) => (forall x. g x -> f x) -> b f -> b g
+bcontramap1 n = bmap1 (Op n)
+
+-- | Map the second-from-right parameter of a type contravariant in it.
+bcontramap2 :: (MapArg2 (c ~> Op) e b) => (forall x. g x -> f x) -> b f h -> b g h
+bcontramap2 n = bmap2 (Op n)
+
+-- | Map the third-from-right parameter of a type contravariant in it.
+bcontramap3 :: (MapArg3 (c ~> Op) e e' b) => (forall x. g x -> f x) -> b f h i -> b g h i
+bcontramap3 n = bmap3 (Op n)
+
+--------------------------------------------------------------------------------
+-- Invariant wrappers
+
+-- | Map the rightmost parameter of a type invariant in it, supplying both legs.
+binvmap1 :: (MapArg1 (c ~> Iso (->)) b) => (forall x. f x -> g x) -> (forall x. g x -> f x) -> b f -> b g
+binvmap1 fwd bwd = bmap1 (Iso fwd bwd)
+
+-- | Map the second-from-right parameter of a type invariant in it.
+binvmap2 :: (MapArg2 (c ~> Iso (->)) e b) => (forall x. f x -> g x) -> (forall x. g x -> f x) -> b f h -> b g h
+binvmap2 fwd bwd = bmap2 (Iso fwd bwd)
+
+-- | Map the third-from-right parameter of a type invariant in it.
+binvmap3 :: (MapArg3 (c ~> Iso (->)) e e' b) => (forall x. f x -> g x) -> (forall x. g x -> f x) -> b f h i -> b g h i
+binvmap3 fwd bwd = bmap3 (Iso fwd bwd)
+
+--------------------------------------------------------------------------------
+-- Mapping several parameters at once
+--
+-- Map several parameters of a concrete rank-2 value by nesting selectors, which
+-- type-checks because the type is known:
+--
+-- > bmap2 n1 (bmap1 n2 x)
+--
+-- There is no polymorphic @bbimap@ \/ @btrimap@ combinator. Every formulation
+-- attempted failed:
+--
+--   * Nesting the selectors inside a polymorphic signature forces GHC to compute
+--     @Dom (b f)@ (a stuck type family) through the @MapArgN@ fundep, and it will
+--     not use the quantified constraint's superclass to unstick it. This is the
+--     GHC < 9.4 quantified-constraint limitation, and it reproduces on 9.10.
+--   * Composing raw @map1@ \/ @map2@ point-free is ambiguous (higher-order
+--     unification of the intermediate); eta-expanded it hits the same stuck @Dom@.
+--   * Routing through @Kindly.Bifunctor.bimap@ would work (a rank-2 HKD is a
+--     bifunctor between functor categories) but its @Bifunctor@ alias pins the
+--     kinds to @Type -> Type -> Type@; a poly-kinded quantified-constraint synonym
+--     is rejected, and the point-free body goes ambiguous at poly-kind anyway.
+--
+-- Nesting already covers this, so the combinator is omitted.
+--
+-- bbimap ::
+--   (MapArg2 (c ~> d) (c' ~> d') b, forall x. MapArg1 (c' ~> d') (b x)) =>
+--   (forall x. d (f x) (g x)) ->
+--   (forall x. d' (h x) (i x)) ->
+--   b f h ->
+--   b g i
+-- bbimap n1 n2 x = bmap2 n1 (bmap1 n2 x)  -- does not compile: stuck Dom (b f)
diff --git a/src/Kindly/Trifunctor.hs b/src/Kindly/Trifunctor.hs
--- a/src/Kindly/Trifunctor.hs
+++ b/src/Kindly/Trifunctor.hs
@@ -5,13 +5,19 @@
 module Kindly.Trifunctor
   ( Trifunctor,
     trimap,
+    trimapIso,
+    Iso (..),
   )
 where
 
 --------------------------------------------------------------------------------
 
 import Control.Category
+import Data.Functor.Contravariant (Op)
+import Data.Isomorphism (Iso (..))
 import Data.Kind (Constraint, Type)
+import Data.Profunctor (Forget (..))
+import GHC.Generics (K1 (..))
 import Kindly.Bifunctor ()
 import Kindly.Class
 
@@ -26,6 +32,24 @@
 trimap :: forall cat1 cat2 cat3 p. (Trifunctor cat1 cat2 cat3 p) => forall a b c a' b' c'. (a `cat3` a') -> (b `cat2` b') -> (c `cat1` c') -> p a b c -> p a' b' c'
 trimap f g h = map3 f . map2 @_ @cat1 g . map1 h
 
+-- | Map a @('->')@ isomorphism through each position of a 'Trifunctor',
+-- regardless of that position's variance. A trifunctor can always transport an
+-- isomorphism in any argument, so 'liftIso' reflects each iso into that
+-- position's category and drops whichever leg the category ignores. The isos
+-- map the type arguments left-to-right: the first maps the first argument, the
+-- second the second, the third the third.
+--
+-- 'trimapIso' is to 'trimap' what 'Kindly.Functor.mapIso' is to
+-- 'Kindly.Functor.fmap'.
+trimapIso ::
+  (Trifunctor cat1 cat2 cat3 p, LiftIso cat1, LiftIso cat2, LiftIso cat3) =>
+  Iso (->) a a' ->
+  Iso (->) b b' ->
+  Iso (->) c c' ->
+  p a b c ->
+  p a' b' c'
+trimapIso i j k = trimap (liftIso i) (liftIso j) (liftIso k)
+
 --------------------------------------------------------------------------------
 
 instance CategoricalFunctor (,,) where
@@ -56,21 +80,21 @@
   map :: (a -> b) -> ((->) ~> (->) ~> (->)) ((,,,,,) x x' x'' a) ((,,,,,) x x' x'' b)
   map f' = Nat (Nat (\(a, b, c, d, e, f) -> (a, b, c, f' d, e, f)))
 
+instance CategoricalFunctor (K1 :: Type -> Type -> Type -> Type) where
+  type Dom K1 = (->)
+  type Cod K1 = (->) ~> (->) ~> (->)
+
+  map _ = Nat (Nat (\(K1 c) -> K1 c))
+
+instance CategoricalFunctor (Forget :: Type -> Type -> Type -> Type) where
+  type Dom Forget = (->)
+  type Cod Forget = Op ~> (->) ~> (->)
+
+  map f = Nat (Nat (\(Forget g) -> Forget (f . g)))
+
 instance CategoricalFunctor ((,,,,,,) x x' x'' x''') where
   type Dom ((,,,,,,) x x' x'' x''') = (->)
   type Cod ((,,,,,,) x x' x'' x''') = (->) ~> (->) ~> (->)
 
   map :: (a -> b) -> ((->) ~> (->) ~> (->)) ((,,,,,,) x x' x'' x''' a) ((,,,,,,) x x' x'' x''' b)
   map f' = Nat (Nat (\(a, b, c, d, e, f, g) -> (a, b, c, d, f' e, f, g)))
-
---------------------------------------------------------------------------------
-
-instance MapArg3 (->) (->) (->) (,,)
-
-instance MapArg3 (->) (->) (->) ((,,,) x)
-
-instance MapArg3 (->) (->) (->) ((,,,,) x x')
-
-instance MapArg3 (->) (->) (->) ((,,,,,) x x' x'')
-
-instance MapArg3 (->) (->) (->) ((,,,,,,) x x' x'' x''')
diff --git a/test/GenericSpec.hs b/test/GenericSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/GenericSpec.hs
@@ -0,0 +1,381 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ImportQualifiedPost #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+-- | Law-checks 'CategoricalFunctor' instances that use the generic @map@
+-- default. Every instance below has an empty body, only its 'Dom' and 'Cod'.
+module GenericSpec (tests) where
+
+--------------------------------------------------------------------------------
+
+import Data.Functor.Contravariant (Op (..))
+import Data.String (fromString)
+import Generics.Kind.TH (deriveGenericK)
+import Hedgehog (Gen, Group (..), Property, PropertyName, checkSequential, forAll, property, (===))
+import Hedgehog.Classes (Laws (..))
+import Hedgehog.Gen qualified as Gen
+import Hedgehog.Range qualified as Range
+import Kindly (CategoricalFunctor (..), Iso (..), map1, map2, map3, type (~>))
+import Kindly.Functor qualified as K
+import Kindly.Functor.Laws (bifunctorLaws, contravariantFunctorLaws, functorLaws, invariantFunctorLaws, observedBifunctorLaws, observedTrifunctorLaws, profunctorLaws)
+import Prelude
+
+--------------------------------------------------------------------------------
+
+genInt :: Gen Int
+genInt = Gen.int (Range.linear (-100) 100)
+
+-- Covariant product.
+data Pair a = Pair a a
+  deriving (Eq, Show)
+
+$(deriveGenericK ''Pair)
+
+instance CategoricalFunctor Pair where
+  type Dom Pair = (->)
+  type Cod Pair = (->)
+
+genPair :: Gen a -> Gen (Pair a)
+genPair g = Pair <$> g <*> g
+
+-- Covariant nested container.
+newtype Wrap a = Wrap [a]
+  deriving (Eq, Show)
+
+$(deriveGenericK ''Wrap)
+
+instance CategoricalFunctor Wrap where
+  type Dom Wrap = (->)
+  type Cod Wrap = (->)
+
+genWrap :: Gen a -> Gen (Wrap a)
+genWrap g = Wrap <$> Gen.list (Range.linear 0 4) g
+
+-- Contravariant: the parameter to the left of an arrow.
+newtype Pred' a = Pred' (a -> Bool)
+
+$(deriveGenericK ''Pred')
+
+instance CategoricalFunctor Pred' where
+  type Dom Pred' = Op
+  type Cod Pred' = (->)
+
+genPred' :: Gen (Pred' Int)
+genPred' = (\n -> Pred' (> n)) <$> genInt
+
+obsPred' :: Pred' Int -> Int -> Bool
+obsPred' (Pred' p) = p
+
+-- Covariant with the parameter to the right of an arrow.
+data Box a = Box a (Int -> a)
+
+$(deriveGenericK ''Box)
+
+instance CategoricalFunctor Box where
+  type Dom Box = (->)
+  type Cod Box = (->)
+
+boxArrowCodomain :: Property
+boxArrowCodomain = property $ do
+  n <- forAll genInt
+  let Box v f = K.fmap (show :: Int -> String) (Box n (+ n))
+  v === show n
+  f 3 === show (3 + n)
+
+-- Invariant: the parameter on both sides of an arrow.
+newtype Endo' a = Endo' (a -> a)
+
+$(deriveGenericK ''Endo')
+
+instance CategoricalFunctor Endo' where
+  type Dom Endo' = Iso (->)
+  type Cod Endo' = (->)
+
+genEndo' :: Gen (Endo' Int)
+genEndo' = (\n -> Endo' (+ n)) <$> genInt
+
+obsEndo' :: Endo' Int -> Int -> Int
+obsEndo' (Endo' f) = f
+
+-- Invariant with mixed occurrences: contravariant in the arrow, covariant in
+-- the list.
+data Mix a = Mix (a -> Bool) [a]
+
+$(deriveGenericK ''Mix)
+
+instance CategoricalFunctor Mix where
+  type Dom Mix = Iso (->)
+  type Cod Mix = (->)
+
+genMix :: Gen (Mix Int)
+genMix = Mix . (\n -> (> n)) <$> genInt <*> Gen.list (Range.linear 0 4) genInt
+
+obsMix :: Mix Int -> Int -> (Bool, [Int])
+obsMix (Mix p xs) a = (p a, xs)
+
+-- Covariant bifunctor.
+data BiT a b = BiT a b
+  deriving (Eq, Show)
+
+$(deriveGenericK ''BiT)
+
+instance CategoricalFunctor (BiT a) where
+  type Dom (BiT a) = (->)
+  type Cod (BiT a) = (->)
+
+instance CategoricalFunctor BiT where
+  type Dom BiT = (->)
+  type Cod BiT = (->) ~> (->)
+
+genBiT :: Gen a -> Gen b -> Gen (BiT a b)
+genBiT ga gb = BiT <$> ga <*> gb
+
+-- Profunctor: contravariant in the first argument, covariant in the second.
+newtype ProT a b = ProT (a -> b)
+
+$(deriveGenericK ''ProT)
+
+instance CategoricalFunctor (ProT a) where
+  type Dom (ProT a) = (->)
+  type Cod (ProT a) = (->)
+
+instance CategoricalFunctor ProT where
+  type Dom ProT = Op
+  type Cod ProT = (->) ~> (->)
+
+genProT :: Gen (ProT Int Int)
+genProT = (\n -> ProT (+ n)) <$> genInt
+
+obsProT :: ProT Int Int -> Int -> Int
+obsProT (ProT f) = f
+
+-- Covariant first, contravariant second (a `Bifunctor (->) Op`).
+data CovCon a b = CovCon a (b -> Int)
+
+$(deriveGenericK ''CovCon)
+
+instance CategoricalFunctor (CovCon a) where
+  type Dom (CovCon a) = Op
+  type Cod (CovCon a) = (->)
+
+instance CategoricalFunctor CovCon where
+  type Dom CovCon = (->)
+  type Cod CovCon = Op ~> (->)
+
+genCovCon :: Gen (CovCon Int Int)
+genCovCon = CovCon <$> genInt <*> ((\n b -> b * 2 + n) <$> genInt)
+
+obsCovCon :: CovCon Int Int -> Int -> (Int, Int)
+obsCovCon (CovCon a f) x = (a, f x)
+
+-- Contravariant in both arguments (an Op/Op bifunctor).
+data ConCon a b = ConCon (a -> Int) (b -> Int)
+
+$(deriveGenericK ''ConCon)
+
+instance CategoricalFunctor (ConCon a) where
+  type Dom (ConCon a) = Op
+  type Cod (ConCon a) = (->)
+
+instance CategoricalFunctor ConCon where
+  type Dom ConCon = Op
+  type Cod ConCon = Op ~> (->)
+
+conConProp :: Property
+conConProp = property $ do
+  n <- forAll genInt
+  let ConCon f1 g1 = map2 (Op ((+ 1) :: Int -> Int)) (ConCon (* 2) (+ n))
+  f1 3 === (3 + 1) * 2
+  g1 5 === 5 + n
+  let ConCon f2 g2 = map1 (Op ((+ 3) :: Int -> Int)) (ConCon (* 2) (+ n))
+  f2 3 === 3 * 2
+  g2 5 === (5 + 3) + n
+
+-- Invariant first, covariant second.
+data InvCov a b = InvCov (a -> a) b
+
+$(deriveGenericK ''InvCov)
+
+instance CategoricalFunctor (InvCov a) where
+  type Dom (InvCov a) = (->)
+  type Cod (InvCov a) = (->)
+
+instance CategoricalFunctor InvCov where
+  type Dom InvCov = Iso (->)
+  type Cod InvCov = (->) ~> (->)
+
+invCovProp :: Property
+invCovProp = property $ do
+  n <- forAll genInt
+  let InvCov g1 b1 = map2 (Iso (+ (1 :: Int)) (subtract 1)) (InvCov (* 2) n)
+  g1 3 === ((3 - 1) * 2) + 1
+  b1 === n
+  let InvCov g2 b2 = map1 ((+ 10) :: Int -> Int) (InvCov ((* 2) :: Int -> Int) n)
+  g2 4 === 4 * 2
+  b2 === n + 10
+
+-- Covariant trifunctor. map3 hits the first argument, map2 the second (through
+-- the bifunctor partial application), map1 the third.
+data Tri a b c = Tri a b c
+  deriving (Eq, Show)
+
+$(deriveGenericK ''Tri)
+
+instance CategoricalFunctor (Tri a b) where
+  type Dom (Tri a b) = (->)
+  type Cod (Tri a b) = (->)
+
+instance CategoricalFunctor (Tri a) where
+  type Dom (Tri a) = (->)
+  type Cod (Tri a) = (->) ~> (->)
+
+instance CategoricalFunctor Tri where
+  type Dom Tri = (->)
+  type Cod Tri = (->) ~> (->) ~> (->)
+
+genTriBi :: Gen a -> Gen b -> Gen (Tri Int a b)
+genTriBi ga gb = Tri <$> genInt <*> ga <*> gb
+
+obsTri :: Tri Int Int Int -> Int -> (Int, Int, Int)
+obsTri (Tri a b c) _ = (a, b, c)
+
+-- Contravariant-first trifunctor, exercising the nested-Nat contravariant path.
+data TriC a b c = TriC (a -> Int) b c
+
+$(deriveGenericK ''TriC)
+
+instance CategoricalFunctor (TriC a b) where
+  type Dom (TriC a b) = (->)
+  type Cod (TriC a b) = (->)
+
+instance CategoricalFunctor (TriC a) where
+  type Dom (TriC a) = (->)
+  type Cod (TriC a) = (->) ~> (->)
+
+instance CategoricalFunctor TriC where
+  type Dom TriC = Op
+  type Cod TriC = (->) ~> (->) ~> (->)
+
+triCProp :: Property
+triCProp = property $ do
+  n <- forAll genInt
+  let TriC f b c = map3 (Op ((+ 1) :: Int -> Int)) (TriC (* 2) n (n + 1))
+  f 3 === (3 + 1) * 2
+  b === n
+  c === n + 1
+
+-- Sum types with a nullary constructor, one per variance, to exercise the
+-- interpreters' @:+:@ and @U1@ cases.
+
+data Sum3 a = S3None | S3One a | S3Two a a
+  deriving (Eq, Show)
+
+$(deriveGenericK ''Sum3)
+
+instance CategoricalFunctor Sum3 where
+  type Dom Sum3 = (->)
+  type Cod Sum3 = (->)
+
+genSum3 :: Gen a -> Gen (Sum3 a)
+genSum3 g = Gen.choice [pure S3None, S3One <$> g, S3Two <$> g <*> g]
+
+data ConSum a = CSNone | CSOne (a -> Bool) | CSTwo (a -> Int) (a -> Bool)
+
+$(deriveGenericK ''ConSum)
+
+instance CategoricalFunctor ConSum where
+  type Dom ConSum = Op
+  type Cod ConSum = (->)
+
+genConSum :: Gen (ConSum Int)
+genConSum = Gen.choice [pure CSNone, (\n -> CSOne (> n)) <$> genInt, (\n -> CSTwo (+ n) (> n)) <$> genInt]
+
+obsConSum :: ConSum Int -> Int -> (Bool, Int, Bool)
+obsConSum CSNone _ = (False, 0, False)
+obsConSum (CSOne p) x = (p x, 0, False)
+obsConSum (CSTwo f p) x = (False, f x, p x)
+
+data InvSum a = ISNone | ISOne (a -> a)
+
+$(deriveGenericK ''InvSum)
+
+instance CategoricalFunctor InvSum where
+  type Dom InvSum = Iso (->)
+  type Cod InvSum = (->)
+
+genInvSum :: Gen (InvSum Int)
+genInvSum = Gen.choice [pure ISNone, (\n -> ISOne (+ n)) <$> genInt]
+
+obsInvSum :: InvSum Int -> Int -> Int
+obsInvSum ISNone x = x
+obsInvSum (ISOne f) x = f x
+
+-- Invariant-first trifunctor.
+data TriI a b c = TriI (a -> a) b c
+
+$(deriveGenericK ''TriI)
+
+instance CategoricalFunctor (TriI a b) where
+  type Dom (TriI a b) = (->)
+  type Cod (TriI a b) = (->)
+
+instance CategoricalFunctor (TriI a) where
+  type Dom (TriI a) = (->)
+  type Cod (TriI a) = (->) ~> (->)
+
+instance CategoricalFunctor TriI where
+  type Dom TriI = Iso (->)
+  type Cod TriI = (->) ~> (->) ~> (->)
+
+triIProp :: Property
+triIProp = property $ do
+  n <- forAll genInt
+  let TriI f b c = map3 (Iso (+ (1 :: Int)) (subtract 1)) (TriI (* 2) n (n + 1))
+  f 3 === ((3 - 1) * 2) + 1
+  b === n
+  c === n + 1
+
+--------------------------------------------------------------------------------
+
+labeled :: String -> Laws -> [(PropertyName, Property)]
+labeled prefix ls = [(fromString (prefix <> " " <> n), p) | (n, p) <- lawsProperties ls]
+
+tests :: IO Bool
+tests =
+  checkSequential $
+    Group "Generic deriving" $
+      concat
+        [ labeled "Pair (product)" (functorLaws genPair),
+          labeled "Wrap [] (nested)" (functorLaws genWrap),
+          labeled "Pred' (a -> Bool)" (contravariantFunctorLaws genPred' obsPred'),
+          labeled "Endo' (a -> a)" (invariantFunctorLaws genEndo' obsEndo'),
+          labeled "Mix (a -> Bool, [a])" (invariantFunctorLaws genMix obsMix),
+          labeled "BiT (bifunctor, map2)" (bifunctorLaws genBiT),
+          labeled "BiT Int (bifunctor, map1)" (functorLaws (genBiT genInt)),
+          labeled "ProT (profunctor, map2)" (profunctorLaws genProT obsProT),
+          labeled "CovCon ((->)/Op bifunctor, map2)" (observedBifunctorLaws genCovCon obsCovCon),
+          labeled "CovCon Int (contravariant second)" (contravariantFunctorLaws genCovCon obsCovCon),
+          labeled "Tri (trifunctor, map3)" (observedTrifunctorLaws (genTriBi genInt genInt) obsTri),
+          labeled "Tri Int (trifunctor, map2)" (bifunctorLaws genTriBi),
+          labeled "Tri Int Int (trifunctor, map1)" (functorLaws (genTriBi genInt)),
+          labeled "Sum3 (covariant sum + nullary)" (functorLaws genSum3),
+          labeled "ConSum (contravariant sum + nullary)" (contravariantFunctorLaws genConSum obsConSum),
+          labeled "InvSum (invariant sum + nullary)" (invariantFunctorLaws genInvSum obsInvSum)
+        ]
+        ++ [ (fromString "Box (Int -> a) covariant arrow codomain", boxArrowCodomain),
+             (fromString "ConCon (Op/Op bifunctor)", conConProp),
+             (fromString "InvCov (invariant/covariant bifunctor)", invCovProp),
+             (fromString "TriC (contravariant-first trifunctor)", triCProp),
+             (fromString "TriI (invariant-first trifunctor)", triIProp)
+           ]
diff --git a/test/LawsSpec.hs b/test/LawsSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/LawsSpec.hs
@@ -0,0 +1,560 @@
+{-# LANGUAGE ImportQualifiedPost #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE TypeOperators #-}
+
+-- | Self-test for the @kindly-functors:laws@ sublibrary. Runs the exported
+-- 'Laws' against known-good library instances across all three variances, and
+-- across the structural and generic-representation instances the blanket
+-- @MapArgN@ instances must keep resolving (@'Data.Functor.Compose.Compose'@,
+-- @'Data.Functor.Product.Product'@, @(':*:')@, @'Data.Functor.Sum.Sum'@,
+-- @'GHC.Generics.Rec1'@, @'GHC.Generics.Par1'@). Each instance's functor laws
+-- run as hedgehog properties.
+module LawsSpec (tests) where
+
+--------------------------------------------------------------------------------
+
+import Control.Applicative (WrappedArrow (..))
+import Control.Applicative.Lift (Lift (..))
+import Control.Arrow (Kleisli (..))
+import Control.Monad.Trans.Except (ExceptT (..))
+import Control.Monad.Trans.Identity (IdentityT (..))
+import Control.Monad.Trans.Maybe (MaybeT (..))
+import Data.Bifunctor.Biff (Biff (..))
+import Data.Bifunctor.Clown (Clown (..))
+import Data.Bifunctor.Fix (Fix (..))
+import Data.Bifunctor.Flip (Flip (..))
+import Data.Bifunctor.Joker (Joker (..))
+import Data.Bifunctor.Product qualified as BiProduct
+import Data.Bifunctor.Sum qualified as BiSum
+import Data.Bifunctor.Tannen (Tannen (..))
+import Data.Bifunctor.Wrapped (WrappedBifunctor (..))
+import Data.Functor.Compose (Compose (..))
+import Data.Functor.Constant (Constant (..))
+import Data.Functor.Contravariant (Comparison (..), Equivalence (..), Op (..), Predicate (..))
+import Data.Functor.Identity (Identity (..))
+import Data.Functor.Product qualified as Product
+import Data.Functor.Reverse (Reverse (..))
+import Data.Functor.Sum (Sum (..))
+import Data.Functor.These (These1 (..))
+import Data.Graph (SCC (..))
+import Data.IntMap qualified as IntMap
+import Data.Isomorphism (Iso (..))
+import Data.List.NonEmpty (NonEmpty)
+import Data.Map qualified as Map
+import Data.Monoid (Endo (..))
+import Data.Profunctor (Costar (..), Forget (..), Star (..))
+import Data.Profunctor.Cayley (Cayley (..))
+import Data.Profunctor.Choice (CopastroSum (..), CotambaraSum (..), PastroSum (..), TambaraSum (..))
+import Data.Profunctor.Closed (Closure (..), Environment (..))
+import Data.Profunctor.Composition (Procompose (..), Rift (..))
+import Data.Profunctor.Mapping (CofreeMapping (..), FreeMapping (..))
+import Data.Profunctor.Strong (Copastro (..), Cotambara (..), Pastro (..), Tambara (..))
+import Data.Profunctor.Traversing (CofreeTraversing (..), FreeTraversing (..))
+import Data.Profunctor.Yoneda (Coyoneda (..), Yoneda (..))
+import Data.Semigroupoid.Dual (Dual (..))
+import Data.Sequence qualified as Seq
+import Data.String (fromString)
+import Data.Tagged (Tagged (..))
+import Data.Tree (Tree (..))
+import GHC.Generics (K1 (..), Par1 (..), Rec1 (..), (:*:) (..))
+import Hedgehog (Gen, Group (..), Property, PropertyName, checkSequential)
+import Hedgehog.Classes (Laws (..))
+import Hedgehog.Gen qualified as Gen
+import Hedgehog.Range qualified as Range
+-- 'Kindly' is imported only to bring the library's (orphan) CategoricalFunctor
+-- and MapArgN instances into the test's transitive scope.
+import Kindly ()
+import Kindly.Functor.Laws
+  ( bifunctorLaws,
+    bimapIsoLaws,
+    contravariantFunctorLaws,
+    functorLaws,
+    invariantFunctorLaws,
+    liftIsoLaws,
+    mapIsoLaws,
+    observedBifunctorLaws,
+    observedTrifunctorLaws,
+    profunctorLaws,
+    trimapIsoLaws,
+  )
+import Prelude
+
+--------------------------------------------------------------------------------
+-- Generators
+
+genInt :: Gen Int
+genInt = Gen.int (Range.linear (-100) 100)
+
+genMaybe :: Gen a -> Gen (Maybe a)
+genMaybe = Gen.maybe
+
+genList :: Gen a -> Gen [a]
+genList = Gen.list (Range.linear 0 4)
+
+genNonEmpty :: Gen a -> Gen (NonEmpty a)
+genNonEmpty = Gen.nonEmpty (Range.linear 1 4)
+
+genIdentity :: Gen a -> Gen (Identity a)
+genIdentity g = Identity <$> g
+
+obsIdentity :: Identity Int -> Int -> Int
+obsIdentity (Identity x) _ = x
+
+-- Observe an @Iso (->)@ morphism by running both legs.
+obsIsoCat :: Iso (->) Int Int -> Int -> (Int, Int)
+obsIsoCat i a = (embed i a, project i a)
+
+-- Structural and generic-representation functors.
+
+genCompose :: Gen a -> Gen (Compose Maybe [] a)
+genCompose g = Compose <$> genMaybe (genList g)
+
+genProduct :: Gen a -> Gen (Product.Product Maybe [] a)
+genProduct g = Product.Pair <$> genMaybe g <*> genList g
+
+genGenProd :: Gen a -> Gen ((Maybe :*: []) a)
+genGenProd g = (:*:) <$> genMaybe g <*> genList g
+
+genSum :: Gen a -> Gen (Sum Maybe [] a)
+genSum g = Gen.choice [InL <$> genMaybe g, InR <$> genList g]
+
+genRec1 :: Gen a -> Gen (Rec1 Maybe a)
+genRec1 g = Rec1 <$> genMaybe g
+
+genPar1 :: Gen a -> Gen (Par1 a)
+genPar1 g = Par1 <$> g
+
+-- Transformer functors, instantiated at 'Maybe' so 'Eq1' gives back 'Eq'.
+
+genIdentityT :: Gen a -> Gen (IdentityT Maybe a)
+genIdentityT g = IdentityT <$> genMaybe g
+
+genMaybeT :: Gen a -> Gen (MaybeT Maybe a)
+genMaybeT g = MaybeT <$> genMaybe (genMaybe g)
+
+genExceptT :: Gen a -> Gen (ExceptT Int Maybe a)
+genExceptT g = ExceptT <$> genMaybe (genEitherT genInt g)
+
+genReverse :: Gen a -> Gen (Reverse Maybe a)
+genReverse g = Reverse <$> genMaybe g
+
+genConstant :: Gen a -> Gen (Constant Int a)
+genConstant _ = Constant <$> genInt
+
+genLift :: Gen a -> Gen (Lift Maybe a)
+genLift g = Gen.choice [Pure <$> g, Other <$> genMaybe g]
+
+genThese1 :: Gen a -> Gen (These1 Maybe [] a)
+genThese1 g =
+  Gen.choice
+    [ This1 <$> genMaybe g,
+      That1 <$> genList g,
+      These1 <$> genMaybe g <*> genList g
+    ]
+
+-- Contravariant witness. 'Predicate' has no 'Eq' or 'Show', so observe by running.
+
+genPredicate :: Gen (Predicate Int)
+genPredicate = (\n -> Predicate (> n)) <$> genInt
+
+obsPredicate :: Predicate a -> a -> Bool
+obsPredicate (Predicate p) = p
+
+genComparison :: Gen (Comparison Int)
+genComparison = (\n -> Comparison (\x y -> compare (x + n) y)) <$> genInt
+
+obsComparison :: Comparison Int -> Int -> (Ordering, Ordering)
+obsComparison (Comparison c) a = (c a 0, c 0 a)
+
+genEquivalence :: Gen (Equivalence Int)
+genEquivalence = (\n -> Equivalence (\x y -> div x n == div y n)) <$> Gen.int (Range.linear 1 10)
+
+obsEquivalence :: Equivalence Int -> Int -> (Bool, Bool)
+obsEquivalence (Equivalence e) a = (e a 0, e 0 a)
+
+genOp :: Gen (Op Int Int)
+genOp = (\n -> Op (* n)) <$> genInt
+
+obsOp :: Op Int Int -> Int -> Int
+obsOp (Op g) = g
+
+-- Invariant witness 'Endo', observed by applying.
+
+genEndo :: Gen (Endo Int)
+genEndo = (\n -> Endo (+ n)) <$> genInt
+
+obsEndo :: Endo a -> a -> a
+obsEndo (Endo h) = h
+
+-- Bifunctor witnesses.
+
+genPairT :: Gen a -> Gen b -> Gen (a, b)
+genPairT ga gb = (,) <$> ga <*> gb
+
+genEitherT :: Gen a -> Gen b -> Gen (Either a b)
+genEitherT ga gb = Gen.choice [Left <$> ga, Right <$> gb]
+
+-- Bifunctors-package witnesses.
+
+genFlipT :: Gen a -> Gen b -> Gen (Flip (,) a b)
+genFlipT ga gb = Flip <$> genPairT gb ga
+
+genClownT :: Gen a -> Gen b -> Gen (Clown Maybe a b)
+genClownT ga _ = Clown <$> genMaybe ga
+
+genJokerT :: Gen a -> Gen b -> Gen (Joker Maybe a b)
+genJokerT _ gb = Joker <$> genMaybe gb
+
+genBiProductT :: Gen a -> Gen b -> Gen (BiProduct.Product (,) Either a b)
+genBiProductT ga gb = BiProduct.Pair <$> genPairT ga gb <*> genEitherT ga gb
+
+genBiSumT :: Gen a -> Gen b -> Gen (BiSum.Sum (,) Either a b)
+genBiSumT ga gb = Gen.choice [BiSum.L2 <$> genPairT ga gb, BiSum.R2 <$> genEitherT ga gb]
+
+genTannenT :: Gen a -> Gen b -> Gen (Tannen Maybe (,) a b)
+genTannenT ga gb = Tannen <$> genMaybe (genPairT ga gb)
+
+genBiffT :: Gen a -> Gen b -> Gen (Biff (,) Maybe [] a b)
+genBiffT ga gb = Biff <$> genPairT (genMaybe ga) (genList gb)
+
+genWrappedT :: Gen a -> Gen b -> Gen (WrappedBifunctor (,) a b)
+genWrappedT ga gb = WrapBifunctor <$> genPairT ga gb
+
+-- Profunctor witnesses, observed by running since they are function-shaped.
+
+genFn :: Gen (Int -> Int)
+genFn = (\n x -> x * 2 + n) <$> genInt
+
+obsFn :: (Int -> Int) -> Int -> Int
+obsFn g = g
+
+genStar :: Gen (Star Maybe Int Int)
+genStar = (\n -> Star (\x -> if x > n then Just (x + n) else Nothing)) <$> genInt
+
+obsStar :: Star Maybe Int Int -> Int -> Maybe Int
+obsStar (Star g) = g
+
+genCostar :: Gen (Costar Maybe Int Int)
+genCostar = (\n -> Costar (maybe n (+ n))) <$> genInt
+
+obsCostar :: Costar Maybe Int Int -> Int -> (Int, Int)
+obsCostar (Costar g) a = (g (Just a), g Nothing)
+
+genForget :: Gen (Forget Int Int Int)
+genForget = (\n -> Forget (* n)) <$> genInt
+
+obsForget :: Forget Int Int Int -> Int -> Int
+obsForget (Forget g) = g
+
+genKleisli :: Gen (Kleisli Maybe Int Int)
+genKleisli = (\n -> Kleisli (\x -> if x > n then Just (x - n) else Nothing)) <$> genInt
+
+obsKleisli :: Kleisli Maybe Int Int -> Int -> Maybe Int
+obsKleisli (Kleisli g) = g
+
+genWrappedArrow :: Gen (WrappedArrow (->) Int Int)
+genWrappedArrow = (\n -> WrapArrow (+ n)) <$> genInt
+
+obsWrappedArrow :: WrappedArrow (->) Int Int -> Int -> Int
+obsWrappedArrow (WrapArrow g) = g
+
+genProcompose :: Gen (Procompose (->) (->) Int Int)
+genProcompose = (\n m -> Procompose (+ n) (* m)) <$> genInt <*> genInt
+
+obsProcompose :: Procompose (->) (->) Int Int -> Int -> Int
+obsProcompose (Procompose g h) = g . h
+
+genRift :: Gen (Rift (->) (->) Int Int)
+genRift = (\n -> Rift (\g -> g . (+ n))) <$> genInt
+
+obsRift :: Rift (->) (->) Int Int -> Int -> Int
+obsRift r = runRift r (* 2)
+
+genYoneda :: Gen (Yoneda (->) Int Int)
+genYoneda = (\n -> Yoneda (\l r -> r . (+ n) . l)) <$> genInt
+
+obsYoneda :: Yoneda (->) Int Int -> Int -> Int
+obsYoneda y = runYoneda y id id
+
+genCoyoneda :: Gen (Coyoneda (->) Int Int)
+genCoyoneda = (\n -> Coyoneda id id (+ n)) <$> genInt
+
+obsCoyoneda :: Coyoneda (->) Int Int -> Int -> Int
+obsCoyoneda (Coyoneda l r g) = r . g . l
+
+genCayley :: Gen (Cayley Maybe (->) Int Int)
+genCayley = Cayley <$> genMaybe ((+) <$> genInt)
+
+obsCayley :: Cayley Maybe (->) Int Int -> Int -> Maybe Int
+obsCayley (Cayley mf) a = fmap ($ a) mf
+
+genTambara :: Gen (Tambara (->) Int Int)
+genTambara = (\n -> Tambara (\(a, c) -> (a + n, c))) <$> genInt
+
+obsTambara :: Tambara (->) Int Int -> Int -> Int
+obsTambara (Tambara t) a = fst (t (a, ()))
+
+genPastro :: Gen (Pastro (->) Int Int)
+genPastro = (\n k -> Pastro (uncurry (+)) (* n) (,k)) <$> genInt <*> genInt
+
+obsPastro :: Pastro (->) Int Int -> Int -> Int
+obsPastro (Pastro l m r) a = case r a of (x, z) -> l (m x, z)
+
+genCotambara :: Gen (Cotambara (->) Int Int)
+genCotambara = (\n -> Cotambara id (+ n)) <$> genInt
+
+obsCotambara :: Cotambara (->) Int Int -> Int -> Int
+obsCotambara (Cotambara n r) = n r
+
+genCopastro :: Gen (Copastro (->) Int Int)
+genCopastro = (\n -> Copastro (\k -> k (+ n))) <$> genInt
+
+obsCopastro :: Copastro (->) Int Int -> Int -> Int
+obsCopastro (Copastro g) = g id
+
+genTambaraSum :: Gen (TambaraSum (->) Int Int)
+genTambaraSum = (\n -> TambaraSum (either (Left . (+ n)) Right)) <$> genInt
+
+obsTambaraSum :: TambaraSum (->) Int Int -> Int -> Either Int ()
+obsTambaraSum (TambaraSum t) a = t (Left a)
+
+genPastroSum :: Gen (PastroSum (->) Int Int)
+genPastroSum = (\n -> PastroSum (either id id) (* n) Left) <$> genInt
+
+obsPastroSum :: PastroSum (->) Int Int -> Int -> Int
+obsPastroSum (PastroSum l m r) a = case r a of
+  Left x -> l (Left (m x))
+  Right z -> l (Right z)
+
+genCotambaraSum :: Gen (CotambaraSum (->) Int Int)
+genCotambaraSum = (\n -> CotambaraSum id (+ n)) <$> genInt
+
+obsCotambaraSum :: CotambaraSum (->) Int Int -> Int -> Int
+obsCotambaraSum (CotambaraSum n r) = n r
+
+genCopastroSum :: Gen (CopastroSum (->) Int Int)
+genCopastroSum = (\n -> CopastroSum (\k -> k (+ n))) <$> genInt
+
+obsCopastroSum :: CopastroSum (->) Int Int -> Int -> Int
+obsCopastroSum (CopastroSum g) = g id
+
+genClosure :: Gen (Closure (->) Int Int)
+genClosure = (\n -> Closure (\g x -> g x + n)) <$> genInt
+
+obsClosure :: Closure (->) Int Int -> Int -> Int
+obsClosure (Closure t) = t (* 2)
+
+genEnvironment :: Gen (Environment (->) Int Int)
+genEnvironment = (\n -> Environment ($ n) (* 2) (+)) <$> genInt
+
+obsEnvironment :: Environment (->) Int Int -> Int -> Int
+obsEnvironment (Environment l m r) a = l (m . r a)
+
+genFreeTraversing :: Gen (FreeTraversing (->) Int Int)
+genFreeTraversing = (\n -> FreeTraversing sum (* n) (\a -> [a, a + 1])) <$> genInt
+
+obsFreeTraversing :: FreeTraversing (->) Int Int -> Int -> Int
+obsFreeTraversing (FreeTraversing l m r) a = l (fmap m (r a))
+
+genCofreeTraversing :: Gen (CofreeTraversing (->) Int Int)
+genCofreeTraversing = (\n -> CofreeTraversing (fmap (+ n))) <$> genInt
+
+obsCofreeTraversing :: CofreeTraversing (->) Int Int -> Int -> [Int]
+obsCofreeTraversing (CofreeTraversing t) a = t [a, a + 1]
+
+genFreeMapping :: Gen (FreeMapping (->) Int Int)
+genFreeMapping = (\n -> FreeMapping sum (* n) (\a -> [a, a + 1])) <$> genInt
+
+obsFreeMapping :: FreeMapping (->) Int Int -> Int -> Int
+obsFreeMapping (FreeMapping l m r) a = l (fmap m (r a))
+
+genCofreeMapping :: Gen (CofreeMapping (->) Int Int)
+genCofreeMapping = (\n -> CofreeMapping (fmap (+ n))) <$> genInt
+
+obsCofreeMapping :: CofreeMapping (->) Int Int -> Int -> [Int]
+obsCofreeMapping (CofreeMapping t) a = t [a, a + 1]
+
+genTagged :: Gen a -> Gen (Tagged () a)
+genTagged g = Tagged <$> g
+
+genTaggedP :: Gen (Tagged Int Int)
+genTaggedP = Tagged <$> genInt
+
+obsTaggedP :: Tagged Int Int -> Int -> Int
+obsTaggedP (Tagged b) _ = b
+
+genFix :: Gen a -> Gen (Fix Either a)
+genFix g = Gen.recursive Gen.choice [In . Right <$> g] [In . Left <$> genFix g]
+
+genMap :: Gen a -> Gen (Map.Map Int a)
+genMap g = Map.fromList <$> genList ((,) <$> genInt <*> g)
+
+genIntMap :: Gen a -> Gen (IntMap.IntMap a)
+genIntMap g = IntMap.fromList <$> genList ((,) <$> genInt <*> g)
+
+genSeq :: Gen a -> Gen (Seq.Seq a)
+genSeq g = Seq.fromList <$> genList g
+
+genViewL :: Gen a -> Gen (Seq.ViewL a)
+genViewL g = Seq.viewl <$> genSeq g
+
+genViewR :: Gen a -> Gen (Seq.ViewR a)
+genViewR g = Seq.viewr <$> genSeq g
+
+genTree :: Gen a -> Gen (Tree a)
+genTree g = Gen.recursive Gen.choice [Node <$> g <*> pure []] [Node <$> g <*> Gen.list (Range.linear 0 3) (genTree g)]
+
+genSCC :: Gen a -> Gen (SCC a)
+genSCC g = Gen.choice [AcyclicSCC <$> g, CyclicSCC <$> Gen.list (Range.linear 1 4) g]
+
+genConstantT :: Gen a -> Gen b -> Gen (Constant a b)
+genConstantT ga _ = Constant <$> ga
+
+genDual :: Gen (Dual (->) Int Int)
+genDual = (\n -> Dual (+ n)) <$> genInt
+
+obsDual :: Dual (->) Int Int -> Int -> Int
+obsDual (Dual g) = g
+
+genTriple :: Gen (Int, Int, Int)
+genTriple = (,,) <$> genInt <*> genInt <*> genInt
+
+obsTriple :: (Int, Int, Int) -> Int -> (Int, Int, Int)
+obsTriple t _ = t
+
+genForgetT :: Gen (Forget Int Int Int)
+genForgetT = (\n -> Forget (* n)) <$> genInt
+
+obsForgetT :: Forget Int Int Int -> Int -> Int
+obsForgetT (Forget g) = g
+
+genK1 :: Gen (K1 Int Int Int)
+genK1 = K1 <$> genInt
+
+obsK1 :: K1 Int Int Int -> Int -> Int
+obsK1 (K1 c) _ = c
+
+--------------------------------------------------------------------------------
+
+-- | Splice a sublibrary 'Laws' into a hedgehog 'Group', prefixing each property
+-- with the instance under test.
+labeled :: String -> Laws -> [(PropertyName, Property)]
+labeled prefix ls = [(fromString (prefix <> " " <> n), p) | (n, p) <- lawsProperties ls]
+
+tests :: IO Bool
+tests =
+  checkSequential $
+    Group "Functor laws" $
+      concat
+        [ -- Covariant leaves.
+          labeled "Maybe" (functorLaws genMaybe),
+          labeled "[]" (functorLaws genList),
+          labeled "Identity" (functorLaws genIdentity),
+          labeled "NonEmpty" (functorLaws genNonEmpty),
+          -- Structural and generic-representation instances.
+          labeled "Compose Maybe []" (functorLaws genCompose),
+          labeled "Product Maybe []" (functorLaws genProduct),
+          labeled "Maybe :*: []" (functorLaws genGenProd),
+          labeled "Sum Maybe []" (functorLaws genSum),
+          labeled "Rec1 Maybe" (functorLaws genRec1),
+          labeled "Par1" (functorLaws genPar1),
+          -- Transformer and companion functors.
+          labeled "IdentityT Maybe" (functorLaws genIdentityT),
+          labeled "MaybeT Maybe" (functorLaws genMaybeT),
+          labeled "ExceptT Int Maybe" (functorLaws genExceptT),
+          labeled "Reverse Maybe" (functorLaws genReverse),
+          labeled "Constant Int" (functorLaws genConstant),
+          labeled "Lift Maybe" (functorLaws genLift),
+          labeled "These1 Maybe []" (functorLaws genThese1),
+          -- Contravariant and invariant variances.
+          labeled "Predicate" (contravariantFunctorLaws genPredicate obsPredicate),
+          labeled "Comparison" (contravariantFunctorLaws genComparison obsComparison),
+          labeled "Equivalence" (contravariantFunctorLaws genEquivalence obsEquivalence),
+          labeled "Op Int" (contravariantFunctorLaws genOp obsOp),
+          labeled "Endo" (invariantFunctorLaws genEndo obsEndo),
+          -- mapIso across all three variances (isomorphism mapping).
+          labeled "mapIso Identity" (mapIsoLaws (genIdentity genInt) obsIdentity),
+          labeled "mapIso Predicate" (mapIsoLaws genPredicate obsPredicate),
+          labeled "mapIso Endo" (mapIsoLaws genEndo obsEndo),
+          -- bimapIso: isomorphism mapping through a bifunctor's positions.
+          labeled "bimapIso (,)" (bimapIsoLaws (genPairT genInt genInt) const),
+          labeled "bimapIso Op" (bimapIsoLaws genOp obsOp),
+          labeled "bimapIso Dual (->)" (bimapIsoLaws genDual obsDual),
+          -- trimapIso: isomorphism mapping through a trifunctor's positions.
+          labeled "trimapIso (,,)" (trimapIsoLaws genTriple obsTriple),
+          labeled "trimapIso Forget" (trimapIsoLaws genForgetT obsForgetT),
+          labeled "trimapIso K1" (trimapIsoLaws genK1 obsK1),
+          -- liftIso: the core-groupoid inclusion at each target category.
+          labeled "liftIso (->)" (liftIsoLaws obsFn),
+          labeled "liftIso Op" (liftIsoLaws obsOp),
+          labeled "liftIso Iso (->)" (liftIsoLaws obsIsoCat),
+          labeled "liftIso Star Maybe" (liftIsoLaws obsStar),
+          labeled "liftIso Kleisli Maybe" (liftIsoLaws obsKleisli),
+          -- Covariant bifunctors (map2).
+          labeled "(,)" (bifunctorLaws genPairT),
+          labeled "Either" (bifunctorLaws genEitherT),
+          -- Bifunctors-package types (map2 and map1 at the partial application).
+          labeled "Flip (,)" (bifunctorLaws genFlipT),
+          labeled "Flip (,) Int" (functorLaws (genFlipT genInt)),
+          labeled "Clown Maybe" (bifunctorLaws genClownT),
+          labeled "Clown Maybe Int" (functorLaws (genClownT genInt)),
+          labeled "Joker Maybe" (bifunctorLaws genJokerT),
+          labeled "Joker Maybe Int" (functorLaws (genJokerT genInt)),
+          labeled "Product (,) Either" (bifunctorLaws genBiProductT),
+          labeled "Product (,) Either Int" (functorLaws (genBiProductT genInt)),
+          labeled "Sum (,) Either" (bifunctorLaws genBiSumT),
+          labeled "Sum (,) Either Int" (functorLaws (genBiSumT genInt)),
+          labeled "Tannen Maybe (,)" (bifunctorLaws genTannenT),
+          labeled "Tannen Maybe (,) Int" (functorLaws (genTannenT genInt)),
+          labeled "Biff (,) Maybe []" (bifunctorLaws genBiffT),
+          labeled "Biff (,) Maybe [] Int" (functorLaws (genBiffT genInt)),
+          labeled "WrappedBifunctor (,)" (bifunctorLaws genWrappedT),
+          labeled "WrappedBifunctor (,) Int" (functorLaws (genWrappedT genInt)),
+          -- Profunctors (map2 at Op).
+          labeled "(->)" (profunctorLaws genFn obsFn),
+          labeled "Star Maybe" (profunctorLaws genStar obsStar),
+          labeled "Costar Maybe" (profunctorLaws genCostar obsCostar),
+          labeled "Forget Int" (profunctorLaws genForget obsForget),
+          labeled "Kleisli Maybe" (profunctorLaws genKleisli obsKleisli),
+          labeled "WrappedArrow (->)" (profunctorLaws genWrappedArrow obsWrappedArrow),
+          labeled "Procompose (->) (->)" (profunctorLaws genProcompose obsProcompose),
+          labeled "Rift (->) (->)" (profunctorLaws genRift obsRift),
+          labeled "Yoneda (->)" (profunctorLaws genYoneda obsYoneda),
+          labeled "Coyoneda (->)" (profunctorLaws genCoyoneda obsCoyoneda),
+          labeled "Cayley Maybe (->)" (profunctorLaws genCayley obsCayley),
+          labeled "Tambara (->)" (profunctorLaws genTambara obsTambara),
+          labeled "Pastro (->)" (profunctorLaws genPastro obsPastro),
+          labeled "Cotambara (->)" (profunctorLaws genCotambara obsCotambara),
+          labeled "Copastro (->)" (profunctorLaws genCopastro obsCopastro),
+          labeled "TambaraSum (->)" (profunctorLaws genTambaraSum obsTambaraSum),
+          labeled "PastroSum (->)" (profunctorLaws genPastroSum obsPastroSum),
+          labeled "CotambaraSum (->)" (profunctorLaws genCotambaraSum obsCotambaraSum),
+          labeled "CopastroSum (->)" (profunctorLaws genCopastroSum obsCopastroSum),
+          labeled "Closure (->)" (profunctorLaws genClosure obsClosure),
+          labeled "Environment (->)" (profunctorLaws genEnvironment obsEnvironment),
+          labeled "FreeTraversing (->)" (profunctorLaws genFreeTraversing obsFreeTraversing),
+          labeled "CofreeTraversing (->)" (profunctorLaws genCofreeTraversing obsCofreeTraversing),
+          labeled "FreeMapping (->)" (profunctorLaws genFreeMapping obsFreeMapping),
+          labeled "CofreeMapping (->)" (profunctorLaws genCofreeMapping obsCofreeMapping),
+          labeled "Tagged ()" (functorLaws genTagged),
+          labeled "Tagged" (profunctorLaws genTaggedP obsTaggedP),
+          -- Op as a bifunctor into Op: covariant map2, contravariant map1.
+          labeled "Op" (observedBifunctorLaws genOp obsOp),
+          labeled "Fix Either" (functorLaws genFix),
+          labeled "Map Int" (functorLaws genMap),
+          labeled "IntMap" (functorLaws genIntMap),
+          labeled "Seq" (functorLaws genSeq),
+          labeled "ViewL" (functorLaws genViewL),
+          labeled "ViewR" (functorLaws genViewR),
+          labeled "Tree" (functorLaws genTree),
+          labeled "SCC" (functorLaws genSCC),
+          labeled "Constant" (bifunctorLaws genConstantT),
+          labeled "Dual (->) Int" (contravariantFunctorLaws genDual obsDual),
+          labeled "Dual (->)" (observedBifunctorLaws genDual obsDual),
+          -- Trifunctors (map3).
+          labeled "(,,)" (observedTrifunctorLaws genTriple obsTriple),
+          labeled "Forget" (observedTrifunctorLaws genForgetT obsForgetT),
+          labeled "K1" (observedTrifunctorLaws genK1 obsK1)
+        ]
diff --git a/test/Main.hs b/test/Main.hs
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -9,16 +9,37 @@
 
 --------------------------------------------------------------------------------
 
+import Control.Arrow (Kleisli (..))
+import Control.Monad (when)
 import Data.Functor.Contravariant (Op (..), Predicate (..))
 import Data.Functor.Identity (Identity (..))
+import Data.Isomorphism (Iso (Iso))
 import Data.Maybe (maybeToList)
+import Data.Monoid (Endo (..))
+import Data.Profunctor (Star (..))
+import GenericSpec qualified
 import Kindly qualified as UUT
-import Test.Hspec (describe, hspec, it, shouldBe)
+import LawsSpec qualified
+import Rank2LawsSpec qualified
+import System.Exit (exitFailure)
+import Test.Hspec (Spec, describe, it, shouldBe)
+import Test.Hspec.Runner (defaultConfig, hspecWithResult, summaryFailures)
 
 --------------------------------------------------------------------------------
 
 main :: IO ()
-main = hspec $ do
+main = do
+  summary <- hspecWithResult defaultConfig exampleSpec
+  lawsOk <- LawsSpec.tests
+  rank2Ok <- Rank2LawsSpec.tests
+  genOk <- GenericSpec.tests
+  when (summaryFailures summary > 0 || not lawsOk || not rank2Ok || not genOk) exitFailure
+
+--------------------------------------------------------------------------------
+-- Example-based (characterization) tests
+
+exampleSpec :: Spec
+exampleSpec = do
   describe "fmap" $ do
     it "works covariantly" $ do
       UUT.fmap show (Identity True) `shouldBe` Identity "True"
@@ -27,7 +48,36 @@
     it "composes" $ do
       (UUT.fmap . UUT.fmap) show (Just (Just True)) `shouldBe` Just (Just "True")
       UUT.fmap ((\f -> f "True") . getPredicate) ((UUT.fmap . UUT.fmap) (Op read) (Just (Predicate not))) `shouldBe` Just False
+    it "works over a constrained instance (Kleisli)" $ do
+      runKleisli (UUT.fmap show (Kleisli Identity)) (5 :: Int) `shouldBe` Identity "5"
 
+  describe "invmap" $ do
+    it "works invariantly (Endo)" $ do
+      appEndo (UUT.invmap (+ 1) (subtract 1) (Endo (* 2))) (5 :: Int) `shouldBe` 9
+    it "works covariantly (Identity), dropping the backward leg" $ do
+      UUT.invmap (show :: Int -> String) (read :: String -> Int) (Identity (5 :: Int)) `shouldBe` Identity "5"
+    it "works contravariantly (Predicate), dropping the forward leg" $ do
+      getPredicate (UUT.invmap (show :: Int -> String) (read :: String -> Int) (Predicate even)) "4" `shouldBe` True
+      getPredicate (UUT.invmap (show :: Int -> String) (read :: String -> Int) (Predicate even)) "5" `shouldBe` False
+
+  describe "mapIso" $ do
+    it "maps an iso through a covariant functor (Identity)" $ do
+      UUT.mapIso (Iso (show :: Int -> String) (read :: String -> Int)) (Identity (5 :: Int)) `shouldBe` Identity "5"
+    it "maps an iso through a contravariant functor (Predicate)" $ do
+      getPredicate (UUT.mapIso (Iso (show :: Int -> String) (read :: String -> Int)) (Predicate even)) "4" `shouldBe` True
+    it "maps an iso through an invariant functor (Endo)" $ do
+      appEndo (UUT.mapIso (Iso (+ 1) (subtract 1)) (Endo (* 2))) (5 :: Int) `shouldBe` 9
+
+  describe "liftIso (Star)" $ do
+    it "wraps the forward leg in pure, dropping the backward leg" $ do
+      runStar (UUT.liftIso (Iso (show :: Int -> String) (read :: String -> Int)) :: Star Maybe Int String) 5 `shouldBe` Just "5"
+    it "sends an identity iso to the Kleisli identity" $ do
+      runStar (UUT.liftIso (Iso id id :: Iso (->) Int Int) :: Star Maybe Int Int) 5 `shouldBe` Just 5
+
+  describe "liftIso (Kleisli)" $ do
+    it "wraps the forward leg in pure, dropping the backward leg" $ do
+      runKleisli (UUT.liftIso (Iso (show :: Int -> String) (read :: String -> Int)) :: Kleisli Maybe Int String) 5 `shouldBe` Just "5"
+
   describe "lmap" $ do
     it "works covariantly" $ do
       UUT.lmap show (True, False) `shouldBe` ("True", False)
@@ -45,15 +95,24 @@
     it "works contravariantly" $ do
       UUT.bimap (Op (read @Int)) show (+ 1) "0" `shouldBe` "1"
 
-  describe "bimap" $ do
+  describe "trimap" $ do
     it "works covariantly" $ do
       UUT.trimap show show show (True, False, ()) `shouldBe` ("True", "False", "()")
 
-  describe "bmap" $ do
-    it "works" $ do
+  describe "bmap1" $ do
+    it "maps the rightmost functor" $ do
       let hkd = MyHKD (Just True) Nothing
-      project (UUT.bmap maybeToList hkd) `shouldBe` ([True], [])
+      project (UUT.bmap1 maybeToList hkd) `shouldBe` ([True], [])
 
+  describe "bmap2 / bmap1 on a two-functor HKD" $ do
+    it "bmap2 hits the first parameter" $ do
+      projeH2a (UUT.bmap2 maybeToList (MyHKD2 (Just True) (Just 1))) `shouldBe` ([True], Just (1 :: Int))
+    it "bmap1 hits the second parameter" $ do
+      projeH2b (UUT.bmap1 maybeToList (MyHKD2 (Just True) (Just 1))) `shouldBe` (Just True, [1 :: Int])
+
+--------------------------------------------------------------------------------
+-- Rank-2 witnesses
+
 data MyHKD f = MyHKD {one :: f Bool, two :: f ()}
 
 project :: MyHKD f -> (f Bool, f ())
@@ -66,11 +125,22 @@
   map :: (UUT.Nat (->) (->)) f g -> MyHKD f -> MyHKD g
   map (UUT.Nat nat) MyHKD {..} = MyHKD (nat one) (nat two)
 
-newtype MyHKD2 p = MyHKD2 {field :: p () Bool}
+data MyHKD2 f g = MyHKD2 (f Bool) (g Int)
 
+projeH2a :: MyHKD2 [] Maybe -> ([Bool], Maybe Int)
+projeH2a (MyHKD2 a b) = (a, b)
+
+projeH2b :: MyHKD2 Maybe [] -> (Maybe Bool, [Int])
+projeH2b (MyHKD2 a b) = (a, b)
+
+instance UUT.CategoricalFunctor (MyHKD2 f) where
+  type Dom (MyHKD2 f) = (->) UUT.~> (->)
+  type Cod (MyHKD2 f) = (->)
+
+  map (UUT.Nat nat) (MyHKD2 a b) = MyHKD2 a (nat b)
+
 instance UUT.CategoricalFunctor MyHKD2 where
-  type Dom MyHKD2 = (->) UUT.~> ((->) UUT.~> (->))
-  type Cod MyHKD2 = (->)
+  type Dom MyHKD2 = (->) UUT.~> (->)
+  type Cod MyHKD2 = ((->) UUT.~> (->)) UUT.~> (->)
 
-  map :: UUT.Dom MyHKD2 p q -> MyHKD2 p -> MyHKD2 q
-  map (UUT.Nat (UUT.Nat nat)) MyHKD2 {..} = MyHKD2 (nat field)
+  map (UUT.Nat nat) = UUT.Nat (\(MyHKD2 a b) -> MyHKD2 (nat a) b)
diff --git a/test/Rank2LawsSpec.hs b/test/Rank2LawsSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Rank2LawsSpec.hs
@@ -0,0 +1,178 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE ImportQualifiedPost #-}
+{-# LANGUAGE InstanceSigs #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+-- | Self-test for @kindly-functors:laws@' rank-2 bundles. Runs 'bmap1Laws',
+-- 'bmap2Laws', and 'bmap3Laws' against covariant one-, two-, and three-functor
+-- witnesses, plus a contravariant and an invariant witness, so the reused
+-- bundles exercise every variance. The witnesses carry lists, so @reverse@ and
+-- @drop 1@ give genuine, composition-distinguishing natural transformations.
+-- The contravariant and invariant witnesses hold functions, so they are compared
+-- by observation against fixed probe inputs.
+module Rank2LawsSpec (tests) where
+
+--------------------------------------------------------------------------------
+
+import Data.Functor.Contravariant (Op (..))
+import Data.Isomorphism (Iso (..), embed, project)
+import Data.String (fromString)
+import Hedgehog (Gen, Group (..), Property, PropertyName, checkSequential)
+import Hedgehog.Classes (Laws (..))
+import Hedgehog.Gen qualified as Gen
+import Hedgehog.Range qualified as Range
+import Kindly (CategoricalFunctor (..), Nat (..), type (~>))
+import Kindly.Rank2.Laws (bmap1Laws, bmap2Laws, bmap3Laws)
+import Prelude
+
+--------------------------------------------------------------------------------
+-- Covariant witnesses (one, two, three functor parameters)
+
+data H1 f = H1 (f Bool) (f Int)
+
+deriving instance (Eq (f Bool), Eq (f Int)) => Eq (H1 f)
+
+deriving instance (Show (f Bool), Show (f Int)) => Show (H1 f)
+
+instance CategoricalFunctor H1 where
+  type Dom H1 = (->) ~> (->)
+  type Cod H1 = (->)
+  map :: Nat (->) (->) f g -> H1 f -> H1 g
+  map (Nat nat) (H1 a b) = H1 (nat a) (nat b)
+
+data H2 f g = H2 (f Bool) (g Int)
+
+deriving instance (Eq (f Bool), Eq (g Int)) => Eq (H2 f g)
+
+deriving instance (Show (f Bool), Show (g Int)) => Show (H2 f g)
+
+instance CategoricalFunctor (H2 f) where
+  type Dom (H2 f) = (->) ~> (->)
+  type Cod (H2 f) = (->)
+  map (Nat nat) (H2 a b) = H2 a (nat b)
+
+instance CategoricalFunctor H2 where
+  type Dom H2 = (->) ~> (->)
+  type Cod H2 = ((->) ~> (->)) ~> (->)
+  map (Nat nat) = Nat (\(H2 a b) -> H2 (nat a) b)
+
+data H3 f g h = H3 (f Bool) (g Int) (h Bool)
+
+deriving instance (Eq (f Bool), Eq (g Int), Eq (h Bool)) => Eq (H3 f g h)
+
+deriving instance (Show (f Bool), Show (g Int), Show (h Bool)) => Show (H3 f g h)
+
+instance CategoricalFunctor (H3 f g) where
+  type Dom (H3 f g) = (->) ~> (->)
+  type Cod (H3 f g) = (->)
+  map (Nat nat) (H3 a b c) = H3 a b (nat c)
+
+instance CategoricalFunctor (H3 f) where
+  type Dom (H3 f) = (->) ~> (->)
+  type Cod (H3 f) = ((->) ~> (->)) ~> (->)
+  map (Nat nat) = Nat (\(H3 a b c) -> H3 a (nat b) c)
+
+instance CategoricalFunctor H3 where
+  type Dom H3 = (->) ~> (->)
+  type Cod H3 = ((->) ~> (->)) ~> ((->) ~> (->)) ~> (->)
+  map (Nat nat) = Nat (Nat (\(H3 a b c) -> H3 (nat a) b c))
+
+--------------------------------------------------------------------------------
+-- Contravariant and invariant witnesses (function-shaped, over lists)
+
+newtype Consumer f = Consumer (f Int -> Int)
+
+instance CategoricalFunctor Consumer where
+  type Dom Consumer = (->) ~> Op
+  type Cod Consumer = (->)
+  map (Nat opnat) (Consumer c) = Consumer (c . getOp opnat)
+
+newtype Endo1 f = Endo1 (f Int -> f Int)
+
+instance CategoricalFunctor Endo1 where
+  type Dom Endo1 = (->) ~> Iso (->)
+  type Cod Endo1 = (->)
+  map (Nat iso) (Endo1 h) = Endo1 (embed iso . h . project iso)
+
+-- Observation: compare function-shaped witnesses by running them on probes.
+
+consumerProbes :: [[Int]]
+consumerProbes = [[], [0], [1, 2], [3, 4, 5]]
+
+instance Eq (Consumer []) where
+  Consumer p == Consumer q = fmap p consumerProbes == fmap q consumerProbes
+
+instance Show (Consumer []) where
+  show (Consumer p) = "Consumer " <> show (fmap p consumerProbes)
+
+instance Eq (Endo1 []) where
+  Endo1 p == Endo1 q = fmap p consumerProbes == fmap q consumerProbes
+
+instance Show (Endo1 []) where
+  show (Endo1 p) = "Endo1 " <> show (fmap p consumerProbes)
+
+--------------------------------------------------------------------------------
+-- Generators and sample natural transformations
+
+genInt :: Gen Int
+genInt = Gen.int (Range.linear (-100) 100)
+
+genList :: Gen a -> Gen [a]
+genList = Gen.list (Range.linear 0 4)
+
+genH1 :: Gen (H1 [])
+genH1 = H1 <$> genList Gen.bool <*> genList genInt
+
+genH2 :: Gen (H2 [] [])
+genH2 = H2 <$> genList Gen.bool <*> genList genInt
+
+genH3 :: Gen (H3 [] [] [])
+genH3 = H3 <$> genList Gen.bool <*> genList genInt <*> genList Gen.bool
+
+genConsumer :: Gen (Consumer [])
+genConsumer = Gen.element [Consumer sum, Consumer length, Consumer (sum . drop 1)]
+
+genEndo1 :: Gen (Endo1 [])
+genEndo1 = Gen.element [Endo1 id, Endo1 reverse, Endo1 (drop 1)]
+
+-- Covariant samples: natural transformations @forall x. [x] -> [x]@.
+-- Contravariant samples: the same wrapped in @Op@.
+-- Invariant samples: paired legs in @Iso (->)@.
+
+opReverse :: forall x. Op [x] [x]
+opReverse = Op reverse
+
+opDrop :: forall x. Op [x] [x]
+opDrop = Op (drop 1)
+
+isoReverse :: forall x. Iso (->) [x] [x]
+isoReverse = Iso reverse reverse
+
+isoDrop :: forall x. Iso (->) [x] [x]
+isoDrop = Iso (drop 1) (drop 1)
+
+--------------------------------------------------------------------------------
+
+labeled :: String -> Laws -> [(PropertyName, Property)]
+labeled prefix ls = [(fromString (prefix <> " " <> n), p) | (n, p) <- lawsProperties ls]
+
+tests :: IO Bool
+tests =
+  checkSequential $
+    Group "Rank-2 functor laws" $
+      concat
+        [ labeled "H1 [] bmap1" (bmap1Laws genH1 reverse (drop 1)),
+          labeled "H2 [] [] bmap1" (bmap1Laws genH2 reverse (drop 1)),
+          labeled "H2 [] [] bmap2" (bmap2Laws genH2 reverse (drop 1)),
+          labeled "H3 [] [] [] bmap1" (bmap1Laws genH3 reverse (drop 1)),
+          labeled "H3 [] [] [] bmap2" (bmap2Laws genH3 reverse (drop 1)),
+          labeled "H3 [] [] [] bmap3" (bmap3Laws genH3 reverse (drop 1)),
+          labeled "Consumer [] bmap1 (contravariant)" (bmap1Laws genConsumer opReverse opDrop),
+          labeled "Endo1 [] bmap1 (invariant)" (bmap1Laws genEndo1 isoReverse isoDrop)
+        ]