diff --git a/Data/Type/Ordinal.hs b/Data/Type/Ordinal.hs
--- a/Data/Type/Ordinal.hs
+++ b/Data/Type/Ordinal.hs
@@ -1,5 +1,5 @@
 {-# LANGUAGE DataKinds, EmptyDataDecls, FlexibleContexts, FlexibleInstances #-}
-{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE ScopedTypeVariables, TemplateHaskell #-}
 {-# LANGUAGE GADTs, KindSignatures, PolyKinds, StandaloneDeriving           #-}
 {-# LANGUAGE TypeFamilies, TypeOperators                                    #-}
 -- | Set-theoretic ordinal arithmetic
@@ -9,12 +9,18 @@
          -- * Conversion from cardinals to ordinals.
          sNatToOrd', sNatToOrd, ordToInt, ordToSNat,
          ordToSNat', CastedOrdinal(..),
-         unsafeFromInt,
+         unsafeFromInt, inclusion, inclusion',
          -- * Ordinal arithmetics
-         (@+), enumOrdinal
+         (@+), enumOrdinal,
+         -- * Quasi Quote
+         od
        ) where
 import Data.Type.Monomorphic
+import Unsafe.Coerce
+import Language.Haskell.TH.Quote
+import Language.Haskell.TH
 import Data.Type.Natural hiding (promote)
+import Proof.Equational (coerce)
 import Data.Constraint
 
 -- | Set-theoretic (finite) ordinals:
@@ -116,26 +122,38 @@
 
 -- | Inclusion function for ordinals.
 inclusion' :: (n :<<= m) ~ True => SNat m -> Ordinal n -> Ordinal m
+inclusion' _ = unsafeCoerce
+{-# INLINE inclusion' #-}
+{-
+-- The "proof" of the correctness of the above
+inclusion' :: (n :<<= m) ~ True => SNat m -> Ordinal n -> Ordinal m
 inclusion' (SS SZ) OZ = OZ
 inclusion' (SS (SS _)) OZ = OZ
 inclusion' (SS (SS n)) (OS m) = OS $ inclusion' (sS n) m
 inclusion' _ _ = bugInGHC
+-}
 
 -- | Inclusion function for ordinals with codomain inferred.
-inclusion :: ((n :<<= m) ~ True, SingRep m) => Ordinal n -> Ordinal m
-inclusion = inclusion' sing
+inclusion :: ((n :<<= m) ~ True) => Ordinal n -> Ordinal m
+inclusion on = unsafeCoerce on
+{-# INLINE inclusion #-}
 
 -- | Ordinal addition.
 (@+) :: forall n m. (SingRep n, SingRep m) => Ordinal n -> Ordinal m -> Ordinal (n :+ m)
 OZ @+ n =
   let sn = sing :: SNat n
       sm = sing :: SNat m
-  in case singInstance (sn %+ sm) of
-       SingInstance ->
-         case propToBoolLeq (plusLeqR sn sm) of
-           Dict -> inclusion n
+  in case propToBoolLeq (plusLeqR sn sm) of
+      Dict -> inclusion n
 OS n @+ m =
   case sing :: SNat n of
     SS sn -> case singInstance sn of SingInstance -> OS $ n @+ m
     _ -> bugInGHC
 
+-- | Quasiquoter for ordinals
+od :: QuasiQuoter
+od = QuasiQuoter { quoteExp = foldr appE (conE 'OZ) . flip replicate (conE 'OS) . read
+                 , quoteType = error "No type quoter for Ordinals"
+                 , quotePat = foldr (\a b -> conP a [b]) (conP 'OZ []) . flip replicate 'OS . read
+                 , quoteDec = error "No declaration quoter for Ordinals"
+                 }
diff --git a/type-natural.cabal b/type-natural.cabal
--- a/type-natural.cabal
+++ b/type-natural.cabal
@@ -2,7 +2,7 @@
 -- documentation, see http://haskell.org/cabal/users-guide/
 
 name:                type-natural
-version:             0.1.0.0
+version:             0.2.0.0
 synopsis:            Type-level natural and proofs of their properties.
 description:         Type-level natural numbers and proofs of their properties.
 homepage:            https://github.com/konn/type-natural