diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2012, Hiromi ISHII
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Hiromi ISHII nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/Proof/Equational.hs b/Proof/Equational.hs
new file mode 100644
--- /dev/null
+++ b/Proof/Equational.hs
@@ -0,0 +1,115 @@
+{-# LANGUAGE DataKinds, FlexibleContexts, GADTs, PolyKinds, RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables, StandaloneDeriving, TypeFamilies     #-}
+{-# LANGUAGE TypeOperators, TypeSynonymInstances                       #-}
+module Proof.Equational ((:=:)(..), Equality(..), Preorder(..), reflexivity'
+                        ,(:\/:), (:/\:), (=>=), (=~=), Leibniz(..)
+                        , Reason(..), because, by, (===), start, byDefinition
+                        , admitted, Proxy(..), cong, cong', fromRefl
+                        , Proposition(..), (:~>), FromBool (..)
+                          -- * Re-exported modules
+                        , module Data.Singletons, module Data.Proxy
+                        ) where
+import Data.Proxy
+import Data.Singletons
+
+infix 4 :=:
+type a :\/: b = Either a b
+infixr 2 :\/:
+
+type a :/\: b = (a, b)
+infixr 3 :/\:
+
+data a :=: b where
+  Refl :: a :=: a
+
+data Leibniz a b = Leibniz { apply :: forall f. f a -> f b }
+
+fromRefl :: (Preorder eq, SingRep b) => a :=: b -> eq a b
+fromRefl Refl = reflexivity'
+
+deriving instance Show (a :=: b)
+
+class Preorder (eq :: k -> k -> *) where
+  reflexivity  :: Sing a -> eq a a
+  transitivity :: eq a b  -> eq b c -> eq a c
+
+class Preorder eq => Equality (eq :: k -> k -> *) where
+  symmetry     :: eq a b  -> eq b a
+
+instance Preorder (:=:) where
+  transitivity Refl Refl = Refl
+  reflexivity  _         = Refl
+
+instance Equality (:=:) where
+  symmetry     Refl      = Refl
+
+instance Preorder (->) where
+  reflexivity _ = id
+  transitivity = flip (.)
+
+leibniz_refl :: Leibniz a a
+leibniz_refl = Leibniz id
+
+instance Preorder Leibniz where
+  reflexivity _ = leibniz_refl
+  transitivity (Leibniz aEqb) (Leibniz bEqc) = Leibniz $ bEqc . aEqb
+
+instance Equality Leibniz where
+  symmetry eq  = unFlip $ apply eq $ Flip leibniz_refl
+
+newtype Flip f a b = Flip { unFlip :: f b a }
+
+data Reason eq x y where
+  Because :: Sing y -> eq x y -> Reason eq x y
+
+reflexivity' :: (SingRep x, Preorder r) => r x x
+reflexivity' = reflexivity sing
+
+by, because :: Sing y -> eq x y -> Reason eq x y
+because = Because
+by      = Because
+
+infixl 4 ===, =>=, =~=
+infix 5 `Because`
+infix 5 `because`
+
+(=>=) :: Preorder r => r x y -> Reason r y z -> r x z
+eq =>= (_ `Because` eq') = transitivity eq eq'
+
+(===) :: Equality eq => eq x y -> Reason eq y z -> eq x z
+(===) = (=>=)
+
+(=~=) :: Preorder r => r x y -> Sing y -> r x y
+eq =~= _ = eq
+
+start :: Preorder eq => Sing a -> eq a a
+start = reflexivity
+
+byDefinition :: (SingRep a, Preorder eq) => eq a a
+byDefinition = reflexivity sing
+
+admitted :: Reason eq x y
+admitted = undefined
+{-# WARNING admitted "There are some goals left yet unproven." #-}
+
+cong :: forall f a b. Proxy f -> a :=: b -> f a :=: f b
+cong Proxy Refl = Refl
+
+cong' :: (Sing m -> Sing (f m)) -> a :=: b -> f a :=: f b
+cong' _ Refl =  Refl
+
+class Proposition f where
+  type OriginalProp f n :: *
+  unWrap :: f n -> OriginalProp f n
+  wrap   :: OriginalProp f n -> f n
+
+type family   (xs :: [*]) :~> (a :: *) :: *
+type instance '[]       :~> a = a
+type instance (x ': xs) :~> a = x -> (xs :~> a)
+
+infixr 1 :~>
+
+class FromBool (c :: *) where
+  type Predicate c :: Bool
+  type Args c :: [*]
+  fromBool :: Predicate c ~ True => Args c :~> c
diff --git a/Proof/Propositional.hs b/Proof/Propositional.hs
new file mode 100644
--- /dev/null
+++ b/Proof/Propositional.hs
@@ -0,0 +1,52 @@
+{-# LANGUAGE TypeOperators #-}
+-- | Provides type synonyms for logical connectives.
+module Proof.Propositional ( type (/\), type (\/), Not, exfalso, orIntroL
+                           , orIntroR, orElim, andIntro, andElimL
+                           , andElimR, orAssocL, orAssocR
+                           , andAssocL, andAssocR
+                           ) where
+import Data.Void
+
+type a /\ b = (a, b)
+type a \/ b = Either a b
+type Not a  = a -> Void
+
+infixr 2 \/
+infixr 3 /\
+
+exfalso :: a -> Not a -> b
+exfalso a neg = absurd (neg a)
+
+orIntroL :: a -> a \/ b
+orIntroL = Left
+
+orIntroR :: b -> a \/ b
+orIntroR = Right
+
+orElim :: a \/ b -> (a -> c) -> (b -> c) -> c
+orElim aORb aTOc bTOc = either aTOc bTOc aORb
+
+andIntro :: a -> b -> a /\ b
+andIntro = (,)
+
+andElimL :: a /\ b -> a
+andElimL = fst
+
+andElimR :: a /\ b -> b
+andElimR = snd
+
+andAssocL :: a /\ (b /\ c) -> (a /\ b) /\ c
+andAssocL (a,(b,c)) = ((a,b), c)
+
+andAssocR :: (a /\ b) /\ c -> a /\ (b /\ c)
+andAssocR ((a,b),c) = (a,(b,c))
+
+orAssocL :: a \/ (b \/ c) -> (a \/ b) \/ c
+orAssocL (Left a)          = Left (Left a)
+orAssocL (Right (Left b))  = Left (Right b)
+orAssocL (Right (Right c)) = Right c
+
+orAssocR :: (a \/ b) \/ c -> a \/ (b \/ c)
+orAssocR (Left (Left a))  = Left a
+orAssocR (Left (Right b)) = Right (Left b)
+orAssocR (Right c)        = Right (Right c)
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/equational-reasoning.cabal b/equational-reasoning.cabal
new file mode 100644
--- /dev/null
+++ b/equational-reasoning.cabal
@@ -0,0 +1,23 @@
+-- Initial equational-reasoning.cabal generated by cabal init.  For further
+--  documentation, see http://haskell.org/cabal/users-guide/
+
+name:                equational-reasoning
+version:             0.0.1.0
+synopsis:            Proof assistant for Haskell using DataKinds & PolyKinds
+-- description:         
+license:             BSD3
+license-file:        LICENSE
+author:              Hiromi ISHII
+maintainer:          konn.jinro_at_gmail.com
+-- copyright:           
+category:            Math
+build-type:          Simple
+cabal-version:       >=1.8
+
+library
+  exposed-modules:     Proof.Equational, Proof.Propositional
+  build-depends:       base       == 4.6.*
+               ,       singletons == 0.8.*
+               ,       tagged     == 0.6.*
+               ,       void       == 0.6.*
+