diff --git a/Makefile b/Makefile
deleted file mode 100644
--- a/Makefile
+++ /dev/null
@@ -1,1 +0,0 @@
-include ../cho-home-cabal-make.inc
diff --git a/src/Data/Ty.hs b/src/Data/Ty.hs
--- a/src/Data/Ty.hs
+++ b/src/Data/Ty.hs
@@ -1,4 +1,7 @@
 {-# LANGUAGE TypeOperators, ScopedTypeVariables #-}
+{-# LANGUAGE GADTs, PatternGuards #-}
+{-# LANGUAGE KindSignatures #-} -- AsPairTy
+
 {-# OPTIONS_GHC -Wall #-}
 ----------------------------------------------------------------------
 -- |
@@ -12,10 +15,14 @@
 -- Typed typerefs
 ----------------------------------------------------------------------
 
-module Data.Ty (Ty,tyRep,ty,tyOf,Typeable,module Data.IsTy) where
+module Data.Ty
+  ( Typeable,module Data.IsTy
+  , Ty,tyRep,ty,tyOf,tyOf1,tyOf2, (=:=)
+  , AsPairTy(..), asPairTy
+  ) where
 
 
-import Data.Typeable (Typeable,TypeRep,typeOf)
+import Data.Typeable (Typeable,TypeRep,typeOf,TyCon,typeRepTyCon,splitTyConApp)
 import Unsafe.Coerce (unsafeCoerce)
 
 import Data.Proof.EQ ((:=:)(..))
@@ -23,7 +30,7 @@
 import Data.IsTy
 
 -- | Phantom type wrapper around a 'TypeRep'
-data Ty a = Ty { tyRep :: TypeRep }
+data Ty a = Ty { tyRep :: TypeRep } deriving Eq
 
 instance Show (Ty a) where show = show . tyRep
 
@@ -37,3 +44,52 @@
 -- | The 'Ty' of a value
 tyOf :: Typeable a => a -> Ty a
 tyOf a = Ty (typeOf a)
+
+-- | The 'Ty' of a value from a constructor application
+tyOf1 :: forall f a. Typeable a => f a -> Ty a
+tyOf1 _ = Ty (typeOf (undefined :: a))
+
+-- | The 'Ty' of a value from a nested constructor application
+tyOf2 :: forall g f a. Typeable a => g (f a) -> Ty a
+tyOf2 _ = Ty (typeOf (undefined :: a))
+
+-- | Equality of typed values. @'Just' 'Refl'@ means the the types match and the
+-- values match.
+(=:=) :: forall a b. (Typeable a, Typeable b, Eq a) =>
+         a -> b -> Maybe (a :=: b)
+oa =:= ob
+  | Just Refl <- tyOf oa `tyEq` tyOf ob, oa == ob = Just Refl
+  | otherwise                                     = Nothing
+
+{-
+
+-- | Equality of wrapped typed values. @'Just' 'Refl'@ means the the types match
+-- and the values match.
+valTyEq1 :: forall f a b. (Typeable a, Typeable b, Eq (f a)) =>
+            f a -> f b -> Maybe (a :=: b)
+oa `valTyEq1` ob
+  | Just Refl <- tyOf1 oa `tyEq` tyOf1 ob, oa == ob = Just Refl
+  | otherwise                                       = Nothing
+
+-- | Equality of doubly wrapped typed values. @'Just' 'Refl'@ means the the
+-- types match and the values match.
+valTyEq2 :: forall g f a b. (Typeable a, Typeable b, Eq (g (f a))) =>
+            g (f a) -> g (f b) -> Maybe (a :=: b)
+oa `valTyEq2` ob
+  | Just Refl <- tyOf2 oa `tyEq` tyOf2 ob, oa == ob = Just Refl
+  | otherwise                                       = Nothing
+
+-}
+
+data AsPairTy :: * -> * where
+  PairTy :: Ty a -> Ty b -> AsPairTy (a, b)
+
+pairCon :: TyCon
+pairCon = typeRepTyCon (typeOf (False,True))
+
+asPairTy :: Ty t -> Maybe (AsPairTy t)
+asPairTy (Ty t) | con == pairCon = unsafeCoerce (Just (PairTy (Ty a) (Ty b)))
+                | otherwise      = Nothing
+ where
+   (con,args) = splitTyConApp t
+   [a,b] = args
diff --git a/ty.cabal b/ty.cabal
--- a/ty.cabal
+++ b/ty.cabal
@@ -1,32 +1,32 @@
 Name:                ty
-Version:             0.0.2
-Cabal-Version:       >= 1.2
+Version:             0.1.0
 Synopsis:            Typed type representations and equality proofs
 Category:            Data
+Cabal-Version:       >= 1.6
 Description:
   Typed type representations and equality proofs
   .
   Project wiki page: <http://haskell.org/haskellwiki/ty>
   .
-  Copyright 2009 Conal Elliott; BSD3 license.
+  Copyright 2009-2012 Conal Elliott; BSD3 license.
 Author:              Conal Elliott 
 Maintainer:          conal@conal.net
-Homepage:            http://haskell.org/haskellwiki/ty
-Package-Url:         http://code.haskell.org/ty
-Copyright:           (c) 2009 by Conal Elliott
+Homepage:            https://github.com/conal/ty
+Copyright:           (c) 2009-2012 by Conal Elliott
 License:             BSD3
 License-File:        COPYING
 Stability:           experimental
 build-type:          Simple
 
+source-repository head
+  type:     git
+  location: git://github.com/conal/ty.git
+
 Library
   hs-Source-Dirs:      src
-  Extensions:
   Build-Depends:       base<5
   Exposed-Modules:     
                        Data.Proof.EQ
                        Data.IsTy
                        Data.Ty
   ghc-options:         -Wall
-
---  ghc-prof-options:    -prof -auto-all 
diff --git a/wikipage.tw b/wikipage.tw
deleted file mode 100644
--- a/wikipage.tw
+++ /dev/null
@@ -1,13 +0,0 @@
-[[Category:Packages]]
-
-== Abstract ==
-
-'''proof-eq''' is a simple, one-module package for working with equality proofs.
-
-Besides this wiki page, here are more ways to find out about proof-eq:
-* Visit the [http://hackage.haskell.org/cgi-bin/hackage-scripts/package/proof-eq Hackage page] for library documentation and to download & install.
-* Or install with <tt>cabal install proof-eq</tt>.
-* Get the code repository: <tt>http://code.haskell.org/~conal/code/applicative-numbers</tt>.
-<!-- * See the [[proof-eq/Versions| version history]]. -->
-
-<!-- Please leave comments at the [[Talk:proof-eq|Talk page]]. -->