diff --git a/changelog.md b/changelog.md
--- a/changelog.md
+++ b/changelog.md
@@ -1,3 +1,12 @@
+## [0.6.1] - 2022-09-12
+- new ListLength type family and associated functions
+- new Greater type family and associated functions
+- new FixedList type indexed by PeanoNat
+- new ListElement functions
+- new OrderedWitnessMapFor and OrderedWitnessMapOf types
+- new functions:
+  - someForToSome
+
 ## [0.6] - 2022-05-08
 - reorganise modules
 - rename types and functions
diff --git a/src/Data/PeanoNat.hs b/src/Data/PeanoNat.hs
--- a/src/Data/PeanoNat.hs
+++ b/src/Data/PeanoNat.hs
@@ -40,3 +40,8 @@
 type family PeanoToNatural pn where
     PeanoToNatural 'Zero = 0
     PeanoToNatural ('Succ pn) = PeanoToNatural pn + 1
+
+type ListLength :: forall k. [k] -> PeanoNat
+type family ListLength l where
+    ListLength '[] = 'Zero
+    ListLength (a ': aa) = 'Succ (ListLength aa)
diff --git a/src/Data/Type/Witness.hs b/src/Data/Type/Witness.hs
--- a/src/Data/Type/Witness.hs
+++ b/src/Data/Type/Witness.hs
@@ -21,11 +21,14 @@
 import Data.Type.Witness.Specific.Either as I
 import Data.Type.Witness.Specific.Empty as I
 import Data.Type.Witness.Specific.FiniteAllFor as I
+import Data.Type.Witness.Specific.FixedList as I
 import Data.Type.Witness.Specific.List.Element as I
 import Data.Type.Witness.Specific.List.List as I
 import Data.Type.Witness.Specific.List.Product as I
 import Data.Type.Witness.Specific.List.Sum as I
 import Data.Type.Witness.Specific.Natural as I
+import Data.Type.Witness.Specific.OrderedWitnessMap.For as I
+import Data.Type.Witness.Specific.OrderedWitnessMap.Of as I
 import Data.Type.Witness.Specific.Pair as I
 import Data.Type.Witness.Specific.PeanoNat as I
 import Data.Type.Witness.Specific.Single as I
diff --git a/src/Data/Type/Witness/Specific/FixedList.hs b/src/Data/Type/Witness/Specific/FixedList.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Witness/Specific/FixedList.hs
@@ -0,0 +1,76 @@
+module Data.Type.Witness.Specific.FixedList where
+
+import Data.PeanoNat
+import Data.Type.Witness.General.Representative
+import Data.Type.Witness.Specific.PeanoNat
+import Data.Type.Witness.Specific.Some
+import Import
+
+type FixedList :: PeanoNat -> Type -> Type
+data FixedList n a where
+    NilFixedList :: FixedList 'Zero a
+    ConsFixedList :: a -> FixedList n a -> FixedList ('Succ n) a
+
+instance Functor (FixedList n) where
+    fmap _ NilFixedList = NilFixedList
+    fmap ab (ConsFixedList a l) = ConsFixedList (ab a) $ fmap ab l
+
+instance Is PeanoNatType n => Applicative (FixedList n) where
+    pure = let
+        pure' :: PeanoNatType n' -> a -> FixedList n' a
+        pure' ZeroType _ = NilFixedList
+        pure' (SuccType n) a = ConsFixedList a $ pure' n a
+        in pure' representative
+    (<*>) = let
+        ap' :: PeanoNatType n' -> FixedList n' (a -> b) -> FixedList n' a -> FixedList n' b
+        ap' ZeroType NilFixedList NilFixedList = NilFixedList
+        ap' (SuccType n) (ConsFixedList ab lab) (ConsFixedList a la) = ConsFixedList (ab a) $ ap' n lab la
+        in ap' representative
+
+instance Foldable (FixedList n) where
+    foldMap _ NilFixedList = mempty
+    foldMap am (ConsFixedList a l) = am a <> foldMap am l
+
+instance Traversable (FixedList n) where
+    sequenceA NilFixedList = pure NilFixedList
+    sequenceA (ConsFixedList fa l) = liftA2 ConsFixedList fa $ sequenceA l
+
+fixedFromList :: [a] -> (forall n. PeanoNatType n -> FixedList n a -> r) -> r
+fixedFromList [] call = call ZeroType NilFixedList
+fixedFromList (a:aa) call = fixedFromList aa $ \n l -> call (SuccType n) $ ConsFixedList a l
+
+fixedListArrowSequence_ ::
+       forall arrow n a. Arrow arrow
+    => FixedList n (arrow a ())
+    -> arrow (FixedList n a) ()
+fixedListArrowSequence_ NilFixedList = arr $ \_ -> ()
+fixedListArrowSequence_ (ConsFixedList x1 xr) =
+    proc a1r -> do
+        x1 -<
+            case a1r of
+                ConsFixedList a1 _ -> a1
+        fixedListArrowSequence_ xr -<
+            case a1r of
+                ConsFixedList _ ar -> ar
+
+fixedListArrowSequence ::
+       forall arrow n a b. Arrow arrow
+    => FixedList n (arrow a b)
+    -> arrow (FixedList n a) (FixedList n b)
+fixedListArrowSequence NilFixedList = arr $ \_ -> NilFixedList
+fixedListArrowSequence (ConsFixedList x1 xr) =
+    proc a1r -> do
+        b1 <-
+            x1 -<
+                case a1r of
+                    ConsFixedList a1 _ -> a1
+        br <-
+            fixedListArrowSequence xr -<
+                case a1r of
+                    ConsFixedList _ ar -> ar
+        returnA -< ConsFixedList b1 br
+
+fixedListElement :: Some (Greater n) -> FixedList n a -> a
+fixedListElement (MkSome (MkGreater ZeroGreaterEqual)) (ConsFixedList a _) = a
+fixedListElement (MkSome (MkGreater (SuccGreaterEqual n))) (ConsFixedList _ l) =
+    fixedListElement (MkSome $ MkGreater n) l
diff --git a/src/Data/Type/Witness/Specific/List/Element.hs b/src/Data/Type/Witness/Specific/List/Element.hs
--- a/src/Data/Type/Witness/Specific/List/Element.hs
+++ b/src/Data/Type/Witness/Specific/List/Element.hs
@@ -1,7 +1,10 @@
 module Data.Type.Witness.Specific.List.Element where
 
+import Data.PeanoNat
 import Data.Type.Witness.General.Order
 import Data.Type.Witness.Specific.List.List
+import Data.Type.Witness.Specific.PeanoNat
+import Data.Type.Witness.Specific.Some
 import Import
 
 type ListElementType :: forall k. [k] -> k -> Type
@@ -42,6 +45,10 @@
 instance Empty (ListElementType '[] t) where
     never lt = case lt of {}
 
+pickListElement :: forall k (w :: k -> Type) (t :: k) (lt :: [k]). ListElementType lt t -> ListType w lt -> w t
+pickListElement FirstElementType (ConsListType wt _) = wt
+pickListElement (RestElementType n) (ConsListType _ l) = pickListElement n l
+
 lookUpListElement ::
        forall k (w :: k -> Type) (t :: k) (lt :: [k]). TestEquality w
     => w t
@@ -57,3 +64,16 @@
 countListType :: ListType w lt -> ListType (ListElementType lt) lt
 countListType NilListType = NilListType
 countListType (ConsListType _ lt) = ConsListType FirstElementType (mapListType RestElementType $ countListType lt)
+
+listElementTypeIndex :: Some (ListElementType lt) -> Some (Greater (ListLength lt))
+listElementTypeIndex (MkSome FirstElementType) = MkSome $ MkGreater ZeroGreaterEqual
+listElementTypeIndex (MkSome (RestElementType n)) =
+    case listElementTypeIndex $ MkSome n of
+        MkSome (MkGreater n') -> MkSome $ MkGreater $ SuccGreaterEqual n'
+
+indexListElementType :: ListType w lt -> Some (Greater (ListLength lt)) -> SomeFor w (ListElementType lt)
+indexListElementType (ConsListType wa _) (MkSome (MkGreater ZeroGreaterEqual)) = MkSomeFor FirstElementType wa
+indexListElementType (ConsListType _ lt) (MkSome (MkGreater (SuccGreaterEqual n))) =
+    case indexListElementType lt (MkSome (MkGreater n)) of
+        MkSomeFor n' wa -> MkSomeFor (RestElementType n') wa
+indexListElementType NilListType (MkSome n) = never n
diff --git a/src/Data/Type/Witness/Specific/List/List.hs b/src/Data/Type/Witness/Specific/List/List.hs
--- a/src/Data/Type/Witness/Specific/List/List.hs
+++ b/src/Data/Type/Witness/Specific/List/List.hs
@@ -1,7 +1,10 @@
 module Data.Type.Witness.Specific.List.List where
 
+import Data.PeanoNat
 import Data.Type.Witness.General.Representative
+import Data.Type.Witness.Specific.FixedList
 import Data.Type.Witness.Specific.Pair
+import Data.Type.Witness.Specific.PeanoNat
 import Data.Type.Witness.Specific.Some
 import Import
 
@@ -82,3 +85,16 @@
 listTypeFor_ :: Applicative m => ListType w t -> (forall a. w a -> m ()) -> m ()
 listTypeFor_ NilListType _ = pure ()
 listTypeFor_ (ConsListType t tt) f = f t *> listTypeFor_ tt f
+
+listTypeLengthType :: ListType w lt -> PeanoNatType (ListLength lt)
+listTypeLengthType NilListType = ZeroType
+listTypeLengthType (ConsListType _ rest) = SuccType $ listTypeLengthType rest
+
+listTypeToFixedList :: (forall a. w a -> r) -> ListType w t -> FixedList (ListLength t) r
+listTypeToFixedList _wr NilListType = NilFixedList
+listTypeToFixedList wr (ConsListType wa rest) = ConsFixedList (wr wa) $ listTypeToFixedList wr rest
+
+listTypeFromFixedList :: FixedList n (Some w) -> (forall t. n ~ ListLength t => ListType w t -> r) -> r
+listTypeFromFixedList NilFixedList call = call NilListType
+listTypeFromFixedList (ConsFixedList (MkSome wa) l) call =
+    listTypeFromFixedList l $ \rest -> call $ ConsListType wa rest
diff --git a/src/Data/Type/Witness/Specific/OrderedWitnessMap/For.hs b/src/Data/Type/Witness/Specific/OrderedWitnessMap/For.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Witness/Specific/OrderedWitnessMap/For.hs
@@ -0,0 +1,71 @@
+module Data.Type.Witness.Specific.OrderedWitnessMap.For where
+
+import qualified Data.Map as Map
+import Data.Type.Witness.General.Order
+import Data.Type.Witness.Specific.Some
+import Import
+
+-- | A dictionary that is heterogenous up to its simple witness type @w@.
+-- Witnesses are the keys of the dictionary, and the values they witness are the values of the dictionary.
+type OrderedWitnessMapFor :: forall k. (k -> Type) -> (k -> Type) -> Type
+newtype OrderedWitnessMapFor f w =
+    MkOrderedWitnessMapFor (Map.Map (Some w) (SomeFor f w))
+    deriving (Semigroup, Monoid)
+
+-- | An empty dictionary.
+emptyOrderedWitnessMapFor :: TestOrder w => OrderedWitnessMapFor f w
+emptyOrderedWitnessMapFor = mempty
+
+-- | Look up the value in the dictionary that matches the given witness.
+orderedWitnessMapForLookup :: TestOrder w => w a -> OrderedWitnessMapFor f w -> Maybe (f a)
+orderedWitnessMapForLookup wit (MkOrderedWitnessMapFor wmap) = do
+    MkSomeFor wa fa <- Map.lookup (MkSome wit) wmap
+    Refl <- testEquality wa wit -- should always succeed
+    return fa
+
+-- | Modify the value in the dictionary that matches a particular witness.
+orderedWitnessMapForModify ::
+       forall f w a. TestOrder w
+    => w a
+    -> (f a -> f a)
+    -> OrderedWitnessMapFor f w
+    -> OrderedWitnessMapFor f w
+orderedWitnessMapForModify wit amap (MkOrderedWitnessMapFor wmap) = let
+    updater :: SomeFor f w -> Maybe (SomeFor f w)
+    updater (MkSomeFor wa fa) = do
+        Refl <- testEquality wa wit -- should always succeed
+        return $ MkSomeFor wa $ amap fa
+    in MkOrderedWitnessMapFor $ Map.update updater (MkSome wit) wmap
+
+-- | Replace the value in the dictionary that matches the witness
+orderedWitnessMapForReplace :: TestOrder w => w a -> f a -> OrderedWitnessMapFor f w -> OrderedWitnessMapFor f w
+orderedWitnessMapForReplace wit newfa = orderedWitnessMapForModify wit (const newfa)
+
+-- | Add a witness and value to the dictionary.
+orderedWitnessMapForAdd :: TestOrder w => w a -> f a -> OrderedWitnessMapFor f w -> OrderedWitnessMapFor f w
+orderedWitnessMapForAdd wit fa (MkOrderedWitnessMapFor wmap) =
+    MkOrderedWitnessMapFor $ Map.insert (MkSome wit) (MkSomeFor wit fa) wmap
+
+-- | A dictionary for a single witness and value
+orderedWitnessMapForSingle :: w a -> f a -> OrderedWitnessMapFor f w
+orderedWitnessMapForSingle wit fa = MkOrderedWitnessMapFor $ Map.singleton (MkSome wit) $ MkSomeFor wit fa
+
+orderedWitnessMapForFold :: Monoid m => OrderedWitnessMapFor f w -> (forall a. w a -> f a -> m) -> m
+orderedWitnessMapForFold wmf f = mconcat $ fmap (\(MkSomeFor wa fa) -> f wa fa) $ orderedWitnessMapForToList wmf
+
+-- | Remove the entry in the dictionary that matches the given witness.
+orderedWitnessMapForRemove :: TestOrder w => w a -> OrderedWitnessMapFor f w -> OrderedWitnessMapFor f w
+orderedWitnessMapForRemove wit (MkOrderedWitnessMapFor wmap) = MkOrderedWitnessMapFor $ Map.delete (MkSome wit) wmap
+
+orderedWitnessMapForToList :: OrderedWitnessMapFor f w -> [SomeFor f w]
+orderedWitnessMapForToList (MkOrderedWitnessMapFor wmap) = Map.elems wmap
+
+-- | Create a dictionary from a list of witness\/value pairs
+orderedWitnessMapForFromList :: TestOrder w => [SomeFor f w] -> OrderedWitnessMapFor f w
+orderedWitnessMapForFromList ee =
+    MkOrderedWitnessMapFor $ Map.fromList $ fmap (\swf@(MkSomeFor wa _) -> (MkSome wa, swf)) ee
+
+orderedWitnessMapForMapM ::
+       Applicative m => (forall a. f a -> m (g a)) -> OrderedWitnessMapFor f w -> m (OrderedWitnessMapFor g w)
+orderedWitnessMapForMapM fmg (MkOrderedWitnessMapFor cells) =
+    fmap MkOrderedWitnessMapFor $ for cells $ \(MkSomeFor wit fa) -> fmap (MkSomeFor wit) $ fmg fa
diff --git a/src/Data/Type/Witness/Specific/OrderedWitnessMap/Of.hs b/src/Data/Type/Witness/Specific/OrderedWitnessMap/Of.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Witness/Specific/OrderedWitnessMap/Of.hs
@@ -0,0 +1,48 @@
+module Data.Type.Witness.Specific.OrderedWitnessMap.Of where
+
+import Data.Type.Witness.General.Order
+import Data.Type.Witness.Specific.OrderedWitnessMap.For
+import Data.Type.Witness.Specific.Some
+import Import
+
+-- | A dictionary that is heterogenous up to its simple witness type @w@.
+-- Witnesses are the keys of the dictionary, and the values they witness are the values of the dictionary.
+type OrderedWitnessMapOf :: (Type -> Type) -> Type
+type OrderedWitnessMapOf = OrderedWitnessMapFor Identity
+
+-- | An empty dictionary.
+emptyOrderedWitnessMapOf :: TestOrder w => OrderedWitnessMapOf w
+emptyOrderedWitnessMapOf = emptyOrderedWitnessMapFor
+
+-- | Look up the first value in the dictionary that matches the given witness.
+orderedWitnessMapOfLookup :: TestOrder w => w a -> OrderedWitnessMapOf w -> Maybe a
+orderedWitnessMapOfLookup wit d = fmap runIdentity $ orderedWitnessMapForLookup wit d
+
+-- | Modify the first value in the dictionary that matches a particular witness.
+orderedWitnessMapOfModify :: TestOrder w => w a -> (a -> a) -> OrderedWitnessMapOf w -> OrderedWitnessMapOf w
+orderedWitnessMapOfModify wit amap = orderedWitnessMapForModify wit (Identity . amap . runIdentity)
+
+-- | Replace the first value in the dictionary that matches the witness
+orderedWitnessMapOfReplace :: TestOrder w => w a -> a -> OrderedWitnessMapOf w -> OrderedWitnessMapOf w
+orderedWitnessMapOfReplace wit newa = orderedWitnessMapOfModify wit $ const newa
+
+orderedWitnessMapOfSingle :: w a -> a -> OrderedWitnessMapOf w
+orderedWitnessMapOfSingle wit a = orderedWitnessMapForSingle wit $ Identity a
+
+orderedWitnessMapOfFold :: Monoid m => OrderedWitnessMapOf w -> (forall a. w a -> a -> m) -> m
+orderedWitnessMapOfFold d f = orderedWitnessMapForFold d $ \wa (Identity a) -> f wa a
+
+-- | Add a witness and value as the first entry in the dictionary.
+orderedWitnessMapOfAdd :: TestOrder w => w a -> a -> OrderedWitnessMapOf w -> OrderedWitnessMapOf w
+orderedWitnessMapOfAdd wit a = orderedWitnessMapForAdd wit $ Identity a
+
+-- | Remove the first entry in the dictionary that matches the given witness.
+orderedWitnessMapOfRemove :: TestOrder w => w a -> OrderedWitnessMapOf w -> OrderedWitnessMapOf w
+orderedWitnessMapOfRemove = orderedWitnessMapForRemove
+
+-- | Create a dictionary from a list of witness\/value pairs
+orderedWitnessMapOfFromList :: TestOrder w => [SomeOf w] -> OrderedWitnessMapOf w
+orderedWitnessMapOfFromList = orderedWitnessMapForFromList
+
+orderedWitnessMapOfToList :: OrderedWitnessMapOf w -> [SomeOf w]
+orderedWitnessMapOfToList = orderedWitnessMapForToList
diff --git a/src/Data/Type/Witness/Specific/PeanoNat.hs b/src/Data/Type/Witness/Specific/PeanoNat.hs
--- a/src/Data/Type/Witness/Specific/PeanoNat.hs
+++ b/src/Data/Type/Witness/Specific/PeanoNat.hs
@@ -53,6 +53,10 @@
     ZeroGreaterEqual :: GreaterEqual a 'Zero
     SuccGreaterEqual :: GreaterEqual a b -> GreaterEqual ('Succ a) ('Succ b)
 
+greaterEqualIndex :: GreaterEqual a b -> PeanoNatType b
+greaterEqualIndex ZeroGreaterEqual = ZeroType
+greaterEqualIndex (SuccGreaterEqual n) = SuccType $ greaterEqualIndex n
+
 samePeanoGreaterEqual :: PeanoNatType a -> GreaterEqual a a
 samePeanoGreaterEqual ZeroType = ZeroGreaterEqual
 samePeanoGreaterEqual (SuccType a) = SuccGreaterEqual $ samePeanoGreaterEqual a
@@ -94,3 +98,32 @@
 addPeanoNatTypeGE a (SuccType b) =
     case succAddPeanoNatTypeEqual a b of
         Refl -> diff1GreaterEqual $ addPeanoNatTypeGE a b
+
+type Greater :: PeanoNat -> PeanoNat -> Type
+data Greater a b where
+    MkGreater :: GreaterEqual a b -> Greater ('Succ a) b
+
+greaterIndex :: Greater a b -> PeanoNatType b
+greaterIndex (MkGreater n) = greaterEqualIndex n
+
+peanoGreater :: PeanoNatType a -> PeanoNatType b -> Maybe (Greater a b)
+peanoGreater (SuccType a) b = fmap MkGreater $ peanoGreaterEqual a b
+peanoGreater ZeroType _ = Nothing
+
+instance Eq (Greater 'Zero b) where
+    (==) = never
+
+instance Searchable (Greater 'Zero b) where
+    search = finiteSearch
+
+instance Countable (Greater 'Zero b) where
+    countPrevious = never
+    countMaybeNext Nothing = Nothing
+    countMaybeNext (Just n) = never n
+
+instance Finite (Greater 'Zero b) where
+    allValues = []
+    assemble _ = pure never
+
+instance Empty (Greater 'Zero b) where
+    never n = case n of {}
diff --git a/src/Data/Type/Witness/Specific/Some.hs b/src/Data/Type/Witness/Specific/Some.hs
--- a/src/Data/Type/Witness/Specific/Some.hs
+++ b/src/Data/Type/Witness/Specific/Some.hs
@@ -73,3 +73,6 @@
 
 instance forall k (w :: k -> Type). AllConstraint Show w => Show (Some w) where
     show (MkSome wa) = allShow wa
+
+someForToSome :: SomeFor f w -> Some w
+someForToSome (MkSomeFor wa _) = MkSome wa
diff --git a/src/Data/Type/Witness/Specific/WitnessMap/For.hs b/src/Data/Type/Witness/Specific/WitnessMap/For.hs
--- a/src/Data/Type/Witness/Specific/WitnessMap/For.hs
+++ b/src/Data/Type/Witness/Specific/WitnessMap/For.hs
@@ -6,20 +6,20 @@
 -- | A dictionary that is heterogenous up to its simple witness type @w@.
 -- Witnesses are the keys of the dictionary, and the values they witness are the values of the dictionary.
 type WitnessMapFor :: forall k. (k -> Type) -> (k -> Type) -> Type
-newtype WitnessMapFor f w =
-    MkWitnessMapFor [SomeFor f w]
-    deriving (Semigroup, Monoid)
+newtype WitnessMapFor f w = MkWitnessMapFor
+    { witnessMapForToList :: [SomeFor f w]
+    } deriving (Semigroup, Monoid)
 
 -- | An empty dictionary.
 emptyWitnessMapFor :: WitnessMapFor f w
 emptyWitnessMapFor = mempty
 
 -- | Look up the first value in the dictionary that matches the given witness.
-witnessMapForLookup :: (TestEquality w) => w a -> WitnessMapFor f w -> Maybe (f a)
+witnessMapForLookup :: TestEquality w => w a -> WitnessMapFor f w -> Maybe (f a)
 witnessMapForLookup wit (MkWitnessMapFor cells) = listToMaybe (mapMaybe (matchSomeFor wit) cells)
 
 -- | Modify the first value in the dictionary that matches a particular witness.
-witnessMapForModify :: (TestEquality w) => w a -> (f a -> f a) -> WitnessMapFor f w -> WitnessMapFor f w
+witnessMapForModify :: TestEquality w => w a -> (f a -> f a) -> WitnessMapFor f w -> WitnessMapFor f w
 witnessMapForModify wit amap (MkWitnessMapFor cells) =
     MkWitnessMapFor (replaceFirst ((fmap ((MkSomeFor wit) . amap)) . (matchSomeFor wit)) cells)
   where
@@ -31,7 +31,7 @@
     replaceFirst _ _ = []
 
 -- | Replace the first value in the dictionary that matches the witness
-witnessMapForReplace :: (TestEquality w) => w a -> f a -> WitnessMapFor f w -> WitnessMapFor f w
+witnessMapForReplace :: TestEquality w => w a -> f a -> WitnessMapFor f w -> WitnessMapFor f w
 witnessMapForReplace wit newfa = witnessMapForModify wit (const newfa)
 
 -- | Add a witness and value as the first entry in the dictionary.
@@ -46,7 +46,7 @@
 witnessMapForFold (MkWitnessMapFor cells) f = mconcat $ fmap (\(MkSomeFor wit fa) -> f wit fa) cells
 
 -- | Remove the first entry in the dictionary that matches the given witness.
-witnessMapForRemove :: (TestEquality w) => w a -> WitnessMapFor f w -> WitnessMapFor f w
+witnessMapForRemove :: TestEquality w => w a -> WitnessMapFor f w -> WitnessMapFor f w
 witnessMapForRemove wit (MkWitnessMapFor cells) =
     MkWitnessMapFor (removeFirst (\(MkSomeFor cwit _) -> isJust (testEquality wit cwit)) cells)
   where
diff --git a/src/Data/Type/Witness/Specific/WitnessMap/Of.hs b/src/Data/Type/Witness/Specific/WitnessMap/Of.hs
--- a/src/Data/Type/Witness/Specific/WitnessMap/Of.hs
+++ b/src/Data/Type/Witness/Specific/WitnessMap/Of.hs
@@ -14,15 +14,15 @@
 emptyWitnessMapOf = emptyWitnessMapFor
 
 -- | Look up the first value in the dictionary that matches the given witness.
-witnessMapOfLookup :: (TestEquality w) => w a -> WitnessMapOf w -> Maybe a
+witnessMapOfLookup :: TestEquality w => w a -> WitnessMapOf w -> Maybe a
 witnessMapOfLookup wit d = fmap runIdentity $ witnessMapForLookup wit d
 
 -- | Modify the first value in the dictionary that matches a particular witness.
-witnessMapOfModify :: (TestEquality w) => w a -> (a -> a) -> WitnessMapOf w -> WitnessMapOf w
+witnessMapOfModify :: TestEquality w => w a -> (a -> a) -> WitnessMapOf w -> WitnessMapOf w
 witnessMapOfModify wit amap = witnessMapForModify wit (Identity . amap . runIdentity)
 
 -- | Replace the first value in the dictionary that matches the witness
-witnessMapOfReplace :: (TestEquality w) => w a -> a -> WitnessMapOf w -> WitnessMapOf w
+witnessMapOfReplace :: TestEquality w => w a -> a -> WitnessMapOf w -> WitnessMapOf w
 witnessMapOfReplace wit newa = witnessMapOfModify wit $ const newa
 
 witnessMapOfSingle :: w a -> a -> WitnessMapOf w
@@ -36,9 +36,12 @@
 witnessMapOfAdd wit a = witnessMapForAdd wit $ Identity a
 
 -- | Remove the first entry in the dictionary that matches the given witness.
-witnessMapOfRemove :: (TestEquality w) => w a -> WitnessMapOf w -> WitnessMapOf w
+witnessMapOfRemove :: TestEquality w => w a -> WitnessMapOf w -> WitnessMapOf w
 witnessMapOfRemove = witnessMapForRemove
 
 -- | Create a dictionary from a list of witness\/value pairs
 witnessMapOfFromList :: [SomeOf w] -> WitnessMapOf w
 witnessMapOfFromList = MkWitnessMapFor
+
+witnessMapOfToList :: WitnessMapOf w -> [SomeOf w]
+witnessMapOfToList = witnessMapForToList
diff --git a/src/Import.hs b/src/Import.hs
--- a/src/Import.hs
+++ b/src/Import.hs
@@ -3,6 +3,7 @@
     ) where
 
 import Control.Applicative as I
+import Control.Arrow as I
 import Control.Category as I
 import Data.Constraint as I (Dict(..))
 import Data.Countable as I
diff --git a/witness.cabal b/witness.cabal
--- a/witness.cabal
+++ b/witness.cabal
@@ -4,10 +4,10 @@
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: a76cbdba6c2986d516e94b90eb9a51cf636e600c1915604c67d33e50e06f3127
+-- hash: aae0fd4e94350169efa7229b1559a55e3b9d2ed3d389f607534a15403307b6b1
 
 name:           witness
-version:        0.6
+version:        0.6.1
 synopsis:       values that witness types
 description:    A /witness/ is a value that witnesses some sort of constraint on some list of type variables. This library provides support for a wide variety of witness types. It also provides classes for /representatives/, which are values that represent types.
 category:       Data
@@ -74,6 +74,7 @@
   build-depends:
       base >=4.15 && <5
     , constraints >=0.13
+    , containers >=0.4
     , countable >=1.2
   exposed-modules:
       Data.Type.Witness.Apply
@@ -95,8 +96,11 @@
       Data.Type.Witness.Specific.FiniteAllFor
       Data.Type.Witness.Specific.WitnessMap.Of
       Data.Type.Witness.Specific.WitnessMap.For
+      Data.Type.Witness.Specific.OrderedWitnessMap.Of
+      Data.Type.Witness.Specific.OrderedWitnessMap.For
       Data.Type.Witness.Specific.PeanoNat
       Data.Type.Witness.Specific.Natural
+      Data.Type.Witness.Specific.FixedList
       Data.Type.Witness.Specific.List.Element
       Data.Type.Witness.Specific.List.List
       Data.Type.Witness.Specific.Concat