diff --git a/connections.cabal b/connections.cabal
--- a/connections.cabal
+++ b/connections.cabal
@@ -1,6 +1,6 @@
 name:                connections
-version:             0.0.2.1
-synopsis:            Partial orders & Galois connections.
+version:             0.0.2.2
+synopsis:            Partial orders, lattices, & Galois connections.
 description:         A library for precision rounding using Galois connections.
 homepage:            https://github.com/cmk/connections
 license:             BSD3
@@ -29,9 +29,9 @@
 
   build-depends:       
       base              >= 4.10  && < 5.0
+    , lawz              >= 0.0.1 && < 1.0
     , containers        >= 0.4.0 && < 0.7
     , semigroupoids     == 5.*
-    , property          >= 0.0.1 && < 1.0
 
   default-extensions:
       ScopedTypeVariables
diff --git a/src/Data/Connection.hs b/src/Data/Connection.hs
--- a/src/Data/Connection.hs
+++ b/src/Data/Connection.hs
@@ -182,7 +182,7 @@
 --  'Trip'
 ---------------------------------------------------------------------
 
--- | An adforkedt triple.
+-- | An adjoint triple.
 --
 -- @'Trip' f g h@ satisfies:
 --
@@ -190,7 +190,7 @@
 -- ⊥   ⊥
 -- g ⊣ h
 --
--- See <https://ncatlab.org/nlab/show/adforkedt+triple>
+-- See <https://ncatlab.org/nlab/show/adjoint+triple>
 --
 data Trip a b = Trip (a -> b) (b -> a) (a -> b)
 
diff --git a/src/Data/Connection/Float.hs b/src/Data/Connection/Float.hs
--- a/src/Data/Connection/Float.hs
+++ b/src/Data/Connection/Float.hs
@@ -74,16 +74,17 @@
 abs' :: (Eq a, Bound a, Num a) => a -> a
 abs' x = if x == minimal then abs (x+1) else abs x
 
-f32i64 :: Conn Float (Nan Int64)
-f32i64 = Conn (liftNan f) (nan (0/0) g) where
+--TODO f32i64?
+f32i32 :: Conn Float (Nan Int32)
+f32i32 = Conn (liftNan f) (nan (0/0) g) where
   f x | abs x <~ 2**24-1 = ceiling x
       | otherwise = if x >~ 0 then 2^24 else minimal
 
   g i | abs' i <~ 2^24-1 = fromIntegral i
       | otherwise = if i >~ 0 then 1/0 else -2**24
   
-i64f32 :: Conn (Nan Int64) Float
-i64f32 = Conn (nan (0/0) f) (liftNan g) where
+i32f32 :: Conn (Nan Int32) Float
+i32f32 = Conn (nan (0/0) f) (liftNan g) where
   f i | abs i <~ 2^24-1 = fromIntegral i
       | otherwise = if i >~ 0 then 2**24 else -1/0
 
diff --git a/src/Data/Connection/Property.hs b/src/Data/Connection/Property.hs
--- a/src/Data/Connection/Property.hs
+++ b/src/Data/Connection/Property.hs
@@ -6,11 +6,11 @@
 import Data.Prd
 import Data.Connection
 
-import qualified Test.Property.Function.Idempotent as Prop
-import qualified Test.Property.Function.Invertible as Prop
-import qualified Test.Property.Function.Monotone   as Prop
+import qualified Test.Function.Idempotent as Prop
+import qualified Test.Function.Invertible as Prop
+import qualified Test.Function.Monotone   as Prop
 
-import Test.Property.Util
+import Test.Util
 import Prelude hiding (Ord(..))
 
 
diff --git a/src/Data/Connection/Yoneda.hs b/src/Data/Connection/Yoneda.hs
--- a/src/Data/Connection/Yoneda.hs
+++ b/src/Data/Connection/Yoneda.hs
@@ -25,13 +25,15 @@
 import GHC.Num (subtract)
 import Numeric.Natural
 import Data.Bool
-import Prelude hiding (Enum(..), Ord(..), until)
+import Prelude hiding (Enum(..), Ord(..), until, filter)
 
 import qualified Control.Category as C
 
 
 type family Rep a :: *
 
+type instance Rep (Down a) = Down (Rep a)
+type instance Rep Bool = Bool
 
 -- | Yoneda representation for lattice ideals & filters.
 --
@@ -47,51 +49,47 @@
 --
 -- /Rep a/ is upward-closed:
 --
--- * @upper x s && x <~ y ==> upper y s@
+-- * @'upper' x s && x '<~' y ==> 'upper' y s@
 --
--- * @upper x s && upper y s ==> connl filter x /\ connl filter y >~ s@
+-- * @'upper' x s && 'upper' y s ==> 'connl' 'filter' x '/\' 'connl' 'filter' y '>~' s@
 --
 -- /Rep a/ is downward-closed:
 --
--- * @lower x s && x >~ y ==> lower y s@
+-- * @'lower' x s && x '>~' y ==> 'lower' y s@
 --
--- * @lower x s && lower y s ==> connl ideal x \/ connl ideal y ~< s@
+-- * @'lower' x s && 'lower' y s ==> 'connl' 'ideal' x '\/' 'connl' 'ideal' y '~<' s@
 --
 -- Finally /filter >>> ideal/ and /ideal >>> filter/ are both connections
 -- on /a/ and /Rep a/ respectively.
 --
--- See also:
+-- See:
 --
 -- * <https://en.wikipedia.org/wiki/Filter_(mathematics)>
 -- * <https://en.wikipedia.org/wiki/Ideal_(order_theory)>
 --
 class (Prd a, Lattice (Rep a)) => Yoneda a where
 
-    -- Principal ideal generated by an element of /a/.
-    ideal :: Conn (Rep a) a
+  -- | Principal ideal generated by an element of /a/.
+  ideal :: Conn (Rep a) a
 
-    lower :: Rep a -> a -> Bool
+  -- | Lower set in /a/ generated by an element in /Rep a/.
+  lower :: Rep a -> a -> Bool
 
-    -- Principal filter generated by an element of /a/.
-    filter :: Conn a (Rep a)
+  -- | Principal filter generated by an element of /a/.
+  filter :: Conn a (Rep a)
 
-    upper :: Rep a -> a -> Bool
+  -- | Upper set in /a/ generated by an element in /Rep a/.
+  upper :: Rep a -> a -> Bool
 
-type instance Rep (Down a) = Down (Rep a)
-type instance Rep Bool = Bool
 
-instance Yoneda Bool where
-    ideal = C.id
-    lower = (>~)
-    filter = C.id
-    upper = (<~)
-
-{-
-
-incBy :: Yoneda a => Quantale (Rep a) => Rep a -> a -> a
-incBy x = connl filter . (x<>) . connr filter
-
-decBy :: Yoneda a => Quantale (Rep a) => Rep a -> a -> a
-decBy x = connl filter . (x\\) . connr filter
+instance Yoneda a => Yoneda (Down a) where
+  ideal = dual filter
+  lower (Down r) (Down a) = upper @a r a
+  filter = dual ideal
+  upper (Down r) (Down a) = lower @a r a
 
--}
+instance Yoneda Bool where
+  ideal = C.id
+  lower = (>~)
+  filter = C.id
+  upper = (<~)
diff --git a/src/Data/Prd.hs b/src/Data/Prd.hs
--- a/src/Data/Prd.hs
+++ b/src/Data/Prd.hs
@@ -98,7 +98,7 @@
   --
   -- If /a/ implements 'Eq' then (ideally) @x =~ y = x == y@.
   --
-  (=~) :: Prd a => a -> a -> Bool
+  (=~) :: a -> a -> Bool
   x =~ y = x <~ y && x >~ y
 
   -- | Comparability relation on /a/. 
@@ -109,7 +109,7 @@
   --
   -- If /a/ implements 'Ord' then (ideally) @x ?~ y = True@.
   --
-  (?~) :: Prd a => a -> a -> Bool
+  (?~) :: a -> a -> Bool
   x ?~ y = x <~ y || x >~ y
 
   -- | Partial version of 'Data.Ord.compare'.
@@ -136,11 +136,10 @@
 (/~) :: Eq a => Prd a => a -> a -> Bool
 x /~ y = not $ x ~~ y
 
-
 -- | Version of 'pcompare' that uses the derived equivalence relation.
 --
 -- This can be useful if there is no 'Eq' instance or if it is
--- compromised, for example when /a/ is a floating point number.
+-- suspect, for example when /a/ is a floating point number.
 --
 pcomparePrd :: Prd a => a -> a -> Maybe Ordering
 pcomparePrd x y 
@@ -271,7 +270,7 @@
 
 -- | A partial version of 'Data.Ord.max'. 
 --
--- Default instance returns the connr argument in the case of equality.
+-- Returns the right argument in the case of equality.
 --
 pmax :: Eq a => Prd a => a -> a -> Maybe a
 pmax x y = do
@@ -286,7 +285,7 @@
 
 -- | A partial version of 'Data.Ord.min'. 
 --
--- Default instance returns the connr argument in the case of equality.
+-- Returns the right argument in the case of equality.
 --
 pmin :: Eq a => Prd a => a -> a -> Maybe a
 pmin x y = do
diff --git a/src/Data/Prd/Property.hs b/src/Data/Prd/Property.hs
--- a/src/Data/Prd/Property.hs
+++ b/src/Data/Prd/Property.hs
@@ -27,11 +27,11 @@
 
 import Data.Prd
 import Data.Prd.Lattice
-import Test.Property.Util
+import Test.Util
 import Prelude hiding (Ord(..))
 
 import qualified Prelude as P
-import qualified Test.Property.Relation as R
+import qualified Test.Relation as R
 
 -- | \( \forall a, b: (a \eq b) \Leftrightarrow (b \eq a) \)
 --
diff --git a/test/Test/Data/Float.hs b/test/Test/Data/Float.hs
--- a/test/Test/Data/Float.hs
+++ b/test/Test/Data/Float.hs
@@ -6,14 +6,11 @@
 import Data.Word
 import Data.Float
 import Data.Prd
-import Data.Semiring
 import Data.Connection
-import Data.Connection.Filter
+--import Data.Connection.Filter
 import Data.Connection.Float
-import Data.Semigroup.Quantale
 
 import qualified Data.Prd.Property as Prop
-import qualified Data.Semiring.Property as Prop
 import qualified Data.Connection.Property as Prop
 
 import Hedgehog
@@ -33,7 +30,7 @@
 gen_flt32 = G.float rf
 
 gen_nan :: Gen a -> Gen (Nan a)
-gen_nan gen = G.frequency [(9, Def <$> gen), (1, pure NaN)]
+gen_nan gen = G.frequency [(9, Def <$> gen), (1, pure Nan)]
 
 prop_prd_ulp32 :: Property
 prop_prd_ulp32 = withTests 1000 . property $ do
@@ -51,7 +48,7 @@
   assert $ Prop.transitive_eq x y z
 
 prop_prd_flt32 :: Property
-prop_prd_flt32 = withTests 100000 . property $ do
+prop_prd_flt32 = withTests 1000 . property $ do
   x <- forAll gen_flt32'
   y <- forAll gen_flt32'
   z <- forAll gen_flt32'
@@ -77,7 +74,6 @@
 
   assert $ Prop.neutral_addition' x
   assert $ Prop.associative_addition (abs x) (abs y) (abs z)
--}
 
 prop_connections_flt32_wrd64 :: Property
 prop_connections_flt32_wrd64 = withTests 1000 . property $ do
@@ -94,7 +90,7 @@
   ezw <- forAll $ G.element [Left z, Right w]
   ezw' <- forAll $ G.element [Left z', Right w']
 
-  assert $ Prop.closed (idx @Float) x
+  assert $ Prop.closed (idx @Float) x --TODO in Index.hs
   assert $ Prop.kernel (idx @Float) z
   assert $ Prop.monotone' (idx @Float) x x'
   assert $ Prop.monotone (idx @Float) z z'
@@ -111,6 +107,7 @@
   assert $ Prop.monotone' (idx @(Either Float Float)) exy exy'
   assert $ Prop.monotone (idx @(Either Float Float)) ezw ezw'
   assert $ Prop.connection (idx @(Either Float Float)) exy ezw
+-}
 
 prop_connections_flt32_ulp32 :: Property
 prop_connections_flt32_ulp32 = withTests 1000 . property $ do
@@ -141,44 +138,20 @@
   x' <- forAll gen_flt32'
   y' <- forAll (gen_nan $ G.integral ri)
  
-  assert $ Prop.connection f32i64 x y
-  assert $ Prop.connection i64f32 y x
-
-  assert $ Prop.monotone' f32i64 x x'
-  assert $ Prop.monotone' i64f32 y y'
-
-  assert $ Prop.monotone f32i64 y y'
-  assert $ Prop.monotone i64f32 x x'
-
-  assert $ Prop.closed f32i64 x
-  assert $ Prop.closed i64f32 y
-
-  assert $ Prop.kernel i64f32 x
-  assert $ Prop.kernel f32i64 y
-
-
-prop_quantale_flt32 :: Property
-prop_quantale_flt32 = withTests 1000 . withShrinks 0 $ property $ do
-  x <- forAll gen_flt32 -- we do not require `residr pInf` etc
-  y <- forAll gen_flt32'
-  z <- forAll gen_flt32'
-
-  assert $ Prop.connection (residl x) y z
-  assert $ Prop.connection (residr x) y z
-
-  assert $ Prop.monotone' (residl x) y z
-  assert $ Prop.monotone' (residr x) y z
+  assert $ Prop.connection f32i32 x y
+  assert $ Prop.connection i32f32 y x
 
-  assert $ Prop.monotone (residl x) y z
-  assert $ Prop.monotone (residr x) y z
+  assert $ Prop.monotone' f32i32 x x'
+  assert $ Prop.monotone' i32f32 y y'
 
-  assert $ Prop.closed (residl x) y
-  assert $ Prop.closed (residr x) y
+  assert $ Prop.monotone f32i32 y y'
+  assert $ Prop.monotone i32f32 x x'
 
-  assert $ Prop.kernel (residl x) y
-  assert $ Prop.kernel (residr x) y
+  assert $ Prop.closed f32i32 x
+  assert $ Prop.closed i32f32 y
 
-  assert $ residuated x y z
+  assert $ Prop.kernel i32f32 x
+  assert $ Prop.kernel f32i32 y
 
 tests :: IO Bool
 tests = checkParallel $$(discover)
diff --git a/test/test.hs b/test/test.hs
--- a/test/test.hs
+++ b/test/test.hs
@@ -4,13 +4,12 @@
 
 
 import qualified Test.Data.Float as F
-import qualified Test.Data.Dioid.Signed as S
 import qualified Test.Data.Connection.Int as CI
 import qualified Test.Data.Connection.Word as CW
 
 
 tests :: IO [Bool]
-tests = sequence [S.tests] -- [CI.tests, CW.tests, F.tests] 
+tests = sequence [CI.tests, CW.tests, F.tests] 
 
 main :: IO ()
 main = do