diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,7 @@
+## 0.5.0 (2024-05-26)
+* add tentative operator versions of predicates
+* clear up WIP normalization story
+
 ## 0.4.0 (2024-05-11)
 * add `Eq`, `Ord`, `Arbitrary` instances
 * simplify modules (fewer)
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -32,7 +32,7 @@
 in the code).
 
 rerefined has a single-constructor error type which can be easily and
-efficiently turned into a `String` in a single pass.
+efficiently turned into a string-like in a single pass.
 
 ### No insidious `Typeable` contexts
 See [refined#101](https://github.com/nikita-volkov/refined/issues/101).
diff --git a/rerefined.cabal b/rerefined.cabal
--- a/rerefined.cabal
+++ b/rerefined.cabal
@@ -5,7 +5,7 @@
 -- see: https://github.com/sol/hpack
 
 name:           rerefined
-version:        0.4.0
+version:        0.5.0
 synopsis:       Refinement types, again
 description:    Please see README.md.
 category:       Types, Data
@@ -19,7 +19,6 @@
 tested-with:
     GHC==9.8
   , GHC==9.6
-  , GHC==9.4
 extra-source-files:
     README.md
     CHANGELOG.md
@@ -37,20 +36,22 @@
       Rerefined.Predicate.Fail
       Rerefined.Predicate.Logical
       Rerefined.Predicate.Logical.And
-      Rerefined.Predicate.Logical.Equivalences
       Rerefined.Predicate.Logical.If
       Rerefined.Predicate.Logical.Iff
       Rerefined.Predicate.Logical.Nand
       Rerefined.Predicate.Logical.Nor
+      Rerefined.Predicate.Logical.Normalize
       Rerefined.Predicate.Logical.Not
       Rerefined.Predicate.Logical.Or
       Rerefined.Predicate.Logical.Xor
+      Rerefined.Predicate.Normalize
       Rerefined.Predicate.Relational
       Rerefined.Predicate.Relational.Internal
       Rerefined.Predicate.Relational.Length
       Rerefined.Predicate.Relational.Value
       Rerefined.Predicate.Succeed
       Rerefined.Predicates
+      Rerefined.Predicates.Operators
       Rerefined.Refine
       Rerefined.Refine.TH
   other-modules:
@@ -71,10 +72,10 @@
   ghc-options: -Wall -Wno-unticked-promoted-constructors
   build-depends:
       QuickCheck >=2.14 && <2.16
-    , base >=4.17 && <5
+    , base >=4.18 && <5
     , mono-traversable >=1.0.17.0 && <1.1
     , template-haskell >=2.19.0.0 && <2.22
     , text >=2.0 && <2.2
     , text-builder-linear >=0.1.2 && <0.2
-    , type-level-show >=0.1.0 && <0.2
+    , type-level-show >=0.2.1 && <0.3
   default-language: GHC2021
diff --git a/src/Rerefined/Predicate/Logical.hs b/src/Rerefined/Predicate/Logical.hs
--- a/src/Rerefined/Predicate/Logical.hs
+++ b/src/Rerefined/Predicate/Logical.hs
@@ -1,10 +1,12 @@
-{-# LANGUAGE UndecidableInstances #-} -- TODO TMP
+{- | Logical predicates.
 
+Pretty predicates use infix propositional operators. This is chosen for
+consistency. I'm not really sure which I prefer over all, perhaps best would be
+to mix and match. Please let the maintainers know if you have a better idea.
+-}
+
 module Rerefined.Predicate.Logical
   ( And, Iff, If, Nand, Nor, Not, Or, Xor
-  , NormalizeLogicalStep
-  , NormalizeLogical1Step
-  , Result(..), Idk1'
   ) where
 
 import Rerefined.Predicate.Logical.And
@@ -15,27 +17,3 @@
 import Rerefined.Predicate.Logical.Not
 import Rerefined.Predicate.Logical.Or
 import Rerefined.Predicate.Logical.Xor
-
-import Data.Kind ( Type )
--- left = continue, right = normalized
-type NormalizeLogicalStep :: (kl -> kr -> Type) -> kl -> kr -> Result kl
-type family NormalizeLogicalStep op l r where
-    NormalizeLogicalStep Or   l l = Cont  l
-    NormalizeLogicalStep And  l l = Cont  l
-    NormalizeLogicalStep Nand l l = Cont1 (Not l)
-    NormalizeLogicalStep op   l r = Done (op l r)
-
-data Result kl = Done Type | Cont kl | Cont1 Type
-
-type NormalizeLogical1Step :: (k -> Type) -> k -> Result k
-type family NormalizeLogical1Step op p where
-    NormalizeLogical1Step Not (Not p) = Cont p
-    NormalizeLogical1Step op  p       = Done (op p)
-
-type family Idk1 res where
-    Idk1 (Cont p) = Idk1' p
-    Idk1 (Done p) = p
-
-type family Idk1' p where
-    Idk1' (Not p) = Idk1 (NormalizeLogical1Step Not p)
-    Idk1' p = p
diff --git a/src/Rerefined/Predicate/Logical/Equivalences.hs b/src/Rerefined/Predicate/Logical/Equivalences.hs
deleted file mode 100644
--- a/src/Rerefined/Predicate/Logical/Equivalences.hs
+++ /dev/null
@@ -1,19 +0,0 @@
--- | Logical equivalences.
-
-module Rerefined.Predicate.Logical.Equivalences where
-
-{-
-
--- TODO
-rerefineDeMorgans1
-    :: Refined (Not (Logical Or  l r))       a
-    -> Refined (Logical And (Not l) (Not r)) a
-rerefineDeMorgans1 = unsafeRerefine
-
--- TODO
-rerefineDeMorgans2
-    :: Refined (Not (Logical And l r))       a
-    -> Refined (Logical Or  (Not l) (Not r)) a
-rerefineDeMorgans2 = unsafeRerefine
-
--}
diff --git a/src/Rerefined/Predicate/Logical/Normalize.hs b/src/Rerefined/Predicate/Logical/Normalize.hs
new file mode 100644
--- /dev/null
+++ b/src/Rerefined/Predicate/Logical/Normalize.hs
@@ -0,0 +1,10 @@
+module Rerefined.Predicate.Logical.Normalize where
+
+import Rerefined.Predicate.Logical
+
+type family NormLogi p where
+    NormLogi (Not (Not p)) = Just p
+    NormLogi (Or   l l)    = Just l
+    NormLogi (And  l l)    = Just l
+    NormLogi (Nand l l)    = Just (Not l)
+    NormLogi p             = Nothing
diff --git a/src/Rerefined/Predicate/Normalize.hs b/src/Rerefined/Predicate/Normalize.hs
new file mode 100644
--- /dev/null
+++ b/src/Rerefined/Predicate/Normalize.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+module Rerefined.Predicate.Normalize where
+
+import Rerefined.Predicate.Logical.Normalize
+
+type family Norm p where
+    Norm p = Norm' p (NormLogi p)
+
+type family Norm' p mp where
+    Norm' p Nothing   = p
+    Norm' p (Just p') = Norm p'
diff --git a/src/Rerefined/Predicates/Operators.hs b/src/Rerefined/Predicates/Operators.hs
new file mode 100644
--- /dev/null
+++ b/src/Rerefined/Predicates/Operators.hs
@@ -0,0 +1,67 @@
+{- | Predicate re-exports using operators.
+
+We stick with non-operators for base predicate definitions because, very simply,
+there aren't enough symbols to go around. The operators we would want to use for
+logical predicates are already being used on the term level, and I forsee a
+future full of promoted functions, so I wouldn't want to take up the type-level
+name.
+
+Instead, I'm providing operators in separate modules. It's not ideal, because
+predicates already have operators defined in their pretty printing, and they may
+not coincide with available Haskell symbols. I'm not really sure how to do all
+this, it's very tentative for now.
+-}
+
+module Rerefined.Predicates.Operators
+  (
+  -- * Logical
+  -- $logical
+    type (.&&), type (.||)
+  , type (.<->), type (.->)
+  , type (.!&), type (.!|)
+  , type (.!), type (.!=)
+
+  -- * Relational
+  , type (.<), type (.<=), type (.==), type (./=), type (.>=), type (.>)
+  ) where
+
+import Rerefined.Predicate.Logical
+import Rerefined.Predicate.Relational.Internal
+
+{- $logical
+
+Awkward mix of Boolean and propositional operators. Sorry. Let me know if you
+have a better idea.
+-}
+
+infixr 3 .&&
+type (.&&) = And
+
+infixr 2 .||
+type (.||) = Or
+
+infixr 3 .!&
+type (.!&) = Nand
+
+infix 9 .!
+type (.!) = Not
+
+infixr 2 .!|
+type (.!|) = Nor
+
+infixr 4 .!=
+type (.!=) = Xor
+
+infixr 4 .<->
+type (.<->) = Iff
+
+infixr 4 .->
+type (.->) = If
+
+infix 4 .<, .<=, .==, ./=, .>=, .>
+type (.<)  = LT
+type (.<=) = LTE
+type (.==) =  EQ
+type (./=) = NEQ
+type (.>=) = GTE
+type (.>)  = GT
diff --git a/src/Rerefined/Refine.hs b/src/Rerefined/Refine.hs
--- a/src/Rerefined/Refine.hs
+++ b/src/Rerefined/Refine.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE AllowAmbiguousTypes #-} -- for predicate reification
 {-# LANGUAGE UndecidableInstances #-} -- for KnownPredicateName in Arbitrary