diff --git a/Type/Function.hs b/Type/Function.hs
--- a/Type/Function.hs
+++ b/Type/Function.hs
@@ -41,7 +41,6 @@
 import Type.Logic
 import Type.Set
 import Data.Type.Equality
-import Control.Functor.Combinators.Flip
 import Control.Arrow
 import Helper
 import Type.Dummies
@@ -58,6 +57,19 @@
 data ExSnd (f :: SET) (a :: *) :: * where
     ExSnd :: (a, ex) :∈: f -> ExSnd f a
             
+-- | Totality
+type Total dom f =
+  (forall (a :: *). a :∈: dom -> ExSnd f a)            
+
+-- | Single-valuedness (CPS)
+type Sval f =
+          (forall a b1 b2 r.
+
+                   (a, b1) :∈: f -> 
+                   (a, b2) :∈: f -> 
+                   ((b1 ~ b2) => r) ->
+                   r)
+
     
 -- * Functions
             
@@ -74,17 +86,11 @@
            (f :⊆: (dom :×: cod)) 
 
            -- Totality
-       ->   (forall (a :: *). a :∈: dom -> ExSnd f a) 
+       ->  Total dom f
               
-           -- Single-valuedness (CPS)
-       ->   (forall a b1 b2 r.
-
-                   (a, b1) :∈: f -> 
-                   (a, b2) :∈: f -> 
-                   ((b1 ~ b2) => r) ->
-                   r)
+       ->  Sval f
             
-       ->   (dom :~>: cod) f
+       ->  (dom :~>: cod) f
            
 infixr 6 :~>:, :~~>:
 
@@ -451,7 +457,19 @@
 compo_idr f = funEq (compoIsFun f idIsFun) f
               (Subset (\(Compo fxy (Incl x)) -> fxy)) 
 
-        
+              
+
+compo_assoc
+  ::
+       (:~>:) s2 cod g
+     -> (:~>:) s21 s2 f
+     -> (:~>:) dom s21 f1
+     -> ((g :○: f) :○: f1) :==: (g :○: (f :○: f1))
+
+compo_assoc h g f = funEq ((compoIsFun h g) `compoIsFun` f)
+                          (h `compoIsFun` (g `compoIsFun` f))
+                          (Subset (\(Compo (Compo vh vg) vf) ->
+                                       Compo vh (Compo vg vf)))
 -- * Equalisers
 
 -- | Equalisers :D
@@ -642,7 +660,44 @@
           
                       where
                         auto = targetTuplingIsFun auto auto
+                               
 
+
+fst_tupling :: 
+               (dom :~>: cod1) f1 ->
+               (dom :~>: cod2) f2 ->
+               
+               Fst cod1 cod2 :○: (f1 :***: f2) :==: f1
+                   
+fst_tupling f1 f2 = funEq (compoIsFun fstIsFun (targetTuplingIsFun f1 f2)) f1
+                    (Subset (\(Compo (Fst _ _) (vf1 :***: _)) -> vf1))
+                    
+snd_tupling :: 
+               (dom :~>: cod1) f1 ->
+               (dom :~>: cod2) f2 ->
+               
+               Snd cod1 cod2 :○: (f1 :***: f2) :==: f2
+                   
+snd_tupling f1 f2 = funEq (compoIsFun sndIsFun (targetTuplingIsFun f1 f2)) f2
+                    (Subset (\(Compo (Snd _ _) (_ :***: vf2)) -> vf2))
+                    
+
+tupling_eta :: 
+               (dom :~>: (cod1 :×: cod2)) f ->
+
+               ((Fst cod1 cod2 :○: f)
+                        :***: 
+                (Snd cod1 cod2 :○: f))
+
+                :==: f
+                                                       
+tupling_eta f = funEq (targetTuplingIsFun (fstIsFun `compoIsFun` f) 
+                                          (sndIsFun `compoIsFun` f)) f
+
+                (Subset (\((Compo (Fst _ _) vf) :***: (Compo (Snd _ _) vf')) ->
+                             case sval f vf vf' of
+                               Refl -> vf))
+
 -- * Particular functions
                        
 -- | The type-level function:
@@ -926,9 +981,10 @@
                                   
                  ,'injective_Inv, 'inclusion_Injective, 'invId
                  ,'preimage_Image, 'image_Preimage
+                 ,'compo_assoc
 
 
-                                 
+                  ,'fst_tupling, 'snd_tupling, 'tupling_eta
                      ])
 
 
diff --git a/Type/Logic.hs b/Type/Logic.hs
--- a/Type/Logic.hs
+++ b/Type/Logic.hs
@@ -40,6 +40,7 @@
 import Control.Monad.Cont
 import Data.Typeable
 import Data.Monoid hiding(All)
+import Control.Exception
 
 newtype Falsity = Falsity { elimFalsity :: forall a. a }
     deriving Typeable
@@ -187,3 +188,10 @@
 
 deriving instance Typeable2 (:=:)
 instance Show (a :=: b) where show Refl = "Refl"
+
+
+
+
+
+
+                         
diff --git a/Type/Nat.hs b/Type/Nat.hs
new file mode 100644
--- /dev/null
+++ b/Type/Nat.hs
@@ -0,0 +1,173 @@
+--------------------------------------------------------------------------------
+--------------------------------------------------------------------------------
+--Module       : Type.Nat
+--Author       : Daniel Schüssler
+--License      : BSD3
+--Copyright    : Daniel Schüssler
+--
+--Maintainer   : Daniel Schüssler
+--Stability    : Experimental
+--Portability  : Uses various GHC extensions
+--
+--------------------------------------------------------------------------------
+--Description  : 
+--------------------------------------------------------------------------------
+--------------------------------------------------------------------------------
+
+
+
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE NoMonomorphismRestriction #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# OPTIONS -Wall #-}
+
+-- | TODO
+--
+-- * Prove that 'Initor' is an 'NMorphism'
+--
+-- * Prove that it is uniquely so
+--
+module Type.Nat where
+
+import Type.Set
+import Type.Dummies()
+import Type.Function
+import Type.Logic()
+import Data.Type.Equality
+import Control.Monad()
+import Control.Exception
+
+#include "defs.h.hs"
+         
+-- | Sets equipped with a constant and a function to itself
+data NStructure set z succ where
+                  NStructure :: z :∈: set -> (set :~>: set) succ ->
+                               NStructure set z succ
+
+-- | Structure-preserving maps of 'NStructure's
+data NMorphism set1 z1 succ1 set2 z2 succ2 (f :: SET) where
+    NMorphism :: NStructure set1 z1 succ1 ->
+                NStructure set2 z2 succ2 ->
+                (set1 :~>: set2) f ->
+                (f z1 :=: z2) ->
+                (f :○: succ1 
+                 :==:
+                 succ2 :○: f) ->
+
+                NMorphism set1 z1 succ1 z2 set2 succ2 f
+                          
+-- | Expresses that @(set1,z1,succ1)@ is initial in the cat of 'NStructure's, in other words, that it is isomorphic to the natural numbers
+data NInitial set1 z1 succ1 where
+    NInitial :: (forall z2 set2 succ2. ExUniq1 (NMorphism set1 z1 succ1 z2 set2 succ2))
+               -> NInitial set1 z1 succ1
+                 
+
+-- data IsPeano nat z succ = 
+--     IsPeano {
+--       succ_fun :: (nat :~>: nat) succ
+--     , succ_inj :: Injective succ
+--     , not_succ_zero :: forall n. n :∈: nat -> Not ((n,z) :∈: succ)
+--     , induction :: forall set. z :∈: set -> 
+--                   (forall n n1. n :∈: set ->   
+--                            (n,n1) :∈: succ ->
+--                            n1 :∈: set) ->
+
+--                   set :==: nat
+--     }
+
+-- | Actually any pair of (nullary type, unary type constructor) gives us a copy of the naturals; let's call these /TNats/
+data TNat z s :: SET where
+    IsZ :: TNat z s z
+    IsS :: TNat z s n -> TNat z s (s n)
+-- | Successor function made from a unary type constructor
+data Succ z s :: SET where 
+    Succ :: n :∈: TNat z s -> Succ z s (n,s n)
+           
+succFun :: (TNat z s :~>: TNat z s) (Succ z s)
+succFun = IsFun (Subset (\(Succ n) -> n :×: IsS n))
+          (ExSnd . Succ)
+          (\(Succ _) (Succ _) k -> k)
+          
+tyconNStruct :: NStructure (TNat z s) z (Succ z s)
+tyconNStruct = NStructure IsZ succFun
+               
+-- | The unique morphism from an 'TNat' to any 'NStructure' 
+--
+-- NB: @s@ is a type constructor, but @succ2@ is a Function ('IsFun')
+data Initor z s z2 succ2 :: SET where
+      InitorZ :: Initor z s z2 succ2 (z,z2)
+      InitorS :: Initor z s z2 succ2 (n1, n2) -> 
+                (n2,sn2) :∈: succ2 ->
+                Initor z s z2 succ2 (s n1, sn2)
+                       
+
+initorFun :: forall z s set2 z2 succ2. NStructure set2 z2 succ2 -> 
+            (TNat z s :~>: set2) (Initor z s z2 succ2)
+                                
+initorFun (NStructure z2 succ2) =
+
+    let 
+        prelation :: pair :∈: Initor z s z2 succ2 -> 
+                         pair :∈: TNat z s :×: set2
+                              
+        prelation InitorZ = IsZ :×: z2
+        prelation (InitorS i0 p) = case prelation i0 of
+                                          q1 :×: _ -> 
+                                                 IsS q1 
+                                                    :×: 
+                                                 inCod succ2 p
+                                                       
+        ptotal :: n :∈: TNat z s -> ExSnd (Initor z s z2 succ2) n
+        ptotal IsZ = ExSnd InitorZ
+        ptotal (IsS n) = 
+            case ptotal n of
+              ExSnd (inn2 :: Initor z s z2 succ2 (n,n2)) -> 
+                  
+                         (let
+                             succ2ofn2 :: ExSnd succ2 n2
+                             succ2ofn2 =
+                                 case prelation inn2 of
+                                   _ :×: n2 ->
+                                       total succ2 n2
+                          in
+                           case succ2ofn2 of 
+                             ExSnd e -> ExSnd (InitorS inn2 e))
+                         
+        psval :: Initor z s z2 succ2 (n,n2) ->
+                Initor z s z2 succ2 (m,m2) ->
+                    n2 :=: m2
+                       
+        psval InitorZ InitorZ = Refl
+        psval (InitorS inn2 succ2n2) (InitorS inn2' succ2'n2') = 
+            case psval inn2 inn2' of
+              Refl ->
+                  case sval succ2 succ2n2 succ2'n2' of
+                    Refl -> Refl
+                           
+        -- Currently impossible without 'undefined' :-(
+
+        -- http://www.nabble.com/Is-it-possible-to-prove-type-*non*-equality-in-Haskell--to25142999.html 
+        psval (InitorS _ _) InitorZ = assert False undefined
+        psval InitorZ (InitorS _ _) = assert False undefined
+     in
+       IsFun (Subset prelation) ptotal (\p1 p2 k -> case psval p1 p2 of 
+                                                     Refl -> k)
+
+
+-- tyconPeano :: IsPeano (TNat z s) z (Succ z s)
+-- tyconPeano = IsPeano succFun
+--              (Injective (\(Succ _) (Succ _) k -> k))
+             
+--              undefined undefined
+
+
+
diff --git a/Type/Set.hs b/Type/Set.hs
--- a/Type/Set.hs
+++ b/Type/Set.hs
@@ -45,8 +45,6 @@
 import Type.Logic
 import Type.Dummies
 import Data.Monoid
-import Control.Functor.Extras
-import Control.Functor.Combinators.Flip
 import Control.Monad
 import Helper
 import Control.Applicative
@@ -456,6 +454,13 @@
 --     =>      Fact (s1 :⊆: s3) where
         
 --         auto = subsetTrans auto auto
+
+-- * Unique existence of sets
+
+-- | Unique existence, unlowered
+data ExUniq1 (p :: SET -> *) where
+    ExUniq1 :: p b -> (forall b'. p b' -> b :==: b') -> ExUniq1 p
+
 
 
                
diff --git a/Type/Set/Example.hs b/Type/Set/Example.hs
--- a/Type/Set/Example.hs
+++ b/Type/Set/Example.hs
@@ -19,8 +19,6 @@
 import Type.Function
 import Type.Dummies
 import Data.Monoid
-import Control.Functor.Extras
-import Control.Functor.Combinators.Flip
 import Control.Monad
 import Helper
 import Control.Applicative
diff --git a/type-settheory.cabal b/type-settheory.cabal
--- a/type-settheory.cabal
+++ b/type-settheory.cabal
@@ -1,5 +1,5 @@
 name:                type-settheory
-version:             0.1
+version:             0.1.1
 synopsis:            
  Type-level sets and functions expressed as types
 description:         
@@ -30,7 +30,7 @@
 Library
  build-depends:       base >= 4, base < 5
                      , syb
-                     , category-extras, type-equality
+                     , type-equality
                      , template-haskell
                      , mtl
                      , containers
@@ -39,6 +39,7 @@
                      Type.Set.Example
                      Type.Function
                      Type.Dummies
+                     Type.Nat
                      Data.Category
                      Data.Typeable.Extras
                      Control.SMonad