diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,7 @@
+## 0.6.0 (2023-05-10)
+  * add instances for `Refined1 p f a`; use refined1 library instead of refined
+    (pending upstream)
+
 ## 0.5.0 (2023-05-05)
   * allow text-2.0
   * refactor strengthening code, rename some definitions
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -8,6 +8,7 @@
 
 ## What? Why?
 [refined-blog]: http://nikita-volkov.github.io/refined/
+[refined-hackage]: https://hackage.haskell.org/package/refined
 
 Haskell is a wonderful language for accurate data modelling. Algebraic data
 types (and GADTs as a fancy extension) enable defining highly restricted types
@@ -50,6 +51,9 @@
 Oh! So this is like a parser-printer pair for arbitrary data. It seems like a
 useful enough pattern. Let's think of some strongweak pairs:
 
+  * `Refined p a` from the [refined][refined-hackage] library is an `a` where
+    the predicate `p` has been asserted. This can be weakened into an `a` via
+    `unrefine :: Refined p a -> a`.
   * `Word8` is a bounded natural number. `Natural` can represent any natural
     number. So `Natural` is a weak type, which can be strengthened into `Word8`
     (or `Word16`, `Word32`, ...) by asserting well-boundedness.
diff --git a/src/Strongweak/Strengthen.hs b/src/Strongweak/Strengthen.hs
--- a/src/Strongweak/Strengthen.hs
+++ b/src/Strongweak/Strengthen.hs
@@ -189,10 +189,21 @@
     Nothing -> failShowNoVal @(Weak a) detail
 
 -- | Assert a predicate to refine a type.
-instance (Predicate (p :: k) a, Typeable k, Typeable a)
+instance (Predicate p a, Typeable a)
   => Strengthen (Refined p a) where
     strengthen = refine .> \case
       Left  rex -> failShowNoVal @a
+        [ "refinement: "<>tshow (typeRep' @p)
+        , "failed with..."
+        , tshow (displayRefineException rex)
+        ]
+      Right ra  -> Success ra
+
+-- | Assert a functor predicate to refine a type.
+instance (Predicate1 p f, Typeable f, Typeable (a :: ak), Typeable ak)
+  => Strengthen (Refined1 p f a) where
+    strengthen = refine1 .> \case
+      Left  rex -> failShowNoVal @(f a)
         [ "refinement: "<>tshow (typeRep' @p)
         , "failed with..."
         , tshow (displayRefineException rex)
diff --git a/src/Strongweak/Weaken.hs b/src/Strongweak/Weaken.hs
--- a/src/Strongweak/Weaken.hs
+++ b/src/Strongweak/Weaken.hs
@@ -12,7 +12,7 @@
   , type SWDepth
   ) where
 
-import Refined ( Refined, unrefine )
+import Refined ( Refined, unrefine, Refined1, unrefine1 )
 import Data.Word
 import Data.Int
 import Data.Vector.Generic.Sized qualified as VGS -- Shazbot!
@@ -72,6 +72,11 @@
 instance Weaken (Refined p a) where
     type Weak (Refined p a) = a
     weaken = unrefine
+
+-- | Strip refined functor type refinement.
+instance Weaken (Refined1 p f a) where
+    type Weak (Refined1 p f a) = f a
+    weaken = unrefine1
 
 -- | Weaken non-empty lists into plain lists.
 instance Weaken (NonEmpty a) where
diff --git a/strongweak.cabal b/strongweak.cabal
--- a/strongweak.cabal
+++ b/strongweak.cabal
@@ -5,7 +5,7 @@
 -- see: https://github.com/sol/hpack
 
 name:           strongweak
-version:        0.5.0
+version:        0.6.0
 synopsis:       Convert between strong and weak representations of types
 description:    Please see README.md.
 category:       Data
@@ -59,7 +59,7 @@
     , base >=4.14 && <5
     , either >=5.0.1.1 && <5.1
     , prettyprinter >=1.7.1 && <1.8
-    , refined >=0.7 && <0.9
+    , refined1 ==0.9.*
     , text >=1.2.5.0 && <2.1
     , vector >=0.12.3.1 && <0.14
     , vector-sized >=1.5.0 && <1.6
@@ -98,7 +98,7 @@
     , hspec >=2.7 && <2.11
     , prettyprinter >=1.7.1 && <1.8
     , quickcheck-instances >=0.3.26 && <0.4
-    , refined >=0.7 && <0.9
+    , refined1 ==0.9.*
     , strongweak
     , text >=1.2.5.0 && <2.1
     , vector >=0.12.3.1 && <0.14