diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,10 @@
 # Revision history for coercible-subtypes
 
+## 0.2.0.0 -- 2021-09-13
+
+* Add `Related`
+* Add `IsIntersection` and `IsUnion` facilities
+
 ## 0.1.1.0 -- 2021-08-24
 
 * Add instances `Coercible a b => (Read (Sub a b), Enum (Sub a b), Bounded (Sub a b))`
diff --git a/coercible-subtypes.cabal b/coercible-subtypes.cabal
--- a/coercible-subtypes.cabal
+++ b/coercible-subtypes.cabal
@@ -1,6 +1,6 @@
 cabal-version:       2.2
 name:                coercible-subtypes
-version:             0.1.1.0
+version:             0.2.0.0
 stability:           experimental
 synopsis:            Coercible but only in one direction
 description: Newtype wrapper 'Data.Type.Coercion.Sub.Sub'
@@ -27,7 +27,11 @@
 
 library
   exposed-modules:     Data.Type.Coercion.Sub,
-                       Data.Type.Coercion.Sub.Internal
+                       Data.Type.Coercion.Sub.Internal,
+                       Data.Type.Coercion.Related,
+                       Data.Type.Coercion.Related.Internal,
+                       Newtype.Union,
+                       Newtype.Intersection
   build-depends:       base >=4.12 && <4.17,
                        profunctors
   hs-source-dirs:      src
diff --git a/src/Data/Type/Coercion/Related.hs b/src/Data/Type/Coercion/Related.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Coercion/Related.hs
@@ -0,0 +1,50 @@
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE PolyKinds             #-}
+{-# LANGUAGE RankNTypes            #-}
+{- |
+  'Related' type to witness that two types @a@ and @b@ shares the same runtime representation,
+  but nothing about whether @a@ can be safely coerced to or from @b@.
+
+  Unlike 'Coercion' or 'Sub', having a value of @Related a b@ does not allow to
+  touch values of @a@ or @b@.
+
+  This module is used alonside "Newtype.Union" and "Newtype.Intersection"
+  to define union and intersection types of two 'Related' types.
+-}
+module Data.Type.Coercion.Related(
+    Related(),
+    related,
+    subIsRelated, coercionIsRelated,
+    symRelated, undirected, informRelation
+) where
+
+import Data.Coerce
+import Data.Type.Coercion
+import Data.Type.Coercion.Sub
+import Data.Type.Coercion.Sub.Internal
+import Data.Type.Coercion.Related.Internal
+
+-- | @'Coercible' a b@ implies @Related a b@.
+related :: Coercible a b => Related a b
+related = Related Coercion
+
+-- | @'Sub' a b@ implies @Related a b@.
+subIsRelated :: Sub (Sub a b) (Related a b)
+subIsRelated = sub
+
+-- | @'Coercion' a b@ implies @'Sub' a b@, which implies @Related a b@.
+coercionIsRelated :: Sub (Coercion a b) (Related a b)
+coercionIsRelated = sub
+
+-- | @Related@ is a symmetric relation.
+symRelated :: Related a b -> Related b a
+symRelated ab = informRelation ab related
+
+-- | A direct consequence of 'informRelation' and 'subIsRelated'.
+undirected :: Sub a b -> (Coercible a b => Related x y) -> Related x y
+undirected ab = informRelation (upcastWith subIsRelated ab)
+
+-- | Given @Related a b@, you can assume @Coercible a b@ for the purpose of proving
+--   another @Related@ relation.
+informRelation :: Related a b -> (Coercible a b => Related x y) -> Related x y
+informRelation (Related Coercion) body = body
diff --git a/src/Data/Type/Coercion/Related/Internal.hs b/src/Data/Type/Coercion/Related/Internal.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Coercion/Related/Internal.hs
@@ -0,0 +1,44 @@
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE InstanceSigs          #-}
+{-# LANGUAGE PolyKinds             #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{- |
+
+This module exposes internals of "Data.Type.Coercion.Related".
+
+Using this module allows to violate the premises 'Related' 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.Related.Internal where
+
+import           Control.Category
+import           Prelude                    hiding (id, (.))
+
+import           Data.Coerce
+import           Data.Type.Coercion
+
+-- | @Related a b@ witnesses @a@ and @b@ shares the same runtime representation,
+--   but nothing about whether @a@ can be safely coerced to or from @b@.
+-- 
+-- You can make 'Related' witnesses by using combinators in this module, or the methods of
+-- the @'Category' Related@ instance: 'id' and @('.')@.
+newtype Related (a :: k) (b :: k) = Related { getRelated :: Coercion a b }
+  deriving stock (Eq, Ord, Show)
+-- It is intentional to omit the 'TestCoercion' instance, existing for @Coercion@.
+-- Knowing @Related a b@ and @Related a c@ should not conclude
+-- @Coercible b c@.
+
+deriving stock instance Coercible a b => Read (Related a b)
+deriving newtype instance Coercible a b => Enum (Related a b)
+deriving newtype instance Coercible a b => Bounded (Related a b)
+
+instance Category Related where
+  id :: Related a a
+  id = Related Coercion
+
+  (.) :: Related b c -> Related a b -> Related a c
+  Related Coercion . Related Coercion = Related Coercion
diff --git a/src/Data/Type/Coercion/Sub.hs b/src/Data/Type/Coercion/Sub.hs
--- a/src/Data/Type/Coercion/Sub.hs
+++ b/src/Data/Type/Coercion/Sub.hs
@@ -2,38 +2,35 @@
 {-# LANGUAGE PolyKinds             #-}
 {-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE RankNTypes            #-}
-module Data.Type.Coercion.Sub(
-  {- | @Sub a b@ witnesses a zero-cost conversion @a -> b@.
+{- | @'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.
+=== Example
 
-  This is convenient for newtype wrappers which give additional guarantees.
+Think about the following code:
 
-  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)
 
-  > -- | 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.
 
-  If you want to provide this type from a library you maintain,
-  you would want to keep @Range@ abstract from outside of the module.
+A 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@.
 
-  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.
 
-  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.
-  
-  -}
+-}
+module Data.Type.Coercion.Sub(
   Sub(),
   sub, toSub, upcastWith, equiv, gequiv,
 
@@ -53,10 +50,11 @@
 
 import           Data.Type.Coercion.Sub.Internal
 
--- | Make a witness for type-safe casting which respects direction.
+-- | Make a directed witness of @'coerce' :: a -> b@.
 sub :: Coercible a b => Sub a b
 sub = Sub Coercion
 
+-- | Make a directed witness of @'coerce' :: a -> b@, from a 'Coercion' value.
 toSub :: Coercion a b -> Sub a b
 toSub = Sub
 
@@ -146,7 +144,7 @@
        => Sub a a' -> Sub b b' -> Sub (t a' b) (t a b')
 dimapR (Sub Coercion) (Sub Coercion) = Sub Coercion
 
--- | 'dimapR' specialized for '(->)'
+-- | 'dimapR' specialized for functions @(->)@
 arrR :: Sub a a' -> Sub b b' -> Sub (a' -> b) (a -> b')
 arrR = dimapR
 
diff --git a/src/Data/Type/Coercion/Sub/Internal.hs b/src/Data/Type/Coercion/Sub/Internal.hs
--- a/src/Data/Type/Coercion/Sub/Internal.hs
+++ b/src/Data/Type/Coercion/Sub/Internal.hs
@@ -23,6 +23,15 @@
 import           Data.Coerce
 import           Data.Type.Coercion
 
+{- |
+  @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.
+
+  You can make @Sub@ witnesses by using combinators in this module, or the methods of
+  the @'Category' Sub@ instance: 'id' and @('.')@.
+-}
 newtype Sub (a :: k) (b :: k) = Sub { getSub :: Coercion a b }
   deriving stock (Eq, Ord, Show)
 -- It is intentional to omit the 'TestCoercion' instance, existing for @Coercion@.
diff --git a/src/Newtype/Intersection.hs b/src/Newtype/Intersection.hs
new file mode 100644
--- /dev/null
+++ b/src/Newtype/Intersection.hs
@@ -0,0 +1,69 @@
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE TypeOperators #-}
+module Newtype.Intersection(
+  module Data.Type.Coercion.Related,
+  IsIntersection(..),
+  withIntersection,
+  
+  unique, lesser, idemp, commutative, associative
+) where
+
+import Prelude hiding (id, (.))
+import Control.Category
+import Data.Type.Coercion.Sub (equiv, sub)
+import Data.Type.Coercion.Sub.Internal
+import Data.Type.Coercion.Related
+import Data.Type.Coercion.Related.Internal
+import Data.Type.Coercion ( Coercion(Coercion) )
+
+-- | @IsIntersection x y z@ witnesses the fact:
+--
+--   * All @x, y, z@ share the same runtime representation
+--   * @z@ is an intersection type of @x@ and @y@. In other words, the following three holds:
+--
+--       * @'Sub' z x@
+--       * @Sub z y@
+--       * For any type @s@ satisfying both of @(Sub s x, Sub s y)@, @Sub s z@.
+data IsIntersection x y z = IsIntersection
+  {
+    proj1 :: !(Sub z x),
+    proj2 :: !(Sub z y),
+    conjunct :: forall s. Sub s x -> Sub s y -> Sub s z
+  }
+
+-- | For a pair of 'Related' types @x@ and @y@, make some (existentially quantified)
+--   type @xy@ where @xy@ is an intersection type of @x, y@.
+withIntersection :: Related x y -> (forall xy. IsIntersection x y xy -> r) -> r
+withIntersection (Related Coercion) body =
+    body IsIntersection{ proj1 = sub, proj2 = id, conjunct = seq }
+
+-- | Two intersection types @z,z'@ of the same pair of types @x,y@ may be different,
+--   but they are equivalent in terms of coercibility.
+unique :: IsIntersection x y z -> IsIntersection x y z' -> Coercion z z'
+unique xy xy' = equiv (conjunct xy' (proj1 xy) (proj2 xy)) (conjunct xy (proj1 xy') (proj2 xy'))
+
+-- | When @Sub x y@, @x@ itself is an intersection type of @x, y@.
+lesser :: Sub x y -> IsIntersection x y x
+lesser l = IsIntersection{ proj1=id, proj2=l, conjunct= \sx !_ -> sx }
+
+
+-- | Intersection is idempotent.
+--
+--   Note: combining @idemp@ and 'unique', @IsIntersection x x z -> Coercible x z@ holds.
+idemp :: IsIntersection x x x
+idemp = lesser id
+
+-- | Intersection is commutative.
+--
+--   Note: combining @commutative@ and 'unique', @IsIntersection x x z -> Coercible x z@ holds.
+commutative :: IsIntersection x y z -> IsIntersection y x z
+commutative xyz = IsIntersection{ proj1 = proj2 xyz, proj2 = proj1 xyz, conjunct = flip (conjunct xyz)}
+
+-- | Intersection is associative.
+associative :: IsIntersection x y xy -> IsIntersection xy z xy'z -> IsIntersection y z yz -> IsIntersection x yz x'yz -> Coercion xy'z x'yz
+associative xy xy'z yz x'yz =
+    equiv (conjunct x'yz (proj1 xy . proj1 xy'z) (conjunct yz (proj2 xy . proj1 xy'z) (proj2 xy'z)))
+          (conjunct xy'z (conjunct xy (proj1 x'yz) (proj1 yz . proj2 x'yz)) (proj2 yz . proj2 x'yz))
diff --git a/src/Newtype/Union.hs b/src/Newtype/Union.hs
new file mode 100644
--- /dev/null
+++ b/src/Newtype/Union.hs
@@ -0,0 +1,70 @@
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE TypeOperators #-}
+module Newtype.Union(
+  module Data.Type.Coercion.Related,
+  IsUnion(..),
+
+  withUnion,
+  
+  unique, greater, idemp, commutative, associative
+) where
+
+import Prelude hiding (id, (.))
+import Control.Category
+import Data.Type.Coercion.Sub (sub, equiv)
+import Data.Type.Coercion.Sub.Internal
+import Data.Type.Coercion.Related
+import Data.Type.Coercion.Related.Internal
+import Data.Type.Coercion ( Coercion(Coercion))
+
+-- | @IsUnion x y z@ witnesses the fact:
+--
+--   * All @x, y, z@ share the same runtime representation
+--   * @z@ is a union type of @x@ and @y@. In other words, the following three holds:
+--
+--     * @'Sub' x z@
+--     * @Sub y z@
+--     * For any type @r@ satisfying both of @(Sub x r, Sub y r)@, @Sub z r@.
+data IsUnion x y z = IsUnion
+  {
+    inl :: !(Sub x z), -- ^ @x@ can be safely coerced to @z@
+    inr :: !(Sub y z), -- ^ @y@ can be safely coerced to @z@
+    elim :: forall r. Sub x r -> Sub y r -> Sub z r
+      -- ^ Given both @x@ and @y@ can be safely coerced to @r@, too @z@ can.
+  }
+
+-- | For a pair of 'Related' types @x@ and @y@, make some (existentially quantified)
+--   type @xy@ where @xy@ is a union type of @x, y@.
+withUnion :: Related x y -> (forall xy. IsUnion x y xy -> r) -> r
+withUnion (Related Coercion) body =
+    body IsUnion{ inl = sub, inr = id, elim = seq }
+
+-- | Two union types @z,z'@ of the same pair of types @x,y@ may be different,
+--   but they are equivalent in terms of coercibility.
+unique :: IsUnion x y z -> IsUnion x y z' -> Coercion z z'
+unique xy xy' = equiv (elim xy (inl xy') (inr xy')) (elim xy' (inl xy) (inr xy))
+
+-- | When @Sub x y@, @y@ itself is a union type of @x, y@.
+greater :: Sub x y -> IsUnion x y y
+greater l = IsUnion{ inl = l, inr = id, elim=seq }
+
+-- | Union is idempotent.
+--
+--   Note: combining @idemp@ and 'unique', @IsUnion x x z -> Coercible x z@ holds.
+idemp :: IsUnion x x x
+idemp = greater id
+
+-- | Union is commutative.
+--
+--   Note: combining @commutative@ and 'unique', @IsUnion x y xy -> IsUnion y x yx -> Coercible xy yx@ holds.
+commutative :: IsUnion x y z -> IsUnion y x z
+commutative xyz = IsUnion{ inl = inr xyz, inr = inl xyz, elim = flip (elim xyz) }
+
+-- | Union is associative.
+associative :: IsUnion x y xy -> IsUnion xy z xy'z -> IsUnion y z yz -> IsUnion x yz x'yz -> Coercion xy'z x'yz
+associative xy xy'z yz x'yz =
+    equiv (elim xy'z (elim xy (inl x'yz) (inr x'yz . inl yz)) (inr x'yz . inr yz))
+          (elim x'yz (inl xy'z . inl xy) (elim yz (inl xy'z . inr xy) (inr xy'z)))