diff --git a/Control/SMonad.hs b/Control/SMonad.hs
deleted file mode 100644
--- a/Control/SMonad.hs
+++ /dev/null
@@ -1,196 +0,0 @@
---------------------------------------------------------------------------------
---------------------------------------------------------------------------------
---Module       : Type.SMonad
---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 NoMonomorphismRestriction #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE FunctionalDependencies #-}
-
--- | Example application of sets
---
--- This is quite similar to what the /rmonad/ package does, but we use preexisting sets rather than an associated datatype
---
--- * The apostrophed variants take proof objects as arguments
---
--- * The plain variants use 'auto'; that is, they assume that membership has been proved by an instance of 'Fact'
---
-module Control.SMonad where
-    
-import Type.Set
-import Type.Logic
-import Data.Set as Set
-    
-
-
-class SFunctor dom f | f -> dom where
-    sfmap' :: x :∈: dom ->
-             y :∈: dom ->
-                (x -> y) -> f x -> f y
-
-class SFunctor dom f => SApplicative dom f | f -> dom where
-    spure' :: x :∈: dom ->
-            x -> f x
-
-    sap' :: x :∈: dom ->
-           y :∈: dom ->
-           (x -> y) :∈: dom -> 
-               
-               f (x -> y) -> f x -> f y
-
-class SApplicative dom m => SMonad dom m | m -> dom where
-    sbind' :: x :∈: dom ->
-             y :∈: dom ->
-                 m x -> (x -> m y) -> m y
-    
--- * Variants using auto for the domain-membership proofs
-
-sfmap :: ( SFunctor dom f
-        , Fact (x :∈: dom)
-        , Fact (y :∈: dom) )
-                     =>
-                     (x -> y) -> f x -> f y
-sfmap = sfmap' auto auto
-
-spure :: ( SApplicative dom f
-        , Fact (x :∈: dom) )
-               
-                     =>
-                    x -> f x
-spure = spure' auto
-
-sap :: ( SApplicative dom f
-        , Fact (x :∈: dom)
-        , Fact (y :∈: dom)
-        , Fact ((x -> y) :∈: dom) )
-               
-                     =>
-                    f (x->y) -> f x -> f y
-sap = sap' auto auto auto
-
-
-sreturn' :: (SMonad dom f) => (x :∈: dom) -> x -> f x
-sreturn' = spure'
-           
-
-sreturn :: (SMonad dom f, Fact (x :∈: dom)) => x -> f x
-sreturn = spure
-
-sbind
-  :: (Fact (x :∈: dom), Fact (y :∈: dom), SMonad dom m) =>
-     m x -> (x -> m y) -> m y
-sbind = sbind' auto auto
-        
--- * Derived combinators
-
-sjoin'
-  :: (SMonad dom m) => (m y :∈: dom) -> (y :∈: dom) -> m (m y) -> m y
-sjoin' p1 p2 y = sbind' p1 p2 y id
-
-
-sjoin
-  :: (Fact (m y :∈: dom), Fact (y :∈: dom), SMonad dom m) =>
-     m (m y) -> m y
-sjoin y = sbind y id
-
--- | 'sfmap'' in terms of 'spure'' and 'sbind''
-sfmap'Default
-  :: (SMonad dom m) =>
-     (x :∈: dom) -> (y :∈: dom) -> (x -> y) -> m x -> m y
-sfmap'Default px py f x = sbind' px py x (\x0 -> sreturn' py (f x0))
-                         
--- | 'sap'' in terms of 'spure'' and 'sbind''
-sap'Default
-  :: (SMonad dom m) =>
-     (x :∈: dom)
-     -> (y :∈: dom)
-     -> ((x -> y) :∈: dom)
-     -> m (x -> y)
-     -> m x
-     -> m y
-sap'Default px py pxy f x = sbind' pxy py f
-                             (\f0 -> sbind' px py x (\x0 -> sreturn' py (f0 x0)))
-
-
-
-
-sliftA2'
-  :: (SApplicative dom f) =>
-       (x :∈: dom)
-     -> (y :∈: dom)
-     -> (z :∈: dom)
-     -> ((y -> z) :∈: dom)
-     -> (x -> y -> z)
-     -> f x
-     -> f y
-     -> f z
-sliftA2' px py pz pyz f x y = 
-
-    sap' py pz pyz
-    (sfmap' px pyz f x)
-    y
-
-
-
-sliftA2
-  :: (Fact ((x1 -> y) :∈: dom),
-      Fact (y :∈: dom),
-      Fact (x1 :∈: dom),
-      SApplicative dom f,
-      Fact (x :∈: dom)) =>
-     (x -> x1 -> y) -> f x -> f x1 -> f y
-sliftA2 f x y = sfmap f x `sap` y
-
-
-ssequence'
-  :: (SApplicative dom f) =>
-     (a :∈: dom)
-     -> ([a] :∈: dom)
-     -> (([a] -> [a]) :∈: dom)
-       
-     -> [f a]
-     -> f [a]
-
-ssequence' px pxs pxsxs = go
-    where
-      go [] = spure' pxs []
-      go (x:xs) = sliftA2' px pxs pxs pxsxs (:) x (go xs)
-
-
-ssequence
-  :: (Fact (a :∈: dom),
-      Fact ([a] :∈: dom),
-      Fact (([a] -> [a]) :∈: dom),
-      SApplicative dom f) =>
-     [f a] -> f [a]
-ssequence = ssequence' auto auto auto
-
-
-
-
-
-instance SFunctor OrdType Set where
-    sfmap' OrdType OrdType = Set.map
-
-instance SApplicative OrdType Set where
-    spure' OrdType = singleton
-    sap' = sap'Default
-
-instance SMonad OrdType Set where
-    sbind' OrdType OrdType xs f = Set.fold (\x r -> Set.union (f x) r) Set.empty xs
diff --git a/Data/Category.hs b/Data/Category.hs
deleted file mode 100644
--- a/Data/Category.hs
+++ /dev/null
@@ -1,184 +0,0 @@
---------------------------------------------------------------------------------
---------------------------------------------------------------------------------
---Module       : Data.Category
---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 TypeFamilies #-}
-{-# LANGUAGE NoMonomorphismRestriction #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE RankNTypes #-}
-
--- | This module is a stub!
-module Data.Category where
-
-import Type.Set
-import Type.Dummies
-import Type.Function
-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. a :∈: ob -> ExId hom a
-    -- | Composition
-    , 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) ->
-
-           ExC hom a b c
-
-                
-hask :: Cat Univ HaskFun
-hask = Cat (extendCod haskFunIsFun auto)
-       (\_ -> ExId HaskFun id)
-       (\_ _ _ -> ExC HaskFun HaskFun HaskFun (.))
-       
-kleisli :: Monad m => Cat Univ (KleisliHom m)
-kleisli = Cat (extendCod kleisliHomIsFun auto)
-          (\_ -> ExId KleisliHom return)
-          (\_ _ _ -> ExC KleisliHom KleisliHom KleisliHom (<=<))
-          
-
-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 :: (Fact (a :∈: ob)) => Cat ob hom -> ExId hom a
-idauto cat = getid cat auto
-
---      Cat ob hom -> bc -> ab -> ac
-
-
-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
-
--- 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
-      
--- foo :: forall a. a -> a
--- foo = idEx hask (Univ :: Univ a) go
---       where
---          go :: (((a, a), aa) :∈: HaskFun) -> aa -> (a -> a)
---          go HaskFun x = x
-
-       
-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/Data/Typeable/Extras.hs b/Data/Typeable/Extras.hs
--- a/Data/Typeable/Extras.hs
+++ b/Data/Typeable/Extras.hs
@@ -31,8 +31,7 @@
               Just b' -> b' == b
               Nothing -> False
 
-instance Ord TypeRep where
-    compare x y = -- compare the string representations first
+compareTypeReps x y = -- compare the string representations first
                   ((compare `on` show) x y)
                   `mappend`
                   -- not sure why 'typeRepKey' is in IO
@@ -43,5 +42,5 @@
 dynCompare :: (Typeable b, Typeable a, Ord b) => a -> b -> Ordering
 dynCompare a b = case cast a of
                    Just b' -> compare b' b
-                   Nothing -> let r = compare (typeOf a) (typeOf b)
+                   Nothing -> let r = compareTypeReps (typeOf a) (typeOf b)
                              in assert (r/=EQ) r
diff --git a/Helper.hs b/Helper.hs
--- a/Helper.hs
+++ b/Helper.hs
@@ -8,7 +8,7 @@
 import Control.Monad
 import Data.Generics
     
-decomposeForallT :: Type -> ([Type],Type)
+decomposeForallT :: Type -> (Cxt,Type)
 decomposeForallT (ForallT _ cxt t) = case decomposeForallT t of
                                        (x,y) -> (cxt++x,y)
 decomposeForallT t = ([],t)
diff --git a/Type/Dummies.hs b/Type/Dummies.hs
--- a/Type/Dummies.hs
+++ b/Type/Dummies.hs
@@ -53,6 +53,20 @@
 -- | Pair of types of kind @ SET3 @
 data PAIR3 (a :: SET3) (b :: SET3) (x :: SET2)
     
+data Bool0
+data Bool1
+    
+data BOOL :: SET where
+    Bool0 :: BOOL Bool0
+    Bool1 :: BOOL Bool1
+            
+elimBOOL :: BOOL a -> r Bool0 -> r Bool1 -> r a
+elimBOOL Bool0 x _ = x
+elimBOOL Bool1 _ x = x
+                      
+kelimBOOL :: BOOL a -> r -> r -> r
+kelimBOOL Bool0 x _ = x
+kelimBOOL Bool1 _ x = x
 
 
 -- data ΣPair (a :: SET) (b :: *)
diff --git a/Type/Function.hs b/Type/Function.hs
--- a/Type/Function.hs
+++ b/Type/Function.hs
@@ -404,7 +404,7 @@
 
 -- | Composition
 data ((g :: SET) :○: (f :: SET)) :: SET where
-    Compo :: forall a b c. 
+    Compo ::
             (b, c) :∈: g -> 
             (a, b) :∈: f -> 
             (g :○: f) (a, c)
@@ -954,6 +954,8 @@
 invId = SetEq (Subset (\(Inv (Incl xx)) -> Incl xx))
               (Subset (\(Incl xx) -> (Inv (Incl xx))))
 
+
+              
 
     
 -- TODO: inverse of composition
diff --git a/Type/Logic.hs b/Type/Logic.hs
--- a/Type/Logic.hs
+++ b/Type/Logic.hs
@@ -42,13 +42,31 @@
 import Data.Monoid hiding(All)
 import Control.Exception
 
+    
+-- class Prop p where
+--     proofs :: [p]
+-- instance (Prop a, Prop b) => Prop (Either a b) where
+--     proofs = diagonal [ fmap Left proofs, fmap Right proofs ]
+             
+-- instance (Prop a, Prop b) => Prop (a, b) where
+--     proofs = liftM2 (,) proofs proofs
+             
+-- instance (Prop a, Prop b) => Prop (a -> b) where
+--     proofs = case
+
 newtype Falsity = Falsity { elimFalsity :: forall a. a }
     deriving Typeable
+             
+-- instance Prop Falsity where proofs = []
+                                     
+-- instance Show Falsity where show _ = error "show: Proof of Falsity used"
 
+
 data Truth = TruthProof
            deriving (Show,Typeable)
                     
-instance Show Falsity where show _ = error "show: Proof of Falsity used"
+-- instance Prop Truth where proofs = [TruthProof]
+                    
 
 type Not a = a -> Falsity
     
@@ -97,57 +115,98 @@
     auto p q = q p
                
                
-data Decidable a = Decidable { decide :: Either (Not a) a }
-                 deriving (Show,Typeable)
+-- data Decidable a = Decidable { decide :: Either (Not a) a }
+--                  deriving (Show,Typeable)
              
-instance Fact (Decidable Falsity) where
-    auto = Decidable (Left id)
+-- instance Fact (Decidable Falsity) where
+--     auto = Decidable (Left id)
              
-instance Fact (Decidable Truth) where
-    auto = Decidable (Right TruthProof)
+-- instance Fact (Decidable Truth) where
+--     auto = Decidable (Right TruthProof)
 
-instance Fact (Decidable a -> Decidable b -> Decidable (a,b)) where
-    auto p1 p2 = Decidable (case (decide p1,decide p2) of
+-- instance Fact (Decidable a -> Decidable b -> Decidable (a,b)) where
+--     auto p1 p2 = Decidable (case (decide p1,decide p2) of
+--                               (Right p, Right q) -> Right (p,q)
+--                               (Left p, _) -> Left (p . fst)
+--                               (_, Left q) -> Left (q . snd)
+--                            )
+
+-- instance Fact (Decidable a -> Decidable b -> Decidable (Either a b)) where
+--     auto p1 p2 = Decidable (case (decide p1,decide p2) of
+--                               (Left p, Left q) -> Left (either p q)
+--                               (Right p, _) -> Right (Left p)
+--                               (_, Right q) -> Right (Right q)
+--                            )
+
+-- instance Fact (Decidable a -> Decidable b -> Decidable (a -> b)) where
+--     auto p1 p2 = Decidable (case decide p2 of
+--                               Right q -> Right (const q)
+--                               Left q -> case decide p1 of
+--                                          Right p -> Left (\f -> q (f p))
+--                                          Left p -> Right (elimFalsity . p)
+--                            )
+
+-- instance Fact (Decidable a -> Decidable (Not a)) where
+--     auto p1 = Decidable (case decide p1 of
+--                            Right p -> Left ($p)
+--                            Left p -> Right p
+--                         )
+
+-- isLeft :: Either t t1 -> Bool
+-- isLeft (Left _) = True
+-- isLeft (Right _) = False
+
+-- isRight = not . isLeft
+    
+-- instance Show (a :=: b) where show Refl = "Refl"
+
+class Decidable a where decide :: Either (Not a) a
+             
+instance (Decidable Falsity) where
+    decide = (Left id)
+             
+instance (Decidable Truth) where
+    decide = (Right TruthProof)
+
+instance (Decidable a, Decidable b) => Decidable (a,b) where
+    decide  = (case (decide ,decide ) of
                               (Right p, Right q) -> Right (p,q)
                               (Left p, _) -> Left (p . fst)
                               (_, Left q) -> Left (q . snd)
                            )
 
-instance Fact (Decidable a -> Decidable b -> Decidable (Either a b)) where
-    auto p1 p2 = Decidable (case (decide p1,decide p2) of
+instance (Decidable a, Decidable b) => Decidable (Either a b) where
+    decide  = (case (decide ,decide ) of
                               (Left p, Left q) -> Left (either p q)
                               (Right p, _) -> Right (Left p)
                               (_, Right q) -> Right (Right q)
                            )
 
-instance Fact (Decidable a -> Decidable b -> Decidable (a -> b)) where
-    auto p1 p2 = Decidable (case decide p2 of
+instance (Decidable a, Decidable b) => Decidable (a -> b) where
+    decide  = (case decide  of
                               Right q -> Right (const q)
-                              Left q -> case decide p1 of
+                              Left q -> case decide  of
                                          Right p -> Left (\f -> q (f p))
                                          Left p -> Right (elimFalsity . p)
                            )
 
-instance Fact (Decidable a -> Decidable (Not a)) where
-    auto p1 = Decidable (case decide p1 of
+instance (Decidable a) => Decidable (Not a) where
+    decide  = (case decide  of
                            Right p -> Left ($p)
                            Left p -> Right p
                         )
 
--- isLeft :: Either t t1 -> Bool
--- isLeft (Left _) = True
--- isLeft (Right _) = False
 
--- isRight = not . isLeft
 
 
-           
-    
--- instance Show (a :=: b) where show Refl = "Refl"
 
+
+
+
+
 -- | Existential quantification                                                         
 data Ex p where
-    Ex :: forall b. p b -> Ex p
+    Ex :: p b -> Ex p
          
          
 
@@ -190,8 +249,18 @@
 instance Show (a :=: b) where show Refl = "Refl"
 
 
-
+class Decidable1 s where
+    decide1 :: Either (Not (s a)) (s a)
 
+class Finite s where
+    enum :: [Ex s]
 
+instance Finite s => Decidable (Ex s) where
+    decide = case enum of
+               [] -> Left (\_ -> Falsity (assert False undefined))
+               [x] -> Right x
 
-                         
+-- instance Finite s => Decidable (Ex s) where
+--     decide = case enum of
+--                [] -> Left (\_ -> Falsity (assert False undefined))
+--                [x] -> Right x
diff --git a/Type/Set.hs b/Type/Set.hs
--- a/Type/Set.hs
+++ b/Type/Set.hs
@@ -51,7 +51,6 @@
 import Data.Typeable.Extras
 import Data.Data hiding (DataType)
     
-    
 
 {-----------------------------                                  
 emacs snippets for the funny characters (move behind the final parenthesis, press C-x C-e)
@@ -78,7 +77,6 @@
 #include "../Defs.hs"
     
     
-
     
 
 
@@ -92,6 +90,8 @@
 -- | Represents a proof that @set1@ is a subset of @set2@
 data (set1 :: SET) :⊆: (set2 :: SET) where
        Subset :: (forall a. a :∈: set1 -> a :∈: set2) -> set1 :⊆: set2
+                
+                
 
 -- | Coercion from subset to superset
 scoerce :: (set1 :⊆: set2) -> a :∈: set1 -> a :∈: set2 
@@ -211,7 +211,7 @@
                      
 -- | Union of a family
 data Unions (fam :: SET) :: SET where
-                          Unions :: forall s. Lower s :∈: fam -> a :∈: s -> Unions fam a
+                          Unions :: Lower s :∈: fam -> a :∈: s -> Unions fam a
             
 elimUnions :: Unions fam a -> (forall s. Lower s :∈: fam -> a :∈: s -> r) -> r
 elimUnions (Unions p1 p2) k = k p1 p2
@@ -336,6 +336,10 @@
 
 data ShowType :: SET where ShowType :: Show a => ShowType a
 instance Show a => Fact (a :∈: ShowType) where auto = ShowType
+                                                     
+-- data ReflectShow a = ReflectShow (ShowType a) a
+-- instance Show (ReflectShow a) where show (ReflectShow ShowType a) = show a
+
                                      
 -- | Example application
 getShow :: a :∈: ShowType -> a -> String
@@ -472,7 +476,7 @@
 
 -- | @V s@ is the sum of all types @x@ such that @s x@ is provable.
 data V (s :: SET) where
-    V :: forall x. s x -> x -> V s
+    V :: s x -> x -> V s
 
 liftEq :: (s :⊆: EqType) -> (s :⊆: TypeableType) -> (V s -> V s -> Bool)
 liftEq s s2 (V px x) (V py y) = 
diff --git a/type-settheory.cabal b/type-settheory.cabal
--- a/type-settheory.cabal
+++ b/type-settheory.cabal
@@ -1,17 +1,19 @@
 name:                type-settheory
-version:             0.1.2
+version:             0.1.3
 synopsis:            
- Type-level sets and functions expressed as types
+ Sets and functions-as-relations in the type system
 description:         
- Type classes can express sets and functions on the type level, but they are not first-class citizens. Here we take the approach of expressing type-level sets and functions as /types/. The instance system is replaced by value-level proofs which can be directly manipulated. In this way the Haskell type level can support a quite expressive constructive set theory; for example, we have:
+ Type classes can express sets and functions on the type level, but they are not first-class. This package expresses type-level sets and functions as /types/ instead. 
+ . 
+ Instances are replaced by value-level proofs which can be directly manipulated; this makes quite a bit of (constructive) set theory expressible; for example, we have:
  .
  * Subsets and extensional set equality
  .
- * Unions (binary or of sets of sets), intersections, cartesian products, powersets, and a kind of dependent sum and product 
+ * Unions (binary or of sets of sets), intersections, cartesian products, powersets, and a sort of dependent sum and product
  .
  * Functions and their composition, images, preimages, injectivity
  .
- The meaning of the proposition-types here is /not/ purely by convention; it is actually grounded in GHC \"reality\": A proof of @A :=: B@ gives us a safe coercion operator @A -> B@ (while the logic is inconsistent /at compile-time/ due to the fact that Haskell has general recursion, we still have that proofs of falsities are 'undefined' or non-terminating programs, so for example if 'Refl' is successfully pattern-matched, the proof must have been correct). 
+ The proposition-types (derived from the ':=:' equality type) aren't meaningful purely by convention; they relate to the rest of Haskell as follows: A proof of @A :=: B@ gives us a safe coercion operator @A -> B@ (while the logic is inevitably inconsistent /at compile-time/ since 'undefined' proves anything, I think that we still have the property that if the 'Refl' value is successfully pattern-matched, then the two parameters in its type are actually equal). 
  
 category:            Math, Language
 license:             BSD3
@@ -27,7 +29,7 @@
  location: http://code.haskell.org/~daniels/type-settheory
 
 Library
- build-depends:       base >= 4, base < 5
+ build-depends:        base >= 4, base < 5
                      , syb
                      , type-equality
                      , template-haskell
@@ -39,8 +41,6 @@
                      Type.Function
                      Type.Dummies
                      Type.Nat
-                     Data.Category
                      Data.Typeable.Extras
-                     Control.SMonad
  other-modules:       Helper, Defs
  ghc-options: