diff --git a/Data/Category.hs b/Data/Category.hs
--- a/Data/Category.hs
+++ b/Data/Category.hs
@@ -35,60 +35,109 @@
 import Type.Logic
 import Data.Type.Equality
 import Control.Monad
+import Control.Category
+import Prelude hiding(id,(.))
     
 
 -- | Category with type-level set of objects and type-level /hom/ function, but value-level composition and value-level definition of identity functions.
 data Cat ob hom =
     Cat {
       homIsFun :: ((ob :×: ob) :~>: Univ) hom
-    , getId :: forall a aa. ((a,a), aa) :∈: hom -> aa
+    , getid :: forall a. a :∈: ob -> ExId hom a
     -- | Composition
-    , cc :: forall a b c bc ab ac. 
+    , getc :: forall a b c. 
+           a :∈: ob ->
+           b :∈: ob ->
+           c :∈: ob ->
+           ExC hom a b c
+    }
+                
+-- | Existential wrapping of the identity function on a
+data ExId hom a where
+    ExId :: ((a,a),aa) :∈: hom -> aa -> ExId hom a
+           
+-- | Existential wrapping of the composition for types a,b,c
+data ExC hom a b c where
+    ExC ::
            ((b,c), bc) :∈: hom ->
            ((a,b), ab) :∈: hom ->
            ((a,c), ac) :∈: hom ->
+               
+           (bc -> ab -> ac) ->
 
-               bc -> ab -> ac
-    }
+           ExC hom a b c
+
                 
 hask :: Cat Univ HaskFun
 hask = Cat (extendCod haskFunIsFun auto)
-       (\HaskFun -> id)
-       (\HaskFun HaskFun HaskFun -> (.))
+       (\_ -> ExId HaskFun id)
+       (\_ _ _ -> ExC HaskFun HaskFun HaskFun (.))
        
 kleisli :: Monad m => Cat Univ (KleisliHom m)
 kleisli = Cat (extendCod kleisliHomIsFun auto)
-          (\KleisliHom -> return)
-          (\KleisliHom KleisliHom KleisliHom -> (<=<))
+          (\_ -> ExId KleisliHom return)
+          (\_ _ _ -> ExC KleisliHom KleisliHom KleisliHom (<=<))
+          
 
-idEx :: Cat ob hom -> ob a -> (forall aa. ((a,a),aa) :∈: hom -> aa -> r) -> r
-idEx cat a k = case total (homIsFun cat) (a :×: a) of
-                 ExSnd faa -> k faa (getId cat faa)
+fromControlCategory :: (Category hom) => Cat Univ (BiGraph hom)
+fromControlCategory = Cat biGraphIsFun
+                      (\_ -> ExId BiGraph id)
+                      (\_ _ _ -> ExC BiGraph BiGraph BiGraph (.))
+
+          
+-- | Lemma for constructing categories; abstracts the usage of the hom function's 'total'
+makeCat :: ((ob :×: ob) :~>: Univ) hom ->  
+          (forall a aa. ((a,a),aa) :∈: hom -> aa) ->
+              
+          (forall a b c bc ab ac.
+           ((b,c), bc) :∈: hom ->
+           ((a,b), ab) :∈: hom ->
+           ((a,c), ac) :∈: hom ->
+               
+           (bc -> ab -> ac)) ->
+
+
+          Cat ob hom
+
+makeCat hom k1 k2 =
+    Cat hom 
+     (\a -> case total hom (a :×: a) of
+             ExSnd aa -> ExId aa (k1 aa))
+     (\a b c -> case ( total hom (b :×: c)
+                    , total hom (a :×: b)
+                    , total hom (a :×: c) ) of
+                      
+                      ( ExSnd bc
+                       ,ExSnd ab
+                       ,ExSnd ac ) ->  
+
+                           ExC bc ab ac (k2 bc ab ac) )
+
+               
+                                 
                              
 -- idAuto :: forall ob hom a aa. Fact (((a, a), aa) :∈: hom) => Cat ob hom -> aa
--- -- idAuto cat _ = idn cat auto
--- idAuto cat _ = case total (homIsFun cat) 
 
-idAuto :: forall a aa hom ob. (Fact (((a, a), aa) :∈: hom)) => Cat ob hom -> aa
-idAuto cat = getId cat (auto :: ((a,a),aa) :∈: hom)
-             
--- ccAuto :: forall a b c bc ab ac hom ob.
---      (Fact (((b, c), bc) :∈: hom),
---       Fact (((a, b), ab) :∈: hom),
---       Fact (((a, c), ac) :∈: hom)) =>
+idauto :: (Fact (a :∈: ob)) => Cat ob hom -> ExId hom a
+idauto cat = getid cat auto
+
 --      Cat ob hom -> bc -> ab -> ac
-ccAuto cat = cc cat auto auto auto
 
-test :: a -> a
-test = idAuto hask
 
+cauto :: (Fact (a :∈: ob), Fact (b :∈: ob), Fact (c :∈: ob)) =>
+     Cat ob hom -> ExC hom a b c
+cauto cat = getc cat auto auto auto
 
-test2 :: (b -> c) -> (a -> b) -> a -> c
-test2 = ccAuto hask
+-- test :: a -> a
+-- test = idAuto hask
+
+
+-- test2 :: (b -> c) -> (a -> b) -> a -> c
+-- test2 = ccAuto hask
         
 
-test3 :: forall m a. Monad m => a -> m a
-test3 = idAuto kleisli
+-- test3 :: forall m a. Monad m => a -> m a
+-- test3 = idAuto kleisli
       
 -- foo :: forall a. a -> a
 -- foo = idEx hask (Univ :: Univ a) go
@@ -97,4 +146,39 @@
 --          go HaskFun x = x
 
        
--- data Functor omap
+data GFunctor ob1 hom1 ob2 hom2 f = 
+    GFunctor {
+      omapIsFun :: (ob1 :~>: ob2) f
+    , getfmap :: forall a b.
+              a :∈: ob1 ->
+              b :∈: ob1 ->
+              
+              ExFmap hom1 hom2 f a b
+                  
+    }
+
+data ExFmap hom1 hom2 f a b where
+    ExFmap ::
+              (a,fa) :∈: f ->
+              (b,fb) :∈: f ->
+              ((a,b),ab) :∈: hom1 ->
+              ((fa,fb),fafb) :∈: hom2 ->
+
+              (ab -> fafb) ->
+
+                  ExFmap hom1 hom2 f a b
+
+fromFunctor :: (Functor f) => GFunctor Univ HaskFun Univ HaskFun (Graph f)
+fromFunctor = GFunctor graphIsFun (\_ _ -> ExFmap Graph Graph HaskFun HaskFun fmap)
+
+
+                                  
+-- gmapCPS f afa bfb abab fafbfafb k
+--         = case ( total (homIsFun cat) (b :×: c)
+--                , total (homIsFun cat) (a :×: b)
+--                , total (homIsFun cat) (a :×: c) ) of
+                      
+--                       ( ExSnd bc
+--                        ,ExSnd ab
+--                        ,ExSnd ac ) ->  k bc ab ac (cc cat bc ab ac) 
+    
diff --git a/Defs.hs b/Defs.hs
new file mode 100644
--- /dev/null
+++ b/Defs.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE CPP #-}
+{-# OPTIONS -DMODULE #-} -- works because Pragmas are parsed only /before/ CPP has kicked in
+
+#ifdef MODULE
+module Defs where
+#endif
+
+#define PROP *
+#define SET (* -> PROP)
+#define SET1 (SET -> PROP)
+#define SET2 (SET1 -> PROP)
+#define SET3 (SET2 -> PROP)
+
+
diff --git a/Type/Dummies.hs b/Type/Dummies.hs
--- a/Type/Dummies.hs
+++ b/Type/Dummies.hs
@@ -27,7 +27,7 @@
 
 module Type.Dummies where
     
-#include "defs.h.hs"
+#include "../Defs.hs"
          
 -- | \"Kind-cast\" @ SET @ to @*@
 data Lower (a :: SET)
diff --git a/Type/Function.hs b/Type/Function.hs
--- a/Type/Function.hs
+++ b/Type/Function.hs
@@ -47,7 +47,7 @@
 
     
 
-#include "defs.h.hs"
+#include "../Defs.hs"
 
     
 -- * Preliminary
diff --git a/Type/Nat.hs b/Type/Nat.hs
--- a/Type/Nat.hs
+++ b/Type/Nat.hs
@@ -46,7 +46,7 @@
 import Control.Monad()
 import Control.Exception
 
-#include "defs.h.hs"
+#include "../Defs.hs"
          
 -- | Sets equipped with a constant and a function to itself
 data NStructure set z succ where
diff --git a/Type/Set.hs b/Type/Set.hs
--- a/Type/Set.hs
+++ b/Type/Set.hs
@@ -74,7 +74,8 @@
 
 
 
-#include "defs.h.hs"
+
+#include "../Defs.hs"
     
     
 
diff --git a/Type/defs.h.hs b/Type/defs.h.hs
deleted file mode 100644
--- a/Type/defs.h.hs
+++ /dev/null
@@ -1,56 +0,0 @@
---------------------------------------------------------------------------------
---------------------------------------------------------------------------------
--- |
---Module       : 
---Author       : 
---License      : 
---Copyright    : 
---
---Maintainer   : 
---Stability    : 
---Portability  : 
---
---------------------------------------------------------------------------------
---Description  : 
---------------------------------------------------------------------------------
---------------------------------------------------------------------------------
-
---------------------------------------------------------------------------------
---------------------------------------------------------------------------------
--- |
---Module       : 
---Author       : 
---License      : 
---Copyright    : 
---
---Maintainer   : 
---Stability    : 
---Portability  : 
---
---------------------------------------------------------------------------------
---Description  : 
---------------------------------------------------------------------------------
---------------------------------------------------------------------------------
-
---------------------------------------------------------------------------------
---------------------------------------------------------------------------------
--- |
---Module       : 
---Author       : 
---License      : 
---Copyright    : 
---
---Maintainer   : 
---Stability    : 
---Portability  : 
---
---------------------------------------------------------------------------------
---Description  : 
---------------------------------------------------------------------------------
---------------------------------------------------------------------------------
-
-#define PROP *
-#define SET (* -> PROP)
-#define SET1 (SET -> PROP)
-#define SET2 (SET1 -> PROP)
-#define SET3 (SET2 -> PROP)
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.1
+version:             0.1.2
 synopsis:            
  Type-level sets and functions expressed as types
 description:         
@@ -20,7 +20,6 @@
 maintainer:          daniels@community.haskell.org
 build-type:          Simple
 cabal-version:       >= 1.6
-extra-source-files:  Type/defs.h.hs
 stability:           Alpha
 
 source-repository head
@@ -43,5 +42,5 @@
                      Data.Category
                      Data.Typeable.Extras
                      Control.SMonad
- other-modules:       Helper
+ other-modules:       Helper, Defs
  ghc-options: