diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,5 +1,10 @@
 # Revision history for boring
 
+## 0.0.2
+
+- In `Fin` add: `append` and `split`
+- Add `(Enum a, Enum b) => Enum (Either a b)` instance
+
 ## 0.0.1
 
 - GHC-8.4.1 / base-4.11 support
diff --git a/Setup.hs b/Setup.hs
deleted file mode 100644
--- a/Setup.hs
+++ /dev/null
@@ -1,2 +0,0 @@
-import Distribution.Simple
-main = defaultMain
diff --git a/fin.cabal b/fin.cabal
--- a/fin.cabal
+++ b/fin.cabal
@@ -1,6 +1,8 @@
-name:                fin
-version:             0.0.1
-synopsis:            Nat and Fin: peano naturals and finite numbers
+cabal-version:      >=1.10
+name:               fin
+version:            0.0.2
+synopsis:           Nat and Fin: peano naturals and finite numbers
+category:           Data
 description:
   This package provides two simple types, and some tools to work with them.
   Also on type level as @DataKinds@.
@@ -31,40 +33,34 @@
   . Is a great package, but uses @GHC.TypeLits@.
   .
   * [type-natural](https://hackage.haskell.org/package/type-natural) depends
-    on @singletons@ package. @fin@ will try to stay light on the dependencies,
-    and support as many GHC versions as practical.
+  on @singletons@ package. @fin@ will try to stay light on the dependencies,
+  and support as many GHC versions as practical.
   .
   * [peano](https://hackage.haskell.org/package/peano) is very incomplete
   .
   * [nat](https://hackage.haskell.org/package/nat) as well.
   .
   * [PeanoWitnesses](https://hackage.haskell.org/package/PeanoWitnesses)
-    doesn't use @DataKinds@.
+  doesn't use @DataKinds@.
   .
   * [type-combinators](https://hackage.haskell.org/package/type-combinators)
-    is big package too.
+  is big package too.
 
-homepage:            https://github.com/phadej/vec
-bug-reports:         https://github.com/phadej/vec/issues
-license:             BSD3
-license-file:        LICENSE
-author:              Oleg Grenrus <oleg.grenrus@iki.fi>
-maintainer:          Oleg.Grenrus <oleg.grenrus@iki.fi>
-copyright:           (c) 2017 Oleg Grenrus
-category:            Data
-build-type:          Simple
-extra-source-files:  ChangeLog.md
-cabal-version:       >=1.10
+homepage:           https://github.com/phadej/vec
+bug-reports:        https://github.com/phadej/vec/issues
+license:            BSD3
+license-file:       LICENSE
+author:             Oleg Grenrus <oleg.grenrus@iki.fi>
+maintainer:         Oleg.Grenrus <oleg.grenrus@iki.fi>
+copyright:          (c) 2017 Oleg Grenrus
+build-type:         Simple
+extra-source-files: ChangeLog.md
 tested-with:
-  GHC==7.8.4,
-  GHC==7.10.3,
-  GHC==8.0.2,
-  GHC==8.2.2,
-  GHC==8.4.1
+  GHC ==8.8.1 || ==8.6.5 || ==8.4.4 || ==8.2.2 || ==8.0.2 || ==7.10.3 || ==7.8.4
 
 source-repository head
-  type:      git
-  location:  https://github.com/phadej/vec.git
+  type:     git
+  location: https://github.com/phadej/vec.git
 
 library
   exposed-modules:
@@ -72,49 +68,46 @@
     Data.Fin.Enum
     Data.Nat
     Data.Type.Nat
+
   build-depends:
-    base     >=4.7     && <4.12,
-    deepseq  >=1.3.0.2 && <1.5,
-    hashable >=1.2.7.0 && <1.3
+      base      >=4.7     && <4.13
+    , deepseq   >=1.3.0.2 && <1.5
+    , hashable  >=1.2.7.0 && <1.3
 
-  if !impl(ghc >= 8.0)
-    build-depends:
-      semigroups >=0.18.4 && <0.19
+  if !impl(ghc >=8.2)
+    build-depends: bifunctors >=5.5.3 && <5.6
 
-  if !impl(ghc >= 7.10)
+  if !impl(ghc >=8.0)
+    build-depends: semigroups >=0.18.4 && <0.19
+
+  if !impl(ghc >=7.10)
     build-depends:
-       nats >=1.1.2 && <1.2,
-       void >=0.7.2 && <0.8
+        nats  >=1.1.2 && <1.2
+      , void  >=0.7.2 && <0.8
 
-  ghc-options:         -Wall -fprint-explicit-kinds
-  hs-source-dirs:      src
-  default-language:    Haskell2010
+  ghc-options:      -Wall -fprint-explicit-kinds
+  hs-source-dirs:   src
+  default-language: Haskell2010
 
-  -- dump-core
-  -- if impl(ghc >= 8.0)
-  --  build-depends: dump-core
-  --  ghc-options: -fplugin=DumpCore -fplugin-opt DumpCore:core-html
+-- dump-core
+-- if impl(ghc >= 8.0)
+--  build-depends: dump-core
+--  ghc-options: -fplugin=DumpCore -fplugin-opt DumpCore:core-html
 
 test-suite inspection
-  type:                exitcode-stdio-1.0
-  main-is:             Inspection.hs
-  ghc-options:         -Wall -fprint-explicit-kinds
-  hs-source-dirs:      test
-  default-language:    Haskell2010
+  type:             exitcode-stdio-1.0
+  main-is:          Inspection.hs
+  ghc-options:      -Wall -fprint-explicit-kinds
+  hs-source-dirs:   test
+  default-language: Haskell2010
   build-depends:
-    base,
-    fin,
-    tagged,
-    inspection-testing >= 0.2.0.1 && <0.3
+      base
+    , fin
+    , inspection-testing  >=0.2.0.1 && <0.5
+    , tagged
 
-  if !impl(ghc >= 8.0)
+  if !impl(ghc >=8.0)
     buildable: False
 
   -- useful for development
   ghc-options:
-  -- -dsuppress-idinfo
-  -- -dsuppress-coercions
-  -- -dsuppress-type-applications
-  -- -dsuppress-module-prefixes
-  -- -dsuppress-type-signatures
-  -- -dsuppress-uniques
diff --git a/src/Data/Fin.hs b/src/Data/Fin.hs
--- a/src/Data/Fin.hs
+++ b/src/Data/Fin.hs
@@ -28,11 +28,17 @@
     inlineUniverse1,
     absurd,
     boring,
+    -- * Plus
+    weakenLeft,
+    weakenRight,
+    append,
+    split,
     -- * Aliases
     fin0, fin1, fin2, fin3, fin4, fin5, fin6, fin7, fin8, fin9,
     ) where
 
 import Control.DeepSeq    (NFData (..))
+import Data.Bifunctor     (bimap)
 import Data.Hashable      (Hashable (..))
 import Data.List.NonEmpty (NonEmpty (..))
 import Data.Proxy         (Proxy (..))
@@ -283,6 +289,64 @@
 -- 0
 boring :: Fin N.Nat1
 boring = Z
+
+-------------------------------------------------------------------------------
+-- Append & Split
+-------------------------------------------------------------------------------
+
+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 'N.Z
+    start = WeakenLeft absurd
+
+    step :: WeakenLeft m p -> WeakenLeft m ('N.S p)
+    step (WeakenLeft go) = WeakenLeft $ \n -> case n of
+        Z    -> Z
+        S n' -> S (go n')
+
+newtype WeakenLeft m n = WeakenLeft { getWeakenLeft :: Fin n -> Fin (N.Plus n m) }
+
+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
+    step (WeakenRight go) = WeakenRight $ \x -> S $ go x
+
+newtype WeakenRight m n = WeakenRight { getWeakenRight :: Fin m -> Fin (N.Plus n m) }
+
+-- | Append two 'Fin's together.
+--
+-- >>> append (Left fin2 :: Either (Fin N.Nat5) (Fin N.Nat4))
+-- 2
+--
+-- >>> append (Right fin2 :: Either (Fin N.Nat5) (Fin N.Nat4))
+-- 7
+--
+append :: forall n m. N.InlineInduction n => Either (Fin n) (Fin m) -> Fin (N.Plus n m)
+append (Left n)  = weakenLeft (Proxy :: Proxy m) n
+append (Right m) = weakenRight (Proxy :: Proxy n) m
+
+-- | Inverse of 'append'.
+--
+-- >>> split fin2 :: Either (Fin N.Nat2) (Fin N.Nat3)
+-- Right 0
+--
+-- >>> split fin1 :: Either (Fin N.Nat2) (Fin N.Nat3)
+-- Left 1
+--
+-- >>> map split universe :: [Either (Fin N.Nat2) (Fin N.Nat3)]
+-- [Left 0,Left 1,Right 0,Right 1,Right 2]
+--
+split :: forall n m. N.InlineInduction n => Fin (N.Plus n m) -> Either (Fin n) (Fin m)
+split = getSplit (N.inlineInduction start step) where
+    start :: Split m 'N.Z
+    start = Split Right
+
+    step :: Split m p -> Split m ('N.S p)
+    step (Split go) = Split $ \x -> case x of
+        Z    -> Left Z
+        S x' -> bimap S id $ go x'
+
+newtype Split m n = Split { getSplit :: Fin (N.Plus n m) -> Either (Fin n) (Fin m) }
 
 -------------------------------------------------------------------------------
 -- Aliases
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
@@ -27,10 +27,11 @@
 
 import Prelude hiding (Enum (..))
 
-import Data.Fin     (Fin)
-import Data.Nat     (Nat)
-import Data.Proxy   (Proxy (..))
-import GHC.Generics ((:+:) (..), M1 (..), U1 (..), V1)
+import Data.Bifunctor (bimap)
+import Data.Fin       (Fin)
+import Data.Nat       (Nat)
+import Data.Proxy     (Proxy (..))
+import GHC.Generics   ((:+:) (..), M1 (..), U1 (..), V1)
 
 import qualified Data.Fin      as F
 import qualified Data.Type.Nat as N
@@ -86,6 +87,13 @@
 
 -- | 'Ordering' ~ 3
 instance Enum Ordering
+
+-- | 'Either' ~ @+@
+instance (Enum a, Enum b, N.InlineInduction (EnumSize a)) => Enum (Either a b) where
+    type EnumSize (Either a b) = N.Plus (EnumSize a) (EnumSize b)
+
+    to   = bimap to to . F.split
+    from = F.append . bimap from from
 
 -------------------------------------------------------------------------------
 -- EnumSize
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
@@ -341,7 +341,7 @@
 proofMultZeroN :: Mult Nat0 n :~: Nat0
 proofMultZeroN = Refl
 
--- | @n * 0 = n@
+-- | @n * 0 = 0@
 proofMultNZero :: forall n proxy. SNatI n => proxy n -> Mult n Nat0 :~: Nat0
 proofMultNZero _ =
     getProofMultNZero (induction (ProofMultNZero Refl) step :: ProofMultNZero n)