diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright Author name here (c) 2018
+
+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 Author name here 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/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,4 @@
+# gdp: Ghosts of Departed Proofs
+
+
+
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/app/Main.hs b/app/Main.hs
new file mode 100644
--- /dev/null
+++ b/app/Main.hs
@@ -0,0 +1,84 @@
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE GADTs         #-}
+
+module Main where
+
+import GDP
+
+import Data.Ord
+import qualified Data.List as L
+
+-- An unsafe merge. This relies on the user remembering to
+-- sort both of the inputs using the same comparator passed
+-- as the first argument to `unsafeMergeBy`. Otherwise, it
+-- will produce nonsense.
+unsafeMergeBy :: (a -> a -> Ordering) -> [a] -> [a] -> [a]
+unsafeMergeBy comp xs ys = go xs ys
+  where
+    go [] ys' = ys'
+    go xs' [] = xs'
+    go (x:xs') (y:ys') = case comp x y of
+      GT -> y : go (x:xs') ys'
+      _  -> x : go xs' (y:ys')
+
+
+-- Introduce a predicate `SortedBy comp`, indicating that
+-- the value has been sorted by the comparator named `comp`.
+newtype SortedBy comp name = SortedBy Defn
+
+-- Sort a value using the comparator named `comp`. The
+-- resulting value will satisfy `SortedBy comp`.
+sortBy :: ((a -> a -> Ordering) ~~ comp)
+       -> [a]
+       -> ([a] ?SortedBy comp)
+sortBy (The comp) xs = assert (L.sortBy comp xs)
+
+-- Merge the two lists using the comparator named `comp`. The lists must
+-- have already been sorted using `comp`, and the result will also be
+-- sorted with respect to `comp`.
+mergeBy :: ((a -> a -> Ordering) ~~ comp)
+        -> ([a] ?SortedBy comp)
+        -> ([a] ?SortedBy comp)
+        -> ([a] ?SortedBy comp)
+mergeBy (The comp) (The xs) (The ys) = assert (unsafeMergeBy comp xs ys)
+
+newtype Opposite comp = Opposite Defn
+
+-- A named version of the opposite ordering.
+opposite :: ((a -> a -> Ordering) ~~ comp)
+         -> ((a -> a -> Ordering) ~~ Opposite comp)
+opposite (The comp) = defn $ \x y -> case comp x y of
+  GT -> LT
+  EQ -> EQ
+  LT -> GT
+
+newtype Reverse xs = Reverse Defn
+
+-- A named version of Prelude's 'reverse'.
+rev :: ([a] ~~ xs) -> ([a] ~~ Reverse xs)
+rev (The xs) = defn (reverse xs)
+
+-- A lemma about reversing sorted lists.
+rev_ord_lemma :: SortedBy comp xs -> Proof (SortedBy (Opposite comp) (Reverse xs))
+rev_ord_lemma _ = axiom
+
+-- Usage example.
+main :: IO ()
+main = do
+  name compare $ \up -> do
+
+    -- Read two lists and sort them in ascending order, then
+    -- merge them and print the result.
+    xs <- sortBy up <$> (readLn :: IO [Int])
+    ys <- sortBy up <$> readLn
+    let ans1 = mergeBy up xs ys
+    print (the ans1)
+
+    -- Now reverse the two lists and merge them using the
+    -- descending comparator. This requires a proof that
+    -- the reversed lists are sorted by the opposite of `up`,
+    -- which we provide using (...?).
+    let down = opposite up
+        ans2 = mergeBy down (rev' xs) (rev' ys)
+        rev' = rev ...? rev_ord_lemma
+    print (the ans2)
diff --git a/gdp.cabal b/gdp.cabal
new file mode 100644
--- /dev/null
+++ b/gdp.cabal
@@ -0,0 +1,51 @@
+name:                gdp
+version:             0.0.0.1
+synopsis:            Reason about invariants and preconditions with ghosts of departed proofs.
+description:         Reason about invariants and preconditions with ghosts of departed proofs.
+                     The GDP library implements building blocks for creating and working with
+                     APIs that may carry intricate preconditions for proper use. As a library
+                     author, you can use `gdp` to encode your API's preconditions and invariants,
+                     so that they will be statically checked at compile-time.
+                     As a library user, you can use the `gdp` deduction rules to codify your
+                     proofs that you are using the library correctly.
+homepage:            https://github.com/githubuser/gdp#readme
+license:             BSD3
+license-file:        LICENSE
+author:              Matt Noonan
+maintainer:          matt.noonan@gmail.com
+copyright:           (c) 2018 Matt Noonan
+category:            Safe
+build-type:          Simple
+extra-source-files:  README.md
+cabal-version:       >=1.10
+
+library
+  hs-source-dirs:      src
+  exposed-modules:     GDP
+                     , Data.Arguments
+                     , Data.Refined
+                     , Data.The
+                     , Logic.Classes
+                     , Logic.NegClasses
+                     , Logic.Propositional
+                     , Logic.Proof
+                     , Theory.Equality
+                     , Theory.Named
+                     
+  build-depends:       base >= 4.7 && < 5
+                     , lawful
+                     
+  default-language:    Haskell2010
+
+executable gdp
+  hs-source-dirs:      app
+  main-is:             Main.hs
+  ghc-options:         -threaded -rtsopts -with-rtsopts=-N
+  build-depends:       base
+                     , gdp
+                     
+  default-language:    Haskell2010
+
+source-repository head
+  type:     git
+  location: https://github.com/matt-noonan/gdp
diff --git a/src/Data/Arguments.hs b/src/Data/Arguments.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Arguments.hs
@@ -0,0 +1,49 @@
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE PolyKinds             #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances     #-}
+
+{-|
+  Module      :  Data.Arguments
+  Copyright   :  (c) Matt Noonan 2018
+  License     :  BSD-style
+  Maintainer  :  matt.noonan@gmail.com
+  Portability :  portable
+-}
+
+module Data.Arguments
+  ( Argument(..)
+  , LHS, RHS
+  , Arg(..)
+  , arg
+  ) where
+
+-- | Get or modify a type within a larger type.
+--   This is entirely a type-level operation, there
+--   is nothing corresponding to a value access or update.
+class Argument (f :: k1) (n :: k2) where
+  type GetArg f n   :: k1
+  type SetArg f n x :: k1
+
+-- | Position: the left-hand side of a type.
+data LHS
+
+-- | Position: the right-hand side of a type.
+data RHS
+
+instance Argument (Either a b) LHS where
+  type GetArg (Either a b) LHS    = a
+  type SetArg (Either a b) LHS a' = Either a' b
+
+instance Argument (Either a b) RHS where
+  type GetArg (Either a b) RHS    = b
+  type SetArg (Either a b) RHS b' = Either a b'
+
+-- | A specialized proxy for arguments.
+data Arg n = Arg
+
+-- | Inhabitant of the argument proxy.
+arg :: Arg n
+arg = Arg
+
diff --git a/src/Data/Refined.hs b/src/Data/Refined.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Refined.hs
@@ -0,0 +1,177 @@
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE UndecidableInstances  #-}
+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE KindSignatures        #-}
+{-# LANGUAGE FlexibleContexts      #-}
+
+{-|
+  Module      :  Data.Refined
+  Copyright   :  (c) Matt Noonan 2018
+  License     :  BSD-style
+  Maintainer  :  matt.noonan@gmail.com
+  Portability :  portable
+-}
+
+module Data.Refined
+  (  -- * Refinement types
+    -- ** Attaching arbitrary propositions to values
+    (:::)
+  , (...)
+  , (...>)
+  , ($:)
+  , exorcise
+  , conjure
+
+  -- ** Refinement types
+  , Satisfies
+  , type (?)
+  , assert
+
+  -- *** Forgetting and re-introducing names
+  , unname
+  , rename
+  , (...?)
+
+  -- *** Traversals over collections of refined types
+  , traverseP, traverseP_
+  , forP, forP_
+  ) where
+
+import Data.The
+import Logic.Proof (Proof, axiom)
+import Theory.Named
+
+import Data.Coerce
+import Data.Foldable (traverse_)
+
+{--------------------------------------------------
+  Attaching proofs to values
+--------------------------------------------------}
+
+{-| Given a type @a@ and a proposition @p@, the
+    type @(a ::: p)@ represents a value of type @a@,
+    with an attached "ghost proof" of @p@.
+
+    Values of the type @(a ::: p)@ have
+    the same run-time representation as values of
+    the normal type @a@; the proposition @p@ does
+    not carry a run-time space or time cost.
+-}
+newtype a ::: p = SuchThat a
+infixr 1 :::
+
+instance The a' a => The (a' ::: p) a where
+  the (SuchThat x) = the x
+
+-- | Given a value and a proof, attach the proof as a
+--   ghost proof on the value.
+(...) :: a -> Proof p -> (a ::: p)
+x ...proof = coerce x
+
+-- | Given a value and a proof, apply a function to the value
+--   but leave the proof unchanged.
+($:) :: (a -> b) -> (a ::: p) -> (b ::: p)
+f $: x = coerce (f (exorcise x))
+
+-- | Apply an implication to the ghost proof attached to a value,
+--   leaving the value unchanged.
+(...>) :: (a ::: p) -> (p -> Proof q) -> (a ::: q)
+x ...> _ = coerce x
+
+-- | Forget the ghost proof attached to a value.
+exorcise :: (a ::: p) -> a
+exorcise = coerce
+
+-- | Extract the ghost proof from a value.
+conjure :: (a ::: p) -> Proof p
+conjure _ = axiom
+
+{--------------------------------------------------
+  Refinement types
+--------------------------------------------------}
+
+{-| Given a type @a@ and a predicate @p@, the type
+    @a ?p@ represents a /refinement type/ for @a@.
+    Values of type @a ?p@ should be values of type @a@
+    that satisfy the predicate @p@.
+
+    Values of type @a ?p@ have the same run-time representation
+    as values of type @a@; the proposition @p@ does not carry a
+    run-time space or time cost.
+-}
+newtype Satisfies (p :: * -> *) a = Satisfies a
+instance The (Satisfies p a) a
+
+-- | An infix alias for 'Satisfies'.
+type a ?p = Satisfies p a
+infixr 1 ?
+
+-- | For library authors: assert that a property holds.
+assert :: Defining (p n) => a -> (a ?p)
+assert x = name x (\x -> unname (x ...axiom))
+
+-- | Existential introduction for names: given a named value of
+--   type @a@ that satisfies a predicate @p@, coerce to a value
+--   of type @a ?p@.
+unname :: (a ~~ name ::: p name) -> (a ?p)
+unname = coerce . the
+
+-- | Existential elimination for names: given a value of type
+--   @a ?p@, re-introduce a new name to produce a value of type
+--   @a ~~ name ::: p name@.
+rename :: (a ?p) -> (forall name. (a ~~ name ::: p name) -> t) -> t
+rename x k = name (the x) (\x -> k (x ...axiom))
+
+{-| Take a simple function with one named argument and a named return,
+    plus an implication relating a precondition to a postcondition of the
+    function, and produce a function between refined input and output types.
+
+@
+newtype NonEmpty xs = NonEmpty Defn
+newtype Reverse  xs = Reverse  Defn
+
+rev :: ([a] ~~ xs) -> ([a] ~~ Reverse xs)
+rev xs = defn (reverse (the xs))
+
+rev_nonempty_lemma :: NonEmpty xs -> Proof (NonEmpty (Reverse xs))
+
+rev' :: ([a] ?NonEmpty) -> ([a] ?NonEmpty)
+rev' = rev ...? rev_nonempty_lemma
+@
+-}
+
+(...?) :: (forall name. (a ~~ name) -> (b ~~ f name))
+      -> (forall name. p name -> Proof (q (f name)))
+      -> (a ?p) -> (b ?q)
+(...?) f _ x = rename x (\x -> unname (f (exorcise x) ...axiom))
+
+-- | Traverse a collection of refined values, re-introducing names
+--   in the body of the action.
+traverseP :: (Traversable t, Applicative f)
+          => (forall name. (a ~~ name ::: p name) -> f b)
+          -> t (a ?p)
+          -> f (t b)
+traverseP f = traverse (\x -> rename x f)
+
+-- | Same as 'traverseP', but ignores the action's return value.
+traverseP_ :: (Foldable t, Applicative f)
+          => (forall name. (a ~~ name ::: p name) -> f b)
+          -> t (a ?p)
+          -> f ()
+traverseP_ f = traverse_ (\x -> rename x f)
+
+-- | Same as 'traverse', with the argument order flipped.
+forP :: (Traversable t, Applicative f)
+      => t (a ?p)
+      -> (forall name. (a ~~ name ::: p name) -> f b)
+      -> f (t b)
+forP x f = traverseP f x
+
+-- | Same as 'traverse_', with the argument order flipped.
+forP_ :: (Foldable t, Applicative f)
+      => t (a ?p)
+      -> (forall name. (a ~~ name ::: p name) -> f b)
+      -> f ()
+forP_ x f = traverseP_ f x
diff --git a/src/Data/The.hs b/src/Data/The.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/The.hs
@@ -0,0 +1,54 @@
+{-# LANGUAGE DefaultSignatures      #-}
+{-# LANGUAGE MultiParamTypeClasses  #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE PatternSynonyms        #-}
+{-# LANGUAGE ViewPatterns           #-}
+
+{-|
+  Module      :  Data.The
+  Copyright   :  (c) Matt Noonan 2018
+  License     :  BSD-style
+  Maintainer  :  matt.noonan@gmail.com
+  Portability :  portable
+-}
+
+module Data.The
+  ( The(..)
+  , pattern The
+  ) where
+
+import Data.Coerce
+
+{-| A class for extracing "the" underlying value.
+    'the' should ideally be a coercion from some
+    @newtype@ wrap of @a@ back to @a@.
+ 
+    For this common use case, in the module where
+    @newtype New a = New a@ is defined, an instance
+    of @The@ can be created with an empty definition:
+
+@
+newtype New a = New a
+instance The (New a) a
+@
+-}
+class The d a | d -> a where
+  the :: d -> a
+  default the :: Coercible d a => d -> a
+  the = coerce
+
+{-| A view pattern for discarding the wrapper around
+    a value.
+
+@
+f (The x) = expression x
+@
+
+    is equivalent to
+
+@
+f x = let x' = the x in expression x'
+@
+-}
+pattern The :: The d a => a -> d
+pattern The x <- (the -> x)
diff --git a/src/GDP.hs b/src/GDP.hs
new file mode 100644
--- /dev/null
+++ b/src/GDP.hs
@@ -0,0 +1,29 @@
+{-|
+  Module      :  GDP
+  Copyright   :  (c) Matt Noonan 2018
+  License     :  BSD-style
+  Maintainer  :  matt.noonan@gmail.com
+  Portability :  portable
+-}
+
+module GDP
+  ( module Data.Arguments
+  , module Data.Refined
+  , module Data.The
+  , module Logic.Classes
+  , module Logic.NegClasses
+  , module Logic.Proof
+  , module Logic.Propositional
+  , module Theory.Equality
+  , module Theory.Named
+  ) where
+
+import Data.Arguments
+import Data.Refined
+import Data.The
+import Logic.Classes
+import Logic.NegClasses
+import Logic.Proof
+import Logic.Propositional
+import Theory.Equality
+import Theory.Named
diff --git a/src/Logic/Classes.hs b/src/Logic/Classes.hs
new file mode 100644
--- /dev/null
+++ b/src/Logic/Classes.hs
@@ -0,0 +1,229 @@
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE DefaultSignatures     #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleContexts      #-}
+
+{-|
+  Module      :  Logic.Classes
+  Copyright   :  (c) Matt Noonan 2018
+  License     :  BSD-style
+  Maintainer  :  matt.noonan@gmail.com
+  Portability :  portable
+-}
+
+module Logic.Classes
+  ( -- * Algebraic properties
+    Reflexive(..)
+  , Symmetric(..)
+  , Transitive(..)
+  , transitive'
+
+  , Idempotent(..)
+  , Commutative(..)
+  , Associative(..)
+  , DistributiveL(..)
+  , DistributiveR(..)
+
+  , Injective(..)
+
+  ) where
+
+import Logic.Proof
+import Theory.Equality
+import Theory.Named
+
+{--------------------------------------------------------
+  Special properties of predicates and functions
+--------------------------------------------------------}
+
+{-| A binary relation R is /reflexive/ if, for all x,
+    R(x, x) is true. The @Reflexive r@ typeclass provides
+    a single method, @refl :: Proof (r x x)@,
+    proving R(x, x) for an arbitrary x.
+
+    Within the module where the relation @R@ is defined, you can
+    declare @R@ to be reflexive with an empty instance:
+
+@
+-- Define a reflexive binary relation
+newtype SameColor p q = SameColor Defn
+instance Reflexive SameColor
+@
+-}   
+class Reflexive r where
+  refl :: Proof (r x x)
+  default refl :: (Defining (r x x)) => Proof (r x x)
+  refl = axiom
+
+{-| A binary relation R is /symmetric/ if, for all x and y,
+    R(x, y) is true if and only if R(y, x) is true. The
+    @Symmetric@ typeclass provides
+    a single method, @symmetric :: r x y -> Proof (r y x)@,
+    proving the implication "R(x, y) implies R(y, x)".
+
+    Within the module where @R@ is defined, you can
+    declare @R@ to be symmetric with an empty instance:
+
+@
+-- Define a symmetric binary relation
+newtype NextTo p q = NextTo Defn
+instance Symmetric NextTo
+@
+-}   
+class Symmetric c where
+  symmetric :: c p q -> Proof (c q p)
+  default symmetric :: (Defining (c p q)) => c p q -> Proof (c q p)
+  symmetric _ = axiom
+
+{-| A binary relation R is /transitive/ if, for all x, y, z,
+    if R(x, y) is true and R(y, z) is true, then  R(x, z) is true.
+    The @Transitive r@ typeclass provides
+    a single method, @transitive :: r x y -> r y z -> Proof (r x z)@,
+    proving R(x, z) from R(x, y) and R(y, z).
+
+    Within the module where @R@ is defined, you can
+    declare @R@ to be transitive with an empty instance:
+
+@
+-- Define a transitive binary relation
+newtype CanReach p q = CanReach Defn
+instance Transitive CanReach
+@
+-}   
+class Transitive c where
+  transitive :: c p q -> c q r -> Proof (c p r)
+  default transitive :: Defining (c p q) => c p q -> c q r -> Proof (c p r)
+  transitive _ _ = axiom
+
+-- | @transitive@, with the arguments flipped.
+transitive' :: Transitive c => c q r -> c p q -> Proof (c p r)
+transitive' = flip transitive
+
+{-| A binary operation @#@ is idempotent if @x # x == x@ for all @x@.
+    The @Idempotent c@ typeclass provides a single method,
+    @idempotent :: Proof (c p p == p)@.
+
+    Within the module where @F@ is defined, you can declare @F@ to be
+    idempotent with an empty instance:
+
+@
+-- Define an idempotent binary operation
+newtype Union x y = Union Defn
+instance Idempotent Union
+@
+-}
+class Idempotent c where
+  idempotent :: Proof (c p p == p)
+  default idempotent :: Defining (c p p) => Proof (c p p == p)
+  idempotent = axiom
+  
+{-| A binary operation @#@ is commutative if @x # y == y # x@ for all @x@ and @y@.
+    The @Commutative c@ typeclass provides a single method,
+    @commutative :: Proof (c x y == c y x)@.
+
+    Within the module where @F@ is defined, you can declare @F@ to be
+    commutative with an empty instance:
+
+@
+-- Define a commutative binary operation
+newtype Union x y = Union Defn
+instance Commutative Union
+@
+-}
+class Commutative c where
+  commutative :: Proof (c p q == c q p)
+  default commutative :: Defining (c p q) => Proof (c p q == c q p)
+  commutative = axiom
+
+{-| A binary operation @#@ is associative if @x # (y # z) == (x # y) # z@ for
+    all @x@, @y@, and @z@.
+    The @Associative c@ typeclass provides a single method,
+    @associative :: Proof (c x (c y z) == c (c x y) z)@.
+
+    Within the module where @F@ is defined, you can declare @F@ to be
+    associative with an empty instance:
+
+@
+-- Define an associative binary operation
+newtype Union x y = Union Defn
+instance Associative Union
+@
+-}
+class Associative c where
+  associative :: Proof (c p (c q r) == c (c p q) r)
+  default associative :: Defining (c p q) => Proof (c p (c q r) == c (c p q) r)
+  associative = axiom
+
+{-| A binary operation @#@ distributes over @%@ on the left if
+    @x # (y % z) == (x # y) % (x # z)@ for
+    all @x@, @y@, and @z@.
+    The @DistributiveL c c'@ typeclass provides a single method,
+    @distributiveL :: Proof (c x (c' y z) == c' (c x y) (c x z))@.
+
+    Within the module where @F@ and @G@ are defined, you can declare @F@ to
+    distribute over @G@ on the left with an empty instance:
+
+@
+-- x `Union` (y `Intersect` z) == (x `Union` y) `Intersect` (x `Union` z)
+newtype Union     x y = Union     Defn
+newtype Intersect x y = Intersect Defn
+instance DistributiveL Union Intersect
+@
+-}
+class DistributiveL c c' where
+  distributiveL :: Proof (c p (c' q r) == c' (c p q) (c p r))
+  default distributiveL :: (Defining (c p q), Defining (c' p q)) => Proof (c p (c' q r) == c' (c p q) (c p r))
+  distributiveL = axiom
+
+{-| A binary operation @#@ distributes over @%@ on the right if
+    @(x % y) # z == (x # z) % (y # z)@ for
+    all @x@, @y@, and @z@.
+    The @DistributiveR c c'@ typeclass provides a single method,
+    @distributiveR :: Proof (c (c' x y) z == c' (c x z) (c y z))@.
+
+    Within the module where @F@ and @G@ are defined, you can declare @F@ to
+    distribute over @G@ on the left with an empty instance:
+
+@
+-- (x `Intersect` y) `Union` z == (x `Union` z) `Intersect` (y `Union` z)
+newtype Union     x y = Union     Defn
+newtype Intersect x y = Intersect Defn
+instance DistributiveR Union Intersect
+@
+-}
+class DistributiveR c c' where
+  distributiveR :: Proof (c (c' p q) r == c' (c p r) (c q r))
+  default distributiveR :: (Defining (c p q), Defining (c' p q)) => Proof (c (c' p q) r == c' (c p r) (c q r))
+  distributiveR = axiom
+
+{-| A function @f@ is /injective/ if @f x == f y@ implies @x == y@.
+    The @Injective f@ typeclass provides a single method,
+    @elim_inj :: (f x == f y) -> Proof (x == y)@.
+
+    Within the module where @F@ is defined, you can declare @F@ to be
+    injective with an empty instance:
+
+@
+-- {x} == {y} implies x == y.
+newtype Singleton x = Singleton Defn
+instance Injective Singleton
+@
+-}
+class Injective f where
+  elim_inj :: (f x == f y) -> Proof (x == y)
+  default elim_inj :: (Defining (f x), Defining (f y)) => (f x == f y) -> Proof (x == y)
+  elim_inj _ = axiom
+
+
+{--------------------------------------------------------
+  Properites of equality
+--------------------------------------------------------}
+
+instance Reflexive Equals where
+  refl = axiom
+
+instance Symmetric Equals where
+  symmetric _ = axiom
+
+instance Transitive Equals where
+  transitive _ _ = axiom
diff --git a/src/Logic/NegClasses.hs b/src/Logic/NegClasses.hs
new file mode 100644
--- /dev/null
+++ b/src/Logic/NegClasses.hs
@@ -0,0 +1,67 @@
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE DefaultSignatures     #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleContexts      #-}
+
+{-|
+  Module      :  Logic.NegClasses
+  Copyright   :  (c) Matt Noonan 2018
+  License     :  BSD-style
+  Maintainer  :  matt.noonan@gmail.com
+  Portability :  portable
+-}
+
+module Logic.NegClasses
+  ( -- * Algebraic properties
+    Irreflexive(..)
+  , Antisymmetric(..)
+  ) where
+
+import Logic.Proof
+import Logic.Propositional (Not)
+import Theory.Equality
+import Theory.Named
+
+{--------------------------------------------------------
+  Special properties of predicates and functions
+--------------------------------------------------------}
+
+{-| A binary relation R is /irreflexive/ if, for all x,
+    R(x, x) is false. The @Irreflexive r@ typeclass provides
+    a single method, @irrefl :: Proof (Not (r x x))@,
+    proving the negation of R(x, x) for an arbitrary x.
+
+    Within the module where the relation @R@ is defined, you can
+    declare @R@ to be irreflexive with an empty instance:
+
+@
+-- Define an irreflexive binary relation
+newtype DifferentColor p q = DifferentColor Defn
+instance Irreflexive DifferentColor
+@
+-}
+class Irreflexive r where
+  irrefl :: Proof (Not (r x x))
+  default irrefl :: (Defining (r x x)) => Proof (Not (r x x))
+  irrefl = axiom
+
+
+{-| A binary relation R is /antisymmetric/ if, for all x and y,
+    when R(x, y) is true, then R(y, x) is false. The
+    @Antisymmetric@ typeclass provides
+    a single method, @antisymmetric :: r x y -> Proof (Not (r y x))@,
+    proving the implication "R(x, y) implies the negation of R(y, x)".
+
+    Within the module where @R@ is defined, you can
+    declare @R@ to be antisymmetric with an empty instance:
+
+@
+-- Define an antisymmetric binary relation
+newtype AncestorOf p q = AncestorOf Defn
+instance Antisymmetric AncestorOf
+@
+-}   
+class Antisymmetric c where
+  antisymmetric :: c p q -> Proof (Not (c q p))
+  default antisymmetric :: Defining (c p q) => c p q -> Proof (Not (c q p))
+  antisymmetric _ = axiom
diff --git a/src/Logic/Proof.hs b/src/Logic/Proof.hs
new file mode 100644
--- /dev/null
+++ b/src/Logic/Proof.hs
@@ -0,0 +1,203 @@
+{-# LANGUAGE KindSignatures #-}
+
+{-|
+  Module      :  Logic.Proof
+  Copyright   :  (c) Matt Noonan 2018
+  License     :  BSD-style
+  Maintainer  :  matt.noonan@gmail.com
+  Portability :  portable
+-}
+
+module Logic.Proof
+  ( -- * The `Proof` monad
+    Proof
+  , (|.), (|$), (|/), (|\), ($$)
+  , given
+  , axiom, sorry
+  ) where
+
+import Data.Coerce
+import Control.Monad ((>=>))
+
+{--------------------------------------------------
+  The `Proof` monad
+--------------------------------------------------}
+
+{-| The @Proof@ monad is used as a domain-specific
+    language for constructing proofs. A value of type
+    @Proof p@ represents a proof of the proposition @p@.
+
+    For example, this function constructions a proof of
+    "P or Q" from the assumption "P and Q":
+
+> and2or :: (p && q) -> Proof (p || q)
+>
+> and2or pq = do
+>    p <- and_elimL pq    -- or: "p <- fst <$> and_elim pq"
+>    or_introL p
+
+    If the body of the proof does not match the proposition
+    you claim to be proving, the compiler will raise a type
+    error. Here, we accidentally try to use @or_introR@
+    instead of @or_introL@:
+
+> and2or :: (p && q) -> Proof (p || q)
+>
+> and2or pq = do
+>    p <- and_elimL pq
+>    or_introR p
+
+resulting in the error
+
+@
+    • Couldn't match type ‘p’ with ‘q’
+      ‘p’ is a rigid type variable bound by
+        the type signature for:
+          and2or :: forall p q. (p && q) -> Proof (p || q)
+
+      ‘q’ is a rigid type variable bound by
+        the type signature for:
+          and2or :: forall p q. (p && q) -> Proof (p || q)
+
+      Expected type: Proof (p || q)
+        Actual type: Proof (p || p)
+@
+-}
+data Proof (pf :: *) = QED
+
+instance Functor Proof where
+  fmap _ = const QED -- modus ponens (external?)
+
+instance Applicative Proof where
+  pure = const QED -- axiom
+  pf1 <*> pf2 = QED -- modus ponens (internal?)
+
+instance Monad Proof where
+  pf >>= f = QED
+
+{-| This operator is just a specialization of @(>>=)@, but
+    can be used to create nicely delineated chains of
+    derivations within a larger proof. The first statement
+    in the chain should produce a formula; @(|$)@ then
+    pipes this formula into the following derivation rule.
+
+> and2or :: (p && q) -> Proof (p || q)
+>
+> and2or pq =  and_elimL pq
+>           |$ or_introL
+-}
+
+(|$) :: Proof p -> (p -> Proof q) -> Proof q
+(|$) = (>>=)
+
+infixr 7 |$
+
+--(|-) :: ((p -> Proof r) -> Proof r) -> (p -> Proof r) -> Proof r
+
+{-| This operator is used to create nicely delineated chains of
+    derivations within a larger proof. If X and Y are two
+    deduction rules, each with a single premise and a single
+    conclusion, and the premise of Y matches the conclusion of X,
+    then @X |. Y@ represents the composition of the two
+    deduction rules.
+
+> and2or :: (p && q) -> Proof (p || q)
+>
+> and2or =  and_elimL
+>        |. or_introL
+-}
+
+(|.) :: (p -> Proof q) -> (q -> Proof r) -> p -> Proof r
+(|.) = (>=>)
+
+infixr 9 |.
+
+{-| The @(|/)@ operator is used to feed the remainder of the proof in
+    as a premise of the first argument.
+
+    A common use-case is with the @Or@-elimination rules @or_elimL@ and
+    @or_elimR@, when one case is trivial. For example, suppose we wanted
+    to prove that @R && (P or (Q and (Q implies P)))@ implies @P@:
+
+@
+my_proof :: r && (p || (q && (q --> p))) -> Proof p
+
+my_proof =
+  do  and_elimR          -- Forget the irrelevant r.
+   |. or_elimL given     -- The first case of the || is immediate;
+   |/ and_elim           -- The rest of the proof handles the second case,
+   |. uncurry impl_elim  --   by unpacking the && and feeding the q into
+                         --   the implication (q --> p).
+@
+
+    The rising @/@ is meant to suggest the bottom half of the proof getting
+    plugged in to the Or-elimination line.
+-}
+(|/) :: (p -> (q -> Proof r) -> Proof r) -> (q -> Proof r) -> p -> Proof r
+(|/) = flip
+infixr 9 |/
+
+{-| The @(|\\)@ operator is used to take the subproof so far and feed it
+    into a rule that is expecting a subproof as a premise.
+
+    A common use-case is with the @Not@-introduction rule @not_intro@,
+    which has a type that fits the second argument of @(|\\)@. By way
+    of example, here is a proof that "P implies Q" along with "Not Q"
+    implies "Not P".
+
+@
+my_proof :: (p --> q) -> (Not p --> r) -> Not q -> Proof r
+
+my_proof impl1 impl2 q' =
+  do  modus_ponens impl1   -- This line, composed with the next,
+   |. contradicts' q'      --   form a proof of FALSE from p.
+   |\\ not_intro            -- Closing the subproof above, conclude not-p.
+   |. modus_ponens impl2   -- Now apply the second implication to conclude r.
+@
+
+    The falling @\\@ is meant to suggest the upper half of the proof
+    being closed off by the Not-introduction line.
+-}
+(|\) :: (p -> Proof q) -> ((p -> Proof q) -> Proof r) -> Proof r
+(|\) = flip ($)
+infixl 8 |\
+
+-- | Take a proof of @p@ and feed it in as the first premise of
+--   an argument that expects a @p@ and a @q@.
+($$) :: (p -> q -> Proof r) -> Proof p -> (q -> Proof r)
+(f $$ pp) q = do { p <- pp; f p q }
+
+-- | @given@ creates a proof of P, given P as
+--   an assumption.
+--
+--   @given@ is just a specialization of @pure@ / @return@.
+given :: p -> Proof p
+given _ = QED
+
+-- | @sorry@ can be used to provide a "proof" of
+--   any proposition, by simply assering it as
+--   true. This is useful for stubbing out portions
+--   of a proof as you work on it, but subverts
+--   the entire proof system.
+--
+-- _Completed proofs should never use @sorry@!_
+sorry :: Proof p
+sorry = QED
+
+{-| @axiom@, like @sorry@, provides a "proof" of any
+    proposition. Unlike @sorry@, which is used to indicate
+    that a proof is still in progress, @axiom@ is meant to
+    be used by library authors to assert axioms about how
+    their library works. For example:
+
+@
+data Reverse xs = Reverse Defn
+data Length  xs = Length  Defn
+
+rev_length_lemma :: Proof (Length (Reverse xs) == Length xs)
+rev_length_lemma = axiom
+@
+-}
+axiom :: Proof p
+axiom = QED
+
diff --git a/src/Logic/Propositional.hs b/src/Logic/Propositional.hs
new file mode 100644
--- /dev/null
+++ b/src/Logic/Propositional.hs
@@ -0,0 +1,478 @@
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE KindSignatures        #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE DefaultSignatures     #-}
+{-# LANGUAGE ConstraintKinds       #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
+{-# LANGUAGE TypeFamilies #-}
+
+{-|
+  Module      :  Logic.Propositional
+  Copyright   :  (c) Matt Noonan 2018
+  License     :  BSD-style
+  Maintainer  :  matt.noonan@gmail.com
+  Portability :  portable
+-}
+
+module Logic.Propositional
+  ( -- * First-order Logic
+
+  -- ** Logical symbols
+    TRUE, FALSE
+  
+  , And,     type (&&), type (∧), type (/\)
+  , Or,      type (||), type (∨), type (\/)
+  , Implies, type (-->)
+  , Not
+  , ForAll
+  , Exists
+
+  -- ** Natural deduction
+
+  -- *** Tautologies
+  , true
+  , noncontra
+
+  -- *** Introduction rules
+
+  -- | Introduction rules give the elementary building blocks
+  --   for creating a formula from simpler ones.
+  , and_intro
+  , or_introL
+  , or_introR
+  , impl_intro
+  , not_intro
+  , contrapositive
+  , contradicts
+  , contradicts'
+  , univ_intro
+  , ex_intro
+
+  -- *** Elimination rules
+
+  -- | Elimination rules give the elementary building blocks for
+  --   decomposing a complex formula into simpler ones.
+  , and_elimL
+  , and_elimR
+  , and_elim
+  , or_elim
+  , or_elimL
+  , or_elimR
+  , impl_elim
+  , modus_ponens
+  , modus_tollens
+  , absurd
+  , univ_elim
+  , ex_elim
+
+  -- *** Classical logic and the Law of the Excluded Middle
+  , Classical
+  , classically
+  , lem
+  , contradiction
+  , not_not_elim
+
+   -- *** Mapping over conjunctions and disjunctions
+  , and_mapL
+  , and_mapR
+  , and_map
+
+  , or_mapL
+  , or_mapR
+  , or_map
+
+  , impl_mapL
+  , impl_mapR
+  , impl_map
+
+  , not_map
+
+  ) where
+
+import Data.Arguments
+import Data.Refined
+import Data.The
+import Logic.Classes
+import Logic.Proof
+import Theory.Named
+
+{--------------------------------------------------
+  Logical constants
+--------------------------------------------------}
+
+-- | The constant "true".
+newtype TRUE  = TRUE Defn
+
+-- | The constant "false".
+newtype FALSE = FALSE Defn
+
+-- | The conjunction of @p@ and @q@.
+newtype And p q = And Defn
+
+-- | The disjunction of @p@ and @q@.
+newtype Or p q  = Or  Defn
+
+-- | The negation of @p@.
+newtype Not p   = Not Defn
+
+-- | The implication "@p@ implies @q@".
+newtype Implies p q = Implies Defn
+
+-- | Existential quantifiation.
+newtype Exists x p = Exists Defn
+
+-- | Universal quantification.
+newtype ForAll x p = ForAll Defn
+
+-- | An infix alias for @Or@.
+type p || q   = p `Or` q
+
+-- | An infix alias for @Or@.
+type p ∨ q   = p `Or` q
+
+-- | An infix alias for @Or@.
+type p \/ q  = p `Or` q
+
+-- | An infix alias for @And@.
+type p && q  = p `And` q
+
+-- | An infix alias for @And@.
+type p ∧ q   = p `And` q
+
+-- | An infix alias for @And@.
+type p /\ q  = p `And` q
+
+-- | An infix alias for @Implies@.
+type p --> q = p `Implies` q
+
+infixl 2 `Or`
+infixl 2 ||
+infixl 2 ∨
+infixl 2 \/
+
+infixl 3 `And`
+infixl 3 &&
+infixl 3 ∧
+infixl 3 /\
+
+infixr 1 `Implies`
+infixr 1 -->
+
+{--------------------------------------------------
+  Mapping over conjunctions and disjunctions
+--------------------------------------------------}
+
+-- | Apply a derivation to the left side of a conjunction.
+and_mapL :: (p -> Proof p') -> (p && q) -> Proof (p' && q)
+and_mapL impl conj = do
+  (lhs, rhs) <- and_elim conj
+  lhs' <- impl lhs
+  and_intro lhs' rhs
+
+-- | Apply a derivation to the right side of a conjunction.
+and_mapR :: (q -> Proof q') -> (p && q) -> Proof (p && q')
+and_mapR impl conj = do
+  (lhs, rhs) <- and_elim conj
+  rhs' <- impl rhs
+  and_intro lhs rhs'
+
+-- | Apply derivations to the left and right sides of a conjunction.
+and_map :: (p -> Proof p') -> (q -> Proof q') -> (p && q) -> Proof (p' && q')
+and_map implP implQ conj = do
+  (lhs, rhs) <- and_elim conj
+  lhs' <- implP lhs
+  rhs' <- implQ rhs
+  and_intro lhs' rhs'
+
+-- | Apply a derivation to the left side of a disjunction.
+or_mapL :: (p -> Proof p') -> (p || q) -> Proof (p' || q)
+or_mapL impl = or_elim (impl |. or_introL) or_introR
+
+-- | Apply a derivation to the right side of a disjunction.
+or_mapR :: (q -> Proof q') -> (p || q) -> Proof (p || q')
+or_mapR impl = or_elim or_introL (impl |. or_introR)
+
+-- | Apply derivations to the left and right sides of a disjunction.
+or_map :: (p -> Proof p') -> (q -> Proof q') -> (p || q) -> Proof (p' || q')
+or_map implP implQ = or_elim (implP |. or_introL) (implQ |. or_introR)
+
+-- | Apply a derivation to the left side of an implication.
+impl_mapL :: (p' -> Proof p) -> (p --> q) -> Proof (p' --> q)
+impl_mapL derv impl = impl_intro (derv |. modus_ponens impl)
+
+-- | Apply a derivation to the right side of an implication.
+impl_mapR :: (q -> Proof q') -> (p --> q) -> Proof (p --> q')
+impl_mapR derv impl = impl_intro (modus_ponens impl |. derv)
+
+-- | Apply derivations to the left and right sides of an implication.
+impl_map :: (p' -> Proof p) -> (q -> Proof q') -> (p --> q) -> Proof (p' --> q')
+impl_map dervL dervR impl = impl_intro (dervL |. modus_ponens impl |. dervR)
+
+-- | Apply a derivation inside of a negation.
+not_map :: (p' -> Proof p) -> Not p -> Proof (Not p')
+not_map impl notP = not_intro (impl |. contradicts' notP |. absurd)
+
+{--------------------------------------------------
+  Tautologies
+--------------------------------------------------}
+
+-- | @TRUE@ is always true, and can be introduced into a proof at any time.
+true :: Proof TRUE
+true = axiom
+
+-- | The Law of Noncontradiction: for any proposition P, "P and not-P" is false.
+noncontra :: Proof (Not (p && Not p))
+noncontra = axiom
+
+{--------------------------------------------------
+  Introduction rules
+--------------------------------------------------}
+
+-- | Prove "P and Q" from P and Q.
+and_intro :: p -> q -> Proof (p && q)
+and_intro _ _ = axiom
+
+-- | Prove "P and Q" from Q and P.
+and_intro' :: q -> p -> Proof (p && q)
+and_intro' _ _ = axiom
+
+-- | Prove "P or Q" from  P.
+or_introL :: p -> Proof (p || q)
+or_introL _ = axiom
+
+-- | Prove "P or Q" from Q.
+or_introR :: q -> Proof (p || q)
+or_introR _ = axiom
+
+-- | Prove "P implies Q" by demonstrating that,
+--   from the assumption P, you can prove Q.
+impl_intro :: (p -> Proof q) -> Proof (p --> q)
+impl_intro _ = axiom
+
+-- | Prove "not P" by demonstrating that,
+--   from the assumption P, you can derive a false conclusion.
+not_intro :: (p -> Proof FALSE) -> Proof (Not p)
+not_intro _ = axiom
+
+-- | `contrapositive` is an alias for `not_intro`, with
+--   a somewhat more suggestive name. Not-introduction
+--   corresponds to the proof technique "proof by contrapositive".
+contrapositive :: (p -> Proof FALSE) -> Proof (Not p)
+contrapositive = not_intro
+
+-- | Prove a contradiction from "P" and "not P".
+contradicts :: p -> Not p -> Proof FALSE
+contradicts _ _ = axiom
+
+-- | `contradicts'` is `contradicts` with the arguments
+--   flipped. It is useful when you want to partially
+--   apply `contradicts` to a negation.
+contradicts' :: Not p -> p -> Proof FALSE
+contradicts' = flip contradicts
+
+-- | Prove "For all x, P(x)" from a proof of P(*c*) with
+--   *c* indeterminate.
+univ_intro :: (forall c. Proof (p c)) -> Proof (ForAll x (p x))
+univ_intro _ = axiom
+
+-- | Prove "There exists an x such that P(x)" from a specific
+--   instance of P(c).
+ex_intro :: p c -> Proof (Exists x (p x))
+ex_intro _ = axiom
+
+{--------------------------------------------------
+  Elimination rules
+--------------------------------------------------}
+
+-- | From the assumption "P and Q", produce a proof of P.
+and_elimL :: p && q -> Proof p
+and_elimL _ = axiom
+
+-- | From the assumption "P and Q", produce a proof of Q.
+and_elimR :: p && q -> Proof q
+and_elimR _ = axiom
+
+-- | From the assumption "P and Q", produce both a proof
+--   of P, and a proof of Q.
+and_elim :: p && q -> Proof (p, q)
+and_elim c = (,) <$> and_elimL c <*> and_elimR c
+  
+{-| If you have a proof of R from P, and a proof of
+     R from Q, then convert "P or Q" into a proof of R.
+-}
+or_elim :: (p -> Proof r) -> (q -> Proof r) -> (p || q) -> Proof r
+or_elim _ _ _ = axiom
+
+{-| Eliminate the first alternative in a conjunction.
+-}
+or_elimL :: (p -> Proof r) -> (p || q) -> (q -> Proof r) -> Proof r
+or_elimL case1 disj case2 = or_elim case1 case2 disj
+
+{-| Eliminate the second alternative in a conjunction.
+-}
+or_elimR :: (q -> Proof r) -> (p || q) -> (p -> Proof r) -> Proof r
+or_elimR case2 disj case1 = or_elim case1 case2 disj
+
+-- | Given "P imples Q" and P, produce a proof of Q.
+--   (modus ponens)
+impl_elim :: p -> (p --> q) -> Proof q
+impl_elim _ _ = axiom
+
+-- | @modus_ponens@ is just @impl_elim@ with the arguments
+--   flipped. In this form, it is useful for partially
+--   applying an implication.
+modus_ponens :: (p --> q) -> p -> Proof q
+modus_ponens = flip impl_elim
+
+{-| Modus tollens lets you prove "Not P" from
+    "P implies Q" and "Not Q".
+
+    Modus tollens is not fundamental, and can be derived from
+    other rules:
+
+@
+                                  -----         (assumption)
+                        p --> q,    p
+                       ---------------------    (modus ponens)
+                 q,           Not q    
+              --------------------------        (contradicts')
+                      FALSE
+          ------------------------------------- (not-intro)
+                             Not p
+@
+
+We can encode this proof tree more-or-less directly as a @Proof@
+to implement @modus_tollens@:
+
+@
+modus_tollens :: (p --> q) -> Not q -> Proof (Not p)
+
+modus_tollens impl q' =
+  do  modus_ponens impl
+   |. contradicts' q'
+   |\\ not_intro
+@
+-}
+
+modus_tollens :: (p --> q) -> Not q -> Proof (Not p)
+modus_tollens impl q' =
+  do  modus_ponens impl
+   |. contradicts' q'
+   |\ not_intro
+
+-- | From a falsity, prove anything.
+absurd :: FALSE -> Proof p
+absurd _ = axiom
+
+-- | Given "For all x, P(x)" and any c, prove the proposition
+--   "P(c)".
+univ_elim :: ForAll x (p x) -> Proof (p c)
+univ_elim _ = axiom
+
+-- | Given a proof of Q from P(c) with c generic, and the
+--   statement "There exists an x such that P(x)", produce
+--   a proof of Q.
+ex_elim :: (forall c. p c -> Proof q) -> Exists x (p x) -> Proof q
+ex_elim _ _ = axiom
+
+
+{--------------------------------------------------
+  Classical logic
+--------------------------------------------------}
+
+-- | The inference rules so far have all been valid in
+--   constructive logic. Proofs in classical logic are
+--   also allowed, but will be constrained by the
+--   `Classical` typeclass.
+class Classical
+
+-- | Discharge a @Classical@ constraint, by saying
+--   "I am going to allow a classical argument here."
+--
+--   NOTE: The existence of this function means that a proof
+--   should only be considered constructive if it
+--   does not have a @Classical@ constraint, *and*
+--   it does not invoke @classically@.
+classically :: (Classical => Proof p) -> Proof p
+classically _ = axiom
+
+-- | The Law of the Excluded Middle: for any proposition
+--   P, assert that either P is true, or Not P is true.
+lem :: Classical => Proof (p || Not p)
+lem = axiom
+
+{-| Proof by contradiction: this proof technique allows
+     you to prove P by showing that, from "Not P", you
+     can prove a falsehood.
+  
+     Proof by contradiction is not a theorem of
+     constructive logic, so it requires the @Classical@
+     constraint. But note that the similar technique
+     of proof by contrapositive (not-introduction) /is/
+     valid in constructive logic! For comparison, the two types are:
+
+@
+contradiction  :: Classical => (Not p -> Proof FALSE) -> p
+not_intro      ::              (p     -> Proof FALSE) -> Not p
+@
+
+The derivation of proof by contradiction from the law of the excluded
+middle goes like this: first, use the law of the excluded middle to
+prove @p || Not p@. Then use or-elimination to prove @p@ for each
+alternative. The first alternative is immediate; for the second
+alternative, use the provided implication to get a proof of falsehood,
+from which the desired conclusion is derived.
+
+@
+contradiction impl =
+  do  lem             -- introduce p || Not p
+   |$ or_elimL given  -- dispatch the first, straightforward case
+   |/ impl            -- Now we're on the second case. Apply the implication..
+   |. absurd          -- .. and, from falsity, conclude p.
+@
+-}
+contradiction :: forall p. Classical => (Not p -> Proof FALSE) -> Proof p
+contradiction impl =
+  do  lem
+   |$ or_elimL given
+   |/ impl
+   |. absurd
+  
+{-| Double-negation elimination. This is another non-constructive
+    proof technique, so it requires the @Classical@ constraint.
+
+    The derivation of double-negation elimination follows from
+    proof by contradiction, since "Not (Not p)" contradicts "Not p".
+@
+not_not_elim p'' = contradiction (contradicts' p'')
+@
+-}
+
+not_not_elim :: Classical => Not (Not p) -> Proof p
+not_not_elim p'' = contradiction (contradicts' p'')
+
+{--------------------------------------------------
+  Algebraic properties
+--------------------------------------------------}
+
+instance Symmetric And
+instance Symmetric Or
+
+instance Associative And
+instance Associative Or
+
+instance DistributiveR And And
+instance DistributiveR And Or
+instance DistributiveR Or  And
+instance DistributiveR Or  Or
+
+instance DistributiveL And And
+instance DistributiveL And Or
+instance DistributiveL Or  And
+instance DistributiveL Or  Or
+
diff --git a/src/Theory/Equality.hs b/src/Theory/Equality.hs
new file mode 100644
--- /dev/null
+++ b/src/Theory/Equality.hs
@@ -0,0 +1,136 @@
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE FlexibleContexts      #-}
+
+{-|
+  Module      :  Theory.Equality
+  Copyright   :  (c) Matt Noonan 2018
+  License     :  BSD-style
+  Maintainer  :  matt.noonan@gmail.com
+  Portability :  portable
+-}
+
+module Theory.Equality
+  (
+    Equals, type (==)
+
+  -- ** Substitutions and equational reasoning
+  , (==.)
+  , apply
+  , substitute
+  , substituteL
+  , substituteR
+
+  -- ** Relating to other forms of equality
+  , same
+  , reflectEq
+  , propEq
+  ) where
+
+import Data.Arguments
+import Data.The
+import Theory.Named
+import Logic.Proof (Proof, axiom)
+
+import Lawful
+
+import Unsafe.Coerce
+import Data.Type.Equality ((:~:)(..))
+
+{--------------------------------------------------
+  Theory of equality
+--------------------------------------------------}
+
+-- | The @Equals@ relation is used to express equality between two entities.
+--   Given an equality, you are then able to substitute one side of the equality
+--   for the other, anywhere you please.
+newtype Equals x y = Equals Defn
+
+-- | An infix alias for 'Equals'.
+type x == y = x `Equals` y
+infix 4 ==
+
+instance Argument (Equals x y) 0 where
+  type GetArg (Equals x y) 0    = x
+  type SetArg (Equals x y) 0 x' = Equals x' y
+
+instance Argument (Equals x y) 1 where
+  type GetArg (Equals x y) 1    = y
+  type SetArg (Equals x y) 1 y' = Equals x y'
+
+instance Argument (Equals x y) LHS where
+  type GetArg (Equals x y) LHS    = x
+  type SetArg (Equals x y) LHS x' = Equals x' y
+
+instance Argument (Equals x y) RHS where
+  type GetArg (Equals x y) RHS    = y
+  type SetArg (Equals x y) RHS y' = Equals x y'
+
+-- | Chain equalities, a la Liquid Haskell.
+(==.) :: Proof (x == y) -> Proof (y == z) -> Proof (x == z)
+_ ==. _ = axiom
+
+-- | Apply a function to both sides of an equality.
+apply :: forall f n x x'. (Argument f n, GetArg f n ~ x)
+    => Arg n -> (x == x') -> Proof (f == SetArg f n x')
+apply _ _ = axiom
+
+-- | Given a formula and an equality over ones of its arguments,
+--   replace the left-hand side of the equality with the right-hand side.
+substitute :: (Argument f n, GetArg f n ~ x)
+    => Arg n -> (x == x') -> f -> Proof (SetArg f n x')
+substitute _ _ _ = axiom
+
+-- | Substitute @x'@ for @x@ under the function @f@, on the left-hand side
+--   of an equality.
+substituteL :: (Argument f n, GetArg f n ~ x)
+    => Arg n -> (x == x') -> (f == g) -> Proof (SetArg f n x' == g)
+substituteL _ _ _ = axiom
+
+-- | Substitute @x'@ for @x@ under the function @f@, on the right-hand side
+--   of an equality.
+substituteR :: (Argument f n, GetArg f n ~ x)
+    => Arg n -> (x == x') -> (g == f) -> Proof (g == SetArg f n x')
+substituteR _ _ _ = axiom
+
+{--------------------------------------------------
+  Theory of equality
+--------------------------------------------------}
+
+-- | Test if the two name arguments are equal an, if so, produce a proof
+--   of equality for the names.
+same :: Lawful Eq a => (a ~~ x) -> (a ~~ y) -> Maybe (Proof (x == y))
+same (The x) (The y) = if x == y then Just axiom else Nothing
+
+{-| Reflect an equality between @x@ and @y@ into a propositional
+    equality between the /types/ @x@ and @y@.
+
+@
+newtype Bob = Bob Defn
+
+bob :: Int ~~ Bob
+bob = defn 42
+
+needsBob :: (Int ~~ Bob) -> Int
+needsBob x = the x + the x
+
+isBob :: (Int ~~ name) -> Maybe (Proof (name == Bob))
+isBob = same x bob
+
+f :: (Int ~~ name) -> Int
+f x = case reflectEq \<$\> isBob x of
+  Nothing   -> 17
+  Just Refl -> needsBob x x
+@
+-}
+reflectEq :: Proof (x == y) -> (x :~: y)
+reflectEq _ = unsafeCoerce (Refl :: a :~: a)
+
+-- | Convert a propositional equality between the types @x@ and @y@
+--   into a proof of @x == y@.
+propEq :: (x :~: y) -> Proof (x == y)
+propEq _ = axiom
diff --git a/src/Theory/Named.hs b/src/Theory/Named.hs
new file mode 100644
--- /dev/null
+++ b/src/Theory/Named.hs
@@ -0,0 +1,86 @@
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE ConstraintKinds       #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+
+{-|
+  Module      :  Theory.Named
+  Copyright   :  (c) Matt Noonan 2018
+  License     :  BSD-style
+  Maintainer  :  matt.noonan@gmail.com
+  Portability :  portable
+-}
+
+module Theory.Named
+  ( -- * Named values
+    Named, type (~~)
+  , name
+  , name2, name3
+
+  -- ** Definitions
+  , Defining
+  , Defn
+  , defn
+  ) where
+
+import Data.The
+import Data.Coerce
+
+{--------------------------------------------------
+  Named values
+--------------------------------------------------}
+
+-- | A value of type @a ~~ name@ has the same runtime
+--   representation as a value of type @a@, with a
+--   phantom "name" attached.
+newtype Named name a = Named a
+
+-- | An infix alias for 'Named'.
+type a ~~ name = Named name a
+
+instance The (Named name a) a
+
+-- | Introduce a name for the argument, and pass the
+--   named argument into the given function.
+name :: a -> (forall name. a ~~ name -> t) -> t
+name x k = k (coerce x)
+
+-- | Same as 'name', but names two values at once.
+name2 :: a -> b -> (forall name1 name2. (a ~~ name1) -> (b ~~ name2) -> t) -> t
+name2 x y k = k (coerce x) (coerce y)
+
+-- | Same as 'name', but names three values at once.
+name3 :: a -> b -> c -> (forall name1 name2 name3. (a ~~ name1) -> (b ~~ name2) -> (c ~~ name3) -> t) -> t
+name3 x y z k = k (coerce x) (coerce y) (coerce z)
+
+
+{--------------------------------------------------
+  Definitions
+--------------------------------------------------}
+
+{-| Library authors can introduce new names in a controlled way
+    by creating @newtype@ wrappers of @Defn@. The constructor of
+    the @newtype@ should *not* be exported, so that the library
+    can retain control of how the name is introduced.
+
+@
+newtype Bob = Bob Defn
+
+bob :: Int ~~ Bob
+bob = defn 42
+@
+-}
+data Defn = Defn
+
+-- | The @Defining P@ constraint holds in any module where @P@
+--   has been defined as a @newtype@ wrapper of @Defn@. It
+--   holds /only/ in that module, if the constructor of @P@
+--   is not exported.
+type Defining p = (Coercible p Defn, Coercible Defn p)
+
+-- | In the module where the name @f@ is defined, attach the
+--   name @f@ to a value.
+defn :: Defining f => a -> (a ~~ f)
+defn = coerce