diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,5 +1,14 @@
 # Revision history for fin
 
+## 0.1.1
+
+- Add `isMin` and `isMax`
+- Add `mirror`, `weakenRight1` and `weakenLeft1`
+- Add `Mult2` and `DivMod2`
+- Explicitly derive `Typeable SNat` and `Typeable LEProof`
+- Derive `Typeable` for `Z` and `S` on GHC-7.8 explicitly
+- Add `QuickCheck` instances for `Nat` and `Fin`
+
 ## 0.1
 
 - Rename `Fin` constructors to `FZ` and `FS`.
diff --git a/fin.cabal b/fin.cabal
--- a/fin.cabal
+++ b/fin.cabal
@@ -1,8 +1,8 @@
 cabal-version:      >=1.10
 name:               fin
-version:            0.1
+version:            0.1.1
 synopsis:           Nat and Fin: peano naturals and finite numbers
-category:           Data, Dependent Types, Singletons
+category:           Data, Dependent Types, Singletons, Math
 description:
   This package provides two simple types, and some tools to work with them.
   Also on type level as @DataKinds@.
@@ -56,11 +56,18 @@
 build-type:         Simple
 extra-source-files: ChangeLog.md
 tested-with:
-  GHC ==8.8.1 || ==8.6.5 || ==8.4.4 || ==8.2.2 || ==8.0.2 || ==7.10.3 || ==7.8.4
+  GHC ==7.8.4
+   || ==7.10.3
+   || ==8.0.2
+   || ==8.2.2
+   || ==8.4.4
+   || ==8.6.5
+   || ==8.8.1
 
 source-repository head
   type:     git
   location: https://github.com/phadej/vec.git
+  subdir:   fin
 
 library
   exposed-modules:
@@ -73,10 +80,11 @@
     Data.Type.Nat.LT
 
   build-depends:
-      base      >=4.7     && <4.13
-    , dec       >=0.0.3   && <0.1
-    , deepseq   >=1.3.0.2 && <1.5
-    , hashable  >=1.2.7.0 && <1.4
+      base        >=4.7     && <4.14
+    , dec         >=0.0.3   && <0.1
+    , deepseq     >=1.3.0.2 && <1.5
+    , hashable    >=1.2.7.0 && <1.4
+    , QuickCheck  >=2.13.2  && <2.14
 
   if !impl(ghc >=8.2)
     build-depends: bifunctors >=5.5.3 && <5.6
@@ -112,6 +120,3 @@
 
   if !impl(ghc >=8.0)
     buildable: False
-
-  -- useful for development
-  ghc-options:
diff --git a/src/Data/Fin.hs b/src/Data/Fin.hs
--- a/src/Data/Fin.hs
+++ b/src/Data/Fin.hs
@@ -5,6 +5,7 @@
 {-# LANGUAGE KindSignatures       #-}
 {-# LANGUAGE ScopedTypeVariables  #-}
 {-# LANGUAGE StandaloneDeriving   #-}
+{-# LANGUAGE TypeOperators        #-}
 {-# LANGUAGE UndecidableInstances #-}
 -- | Finite numbers.
 --
@@ -27,6 +28,7 @@
     toNatural,
     toInteger,
     -- * Interesting
+    mirror,
     inverse,
     universe,
     inlineUniverse,
@@ -36,9 +38,14 @@
     boring,
     -- * Plus
     weakenLeft,
+    weakenLeft1,
     weakenRight,
+    weakenRight1,
     append,
     split,
+    -- * Min and max
+    isMin,
+    isMax,
     -- * Aliases
     fin0, fin1, fin2, fin3, fin4, fin5, fin6, fin7, fin8, fin9,
     ) where
@@ -48,14 +55,19 @@
 import Data.Hashable      (Hashable (..))
 import Data.List.NonEmpty (NonEmpty (..))
 import Data.Proxy         (Proxy (..))
+import Data.Type.Nat      (Nat (..))
 import Data.Typeable      (Typeable)
 import GHC.Exception      (ArithException (..), throw)
 import Numeric.Natural    (Natural)
-import Data.Type.Nat (Nat (..))
 
 import qualified Data.List.NonEmpty as NE
 import qualified Data.Type.Nat      as N
+import qualified Test.QuickCheck    as QC
 
+-------------------------------------------------------------------------------
+-- Type
+-------------------------------------------------------------------------------
+
 -- | Finite numbers: @[0..n-1]@.
 data Fin (n :: Nat) where
     FZ :: Fin ('S n)
@@ -103,7 +115,7 @@
     signum (FS FZ)     = FS FZ
     signum (FS (FS _)) = FS FZ
 
-    fromInteger = unsafeFromNum . (`mod` (N.reflectToNum (Proxy :: Proxy n)))
+    fromInteger = unsafeFromNum . (`mod` N.reflectToNum (Proxy :: Proxy n))
 
     n + m = fromInteger (toInteger n + toInteger m)
     n * m = fromInteger (toInteger n * toInteger m)
@@ -121,6 +133,28 @@
     quotRem a b = (quot a b, 0)
     quot a b = a * inverse b
 
+-- | Mirror the values, 'minBound' becomes 'maxBound', etc.
+--
+-- >>> map mirror universe :: [Fin N.Nat4]
+-- [3,2,1,0]
+--
+-- >>> reverse universe :: [Fin N.Nat4]
+-- [3,2,1,0]
+--
+-- @since 0.1.1
+--
+mirror :: forall n. N.InlineInduction n => Fin n -> Fin n
+mirror = getMirror (N.inlineInduction start step) where
+    start :: Mirror 'Z
+    start = Mirror id
+
+    step :: forall m. N.InlineInduction m => Mirror m -> Mirror ('S m)
+    step (Mirror rec) = Mirror $ \n -> case n of
+        FZ   -> getMaxBound (N.inlineInduction (MaxBound FZ) (MaxBound . FS . getMaxBound))
+        FS m -> weakenLeft1 (rec m)
+
+newtype Mirror n = Mirror { getMirror :: Fin n -> Fin n }
+
 -- | Multiplicative inverse.
 --
 -- Works for @'Fin' n@ where @n@ is coprime with an argument, i.e. in general when @n@ is prime.
@@ -168,6 +202,39 @@
     hashWithSalt salt = hashWithSalt salt . cata (0 :: Integer) succ
 
 -------------------------------------------------------------------------------
+-- QuickCheck
+-------------------------------------------------------------------------------
+
+instance (n ~ 'S m, N.SNatI m) => QC.Arbitrary (Fin n) where
+    arbitrary = getArb $ N.induction (Arb (return FZ)) step where
+        step :: forall p. N.SNatI p => Arb p -> Arb ('S p)
+        step (Arb p) = Arb $ QC.frequency
+            [ (1,                                 return FZ)
+            , (N.reflectToNum (Proxy :: Proxy p), fmap FS p)
+            ]
+
+    shrink = shrink
+
+shrink :: Fin n -> [Fin n]
+shrink FZ      = []
+shrink (FS FZ) = [FZ]
+shrink (FS n)  = map FS (shrink n)
+
+newtype Arb n = Arb { getArb :: QC.Gen (Fin ('S n)) }
+
+instance QC.CoArbitrary (Fin n) where
+    coarbitrary FZ     = QC.variant (0 :: Int)
+    coarbitrary (FS n) = QC.variant (1 :: Int) . QC.coarbitrary n
+
+instance (n ~ 'S m, N.SNatI m) => QC.Function (Fin n) where
+    function = case N.snat :: N.SNat m of
+        N.SZ -> QC.functionMap (\FZ -> ()) (\() -> FZ)
+        N.SS -> QC.functionMap isMin       (maybe FZ FS)
+
+-- TODO: https://github.com/nick8325/quickcheck/pull/283
+-- newtype Fun b m = Fun { getFun :: (Fin ('S m) -> b) -> Fin ('S m) QC.:-> b }
+
+-------------------------------------------------------------------------------
 -- Showing
 -------------------------------------------------------------------------------
 
@@ -286,7 +353,7 @@
 newtype Universe  n = Universe  { getUniverse  :: [Fin n] }
 newtype Universe1 n = Universe1 { getUniverse1 :: NonEmpty (Fin ('S n)) }
 
--- | @'Fin' 'N.Nat0'@ is inhabited.
+-- | @'Fin' 'N.Nat0'@ is not inhabited.
 absurd :: Fin N.Nat0 -> b
 absurd n = case n of {}
 
@@ -298,9 +365,74 @@
 boring = FZ
 
 -------------------------------------------------------------------------------
+-- min and max
+-------------------------------------------------------------------------------
+
+-- | Return a one less.
+--
+-- >>> isMin (FZ :: Fin N.Nat1)
+-- Nothing
+--
+-- >>> map isMin universe :: [Maybe (Fin N.Nat3)]
+-- [Nothing,Just 0,Just 1,Just 2]
+--
+-- @since 0.1.1
+--
+isMin :: Fin ('S n) -> Maybe (Fin n)
+isMin FZ     = Nothing
+isMin (FS n) = Just n
+
+-- | Return a one less.
+--
+-- >>> isMax (FZ :: Fin N.Nat1)
+-- Nothing
+--
+-- >>> map isMax universe :: [Maybe (Fin N.Nat3)]
+-- [Just 0,Just 1,Just 2,Nothing]
+--
+-- @since 0.1.1
+--
+isMax :: forall n. N.InlineInduction n => Fin ('S n) -> Maybe (Fin n)
+isMax = getIsMax (N.inlineInduction start step) where
+    start :: IsMax 'Z
+    start = IsMax $ \_ -> Nothing
+
+    step :: IsMax m -> IsMax ('S m)
+    step (IsMax rec) = IsMax $ \n -> case n of
+        FZ   -> Just FZ
+        FS m -> fmap FS (rec m)
+
+newtype IsMax n = IsMax { getIsMax :: Fin ('S n) -> Maybe (Fin n) }
+
+-------------------------------------------------------------------------------
 -- Append & Split
 -------------------------------------------------------------------------------
 
+-- | >>> map weakenRight1 universe :: [Fin N.Nat5]
+-- [1,2,3,4]
+--
+-- @since 0.1.1
+weakenRight1 :: Fin n -> Fin ('S n)
+weakenRight1 = FS
+
+-- | >>> map weakenLeft1 universe :: [Fin N.Nat5]
+-- [0,1,2,3]
+--
+-- @since 0.1.1
+weakenLeft1 :: N.InlineInduction n => Fin n -> Fin ('S n)
+weakenLeft1 = getWeaken1 (N.inlineInduction start step) where
+    start :: Weaken1 'Z
+    start = Weaken1 absurd
+
+    step :: Weaken1 n -> Weaken1 ('S n)
+    step (Weaken1 go) = Weaken1 $ \n -> case n of
+        FZ    -> FZ
+        FS n' -> FS (go n')
+
+newtype Weaken1 n = Weaken1 { getWeaken1 :: Fin n -> Fin ('S n) }
+
+-- | >>> map (weakenLeft (Proxy :: Proxy N.Nat2)) (universe :: [Fin N.Nat3])
+-- [0,1,2]
 weakenLeft :: forall n m. N.InlineInduction n => Proxy m -> Fin n -> Fin (N.Plus n m)
 weakenLeft _ = getWeakenLeft (N.inlineInduction start step :: WeakenLeft m n) where
     start :: WeakenLeft m 'Z
@@ -313,6 +445,8 @@
 
 newtype WeakenLeft m n = WeakenLeft { getWeakenLeft :: Fin n -> Fin (N.Plus n m) }
 
+-- | >>> map (weakenRight (Proxy :: Proxy N.Nat2)) (universe :: [Fin N.Nat3])
+-- [2,3,4]
 weakenRight :: forall n m. N.InlineInduction n => Proxy n -> Fin m -> Fin (N.Plus n m)
 weakenRight _ = getWeakenRight (N.inlineInduction start step :: WeakenRight m n) where
     start = WeakenRight id
diff --git a/src/Data/Fin/Enum.hs b/src/Data/Fin/Enum.hs
--- a/src/Data/Fin/Enum.hs
+++ b/src/Data/Fin/Enum.hs
@@ -1,14 +1,14 @@
-{-# LANGUAGE ConstraintKinds        #-}
-{-# LANGUAGE DataKinds              #-}
-{-# LANGUAGE DefaultSignatures      #-}
-{-# LANGUAGE FlexibleContexts       #-}
-{-# LANGUAGE FlexibleInstances      #-}
-{-# LANGUAGE FunctionalDependencies #-}
-{-# LANGUAGE PolyKinds              #-}
-{-# LANGUAGE ScopedTypeVariables    #-}
-{-# LANGUAGE TypeFamilies           #-}
-{-# LANGUAGE TypeOperators          #-}
-{-# LANGUAGE UndecidableInstances   #-}
+{-# LANGUAGE ConstraintKinds       #-}
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE DefaultSignatures     #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds             #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE UndecidableInstances  #-}
 -- |
 --
 -- This module is designed to be imported qualified:
@@ -148,7 +148,7 @@
 
 -- | Generic version of 'to'.
 gto :: (G.Generic a, GTo a) => Fin (GEnumSize a) -> a
-gto = \x -> G.to $ gtoRep x id $ F.absurd
+gto = \x -> G.to $ gtoRep x id F.absurd
 
 -- | Constraint for the class that computes 'gto'.
 type GTo a = GToRep (G.Rep a)
diff --git a/src/Data/Nat.hs b/src/Data/Nat.hs
--- a/src/Data/Nat.hs
+++ b/src/Data/Nat.hs
@@ -1,4 +1,10 @@
+{-# LANGUAGE CPP                #-}
 {-# LANGUAGE DeriveDataTypeable #-}
+
+#if __GLASGOW_HASKELL__ < 710
+{-# LANGUAGE DataKinds          #-}
+{-# LANGUAGE StandaloneDeriving #-}
+#endif
 -- | 'Nat' numbers.
 --
 -- This module is designed to be imported qualified.
@@ -23,6 +29,8 @@
 import GHC.Exception   (ArithException (..), throw)
 import Numeric.Natural (Natural)
 
+import qualified Test.QuickCheck as QC
+
 -------------------------------------------------------------------------------
 -- Nat
 -------------------------------------------------------------------------------
@@ -33,6 +41,11 @@
 --
 data Nat = Z | S Nat deriving (Eq, Ord, Typeable, Data)
 
+#if __GLASGOW_HASKELL__ < 710
+deriving instance Typeable 'Z
+deriving instance Typeable 'S
+#endif
+
 -- | 'Nat' is printed as 'Natural'.
 --
 -- To see explicit structure, use 'explicitShow' or 'explicitShowsPrec'
@@ -63,7 +76,7 @@
     toInteger = cata 0 succ
 
     quotRem _ Z = throw DivideByZero
-    quotRem _ _ = error "un-implemented"
+    quotRem _ _ = error "quotRam @Nat un-implemented"
 
 {- TODO: make <= with witness
 instance Ix Nat where
@@ -89,6 +102,23 @@
 
 instance Hashable Nat where
     hashWithSalt salt = hashWithSalt salt . toInteger
+
+-------------------------------------------------------------------------------
+-- QuickCheck
+-------------------------------------------------------------------------------
+
+instance QC.Arbitrary Nat where
+    arbitrary = fmap fromNatural QC.arbitrarySizedNatural
+
+    shrink Z     = []
+    shrink (S n) = n : QC.shrink n
+
+instance QC.CoArbitrary Nat where
+    coarbitrary Z     = QC.variant (0 :: Int) 
+    coarbitrary (S n) = QC.variant (1 :: Int) . QC.coarbitrary n
+
+instance QC.Function Nat where
+    function = QC.functionIntegral
 
 -------------------------------------------------------------------------------
 -- Showing
diff --git a/src/Data/Type/Nat.hs b/src/Data/Type/Nat.hs
--- a/src/Data/Type/Nat.hs
+++ b/src/Data/Type/Nat.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE CPP                  #-}
 {-# LANGUAGE DataKinds            #-}
+{-# LANGUAGE DeriveDataTypeable   #-}
 {-# LANGUAGE EmptyCase            #-}
 {-# LANGUAGE GADTs                #-}
 {-# LANGUAGE KindSignatures       #-}
@@ -45,6 +46,8 @@
     -- * Arithmetic
     Plus,
     Mult,
+    Mult2,
+    DivMod2,
     -- * Conversion to GHC Nat
     ToGHC,
     FromGHC,
@@ -63,16 +66,26 @@
     )  where
 
 import Data.Function      (fix)
-import Data.Nat
 import Data.Proxy         (Proxy (..))
-import Data.Type.Equality
-import Data.Type.Dec
+import Data.Type.Dec      (Dec (..))
+import Data.Type.Equality ((:~:) (..), TestEquality (..))
+import Data.Typeable      (Typeable)
 import Numeric.Natural    (Natural)
 
 import qualified GHC.TypeLits as GHC
 
 import Unsafe.Coerce (unsafeCoerce)
 
+#if !MIN_VERSION_base(4,11,0)
+import Data.Type.Equality (type (==))
+#endif
+
+import Data.Nat
+
+-- $setup
+-- >>> :set -XTypeOperators -XDataKinds
+-- >>> import Data.Type.Dec (decShow)
+
 -------------------------------------------------------------------------------
 -- SNat
 -------------------------------------------------------------------------------
@@ -81,6 +94,7 @@
 data SNat (n :: Nat) where
     SZ :: SNat 'Z
     SS :: SNatI n => SNat ('S n)
+  deriving (Typeable)
 
 deriving instance Show (SNat p)
 
@@ -338,6 +352,33 @@
     Mult 'Z     m = 'Z
     Mult ('S n) m = Plus m (Mult n m)
 
+-- | Multiplication by two. Doubling.
+--
+-- >>> reflect (snat :: SNat (Mult2 Nat4))
+-- 8
+--
+type family Mult2 (n :: Nat) :: Nat where
+    Mult2 'Z     = 'Z
+    Mult2 ('S n) = 'S ('S (Mult2 n))
+
+-- | Division by two. 'False' is 0 and 'True' is 1 as a remainder.
+--
+-- >>> :kind! DivMod2 Nat7
+-- DivMod2 Nat7 :: (Nat, Bool)
+-- = '( 'S ('S ('S 'Z)), 'True)
+--
+-- >>> :kind! DivMod2 Nat4
+-- DivMod2 Nat4 :: (Nat, Bool)
+-- = '( 'S ('S 'Z), 'False)
+--
+type family DivMod2 (n :: Nat) :: (Nat, Bool) where
+    DivMod2 'Z          = '( 'Z, 'False)
+    DivMod2 ('S 'Z)     = '( 'Z, 'True)
+    DivMod2 ('S ('S n)) = DivMod2' (DivMod2 n)
+
+type family DivMod2' (p :: (Nat, Bool)) :: (Nat, Bool) where
+    DivMod2' '(n, b) = '( 'S n, b)
+
 -------------------------------------------------------------------------------
 -- Aliases
 -------------------------------------------------------------------------------
@@ -425,6 +466,3 @@
 
 retagMap :: (a -> b) -> Tagged n a -> Tagged m b
 retagMap f = Tagged . f . unTagged
-
--- $setup
--- >>> :set -XTypeOperators -XDataKinds
diff --git a/src/Data/Type/Nat/LE.hs b/src/Data/Type/Nat/LE.hs
--- a/src/Data/Type/Nat/LE.hs
+++ b/src/Data/Type/Nat/LE.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE DeriveDataTypeable    #-}
 {-# LANGUAGE EmptyCase             #-}
 {-# LANGUAGE FlexibleContexts      #-}
 {-# LANGUAGE FlexibleInstances     #-}
@@ -48,10 +49,12 @@
     ) where
 
 import Data.Type.Dec      (Dec (..), Decidable (..), Neg)
-import Data.Type.Equality
-import Data.Type.Nat
+import Data.Type.Equality ((:~:) (..))
+import Data.Typeable      (Typeable)
 import Data.Void          (absurd)
 
+import Data.Type.Nat
+
 -------------------------------------------------------------------------------
 -- Proof
 -------------------------------------------------------------------------------
@@ -60,6 +63,7 @@
 data LEProof n m where
     LEZero :: LEProof 'Z m
     LESucc :: LEProof n m -> LEProof ('S n) ('S m)
+  deriving (Typeable)
 
 deriving instance Show (LEProof n m)
 
diff --git a/src/Data/Type/Nat/LE/ReflStep.hs b/src/Data/Type/Nat/LE/ReflStep.hs
--- a/src/Data/Type/Nat/LE/ReflStep.hs
+++ b/src/Data/Type/Nat/LE/ReflStep.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE DeriveDataTypeable    #-}
 {-# LANGUAGE EmptyCase             #-}
 {-# LANGUAGE FlexibleContexts      #-}
 {-# LANGUAGE FlexibleInstances     #-}
@@ -35,10 +36,11 @@
     ) where
 
 import Data.Type.Dec      (Dec (..), Decidable (..), Neg)
-import Data.Type.Equality
-import Data.Type.Nat
+import Data.Type.Equality ((:~:) (..))
+import Data.Typeable      (Typeable)
 import Data.Void          (absurd)
 
+import Data.Type.Nat
 import qualified Data.Type.Nat.LE as ZeroSucc
 
 -------------------------------------------------------------------------------
@@ -49,6 +51,7 @@
 data LEProof n m where
     LERefl :: LEProof n n
     LEStep :: LEProof n m -> LEProof n ('S m)
+  deriving (Typeable)
 
 deriving instance Show (LEProof n m)