diff --git a/CHANGELOG.markdown b/CHANGELOG.markdown
index 961d6bff6..b01a6d0b6 100644
--- a/CHANGELOG.markdown
+++ b/CHANGELOG.markdown
@@ -31,6 +31,11 @@
 * Make `magnify` offer its getter argument the `Contravariant` and `Functor`
   instances it will require. This allows `magnify` to be used without
   knowing the concrete monad being magnified.
+* Add `equality`, `equality'`, `withEquality`, `underEquality`, `overEquality`,
+  `fromLeibniz`, `fromLeibniz'` and `cloneEquality` to `Control.Lens.Equality`.
+* Add `withLens` to `Control.Lens.Lens`.
+* Make `substEq` and `simply` in `Control.Lens.Equality`
+  and `withIso` in `Control.Lens.Iso` levity polymorphic.
 
 4.17.1 [2019.04.26]
 -------------------
diff --git a/lens.cabal b/lens.cabal
index aab7d9572..bef03724d 100644
--- a/lens.cabal
+++ b/lens.cabal
@@ -257,6 +257,7 @@ library
     Control.Lens.Internal.Context
     Control.Lens.Internal.CTypes
     Control.Lens.Internal.Deque
+    Control.Lens.Internal.Equality
     Control.Lens.Internal.Exception
     Control.Lens.Internal.FieldTH
     Control.Lens.Internal.PrismTH
diff --git a/src/Control/Lens/Equality.hs b/src/Control/Lens/Equality.hs
index d3f836aff..5dcd6c1be 100644
--- a/src/Control/Lens/Equality.hs
+++ b/src/Control/Lens/Equality.hs
@@ -2,9 +2,14 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE Rank2Types #-}
 {-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
 #if __GLASGOW_HASKELL__ >= 706
 {-# LANGUAGE PolyKinds #-}
 #endif
+#if __GLASGOW_HASKELL__ >= 800
+{-# LANGUAGE TypeInType #-}
+#endif
+
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Control.Lens.Equality
@@ -20,6 +25,7 @@ module Control.Lens.Equality
   -- * Type Equality
     Equality, Equality'
   , AnEquality, AnEquality'
+  , (:~:)(..)
   , runEq
   , substEq
   , mapEq
@@ -27,12 +33,26 @@ module Control.Lens.Equality
   , simply
   -- * The Trivial Equality
   , simple
+  -- * 'Iso'-like functions
+  , equality
+  , equality'
+  , withEquality
+  , underEquality
+  , overEquality
+  , fromLeibniz
+  , fromLeibniz'
+  , cloneEquality
   -- * Implementation Details
   , Identical(..)
   ) where
 
 import Control.Lens.Type
 import Data.Proxy (Proxy)
+import Control.Lens.Internal.Equality ((:~:)(..))
+#if __GLASGOW_HASKELL__ >= 800
+import GHC.Exts (TYPE)
+import Data.Kind (Type)
+#endif
 
 #ifdef HLINT
 {-# ANN module "HLint: ignore Use id" #-}
@@ -68,14 +88,21 @@ runEq l = case l Identical of Identical -> Identical
 {-# INLINE runEq #-}
 
 -- | Substituting types with 'Equality'.
+#if __GLASGOW_HASKELL__ >= 800
+substEq :: forall s t a b rep (r :: TYPE rep).
+           AnEquality s t a b -> ((s ~ a, t ~ b) => r) -> r
+#else
 substEq :: AnEquality s t a b -> ((s ~ a, t ~ b) => r) -> r
+#endif
 substEq l = case runEq l of
   Identical -> \r -> r
 {-# INLINE substEq #-}
 
 -- | We can use 'Equality' to do substitution into anything.
-#if __GLASGOW_HASKELL__ >= 706
-mapEq :: forall KVS(k1 k2) (s :: k1) (t :: k2) (a :: k1) (b :: k2) (f :: k1 -> *) . AnEquality s t a b -> f s -> f a
+#if __GLASGOW_HASKELL__ >= 800
+mapEq :: forall k1 k2 (s :: k1) (t :: k2) (a :: k1) (b :: k2) (f :: k1 -> Type) . AnEquality s t a b -> f s -> f a
+#elif __GLASGOW_HASKELL__ >= 706
+mapEq :: forall (s :: k1) (t :: k2) (a :: k1) (b :: k2) (f :: k1 -> *) . AnEquality s t a b -> f s -> f a
 #else
 mapEq :: AnEquality s t a b -> f s -> f a
 #endif
@@ -89,7 +116,12 @@ fromEq l = substEq l id
 
 -- | This is an adverb that can be used to modify many other 'Lens' combinators to make them require
 -- simple lenses, simple traversals, simple prisms or simple isos as input.
+#if __GLASGOW_HASKELL__ >= 800
+simply :: forall p f s a rep (r :: TYPE rep).
+  (Optic' p f s a -> r) -> Optic' p f s a -> r
+#else
 simply :: (Optic' p f s a -> r) -> Optic' p f s a -> r
+#endif
 simply = id
 {-# INLINE simply #-}
 
@@ -100,3 +132,60 @@ simply = id
 simple :: Equality' a a
 simple = id
 {-# INLINE simple #-}
+
+cloneEquality :: AnEquality s t a b -> Equality s t a b
+cloneEquality an = substEq an id
+{-# INLINE cloneEquality #-}
+
+-- | Construct an 'Equality' from explicit equality evidence.
+equality :: s :~: a -> b :~: t -> Equality s t a b
+equality Refl Refl = id
+{-# INLINE equality #-}
+
+-- | A 'Simple' version of 'equality'
+equality' :: a :~: b -> Equality' a b
+equality' Refl = id
+{-# INLINE equality' #-}
+
+-- | Recover a "profunctor lens" form of equality. Reverses 'fromLeibniz'.
+overEquality :: AnEquality s t a b -> p a b -> p s t
+overEquality an = substEq an id
+{-# INLINE overEquality #-}
+
+-- | The opposite of working 'overEquality' is working 'underEquality'.
+underEquality :: AnEquality s t a b -> p t s -> p b a
+underEquality an = substEq an id
+{-# INLINE underEquality #-}
+
+-- | Convert a "profunctor lens" form of equality to an equality. Reverses
+-- 'overEquality'.
+--
+-- The type should be understood as
+--
+-- @fromLeibniz :: (forall p. p a b -> p s t) -> Equality s t a b@
+fromLeibniz :: (Identical a b a b -> Identical a b s t) -> Equality s t a b
+fromLeibniz f = case f Identical of Identical -> id
+{-# INLINE fromLeibniz #-}
+
+-- | Convert Leibniz equality to equality. Reverses 'mapEq' in 'Simple' cases.
+--
+-- The type should be understood as
+--
+-- @fromLeibniz' :: (forall f. f s -> f a) -> Equality' s a@
+fromLeibniz' :: (s :~: s -> s :~: a) -> Equality' s a
+-- Note: even though its type signature mentions (:~:), this function works just
+-- fine in base versions before 4.7.0; it just requires a polymorphic argument!
+fromLeibniz' f = case f Refl of Refl -> id
+{-# INLINE fromLeibniz' #-}
+
+-- | A version of 'substEq' that provides explicit, rather than implicit,
+-- equality evidence.
+#if __GLASGOW_HASKELL__ >= 800
+withEquality :: forall s t a b rep (r :: TYPE rep).
+   AnEquality s t a b -> (s :~: a -> b :~: t -> r) -> r
+#else
+withEquality :: forall s t a b r.
+   AnEquality s t a b -> (s :~: a -> b :~: t -> r) -> r
+#endif
+withEquality an = substEq an (\f -> f Refl Refl)
+{-# INLINE withEquality #-}
diff --git a/src/Control/Lens/Internal/Equality.hs b/src/Control/Lens/Internal/Equality.hs
new file mode 100644
index 000000000..f84b1ae23
--- /dev/null
+++ b/src/Control/Lens/Internal/Equality.hs
@@ -0,0 +1,87 @@
+{-# language CPP #-}
+{-# language GADTs #-}
+{-# language RankNTypes #-}
+{-# language StandaloneDeriving #-}
+{-# language TypeOperators #-}
+#if __GLASGOW_HASKELL__ >= 706
+-- PolyKinds is known to be especially flaky in 7.4. It didn't get *really*
+-- solid until 8.0 or, but it's somewhat usable from 7.6 to 7.10.
+{-# language PolyKinds #-}
+#endif
+module Control.Lens.Internal.Equality (
+    (:~:)(..)
+  , sym
+  , trans
+  , castWith
+  , gcastWith
+  , eqT
+
+{-
+We can't define 'apply' or 'outer' for 7.4, since they won't kind-check without
+PolyKinds. We're not currently using them anyway.
+
+'inner' won't typecheck with 7.4 or 7.6, apparently due to GHC bugs.  There
+may be a workaround available if we need it:
+
+  https://github.com/ekmett/lens/pull/862#discussion_r307945760
+-}
+  ) where
+#if MIN_VERSION_base (4,7,0)
+import Data.Type.Equality
+import Data.Typeable (eqT)
+
+#else
+
+import Control.Category
+import Data.Typeable (Typeable, gcast)
+import Prelude hiding (id, (.))
+
+infix 4 :~:
+
+-- | Propositional equality. If @a :~: b@ is inhabited by some terminating
+-- value, then the type @a@ is the same as the type @b@. To use this equality
+-- in practice, pattern-match on the @a :~: b@ to get out the @Refl@ constructor;
+-- in the body of the pattern-match, the compiler knows that @a ~ b@.
+data a :~: b where
+  Refl :: a :~: a
+
+instance Category (:~:) where
+  id = Refl
+  Refl . Refl = Refl
+
+-- | Symmetry of equality
+sym :: (a :~: b) -> (b :~: a)
+sym Refl = Refl
+
+-- | Transitivity of equality
+trans :: (a :~: b) -> (b :~: c) -> (a :~: c)
+trans Refl Refl = Refl
+
+-- | Type-safe cast, using propositional equality
+castWith :: (a :~: b) -> a -> b
+castWith Refl x = x
+
+-- | Generalized form of type-safe cast using propositional equality
+gcastWith :: (a :~: b) -> ((a ~ b) => r) -> r
+gcastWith Refl x = x
+
+deriving instance Eq   (a :~: b)
+deriving instance Ord  (a :~: b)
+deriving instance Show (a :~: b)
+deriving instance a ~ b => Read (a :~: b)
+
+-- This can't be derived until 7.8, when we don't need it anymore.
+instance a ~ b => Bounded (a :~: b) where
+  minBound = Refl
+  maxBound = Refl
+
+instance a ~ b => Enum (a :~: b) where
+  toEnum 0 = Refl
+  toEnum _ = error "Control.Lens.Internal.Equality toEnum: bad argument"
+
+  fromEnum Refl = 0
+
+-- | Extract a witness of equality of two types
+eqT :: (Typeable a, Typeable b) => Maybe (a :~: b)
+eqT = gcast Refl
+#endif
diff --git a/src/Control/Lens/Iso.hs b/src/Control/Lens/Iso.hs
index c633f6612..213ef8c7d 100644
--- a/src/Control/Lens/Iso.hs
+++ b/src/Control/Lens/Iso.hs
@@ -10,6 +10,10 @@
 {-# LANGUAGE Trustworthy #-}
 #endif
 
+#if __GLASGOW_HASKELL__ >= 800
+{-# LANGUAGE TypeInType #-}
+#endif
+
 #ifndef MIN_VERSION_bytestring
 #define MIN_VERSION_bytestring(x,y,z) 1
 #endif
@@ -140,6 +144,10 @@ import Data.Type.Coercion
 import qualified GHC.Exts as Exts
 #endif
 
+#if __GLASGOW_HASKELL__ >= 800
+import GHC.Exts (TYPE)
+#endif
+
 #ifdef HLINT
 {-# ANN module "HLint: ignore Use on" #-}
 #endif
@@ -189,7 +197,12 @@ from l = withIso l $ flip iso
 
 -- | Extract the two functions, one from @s -> a@ and
 -- one from @b -> t@ that characterize an 'Iso'.
+#if __GLASGOW_HASKELL__ >= 800
+withIso :: forall s t a b rep (r :: TYPE rep).
+             AnIso s t a b -> ((s -> a) -> (b -> t) -> r) -> r
+#else
 withIso :: AnIso s t a b -> ((s -> a) -> (b -> t) -> r) -> r
+#endif
 withIso ai k = case ai (Exchange id Identity) of
   Exchange sa bt -> k sa (runIdentity #. bt)
 {-# INLINE withIso #-}
diff --git a/src/Control/Lens/Lens.hs b/src/Control/Lens/Lens.hs
index 188067369..d6957157c 100644
--- a/src/Control/Lens/Lens.hs
+++ b/src/Control/Lens/Lens.hs
@@ -6,6 +6,9 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE Trustworthy #-}
+#if __GLASGOW_HASKELL__ >= 800
+{-# LANGUAGE TypeInType #-}
+#endif
 
 #ifndef MIN_VERSION_mtl
 #define MIN_VERSION_mtl(x,y,z) 1
@@ -70,7 +73,7 @@ module Control.Lens.Lens
   , AnIndexedLens, AnIndexedLens'
 
   -- * Combinators
-  , lens, ilens, iplens
+  , lens, ilens, iplens, withLens
   , (%%~), (%%=)
   , (%%@~), (%%@=)
   , (<%@~), (<%@=)
@@ -154,6 +157,10 @@ import Data.Function ((&))
 #if MIN_VERSION_base(4,11,0)
 import Data.Functor ((<&>))
 #endif
+#if __GLASGOW_HASKELL__ >= 800
+import GHC.Exts (TYPE)
+import Data.Kind -- For *
+#endif
 
 #ifdef HLINT
 {-# ANN module "HLint: ignore Use ***" #-}
@@ -232,6 +239,16 @@ lens :: (s -> a) -> (s -> b -> t) -> Lens s t a b
 lens sa sbt afb s = sbt s <$> afb (sa s)
 {-# INLINE lens #-}
 
+-- | Obtain a getter and a setter from a lens, reversing 'lens'.
+#if __GLASGOW_HASKELL__ >= 800
+withLens :: forall s t a b rep (r :: TYPE rep).
+            ALens s t a b -> ((s -> a) -> (s -> b -> t) -> r) -> r
+#else
+withLens :: ALens s t a b -> ((s -> a) -> (s -> b -> t) -> r) -> r
+#endif
+withLens l f = f (^# l) (flip (storing l))
+{-# INLINE withLens #-}
+
 -- | Build an index-preserving 'Lens' from a 'Control.Lens.Getter.Getter' and a
 -- 'Control.Lens.Setter.Setter'.
 iplens :: (s -> a) -> (s -> b -> t) -> IndexPreservingLens s t a b
diff --git a/src/Data/Data/Lens.hs b/src/Data/Data/Lens.hs
index 0e174d27a..f38708fb7 100644
--- a/src/Data/Data/Lens.hs
+++ b/src/Data/Data/Lens.hs
@@ -5,6 +5,7 @@
 {-# LANGUAGE UnboxedTuples #-}
 #endif
 {-# LANGUAGE PatternGuards #-}
+{-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE ScopedTypeVariables #-}
@@ -48,6 +49,7 @@ module Data.Data.Lens
 import           Control.Applicative
 import           Control.Exception as E
 import           Control.Lens.Internal.Context
+import           Control.Lens.Internal.Equality ((:~:)(..), eqT)
 import           Control.Lens.Internal.Indexed
 import           Control.Lens.Lens
 import           Control.Lens.Setter
@@ -102,8 +104,8 @@ tinplate f = gfoldl (step f) pure
 {-# INLINE tinplate #-}
 
 step :: forall s a f r. (Applicative f, Typeable a, Data s) => (a -> f a) -> f (s -> r) -> s -> f r
-step f w s = w <*> case mightBe :: Maybe (Is s a) of
-  Just Data.Data.Lens.Refl -> f s
+step f w s = w <*> case eqT :: Maybe (s :~: a) of
+  Just Refl -> f s
   Nothing   -> tinplate f s
 {-# INLINE step #-}
 
@@ -262,17 +264,6 @@ onceUpon' field f s = k <$> indexed f i (field s) where
   ~(i, Context k _) = fromMaybe (error "upon': no index, not a member") (lookupon template field s)
 {-# INLINE onceUpon' #-}
 
--------------------------------------------------------------------------------
--- Type equality
--------------------------------------------------------------------------------
-
-data Is a b where
-  Refl :: Is a a
-
-mightBe :: (Typeable a, Typeable b) => Maybe (Is a b)
-mightBe = gcast Data.Data.Lens.Refl
-{-# INLINE mightBe #-}
-
 -------------------------------------------------------------------------------
 -- Data Box
 -------------------------------------------------------------------------------
@@ -389,8 +380,8 @@ newtype Oracle a = Oracle { fromOracle :: forall t. Typeable t => t -> Answer t
 
 hitTest :: forall a b. (Data a, Typeable b) => a -> b -> Oracle b
 hitTest a b = Oracle $ \(c :: c) ->
-  case mightBe :: Maybe (Is c b) of
-    Just Data.Data.Lens.Refl -> Hit c
+  case eqT :: Maybe (c :~: b) of
+    Just Refl -> Hit c
     Nothing ->
       case readCacheFollower (dataBox a) (typeOf b) of
         Just p | not (p (typeOf c)) -> Miss