diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,5 @@
+# Revision history for coercible-subtypes
+
+## 0.1.0.0 -- 2020-04-08
+
+* First version.
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2020, Koji Miyazato
+
+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 Koji Miyazato 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,107 @@
+# coercible-subtypes
+
+This library provides unidirectional (one-way) variant of [Coercion](https://hackage.haskell.org/package/base-4.12.0.0/docs/Data-Type-Coercion.html).
+
+The variant is a type `Sub` defined in `Data.Type.Coercion.Sub`.
+`Sub a b` can be used to convert a type `a` to another type `b`.
+
+```
+upcastWith :: Sub a b -> a -> b
+```
+
+For all `Sub a b` values, the runtime representation of `a` and
+`b` values are same, so `upcastWith` do not require any computation
+to return `b` value, just [coerce](https://hackage.haskell.org/package/base-4.12.0.0/docs/Data-Coerce.html)s
+GHC to treat a value of `a` as type `b`.
+This feature is not different to `Coercion`.
+
+The difference is that while `Coercion` represents
+bidirectional relation, `Sub` represents unidirectional relation.
+`Coercion a b` and its underlying type class `Coercible a b` witnesse you can coerce both `a` to `b` and `b` to `a`.
+Unlike that, `Sub a b` only allows you to coerce `a` to `b`, not `b` to `a`.
+
+## Usage Example
+
+To use this library effectively, it must be used at two places: a library
+and its user code. For this example, let's assume they are written by two people,
+a *library author* and a *user*.
+
+The library author writes a module `RightTriangle` below.
+
+```
+module RightTriangle(Triangle(), toEdges, getEdges, fromEdges) where
+  import Data.Coerce
+  import Data.Type.Coercion.Sub
+  
+  newtype Triangle = MkTriangle (Int, Int, Int)
+  
+  -- | Triangles can be coerced into 3-tuples of Ints
+  toEdges :: Sub Triangle (Int, Int, Int)
+  toEdges = sub
+  
+  getEdges :: Triangle -> (Int, Int, Int)
+  getEdges = coerce
+  
+  -- | Creates right triangle from lengths of edges (a,b,c)
+  -- 
+  -- >  *
+  -- >  |\ c
+  -- > a| \
+  -- >  *--*
+  -- >   b
+  --
+  -- (a^2 + b^2 == c^2) must hold.
+  fromEdges :: (Int, Int, Int) -> Maybe Triangle
+  fromEdges = {- Omit -}
+```
+
+The author wants to protect the invariant condition `a^2 + b^2 == c^2`.
+For that purpose, the author can't export the constructor of `Triangle`.
+Because it is symmetric, `Coercion Triangle (Int,Int,Int)` can't be exported either.
+
+The user is building an application using `RightTriangle` module.
+
+```
+module Main where
+  import Data.Map (Map)
+  import RightTriangle
+  
+  import Data.Type.Coercion.Sub
+  
+  main :: IO ()
+  main = ......
+```
+
+In this application, the user has to convert `Map String Triangle` to
+`Map String (Int, Int, Int)`, revealing the edge lengths of the triangles.
+While it is easy to do so with `fmap getEdges`,
+using `fmap` here can make an entire copy of the Map<sup>[†](#footnote)</sup>.
+This is wasted work and memory. Instead, the user can use `mapR toEdges` to get
+`Sub (Map String Triangle) (Map String (Int, Int, Int))`
+and then `upcastWith` to perform zero cost coercion over `Map`.
+
+## Comparison against other methods
+
+There are some other methods to achive the goal of this library.
+
+* Just give up coercion
+
+  * This is just for better performance, so not doing it
+    is always an option.
+
+* Rewrite rules
+
+  * Rewrite rules based method is currently employed, and working at our hand.
+    So, it is possible you don't need this library at all.
+  
+  * The downside is whether it works or not is on the provider of the
+    "container" type in use, and GHC doing expected optimizations.
+    Without reading source codes and examining the GHC optimization result (e.g. `-ddump-rule-firings`),
+    you can't be sure you are doing the conversion zero-cost.
+
+--------
+
+<a id="footnote">†</a> For `Data.Map`, which [containers](https://hackage.haskell.org/package/containers)
+package provides, can optimize `fmap` away via proper inlining and rewrite rules. The purpose of this library
+is turning optimizations into explicit codes, or handling the cases when the container type in use does not
+provide such an opportunity via rewrite rules.</small>
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/coercible-subtypes.cabal b/coercible-subtypes.cabal
new file mode 100644
--- /dev/null
+++ b/coercible-subtypes.cabal
@@ -0,0 +1,35 @@
+cabal-version:       2.2
+name:                coercible-subtypes
+version:             0.1.0.0
+stability:           experimental
+synopsis:            Coercible but only in one direction
+description: Newtype wrapper 'Data.Type.Coercion.Sub.Sub'
+             around 'Data.Type.Coercion.Coercion'
+             to represent unidirectional coercion,
+             and combinators for it, like 'Data.Type.Coercion.Sub.mapR'
+             which extends coercion over covariant @Functor@.
+
+homepage:            https://github.com/viercc/coercible-subtypes
+bug-reports:         https://github.com/viercc/coercible-subtypes/issues
+license:             BSD-3-Clause
+license-file:        LICENSE
+author:              Koji Miyazato
+maintainer:          viercc@gmail.com
+copyright:           (c) 2020 Koji Miyazato
+category:            Data
+build-type:          Simple
+extra-source-files:  CHANGELOG.md, README.md
+
+source-repository HEAD
+  type:     git
+  location: https://github.com/viercc/coercible-subtypes
+  branch:   master
+
+library
+  exposed-modules:     Data.Type.Coercion.Sub,
+                       Data.Type.Coercion.Sub.Internal
+  build-depends:       base >=4.12 && <4.15,
+                       profunctors
+  hs-source-dirs:      src
+  default-language:    Haskell2010
+  ghc-options:         -Wall -Wcompat
diff --git a/src/Data/Type/Coercion/Sub.hs b/src/Data/Type/Coercion/Sub.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Coercion/Sub.hs
@@ -0,0 +1,121 @@
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE PolyKinds             #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE RankNTypes            #-}
+module Data.Type.Coercion.Sub(
+  {- | @Sub a b@ witnesses a zero-cost conversion @a -> b@.
+
+  @Sub@ is a newtype wrapper around 'Coercion', but made opaque to hide
+  the ability to 'Data.Coerce.coerce' into other direction.
+
+  This is convenient for newtype wrappers which give additional guarantees.
+
+  As an example, think about the following code:
+
+  > -- | A pair @(x::a, y::a)@, but guaranteed @x <= y@
+  > newtype Range a = MkRange (a,a)
+  >
+  > getRange :: Range a -> (a,a)
+  > getRange = coerce
+  > mkRange :: Ord a => a -> a -> Range a
+  > mkRange x y = if x <= y then MkRange (x,y) else MkRange (y,x)
+
+  If you want to provide this type from a library you maintain,
+  you would want to keep @Range@ abstract from outside of the module.
+
+  An user may want to convert @[Range a]@ to @[(a,a)]@ without actually
+  traversing the list. This is possible if the user have access to the
+  internals, or you export a @Coercion (Range a) (a,a)@ value. But doing so
+  breaks the guarantee, because it also allows to use @Coercible@ in the other
+  direction, as in @coerce (10,5) :: Range Int@.
+
+  By exporting only @Sub (Range a) (a,a)@ value from your module,
+  this user can get @Sub [Range a] [(a,a)]@ using 'mapR',
+  without being able to make an invalid value.
+  
+  -}
+  Sub(),
+  sub, toSub, upcastWith, equiv, gequiv,
+
+  coercionIsSub,
+
+  mapR, contramapR,
+  bimapR, dimapR
+) where
+
+import           Data.Coerce
+import           Data.Type.Coercion
+
+import           Data.Bifunctor                  (Bifunctor)
+import           Data.Functor.Contravariant      (Contravariant)
+import           Data.Profunctor                 (Profunctor)
+
+import           Data.Type.Coercion.Sub.Internal
+
+-- | Make a witness for type-safe casting which respects direction.
+sub :: Coercible a b => Sub a b
+sub = Sub Coercion
+
+toSub :: Coercion a b -> Sub a b
+toSub = Sub
+
+-- | Type-safe cast
+upcastWith :: Sub a b -> a -> b
+upcastWith (Sub Coercion) = coerce
+
+-- | All 'Coercion' can be seen as 'Sub'
+coercionIsSub :: Sub (Coercion a b) (Sub a b)
+coercionIsSub = Sub Coercion
+
+-- | `Sub` relation in both direction means there is `Coercion` relation.
+equiv :: Sub a b -> Sub b a -> Coercion a b
+equiv ab ba = gequiv ab ba Coercion
+
+-- | Generalized 'equiv'
+gequiv :: Sub a b -> Sub b a -> (Coercible a b => r) -> r
+gequiv (Sub Coercion) (Sub Coercion) k = k
+
+{-
+
+Note: evaluating both arguments of `equiv` is necessary.
+One might notice the following typechecks.
+
+    equiv :: Sub a b -> Sub b a -> Coercion a b
+    equiv (Sub Coercion) _ = Coercion
+
+But this implementation allows inverting `Sub a b` circumventing the restriction;
+
+    bad :: Sub a b -> Sub b a
+    bad ab =
+      let ba = upcastWith coercionIsSub (equiv ab ba)
+      in ba
+
+This is prevented by evaluating both arguments of `equiv`, making `bad ab` a bottom.
+
+-}
+
+-----------------------------
+
+-- | Extend subtype relation covariantly.
+mapR :: ( forall x x'. Coercible x x' => Coercible (t x) (t x')
+        , Functor t)
+     => Sub a b -> Sub (t a) (t b)
+mapR (Sub Coercion) = Sub Coercion
+
+-- | Extend subtype relation contravariantly
+contramapR :: ( forall x x'. Coercible x x' => Coercible (t x) (t x')
+              , Contravariant t)
+           => Sub a b -> Sub (t b) (t a)
+contramapR (Sub Coercion) = Sub Coercion
+
+bimapR :: ( forall x x' y y'.
+              (Coercible x x', Coercible y y') => Coercible (t x y) (t x' y')
+          , Bifunctor t)
+       => Sub a a' -> Sub b b' -> Sub (t a b) (t a' b')
+bimapR (Sub Coercion) (Sub Coercion) = Sub Coercion
+
+dimapR :: ( forall x x' y y'.
+              (Coercible x x', Coercible y y') => Coercible (t x y) (t x' y')
+          , Profunctor t)
+       => Sub a a' -> Sub b b' -> Sub (t a' b) (t a b')
+dimapR (Sub Coercion) (Sub Coercion) = Sub Coercion
diff --git a/src/Data/Type/Coercion/Sub/Internal.hs b/src/Data/Type/Coercion/Sub/Internal.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Coercion/Sub/Internal.hs
@@ -0,0 +1,42 @@
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE InstanceSigs          #-}
+{-# LANGUAGE PolyKinds             #-}
+
+{- |
+
+This module exposes internals of "Data.Type.Coercion.Sub".
+
+Using this module allows to violate the premises 'Sub' type provides.
+It is advisable not to import this module if there is another way,
+and to limit the amount of code accesible to this module.
+
+-}
+module Data.Type.Coercion.Sub.Internal(
+  Sub(..)
+) where
+
+import           Control.Category
+import           Prelude                    hiding (id, (.))
+
+import           Data.Type.Coercion
+
+newtype Sub (a :: k) (b :: k) = Sub { getSub :: Coercion a b }
+  deriving (Eq, Ord, Show)
+-- It is intentional to omit some instances.
+--
+-- TestCoercion instance should not exist.
+-- Knowing `Sub a b` and `Sub a c` should not conclude
+-- `Coercible b c`.
+--
+-- Among instances `Coercion` has, Enum, Bounded, and Read are
+-- excluded because they allows to make new value of `Sub a b`.
+-- Constructing `Sub a b` values must be done through
+-- combinators provided by this module or exported for
+-- abstract type under library author's careful choice.
+
+instance Category Sub where
+  id :: Sub a a
+  id = Sub Coercion
+
+  (.) :: Sub b c -> Sub a b -> Sub a c
+  Sub Coercion . Sub Coercion = Sub Coercion