diff --git a/fixed-length.cabal b/fixed-length.cabal
--- a/fixed-length.cabal
+++ b/fixed-length.cabal
@@ -1,5 +1,5 @@
 Name:             fixed-length
-Version:          0.1.1
+Version:          0.2
 License:          BSD3
 License-File:     LICENSE
 Author:           Henning Thielemann <haskell@henning-thielemann.de>
@@ -25,7 +25,7 @@
 Build-Type:       Simple
 
 Source-Repository this
-  Tag:         0.1.1
+  Tag:         0.2
   Type:        darcs
   Location:    http://hub.darcs.net/thielema/fixed-length/
 
@@ -33,12 +33,9 @@
   Type:        darcs
   Location:    http://hub.darcs.net/thielema/fixed-length/
 
-Flag tfp
-  Description: use type-level unary numbers from tfp package
-  Default: False
-
 Library
   Build-Depends:
+    tfp >=1.0 && <1.1,
     non-empty >=0.2 && <0.4,
     utility-ht >=0.0.1 && <0.1,
     base >=4 && <5
@@ -47,7 +44,3 @@
   Hs-Source-Dirs:   src
   Exposed-Modules:
     Data.FixedLength
-
-  If flag(tfp)
-    Other-Modules: Data.FixedLength.Unary
-    Build-Depends: tfp >=1.0 && <1.1
diff --git a/src/Data/FixedLength.hs b/src/Data/FixedLength.hs
--- a/src/Data/FixedLength.hs
+++ b/src/Data/FixedLength.hs
@@ -2,19 +2,24 @@
 {-# LANGUAGE Rank2Types #-}
 {-# LANGUAGE EmptyDataDecls #-}
 module Data.FixedLength (
-   C, Position, List, switch,
-   Wrap(Wrap, unwrap),
-   WrapPos(WrapPos, unwrapPos),
-   Zero, Succ(Stop, Succ),
-   toList, equal, showsPrec,
+   T, Position, List, Length,
+   Index, Zero, Succ(Stop, Succ),
+   toList, showsPrec,
    map, zipWith, sequenceA, repeat,
-   index, update, indices, indicesInt, numFromPos,
-   N0, N1, N2, N3, N4, N5, N6, N7, N8,
+   index, update, indices, indicesInt, numFromIndex,
    GE1, GE2, GE3, GE4, GE5, GE6, GE7, GE8,
    i0, i1, i2, i3, i4, i5, i6, i7,
-   (NonEmpty.!:), end,
+   fromFixedList, toFixedList,
+   (!:), end, singleton,
+   viewL, switchL, head, tail, switchEnd,
+   Curried, uncurry,
+   minimum, maximum,
    ) where
 
+import qualified Type.Data.Num.Unary as Unary
+import Type.Data.Num.Unary.Literal (U1)
+import Type.Data.Num.Unary (Positive, Natural, switchNat)
+
 import qualified Data.NonEmpty as NonEmpty
 import qualified Data.Empty as Empty
 
@@ -39,119 +44,142 @@
 import Prelude (Functor, fmap, Show, ShowS, Int, (+), error)
 
 
-type family List position :: * -> *
+type family List n :: * -> *
+type instance List Unary.Zero = Empty.T
+type instance List (Unary.Succ n) = NonEmpty.T (List n)
 
-class (list ~ List (Position list)) => C list where
-   type Position list :: *
-   switch ::
-      f Empty.T ->
-      (forall list0. C list0 => f (NonEmpty.T list0)) ->
-      f list
+type family Length (f :: * -> *)
+type instance Length Empty.T = Unary.Zero
+type instance Length (NonEmpty.T f) = Unary.Succ (Length f)
 
 
-type instance List Zero = Empty.T
+newtype T n a = Cons (List n a)
 
-instance C Empty.T where
-   type Position Empty.T = Zero
-   switch x _ = x
+fromFixedList :: List n a -> T n a
+fromFixedList = Cons
 
+toFixedList :: T n a -> List n a
+toFixedList (Cons xs) = xs
 
-type instance List (Succ position) = NonEmpty.T (List position)
 
-instance C list => C (NonEmpty.T list) where
-   type Position (NonEmpty.T list) = Succ (Position list)
-   switch _ x = x
+end :: T Unary.Zero a
+end = Cons Empty.Cons
 
+infixr 5 !:
 
-newtype
-   SwitchPos f list =
-      SwitchPos {runSwitchPos :: f list (Position list)}
+(!:) :: a -> T n a -> T (Unary.Succ n) a
+x !: Cons xs = Cons $ NonEmpty.Cons x xs
 
-switchPos ::
-   (C list, Position list ~ pos) =>
-   f Empty.T Zero ->
-   (forall list0 pos0. (C list0, Position list0 ~ pos0) =>
-    f (NonEmpty.T list0) (Succ pos0)) ->
-   f list pos
-switchPos empty nonEmpty =
-   runSwitchPos $ switch (SwitchPos empty) (SwitchPos nonEmpty)
+viewL :: T (Unary.Succ n) a -> (a, T n a)
+viewL (Cons (NonEmpty.Cons x xs)) = (x, Cons xs)
 
+switchL :: (a -> T n a -> b) -> (T (Unary.Succ n) a -> b)
+switchL f = P.uncurry f . viewL
 
-end :: Empty.T a
-end = Empty.Cons
+switchEnd :: b -> T Unary.Zero a -> b
+switchEnd x (Cons Empty.Cons) = x
 
 
-equal :: (C list, Eq a) => list a -> list a -> Bool
-equal xs ys = Fold.and $ Wrap $ zipWith (==) xs ys
+newtype WithPos a b n = WithPos {runWithPos :: T n a -> b}
 
-showsPrec :: (C list, Show a) => Int -> list a -> ShowS
+withPos ::
+   (Positive n) =>
+   (forall m. Natural m => T (Unary.Succ m) a -> b) -> T n a -> b
+withPos f = runWithPos $ Unary.switchPos (WithPos f)
+
+head :: (Positive n) => T n a -> a
+head = withPos (P.fst . viewL)
+
+tail :: T (Unary.Succ n) a -> T n a
+tail = P.snd . viewL
+
+singleton :: a -> T U1 a
+singleton x = x!:end
+
+minimum :: (Positive n, Ord a) => T n a -> a
+minimum = withPos (NonEmpty.minimum . switchL NonEmpty.cons)
+
+maximum :: (Positive n, Ord a) => T n a -> a
+maximum = withPos (NonEmpty.maximum . switchL NonEmpty.cons)
+
+
+
+instance (Natural n, Eq a) => Eq (T n a) where
+   xs == ys  =  Fold.and $ zipWith (==) xs ys
+
+showsPrec :: (Natural n, Show a) => Int -> T n a -> ShowS
 showsPrec p =
    P.showParen (p>5) . concatS .
    List.intersperse (P.showString "!:") .
    (++ [P.showString "end"]) .
    List.map (P.showsPrec 6) . toList
 
-toList :: (C list) => list a -> [a]
-toList = Fold.toList . Wrap
+instance (Natural n, Show a) => Show (T n a) where
+   showsPrec = showsPrec
 
-newtype Wrap list a = Wrap {unwrap :: list a}
 
+toList :: (Natural n) => T n a -> [a]
+toList = Fold.toList
 
-newtype Map a b list = Map {runMap :: list a -> list b}
 
-map :: C list => (a -> b) -> list a -> list b
+newtype Map a b n = Map {runMap :: T n a -> T n b}
+
+map :: Natural n => (a -> b) -> T n a -> T n b
 map f =
    runMap $
-   switch
-      (Map $ \Empty.Cons -> Empty.Cons)
-      (Map $ \(NonEmpty.Cons x xs) -> NonEmpty.Cons (f x) $ map f xs)
+   switchNat
+      (Map $ switchEnd end)
+      (Map $ switchL $ \x xs -> f x !: map f xs)
 
 
-newtype Sequence f a list = Sequence {runSequence :: list (f a) -> f (list a)}
+newtype Sequence f a n = Sequence {runSequence :: T n (f a) -> f (T n a)}
 
-sequenceA :: (Applicative f, C list) => list (f a) -> f (list a)
+sequenceA :: (Applicative f, Natural n) => T n (f a) -> f (T n a)
 sequenceA =
    runSequence $
-   switch
-      (Sequence $ \Empty.Cons -> App.pure Empty.Cons)
-      (Sequence $ \(NonEmpty.Cons x xs) -> liftA2 NonEmpty.Cons x $ sequenceA xs)
+   switchNat
+      (Sequence $ switchEnd $ App.pure end)
+      (Sequence $ switchL $ \x xs -> liftA2 (!:) x $ sequenceA xs)
 
 
-newtype Repeat a list = Repeat {runRepeat :: list a}
+newtype Repeat a n = Repeat {runRepeat :: T n a}
 
-repeat :: C list => a -> list a
+repeat :: Natural n => a -> T n a
 repeat a =
    runRepeat $
-   switch
-      (Repeat $ Empty.Cons)
-      (Repeat $ NonEmpty.Cons a $ repeat a)
+   switchNat
+      (Repeat end)
+      (Repeat $ a !: repeat a)
 
 
-newtype Zip a b c list = Zip {runZip :: list a -> list b -> list c}
+newtype Zip a b c n = Zip {runZip :: T n a -> T n b -> T n c}
 
-zipWith :: C list => (a -> b -> c) -> list a -> list b -> list c
+zipWith :: Natural n => (a -> b -> c) -> T n a -> T n b -> T n c
 zipWith f =
    runZip $
-   switch
-      (Zip $ \Empty.Cons Empty.Cons -> Empty.Cons)
-      (Zip $ \(NonEmpty.Cons a as) (NonEmpty.Cons b bs) ->
-         NonEmpty.Cons (f a b) $ zipWith f as bs)
+   switchNat
+      (Zip $ switchEnd $ switchEnd end)
+      (Zip $ switchL $ \a as -> switchL $ \b bs -> f a b !: zipWith f as bs)
 
 
-instance C list => Functor (Wrap list) where
-   fmap f = Wrap . map f . unwrap
+instance Natural n => Functor (T n) where
+   fmap = map
 
-instance C list => Foldable (Wrap list) where
+instance Natural n => Foldable (T n) where
    foldMap = foldMapDefault
 
-instance C list => Traversable (Wrap list) where
-   sequenceA = fmap Wrap . sequenceA . unwrap
+instance Natural n => Traversable (T n) where
+   sequenceA = sequenceA
 
-instance C list => Applicative (Wrap list) where
-   pure = Wrap . repeat
-   Wrap f <*> Wrap x = Wrap $ zipWith ($) f x
+instance Natural n => Applicative (T n) where
+   pure = repeat
+   f <*> x = zipWith ($) f x
 
 
+type family Position n :: *
+type instance Position Unary.Zero = Zero
+type instance Position (Unary.Succ n) = Succ (Position n)
+
 data Zero
 data Succ pos = Stop | Succ pos deriving (Eq, Ord, Show)
 
@@ -159,120 +187,129 @@
 instance Ord Zero where compare _ _ = EQ
 
 
-newtype Update a list pos = Update {runUpdate :: pos -> list a -> list a}
+newtype Index n = Index (Position n)
 
-updatePos :: C list => (a -> a) -> Position list -> list a -> list a
-updatePos f =
-   runUpdate $
-   switchPos
-      (Update $ \ _ Empty.Cons -> Empty.Cons)
-      (Update $ \pos0 (NonEmpty.Cons x xs) ->
-          case pos0 of
-             Stop -> NonEmpty.Cons (f x) xs
-             Succ pos1 -> NonEmpty.Cons x $ updatePos f pos1 xs)
+unpackSucc :: Index (Unary.Succ n) -> Succ (Index n)
+unpackSucc (Index n1) =
+   case n1 of
+      Stop -> Stop
+      Succ n0 -> Succ $ Index n0
 
-update :: C list => (a -> a) -> WrapPos list -> list a -> list a
-update f (WrapPos k) = updatePos f k
 
+newtype Update a n = Update {runUpdate :: Index n -> T n a -> T n a}
 
-newtype Index a list pos = Index {runIndex :: pos -> list a -> a}
+update :: Natural n => (a -> a) -> Index n -> T n a -> T n a
+update f =
+   runUpdate $
+   switchNat
+      (Update $ \ _ xs -> xs)
+      (Update $ \pos0 -> switchL $ \x xs ->
+         case unpackSucc pos0 of
+            Stop -> f x !: xs
+            Succ pos1 -> x !: update f pos1 xs)
 
-indexPos :: C list => Position list -> list a -> a
-indexPos =
+newtype PeekIndex a n = PeekIndex {runIndex :: Index n -> T n a -> a}
+
+index :: Natural n => Index n -> T n a -> a
+index =
    runIndex $
-   switchPos
-      (Index $ \ _ {- Zero -} Empty.Cons -> error "impossible index")
-      (Index $ \pos0 (NonEmpty.Cons x xs) ->
-          case pos0 of
+   switchNat
+      (PeekIndex $ \ _ {- Zero -} -> switchEnd $ error "impossible index")
+      (PeekIndex $ \pos0 -> switchL $ \x xs ->
+          case unpackSucc pos0 of
              Stop -> x
-             Succ pos1 -> indexPos pos1 xs)
-
-index :: C list => WrapPos list -> list a -> a
-index (WrapPos k) = indexPos k
+             Succ pos1 -> index pos1 xs)
 
-newtype Indices list pos = Indices {runIndices :: list pos}
+newtype Indices n = Indices {runIndices :: T n (Index n)}
 
-indicesPos :: C list => list (Position list)
-indicesPos =
+indices :: Natural n => T n (Index n)
+indices =
    runIndices $
-   switchPos
-      (Indices $ Empty.Cons)
-      (Indices $ NonEmpty.Cons Stop $ map Succ indicesPos)
-
-indices :: C list => list (WrapPos list)
-indices = map WrapPos indicesPos
+   switchNat
+      (Indices end)
+      (Indices $ i0 !: map succ indices)
 
-indicesInt :: C list => list Int
+indicesInt :: Natural n => T n Int
 indicesInt =
-   unwrap $ NonEmpty.init $ NonEmpty.scanl (+) 0 $ App.pure 1
-
-
-newtype WrapPos list = WrapPos {unwrapPos :: Position list}
-
-swapWrapPosSucc :: WrapPos (NonEmpty.T list) -> Succ (WrapPos list)
-swapWrapPosSucc (WrapPos n) =
-   case n of
-      Stop -> Stop
-      Succ m -> Succ (WrapPos m)
+   NonEmpty.init $ NonEmpty.scanl (+) 0 $ App.pure 1
 
 
-newtype NumFromPos list = NumFromPos {runNumFromPos :: WrapPos list -> Word}
+newtype NumFromIndex n = NumFromIndex {runNumFromIndex :: Index n -> Word}
 
-numFromPos :: C list => WrapPos list -> Word
-numFromPos =
-   runNumFromPos $
-   switch
-      (NumFromPos $ \_ -> error "numFromPos")
-      (NumFromPos $ \n ->
-         case swapWrapPosSucc n of
+numFromIndex :: Natural n => Index n -> Word
+numFromIndex =
+   runNumFromIndex $
+   switchNat
+      (NumFromIndex $ \_ -> error "numFromIndex")
+      (NumFromIndex $ \n ->
+         case unpackSucc n of
             Stop -> 0
-            Succ m -> 1 + numFromPos m)
+            Succ m -> 1 + numFromIndex m)
 
-newtype Compare a list =
-           Compare {runCompare :: WrapPos list -> WrapPos list -> a}
 
-instance (C list) => Eq (WrapPos list) where
+newtype Compare a n =
+           Compare {runCompare :: Index n -> Index n -> a}
+
+instance (Natural n) => Eq (Index n) where
    (==) =
       runCompare $
-      switch
-         (Compare $ \_ _ -> error "equalPos")
+      switchNat
+         (Compare $ \_ _ -> error "equalIndex")
          (Compare $ \i j ->
-             case (swapWrapPosSucc i, swapWrapPosSucc j) of
-                (Succ k, Succ l) -> k == l
-                (Stop, Stop) -> True
-                _ -> False)
+            case (unpackSucc i, unpackSucc j) of
+               (Succ k, Succ l) -> k == l
+               (Stop, Stop) -> True
+               _ -> False)
 
-instance (C list) => Ord (WrapPos list) where
+instance (Natural n) => Ord (Index n) where
    compare =
       runCompare $
-      switch
-         (Compare $ \_ _ -> error "equalPos")
+      switchNat
+         (Compare $ \_ _ -> error "compareIndex")
          (Compare $ \i j ->
-             case (swapWrapPosSucc i, swapWrapPosSucc j) of
-                (Succ k, Succ l) -> compare k l
-                (Stop, Stop) -> EQ
-                (Stop, Succ _) -> LT
-                (Succ _, Stop) -> GT)
+            case (unpackSucc i, unpackSucc j) of
+               (Succ k, Succ l) -> compare k l
+               (Stop, Stop) -> EQ
+               (Stop, Succ _) -> LT
+               (Succ _, Stop) -> GT)
 
 
-type N0 = Empty.T
-type N1 = GE1 Empty.T; type GE1 list = NonEmpty.T list
-type N2 = GE2 Empty.T; type GE2 list = NonEmpty.T (GE1 list)
-type N3 = GE3 Empty.T; type GE3 list = NonEmpty.T (GE2 list)
-type N4 = GE4 Empty.T; type GE4 list = NonEmpty.T (GE3 list)
-type N5 = GE5 Empty.T; type GE5 list = NonEmpty.T (GE4 list)
-type N6 = GE6 Empty.T; type GE6 list = NonEmpty.T (GE5 list)
-type N7 = GE7 Empty.T; type GE7 list = NonEmpty.T (GE6 list)
-type N8 = GE8 Empty.T; type GE8 list = NonEmpty.T (GE7 list)
+type GE1 n = Unary.Succ n
+type GE2 n = Unary.Succ (GE1 n)
+type GE3 n = Unary.Succ (GE2 n)
+type GE4 n = Unary.Succ (GE3 n)
+type GE5 n = Unary.Succ (GE4 n)
+type GE6 n = Unary.Succ (GE5 n)
+type GE7 n = Unary.Succ (GE6 n)
+type GE8 n = Unary.Succ (GE7 n)
 
-succ :: WrapPos list -> WrapPos (NonEmpty.T list)
-succ (WrapPos n) = WrapPos (Succ n)
+succ :: Index n -> Index (Unary.Succ n)
+succ (Index n) = Index (Succ n)
 
-i0 :: WrapPos (GE1 list); i0 = WrapPos Stop
-i1 :: WrapPos (GE2 list); i1 = succ i0
-i2 :: WrapPos (GE3 list); i2 = succ i1
-i3 :: WrapPos (GE4 list); i3 = succ i2
-i4 :: WrapPos (GE5 list); i4 = succ i3
-i5 :: WrapPos (GE6 list); i5 = succ i4
-i6 :: WrapPos (GE7 list); i6 = succ i5
-i7 :: WrapPos (GE8 list); i7 = succ i6
+i0 :: Index (GE1 n); i0 = Index Stop
+i1 :: Index (GE2 n); i1 = succ i0
+i2 :: Index (GE3 n); i2 = succ i1
+i3 :: Index (GE4 n); i3 = succ i2
+i4 :: Index (GE5 n); i4 = succ i3
+i5 :: Index (GE6 n); i5 = succ i4
+i6 :: Index (GE7 n); i6 = succ i5
+i7 :: Index (GE8 n); i7 = succ i6
+
+
+
+newtype
+   Uncurry a b n =
+      Uncurry {
+         runUncurry :: Curried n a b -> T n a -> b
+      }
+
+type family Curried n a b
+type instance Curried Unary.Zero a b = b
+type instance Curried (Unary.Succ n) a b = a -> Curried n a b
+
+uncurry :: (Unary.Natural n) => Curried n a b -> T n a -> b
+uncurry =
+   runUncurry $
+   Unary.switchNat
+      (Uncurry switchEnd)
+      (Uncurry $ \f -> switchL (\x -> uncurry (f x)))
diff --git a/src/Data/FixedLength/Unary.hs b/src/Data/FixedLength/Unary.hs
deleted file mode 100644
--- a/src/Data/FixedLength/Unary.hs
+++ /dev/null
@@ -1,249 +0,0 @@
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE EmptyDataDecls #-}
-module Data.FixedLength.Unary (
-   T, Position, List,
-   Zero, Succ(Stop, Succ),
-   toList, showsPrec,
-   map, zipWith, sequenceA, repeat,
-   index, update, indices, indicesInt, numFromIndex,
-   GE1, GE2, GE3, GE4, GE5, GE6, GE7, GE8,
-   i0, i1, i2, i3, i4, i5, i6, i7,
-   (!:), end, viewL, switchL,
-   ) where
-
-import qualified Type.Data.Num.Unary as Unary
-import Type.Data.Num.Unary (Natural, switchNat)
-
-import qualified Data.NonEmpty as NonEmpty
-import qualified Data.Empty as Empty
-
-import qualified Control.Applicative as App
-import qualified Data.Traversable as Trav
-import qualified Data.Foldable as Fold
-import qualified Data.List as List
-import Control.Applicative (Applicative, liftA2)
-import Data.Traversable (Traversable, foldMapDefault)
-import Data.Foldable (Foldable, foldMap)
-import Data.List ((++))
-import Data.Word (Word)
-
-import Data.Function (($), (.))
-import Data.Tuple (uncurry)
-import Data.Bool (Bool(False, True))
-import Data.Ord (Ord, Ordering(LT,EQ,GT), compare, (>))
-import Data.Eq (Eq, (==))
-
-import Text.Show.HT (concatS)
-
-import qualified Prelude as P
-import Prelude (Functor, fmap, Show, ShowS, Int, (+), error)
-
-
-type family List n :: * -> *
-type instance List Unary.Zero = Empty.T
-type instance List (Unary.Succ n) = NonEmpty.T (List n)
-
-newtype T n a = Cons (List n a)
-
-
-end :: T Unary.Zero a
-end = Cons Empty.Cons
-
-infixr 5 !:
-
-(!:) :: a -> T n a -> T (Unary.Succ n) a
-x !: Cons xs = Cons $ NonEmpty.Cons x xs
-
-viewL :: T (Unary.Succ n) a -> (a, T n a)
-viewL (Cons (NonEmpty.Cons x xs)) = (x, Cons xs)
-
-switchL :: (a -> T n a -> b) -> (T (Unary.Succ n) a -> b)
-switchL f = uncurry f . viewL
-
-
-instance (Natural n, Eq a) => Eq (T n a) where
-   xs == ys  =  Fold.and $ zipWith (==) xs ys
-
-showsPrec :: (Natural n, Show a) => Int -> T n a -> ShowS
-showsPrec p =
-   P.showParen (p>5) . concatS .
-   List.intersperse (P.showString "!:") .
-   (++ [P.showString "end"]) .
-   List.map (P.showsPrec 6) . toList
-
-toList :: (Natural n) => T n a -> [a]
-toList = Fold.toList
-
-
-newtype Map a b n = Map {runMap :: T n a -> T n b}
-
-map :: Natural n => (a -> b) -> T n a -> T n b
-map f =
-   runMap $
-   switchNat
-      (Map $ \(Cons Empty.Cons) -> end)
-      (Map $ switchL $ \x xs -> f x !: map f xs)
-
-
-newtype Sequence f a n = Sequence {runSequence :: T n (f a) -> f (T n a)}
-
-sequenceA :: (Applicative f, Natural n) => T n (f a) -> f (T n a)
-sequenceA =
-   runSequence $
-   switchNat
-      (Sequence $ \(Cons Empty.Cons) -> App.pure end)
-      (Sequence $ switchL $ \x xs -> liftA2 (!:) x $ sequenceA xs)
-
-
-newtype Repeat a n = Repeat {runRepeat :: T n a}
-
-repeat :: Natural n => a -> T n a
-repeat a =
-   runRepeat $
-   switchNat
-      (Repeat end)
-      (Repeat $ a !: repeat a)
-
-
-newtype Zip a b c n = Zip {runZip :: T n a -> T n b -> T n c}
-
-zipWith :: Natural n => (a -> b -> c) -> T n a -> T n b -> T n c
-zipWith f =
-   runZip $
-   switchNat
-      (Zip $ \(Cons Empty.Cons) (Cons Empty.Cons) -> end)
-      (Zip $ switchL $ \a as -> switchL $ \b bs -> f a b !: zipWith f as bs)
-
-
-instance Natural n => Functor (T n) where
-   fmap = map
-
-instance Natural n => Foldable (T n) where
-   foldMap = foldMapDefault
-
-instance Natural n => Traversable (T n) where
-   sequenceA = sequenceA
-
-instance Natural n => Applicative (T n) where
-   pure = repeat
-   f <*> x = zipWith ($) f x
-
-
-type family Position n :: *
-type instance Position Unary.Zero = Zero
-type instance Position (Unary.Succ n) = Succ (Position n)
-
-data Zero
-data Succ pos = Stop | Succ pos deriving (Eq, Ord, Show)
-
-instance Eq Zero where _==_ = True
-instance Ord Zero where compare _ _ = EQ
-
-
-newtype Index n = Index (Position n)
-
-unpackSucc :: Index (Unary.Succ n) -> Succ (Index n)
-unpackSucc (Index n1) =
-   case n1 of
-      Stop -> Stop
-      Succ n0 -> Succ $ Index n0
-
-
-newtype Update a n = Update {runUpdate :: Index n -> T n a -> T n a}
-
-update :: Natural n => (a -> a) -> Index n -> T n a -> T n a
-update f =
-   runUpdate $
-   switchNat
-      (Update $ \ _ xs -> xs)
-      (Update $ \pos0 -> switchL $ \x xs ->
-         case unpackSucc pos0 of
-            Stop -> f x !: xs
-            Succ pos1 -> x !: update f pos1 xs)
-
-newtype PeekIndex a n = PeekIndex {runIndex :: Index n -> T n a -> a}
-
-index :: Natural n => Index n -> T n a -> a
-index =
-   runIndex $
-   switchNat
-      (PeekIndex $ \ _ {- Zero -} (Cons Empty.Cons) -> error "impossible index")
-      (PeekIndex $ \pos0 -> switchL $ \x xs ->
-          case unpackSucc pos0 of
-             Stop -> x
-             Succ pos1 -> index pos1 xs)
-
-newtype Indices n = Indices {runIndices :: T n (Index n)}
-
-indices :: Natural n => T n (Index n)
-indices =
-   runIndices $
-   switchNat
-      (Indices end)
-      (Indices $ i0 !: map succ indices)
-
-indicesInt :: Natural n => T n Int
-indicesInt =
-   NonEmpty.init $ NonEmpty.scanl (+) 0 $ App.pure 1
-
-
-newtype NumFromIndex n = NumFromIndex {runNumFromIndex :: Index n -> Word}
-
-numFromIndex :: Natural n => Index n -> Word
-numFromIndex =
-   runNumFromIndex $
-   switchNat
-      (NumFromIndex $ \_ -> error "numFromIndex")
-      (NumFromIndex $ \n ->
-         case unpackSucc n of
-            Stop -> 0
-            Succ m -> 1 + numFromIndex m)
-
-
-newtype Compare a n =
-           Compare {runCompare :: Index n -> Index n -> a}
-
-instance (Natural n) => Eq (Index n) where
-   (==) =
-      runCompare $
-      switchNat
-         (Compare $ \_ _ -> error "equalIndex")
-         (Compare $ \i j ->
-            case (unpackSucc i, unpackSucc j) of
-               (Succ k, Succ l) -> k == l
-               (Stop, Stop) -> True
-               _ -> False)
-
-instance (Natural n) => Ord (Index n) where
-   compare =
-      runCompare $
-      switchNat
-         (Compare $ \_ _ -> error "compareIndex")
-         (Compare $ \i j ->
-            case (unpackSucc i, unpackSucc j) of
-               (Succ k, Succ l) -> compare k l
-               (Stop, Stop) -> EQ
-               (Stop, Succ _) -> LT
-               (Succ _, Stop) -> GT)
-
-
-type GE1 n = Unary.Succ n
-type GE2 n = Unary.Succ (GE1 n)
-type GE3 n = Unary.Succ (GE2 n)
-type GE4 n = Unary.Succ (GE3 n)
-type GE5 n = Unary.Succ (GE4 n)
-type GE6 n = Unary.Succ (GE5 n)
-type GE7 n = Unary.Succ (GE6 n)
-type GE8 n = Unary.Succ (GE7 n)
-
-succ :: Index n -> Index (Unary.Succ n)
-succ (Index n) = Index (Succ n)
-
-i0 :: Index (GE1 n); i0 = Index Stop
-i1 :: Index (GE2 n); i1 = succ i0
-i2 :: Index (GE3 n); i2 = succ i1
-i3 :: Index (GE4 n); i3 = succ i2
-i4 :: Index (GE5 n); i4 = succ i3
-i5 :: Index (GE6 n); i5 = succ i4
-i6 :: Index (GE7 n); i6 = succ i5
-i7 :: Index (GE8 n); i7 = succ i6