diff --git a/connections.cabal b/connections.cabal
--- a/connections.cabal
+++ b/connections.cabal
@@ -1,7 +1,7 @@
 name:                connections
-version:             0.2.0
+version:             0.3.0
 synopsis:            Orders, Galois connections, and lattices.
-description:         A library for order manipulation using Galois connections.
+description:         A library for order manipulation using Galois connections. See the README for a brief overview.
 homepage:            https://github.com/cmk/connections
 license:             BSD3
 license-file:        LICENSE
@@ -22,10 +22,11 @@
       Data.Connection
     , Data.Connection.Conn
     , Data.Connection.Class
+    , Data.Connection.Fixed
+    , Data.Connection.Float
     , Data.Connection.Int
-    , Data.Connection.Word
     , Data.Connection.Ratio
-    , Data.Connection.Float
+    , Data.Connection.Word
     , Data.Connection.Property
 
     , Data.Lattice
@@ -49,6 +50,7 @@
     , Test.Data.Connection
     , Test.Data.Connection.Int
     , Test.Data.Connection.Word
+    , Test.Data.Connection.Fixed
     , Test.Data.Connection.Float
     , Test.Data.Connection.Ratio
   build-depends:       
diff --git a/src/Data/Connection/Class.hs b/src/Data/Connection/Class.hs
--- a/src/Data/Connection/Class.hs
+++ b/src/Data/Connection/Class.hs
@@ -2,6 +2,7 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE RankNTypes #-}
@@ -11,71 +12,36 @@
 {-# LANGUAGE ViewPatterns #-}
 
 module Data.Connection.Class (
-    -- * Conn
-    Conn (),
-    identity,
-
-    -- * Connection k
+    -- * Types
+    Left,
+    left,
+    Right,
+    right,
     Triple,
-    pattern Conn,
-    ConnK,
-    embed,
-    extremal,
+
+    -- * Lattices
+    (\/),
+    (/\),
     lub,
     glb,
-    half,
-    midpoint,
-    range,
-    round,
-    round1,
-    round2,
-    truncate,
-    truncate1,
-    truncate2,
-
-    -- * Connection L
-    Left,
-    pattern ConnL,
-    ConnL,
-    connL,
-    embedL,
+    choose,
+    divide,
     minimal,
-    join,
-    ceiling,
-    ceiling1,
-    ceiling2,
-
-    -- * Connection R
-    Right,
-    pattern ConnR,
-    ConnR,
-    connR,
-    embedR,
     maximal,
-    meet,
-    floor,
-    floor1,
-    floor2,
-
-    -- * Combinators
-    (>>>),
-    (<<<),
-    (/|\),
-    (\|/),
-    choice,
-    strong,
+    extremal,
 
     -- * Connection
-    Kan (..),
+    Connection (..),
+
+    -- ** RebindableSyntax
     ConnInteger,
     ConnRational,
-    ConnExtended,
-    Connection (..),
 ) where
 
 import safe Control.Category ((>>>))
 import safe Data.Bool (bool)
 import safe Data.Connection.Conn
+import safe Data.Connection.Fixed
 import safe Data.Connection.Float
 import safe Data.Connection.Int
 import safe Data.Connection.Ratio
@@ -102,8 +68,18 @@
 
 type Left = Connection 'L
 
+-- | A specialization of /conn/ to left-side connections.
+--
+left :: Left a b => ConnL a b
+left = conn @ 'L
+
 type Right = Connection 'R
 
+-- | A specialization of /conn/ to right-side connections.
+--
+right :: Right a b => ConnR a b
+right = conn @ 'R
+
 -- | A constraint kind representing an <https://ncatlab.org/nlab/show/adjoint+triple adjoint triple> of Galois connections.
 type Triple a b = (Left a b, Right a b)
 
@@ -111,18 +87,16 @@
 --
 --  Usable in conjunction with /RebindableSyntax/:
 --
---  > fromInteger = embedL . Just :: ConnInteger a => Integer -> a
+--  > fromInteger = upper conn . Just :: ConnInteger a => Integer -> a
 type ConnInteger a = Left a (Maybe Integer)
 
 -- | A constraint kind for 'Rational' conversions.
 --
 -- Usable in conjunction with /RebindableSyntax/:
 --
---  > fromRational = round :: ConnRational a => Rational -> a
+--  > fromRational = round conn :: ConnRational a => Rational -> a
 type ConnRational a = Triple Rational a
 
-type ConnExtended a b = Triple a (Extended b)
-
 -- | An < https://ncatlab.org/nlab/show/adjoint+string adjoint string > of Galois connections of length 2 or 3.
 class (Preorder a, Preorder b) => Connection k a b where
     -- |
@@ -133,64 +107,7 @@
     -- (3.1415925,3.1415927)
     conn :: Conn k a b
 
-infixr 3 \|/
-
--- | A preorder variant of 'Control.Arrow.|||'.
-(\|/) :: Conn k c a -> Conn k c b -> Conn k c (Either a b)
-f \|/ g = Conn Left (either id id) Right >>> f `choice` g
-
-infixr 4 /|\
-
--- | A preorder variant of 'Control.Arrow.&&&'.
-(/|\) :: Connection k (c, c) c => Conn k a c -> Conn k b c -> Conn k (a, b) c
-f /|\ g = f `strong` g >>> conn
-
----------------------------------------------------------------------
--- Connection k
----------------------------------------------------------------------
-
--- | The canonical connections against a 'Bool'.
-extremal :: Triple () a => Conn k a Bool
-extremal = Conn f g h
-  where
-    g False = minimal
-    g True = maximal
-
-    f i
-        | i ~~ minimal = False
-        | otherwise = True
-
-    h i
-        | i ~~ maximal = True
-        | otherwise = False
-
--- | Least upper bound operator.
---
--- The order dual of 'glb'.
---
--- >>> lub 1.0 9.0 7.0
--- 7.0
--- >>> lub 1.0 9.0 (0.0 / 0.0)
--- 1.0
-lub :: Triple (a, a) a => a -> a -> a -> a
-lub x y z = (x `meet` y) `join` (y `meet` z) `join` (z `meet` x)
-
--- | Greatest lower bound operator.
---
--- > glb x x y = x
--- > glb x y z = glb z x y
--- > glb x y z = glb x z y
--- > glb (glb x w y) w z = glb x w (glb y w z)
---
--- >>> glb 1.0 9.0 7.0
--- 7.0
--- >>> glb 1.0 9.0 (0.0 / 0.0)
--- 9.0
--- >>> glb (fromList [1..3]) (fromList [3..5]) (fromList [5..7]) :: Set Int
--- fromList [3,5]
-glb :: Triple (a, a) a => a -> a -> a -> a
-glb x y z = (x `join` y) `meet` (y `join` z) `meet` (z `join` x)
-
+{-
 -- | Return the nearest value to x.
 --
 -- > round @a @a = id
@@ -205,8 +122,8 @@
     Just LT -> floor x
     _ -> truncate x
   where
-    halfR = x - lower (connR @a @b) x -- dist from lower bound
-    halfL = upper (connL @a @b) x - x -- dist from upper bound
+    halfR = x - right (connR @a @b) x -- dist from lower bound
+    halfL = left (connL @a @b) x - x -- dist from upper bound
 
 -- | Lift a unary function over a 'Conn'.
 --
@@ -255,112 +172,103 @@
 truncate2 :: (Num a, Triple a b) => (a -> a -> a) -> b -> b -> b
 truncate2 f x y = truncate $ f (g x) (g y) where Conn _ g _ = connL
 {-# INLINE truncate2 #-}
+-}
 
 ---------------------------------------------------------------------
--- Connection L
+-- Lattices
 ---------------------------------------------------------------------
 
--- | A specialization of /conn/ to left-side connections.
---
--- This is a convenience function provided primarily to avoid needing
--- to enable /DataKinds/.
-connL :: Left a b => ConnL a b
-connL = conn @ 'L
-
--- | Extract the center of a 'Conn' or upper half of a 'ConnL'.
-embedL :: Left a b => b -> a
-embedL = embed connL
+infixr 5 \/
 
--- | A minimal element of a preorder.
---
--- 'minimal' needn't be unique, but it must obey:
+-- | Lattice join.
 --
--- > x <~ minimal => x ~~ minimal
-minimal :: Left () a => a
-minimal = ceiling ()
+-- > (\/) = curry $ lower semilattice
+(\/) :: Left (a, a) a => a -> a -> a
+(\/) = join conn
 
-infixr 5 `join`
+infixr 6 /\ -- comment for the parser
 
--- | Semigroup operation on a join-lattice.
-join :: Left (a, a) a => a -> a -> a
-join = curry ceiling
+-- | Lattice meet.
+--
+-- > (/\) = curry $ floor semilattice
+(/\) :: Right (a, a) a => a -> a -> a
+(/\) = meet conn
 
--- | Extract the ceiling of a 'Conn' or lower half of a 'ConnL'.
+-- | Least upper bound operator.
 --
--- > ceiling @a @a = id
--- > ceiling (x1 `join` a2) = ceiling x1 `join` ceiling x2
+-- The order dual of 'glb'.
 --
--- The latter law is the adjoint functor theorem for preorders.
+-- >>> lub 1.0 9.0 7.0
+-- 7.0
+-- >>> lub 1.0 9.0 (0.0 / 0.0)
+-- 1.0
+lub :: Triple (a, a) a => a -> a -> a -> a
+lub x y z = x /\ y \/ y /\ z \/ z /\ x
+
+-- | Greatest lower bound operator.
 --
--- >>> Data.Connection.ceiling @Rational @Float (0 :% 0)
--- NaN
--- >>> Data.Connection.ceiling @Rational @Float (1 :% 0)
--- Infinity
--- >>> Data.Connection.ceiling @Rational @Float (13 :% 10)
--- 1.3000001
-ceiling :: Left a b => a -> b
-ceiling = ceilingWith conn
+-- > glb x x y = x
+-- > glb x y z = glb z x y
+-- > glb x y z = glb x z y
+-- > glb (glb x w y) w z = glb x w (glb y w z)
+--
+-- >>> glb 1.0 9.0 7.0
+-- 7.0
+-- >>> glb 1.0 9.0 (0.0 / 0.0)
+-- 9.0
+-- >>> glb (fromList [1..3]) (fromList [3..5]) (fromList [5..7]) :: Set Int
+-- fromList [3,5]
+glb :: Triple (a, a) a => a -> a -> a -> a
+glb x y z = (x \/ y) /\ (y \/ z) /\ (z \/ x)
 
--- | Lift a unary function over a 'ConnL'.
-ceiling1 :: Left a b => (a -> a) -> b -> b
-ceiling1 = ceilingWith1 conn
+infixr 3 `choose`
 
--- | Lift a binary function over a 'ConnL'.
-ceiling2 :: Left a b => (a -> a -> a) -> b -> b -> b
-ceiling2 = ceilingWith2 conn
+-- | A preorder variant of 'Control.Arrow.|||'.
+choose :: Conn k c a -> Conn k c b -> Conn k c (Either a b)
+choose f g = Conn Left (either id id) Right >>> f `choice` g
 
----------------------------------------------------------------------
--- Connection R
----------------------------------------------------------------------
+infixr 4 `divide`
 
--- | A specialization of /conn/ to right-side connections.
---
--- This is a convenience function provided primarily to avoid needing
--- to enable /DataKinds/.
-connR :: Right a b => ConnR a b
-connR = conn @ 'R
+-- | A preorder variant of 'Control.Arrow.&&&'.
+divide :: Connection k (c, c) c => Conn k a c -> Conn k b c -> Conn k (a, b) c
+divide f g = f `strong` g >>> conn
 
--- | Extract the center of a 'ConnK' or lower half of a 'ConnR'.
-embedR :: Right a b => b -> a
-embedR = embed connR
+-- | A minimal element of a preorder.
+--
+-- > x /\ minimal = minimal
+-- > x \/ minimal = x
+--
+-- 'minimal' needn't be unique, but it must obey:
+--
+-- > x <~ minimal => x ~~ minimal
+minimal :: Left () a => a
+minimal = ceiling conn ()
 
 -- | A maximal element of a preorder.
 --
+-- > x /\ maximal = x
+-- > x \/ maximal = maximal
+--
 -- 'maximal' needn't be unique, but it must obey:
 --
 -- > x >~ maximal => x ~~ maximal
 maximal :: Right () a => a
-maximal = floor ()
-
-infixr 6 `meet`
-
--- | Semigroup operation on a meet-lattice.
-meet :: Right (a, a) a => a -> a -> a
-meet = curry floor
+maximal = floor conn ()
 
--- | Extract the floor of a 'ConnK' or upper half of a 'ConnL'.
---
--- > floor @a @a = id
--- > floor (x1 `meet` x2) = floor x1 `meet` floor x2
---
--- The latter law is the adjoint functor theorem for preorders.
---
--- >>> Data.Connection.floor @Rational @Float (0 :% 0)
--- NaN
--- >>> Data.Connection.floor @Rational @Float (1 :% 0)
--- Infinity
--- >>> Data.Connection.floor @Rational @Float (13 :% 10)
--- 1.3
-floor :: Right a b => a -> b
-floor = floorWith conn
+-- | The canonical connection with a 'Bool'.
+extremal :: Triple () a => Conn k a Bool
+extremal = Conn f g h
+  where
+    g False = minimal
+    g True = maximal
 
--- | Lift a unary function over a 'ConnR'.
-floor1 :: Right a b => (a -> a) -> b -> b
-floor1 = floorWith1 conn
+    f i
+        | i ~~ minimal = False
+        | otherwise = True
 
--- | Lift a binary function over a 'ConnR'.
-floor2 :: Right a b => (a -> a -> a) -> b -> b -> b
-floor2 = floorWith2 conn
+    h i
+        | i ~~ maximal = True
+        | otherwise = False
 
 ---------------------------------------------------------------------
 -- Instances
@@ -466,6 +374,35 @@
     conn = Conn (const $ -1 :% 0) (const ()) (const $ 1 :% 0)
 instance Connection k (Rational, Rational) Rational where conn = latticeN5
 
+instance Connection k Deci Uni where conn = f01f00
+instance Connection k Centi Uni where conn = f02f00
+instance Connection k Milli Uni where conn = f03f00
+instance Connection k Micro Uni where conn = f06f00
+instance Connection k Nano Uni where conn = f09f00
+instance Connection k Pico Uni where conn = f12f00
+
+instance Connection k Centi Deci where conn = f02f01
+instance Connection k Milli Deci where conn = f03f01
+instance Connection k Micro Deci where conn = f06f01
+instance Connection k Nano Deci where conn = f09f01
+instance Connection k Pico Deci where conn = f12f01
+
+instance Connection k Milli Centi where conn = f03f02
+instance Connection k Micro Centi where conn = f06f02
+instance Connection k Nano Centi where conn = f09f02
+instance Connection k Pico Centi where conn = f12f02
+
+instance Connection k Micro Milli where conn = f06f03
+instance Connection k Nano Milli where conn = f09f03
+instance Connection k Pico Milli where conn = f12f03
+
+instance Connection k Nano Micro where conn = f09f06
+instance Connection k Pico Micro where conn = f12f06
+
+instance Connection k Pico Nano where conn = f12f09
+
+instance Connection k (Fixed e, Fixed e) (Fixed e) where conn = latticeOrd
+
 instance Connection k () Float where conn = extremalN5
 instance Connection k Double Float where conn = f64f32
 instance Connection k Rational Float where conn = ratf32
@@ -510,28 +447,51 @@
 instance Connection 'L Int32 (Maybe Integer) where conn = i32int
 instance Connection 'L Int64 (Maybe Integer) where conn = i64int
 instance Connection 'L Int (Maybe Integer) where conn = ixxint
-
-{-
 instance Connection 'L Integer (Maybe Integer) where
-  -- | Provided as a shim for /RebindableSyntax/.
-  -- Note that this instance will clip negative numbers to zero.
-conn = swapR $ intnat >>> natint
--}
+    conn = c1 >>> intnat >>> natint >>> c2
+      where
+        c1 = Conn shiftR shiftL shiftR
+        c2 = Conn (fmap shiftL) (fmap shiftR) (fmap shiftL)
 
+        shiftR x = x + m
+        shiftL x = x - m
+        m = 9223372036854775808
+
 instance Connection k Rational (Extended Int8) where conn = rati08
 instance Connection k Rational (Extended Int16) where conn = rati16
 instance Connection k Rational (Extended Int32) where conn = rati32
 instance Connection k Rational (Extended Int64) where conn = rati64
 instance Connection k Rational (Extended Int) where conn = ratixx
 instance Connection k Rational (Extended Integer) where conn = ratint
+instance HasResolution prec => Connection k Rational (Extended (Fixed prec)) where conn = ratfix
 
--- | All 'Data.Int.Int08' values are exactly representable in a 'Float'.
+instance Connection 'L Float (Extended Word8) where conn = f32i08 >>> mapped i08w08
+instance Connection 'L Float (Extended Word16) where conn = f32i16 >>> mapped i16w16
+instance Connection 'L Float (Extended Word32) where conn = f32i32 >>> mapped i32w32
+instance Connection 'L Float (Extended Word64) where conn = f32i64 >>> mapped i64w64
+instance Connection 'L Float (Extended Word) where conn = f32ixx >>> mapped ixxwxx
+instance Connection 'L Float (Extended Natural) where conn = f32int >>> mapped intnat
+
+-- | All 'Data.Int.Int8' values are exactly representable in a 'Float'.
 instance Connection k Float (Extended Int8) where conn = f32i08
 
 -- | All 'Data.Int.Int16' values are exactly representable in a 'Float'.
 instance Connection k Float (Extended Int16) where conn = f32i16
 
--- | All 'Data.Int.Int08' values are exactly representable in a 'Double'.
+instance Connection 'L Float (Extended Int32) where conn = f32i32
+instance Connection 'L Float (Extended Int64) where conn = f32i64
+instance Connection 'L Float (Extended Int) where conn = f32ixx
+instance Connection 'L Float (Extended Integer) where conn = f32int
+instance HasResolution res => Connection 'L Float (Extended (Fixed res)) where conn = connL ratf32 >>> ratfix
+
+instance Connection 'L Double (Extended Word8) where conn = f64i08 >>> mapped i08w08
+instance Connection 'L Double (Extended Word16) where conn = f64i16 >>> mapped i16w16
+instance Connection 'L Double (Extended Word32) where conn = f64i32 >>> mapped i32w32
+instance Connection 'L Double (Extended Word64) where conn = f64i64 >>> mapped i64w64
+instance Connection 'L Double (Extended Word) where conn = f64ixx >>> mapped ixxwxx
+instance Connection 'L Double (Extended Natural) where conn = f64int >>> mapped intnat
+
+-- | All 'Data.Int.Int8' values are exactly representable in a 'Double'.
 instance Connection k Double (Extended Int8) where conn = f64i08
 
 -- | All 'Data.Int.Int16' values are exactly representable in a 'Double'.
@@ -540,6 +500,11 @@
 -- | All 'Data.Int.Int32' values are exactly representable in a 'Double'.
 instance Connection k Double (Extended Int32) where conn = f64i32
 
+instance Connection 'L Double (Extended Int64) where conn = f64i64
+instance Connection 'L Double (Extended Int) where conn = f64ixx
+instance Connection 'L Double (Extended Integer) where conn = f64int
+instance HasResolution res => Connection 'L Double (Extended (Fixed res)) where conn = connL ratf64 >>> ratfix
+
 instance Connection k a b => Connection k (Identity a) b where
     conn = Conn runIdentity Identity runIdentity >>> conn
 
@@ -586,19 +551,19 @@
     conn = ConnL (const Map.empty) (const ())
 
 instance (Total a, Left (b, b) b) => Connection 'L (Map.Map a b, Map.Map a b) (Map.Map a b) where
-    conn = ConnL (uncurry $ Map.unionWith join) fork
+    conn = ConnL (uncurry $ Map.unionWith (join conn)) fork
 
 instance (Total a, Right (b, b) b) => Connection 'R (Map.Map a b, Map.Map a b) (Map.Map a b) where
-    conn = ConnR fork (uncurry $ Map.intersectionWith meet)
+    conn = ConnR fork (uncurry $ Map.intersectionWith (meet conn))
 
 instance Preorder a => Connection 'L () (IntMap.IntMap a) where
     conn = ConnL (const IntMap.empty) (const ())
 
 instance Left (a, a) a => Connection 'L (IntMap.IntMap a, IntMap.IntMap a) (IntMap.IntMap a) where
-    conn = ConnL (uncurry $ IntMap.unionWith join) fork
+    conn = ConnL (uncurry $ IntMap.unionWith (join conn)) fork
 
 instance Right (a, a) a => Connection 'R (IntMap.IntMap a, IntMap.IntMap a) (IntMap.IntMap a) where
-    conn = ConnR fork (uncurry $ IntMap.intersectionWith meet)
+    conn = ConnR fork (uncurry $ IntMap.intersectionWith (meet conn))
 
 -- Internal
 
@@ -666,7 +631,7 @@
 joinMaybe _ u@(Just _) = u
 joinMaybe Nothing Nothing = Nothing
 
-meetMaybe :: Connection 'R (a, a) a => Maybe a -> Maybe a -> Maybe a
+meetMaybe :: Right (a, a) a => Maybe a -> Maybe a -> Maybe a
 meetMaybe Nothing Nothing = Nothing
 meetMaybe Nothing _ = Nothing
 meetMaybe _ Nothing = Nothing
@@ -679,7 +644,7 @@
 joinExtended Bottom       y            = y
 joinExtended x            Bottom       = x
 
-meetExtended :: Connection 'R (a, a) a => Extended a -> Extended a -> Extended a
+meetExtended :: Right (a, a) a => Extended a -> Extended a -> Extended a
 meetExtended Top          y            = y
 meetExtended x            Top          = x
 meetExtended (Extended x) (Extended y) = Extended (x `meet` y)
@@ -692,7 +657,7 @@
 joinEither _ u@(Right _) = u
 joinEither (Left x) (Left y) = Left (x `join` y)
 
-meetEither :: (Connection 'R (a, a) a, Connection 'R (b, b) b) => Either a b -> Either a b -> Either a b
+meetEither :: (Right (a, a) a, Right (b, b) b) => Either a b -> Either a b -> Either a b
 meetEither (Left x) (Left y) = Left (x `meet` y)
 meetEither l@(Left _) _ = l
 meetEither _ l@(Left _) = l
@@ -701,6 +666,6 @@
 joinTuple :: (Connection 'L (a, a) a, Connection 'L (b, b) b) => (a, b) -> (a, b) -> (a, b)
 joinTuple (x1, y1) (x2, y2) = (x1 `join` x2, y1 `join` y2)
 
-meetTuple :: (Connection 'R (a, a) a, Connection 'R (b, b) b) => (a, b) -> (a, b) -> (a, b)
+meetTuple :: (Right (a, a) a, Right (b, b) b) => (a, b) -> (a, b) -> (a, b)
 meetTuple (x1, y1) (x2, y2) = (x1 `meet` x2, y1 `meet` y2)
 -}
diff --git a/src/Data/Connection/Conn.hs b/src/Data/Connection/Conn.hs
--- a/src/Data/Connection/Conn.hs
+++ b/src/Data/Connection/Conn.hs
@@ -14,65 +14,66 @@
     -- * Conn
     Kan (..),
     Conn (),
-    pattern Conn,
     embed,
     range,
     identity,
-
-    -- * Connection k
-    ConnK,
-    half,
-    midpoint,
-    roundWith,
-    roundWith1,
-    roundWith2,
-    truncateWith,
-    truncateWith1,
-    truncateWith2,
+    (>>>),
+    (<<<),
+    mapped,
+    choice,
+    strong,
 
     -- * Connection L
     ConnL,
     pattern ConnL,
-    upL,
-    downL,
-    swapL,
-    counit,
+    connL,
     upper,
     upper1,
     upper2,
-    filterWith,
-    ceilingWith,
-    ceilingWith1,
-    ceilingWith2,
+    join,
+    ceiling,
+    ceiling1,
+    ceiling2,
 
     -- * Connection R
     ConnR,
     pattern ConnR,
-    upR,
-    downR,
-    swapR,
-    unit,
+    connR,
     lower,
     lower1,
     lower2,
-    idealWith,
-    floorWith,
-    floorWith1,
-    floorWith2,
+    meet,
+    floor,
+    floor1,
+    floor2,
 
-    -- * Combinators
-    (>>>),
-    (<<<),
-    choice,
-    strong,
+    -- * Connection k
+    pattern Conn,
+    half,
+    midpoint,
+    round,
+    round1,
+    round2,
+    truncate,
+    truncate1,
+    truncate2,
+
+    -- * Down
+    upL,
+    upR,
+    downL,
+    downR,
+    filterL,
+    filterR,
+    Down (..),
 ) where
 
-import safe Control.Arrow
+import safe Control.Arrow ((&&&))
 import safe Control.Category (Category, (<<<), (>>>))
 import safe qualified Control.Category as C
 import safe Data.Bifunctor (bimap)
 import safe Data.Order
-import safe Prelude hiding (Ord (..))
+import safe Prelude hiding (Ord (..), ceiling, floor, round, truncate)
 
 -- $setup
 -- >>> :set -XTypeApplications
@@ -85,322 +86,411 @@
 
 -- | A data kind distinguishing the directionality of a Galois connection:
 --
--- * /L/-tagged types are low / increasing (e.g. 'Data.Connection.Class.minimal', 'Data.Connection.Class.upper', 'Data.Connection.Class.ceiling', 'Data.Connection.Class.join')
+-- * /L/-tagged types are low / increasing (e.g. 'Data.Connection.Class.minimal', 'Data.Connection.Class.ceiling', 'Data.Connection.Class.join')
 --
--- * /R/-tagged types are high / decreasing (e.g. 'Data.Connection.Class.maximal', 'Data.Connection.Class.lower', 'Data.Connection.Class.floor', 'Data.Connection.Class.meet')
+-- * /R/-tagged types are high / decreasing (e.g. 'Data.Connection.Class.maximal', 'Data.Connection.Class.floor', 'Data.Connection.Class.meet')
 data Kan = L | R
 
--- | An < https://ncatlab.org/nlab/show/adjoint+string adjoint string > of Galois connections of length 2 or 3.
+-- | A (chain of) Galois connections.
 --
+-- A [Galois connection](https://en.wikipedia.org/wiki/Galois_connection) between preorders P and Q
+-- is a pair of monotone maps `f :: p -> q` and `g :: q -> p` such that:
+--
+-- > f x <= y iff x <= g y
+--
+-- We say that `f` is the left or right adjoint, and `g` is the right or left adjoint of the connection.
+--
 -- Connections have many nice properties wrt numerical conversion:
 --
 -- >>> range (conn @_ @Rational @Float) (1 :% 8) -- eighths are exactly representable in a float
 -- (0.125,0.125)
 -- >>> range (conn @_ @Rational @Float) (1 :% 7) -- sevenths are not
 -- (0.14285713,0.14285715)
-data Conn (k :: Kan) a b = Galois (a -> (b, b)) (b -> a)
+--
+-- See the /README/ file for a slightly more in-depth introduction.
+data Conn (k :: Kan) a b = Conn_ (a -> (b, b)) (b -> a)
 
 instance Category (Conn k) where
     id = identity
     {-# INLINE id #-}
 
-    Galois f1 g1 . Galois f2 g2 = Galois ((fst . f1) . (fst . f2) &&& (snd . f1) . (snd . f2)) (g2 . g1)
+    Conn_ f1 g1 . Conn_ f2 g2 = Conn_ ((fst . f1) . (fst . f2) &&& (snd . f1) . (snd . f2)) (g2 . g1)
     {-# INLINE (.) #-}
 
--- | Obtain a /Conn/ from an adjoint triple of monotone functions.
---
---  This is a view pattern for an arbitrary 'Conn'. When applied to a 'ConnL'
---  or 'ConnR', the two functions of type @a -> b@ returned will be identical.
---
---  /Caution/: /Conn f g h/ must obey \(f \dashv g \dashv h\). This condition is not checked.
---
---  For detailed properties see 'Data.Connection.Property'.
-pattern Conn :: (a -> b) -> (b -> a) -> (a -> b) -> Conn k a b
-pattern Conn f g h <- (embed &&& _1 &&& _2 -> (g, (h, f))) where Conn f g h = Galois (h &&& f) g
-
-{-# COMPLETE Conn #-}
-
 -- Internal floor function. When \(f \dashv g \dashv h \) this is h.
 _1 :: Conn k a b -> a -> b
-_1 (Galois f _) = fst . f
+_1 (Conn_ f _) = fst . f
 {-# INLINE _1 #-}
 
 -- Internal ceiling function. When \(f \dashv g \dashv h \) this is f.
 _2 :: Conn k a b -> a -> b
-_2 (Galois f _) = snd . f
+_2 (Conn_ f _) = snd . f
 {-# INLINE _2 #-}
 
--- | The identity 'Conn'.
-identity :: Conn k a a
-identity = Galois (id &&& id) id
-{-# INLINE identity #-}
-
--- | Obtain the center of a 'ConnK', upper adjoint of a 'ConnL', or lower adjoint of a 'ConnR'.
+-- | Retrieve the upper adjoint of a 'ConnL', or lower adjoint of a 'ConnR'.
 embed :: Conn k a b -> b -> a
-embed (Galois _ g) = g
+embed (Conn_ _ g) = g
 {-# INLINE embed #-}
 
--- | Obtain the upper and/or lower adjoints of a connection.
+-- | Retrieve the left and/or right adjoints of a connection.
 --
--- > range c = floorWith c &&& ceilingWith c
+-- > range c = floor c &&& ceiling c
 --
 -- >>> range f64f32 pi
 -- (3.1415925,3.1415927)
 -- >>> range f64f32 (0/0)
 -- (NaN,NaN)
 range :: Conn k a b -> a -> (b, b)
-range (Galois f _) = f
+range (Conn_ f _) = f
 {-# INLINE range #-}
 
+-- | The identity 'Conn'.
+identity :: Conn k a a
+identity = Conn_ (id &&& id) id
+{-# INLINE identity #-}
+
+-- | Lift a 'Conn' into a functor.
+--
+-- /Caution/: This function will result in an invalid connection
+-- if the functor alters the internal preorder (i.e. 'Data.Ord.Down').
+mapped :: Functor f => Conn k a b -> Conn k (f a) (f b)
+mapped (Conn f g h) = Conn (fmap f) (fmap g) (fmap h)
+{-# INLINE mapped #-}
+
+-- | Lift two 'Conn's into a 'Conn' on the <https://en.wikibooks.org/wiki/Category_Theory/Categories_of_ordered_sets coproduct order>
+--
+-- > (choice id) (ab >>> cd) = (choice id) ab >>> (choice id) cd
+-- > (flip choice id) (ab >>> cd) = (flip choice id) ab >>> (flip choice id) cd
+choice :: Conn k a b -> Conn k c d -> Conn k (Either a c) (Either b d)
+choice (Conn ab ba ab') (Conn cd dc cd') = Conn f g h
+  where
+    f = either (Left . ab) (Right . cd)
+    g = either (Left . ba) (Right . dc)
+    h = either (Left . ab') (Right . cd')
+{-# INLINE choice #-}
+
+-- | Lift two 'Conn's into a 'Conn' on the <https://en.wikibooks.org/wiki/Order_Theory/Preordered_classes_and_poclasses#product_order product order>
+--
+-- > (strong id) (ab >>> cd) = (strong id) ab >>> (strong id) cd
+-- > (flip strong id) (ab >>> cd) = (flip strong id) ab >>> (flip strong id) cd
+strong :: Conn k a b -> Conn k c d -> Conn k (a, c) (b, d)
+strong (Conn ab ba ab') (Conn cd dc cd') = Conn f g h
+  where
+    f = bimap ab cd
+    g = bimap ba dc
+    h = bimap ab' cd'
+{-# INLINE strong #-}
+
 ---------------------------------------------------------------------
--- ConnK
+-- Conn 'L
 ---------------------------------------------------------------------
 
--- | An <https://ncatlab.org/nlab/show/adjoint+triple adjoint triple> of Galois connections.
+type ConnL = Conn 'L
+
+-- | A <https://ncatlab.org/nlab/show/Galois+connection Galois connection> between two monotone functions.
 --
--- An adjoint triple is a chain of connections of length 3:
+-- A Galois connection between /f/ and /g/, written \(f \dashv g \)
+-- is an adjunction in the category of preorders.
 --
--- \(f \dashv g \dashv h \)
+-- Each side of the connection may be defined in terms of the other:
 --
--- For detailed properties see 'Data.Connection.Property'.
-type ConnK a b = forall k. Conn k a b
-
--- | Determine which half of the interval between 2 representations of /a/ a particular value lies.
+--  \( g(x) = \sup \{y \in E \mid f(y) \leq x \} \)
 --
--- @ 'half' t x = 'pcompare' (x - 'lower' t x) ('upper' t x - x) @
+--  \( f(x) = \inf \{y \in E \mid g(y) \geq x \} \)
 --
--- >>> maybe False (== EQ) $ half f64f32 (midpoint f64f32 pi)
--- True
-half :: (Num a, Preorder a) => ConnK a b -> a -> Maybe Ordering
-half c x = pcompare (x - lower c x) (upper c x - x)
-{-# INLINE half #-}
+-- /Caution/: /ConnL f g/ must obey \(f \dashv g \). This condition is not checked.
+--
+-- For further information see 'Data.Connection.Property'.
+pattern ConnL :: (a -> b) -> (b -> a) -> ConnL a b
+pattern ConnL f g <- (_2 &&& upper -> (f, g)) where ConnL f g = Conn_ (f &&& f) g
 
--- | Return the midpoint of the interval containing x.
+{-# COMPLETE ConnL #-}
+
+-- | Witness to the symmetry between 'ConnL' and 'ConnR'.
 --
--- >>> pi - midpoint f64f32 pi
--- 3.1786509424591713e-8
-midpoint :: Fractional a => ConnK a b -> a -> a
-midpoint c x = lower c x / 2 + upper c x / 2
-{-# INLINE midpoint #-}
+-- > connL . connR = id
+-- > connR . connL = id
+connL :: ConnR a b -> ConnL b a
+connL (ConnR f g) = ConnL f g
+{-# INLINE connL #-}
 
--- | Return the nearest value to x.
+-- | Obtain the upper adjoint of a 'ConnL', or lower adjoint of a 'ConnR'.
+upper :: ConnL a b -> b -> a
+upper = embed
+{-# INLINE upper #-}
+
+-- | Map over a 'ConnL' from the right.
 --
--- > roundWith identity = id
+-- This is the unit of the resulting monad:
 --
--- If x lies halfway between two finite values, then return the value
--- with the larger absolute value (i.e. round away from zero).
+-- > x <~ upper1 c id x
 --
--- See <https://en.wikipedia.org/wiki/Rounding>.
-roundWith :: forall a b. (Num a, Preorder a) => ConnK a b -> a -> b
-roundWith c x = case half c x of
-    Just GT -> ceilingWith c x
-    Just LT -> floorWith c x
-    _ -> truncateWith c x
-{-# INLINE roundWith #-}
+-- >>> compare pi $ upper1 f64f32 id pi
+-- LT
+upper1 :: ConnL a b -> (b -> b) -> a -> a
+upper1 (ConnL f g) h a = g $ h (f a)
+{-# INLINE upper1 #-}
 
--- | Lift a unary function over a 'ConnK'.
---
--- Results are rounded to the nearest value with ties away from 0.
-roundWith1 :: (Num a, Preorder a) => ConnK a b -> (a -> a) -> b -> b
-roundWith1 c f x = roundWith c $ f (g x) where Conn _ g _ = c
-{-# INLINE roundWith1 #-}
+-- | Zip over a 'ConnL' from the right.
+upper2 :: ConnL a b -> (b -> b -> b) -> a -> a -> a
+upper2 (ConnL f g) h a1 a2 = g $ h (f a1) (f a2)
+{-# INLINE upper2 #-}
 
--- | Lift a binary function over a 'ConnK'.
+infixr 5 `join`
+
+-- | Semigroup operation on a join-semilattice.
+join :: ConnL (a, a) b -> a -> a -> b
+join = curry . ceiling
+{-# INLINE join #-}
+
+-- | Extract the lower half of a 'ConnL'.
 --
--- Results are rounded to the nearest value with ties away from 0.
+-- > ceiling identity = id
+-- > ceiling c (x \/ y) = ceiling c x \/ ceiling c y
 --
--- Example avoiding loss-of-precision:
+-- The latter law is the adjoint functor theorem for preorders.
 --
--- >>> f x y = (x + y) - x
--- >>> maxOdd32 = 1.6777215e7
--- >>> f maxOdd32 2.0 :: Float
--- 1.0
--- >>> roundWith2 ratf32 f maxOdd32 2.0
--- 2.0
-roundWith2 :: (Num a, Preorder a) => ConnK a b -> (a -> a -> a) -> b -> b -> b
-roundWith2 c f x y = roundWith c $ f (g x) (g y) where Conn _ g _ = c
-{-# INLINE roundWith2 #-}
+-- >>> Data.Connection.ceiling ratf32 (0 :% 0)
+-- NaN
+-- >>> Data.Connection.ceiling ratf32 (1 :% 0)
+-- Infinity
+-- >>> Data.Connection.ceiling ratf32 (13 :% 10)
+-- 1.3000001
+-- >>> Data.Connection.ceiling f64f32 pi
+-- 3.1415927
+ceiling :: ConnL a b -> a -> b
+ceiling (ConnL f _) = f
+{-# INLINE ceiling #-}
 
--- | Truncate towards zero.
+-- | Map over a 'ConnL' from the left.
 --
--- > truncateWith identity = id
-truncateWith :: (Num a, Preorder a) => ConnK a b -> a -> b
-truncateWith c x = if x >~ 0 then floorWith c x else ceilingWith c x
-{-# INLINE truncateWith #-}
-
--- | Lift a unary function over a 'ConnK'.
+-- This is the counit of the resulting comonad:
 --
--- Results are truncated towards zero.
+-- > x >~ ceiling1 c id x
 --
--- > truncateWith1 identity = id
-truncateWith1 :: (Num a, Preorder a) => ConnK a b -> (a -> a) -> b -> b
-truncateWith1 c f x = truncateWith c $ f (g x) where Conn _ g _ = c
-{-# INLINE truncateWith1 #-}
+-- >>> ceiling1 (conn @_ @() @Ordering) id LT
+-- LT
+-- >>> ceiling1 (conn @_ @() @Ordering) id GT
+-- LT
+ceiling1 :: ConnL a b -> (a -> a) -> b -> b
+ceiling1 (ConnL f g) h b = f $ h (g b)
+{-# INLINE ceiling1 #-}
 
-truncateWith2 :: (Num a, Preorder a) => ConnK a b -> (a -> a -> a) -> b -> b -> b
-truncateWith2 c f x y = truncateWith c $ f (g x) (g y) where Conn _ g _ = c
-{-# INLINE truncateWith2 #-}
+-- | Zip over a 'ConnL' from the left.
+ceiling2 :: ConnL a b -> (a -> a -> a) -> b -> b -> b
+ceiling2 (ConnL f g) h b1 b2 = f $ h (g b1) (g b2)
+{-# INLINE ceiling2 #-}
 
 ---------------------------------------------------------------------
--- ConnL
+-- Conn 'R
 ---------------------------------------------------------------------
 
--- | A <https://ncatlab.org/nlab/show/Galois+connection Galois connection> between two monotone functions.
+type ConnR = Conn 'R
+
+-- | A Galois connection between two monotone functions.
 --
--- A Galois connection between /f/ and /g/, written \(f \dashv g \)
--- is an adjunction in the category of preorders.
+-- 'ConnR' is the mirror image of 'ConnL':
 --
--- Each side of the connection may be defined in terms of the other:
+-- > connR :: ConnL a b -> ConnR b a
 --
---  \( g(x) = \sup \{y \in E \mid f(y) \leq x \} \)
+-- If you only require one connection there is no particular reason to
+-- use one version over the other. However some use cases (e.g. rounding)
+-- require an adjoint triple of connections that can lower into a standard
+-- connection in either of two ways.
 --
---  \( f(x) = \inf \{y \in E \mid g(y) \geq x \} \)
+-- /Caution/: /ConnR f g/ must obey \(f \dashv g \). This condition is not checked.
 --
 -- For further information see 'Data.Connection.Property'.
---
--- /Caution/: Monotonicity is not checked.
-type ConnL = Conn 'L
+pattern ConnR :: (b -> a) -> (a -> b) -> ConnR a b
+pattern ConnR f g <- (lower &&& _1 -> (f, g)) where ConnR f g = Conn_ (g &&& g) f
 
--- | A view pattern for a 'ConnL'.
+{-# COMPLETE ConnR #-}
+
+-- | Witness to the symmetry between 'ConnL' and 'ConnR'.
 --
--- /Caution/: /ConnL f g/ must obey \(f \dashv g \). This condition is not checked.
-pattern ConnL :: (a -> b) -> (b -> a) -> ConnL a b
-pattern ConnL f g <- (_2 &&& embed -> (f, g)) where ConnL f g = Galois (f &&& f) g
+-- > connL . connR = id
+-- > connR . connL = id
+connR :: ConnL a b -> ConnR b a
+connR (ConnL f g) = ConnR f g
+{-# INLINE connR #-}
 
-{-# COMPLETE ConnL #-}
+-- | Obtain the  lower adjoint of a 'ConnR'.
+lower :: ConnR a b -> b -> a
+lower = embed
+{-# INLINE lower #-}
 
--- | Convert an inverted 'ConnL' to a 'ConnL'.
+-- | Map over a 'ConnR' from the left.
 --
--- > upL . downL = downL . upL = id
-upL :: ConnL (Down a) (Down b) -> ConnL b a
-upL (ConnL f g) = ConnL g' f'
-  where
-    f' x = let (Down y) = f (Down x) in y
-    g' x = let (Down y) = g (Down x) in y
-{-# INLINE upL #-}
-
--- | Convert a 'ConnL' to an inverted 'ConnL'.
+-- This is the counit of the resulting comonad:
 --
--- >>> upper (downL $ conn @_ @() @Ordering) (Down LT)
--- Down LT
--- >>> upper (downL $ conn @_ @() @Ordering) (Down GT)
--- Down LT
-downL :: ConnL a b -> ConnL (Down b) (Down a)
-downL (ConnL f g) = ConnL (\(Down x) -> Down $ g x) (\(Down x) -> Down $ f x)
-{-# INLINE downL #-}
-
--- | Witness to the symmetry between 'ConnL' and 'ConnR'.
+-- > x >~ lower1 c id x
 --
--- > swapL . swapR = id
--- > swapR . swapL = id
-swapL :: ConnR a b -> ConnL b a
-swapL (ConnR f g) = ConnL f g
-{-# INLINE swapL #-}
+-- >>> compare pi $ lower1 f64f32 id pi
+-- GT
+lower1 :: ConnR a b -> (b -> b) -> a -> a
+lower1 (ConnR f g) h a = f $ h (g a)
+{-# INLINE lower1 #-}
 
--- | Reverse round trip through a 'ConnK' or 'ConnL'.
+-- | Zip over a 'ConnR' from the left.
+lower2 :: ConnR a b -> (b -> b -> b) -> a -> a -> a
+lower2 (ConnR f g) h a1 a2 = f $ h (g a1) (g a2)
+{-# INLINE lower2 #-}
+
+infixr 6 `meet`
+
+-- | Semigroup operation on a meet-semilattice.
+meet :: ConnR (a, a) b -> a -> a -> b
+meet = curry . floor
+{-# INLINE meet #-}
+
+-- | Extract the upper half of a 'ConnR'
 --
--- This is the counit of the resulting comonad:
+-- > floor identity = id
+-- > floor c (x /\ y) = floor c x /\ floor c y
 --
--- > x >~ counit c x
+-- The latter law is the adjoint functor theorem for preorders.
 --
--- >>> counit (conn @_ @() @Ordering) LT
--- LT
--- >>> counit (conn @_ @() @Ordering) GT
--- LT
-counit :: ConnL a b -> b -> b
-counit c = ceilingWith1 c id
-{-# INLINE counit #-}
+-- >>> Data.Connection.floor ratf32 (0 :% 0)
+-- NaN
+-- >>> Data.Connection.floor ratf32 (1 :% 0)
+-- Infinity
+-- >>> Data.Connection.floor ratf32 (13 :% 10)
+-- 1.3
+-- >>> Data.Connection.floor f64f32 pi
+-- 3.1415925
+floor :: ConnR a b -> a -> b
+floor (ConnR _ g) = g
+{-# INLINE floor #-}
 
--- | Round trip through a 'ConnK' or 'ConnL'.
+-- | Map over a 'ConnR' from the right.
 --
--- > upper c = upper1 c id = embed c . ceilingWith c
--- > x <= upper c x
+-- This is the unit of the resulting monad:
 --
--- >>> compare pi $ upper f64f32 pi
--- LT
-upper :: ConnL a b -> a -> a
-upper c = upper1 c id
-{-# INLINE upper #-}
+-- > x <~ floor1 c id x
+--
+-- >>> floor1 (conn @_ @() @Ordering) id LT
+-- GT
+-- >>> floor1 (conn @_ @() @Ordering) id GT
+-- GT
+floor1 :: ConnR a b -> (a -> a) -> b -> b
+floor1 (ConnR f g) h b = g $ h (f b)
+{-# INLINE floor1 #-}
 
--- | Map over a 'ConnK' or 'ConnL' from the right.
-upper1 :: ConnL a b -> (b -> b) -> a -> a
-upper1 (ConnL f g) h a = g $ h (f a)
-{-# INLINE upper1 #-}
+-- | Zip over a 'ConnR' from the right.
+floor2 :: ConnR a b -> (a -> a -> a) -> b -> b -> b
+floor2 (ConnR f g) h b1 b2 = g $ h (f b1) (f b2)
+{-# INLINE floor2 #-}
 
--- | Zip over a 'ConnK' or 'ConnL' from the right.
-upper2 :: ConnL a b -> (b -> b -> b) -> a -> a -> a
-upper2 (ConnL f g) h a1 a2 = g $ h (f a1) (f a2)
-{-# INLINE upper2 #-}
+---------------------------------------------------------------------
+-- Conn k
+---------------------------------------------------------------------
 
--- | Obtain the principal filter in /B/ generated by an element of /A/.
---
--- A subset /B/ of a lattice is an filter if and only if it is an upper set
--- that is closed under finite meets, i.e., it is nonempty and for all
--- /x/, /y/ in /B/, the element @x `meet` y@ is also in /b/.
+-- | An <https://ncatlab.org/nlab/show/adjoint+triple adjoint triple> of Galois connections.
 --
--- /filterWith/ and /idealWith/ commute with /Down/:
+-- An adjoint triple is a chain of connections of length 3:
 --
--- > filterWith c a b <=> idealWith c (Down a) (Down b)
+-- \(f \dashv g \dashv h \)
 --
--- > filterWith c (Down a) (Down b) <=> idealWith c a b
+-- When applied to a 'ConnL' or 'ConnR', the two functions of type @a -> b@ returned will be identical.
 --
--- /filterWith c a/ is upward-closed for all /a/:
+-- /Caution/: /Conn f g h/ must obey \(f \dashv g \dashv h\). This condition is not checked.
 --
--- > a <= b1 && b1 <= b2 => a <= b2
+-- For detailed properties see 'Data.Connection.Property'.
+pattern Conn :: (a -> b) -> (b -> a) -> (a -> b) -> Conn k a b
+pattern Conn f g h <- (embed &&& _1 &&& _2 -> (g, (h, f))) where Conn f g h = Conn_ (h &&& f) g
+
+{-# COMPLETE Conn #-}
+
+-- | Determine which half of the interval between 2 representations of /a/ a particular value lies.
 --
--- > a1 <= b && inf a2 <= b => ceiling a1 `meet` ceiling a2 <= b
+-- @ 'half' c x = 'pcompare' (x - 'lower1' c 'id' x) ('upper1' c 'id' x - x) @
 --
--- See <https://en.wikipedia.org/wiki/Filter_(mathematics)>
-filterWith :: Preorder b => ConnL a b -> a -> b -> Bool
-filterWith c a b = ceilingWith c a <~ b
-{-# INLINE filterWith #-}
+-- >>> maybe False (== EQ) $ half f64f32 (midpoint f64f32 pi)
+-- True
+half :: (Num a, Preorder a) => (forall k. Conn k a b) -> a -> Maybe Ordering
+half c x = pcompare (x - lower1 c id x) (upper1 c id x - x)
+{-# INLINE half #-}
 
--- | Extract the left half of a 'ConnK' or 'ConnL'.
+-- | Return the midpoint of the interval containing x.
 --
--- >>> floorWith f64f32 pi
--- 3.1415925
--- >>> ceilingWith f64f32 pi
--- 3.1415927
-ceilingWith :: ConnL a b -> a -> b
-ceilingWith (ConnL f _) = f
-{-# INLINE ceilingWith #-}
-
--- | Map over a 'ConnK' or 'ConnL' from the left.
-ceilingWith1 :: ConnL a b -> (a -> a) -> b -> b
-ceilingWith1 (ConnL f g) h b = f $ h (g b)
-{-# INLINE ceilingWith1 #-}
+-- >>> pi - midpoint f64f32 pi
+-- 3.1786509424591713e-8
+midpoint :: Fractional a => (forall k. Conn k a b) -> a -> a
+midpoint c x = lower1 c id x / 2 + upper1 c id x / 2
+{-# INLINE midpoint #-}
 
--- | Zip over a 'ConnK' or 'ConnL' from the left.
-ceilingWith2 :: ConnL a b -> (a -> a -> a) -> b -> b -> b
-ceilingWith2 (ConnL f g) h b1 b2 = f $ h (g b1) (g b2)
-{-# INLINE ceilingWith2 #-}
+-- | Return the nearest value to x.
+--
+-- > round identity = id
+--
+-- If x lies halfway between two finite values, then return the value
+-- with the larger absolute value (i.e. round away from zero).
+--
+-- See <https://en.wikipedia.org/wiki/Rounding>.
+round :: (Num a, Preorder a) => (forall k. Conn k a b) -> a -> b
+round c x = case half c x of
+    Just GT -> ceiling c x
+    Just LT -> floor c x
+    _ -> truncate c x
+{-# INLINE round #-}
 
----------------------------------------------------------------------
--- ConnR
----------------------------------------------------------------------
+-- | Lift a unary function over a 'Trip'.
+--
+-- Results are rounded to the nearest value with ties away from 0.
+round1 :: (Num a, Preorder a) => (forall k. Conn k a b) -> (a -> a) -> b -> b
+round1 c f x = round c $ f (g x) where Conn _ g _ = c
+{-# INLINE round1 #-}
 
--- | A Galois connection between two monotone functions.
+-- | Lift a binary function over a 'Trip'.
 --
--- 'ConnR' is the mirror image of 'ConnL':
+-- Results are rounded to the nearest value with ties away from 0.
 --
--- > swapR :: ConnL a b -> ConnR b a
+-- Example avoiding loss-of-precision:
 --
--- If you only require one connection there is no particular reason to
--- use one version over the other.
+-- >>> f x y = (x + y) - x
+-- >>> maxOdd32 = 1.6777215e7
+-- >>> f maxOdd32 2.0 :: Float
+-- 1.0
+-- >>> round2 ratf32 f maxOdd32 2.0
+-- 2.0
+round2 :: (Num a, Preorder a) => (forall k. Conn k a b) -> (a -> a -> a) -> b -> b -> b
+round2 c f x y = round c $ f (g x) (g y) where Conn _ g _ = c
+{-# INLINE round2 #-}
+
+-- | Truncate towards zero.
 --
--- However some use cases (e.g. rounding) require an adjoint triple
--- of connections (i.e. a 'ConnK') that can lower into a standard
--- connection in either of two ways.
-type ConnR = Conn 'R
+-- > truncate identity = id
+truncate :: (Num a, Preorder a) => (forall k. Conn k a b) -> a -> b
+truncate c x = if x >~ 0 then floor c x else ceiling c x
+{-# INLINE truncate #-}
 
--- | A view pattern for a 'ConnR'.
+-- | Lift a unary function over a 'Trip'.
 --
--- /Caution/: /ConnR f g/ must obey \(f \dashv g \). This condition is not checked.
-pattern ConnR :: (b -> a) -> (a -> b) -> ConnR a b
-pattern ConnR f g <- (embed &&& _1 -> (f, g)) where ConnR f g = Galois (g &&& g) f
+-- Results are truncated towards zero.
+--
+-- > truncate1 identity = id
+truncate1 :: (Num a, Preorder a) => (forall k. Conn k a b) -> (a -> a) -> b -> b
+truncate1 c f x = truncate c $ f (g x) where Conn _ g _ = c
+{-# INLINE truncate1 #-}
 
-{-# COMPLETE ConnR #-}
+truncate2 :: (Num a, Preorder a) => (forall k. Conn k a b) -> (a -> a -> a) -> b -> b -> b
+truncate2 c f x y = truncate c $ f (g x) (g y) where Conn _ g _ = c
+{-# INLINE truncate2 #-}
 
+---------------------------------------------------------------------
+-- Down
+---------------------------------------------------------------------
+
+-- | Convert an inverted 'ConnL' to a 'ConnL'.
+--
+-- > upL . downL = downL . upL = id
+upL :: ConnL (Down a) (Down b) -> ConnL b a
+upL (ConnL f g) = ConnL g' f'
+  where
+    f' x = let (Down y) = f (Down x) in y
+    g' x = let (Down y) = g (Down x) in y
+{-# INLINE upL #-}
+
 -- | Convert an inverted 'ConnR' to a 'ConnR'.
 --
 -- > upR . downR = downR . upR = id
@@ -411,122 +501,63 @@
     g' x = let (Down y) = g (Down x) in y
 {-# INLINE upR #-}
 
+-- | Convert a 'ConnL' to an inverted 'ConnL'.
+--
+-- >>> let counit = upper1 (downL $ conn @_ @() @Ordering) id
+-- >>> counit (Down LT)
+-- Down LT
+-- >>> counit (Down GT)
+-- Down LT
+downL :: ConnL a b -> ConnL (Down b) (Down a)
+downL (ConnL f g) = ConnL (\(Down x) -> Down $ g x) (\(Down x) -> Down $ f x)
+{-# INLINE downL #-}
+
 -- | Convert a 'ConnR' to an inverted 'ConnR'.
 --
--- >>> lower (downR $ conn @_ @() @Ordering) (Down LT)
+-- >>> let unit = lower1 (downR $ conn @_ @() @Ordering) id
+-- >>> unit (Down LT)
 -- Down GT
--- >>> lower (downR $ conn @_ @() @Ordering) (Down GT)
+-- >>> unit (Down GT)
 -- Down GT
 downR :: ConnR a b -> ConnR (Down b) (Down a)
 downR (ConnR f g) = ConnR (\(Down x) -> Down $ g x) (\(Down x) -> Down $ f x)
 {-# INLINE downR #-}
 
--- | Witness to the symmetry between 'ConnL' and 'ConnR'.
+-- | Obtain the principal filter in /B/ generated by an element of /A/.
 --
--- > swapL . swapR = id
--- > swapR . swapL = id
-swapR :: ConnL a b -> ConnR b a
-swapR (ConnL f g) = ConnR f g
-{-# INLINE swapR #-}
-
--- | Round trip through a 'ConnK' or 'ConnR'.
+-- A subset /B/ of a lattice is an filter if and only if it is an upper set
+-- that is closed under finite meets, i.e., it is nonempty and for all
+-- /x/, /y/ in /B/, the element @meet c x y@ is also in /b/.
 --
--- This is the unit of the resulting monad:
+-- /filterL/ and /filterR/ commute with /Down/:
 --
--- > x <~ unit c x
--- > unit c = floorWith1 c id = floorWith c . embed c
+-- > filterL c a b <=> ideal c (Down a) (Down b)
 --
--- >>> unit (conn @_ @() @Ordering) LT
--- GT
--- >>> unit (conn @_ @() @Ordering) GT
--- GT
-unit :: ConnR a b -> b -> b
-unit c = floorWith1 c id
-{-# INLINE unit #-}
-
--- | Reverse round trip through a 'ConnK' or 'ConnR'.
+-- > filterL c (Down a) (Down b) <=> ideal c a b
 --
--- > x >~ lower c x
+-- /filterL c a/ is upward-closed for all /a/:
 --
--- >>> compare pi $ lower f64f32 pi
--- GT
-lower :: ConnR a b -> a -> a
-lower c = lower1 c id
-{-# INLINE lower #-}
-
--- | Map over a 'ConnK' or 'ConnR' from the left.
-lower1 :: ConnR a b -> (b -> b) -> a -> a
-lower1 (ConnR f g) h a = f $ h (g a)
-{-# INLINE lower1 #-}
-
--- | Zip over a 'ConnK' or 'ConnR' from the left.
-lower2 :: ConnR a b -> (b -> b -> b) -> a -> a -> a
-lower2 (ConnR f g) h a1 a2 = f $ h (g a1) (g a2)
-{-# INLINE lower2 #-}
+-- > a <= b1 && b1 <= b2 => a <= b2
+-- > a1 <= b && a2 <= b => meet c (ceiling c a1) (ceiling c a2) <= b
+--
+-- See <https://en.wikipedia.org/wiki/Filter_(mathematics)>
+filterL :: Preorder b => ConnL a b -> a -> b -> Bool
+filterL c a b = ceiling c a <~ b
+{-# INLINE filterL #-}
 
 -- | Obtain the principal ideal in /B/ generated by an element of /A/.
 --
 -- A subset /B/ of a lattice is an ideal if and only if it is a lower set
 -- that is closed under finite joins, i.e., it is nonempty and for all
--- /x/, /y/ in /B/, the element /x `join` y/ is also in /B/.
+-- /x/, /y/ in /B/, the element /join c x y/ is also in /B/.
 --
--- /idealWith c a/ is downward-closed for all /a/:
+-- /filterR c a/ is downward-closed for all /a/:
 --
 -- > a >= b1 && b1 >= b2 => a >= b2
 --
--- > a1 >= b && a2 >= b => floor a1 `join` floor a2 >= b
+-- > a1 >= b && a2 >= b => join c (floor c a1) (floor c a2) >= b
 --
 -- See <https://en.wikipedia.org/wiki/Ideal_(order_theory)>
-idealWith :: Preorder b => ConnR a b -> a -> b -> Bool
-idealWith c a b = b <~ floorWith c a
-{-# INLINE idealWith #-}
-
--- | Extract the right half of a 'ConnK' or 'ConnR'
---
--- This is the adjoint functor theorem for preorders.
---
--- >>> floorWith f64f32 pi
--- 3.1415925
--- >>> ceilingWith f64f32 pi
--- 3.1415927
-floorWith :: ConnR a b -> a -> b
-floorWith (ConnR _ g) = g
-{-# INLINE floorWith #-}
-
--- | Map over a 'ConnK' or 'ConnR' from the right.
-floorWith1 :: ConnR a b -> (a -> a) -> b -> b
-floorWith1 (ConnR f g) h b = g $ h (f b)
-{-# INLINE floorWith1 #-}
-
--- | Zip over a 'ConnK' or 'ConnR' from the right.
-floorWith2 :: ConnR a b -> (a -> a -> a) -> b -> b -> b
-floorWith2 (ConnR f g) h b1 b2 = g $ h (f b1) (f b2)
-{-# INLINE floorWith2 #-}
-
----------------------------------------------------------------------
--- Combinators
----------------------------------------------------------------------
-
--- | Lift two 'Conn's into a 'Conn' on the <https://en.wikibooks.org/wiki/Category_Theory/Categories_of_ordered_sets coproduct order>
---
--- > (choice id) (ab >>> cd) = (choice id) ab >>> (choice id) cd
--- > (flip choice id) (ab >>> cd) = (flip choice id) ab >>> (flip choice id) cd
-choice :: Conn k a b -> Conn k c d -> Conn k (Either a c) (Either b d)
-choice (Conn ab ba ab') (Conn cd dc cd') = Conn f g h
-  where
-    f = either (Left . ab) (Right . cd)
-    g = either (Left . ba) (Right . dc)
-    h = either (Left . ab') (Right . cd')
-{-# INLINE choice #-}
-
--- | Lift two 'Conn's into a 'Conn' on the <https://en.wikibooks.org/wiki/Order_Theory/Preordered_classes_and_poclasses#product_order product order>
---
--- > (strong id) (ab >>> cd) = (strong id) ab >>> (strong id) cd
--- > (flip strong id) (ab >>> cd) = (flip strong id) ab >>> (flip strong id) cd
-strong :: Conn k a b -> Conn k c d -> Conn k (a, c) (b, d)
-strong (Conn ab ba ab') (Conn cd dc cd') = Conn f g h
-  where
-    f = bimap ab cd
-    g = bimap ba dc
-    h = bimap ab' cd'
-{-# INLINE strong #-}
+filterR :: Preorder b => ConnR a b -> a -> b -> Bool
+filterR c a b = b <~ floor c a
+{-# INLINE filterR #-}
diff --git a/src/Data/Connection/Fixed.hs b/src/Data/Connection/Fixed.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Connection/Fixed.hs
@@ -0,0 +1,152 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE Safe #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+
+module Data.Connection.Fixed (
+    Fixed (..),
+    showFixed,
+    shiftf,
+
+    -- * Uni
+    Uni,
+
+    -- * Deci
+    Deci,
+    f01f00,
+
+    -- * Centi
+    Centi,
+    f02f00,
+    f02f01,
+
+    -- * Milli
+    Milli,
+    f03f00,
+    f03f01,
+    f03f02,
+
+    -- * Micro
+    Micro,
+    f06f00,
+    f06f01,
+    f06f02,
+    f06f03,
+
+    -- * Nano
+    Nano,
+    f09f00,
+    f09f01,
+    f09f02,
+    f09f03,
+    f09f06,
+
+    -- * Pico
+    Pico,
+    f12f00,
+    f12f01,
+    f12f02,
+    f12f03,
+    f12f06,
+    f12f09,
+
+    -- * HasResolution
+    HasResolution (..),
+) where
+
+import safe Data.Connection.Conn
+import safe Data.Fixed
+import safe Data.Order.Syntax
+import safe Prelude hiding (Eq (..), Ord (..))
+
+-- | Shift by n 'units of least precision' where the ULP is determined by the precision.
+--
+-- This is an analog of 'Data.Connection.Float.shift32' for fixed point numbers.
+shiftf :: Integer -> Fixed a -> Fixed a
+shiftf j (MkFixed i) = MkFixed (i + j)
+
+-- Deci
+
+f01f00 :: Conn k Deci Uni
+f01f00 = triple 10
+
+-- Centi
+
+f02f00 :: Conn k Centi Uni
+f02f00 = triple 100
+
+f02f01 :: Conn k Centi Deci
+f02f01 = triple 10
+
+-- Milli
+
+f03f00 :: Conn k Milli Uni
+f03f00 = triple 1000
+
+f03f01 :: Conn k Milli Deci
+f03f01 = triple 100
+
+f03f02 :: Conn k Milli Centi
+f03f02 = triple 10
+
+-- Micro
+
+f06f00 :: Conn k Micro Uni
+f06f00 = triple $ 10 ^ (6 :: Integer)
+
+f06f01 :: Conn k Micro Deci
+f06f01 = triple $ 10 ^ (5 :: Integer)
+
+f06f02 :: Conn k Micro Centi
+f06f02 = triple $ 10 ^ (4 :: Integer)
+
+f06f03 :: Conn k Micro Milli
+f06f03 = triple $ 10 ^ (3 :: Integer)
+
+-- Nano
+
+f09f00 :: Conn k Nano Uni
+f09f00 = triple $ 10 ^ (9 :: Integer)
+
+f09f01 :: Conn k Nano Deci
+f09f01 = triple $ 10 ^ (8 :: Integer)
+
+f09f02 :: Conn k Nano Centi
+f09f02 = triple $ 10 ^ (7 :: Integer)
+
+f09f03 :: Conn k Nano Milli
+f09f03 = triple $ 10 ^ (6 :: Integer)
+
+f09f06 :: Conn k Nano Micro
+f09f06 = triple $ 10 ^ (3 :: Integer)
+
+-- Pico
+
+f12f00 :: Conn k Pico Uni
+f12f00 = triple $ 10 ^ (12 :: Integer)
+
+f12f01 :: Conn k Pico Deci
+f12f01 = triple $ 10 ^ (11 :: Integer)
+
+f12f02 :: Conn k Pico Centi
+f12f02 = triple $ 10 ^ (10 :: Integer)
+
+f12f03 :: Conn k Pico Milli
+f12f03 = triple $ 10 ^ (9 :: Integer)
+
+f12f06 :: Conn k Pico Micro
+f12f06 = triple $ 10 ^ (6 :: Integer)
+
+f12f09 :: Conn k Pico Nano
+f12f09 = triple $ 10 ^ (3 :: Integer)
+
+-- Internal
+
+-------------------------
+
+triple :: Integer -> Conn k (Fixed e1) (Fixed e2)
+triple prec = Conn f g h
+  where
+    f (MkFixed i) = MkFixed $ let j = i `div` prec in if i `mod` prec == 0 then j else j + 1
+    g (MkFixed i) = MkFixed $ i * prec
+    h (MkFixed i) = MkFixed $ let j = i `div` prec in if i `mod` prec == 0 then j else j -1
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
@@ -1,34 +1,45 @@
 {-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE Safe #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE ViewPatterns #-}
 
 module Data.Connection.Float (
-    -- * Connections
-    f32i08,
-    f32i16,
-    f64i08,
-    f64i16,
-    f64i32,
-    f64f32,
-
     -- * Float
     min32,
     max32,
+    eps32,
     ulp32,
     near32,
     shift32,
+    f32i08,
+    f32i16,
+    f32i32,
+    f32i64,
+    f32ixx,
+    f32int,
 
     -- * Double
     min64,
     max64,
+    eps64,
     ulp64,
     near64,
     shift64,
+    f64i08,
+    f64i16,
+    f64i32,
+    f64i64,
+    f64ixx,
+    f64int,
+    f64f32,
     until,
 ) where
 
 import safe Data.Bool
-import safe Data.Connection.Conn
+import safe Data.Connection.Conn hiding (ceiling, floor)
 import safe Data.Int
 import safe Data.Order
 import safe Data.Order.Extended
@@ -39,56 +50,6 @@
 import safe qualified Prelude as P
 
 ---------------------------------------------------------------------
--- Connections
----------------------------------------------------------------------
-
--- | All 'Data.Int.Int08' values are exactly representable in a 'Float'.
-f32i08 :: Conn k Float (Extended Int8)
-f32i08 = triple 127
-
--- | All 'Data.Int.Int16' values are exactly representable in a 'Float'.
---
---  > ceilingWith f32i16 32767.0
---  Extended 32767
---  > ceilingWith f32i16 32767.1
---  Top
-f32i16 :: Conn k Float (Extended Int16)
-f32i16 = triple 32767
-
--- | All 'Data.Int.Int08' values are exactly representable in a 'Double'.
-f64i08 :: Conn k Double (Extended Int8)
-f64i08 = triple 127
-
--- | All 'Data.Int.Int16' values are exactly representable in a 'Double'.
-f64i16 :: Conn k Double (Extended Int16)
-f64i16 = triple 32767
-
--- | All 'Data.Int.Int32' values are exactly representable in a 'Double'.
-f64i32 :: Conn k Double (Extended Int32)
-f64i32 = triple 2147483647
-
-f64f32 :: Conn k Double Float
-f64f32 = Conn f1 g f2
-  where
-    f1 x =
-        let est = F.double2Float x
-         in if g est >~ x
-                then est
-                else ascend32 est g x
-
-    f2 x =
-        let est = F.double2Float x
-         in if g est <~ x
-                then est
-                else descend32 est g x
-
-    g = F.float2Double
-
-    ascend32 z g1 y = until (\x -> g1 x >~ y) (<~) (shift32 1) z
-
-    descend32 z h1 x = until (\y -> h1 y <~ x) (>~) (shift32 (-1)) z
-
----------------------------------------------------------------------
 -- Float
 ---------------------------------------------------------------------
 
@@ -114,6 +75,12 @@
     (True, False) -> y
     (True, True) -> x
 
+-- | Compute the difference between a float and its next largest neighbor.
+--
+-- See < https://en.wikipedia.org/wiki/Machine_epsilon >.
+eps32 :: Float -> Float
+eps32 x = shift32 1 x - x
+
 -- | Compute the signed distance between two floats in units of least precision.
 --
 -- >>> ulp32 1.0 (shift32 1 1.0)
@@ -133,7 +100,7 @@
 --
 -- Required accuracy is specified in units of least precision.
 --
--- See also <https://randomascii.wordpress.com/2012/02/25/comparing-floating-point-numbers-2012-edition/>.
+-- See <https://randomascii.wordpress.com/2012/02/25/comparing-floating-point-numbers-2012-edition/>.
 near32 :: Word32 -> Float -> Float -> Bool
 near32 tol x y = maybe False ((<= tol) . snd) $ ulp32 x y
 
@@ -144,16 +111,45 @@
 -- >>> shift32 1 1 - 1
 -- 1.1920929e-7
 -- >>> shift32 1 $ 0/0
--- NaN
+-- Infinity
 -- >>> shift32 (-1) $ 0/0
--- NaN
+-- -Infinity
 -- >>> shift32 1 $ 1/0
 -- Infinity
 shift32 :: Int32 -> Float -> Float
-shift32 n x
-    | x ~~ 0 / 0 = x
-    | otherwise = int32Float . clamp32 . (+ n) . floatInt32 $ x
+shift32 n x =
+    if isNaN x == True
+        then case signum n of
+            -1 -> -1 / 0
+            1 -> 1 / 0
+            _ -> 0 / 0
+        else int32Float . clamp32 . (+ n) . floatInt32 $ x
 
+-- | All 'Data.Int.Int08' values are exactly representable in a 'Float'.
+f32i08 :: Conn k Float (Extended Int8)
+f32i08 = fxxext
+
+-- | All 'Data.Int.Int16' values are exactly representable in a 'Float'.
+--
+-- >>> Data.Connection.Conn.ceiling f32i16 32767.0
+-- Extended 32767
+-- >>> Data.Connection.Conn.ceiling f32i16 32767.1
+-- Top
+f32i16 :: Conn k Float (Extended Int16)
+f32i16 = fxxext
+
+f32i32 :: Conn 'L Float (Extended Int32)
+f32i32 = f32ext
+
+f32i64 :: Conn 'L Float (Extended Int64)
+f32i64 = f32ext
+
+f32ixx :: Conn 'L Float (Extended Int)
+f32ixx = f32ext
+
+f32int :: Conn 'L Float (Extended Integer)
+f32int = f32ext
+
 ---------------------------------------------------------------------
 -- Double
 ---------------------------------------------------------------------
@@ -180,6 +176,12 @@
     (True, False) -> y
     (True, True) -> x
 
+-- | Compute the difference between a double and its next largest neighbor.
+--
+-- See < https://en.wikipedia.org/wiki/Machine_epsilon >.
+eps64 :: Double -> Double
+eps64 x = shift64 1 x - x
+
 -- | Compute the signed distance between two doubles in units of least precision.
 --
 -- >>> ulp64 1.0 (shift64 1 1.0)
@@ -210,16 +212,63 @@
 -- >>> shift64 1 1 - 1
 -- 2.220446049250313e-16
 -- >>> shift64 1 $ 0/0
--- NaN
+-- Infinity
 -- >>> shift64 (-1) $ 0/0
--- NaN
+-- -Infinity
 -- >>> shift64 1 $ 1/0
 -- Infinity
 shift64 :: Int64 -> Double -> Double
-shift64 n x
-    | x ~~ 0 / 0 = x
-    | otherwise = int64Double . clamp64 . (+ n) . doubleInt64 $ x
+shift64 n x =
+    if isNaN x == True
+        then case signum n of
+            -1 -> -1 / 0
+            1 -> 1 / 0
+            _ -> 0 / 0
+        else int64Double . clamp64 . (+ n) . doubleInt64 $ x
 
+-- | All 'Data.Int.Int08' values are exactly representable in a 'Double'.
+f64i08 :: Conn k Double (Extended Int8)
+f64i08 = fxxext
+
+-- | All 'Data.Int.Int16' values are exactly representable in a 'Double'.
+f64i16 :: Conn k Double (Extended Int16)
+f64i16 = fxxext
+
+-- | All 'Data.Int.Int32' values are exactly representable in a 'Double'.
+f64i32 :: Conn k Double (Extended Int32)
+f64i32 = fxxext
+
+f64i64 :: Conn 'L Double (Extended Int64)
+f64i64 = f64ext
+
+f64ixx :: Conn 'L Double (Extended Int)
+f64ixx = f64ext
+
+f64int :: Conn 'L Double (Extended Integer)
+f64int = f64ext
+
+f64f32 :: Conn k Double Float
+f64f32 = Conn f g h
+  where
+    f x =
+        let est = double2Float x
+         in if g est >~ x
+                then est
+                else ascend32 est g x
+
+    g = float2Double
+
+    h x =
+        let est = double2Float x
+         in if g est <~ x
+                then est
+                else descend32 est g x
+
+    ascend32 z g1 y = until (\x -> g1 x >~ y) (<~) (shift32 1) z
+
+    descend32 z h1 x = until (\y -> h1 y <~ x) (>~) (shift32 (-1)) z
+{-# INLINE f64f32 #-}
+
 ---------------------------------------------------------------------
 -- Internal
 ---------------------------------------------------------------------
@@ -245,7 +294,7 @@
 signed64 :: Word64 -> Int64
 signed64 x
     | x < 0x8000000000000000 = fromIntegral x
-    | otherwise = fromIntegral (maxBound P.- (x P.- 0x8000000000000000))
+    | otherwise = fromIntegral (maxBound - (x - 0x8000000000000000))
 
 -- Non-monotonic function converting from 2s-complement format.
 unsigned32 :: Int32 -> Word32
@@ -256,20 +305,21 @@
 -- Non-monotonic function converting from 2s-complement format.
 unsigned64 :: Int64 -> Word64
 unsigned64 x
-    | x >~ 0 = fromIntegral x
-    | otherwise = 0x8000000000000000 + (maxBound P.- (fromIntegral x))
+    | x >= 0 = fromIntegral x
+    | otherwise = 0x8000000000000000 + (maxBound - (fromIntegral x))
 
 int32Float :: Int32 -> Float
-int32Float = F.castWord32ToFloat . unsigned32
+int32Float = castWord32ToFloat . unsigned32
 
+-- NB: I needed these zeros to avoid some error
 floatInt32 :: Float -> Int32
-floatInt32 = signed32 . (+ 0) . F.castFloatToWord32
+floatInt32 = signed32 . (+ 0) . castFloatToWord32
 
 int64Double :: Int64 -> Double
-int64Double = F.castWord64ToDouble . unsigned64
+int64Double = castWord64ToDouble . unsigned64
 
 doubleInt64 :: Double -> Int64
-doubleInt64 = signed64 . (+ 0) . F.castDoubleToWord64
+doubleInt64 = signed64 . (+ 0) . castDoubleToWord64
 
 -- Clamp between the int representations of -1/0 and 1/0
 clamp32 :: Int32 -> Int32
@@ -279,51 +329,59 @@
 clamp64 :: Int64 -> Int64
 clamp64 = P.max (-9218868437227405313) . P.min 9218868437227405312
 
-triple :: (RealFrac a, Preorder a, Bounded b, Integral b) => a -> Conn k a (Extended b)
-triple high = Conn f g h
+f32ext :: Integral a => Conn 'L Float (Extended a)
+f32ext = ConnL f g
   where
-    f = liftExtended (~~ -1 / 0) (\x -> x ~~ 0 / 0 || x > high) $ \x -> if x < low then minBound else P.ceiling x
+    prec = 24 :: Int -- Float loses integer precision beyond 2^prec
+    f x
+        | abs x <= 2 ** 24 -1 = Extended (ceiling x)
+        | otherwise = case pcompare x 0 of
+            Just LT -> Bottom
+            _ -> Extended (2 ^ prec)
 
-    g = extended (-1 / 0) (1 / 0) P.fromIntegral
+    g Bottom = -2 ** 24
+    g Top = 1 / 0
+    g (Extended i)
+        | abs i P.<= 2 ^ prec -1 = fromIntegral i
+        | otherwise = if i P.>= 0 then 1 / 0 else -2 ** 24
+{-# INLINE f32ext #-}
 
-    h = liftExtended (\x -> x ~~ 0 / 0 || x < low) (~~ 1 / 0) $ \x -> if x > high then maxBound else P.floor x
+f64ext :: Integral a => Conn 'L Double (Extended a)
+f64ext = ConnL f g
+  where
+    prec = 53 :: Int -- Double loses integer precision beyond 2^prec
+    f x
+        | abs x <= 2 ** 53 -1 = Extended (ceiling x)
+        | otherwise = case pcompare x 0 of
+            Just LT -> Bottom
+            _ -> Extended (2 ^ prec)
 
-    low = -1 - high
+    g Bottom = -2 ** 53
+    g Top = 1 / 0
+    g (Extended i)
+        | abs i P.<= 2 ^ prec -1 = fromIntegral i
+        | otherwise = if i P.>= 0 then 1 / 0 else -2 ** 53
+{-# INLINE f64ext #-}
 
-{-
--- | Exact embedding up to the largest representable 'Int32'.
-f32i32 :: ConnL Float (Maybe Int32)
-f32i32 = Conn (nanf f) (nan g) where
-  f x | abs x <~ 2**24-1 = P.ceiling x
-      | otherwise = if x >~ 0 then 2^24 else minBound
+fxxext :: forall a b k. (RealFrac a, Preorder a, Bounded b, Integral b) => Conn k a (Extended b)
+fxxext = Conn f g h
+  where
+    f = liftExtended (~~ -1 / 0) (\x -> x ~~ 0 / 0 || x > high) $ \x -> if x < low then minBound else ceiling x
 
-  g i | abs' i <~ 2^24-1 = fromIntegral i
-      | otherwise = if i >~ 0 then 1/0 else -2**24
+    g = extended (-1 / 0) (1 / 0) fromIntegral
 
--- | Exact embedding up to the largest representable 'Int32'.
-i32f32 :: ConnL (Maybe Int32) Float
-i32f32 = Conn (nan g) (nanf f) where
-  f x | abs x <~ 2**24-1 = P.floor x
-      | otherwise = if x >~ 0 then maxBound else -2^24
+    h = liftExtended (\x -> x ~~ 0 / 0 || x < low) (~~ 1 / 0) $ \x -> if x > high then maxBound else floor x
 
-  g i | abs i <~ 2^24-1 = fromIntegral i
-      | otherwise = if i >~ 0 then 2**24 else -1/0
+    low = fromIntegral $ minBound @b
 
--- | Exact embedding up to the largest representable 'Int64'.
-f64i64 :: Conn Double (Maybe Int64)
-f64i64 = Conn (nanf f) (nan g) where
-  f x | abs x <~ 2**53-1 = P.ceiling x
-      | otherwise = if x >~ 0 then 2^53 else minBound
+    high = fromIntegral $ maxBound @b
+{-# INLINE fxxext #-}
 
-  g i | abs' i <~ 2^53-1 = fromIntegral i
-      | otherwise = if i >~ 0 then 1/0 else -2**53
+{-
 
--- | Exact embedding up to the largest representable 'Int64'.
-f64ixx :: Conn Double (Maybe Int)
-f64ixx = Conn (nanf f) (nan g) where
-  f x | abs x <~ 2**53-1 = P.ceiling x
-      | otherwise = if x >~ 0 then 2^53 else minBound
+frac2fixed :: (RealFrac a, HasResolution b) => a -> Fixed b
+frac2fixed (flip approxRational 0 -> (n :% d)) = fromInteger n / fromInteger d
 
-  g i | abs' i <~ 2^53-1 = fromIntegral i
-      | otherwise = if i >~ 0 then 1/0 else -2**53
+--fixed2Float :: forall a . HasResolution a => Fixed a -> Float
+--fixed2Float (MkFixed i) = rationalToFloat i $ resolution (Proxy :: Proxy a)
 -}
diff --git a/src/Data/Connection/Int.hs b/src/Data/Connection/Int.hs
--- a/src/Data/Connection/Int.hs
+++ b/src/Data/Connection/Int.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
 {-# LANGUAGE Safe #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
@@ -54,61 +55,61 @@
 import safe Prelude
 
 -- Int16
-w08i16 :: ConnL Word8 (Maybe Int16)
+w08i16 :: Conn 'L Word8 (Maybe Int16)
 w08i16 = signed
 
-i08i16 :: ConnL Int8 (Maybe Int16)
+i08i16 :: Conn 'L Int8 (Maybe Int16)
 i08i16 = signed
 
 -- Int32
-w08i32 :: ConnL Word8 (Maybe Int32)
+w08i32 :: Conn 'L Word8 (Maybe Int32)
 w08i32 = signed
 
-w16i32 :: ConnL Word16 (Maybe Int32)
+w16i32 :: Conn 'L Word16 (Maybe Int32)
 w16i32 = signed
 
-i08i32 :: ConnL Int8 (Maybe Int32)
+i08i32 :: Conn 'L Int8 (Maybe Int32)
 i08i32 = signed
 
-i16i32 :: ConnL Int16 (Maybe Int32)
+i16i32 :: Conn 'L Int16 (Maybe Int32)
 i16i32 = signed
 
 -- Int64
-w08i64 :: ConnL Word8 (Maybe Int64)
+w08i64 :: Conn 'L Word8 (Maybe Int64)
 w08i64 = signed
 
-w16i64 :: ConnL Word16 (Maybe Int64)
+w16i64 :: Conn 'L Word16 (Maybe Int64)
 w16i64 = signed
 
-w32i64 :: ConnL Word32 (Maybe Int64)
+w32i64 :: Conn 'L Word32 (Maybe Int64)
 w32i64 = signed
 
-i08i64 :: ConnL Int8 (Maybe Int64)
+i08i64 :: Conn 'L Int8 (Maybe Int64)
 i08i64 = signed
 
-i16i64 :: ConnL Int16 (Maybe Int64)
+i16i64 :: Conn 'L Int16 (Maybe Int64)
 i16i64 = signed
 
-i32i64 :: ConnL Int32 (Maybe Int64)
+i32i64 :: Conn 'L Int32 (Maybe Int64)
 i32i64 = signed
 
 -- Int
-w08ixx :: ConnL Word8 (Maybe Int)
+w08ixx :: Conn 'L Word8 (Maybe Int)
 w08ixx = signed
 
-w16ixx :: ConnL Word16 (Maybe Int)
+w16ixx :: Conn 'L Word16 (Maybe Int)
 w16ixx = signed
 
-w32ixx :: ConnL Word32 (Maybe Int)
+w32ixx :: Conn 'L Word32 (Maybe Int)
 w32ixx = signed
 
-i08ixx :: ConnL Int8 (Maybe Int)
+i08ixx :: Conn 'L Int8 (Maybe Int)
 i08ixx = signed
 
-i16ixx :: ConnL Int16 (Maybe Int)
+i16ixx :: Conn 'L Int16 (Maybe Int)
 i16ixx = signed
 
-i32ixx :: ConnL Int32 (Maybe Int)
+i32ixx :: Conn 'L Int32 (Maybe Int)
 i32ixx = signed
 
 -- | /Caution/: This assumes that 'Int' on your system is 64 bits.
@@ -116,37 +117,37 @@
 i64ixx = Conn fromIntegral fromIntegral fromIntegral
 
 -- Integer
-w08int :: ConnL Word8 (Maybe Integer)
+w08int :: Conn 'L Word8 (Maybe Integer)
 w08int = signed
 
-w16int :: ConnL Word16 (Maybe Integer)
+w16int :: Conn 'L Word16 (Maybe Integer)
 w16int = signed
 
-w32int :: ConnL Word32 (Maybe Integer)
+w32int :: Conn 'L Word32 (Maybe Integer)
 w32int = signed
 
-w64int :: ConnL Word64 (Maybe Integer)
+w64int :: Conn 'L Word64 (Maybe Integer)
 w64int = signed
 
-wxxint :: ConnL Word (Maybe Integer)
+wxxint :: Conn 'L Word (Maybe Integer)
 wxxint = signed
 
-natint :: ConnL Natural (Maybe Integer)
+natint :: Conn 'L Natural (Maybe Integer)
 natint = ConnL (fmap fromIntegral . fromPred (/= 0)) (maybe 0 $ fromInteger . max 0)
 
-i08int :: ConnL Int8 (Maybe Integer)
+i08int :: Conn 'L Int8 (Maybe Integer)
 i08int = signed
 
-i16int :: ConnL Int16 (Maybe Integer)
+i16int :: Conn 'L Int16 (Maybe Integer)
 i16int = signed
 
-i32int :: ConnL Int32 (Maybe Integer)
+i32int :: Conn 'L Int32 (Maybe Integer)
 i32int = signed
 
-i64int :: ConnL Int64 (Maybe Integer)
+i64int :: Conn 'L Int64 (Maybe Integer)
 i64int = signed
 
-ixxint :: ConnL Int (Maybe Integer)
+ixxint :: Conn 'L Int (Maybe Integer)
 ixxint = signed
 
 ---------------------------------------------------------------------
@@ -156,7 +157,7 @@
 fromPred :: (a -> Bool) -> a -> Maybe a
 fromPred p a = a <$ guard (p a)
 
-signed :: forall a b. (Bounded a, Integral a, Integral b) => ConnL a (Maybe b)
+signed :: forall a b. (Bounded a, Integral a, Integral b) => Conn 'L a (Maybe b)
 signed = ConnL f g
   where
     f = fmap fromIntegral . fromPred (/= minBound)
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
@@ -8,117 +8,138 @@
 --
 --  \( \forall x, y : f \dashv g \Rightarrow f (x) \leq b \Leftrightarrow x \leq g (y) \)
 --
---  \( \forall x, y : x \leq y \Rightarrow f (x) \leq f (y) \)
---
---  \( \forall x, y : x \leq y \Rightarrow g (x) \leq g (y) \)
---
 --  \( \forall x : f \dashv g \Rightarrow x \leq g \circ f (x) \)
 --
 --  \( \forall x : f \dashv g \Rightarrow f \circ g (x) \leq x \)
---
---  \( \forall x : unit \circ unit (x) \sim unit (x) \)
---
---  \( \forall x : counit \circ counit (x) \sim counit (x) \)
---
---  \( \forall x : counit \circ f (x) \sim f (x) \)
---
---  \( \forall x : unit \circ g (x) \sim g (x) \)
-module Data.Connection.Property where
+module Data.Connection.Property (
+    -- * Adjointness
+    adjointL,
+    adjointR,
+    adjoint,
+    adjunction,
 
+    -- * Closure
+    closedL,
+    closedR,
+    closed,
+    kernelL,
+    kernelR,
+    kernel,
+    invertible,
+
+    -- * Monotonicity
+    monotonicR,
+    monotonicL,
+    monotonic,
+    monotone,
+
+    -- * Idempotence
+    idempotentL,
+    idempotentR,
+    idempotent,
+    projective,
+) where
+
 import Data.Connection
 import Data.Order
 import Data.Order.Property
 import Prelude hiding (Num (..), Ord (..), ceiling, floor)
 
+-- Adjointness
+
+-------------------------
+
 -- | \( \forall x, y : f \dashv g \Rightarrow f (x) \leq y \Leftrightarrow x \leq g (y) \)
 --
 -- A Galois connection is an adjunction of preorders. This is a required property.
-adjoint :: (Preorder a, Preorder b) => ConnK a b -> a -> b -> Bool
-adjoint t a b =
-    adjointL t a b
-        && adjointR t a b
-        && adjointL (swapL t) b a
-        && adjointR (swapR t) b a
-
 adjointL :: (Preorder a, Preorder b) => ConnL a b -> a -> b -> Bool
 adjointL (ConnL f g) = adjunction (<~) (<~) f g
 
 adjointR :: (Preorder a, Preorder b) => ConnR a b -> a -> b -> Bool
 adjointR (ConnR f g) = adjunction (>~) (>~) g f
 
+adjoint :: (Preorder a, Preorder b) => (forall k. Conn k a b) -> a -> b -> Bool
+adjoint t a b =
+    adjointL t a b
+        && adjointR t a b
+        && adjointL (connL t) b a
+        && adjointR (connR t) b a
+
+-- | \( \forall a: f a \leq b \Leftrightarrow a \leq g b \)
+--
+-- A monotone Galois connection is defined by @adjunction (<~) (<~)@,
+-- while an antitone Galois connection is defined by @adjunction (>~) (<~)@.
+adjunction :: Rel r Bool -> Rel s Bool -> (s -> r) -> (r -> s) -> s -> r -> Bool
+adjunction (#) (%) f g a b = f a # b <=> a % g b
+
+-- Closure
+
+-------------------------
+
 -- | \( \forall x : f \dashv g \Rightarrow x \leq g \circ f (x) \)
 --
 -- This is a required property.
-closed :: (Preorder a, Preorder b) => ConnK a b -> a -> Bool
-closed t a = closedL t a && closedR t a
-
 closedL :: (Preorder a, Preorder b) => ConnL a b -> a -> Bool
 closedL (ConnL f g) = invertible (>~) f g
 
 closedR :: (Preorder a, Preorder b) => ConnR a b -> a -> Bool
 closedR (ConnR f g) = invertible (<~) g f
 
+closed :: (Preorder a, Preorder b) => (forall k. Conn k a b) -> a -> Bool
+closed t a = closedL t a && closedR t a
+
 -- | \( \forall x : f \dashv g \Rightarrow x \leq g \circ f (x) \)
 --
 -- This is a required property.
-kernel :: (Preorder a, Preorder b) => ConnK a b -> b -> Bool
-kernel t b = kernelL t b && kernelR t b
-
 kernelL :: (Preorder a, Preorder b) => ConnL a b -> b -> Bool
 kernelL (ConnL f g) = invertible (<~) g f
 
 kernelR :: (Preorder a, Preorder b) => ConnR a b -> b -> Bool
 kernelR (ConnR f g) = invertible (>~) f g
 
+kernel :: (Preorder a, Preorder b) => (forall k. Conn k a b) -> b -> Bool
+kernel t b = kernelL t b && kernelR t b
+
+-- | \( \forall a: f (g a) \sim a \)
+invertible :: Rel s b -> (s -> r) -> (r -> s) -> s -> b
+invertible (#) f g a = g (f a) # a
+
+-- Monotonicity
+
+-------------------------
+
 -- | \( \forall x, y : x \leq y \Rightarrow f (x) \leq f (y) \)
 --
 -- This is a required property.
-monotonic :: (Preorder a, Preorder b) => ConnK a b -> a -> a -> b -> b -> Bool
-monotonic t a1 a2 b1 b2 = monotonicL t a1 a2 b1 b2 && monotonicR t a1 a2 b1 b2
-
 monotonicR :: (Preorder a, Preorder b) => ConnR a b -> a -> a -> b -> b -> Bool
 monotonicR (ConnR f g) a1 a2 b1 b2 = monotone (<~) (<~) g a1 a2 && monotone (<~) (<~) f b1 b2
 
 monotonicL :: (Preorder a, Preorder b) => ConnL a b -> a -> a -> b -> b -> Bool
 monotonicL (ConnL f g) a1 a2 b1 b2 = monotone (<~) (<~) f a1 a2 && monotone (<~) (<~) g b1 b2
 
--- | \( \forall x: f \dashv g \Rightarrow counit \circ f (x) \sim f (x) \wedge unit \circ g (x) \sim g (x) \)
---
--- See <https://ncatlab.org/nlab/show/idempotent+adjunction>
-idempotent :: (Preorder a, Preorder b) => ConnK a b -> a -> b -> Bool
-idempotent t a b = idempotentL t a b && idempotentR t a b
-
-idempotentL :: (Preorder a, Preorder b) => ConnL a b -> a -> b -> Bool
-idempotentL c@(ConnL f g) a b = projective (~~) g (upper c) b && projective (~~) f (counit c) a
-
-idempotentR :: (Preorder a, Preorder b) => ConnR a b -> a -> b -> Bool
-idempotentR c@(ConnR f g) a b = projective (~~) g (unit c) a && projective (~~) f (lower c) b
-
----------------------------------------------------------------------
--- Properties of general relations
----------------------------------------------------------------------
+monotonic :: (Preorder a, Preorder b) => (forall k. Conn k a b) -> a -> a -> b -> b -> Bool
+monotonic t a1 a2 b1 b2 = monotonicL t a1 a2 b1 b2 && monotonicR t a1 a2 b1 b2
 
 -- | \( \forall a, b: a \leq b \Rightarrow f(a) \leq f(b) \)
 monotone :: Rel r Bool -> Rel s Bool -> (r -> s) -> r -> r -> Bool
 monotone (#) (%) f a b = a # b ==> f a % f b
 
--- | \( \forall a, b: a \leq b \Rightarrow f(b) \leq f(a) \)
-antitone :: Rel r Bool -> Rel s Bool -> (r -> s) -> r -> r -> Bool
-antitone (#) (%) f a b = a # b ==> f b % f a
+-- Idempotence
 
--- | \( \forall a: f a \leq b \Leftrightarrow a \leq g b \)
+-------------------------
+
+-- | \( \forall x: f \dashv g \Rightarrow counit \circ f (x) \sim f (x) \wedge unit \circ g (x) \sim g (x) \)
 --
--- For example, a monotone Galois connection is defined by @adjunction (<~) (<~)@,
--- and an antitone Galois connection is defined by @adjunction (>~) (<~)@.
-adjunction :: Rel r Bool -> Rel s Bool -> (s -> r) -> (r -> s) -> s -> r -> Bool
-adjunction (#) (%) f g a b = f a # b <=> a % g b
+-- See <https://ncatlab.org/nlab/show/idempotent+adjunction>
+idempotentL :: (Preorder a, Preorder b) => ConnL a b -> a -> b -> Bool
+idempotentL c@(ConnL f g) a b = projective (~~) g (upper1 c id) b && projective (~~) f (ceiling1 c id) a
 
--- | \( \forall a: f (g a) \sim a \)
-invertible :: Rel s b -> (s -> r) -> (r -> s) -> s -> b
-invertible (#) f g a = g (f a) # a
+idempotentR :: (Preorder a, Preorder b) => ConnR a b -> a -> b -> Bool
+idempotentR c@(ConnR f g) a b = projective (~~) g (floor1 c id) a && projective (~~) f (lower1 c id) b
 
+idempotent :: (Preorder a, Preorder b) => (forall k. Conn k a b) -> a -> b -> Bool
+idempotent t a b = idempotentL t a b && idempotentR t a b
+
 -- | \( \forall a: g \circ f (a) \sim f (a) \)
---
--- > idempotent (#) f = projective (#) f f
 projective :: Rel s b -> (r -> s) -> (s -> s) -> r -> b
 projective (#) f g r = g (f r) # f r
diff --git a/src/Data/Connection/Ratio.hs b/src/Data/Connection/Ratio.hs
--- a/src/Data/Connection/Ratio.hs
+++ b/src/Data/Connection/Ratio.hs
@@ -2,21 +2,23 @@
 {-# LANGUAGE Safe #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE ViewPatterns #-}
 
 module Data.Connection.Ratio (
     Ratio (..),
     reduce,
-    shiftd,
+    shiftr,
 
     -- * Rational
-    ratf32,
-    ratf64,
     rati08,
     rati16,
     rati32,
     rati64,
     ratixx,
     ratint,
+    ratfix,
+    ratf32,
+    ratf64,
 
     -- * Positive
     posw08,
@@ -27,18 +29,19 @@
     posnat,
 ) where
 
-import safe Data.Connection.Conn
-import safe qualified Data.Connection.Float as Float
+import safe Data.Connection.Conn hiding (ceiling, floor)
+import safe Data.Connection.Fixed
+import safe Data.Connection.Float as Float
 import safe Data.Int
 import safe Data.Order
 import safe Data.Order.Extended
 import safe Data.Order.Syntax
+import safe Data.Proxy
 import safe Data.Ratio
 import safe Data.Word
 import safe GHC.Real (Ratio (..), Rational)
 import safe Numeric.Natural
-import safe Prelude hiding (Ord (..), until)
-import safe qualified Prelude as P
+import safe Prelude hiding (Eq (..), Ord (..), until)
 
 -- | A total version of 'GHC.Real.reduce'.
 reduce :: Integral a => Ratio a -> Ratio a
@@ -48,74 +51,89 @@
 -- | Shift by n 'units of least precision' where the ULP is determined by the denominator
 --
 -- This is an analog of 'Data.Connection.Float.shift32' for rationals.
-shiftd :: Num a => a -> Ratio a -> Ratio a
-shiftd n (x :% y) = (n + x) :% y
+shiftr :: Num a => a -> Ratio a -> Ratio a
+shiftr n (x :% y) = (n + x) :% y
 
 ---------------------------------------------------------------------
 -- Ratio Integer
 ---------------------------------------------------------------------
 
 rati08 :: Conn k Rational (Extended Int8)
-rati08 = signedTriple
+rati08 = tripleI
 
 rati16 :: Conn k Rational (Extended Int16)
-rati16 = signedTriple
+rati16 = tripleI
 
 rati32 :: Conn k Rational (Extended Int32)
-rati32 = signedTriple
+rati32 = tripleI
 
 rati64 :: Conn k Rational (Extended Int64)
-rati64 = signedTriple
+rati64 = tripleI
 
 ratixx :: Conn k Rational (Extended Int)
-ratixx = signedTriple
+ratixx = tripleI
 
 ratint :: Conn k Rational (Extended Integer)
 ratint = Conn f g h
   where
-    f = liftExtended (~~ ninf) (\x -> x ~~ nan || x ~~ pinf) P.ceiling
+    f = liftExtended (~~ ninf) (\x -> x ~~ nan || x ~~ pinf) ceiling
 
-    g = extended ninf pinf P.fromIntegral
+    g = extended ninf pinf fromIntegral
 
-    h = liftExtended (\x -> x ~~ nan || x ~~ ninf) (~~ pinf) P.floor
+    h = liftExtended (\x -> x ~~ nan || x ~~ ninf) (~~ pinf) floor
 
+ratfix :: forall e k. HasResolution e => Conn k Rational (Extended (Fixed e))
+ratfix = Conn f' g h'
+  where
+    prec = resolution (Proxy :: Proxy e)
+
+    f (reduce . (* (toRational prec)) -> n :% d) = MkFixed $ let i = n `div` d in if n `mod` d == 0 then i else i + 1
+
+    f' = liftExtended (~~ ninf) (\x -> x ~~ nan || x ~~ pinf) f
+
+    g = extended ninf pinf toRational
+
+    h (reduce . (* (toRational prec)) -> n :% d) = MkFixed $ n `div` d
+
+    h' = liftExtended (\x -> x ~~ nan || x ~~ ninf) (~~ pinf) h
+
 ratf32 :: Conn k Rational Float
-ratf32 = Conn (toFloating f) (fromFloating g) (toFloating h)
+ratf32 = Conn (toFractional f) (fromFractional g) (toFractional h)
   where
     f x =
-        let est = P.fromRational x
-         in if fromFloating g est >~ x
+        let est = fromRational x
+         in if fromFractional g est >~ x
                 then est
-                else ascendf est (fromFloating g) x
+                else ascendf est (fromFractional g) x
 
     g = flip approxRational 0
 
     h x =
-        let est = P.fromRational x
-         in if fromFloating g est <~ x
+        let est = fromRational x
+         in if fromFractional g est <~ x
                 then est
-                else descendf est (fromFloating g) x
+                else descendf est (fromFractional g) x
 
     ascendf z g1 y = Float.until (\x -> g1 x >~ y) (<~) (Float.shift32 1) z
 
     descendf z f1 x = Float.until (\y -> f1 y <~ x) (>~) (Float.shift32 (-1)) z
 
 ratf64 :: Conn k Rational Double
-ratf64 = Conn (toFloating f) (fromFloating g) (toFloating h)
+ratf64 = Conn (toFractional f) (fromFractional g) (toFractional h)
   where
     f x =
-        let est = P.fromRational x
-         in if fromFloating g est >~ x
+        let est = fromRational x
+         in if fromFractional g est >~ x
                 then est
-                else ascendf est (fromFloating g) x
+                else ascendf est (fromFractional g) x
 
     g = flip approxRational 0
 
     h x =
-        let est = P.fromRational x
-         in if fromFloating g est <~ x
+        let est = fromRational x
+         in if fromFractional g est <~ x
                 then est
-                else descendf est (fromFloating g) x
+                else descendf est (fromFractional g) x
 
     ascendf z g1 y = Float.until (\x -> g1 x >~ y) (<~) (Float.shift64 1) z
 
@@ -126,28 +144,28 @@
 ---------------------------------------------------------------------
 
 posw08 :: Conn k Positive (Lowered Word8)
-posw08 = unsignedTriple
+posw08 = tripleW
 
 posw16 :: Conn k Positive (Lowered Word16)
-posw16 = unsignedTriple
+posw16 = tripleW
 
 posw32 :: Conn k Positive (Lowered Word32)
-posw32 = unsignedTriple
+posw32 = tripleW
 
 posw64 :: Conn k Positive (Lowered Word64)
-posw64 = unsignedTriple
+posw64 = tripleW
 
 poswxx :: Conn k Positive (Lowered Word)
-poswxx = unsignedTriple
+poswxx = tripleW
 
 posnat :: Conn k Positive (Lowered Natural)
 posnat = Conn f g h
   where
-    f = liftEitherR (\x -> x ~~ nan || x ~~ pinf) P.ceiling
+    f = liftEitherR (\x -> x ~~ nan || x ~~ pinf) ceiling
 
-    g = either P.fromIntegral (const pinf)
+    g = either fromIntegral (const pinf)
 
-    h = liftEitherR (~~ pinf) $ \x -> if x ~~ nan then 0 else P.floor x
+    h = liftEitherR (~~ pinf) $ \x -> if x ~~ nan then 0 else floor x
 
 ---------------------------------------------------------------------
 -- Internal
@@ -162,45 +180,45 @@
 nan :: Num a => Ratio a
 nan = 0 :% 0
 
-unsignedTriple :: forall a k. (Bounded a, Integral a) => Conn k Positive (Lowered a)
-unsignedTriple = Conn f g h
+tripleW :: forall a k. (Bounded a, Integral a) => Conn k Positive (Lowered a)
+tripleW = Conn f g h
   where
     f x
         | x ~~ nan = Right maxBound
         | x > high = Right maxBound
-        | otherwise = Left $ P.ceiling x
+        | otherwise = Left $ ceiling x
 
-    g = either P.fromIntegral (const pinf)
+    g = either fromIntegral (const pinf)
 
     h x
         | x ~~ nan = Left minBound
         | x ~~ pinf = Right maxBound
         | x > high = Left maxBound
-        | otherwise = Left $ P.floor x
+        | otherwise = Left $ floor x
 
-    high = P.fromIntegral @a maxBound
+    high = fromIntegral @a maxBound
 
-signedTriple :: forall a k. (Bounded a, Integral a) => Conn k Rational (Extended a)
-signedTriple = Conn f g h
+tripleI :: forall a k. (Bounded a, Integral a) => Conn k Rational (Extended a)
+tripleI = Conn f g h
   where
-    f = liftExtended (~~ ninf) (\x -> x ~~ nan || x > high) $ \x -> if x < low then minBound else P.ceiling x
+    f = liftExtended (~~ ninf) (\x -> x ~~ nan || x > high) $ \x -> if x < low then minBound else ceiling x
 
-    g = extended ninf pinf P.fromIntegral
+    g = extended ninf pinf fromIntegral
 
-    h = liftExtended (\x -> x ~~ nan || x < low) (~~ pinf) $ \x -> if x > high then maxBound else P.floor x
+    h = liftExtended (\x -> x ~~ nan || x < low) (~~ pinf) $ \x -> if x > high then maxBound else floor x
 
-    high = P.fromIntegral @a maxBound
+    high = fromIntegral @a maxBound
     low = -1 - high
 
-toFloating :: Fractional a => (Rational -> a) -> Rational -> a
-toFloating f x
+toFractional :: Fractional a => (Rational -> a) -> Rational -> a
+toFractional f x
     | x ~~ nan = 0 / 0
     | x ~~ ninf = (-1) / 0
     | x ~~ pinf = 1 / 0
     | otherwise = f x
 
-fromFloating :: (Order a, Fractional a) => (a -> Rational) -> a -> Rational
-fromFloating f x
+fromFractional :: (Order a, Fractional a) => (a -> Rational) -> a -> Rational
+fromFractional f x
     | x ~~ 0 / 0 = nan
     | x ~~ (-1) / 0 = ninf
     | x ~~ 1 / 0 = pinf
@@ -221,9 +239,9 @@
 ratpos :: Conn k Rational Positive
 ratpos = Conn k f g h where
 
-  f = liftExtended (~~ ninf) (\x -> x ~~ nan || x ~~ pinf) P.ceiling
+  f = liftExtended (~~ ninf) (\x -> x ~~ nan || x ~~ pinf) ceiling
 
-  g = extended minBound maxBound P.fromIntegral
+  g = extended minBound maxBound fromIntegral
 
-  h = liftExtended (\x -> x ~~ nan || x ~~ ninf) (~~ pinf) P.floor
+  h = liftExtended (\x -> x ~~ nan || x ~~ ninf) (~~ pinf) floor
 -}
diff --git a/src/Data/Lattice.hs b/src/Data/Lattice.hs
--- a/src/Data/Lattice.hs
+++ b/src/Data/Lattice.hs
@@ -60,7 +60,7 @@
 
 import safe Data.Bifunctor (bimap)
 import safe Data.Bool hiding (not)
-import safe Data.Connection.Class
+import safe Data.Connection.Class hiding ((/\), (\/))
 import safe Data.Connection.Conn
 import safe Data.Either
 import safe Data.Int
@@ -72,7 +72,7 @@
 import safe Data.Order.Syntax
 import safe qualified Data.Set as Set
 import safe Data.Word
-import safe Prelude hiding (Eq (..), Ord (..), not)
+import safe Prelude hiding (Eq (..), Ord (..), ceiling, floor, not)
 import safe qualified Prelude as P
 
 -------------------------------------------------------------------------------
@@ -161,31 +161,31 @@
 
 -- | Lattice meet.
 --
--- > (/\) = curry $ floorWith semilattice
+-- > (/\) = curry $ floor semilattice
 (/\) :: Meet a => a -> a -> a
-(/\) = curry $ floorWith semilattice
+(/\) = curry $ floor semilattice
 
 -- | The unique top element of a bounded lattice
 --
 -- > x /\ top = x
 -- > x \/ top = top
 top :: Meet a => a
-top = floorWith bounded ()
+top = floor bounded ()
 
 infixr 5 \/
 
 -- | Lattice join.
 --
--- > (\/) = curry $ ceilingWith semilattice
+-- > (\/) = curry $ lower semilattice
 (\/) :: Join a => a -> a -> a
-(\/) = curry $ ceilingWith semilattice
+(\/) = curry $ ceiling semilattice
 
 -- | The unique bottom element of a bounded lattice
 --
 -- > x /\ bottom = bottom
 -- > x \/ bottom = x
 bottom :: Join a => a
-bottom = ceilingWith bounded ()
+bottom = ceiling bounded ()
 
 -------------------------------------------------------------------------------
 -- Heyting algebras
@@ -278,7 +278,7 @@
 -- >>> True // True
 -- True
 (//) :: Algebra 'R a => a -> a -> a
-(//) = floorWith . algebra
+(//) = floor . algebra
 
 -- | Intuitionistic equivalence.
 --
@@ -363,7 +363,7 @@
 -- >>> [GT,EQ] \\ [LT]
 -- fromList [EQ,GT]
 (\\) :: Algebra 'L a => a -> a -> a
-(\\) = flip $ ceilingWith . algebra
+(\\) = flip $ ceiling . algebra
 
 -- | Intuitionistic co-equivalence.
 equiv :: Algebra 'L a => a -> a -> a
@@ -513,7 +513,6 @@
     not LT = GT
     not EQ = EQ
     not GT = LT
-instance Boolean Ordering
 
 instance Semilattice k Word8
 instance Algebra 'L Word8 where algebra = coheyting impliesL
@@ -678,7 +677,7 @@
 
     semilattice = ConnL f fork
       where
-        f = uncurry $ Map.unionWith (curry $ ceilingWith semilattice)
+        f = uncurry $ Map.unionWith (curry $ ceiling semilattice)
 
 instance (Total k, Join a) => Algebra 'L (Map.Map k a) where
     algebra = coheyting (Map.\\)
@@ -688,7 +687,7 @@
 
     semilattice = ConnL f fork
       where
-        f = uncurry $ IntMap.unionWith (curry $ ceilingWith semilattice)
+        f = uncurry $ IntMap.unionWith (curry $ ceiling semilattice)
 
 instance (Join a) => Algebra 'L (IntMap.IntMap a) where
     algebra = coheyting (IntMap.\\)
diff --git a/src/Data/Order.hs b/src/Data/Order.hs
--- a/src/Data/Order.hs
+++ b/src/Data/Order.hs
@@ -36,6 +36,7 @@
 import safe Data.Complex
 import safe Data.Either
 import safe qualified Data.Eq as Eq
+import safe Data.Fixed
 import safe Data.Functor.Identity
 import safe Data.Int
 import safe qualified Data.IntMap as IntMap
@@ -287,7 +288,20 @@
 deriving via (Base Int64) instance Preorder Int64
 deriving via (Base Integer) instance Preorder Integer
 
---TODO move to Order and derive Preorder as well
+deriving via (Base (Fixed e)) instance Preorder (Fixed e)
+
+-- | An < https://en.wikipedia.org/wiki/Modular_lattice#Examples /N5/ > lattice.
+--
+--  A non-modular lattice formed by the < https://en.wikipedia.org/wiki/Extended_real_number_line affine extended >
+--  reals along with a /NaN/ value that is incomparable to any finite number, i.e.:
+--
+--  > pcompare (N5 NaN) (N5 x) = pcompare (N5 x) (N5 NaN) = Nothing
+--
+--  for any finite /x/.
+--
+--  > N5 NaN == N5 NaN = True
+--  > N5 NaN < N5 (1/0) = True
+--  > N5 NaN > N5 (-1/0) = True
 newtype N5 a = N5 {getN5 :: a}
     deriving stock (Eq, Show, Functor)
     deriving (Applicative) via Identity
diff --git a/test/Test/Data/Connection.hs b/test/Test/Data/Connection.hs
--- a/test/Test/Data/Connection.hs
+++ b/test/Test/Data/Connection.hs
@@ -11,6 +11,7 @@
 import Data.Lattice
 import Data.Int
 import Data.Word
+import Data.Fixed
 import Data.Order
 import Data.Order.Extended
 import Data.Order.Interval
@@ -53,9 +54,11 @@
 f64 = gen_flt $ G.double rd
 
 rat :: Gen (Ratio Integer)
-rat = G.frequency [(49, gen), (1, G.element [-1 :% 0, 1 :% 0, 0 :% 0])]
-  where gen = G.realFrac_ (R.linearFracFrom 0 (- 2^127) (2^127))
+rat = G.realFrac_ $ R.linearFracFrom 0 (- 2^(127 :: Integer)) (2^(127 :: Integer))
 
+rat' :: Gen (Ratio Integer)
+rat' = G.frequency [(49, rat), (1, G.element [-1 :% 0, 1 :% 0, 0 :% 0])]
+
 pos :: Gen (Ratio Natural)
 pos = G.frequency [(49, gen), (1, G.element [1 :% 0, 0 :% 0])]
   where gen = G.realFrac_ (R.linearFracFrom 0 0 (2^127))
@@ -85,8 +88,8 @@
   x' <- forAll f32
   o <- forAll ord
   o' <- forAll ord
-  r <- forAll rat
-  r' <- forAll rat
+  r <- forAll rat'
+  r' <- forAll rat'
 
   assert $ Prop.adjoint (conn @_ @() @Ordering) () o
   assert $ Prop.closed (conn @_ @() @Ordering) ()
diff --git a/test/Test/Data/Connection/Fixed.hs b/test/Test/Data/Connection/Fixed.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Data/Connection/Fixed.hs
@@ -0,0 +1,153 @@
+{-# LANGUAGE TemplateHaskell #-}
+
+module Test.Data.Connection.Fixed where
+
+import Data.Connection.Fixed
+import qualified Data.Connection.Property as Prop
+import Hedgehog
+import qualified Hedgehog.Gen as G
+import Test.Data.Connection
+
+fxx :: Gen (Fixed k)
+fxx = MkFixed <$> G.integral ri'
+
+prop_connections_micro :: Property
+prop_connections_micro = withTests 1000 . property $ do
+    f00 <- forAll fxx
+    f01 <- forAll fxx
+    f02 <- forAll fxx
+    f03 <- forAll fxx
+    f06 <- forAll fxx
+
+    f00' <- forAll fxx
+    f01' <- forAll fxx
+    f02' <- forAll fxx
+    f03' <- forAll fxx
+    f06' <- forAll fxx
+
+    assert $ Prop.adjoint f06f00 f06 f00
+    assert $ Prop.closed f06f00 f06
+    assert $ Prop.kernel f06f00 f00
+    assert $ Prop.monotonic f06f00 f06 f06' f00 f00'
+    assert $ Prop.idempotent f06f00 f06 f00
+
+    assert $ Prop.adjoint f06f01 f06 f01
+    assert $ Prop.closed f06f01 f06
+    assert $ Prop.kernel f06f01 f01
+    assert $ Prop.monotonic f06f01 f06 f06' f01 f01'
+    assert $ Prop.idempotent f06f01 f06 f01
+
+    assert $ Prop.adjoint f06f02 f06 f02
+    assert $ Prop.closed f06f02 f06
+    assert $ Prop.kernel f06f02 f02
+    assert $ Prop.monotonic f06f02 f06 f06' f02 f02'
+    assert $ Prop.idempotent f06f02 f06 f02
+
+    assert $ Prop.adjoint f06f03 f06 f03
+    assert $ Prop.closed f06f03 f06
+    assert $ Prop.kernel f06f03 f03
+    assert $ Prop.monotonic f06f03 f06 f06' f03 f03'
+    assert $ Prop.idempotent f06f03 f06 f03
+
+prop_connections_nano :: Property
+prop_connections_nano = withTests 1000 . property $ do
+    f00 <- forAll fxx
+    f01 <- forAll fxx
+    f02 <- forAll fxx
+    f03 <- forAll fxx
+    f06 <- forAll fxx
+    f09 <- forAll fxx
+
+    f00' <- forAll fxx
+    f01' <- forAll fxx
+    f02' <- forAll fxx
+    f03' <- forAll fxx
+    f06' <- forAll fxx
+    f09' <- forAll fxx
+
+    assert $ Prop.adjoint f09f00 f09 f00
+    assert $ Prop.closed f09f00 f09
+    assert $ Prop.kernel f09f00 f00
+    assert $ Prop.monotonic f09f00 f09 f09' f00 f00'
+    assert $ Prop.idempotent f09f00 f09 f00
+
+    assert $ Prop.adjoint f09f01 f09 f01
+    assert $ Prop.closed f09f01 f09
+    assert $ Prop.kernel f09f01 f01
+    assert $ Prop.monotonic f09f01 f09 f09' f01 f01'
+    assert $ Prop.idempotent f09f01 f09 f01
+
+    assert $ Prop.adjoint f09f02 f09 f02
+    assert $ Prop.closed f09f02 f09
+    assert $ Prop.kernel f09f02 f02
+    assert $ Prop.monotonic f09f02 f09 f09' f02 f02'
+    assert $ Prop.idempotent f09f02 f09 f02
+
+    assert $ Prop.adjoint f09f03 f09 f03
+    assert $ Prop.closed f09f03 f09
+    assert $ Prop.kernel f09f03 f03
+    assert $ Prop.monotonic f09f03 f09 f09' f03 f03'
+    assert $ Prop.idempotent f09f03 f09 f03
+
+    assert $ Prop.adjoint f09f06 f09 f06
+    assert $ Prop.closed f09f06 f09
+    assert $ Prop.kernel f09f06 f06
+    assert $ Prop.monotonic f09f06 f09 f09' f06 f06'
+    assert $ Prop.idempotent f09f06 f09 f06
+
+prop_connections_pico :: Property
+prop_connections_pico = withTests 1000 . property $ do
+    f00 <- forAll fxx
+    f01 <- forAll fxx
+    f02 <- forAll fxx
+    f03 <- forAll fxx
+    f06 <- forAll fxx
+    f09 <- forAll fxx
+    f12 <- forAll fxx
+
+    f00' <- forAll fxx
+    f01' <- forAll fxx
+    f02' <- forAll fxx
+    f03' <- forAll fxx
+    f06' <- forAll fxx
+    f09' <- forAll fxx
+    f12' <- forAll fxx
+
+    assert $ Prop.adjoint f12f00 f12 f00
+    assert $ Prop.closed f12f00 f12
+    assert $ Prop.kernel f12f00 f00
+    assert $ Prop.monotonic f12f00 f12 f12' f00 f00'
+    assert $ Prop.idempotent f12f00 f12 f00
+
+    assert $ Prop.adjoint f12f01 f12 f01
+    assert $ Prop.closed f12f01 f12
+    assert $ Prop.kernel f12f01 f01
+    assert $ Prop.monotonic f12f01 f12 f12' f01 f01'
+    assert $ Prop.idempotent f12f01 f12 f01
+
+    assert $ Prop.adjoint f12f02 f12 f02
+    assert $ Prop.closed f12f02 f12
+    assert $ Prop.kernel f12f02 f02
+    assert $ Prop.monotonic f12f02 f12 f12' f02 f02'
+    assert $ Prop.idempotent f12f02 f12 f02
+
+    assert $ Prop.adjoint f12f03 f12 f03
+    assert $ Prop.closed f12f03 f12
+    assert $ Prop.kernel f12f03 f03
+    assert $ Prop.monotonic f12f03 f12 f12' f03 f03'
+    assert $ Prop.idempotent f12f03 f12 f03
+
+    assert $ Prop.adjoint f12f06 f12 f06
+    assert $ Prop.closed f12f06 f12
+    assert $ Prop.kernel f12f06 f06
+    assert $ Prop.monotonic f12f06 f12 f12' f06 f06'
+    assert $ Prop.idempotent f12f06 f12 f06
+
+    assert $ Prop.adjoint f12f09 f12 f09
+    assert $ Prop.closed f12f09 f12
+    assert $ Prop.kernel f12f09 f09
+    assert $ Prop.monotonic f12f09 f12 f12' f09 f09'
+    assert $ Prop.idempotent f12f09 f12 f09
+
+tests :: IO Bool
+tests = checkParallel $$(discover)
diff --git a/test/Test/Data/Connection/Float.hs b/test/Test/Data/Connection/Float.hs
--- a/test/Test/Data/Connection/Float.hs
+++ b/test/Test/Data/Connection/Float.hs
@@ -1,93 +1,188 @@
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE ViewPatterns #-}
+
 module Test.Data.Connection.Float where
 
 import Data.Connection.Conn
 import Data.Connection.Float
+import Data.Fixed
 import Data.Int
-import Hedgehog
-import Prelude hiding (Ord(..),Bounded, until)
-import Test.Data.Connection
+import Data.Order
+
 import qualified Data.Connection.Property as Prop
+import Hedgehog
 import qualified Hedgehog.Gen as G
-
+import Test.Data.Connection
 
 prop_connection_f32i08 :: Property
 prop_connection_f32i08 = withTests 1000 . property $ do
-  x <- forAll f32
-  x' <- forAll f32
-  y <- forAll $ gen_extended $ G.integral (ri @Int8)
-  y' <- forAll $ gen_extended $ G.integral (ri @Int8)
+    x <- forAll f32
+    x' <- forAll f32
+    y <- forAll $ gen_extended $ G.integral (ri @Int8)
+    y' <- forAll $ gen_extended $ G.integral (ri @Int8)
 
-  assert $ Prop.adjoint (f32i08) x y
-  assert $ Prop.closed (f32i08) x
-  assert $ Prop.kernel (f32i08) y
-  assert $ Prop.monotonic (f32i08) x x' y y'
-  assert $ Prop.idempotent (f32i08) x y
+    assert $ Prop.adjoint f32i08 x y
+    assert $ Prop.closed f32i08 x
+    assert $ Prop.kernel f32i08 y
+    assert $ Prop.monotonic f32i08 x x' y y'
+    assert $ Prop.idempotent f32i08 x y
 
 prop_connection_f32i16 :: Property
 prop_connection_f32i16 = withTests 1000 . property $ do
-  x <- forAll f32
-  x' <- forAll f32
-  y <- forAll $ gen_extended $ G.integral (ri @Int16)
-  y' <- forAll $ gen_extended $ G.integral (ri @Int16)
+    x <- forAll f32
+    x' <- forAll f32
+    y <- forAll $ gen_extended $ G.integral (ri @Int16)
+    y' <- forAll $ gen_extended $ G.integral (ri @Int16)
 
-  assert $ Prop.adjoint (f32i16) x y
-  assert $ Prop.closed (f32i16) x
-  assert $ Prop.kernel (f32i16) y
-  assert $ Prop.monotonic (f32i16) x x' y y'
-  assert $ Prop.idempotent (f32i16) x y
+    assert $ Prop.adjoint f32i16 x y
+    assert $ Prop.closed f32i16 x
+    assert $ Prop.kernel f32i16 y
+    assert $ Prop.monotonic f32i16 x x' y y'
+    assert $ Prop.idempotent f32i16 x y
 
+prop_connection_f32i32 :: Property
+prop_connection_f32i32 = withTests 1000 . property $ do
+    x <- forAll f32
+    x' <- forAll f32
+    y <- forAll $ gen_extended $ G.integral (ri @Int32)
+    y' <- forAll $ gen_extended $ G.integral (ri @Int32)
+
+    assert $ Prop.adjointL f32i32 x y
+    assert $ Prop.closedL f32i32 x
+    assert $ Prop.kernelL f32i32 y
+    assert $ Prop.monotonicL f32i32 x x' y y'
+    assert $ Prop.idempotentL f32i32 x y
+
+prop_connection_f32i64 :: Property
+prop_connection_f32i64 = withTests 1000 . property $ do
+    x <- forAll f32
+    x' <- forAll f32
+    y <- forAll $ gen_extended $ G.integral (ri @Int64)
+    y' <- forAll $ gen_extended $ G.integral (ri @Int64)
+
+    assert $ Prop.adjointL f32i64 x y
+    assert $ Prop.closedL f32i64 x
+    assert $ Prop.kernelL f32i64 y
+    assert $ Prop.monotonicL f32i64 x x' y y'
+    assert $ Prop.idempotentL f32i64 x y
+
+prop_connection_f32ixx :: Property
+prop_connection_f32ixx = withTests 1000 . property $ do
+    x <- forAll f32
+    x' <- forAll f32
+    y <- forAll $ gen_extended $ G.integral (ri @Int)
+    y' <- forAll $ gen_extended $ G.integral (ri @Int)
+
+    assert $ Prop.adjointL f32ixx x y
+    assert $ Prop.closedL f32ixx x
+    assert $ Prop.kernelL f32ixx y
+    assert $ Prop.monotonicL f32ixx x x' y y'
+    assert $ Prop.idempotentL f32ixx x y
+
+prop_connection_f32int :: Property
+prop_connection_f32int = withTests 1000 . property $ do
+    x <- forAll f32
+    x' <- forAll f32
+    y <- forAll $ gen_extended $ G.integral ri'
+    y' <- forAll $ gen_extended $ G.integral ri'
+
+    assert $ Prop.adjointL f32int x y
+    assert $ Prop.closedL f32int x
+    assert $ Prop.kernelL f32int y
+    assert $ Prop.monotonicL f32int x x' y y'
+    assert $ Prop.idempotentL f32int x y
+
 prop_connection_f64i08 :: Property
 prop_connection_f64i08 = withTests 1000 . property $ do
-  x <- forAll f64
-  x' <- forAll f64
-  y <- forAll $ gen_extended $ G.integral (ri @Int8)
-  y' <- forAll $ gen_extended $ G.integral (ri @Int8)
+    x <- forAll f64
+    x' <- forAll f64
+    y <- forAll $ gen_extended $ G.integral (ri @Int8)
+    y' <- forAll $ gen_extended $ G.integral (ri @Int8)
 
-  assert $ Prop.adjoint (f64i08) x y
-  assert $ Prop.closed (f64i08) x
-  assert $ Prop.kernel (f64i08) y
-  assert $ Prop.monotonic (f64i08) x x' y y'
-  assert $ Prop.idempotent (f64i08) x y
+    assert $ Prop.adjoint f64i08 x y
+    assert $ Prop.closed f64i08 x
+    assert $ Prop.kernel f64i08 y
+    assert $ Prop.monotonic f64i08 x x' y y'
+    assert $ Prop.idempotent f64i08 x y
 
 prop_connection_f64i16 :: Property
 prop_connection_f64i16 = withTests 1000 . property $ do
-  x <- forAll f64
-  x' <- forAll f64
-  y <- forAll $ gen_extended $ G.integral (ri @Int16)
-  y' <- forAll $ gen_extended $ G.integral (ri @Int16)
+    x <- forAll f64
+    x' <- forAll f64
+    y <- forAll $ gen_extended $ G.integral (ri @Int16)
+    y' <- forAll $ gen_extended $ G.integral (ri @Int16)
 
-  assert $ Prop.adjoint (f64i16) x y
-  assert $ Prop.closed (f64i16) x
-  assert $ Prop.kernel (f64i16) y
-  assert $ Prop.monotonic (f64i16) x x' y y'
-  assert $ Prop.idempotent (f64i16) x y
+    assert $ Prop.adjoint f64i16 x y
+    assert $ Prop.closed f64i16 x
+    assert $ Prop.kernel f64i16 y
+    assert $ Prop.monotonic f64i16 x x' y y'
+    assert $ Prop.idempotent f64i16 x y
 
 prop_connection_f64i32 :: Property
 prop_connection_f64i32 = withTests 1000 . property $ do
-  x <- forAll f64
-  x' <- forAll f64
-  y <- forAll $ gen_extended $ G.integral (ri @Int32)
-  y' <- forAll $ gen_extended $ G.integral (ri @Int32)
+    x <- forAll f64
+    x' <- forAll f64
+    y <- forAll $ gen_extended $ G.integral (ri @Int32)
+    y' <- forAll $ gen_extended $ G.integral (ri @Int32)
 
-  assert $ Prop.adjoint (f64i32) x y
-  assert $ Prop.closed (f64i32) x
-  assert $ Prop.kernel (f64i32) y
-  assert $ Prop.monotonic (f64i32) x x' y y'
-  assert $ Prop.idempotent (f64i32) x y
+    assert $ Prop.adjoint f64i32 x y
+    assert $ Prop.closed f64i32 x
+    assert $ Prop.kernel f64i32 y
+    assert $ Prop.monotonic f64i32 x x' y y'
+    assert $ Prop.idempotent f64i32 x y
 
+prop_connection_f64i64 :: Property
+prop_connection_f64i64 = withTests 1000 . property $ do
+    x <- forAll f64
+    x' <- forAll f64
+    y <- forAll $ gen_extended $ G.integral (ri @Int64)
+    y' <- forAll $ gen_extended $ G.integral (ri @Int64)
+
+    assert $ Prop.adjointL f64i64 x y
+    assert $ Prop.closedL f64i64 x
+    assert $ Prop.kernelL f64i64 y
+    assert $ Prop.monotonicL f64i64 x x' y y'
+    assert $ Prop.idempotentL f64i64 x y
+
+prop_connection_f64ixx :: Property
+prop_connection_f64ixx = withTests 1000 . property $ do
+    x <- forAll f64
+    x' <- forAll f64
+    y <- forAll $ gen_extended $ G.integral (ri @Int)
+    y' <- forAll $ gen_extended $ G.integral (ri @Int)
+
+    assert $ Prop.adjointL f64ixx x y
+    assert $ Prop.closedL f64ixx x
+    assert $ Prop.kernelL f64ixx y
+    assert $ Prop.monotonicL f64ixx x x' y y'
+    assert $ Prop.idempotentL f64ixx x y
+
+prop_connection_f64int :: Property
+prop_connection_f64int = withTests 1000 . property $ do
+    x <- forAll f64
+    x' <- forAll f64
+    y <- forAll $ gen_extended $ G.integral ri'
+    y' <- forAll $ gen_extended $ G.integral ri'
+
+    assert $ Prop.adjointL f64int x y
+    assert $ Prop.closedL f64int x
+    assert $ Prop.kernelL f64int y
+    assert $ Prop.monotonicL f64int x x' y y'
+    assert $ Prop.idempotentL f64int x y
+
 prop_connection_f64f32 :: Property
 prop_connection_f64f32 = withTests 1000 . property $ do
-  x <- forAll f64
-  x' <- forAll f64
-  y <- forAll f32
-  y' <- forAll f32
+    x <- forAll f64
+    x' <- forAll f64
+    y <- forAll f32
+    y' <- forAll f32
 
-  assert $ Prop.adjoint (f64f32) x y
-  assert $ Prop.closed (f64f32) x
-  assert $ Prop.kernel (f64f32) y
-  assert $ Prop.monotonic (f64f32) x x' y y'
-  assert $ Prop.idempotent (f64f32) x y
+    assert $ Prop.adjoint (f64f32) x y
+    assert $ Prop.closed (f64f32) x
+    assert $ Prop.kernel (f64f32) y
+    assert $ Prop.monotonic (f64f32) x x' y y'
+    assert $ Prop.idempotent (f64f32) x y
 
 tests :: IO Bool
 tests = checkParallel $$(discover)
diff --git a/test/Test/Data/Connection/Ratio.hs b/test/Test/Data/Connection/Ratio.hs
--- a/test/Test/Data/Connection/Ratio.hs
+++ b/test/Test/Data/Connection/Ratio.hs
@@ -1,170 +1,218 @@
 {-# LANGUAGE TemplateHaskell #-}
-{-# Language AllowAmbiguousTypes #-}
+{-# LANGUAGE TypeApplications #-}
+
 module Test.Data.Connection.Ratio where
 
+import qualified Data.Connection.Property as Prop
+import Data.Connection.Ratio
+import Data.Fixed
 import Data.Int
+import Data.Order.Extended
 import Data.Word
-import Data.Connection.Ratio
+import GHC.Real hiding (Fractional (..), div, (^), (^^))
 import Hedgehog
-import Test.Data.Connection
-import qualified Data.Connection.Property as Prop
 import qualified Hedgehog.Gen as G
+import qualified Hedgehog.Range as R
+import Numeric.Natural
+import Test.Data.Connection
 
+fxx :: Gen (Extended (Fixed k))
+fxx = gen_extended $ MkFixed <$> G.integral ri'
+
+prop_connection_ratf06 :: Property
+prop_connection_ratf06 = withTests 1000 . property $ do
+    x <- forAll rat
+    x' <- forAll rat
+    y <- forAll fxx
+    y' <- forAll fxx
+
+    assert $ Prop.adjoint (ratfix @E6) x y
+    assert $ Prop.closed (ratfix @E6) x
+    assert $ Prop.kernel (ratfix @E6) y
+    assert $ Prop.monotonic (ratfix @E6) x x' y y'
+    assert $ Prop.idempotent (ratfix @E6) x y
+
+prop_connection_ratf09 :: Property
+prop_connection_ratf09 = withTests 1000 . property $ do
+    x <- forAll rat
+    x' <- forAll rat
+    y <- forAll fxx
+    y' <- forAll fxx
+
+    assert $ Prop.adjoint (ratfix @E9) x y
+    assert $ Prop.closed (ratfix @E9) x
+    assert $ Prop.kernel (ratfix @E9) y
+    assert $ Prop.monotonic (ratfix @E9) x x' y y'
+    assert $ Prop.idempotent (ratfix @E9) x y
+
+prop_connection_ratf12 :: Property
+prop_connection_ratf12 = withTests 1000 . property $ do
+    x <- forAll rat
+    x' <- forAll rat
+    y <- forAll fxx
+    y' <- forAll fxx
+
+    assert $ Prop.adjoint (ratfix @E12) x y
+    assert $ Prop.closed (ratfix @E12) x
+    assert $ Prop.kernel (ratfix @E12) y
+    assert $ Prop.monotonic (ratfix @E12) x x' y y'
+    assert $ Prop.idempotent (ratfix @E12) x y
+
 prop_connection_ratf32 :: Property
 prop_connection_ratf32 = withTests 1000 . property $ do
-  x <- forAll rat
-  x' <- forAll rat
-  y <- forAll f32
-  y' <- forAll f32
+    x <- forAll rat'
+    x' <- forAll rat'
+    y <- forAll f32
+    y' <- forAll f32
 
-  assert $ Prop.adjoint (ratf32) x y
-  assert $ Prop.closed (ratf32) x
-  assert $ Prop.kernel (ratf32) y
-  assert $ Prop.monotonic (ratf32) x x' y y'
-  assert $ Prop.idempotent (ratf32) x y
+    assert $ Prop.adjoint (ratf32) x y
+    assert $ Prop.closed (ratf32) x
+    assert $ Prop.kernel (ratf32) y
+    assert $ Prop.monotonic (ratf32) x x' y y'
+    assert $ Prop.idempotent (ratf32) x y
 
 prop_connection_ratf64 :: Property
 prop_connection_ratf64 = withTests 1000 . property $ do
-  x <- forAll rat
-  x' <- forAll rat
-  y <- forAll f64
-  y' <- forAll f64
+    x <- forAll rat'
+    x' <- forAll rat'
+    y <- forAll f64
+    y' <- forAll f64
 
-  assert $ Prop.adjoint (ratf64) x y
-  assert $ Prop.closed (ratf64) x
-  assert $ Prop.kernel (ratf64) y
-  assert $ Prop.monotonic (ratf64) x x' y y'
-  assert $ Prop.idempotent (ratf64) x y
+    assert $ Prop.adjoint (ratf64) x y
+    assert $ Prop.closed (ratf64) x
+    assert $ Prop.kernel (ratf64) y
+    assert $ Prop.monotonic (ratf64) x x' y y'
+    assert $ Prop.idempotent (ratf64) x y
 
 prop_connection_rati08 :: Property
 prop_connection_rati08 = withTests 1000 . property $ do
-  x <- forAll rat
-  x' <- forAll rat
-  y <- forAll $ gen_extended $ G.integral (ri @Int8)
-  y' <- forAll $ gen_extended $ G.integral (ri @Int8)
+    x <- forAll rat'
+    x' <- forAll rat'
+    y <- forAll $ gen_extended $ G.integral (ri @Int8)
+    y' <- forAll $ gen_extended $ G.integral (ri @Int8)
 
-  assert $ Prop.adjoint (rati08) x y
-  assert $ Prop.closed (rati08) x
-  assert $ Prop.kernel (rati08) y
-  assert $ Prop.monotonic (rati08) x x' y y'
-  assert $ Prop.idempotent (rati08) x y
+    assert $ Prop.adjoint (rati08) x y
+    assert $ Prop.closed (rati08) x
+    assert $ Prop.kernel (rati08) y
+    assert $ Prop.monotonic (rati08) x x' y y'
+    assert $ Prop.idempotent (rati08) x y
 
 prop_connection_rati16 :: Property
 prop_connection_rati16 = withTests 1000 . property $ do
-  x <- forAll rat
-  x' <- forAll rat
-  y <- forAll $ gen_extended $ G.integral (ri @Int16)
-  y' <- forAll $ gen_extended $ G.integral (ri @Int16)
+    x <- forAll rat'
+    x' <- forAll rat'
+    y <- forAll $ gen_extended $ G.integral (ri @Int16)
+    y' <- forAll $ gen_extended $ G.integral (ri @Int16)
 
-  assert $ Prop.adjoint (rati16) x y
-  assert $ Prop.closed (rati16) x
-  assert $ Prop.kernel (rati16) y
-  assert $ Prop.monotonic (rati16) x x' y y'
-  assert $ Prop.idempotent (rati16) x y
+    assert $ Prop.adjoint (rati16) x y
+    assert $ Prop.closed (rati16) x
+    assert $ Prop.kernel (rati16) y
+    assert $ Prop.monotonic (rati16) x x' y y'
+    assert $ Prop.idempotent (rati16) x y
 
 prop_connection_rati32 :: Property
 prop_connection_rati32 = withTests 1000 . property $ do
-  x <- forAll rat
-  x' <- forAll rat
-  y <- forAll $ gen_extended $ G.integral (ri @Int32)
-  y' <- forAll $ gen_extended $ G.integral (ri @Int32)
+    x <- forAll rat'
+    x' <- forAll rat'
+    y <- forAll $ gen_extended $ G.integral (ri @Int32)
+    y' <- forAll $ gen_extended $ G.integral (ri @Int32)
 
-  assert $ Prop.adjoint (rati32) x y
-  assert $ Prop.closed (rati32) x
-  assert $ Prop.kernel (rati32) y
-  assert $ Prop.monotonic (rati32) x x' y y'
-  assert $ Prop.idempotent (rati32) x y
+    assert $ Prop.adjoint (rati32) x y
+    assert $ Prop.closed (rati32) x
+    assert $ Prop.kernel (rati32) y
+    assert $ Prop.monotonic (rati32) x x' y y'
+    assert $ Prop.idempotent (rati32) x y
 
 prop_connection_rati64 :: Property
 prop_connection_rati64 = withTests 1000 . property $ do
-  x <- forAll rat
-  x' <- forAll rat
-  y <- forAll $ gen_extended $ G.integral (ri @Int64)
-  y' <- forAll $ gen_extended $ G.integral (ri @Int64)
+    x <- forAll rat'
+    x' <- forAll rat'
+    y <- forAll $ gen_extended $ G.integral (ri @Int64)
+    y' <- forAll $ gen_extended $ G.integral (ri @Int64)
 
-  assert $ Prop.adjoint (rati64) x y
-  assert $ Prop.closed (rati64) x
-  assert $ Prop.kernel (rati64) y
-  assert $ Prop.monotonic (rati64) x x' y y'
-  assert $ Prop.idempotent (rati64) x y
+    assert $ Prop.adjoint (rati64) x y
+    assert $ Prop.closed (rati64) x
+    assert $ Prop.kernel (rati64) y
+    assert $ Prop.monotonic (rati64) x x' y y'
+    assert $ Prop.idempotent (rati64) x y
 
 prop_connection_ratint :: Property
 prop_connection_ratint = withTests 1000 . property $ do
-  x <- forAll rat
-  x' <- forAll rat
-  y <- forAll $ gen_extended $ G.integral ri'
-  y' <- forAll $ gen_extended $ G.integral ri'
+    x <- forAll rat'
+    x' <- forAll rat'
+    y <- forAll $ gen_extended $ G.integral ri'
+    y' <- forAll $ gen_extended $ G.integral ri'
 
-  assert $ Prop.adjoint (ratint) x y
-  assert $ Prop.closed (ratint) x
-  assert $ Prop.kernel (ratint) y
-  assert $ Prop.monotonic (ratint) x x' y y'
-  assert $ Prop.idempotent (ratint) x y
+    assert $ Prop.adjoint (ratint) x y
+    assert $ Prop.closed (ratint) x
+    assert $ Prop.kernel (ratint) y
+    assert $ Prop.monotonic (ratint) x x' y y'
+    assert $ Prop.idempotent (ratint) x y
 
 prop_connection_posw08 :: Property
 prop_connection_posw08 = withTests 1000 . property $ do
-  x <- forAll pos
-  x' <- forAll pos
-  y <- forAll $ gen_lowered $ G.integral (ri @Word8)
-  y' <- forAll $ gen_lowered $ G.integral (ri @Word8)
+    x <- forAll pos
+    x' <- forAll pos
+    y <- forAll $ gen_lowered $ G.integral (ri @Word8)
+    y' <- forAll $ gen_lowered $ G.integral (ri @Word8)
 
-  assert $ Prop.adjoint (posw08) x y
-  assert $ Prop.closed (posw08) x
-  assert $ Prop.kernel (posw08) y
-  assert $ Prop.monotonic (posw08) x x' y y'
-  assert $ Prop.idempotent (posw08) x y
+    assert $ Prop.adjoint (posw08) x y
+    assert $ Prop.closed (posw08) x
+    assert $ Prop.kernel (posw08) y
+    assert $ Prop.monotonic (posw08) x x' y y'
+    assert $ Prop.idempotent (posw08) x y
 
 prop_connection_posw16 :: Property
 prop_connection_posw16 = withTests 1000 . property $ do
-  x <- forAll pos
-  x' <- forAll pos
-  y <- forAll $ gen_lowered $ G.integral (ri @Word16)
-  y' <- forAll $ gen_lowered $ G.integral (ri @Word16)
+    x <- forAll pos
+    x' <- forAll pos
+    y <- forAll $ gen_lowered $ G.integral (ri @Word16)
+    y' <- forAll $ gen_lowered $ G.integral (ri @Word16)
 
-  assert $ Prop.adjoint (posw16) x y
-  assert $ Prop.closed (posw16) x
-  assert $ Prop.kernel (posw16) y
-  assert $ Prop.monotonic (posw16) x x' y y'
-  assert $ Prop.idempotent (posw16) x y
+    assert $ Prop.adjoint (posw16) x y
+    assert $ Prop.closed (posw16) x
+    assert $ Prop.kernel (posw16) y
+    assert $ Prop.monotonic (posw16) x x' y y'
+    assert $ Prop.idempotent (posw16) x y
 
 prop_connection_posw32 :: Property
 prop_connection_posw32 = withTests 1000 . property $ do
-  x <- forAll pos
-  x' <- forAll pos
-  y <- forAll $ gen_lowered $ G.integral (ri @Word32)
-  y' <- forAll $ gen_lowered $ G.integral (ri @Word32)
+    x <- forAll pos
+    x' <- forAll pos
+    y <- forAll $ gen_lowered $ G.integral (ri @Word32)
+    y' <- forAll $ gen_lowered $ G.integral (ri @Word32)
 
-  assert $ Prop.adjoint (posw32) x y
-  assert $ Prop.closed (posw32) x
-  assert $ Prop.kernel (posw32) y
-  assert $ Prop.monotonic (posw32) x x' y y'
-  assert $ Prop.idempotent (posw32) x y
+    assert $ Prop.adjoint (posw32) x y
+    assert $ Prop.closed (posw32) x
+    assert $ Prop.kernel (posw32) y
+    assert $ Prop.monotonic (posw32) x x' y y'
+    assert $ Prop.idempotent (posw32) x y
 
 prop_connection_posw64 :: Property
 prop_connection_posw64 = withTests 1000 . property $ do
-  x <- forAll pos
-  x' <- forAll pos
-  y <- forAll $ gen_lowered $ G.integral (ri @Word64)
-  y' <- forAll $ gen_lowered $ G.integral (ri @Word64)
+    x <- forAll pos
+    x' <- forAll pos
+    y <- forAll $ gen_lowered $ G.integral (ri @Word64)
+    y' <- forAll $ gen_lowered $ G.integral (ri @Word64)
 
-  assert $ Prop.adjoint (posw64) x y
-  assert $ Prop.closed (posw64) x
-  assert $ Prop.kernel (posw64) y
-  assert $ Prop.monotonic (posw64) x x' y y'
-  assert $ Prop.idempotent (posw64) x y
+    assert $ Prop.adjoint (posw64) x y
+    assert $ Prop.closed (posw64) x
+    assert $ Prop.kernel (posw64) y
+    assert $ Prop.monotonic (posw64) x x' y y'
+    assert $ Prop.idempotent (posw64) x y
 
 prop_connection_posnat :: Property
 prop_connection_posnat = withTests 1000 . property $ do
-  x <- forAll pos
-  x' <- forAll pos
-  y <- forAll $ gen_lowered $ G.integral rn
-  y' <- forAll $ gen_lowered $ G.integral rn
+    x <- forAll pos
+    x' <- forAll pos
+    y <- forAll $ gen_lowered $ G.integral rn
+    y' <- forAll $ gen_lowered $ G.integral rn
 
-  assert $ Prop.adjoint (posnat) x y
-  assert $ Prop.closed (posnat) x
-  assert $ Prop.kernel (posnat) y
-  assert $ Prop.monotonic (posnat) x x' y y'
-  assert $ Prop.idempotent (posnat) x y
+    assert $ Prop.adjoint (posnat) x y
+    assert $ Prop.closed (posnat) x
+    assert $ Prop.kernel (posnat) y
+    assert $ Prop.monotonic (posnat) x x' y y'
+    assert $ Prop.idempotent (posnat) x y
 
 tests :: IO Bool
 tests = checkParallel $$(discover)
diff --git a/test/Test/Data/Order.hs b/test/Test/Data/Order.hs
--- a/test/Test/Data/Order.hs
+++ b/test/Test/Data/Order.hs
@@ -250,10 +250,10 @@
 
 prop_order_rat :: Property
 prop_order_rat = withTests 1000 . property $ do
-  x <- forAll rat
-  y <- forAll rat
-  z <- forAll rat
-  w <- forAll rat
+  x <- forAll rat'
+  y <- forAll rat'
+  z <- forAll rat'
+  w <- forAll rat'
   assert $ Prop.preorder x y
   assert $ Prop.order z w
   assert $ Prop.reflexive_eq x
diff --git a/test/test.hs b/test/test.hs
--- a/test/test.hs
+++ b/test/test.hs
@@ -3,6 +3,7 @@
 import System.IO (BufferMode (..), hSetBuffering, stderr, stdout)
 
 import qualified Test.Data.Connection as C
+import qualified Test.Data.Connection.Fixed as CX
 import qualified Test.Data.Connection.Float as CF
 import qualified Test.Data.Connection.Int as CI
 import qualified Test.Data.Connection.Ratio as CR
@@ -19,6 +20,7 @@
         , CI.tests
         , CW.tests
         , CF.tests
+        , CX.tests
         , CR.tests
         ]