diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,14 @@
 # Revision history for coercible-subtypes
 
+## 0.3.0.0 -- 2023-01-01
+
+* Breaking changes
+  
+  * Change the `Newtype.Intersection.associative` and `Newtype.Union.associative` to new,
+    more succinct type.
+
+* Instance added to `IsIntersection` and `IsUnion`
+
 ## 0.2.0.0 -- 2021-09-13
 
 * Add `Related`
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.2.0.0
+version:             0.3.0.0
 stability:           experimental
 synopsis:            Coercible but only in one direction
 description: Newtype wrapper 'Data.Type.Coercion.Sub.Sub'
@@ -32,7 +32,7 @@
                        Data.Type.Coercion.Related.Internal,
                        Newtype.Union,
                        Newtype.Intersection
-  build-depends:       base >=4.12 && <4.17,
+  build-depends:       base >=4.12 && <4.18,
                        profunctors
   hs-source-dirs:      src
   default-language:    Haskell2010
diff --git a/src/Newtype/Intersection.hs b/src/Newtype/Intersection.hs
--- a/src/Newtype/Intersection.hs
+++ b/src/Newtype/Intersection.hs
@@ -2,7 +2,6 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ExistentialQuantification #-}
-{-# LANGUAGE TypeOperators #-}
 module Newtype.Intersection(
   module Data.Type.Coercion.Related,
   IsIntersection(..),
@@ -17,7 +16,7 @@
 import Data.Type.Coercion.Sub.Internal
 import Data.Type.Coercion.Related
 import Data.Type.Coercion.Related.Internal
-import Data.Type.Coercion ( Coercion(Coercion) )
+import Data.Type.Coercion ( Coercion(Coercion), TestCoercion(..) )
 
 -- | @IsIntersection x y z@ witnesses the fact:
 --
@@ -34,6 +33,14 @@
     conjunct :: forall s. Sub s x -> Sub s y -> Sub s z
   }
 
+instance Eq (IsIntersection x y z) where
+  _ == _ = True
+instance Ord (IsIntersection x y z) where
+  compare _ _ = EQ
+
+instance TestCoercion (IsIntersection x y) where
+  testCoercion u1 u2 = Just (unique u1 u2)
+
 -- | 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
@@ -52,18 +59,27 @@
 
 -- | Intersection is idempotent.
 --
---   Note: combining @idemp@ and 'unique', @IsIntersection x x z -> Coercible x z@ holds.
+--   Note: combining @idemp@ and 'unique', @IsIntersection x x z -> Coercion 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.
+--   Note: combining @commutative@ and 'unique', @IsIntersection x y xy -> IsIntersection y x yx -> Coercion xy yx@ 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))
+--
+--   Note: combining @associative@ and 'unique', the following holds.
+--   
+--   >    IsIntersection x y xy -> IsIntersection xy z xy'z
+--   > -> IsIntersection y z yz -> IsIntersection x yz x'yz
+--   > -> Coercion xy'z x'yz 
+associative :: IsIntersection x y xy -> IsIntersection xy z xyz -> IsIntersection y z yz -> IsIntersection x yz xyz
+associative xy xy'z yz =
+    IsIntersection {
+       proj1 = proj1 xy . proj1 xy'z
+     , proj2 = conjunct yz (proj2 xy . proj1 xy'z) (proj2 xy'z)
+     , conjunct = \s_x s_yz -> conjunct xy'z (conjunct xy s_x (proj1 yz . s_yz)) (proj2 yz . s_yz)
+    }
diff --git a/src/Newtype/Union.hs b/src/Newtype/Union.hs
--- a/src/Newtype/Union.hs
+++ b/src/Newtype/Union.hs
@@ -1,8 +1,6 @@
-{-# LANGUAGE BangPatterns #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ExistentialQuantification #-}
-{-# LANGUAGE TypeOperators #-}
 module Newtype.Union(
   module Data.Type.Coercion.Related,
   IsUnion(..),
@@ -18,7 +16,7 @@
 import Data.Type.Coercion.Sub.Internal
 import Data.Type.Coercion.Related
 import Data.Type.Coercion.Related.Internal
-import Data.Type.Coercion ( Coercion(Coercion))
+import Data.Type.Coercion ( Coercion(Coercion), TestCoercion(..))
 
 -- | @IsUnion x y z@ witnesses the fact:
 --
@@ -36,6 +34,14 @@
       -- ^ Given both @x@ and @y@ can be safely coerced to @r@, too @z@ can.
   }
 
+instance Eq (IsUnion x y z) where
+  _ == _ = True
+instance Ord (IsUnion x y z) where
+  compare _ _ = EQ
+
+instance TestCoercion (IsUnion x y) where
+  testCoercion u1 u2 = Just (unique u1 u2)
+
 -- | 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
@@ -53,18 +59,27 @@
 
 -- | Union is idempotent.
 --
---   Note: combining @idemp@ and 'unique', @IsUnion x x z -> Coercible x z@ holds.
+--   Note: combining @idemp@ and 'unique', @IsUnion x x z -> Coercion 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.
+--   Note: combining @commutative@ and 'unique', @IsUnion x y xy -> IsUnion y x yx -> Coercion 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)))
+--
+--   Note: combining @associative@ and 'unique', the following holds.
+--   
+--   >    IsUnion x y xy -> IsUnion xy z xy'z
+--   > -> IsUnion y z yz -> IsUnion x yz x'yz
+--   > -> Coercion xy'z x'yz 
+associative :: IsUnion x y xy -> IsUnion xy z xyz -> IsUnion y z yz -> IsUnion x yz xyz
+associative xy xy'z yz =
+    IsUnion {
+       inl = inl xy'z . inl xy 
+     , inr = elim yz (inl xy'z . inr xy) (inr xy'z)
+     , elim = \x_r yz_r -> elim xy'z (elim xy x_r (yz_r . inl yz)) (yz_r . inr yz)
+    }