diff --git a/src/1Lab/Path.lagda.md b/src/1Lab/Path.lagda.md
index 1b8d31fcf..ad6f42ca9 100644
--- a/src/1Lab/Path.lagda.md
+++ b/src/1Lab/Path.lagda.md
@@ -557,7 +557,7 @@ Thus, the definition of `J`{.Agda}: `transport`{.Agda} +
 ```agda
 J : ∀ {ℓ₁ ℓ₂} {A : Type ℓ₁} {x : A}
     (P : (y : A) → x ≡ y → Type ℓ₂)
-  → P x refl
+  → P x (λ _ → x)
   → {y : A} (p : x ≡ y)
   → P y p
 J {x = x} P prefl {y} p = transport (λ i → P (path i .fst) (path i .snd)) prefl where
diff --git a/src/1Lab/Prelude.agda b/src/1Lab/Prelude.agda
index fbbfb63ac..d133c2dd0 100644
--- a/src/1Lab/Prelude.agda
+++ b/src/1Lab/Prelude.agda
@@ -34,3 +34,4 @@ open import 1Lab.Reflection.Marker public
 open import 1Lab.Reflection.Record
   using ( declare-record-iso ) public
 open import 1Lab.Reflection.HLevel public
+open import 1Lab.Reflection.Regularity public
diff --git a/src/1Lab/Prim/Monad.lagda.md b/src/1Lab/Prim/Monad.lagda.md
index 32017ad36..4bd242271 100644
--- a/src/1Lab/Prim/Monad.lagda.md
+++ b/src/1Lab/Prim/Monad.lagda.md
@@ -15,6 +15,9 @@ record
   _>>_ : ∀ {ℓ ℓ′} {A : Type ℓ} {B : Type ℓ′} → M A → M B → M B
   _>>_ f g = f >>= λ _ → g
 
+  _=<<_ : ∀ {ℓ ℓ′} {A : Type ℓ} {B : Type ℓ′} → (A → M B) → M A → M B
+  _=<<_ f x = x >>= f
+
 open Do-syntax ⦃ ... ⦄ public
 
 record Idiom-syntax (f : Level → Level) (M : ∀ {ℓ} → Type ℓ → Type (f ℓ)) : Typeω where
diff --git a/src/1Lab/Reflection.lagda.md b/src/1Lab/Reflection.lagda.md
index 4cc557b54..f7389953d 100644
--- a/src/1Lab/Reflection.lagda.md
+++ b/src/1Lab/Reflection.lagda.md
@@ -572,15 +572,50 @@ _ term=? _ = false
 “refl” : Term
 “refl” = def (quote refl) []
 
+wait-for-args : List (Arg Term) → TC (List (Arg Term))
 wait-for-type : Term → TC Term
-wait-for-type (meta m _) = blockOnMeta m
-wait-for-type tm = pure tm
+
+wait-for-type (var x args) = var x <$> wait-for-args args
+wait-for-type (con c args) = con c <$> wait-for-args args
+wait-for-type (def f args) = def f <$> wait-for-args args
+wait-for-type (lam v (abs x t)) = pure (lam v (abs x t))
+wait-for-type (pat-lam cs args) = pure (pat-lam cs args)
+wait-for-type (pi (arg i a) (abs x b)) = do
+  a ← wait-for-type a
+  b ← wait-for-type b
+  pure (pi (arg i a) (abs x b))
+wait-for-type (agda-sort s) = pure (agda-sort s)
+wait-for-type (lit l) = pure (lit l)
+wait-for-type (meta x x₁) = blockOnMeta x
+wait-for-type unknown = pure unknown
+
+wait-for-args [] = pure []
+wait-for-args (arg i a ∷ xs) = ⦇ ⦇ (arg i) (wait-for-type a) ⦈ ∷ wait-for-args xs ⦈
+
+wait-just-a-bit : Term → TC Term
+wait-just-a-bit (meta m _) = blockOnMeta m
+wait-just-a-bit tm = pure tm
 
 unapply-path : Term → TC (Maybe (Term × Term × Term))
-unapply-path tm = (reduce tm >>= wait-for-type) >>= λ where
+unapply-path red@(def (quote PathP) (l h∷ T v∷ x v∷ y v∷ [])) = do
+  domain ← newMeta (def (quote Type) (l v∷ []))
+  ty ← pure (def (quote Path) (domain v∷ x v∷ y v∷ []))
+  debugPrint "tactic" 50 $ "(no reduction) got a " ∷ termErr red ∷ " but I really want it to be " ∷ termErr ty ∷ []
+  unify red ty
+  pure (just (domain , x , y))
+unapply-path tm = reduce tm >>= λ where
+  tm@(meta _ _) → do
+    dom ← newMeta (def (quote Type) [])
+    l ← newMeta dom
+    r ← newMeta dom
+    unify tm (def (quote Type) (dom v∷ l v∷ r v∷ []))
+    traverse (l ∷ r ∷ []) wait-for-type
+    pure (just (dom , l , r))
   red@(def (quote PathP) (l h∷ T v∷ x v∷ y v∷ [])) → do
     domain ← newMeta (def (quote Type) (l v∷ []))
-    unify red (def (quote Path) (domain v∷ x v∷ y v∷ []))
+    ty ← pure (def (quote Path) (domain v∷ x v∷ y v∷ []))
+    debugPrint "tactic" 50 $ "got a " ∷ termErr red ∷ " but I really want it to be " ∷ termErr ty ∷ []
+    unify red ty
     pure (just (domain , x , y))
   _ → returnTC nothing
 
@@ -630,4 +665,13 @@ print-depth key level nesting es = debugPrint key level $
     nest : Nat → String → String
     nest zero s = s
     nest (suc x) s = nest x (s <> "  ")
+
+argH : ∀ {ℓ} {A : Type ℓ} → A → Arg A
+argH = arg (arginfo hidden (modality relevant quantity-ω))
+
+argH0 : ∀ {ℓ} {A : Type ℓ} → A → Arg A
+argH0 = arg (arginfo hidden (modality relevant quantity-0))
+
+argN : ∀ {ℓ} {A : Type ℓ} → A → Arg A
+argN = arg (arginfo visible (modality relevant quantity-ω))
 ```
diff --git a/src/1Lab/Reflection/HLevel.agda b/src/1Lab/Reflection/HLevel.agda
index 18f8a8da2..3a965ab24 100644
--- a/src/1Lab/Reflection/HLevel.agda
+++ b/src/1Lab/Reflection/HLevel.agda
@@ -168,15 +168,15 @@ private
       where
         -- Handle the ones with special names:
         def (quote is-set) (_ ∷ ty v∷ []) → do
-          ty ← wait-for-type ty
+          ty ← wait-just-a-bit ty
           pure (ty , quoteTerm 2)
 
         def (quote is-prop) (_ ∷ ty v∷ []) → do
-          ty ← wait-for-type ty
+          ty ← wait-just-a-bit ty
           pure (ty , quoteTerm 1)
 
         def (quote is-contr) (_ ∷ ty v∷ []) → do
-          ty ← wait-for-type ty
+          ty ← wait-just-a-bit ty
           pure (ty , quoteTerm 0)
 
         _ → backtrack "Goal type isn't is-hlevel"
@@ -185,8 +185,8 @@ private
     -- block decomposition on having a rigid-ish type at the
     -- top-level. Otherwise the first hint that matches will get
     -- matched endlessly until we run out of fuel!
-    ty ← wait-for-type ty
-    lv ← wait-for-type lv
+    ty ← wait-just-a-bit ty
+    lv ← wait-just-a-bit lv
     pure (ty , lv)
 
 {-
@@ -330,6 +330,7 @@ from the wanted level (k + n) until is-hlevel-+ n (sucᵏ′ n) w works.
     use-projections
       <|> use-hints
       <|> use-instance-search has-alts goal
+      <|> typeError "Search failed!!"
     where
       open hlevel-projection
 
@@ -546,7 +547,7 @@ from the wanted level (k + n) until is-hlevel-+ n (sucᵏ′ n) w works.
     → Term → TC (Term × Term × (TC A → TC A) × (Term → Term))
   decompose-is-hlevel-top goal =
     do
-      ty ← dontReduceDefs hlevel-types $ (inferType goal >>= reduce) >>= wait-for-type
+      ty ← dontReduceDefs hlevel-types $ (inferType goal >>= reduce) >>= wait-just-a-bit
       go ty
     where
       go : Term → TC _
@@ -606,6 +607,13 @@ prop-ext! {aprop = aprop} {bprop = bprop} = prop-ext aprop bprop
   → x ≡ y
 Σ-prop-path! {bxprop = bxprop} = Σ-prop-path bxprop
 
+prop!
+  : ∀ {ℓ} {A : I → Type ℓ} {@(tactic hlevel-tactic-worker) aip : is-hlevel (A i0) 1}
+  → {x : A i0} {y : A i1}
+  → PathP (λ i → A i) x y
+prop! {A = A} {aip = aip} {x} {y} =
+  is-prop→pathp (λ i → coe (λ j → is-prop (A j)) i0 i aip) x y
+
 open hlevel-projection
 
 -- Hint database bootstrap
diff --git a/src/1Lab/Reflection/Regularity.agda b/src/1Lab/Reflection/Regularity.agda
new file mode 100644
index 000000000..8e4151a0c
--- /dev/null
+++ b/src/1Lab/Reflection/Regularity.agda
@@ -0,0 +1,219 @@
+{-# OPTIONS --allow-unsolved-metas #-}
+open import 1Lab.Reflection.HLevel
+open import 1Lab.Reflection.Subst
+open import 1Lab.Reflection
+open import 1Lab.Path
+open import 1Lab.Type
+
+module 1Lab.Reflection.Regularity where
+
+{-
+A tactic for reducing "transport refl x" in other-wise normal terms. The
+implementation is actually surprisingly simple: A term of the form (e.g.)
+
+    transport refl (f (transport refl x))
+
+is already a blueprint for how to normalise it. We simply have to turn it into
+
+    λ i → transport-refl (f (transport-refl x i)) i
+
+The implementation presents itself: Raise the original term, and look
+through to find reflexive transports. These can be replaced by an
+application of transport-refl.
+-}
+
+private
+  -- Ahem, not transport-refl, but a tiny tiny wrapper around it. The
+  -- reason we have 'regular' is to mark terms we're *leaving*: The
+  -- translation proceeds inside out, so to have a way to stop, we mark
+  -- terms we have already visited entirely using `regular`.
+  regular : ∀ {ℓ} {A : Type ℓ} (x : A) → transport refl x ≡ x
+  regular x = transport-refl x
+
+  -- And we have a double composition operator that doesn't use the
+  -- fancy hcomp syntax in its definition. This has better type
+  -- inference for one of the macros since it guarantees that the base
+  -- (q i) is independent of j without any reduction.
+  double-comp
+    : ∀ {ℓ} {A : Type ℓ} {w z : A} (x y : A)
+    → w ≡ x → x ≡ y → y ≡ z
+    → w ≡ z
+  double-comp x y p q r i = primHComp
+    (λ { j (i = i0) → p (~ j) ; j (i = i1) → r j }) (q i)
+
+  -- The regularity tactic can operate in two modes: `precise` will work
+  -- with the type-checker to identify which `transp`s are along refl,
+  -- and which should be preserved. The `fast` mode says YOLO and
+  -- assumes that **every** application of `transp` is one that would
+  -- reduce by regularity. Needless to say, only use `fast` when you're
+  -- sure that's the case (e.g. the fibres of a displayed category over
+  -- Sets)
+  data Regularity-precision : Type where
+    precise fast : Regularity-precision
+  -- As the name implies, `precise` is `precise`, while `fast` is
+  -- `fast`. The reason is that `fast` will avoid traversing many of the
+  -- terms involved in a `transp`: It doesn't care about the level, it
+  -- doesn't care about the line, and it doesn't care about the
+  -- cofibration.
+
+  -- The core of the tactic is this triad of mutually recursive
+  -- functions. In all three of them, the `Nat` argument indicates how
+  -- many binders we've gone under: it is the dimension variable we
+  -- abstracted over at the start.
+  refl-transport : Nat → Term → TC Term
+  -- ^ Determines whether an application of `transp` is a case of
+  -- regularity, and if so, replaces it by `regular`. Precondition: its
+  -- subterms must already be reduced.
+  go  : Regularity-precision → Nat → Term → TC Term
+  -- ^ Reduces all the subterms, and finds applications of `transp` to
+  -- hand off to `refl-transport`.
+  go* : Regularity-precision → Nat → List (Arg Term) → TC (List (Arg Term))
+  -- ^ Isn't the termination checker just lovely?
+
+  refl-transport n tm′@(def (quote transp) (ℓ h∷ Al v∷ phi v∷ x v∷ [])) =
+    -- This match might make you wonder: Can't Al be a line of
+    -- functions, so that the transport will have more arguments? No:
+    -- The term is in normal form.
+    (do
+      -- The way we check for regularity is simple: The line must have
+      -- been reduced to an abstraction, and it must unify with refl. We
+      -- use backtracking to fall back to the case where the transport
+      -- was legitimately interesting!
+      debugPrint "tactic.regularity:" 10 $ "Checking regularity of " ∷ termErr Al ∷ []
+      lam visible (abs v Ab) ← pure Al
+        where _ → typeError []
+      unify-loudly Al (def (quote refl) [])
+      unify phi (con (quote i0) [])
+      let tm′ = def (quote regular) (x v∷ var n [] v∷ [])
+      pure tm′) <|>
+    (do
+      debugPrint "tactic.regularity" 10 $ "NOT a (transport refl): " ∷ termErr tm′ ∷ []
+      pure tm′)
+  refl-transport _ tm′ = pure tm′
+
+  -- Boring term traversal.
+  go pre n (var x args) = var x <$> go* pre n args
+  go pre n (con c args) = con c <$> go* pre n args
+  go fast n (def (quote transp) (_ ∷ _ ∷ _ ∷ x v∷ [])) = do
+    x ← go fast n x
+    pure $ def (quote regular) (x v∷ var n [] v∷ [])
+  go pre n (def f args) = do
+    as ← go* pre n args
+    refl-transport n (def f as)
+  go pre k (lam v (abs n b)) = lam v ∘ abs n <$> go pre (suc k) b
+  go pre n (pat-lam cs args) = typeError $ "regularity: Can not deal with pattern lambdas"
+  go pre n (pi (arg i a) (abs nm b)) = do
+    a ← go pre n a
+    b ← go pre (suc n) b
+    pure (pi (arg i a) (abs nm b))
+  go pre n (agda-sort s) = pure (agda-sort s)
+  go pre n (lit l) = pure (lit l)
+  go pre n (meta x args) = meta x <$> go* pre n args
+  go pre n unknown = pure unknown
+
+  go* pre n [] = pure []
+  go* pre n (arg i a ∷ as) = do
+    a ← go pre n a
+    (arg i a ∷_) <$> go* pre n as
+
+  -- To turn a term into a regularity path, given a level of precision,
+  -- all we have to do is raise the term by one, do the procedure above,
+  -- then wrap it in a lambda. Nice!
+  to-regularity-path : Regularity-precision → Term → TC Term
+  to-regularity-path pre tm = do
+    tm ← raise 1 tm
+    -- Since we'll be comparing terms, Agda really wants them to be
+    -- well-scoped. Since we shifted eeeverything up by one, we have to
+    -- grow the context, too.
+    tm ← runSpeculative $ extendContext "i" (argN (quoteTerm I)) do
+      tm ← go pre 0 tm
+      pure (tm , false)
+    pure $ lam visible $ abs "i" $ tm
+
+  -- Extend a path x ≡ y to a path x′ ≡ y′, where x′ --> x and y′ --> y
+  -- under the given regularity precision. Shorthand for composing
+  --    regularity! ∙ p ∙ sym regularity!.
+  regular!-worker :
+    ∀ {ℓ} {A : Type ℓ} {x y : A}
+    → Regularity-precision
+    → x ≡ y
+    → Term
+    → TC ⊤
+  regular!-worker {x = x} {y} pre p goal = do
+    gt ← inferType goal
+    `x ← quoteTC x
+    `y ← quoteTC y
+    `p ← quoteTC p
+    just (_ , l , r) ← unapply-path =<< inferType goal
+      where _ → typeError []
+    l ← normalise =<< wait-for-type l
+    r ← normalise =<< wait-for-type r
+    reg ← to-regularity-path pre l
+    reg′ ← to-regularity-path pre r
+    unify-loudly goal $ def (quote double-comp) $
+         `x v∷ `y v∷ reg
+      v∷ `p
+      v∷ def (quote sym) (reg′ v∷ [])
+      v∷ []
+
+module Regularity where
+  open Regularity-precision public
+  -- The reflection interface: Regularity.reduce! will, well, reduce a
+  -- term. The tactic is robust enough to grow terms, if you invert the
+  -- path, as well. There's a lot of blocking involved in making this
+  -- work.
+  macro
+    reduce! : Term → TC ⊤
+    reduce! goal = do
+      just (_ , l , r) ← unapply-path =<< inferType goal
+        where _ → typeError []
+      reg ← to-regularity-path precise =<< (wait-for-type =<< normalise l)
+      unify-loudly goal reg
+
+    -- We then have wrappers that reduce on one side, and expand on the
+    -- other, depending on how precise you want the reduction to be.
+    precise! : ∀ {ℓ} {A : Type ℓ} {x y : A} → x ≡ y → Term → TC ⊤
+    fast! : ∀ {ℓ} {A : Type ℓ} {x y : A} → x ≡ y → Term → TC ⊤
+
+    precise! p goal = regular!-worker precise p goal
+    fast! p goal = regular!-worker fast p goal
+
+    -- For debugging purposes, this macro will take a term and output
+    -- its (transport refl)-normal form, according to the given level of
+    -- precision.
+    reduct : Regularity-precision → Term → Term → TC ⊤
+    reduct pres tm _ = do
+      orig ← wait-for-type =<< normalise tm
+      tm ← to-regularity-path pres orig
+      red ← apply-tm tm (argN (con (quote i1) [])) >>= normalise
+      `pres ← quoteTC pres
+      typeError $
+        "The term\n\n  " ∷ termErr orig ∷ "\n\nreduces modulo " ∷ termErr `pres ∷ " regularity to\n\n  "
+        ∷ termErr red
+        ∷ "\n"
+
+-- Test cases.
+module
+  _ {ℓ ℓ′} {A : Type ℓ} {B : Type ℓ′} (f g : A → B) (x : A)
+    (a-loop : (i : I) → Type ℓ [ (i ∨ ~ i) ↦ (λ ._ → A) ])
+  where private
+
+  p : (h : ∀ x → f x ≡ g x)
+    → transport (λ i → A → B)
+        (λ x → transport refl (transport refl (f (transport refl x)))) ≡ g
+  p h = Regularity.reduce! ∙ funext h
+
+  q : transport refl (transp (λ i → outS (a-loop i)) i0 x) ≡ transp (λ i → outS (a-loop i)) i0 x
+  q = Regularity.reduce!
+
+  -- Imprecise/fast reduction: According to it, the normal form of the
+  -- transport below is refl. That's.. not the case, at least we don't
+  -- know so. Precise regularity handles it, though.
+  q′ : ⊤
+  q′ = {! Regularity.reduct Regularity.fast (transp (λ i → outS (a-loop i)) i0 x) !}
+
+  r : (h : ∀ x → f x ≡ g x) → transport refl (f x) ≡ transport refl (g x)
+  r h = Regularity.precise! (h x)
+
+  s : (h : ∀ x → f x ≡ g x) → transport refl (g x) ≡ transport refl (f x)
+  s h = sym $ Regularity.fast! (h x)
diff --git a/src/1Lab/Reflection/Solver.agda b/src/1Lab/Reflection/Solver.agda
index c64860d01..1923d8c68 100644
--- a/src/1Lab/Reflection/Solver.agda
+++ b/src/1Lab/Reflection/Solver.agda
@@ -45,7 +45,7 @@ record SimpleSolver : Type where
     dont-reduce : List Name
     build-expr : Term → TC Term
     invoke-solver : Term → Term → Term
-    invoke-normalisier : Term → Term
+    invoke-normaliser : Term → Term
 
 module _ (solver : SimpleSolver) where
   open SimpleSolver solver
@@ -67,7 +67,7 @@ module _ (solver : SimpleSolver) where
     withNormalisation false $
     dontReduceDefs dont-reduce $ do
     e ← normalise tm >>= build-expr
-    unify hole (invoke-normalisier e)
+    unify hole (invoke-normaliser e)
 
   mk-simple-repr : Term → TC ⊤
   mk-simple-repr tm =
@@ -85,7 +85,7 @@ record VariableSolver {ℓ} (A : Type ℓ) : Type ℓ where
     dont-reduce : List Name
     build-expr : Variables A → Term → TC (Term × Variables A)
     invoke-solver : Term → Term → Term → Term
-    invoke-normalisier : Term → Term → Term
+    invoke-normaliser : Term → Term → Term
 
 module _ {ℓ} {A : Type ℓ} (solver : VariableSolver A) where
   open VariableSolver solver
@@ -113,7 +113,7 @@ module _ {ℓ} {A : Type ℓ} (solver : VariableSolver A) where
     dontReduceDefs dont-reduce $ do
     e , vs ← normalise tm >>= build-expr empty-vars
     size , env ← environment vs
-    soln ← reduce (invoke-normalisier e env)
+    soln ← reduce (invoke-normaliser e env)
     unify hole soln
 
   mk-var-repr : Term → TC ⊤
diff --git a/src/1Lab/Reflection/Subst.agda b/src/1Lab/Reflection/Subst.agda
new file mode 100644
index 000000000..6fae6bde7
--- /dev/null
+++ b/src/1Lab/Reflection/Subst.agda
@@ -0,0 +1,122 @@
+open import 1Lab.Prim.Data.Nat
+
+open import 1Lab.Reflection
+open import 1Lab.Type
+
+module 1Lab.Reflection.Subst where
+
+{-# NO_UNIVERSE_CHECK #-}
+record Impossible : Type where
+  field throw-impossible : ∀ {ℓ} {A : Type ℓ} → TC A
+
+open Impossible
+
+impossible : Impossible
+impossible .throw-impossible = typeError "The impossible happened!"
+
+data Subst : Type where
+  ids        : Subst
+  _∷_        : Term → Subst → Subst
+  wk         : Nat → Subst → Subst
+  lift       : Nat → Subst → Subst
+  strengthen : Impossible → Nat → Subst → Subst
+
+infixr 20 _∷_
+
+wkS : Nat → Subst → Subst
+wkS zero ρ = ρ
+wkS n (wk x ρ) = wk (n + x) ρ
+wkS n ρ        = wk n ρ
+
+liftS : Nat → Subst → Subst
+liftS zero ρ       = ρ
+liftS n ids        = ids
+liftS n (lift k ρ) = lift (n + k) ρ
+liftS n ρ          = lift n ρ
+
+_++#_ : List Term → Subst → Subst
+x ++# ρ = foldr (_∷_) ρ x
+infix 15 _++#_
+
+raiseS : Nat → Subst
+raiseS n = wk n ids
+
+raise-fromS : Nat → Nat → Subst
+raise-fromS n k = liftS n $ raiseS k
+
+singletonS : Nat → Term → Subst
+singletonS n u = map (λ i → var i []) (count (n - 1)) ++# u ∷ (raiseS n)
+  where
+    count : Nat → List Nat
+    count zero = []
+    count (suc n) = 1 ∷ map suc (count n)
+
+{-# TERMINATING #-}
+subst-tm  : Subst → Term → TC Term
+subst-tm* : Subst → List (Arg Term) → TC (List (Arg Term))
+apply-tm  : Term → Arg Term → TC Term
+
+raise : Nat → Term → TC Term
+raise n = subst-tm (raiseS n)
+
+subst-tm* ρ [] = pure []
+subst-tm* ρ (arg ι x ∷ ls) = do
+  x ← subst-tm ρ x
+  (arg ι x ∷_) <$> subst-tm* ρ ls
+
+apply-tm* : Term → List (Arg Term) → TC Term
+apply-tm* tm [] = pure tm
+apply-tm* tm (x ∷ xs) = do
+  tm′ ← apply-tm tm x
+  apply-tm* tm′ xs
+
+lookup-tm : (σ : Subst) (i : Nat) → TC Term
+lookup-tm ids i = pure $ var i []
+lookup-tm (wk n ids) i = pure $ var (i + n) []
+lookup-tm (wk n ρ) i = lookup-tm ρ i >>= subst-tm (raiseS n)
+lookup-tm (x ∷ ρ) i with (i == 0)
+… | true  = pure x
+… | false = lookup-tm ρ (i - 1)
+lookup-tm (strengthen err n ρ) i with (i < n)
+… | true = err .throw-impossible
+… | false = lookup-tm ρ (i - n)
+lookup-tm (lift n σ) i with (i < n)
+… | true  = pure $ var i []
+… | false = lookup-tm σ (i - n) >>= raise n
+
+apply-tm (var x args)      argu = pure $ var x (args ++ argu ∷ [])
+apply-tm (con c args)      argu = pure $ con c (args ++ argu ∷ [])
+apply-tm (def f args)      argu = pure $ def f (args ++ argu ∷ [])
+apply-tm (lam v (abs n t)) (arg _ argu) = subst-tm (argu ∷ ids) t
+apply-tm (pat-lam cs args) argu = typeError "Unsupported apply pat-lam"
+apply-tm (pi a b)          argu = typeError "Type error: apply Π to argument"
+apply-tm (agda-sort s)     argu = typeError "Type error: apply sort to argument"
+apply-tm (lit l)           argu = typeError "Type error: apply literal to argument"
+apply-tm (meta x args)     argu = pure $ meta x (args ++ argu ∷ [])
+apply-tm unknown           argu = do
+  mv ← newMeta unknown
+  apply-tm mv argu
+
+subst-tm ids tm = pure tm
+subst-tm ρ (var i args) = do
+  r ← lookup-tm ρ i
+  es ← subst-tm* ρ args
+  apply-tm* r es
+subst-tm ρ (con c args)      = con c <$> subst-tm* ρ args
+subst-tm ρ (def f args)      = def f <$> subst-tm* ρ args
+subst-tm ρ (meta x args)     = meta x <$> subst-tm* ρ args
+subst-tm ρ (pat-lam cs args) = typeError $ "Unsupported subst pat-lam"
+subst-tm ρ (lam v (abs n b)) = lam v ∘ abs n <$> subst-tm (liftS 1 ρ) b
+subst-tm ρ (pi (arg ι a) (abs n b)) = do
+  a ← subst-tm ρ a
+  b ← subst-tm (liftS 1 ρ) b
+  pure (pi (arg ι a) (abs n b))
+subst-tm ρ (lit l) = pure (lit l)
+subst-tm ρ unknown = pure unknown
+subst-tm ρ (agda-sort s) with s
+… | set t     = agda-sort ∘ set <$> subst-tm ρ t
+… | lit n     = pure (agda-sort (lit n))
+… | prop t    = agda-sort ∘ prop <$> subst-tm ρ t
+… | propLit n = pure (agda-sort (propLit n))
+… | inf n     = pure (agda-sort (inf n))
+… | unknown   = pure unknown
diff --git a/src/1Lab/Type/Sigma.lagda.md b/src/1Lab/Type/Sigma.lagda.md
index 0232dedb0..420e690bb 100644
--- a/src/1Lab/Type/Sigma.lagda.md
+++ b/src/1Lab/Type/Sigma.lagda.md
@@ -246,6 +246,9 @@ If `B` is a family of contractible types, then `Σ B ≃ A`:
   → PathP (λ i → Σ (A i) (B i)) x y
 Σ-pathp-dep p q i = p i , q i
 
+_,ₚ_ = Σ-pathp-dep
+infixr 4 _,ₚ_
+
 Σ-prop-pathp
   : ∀ {ℓ ℓ′} {A : I → Type ℓ} {B : ∀ i → A i → Type ℓ′}
   → (∀ i x → is-prop (B i x))
diff --git a/src/Algebra/Group.lagda.md b/src/Algebra/Group.lagda.md
index 63ba30c9c..2c3b23ee3 100644
--- a/src/Algebra/Group.lagda.md
+++ b/src/Algebra/Group.lagda.md
@@ -107,21 +107,21 @@ private unquoteDecl eqv = declare-record-iso eqv (quote is-group)
 
 is-group-is-prop : ∀ {ℓ} {A : Type ℓ} {_*_ : A → A → A}
                  → is-prop (is-group _*_)
-is-group-is-prop {A = A} x =
-  Iso→is-hlevel 1 eqv hl x
+is-group-is-prop {A = A} x y = Equiv.injective (Iso→Equiv eqv) $
+     1x=1y
+  ,ₚ funext (λ a →
+      monoid-inverse-unique x.has-is-monoid a _ _
+        x.inversel
+        (y.inverser ∙ sym 1x=1y))
+  ,ₚ prop!
   where
-    instance
-      A-hl : ∀ {n} → H-Level A (2 + n)
-      A-hl = basic-instance {T = A} 2 (x .is-group.has-is-set)
-    hl : ∀ x y → x ≡ y
-    hl x y = Σ-pathp xunit=yunit $ Σ-prop-pathp (λ _ → hlevel!)
-        (funext λ a → monoid-inverse-unique (x .snd .snd .fst) a _ _
-          (x .snd .snd .snd .fst {_})
-          (y .snd .snd .snd .snd {_} ∙ sym xunit=yunit))
-      where
-        xunit=yunit = identities-equal (x .fst) (y .fst)
-          (is-monoid→is-unital-magma (x .snd .snd .fst))
-          (is-monoid→is-unital-magma (y .snd .snd .fst))
+    module x = is-group x
+    module y = is-group y hiding (magma-hlevel ; module HLevel-instance)
+    A-hl : ∀ {n} → H-Level A (2 + n)
+    A-hl = basic-instance {T = A} 2 (x .is-group.has-is-set)
+    1x=1y = identities-equal _ _
+      (is-monoid→is-unital-magma x.has-is-monoid)
+      (is-monoid→is-unital-magma y.has-is-monoid)
 
 instance
   H-Level-is-group
diff --git a/src/Algebra/Ring/Ideal.lagda.md b/src/Algebra/Ring/Ideal.lagda.md
index c33a5c09f..de3a5905f 100644
--- a/src/Algebra/Ring/Ideal.lagda.md
+++ b/src/Algebra/Ring/Ideal.lagda.md
@@ -115,7 +115,7 @@ $\mathfrak{a}$ is a sub-$R$-module of $R$:
     { mor   = record { map = fst ; linear = λ r m s n → refl }
     ; monic = λ {c = c} g h x → Linear-map-path $
       embedding→monic (Subset-proj-embedding λ _ → 𝔞 _ .is-tr) (g .map) (h .map)
-        (sym (transport-refl _) ·· ap map x ·· transport-refl _)
+        (sym (transport-refl _) ∙ ap map x ∙ transport-refl _)
     }
 ```
 
diff --git a/src/Algebra/Ring/Module/Category.lagda.md b/src/Algebra/Ring/Module/Category.lagda.md
index b063106d6..990b32b07 100644
--- a/src/Algebra/Ring/Module/Category.lagda.md
+++ b/src/Algebra/Ring/Module/Category.lagda.md
@@ -73,26 +73,13 @@ decency.</summary>
 R-Mod-ab-category .Hom-grp-ab A B f g =
   Linear-map-path (funext λ x → Module.G.commutative B)
 R-Mod-ab-category .∘-linear-l {C = C} f g h =
-  Linear-map-path $ funext λ x →
-    ap₂ C._+_
-      (transport-refl _ ∙ ap (f .map ⊙ h .map) (transport-refl _))
-      (transport-refl _ ∙ ap (g .map ⊙ h .map) (transport-refl _))
-    ∙ sym ( transport-refl _
-          ∙ ap₂ C._+_
-              (ap (f .map ⊙ h .map) (transport-refl _))
-              (ap (g .map ⊙ h .map) (transport-refl _)))
-  where module C = Module C
+  Linear-map-path $ funext λ x → Regularity.fast! refl
 R-Mod-ab-category .∘-linear-r {B = B} {C} f g h =
-  Linear-map-path $ funext λ x →
-    ap₂ C._+_
-      (transport-refl _ ∙ ap (f .map ⊙ g .map) (transport-refl _))
-      (transport-refl _ ∙ ap (f .map ⊙ h .map) (transport-refl _))
-    ∙ sym ( transport-refl _
-          ∙ ap (f .map) (ap₂ B._+_
-              (ap (g .map) (transport-refl _) ∙ sym (B.⋆-id _))
-              (ap (h .map) (transport-refl _) ∙ sym (B.⋆-id _)))
-          ∙ f .linear R.1r (g .map x) R.1r (h .map x)
-          ∙ ap₂ C._+_ (C.⋆-id _) (C.⋆-id _))
+  Linear-map-path $ funext λ x → Regularity.fast! (
+    f .map (g .map x) C.+ f .map (h .map x)                     ≡⟨ ap₂ C._+_ (sym (C.⋆-id _)) (sym (C.⋆-id _)) ⟩
+    R.1r C.⋆ f .map (g .map x) C.+ (R.1r C.⋆ f .map (h .map x)) ≡⟨ sym (f .linear R.1r (g .map x) R.1r (h .map x)) ⟩
+    f .map (R.1r B.⋆ g .map x B.+ R.1r B.⋆ h .map x)            ≡⟨ ap (f .map) (ap₂ B._+_ (B.⋆-id _) (B.⋆-id _)) ⟩
+    f .map (g .map x B.+ h .map x)                              ∎)
   where
     module C = Module C
     module B = Module B
@@ -173,14 +160,10 @@ path-mangling, but it's nothing _too_ bad:
     Σ-pathp (f .linear _ _ _ _) (g .linear _ _ _ _)
   prod .has-is-product .π₁∘factor = Linear-map-path (transport-refl _)
   prod .has-is-product .π₂∘factor = Linear-map-path (transport-refl _)
-  prod .has-is-product .unique other p q = Linear-map-path $
-    funext λ x → Σ-pathp
-      (sym ( sym (ap map p $ₚ x)
-          ·· transport-refl _
-          ·· ap (λ e → other .map e .fst) (transport-refl _)))
-      (sym ( sym (ap map q $ₚ x)
-          ·· transport-refl _
-          ·· ap (λ e → other .map e .snd) (transport-refl _)))
+  prod .has-is-product .unique other p q = Linear-map-path $ funext λ x →
+    Σ-pathp
+      (sym Regularity.reduce! ∙ (ap map p $ₚ x))
+      (sym Regularity.reduce! ∙ (ap map q $ₚ x))
 ```
 
 <!-- TODO [Amy 2022-09-15]
diff --git a/src/Cat/Diagram/Product/Solver.lagda.md b/src/Cat/Diagram/Product/Solver.lagda.md
index f6e36d843..67725e927 100644
--- a/src/Cat/Diagram/Product/Solver.lagda.md
+++ b/src/Cat/Diagram/Product/Solver.lagda.md
@@ -47,7 +47,7 @@ with un-quotiented syntax.
 
   data Expr : ‶Ob‶ → ‶Ob‶ → Type (o ⊔ ℓ) where
     ‶id‶    : ∀ {X} → Expr X X
-    _‶∘‶_   : ∀ {X Y Z} → Expr Y Z → Expr X Y → Expr X Z 
+    _‶∘‶_   : ∀ {X Y Z} → Expr Y Z → Expr X Y → Expr X Z
     ‶π₁‶    : ∀ {X Y} → Expr (X ‶⊗‶ Y) X
     ‶π₂‶    : ∀ {X Y} → Expr (X ‶⊗‶ Y) Y
     ‶⟨_,_⟩‶ : ∀ {X Y Z} → Expr X Y → Expr X Z → Expr X (Y ‶⊗‶ Z)
@@ -81,7 +81,7 @@ makes the enaction of η-laws[^eta] more difficult. On the other hand,
 if we quote in a type directed manner, we can perform η-expansion
 at every possible opportunity, which simplifies the implementation
 considerably. This will result in larger normal forms, but the
-expressions the solver needs to deal with are small, so this isn't 
+expressions the solver needs to deal with are small, so this isn't
 a pressing issue.
 
 [category solver]: Cat.Solver.html
@@ -287,7 +287,7 @@ a macro, which is critical for performance.
 ```agda
   abstract
     solve : ∀ X Y → (e1 e2 : Expr X Y) → nf X Y e1 ≡ nf X Y e2 → ⟦ e1 ⟧ₑ ≡ ⟦ e2 ⟧ₑ
-    solve X Y e1 e2 p = sym (sound X Y e1) ·· p ·· sound X Y e2 
+    solve X Y e1 e2 p = sym (sound X Y e1) ·· p ·· sound X Y e2
 ```
 
 # Reflection
@@ -309,7 +309,7 @@ module Reflection where
   private
     pattern is-product-field X Y args =
       _ h0∷ _ h0∷ _ h0∷ -- category args
-      X h0∷ Y h0∷       -- objects of product 
+      X h0∷ Y h0∷       -- objects of product
       _ h0∷             -- apex
       _ h0∷ _ h0∷       -- projections
       _ v∷              -- is-product record argument
@@ -420,7 +420,7 @@ calls to the solver/normaliser.
 
 ```agda
   get-objects : Term → TC (Term × Term)
-  get-objects tm = ((inferType tm >>= normalise) >>= wait-for-type) >>= λ where
+  get-objects tm = ((inferType tm >>= normalise) >>= wait-just-a-bit) >>= λ where
     (def (quote Precategory.Hom) (category-field (x v∷ y v∷ []))) →
       returnTC (x , y)
     tp →
@@ -445,7 +445,7 @@ want to examine the exact quoted representations of objects/homs.
                 termErr “x” ∷ strErr "\nAnd\n  " ∷
                 termErr “y” ∷ []
 
-  hom-repr-macro : ∀ {o ℓ} (𝒞 : Precategory o ℓ) (cartesian : ∀ X Y → Product 𝒞 X Y) → Term → Term → TC ⊤ 
+  hom-repr-macro : ∀ {o ℓ} (𝒞 : Precategory o ℓ) (cartesian : ∀ X Y → Product 𝒞 X Y) → Term → Term → TC ⊤
   hom-repr-macro cat cart hom hole =
     withReconstructed $
     withNormalisation false $
@@ -564,22 +564,22 @@ private module Tests {o ℓ} (𝒞 : Precategory o ℓ) (cartesian : ∀ X Y →
 
   test-β₁ : ∀ {X Y Z} → (f : Hom X Y) → (g : Hom X Z)
             → π₁ ∘ ⟨ f , g ⟩ ≡ f
-  test-β₁ f g = products! 𝒞 cartesian 
+  test-β₁ f g = products! 𝒞 cartesian
 
   test-β₂ : ∀ {X Y Z} → (f : Hom X Y) → (g : Hom X Z)
             → π₂ ∘ ⟨ f , g ⟩ ≡ g
-  test-β₂ f g = products! 𝒞 cartesian 
+  test-β₂ f g = products! 𝒞 cartesian
 
   test-⟨⟩∘ : ∀ {W X Y Z} → (f : Hom X Y) → (g : Hom X Z) → (h : Hom W X)
              → ⟨ f ∘ h , g ∘ h ⟩ ≡ ⟨ f , g ⟩ ∘ h
-  test-⟨⟩∘ f g h = products! 𝒞 cartesian 
+  test-⟨⟩∘ f g h = products! 𝒞 cartesian
 
   -- If you don't have 'withReconstructed' on, this test will fail!
   test-nested : ∀ {W X Y Z} → (f : Hom W X) → (g : Hom W Y) → (h : Hom W Z)
              → ⟨ ⟨ f , g ⟩ , h ⟩ ≡ ⟨ ⟨ f , g ⟩ , h ⟩
   test-nested {W} {X} {Y} {Z} f g h = products! 𝒞 cartesian
 
-  
+
   test-big : ∀ {W X Y Z} → (f : Hom (W ⊗ X) (W ⊗ Y)) → (g : Hom (W ⊗ X) Z)
              → (π₁ ∘ ⟨ f , g ⟩) ∘ id ≡ id ∘ ⟨ π₁ , π₂ ⟩ ∘ f
   test-big f g = products! 𝒞 cartesian
diff --git a/src/Cat/Displayed/Solver.agda b/src/Cat/Displayed/Solver.agda
index 5d96989df..f82f6b308 100644
--- a/src/Cat/Displayed/Solver.agda
+++ b/src/Cat/Displayed/Solver.agda
@@ -228,8 +228,8 @@ module Reflection where
     def (quote NbE.solve′) (mk-displayed-fn disp (infer-hidden 6 $ lhs v∷ rhs v∷ “refl” v∷ “reindex” v∷ []))
     where “reindex” = def (quote Dr.reindex) (disp v∷ unknown v∷ unknown v∷ [])
 
-  invoke-normalisier : Term → Term → Term
-  invoke-normalisier disp tm = def (quote NbE.nf′) (mk-displayed-fn disp (infer-hidden 5 $ tm v∷ []))
+  invoke-normaliser : Term → Term → Term
+  invoke-normaliser disp tm = def (quote NbE.nf′) (mk-displayed-fn disp (infer-hidden 5 $ tm v∷ []))
 
   build-expr : Term → TC Term
   build-expr “id” = returnTC $ con (quote NbE.`id) []
@@ -258,7 +258,7 @@ module Reflection where
   displayed-solver disp .SimpleSolver.dont-reduce = dont-reduce
   displayed-solver disp .SimpleSolver.build-expr tm = build-expr tm
   displayed-solver disp .SimpleSolver.invoke-solver = invoke-solver disp
-  displayed-solver disp .SimpleSolver.invoke-normalisier = invoke-normalisier disp
+  displayed-solver disp .SimpleSolver.invoke-normaliser = invoke-normaliser disp
 
   repr-macro : Term → Term → Term → TC ⊤
   repr-macro disp f _ =
diff --git a/src/Cat/Functor/Base.lagda.md b/src/Cat/Functor/Base.lagda.md
index 3c79441e3..6b3eac3c4 100644
--- a/src/Cat/Functor/Base.lagda.md
+++ b/src/Cat/Functor/Base.lagda.md
@@ -203,10 +203,10 @@ module _ {C : Precategory o h} {D : Precategory o₁ h₁} where
   ap-F₀-to-iso
     : ∀ (F : Functor C D) {y z : C .Ob}
     → (p : y ≡ z) → path→iso (ap (F₀ F) p) ≡ F-map-iso F (path→iso p)
-  ap-F₀-to-iso F =
+  ap-F₀-to-iso F {y} =
     J (λ _ p → path→iso (ap (F₀ F) p) ≡ F-map-iso F (path→iso p))
-      (D.≅-pathp _ _
-        (transport-refl _ ·· sym (F .F-id) ·· ap (F .F₁) (sym (transport-refl _))))
+      (D.≅-pathp (λ _ → F .F₀ y) (λ _ → F .F₀ y)
+        (Regularity.fast! (sym (F .F-id))))
 
   is-ff→F-map-iso-is-equiv
     : {F : Functor C D} → is-fully-faithful F
diff --git a/src/Cat/Solver.lagda.md b/src/Cat/Solver.lagda.md
index f2a794565..65da96e8f 100644
--- a/src/Cat/Solver.lagda.md
+++ b/src/Cat/Solver.lagda.md
@@ -163,7 +163,7 @@ module Reflection where
   cat-solver cat .SimpleSolver.dont-reduce = dont-reduce
   cat-solver cat .SimpleSolver.build-expr tm = returnTC $ build-expr tm
   cat-solver cat .SimpleSolver.invoke-solver = “solve” cat
-  cat-solver cat .SimpleSolver.invoke-normalisier = “nf” cat
+  cat-solver cat .SimpleSolver.invoke-normaliser = “nf” cat
 
   repr-macro : Term → Term → Term → TC ⊤
   repr-macro cat f _ =