From 7297867f52cfe15f4eed812e9b071b770c7ac24b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Am=C3=A9lia=20Liao?= <me@amelia.how>
Date: Mon, 13 Apr 2026 08:04:21 -0300
Subject: [PATCH 01/12] chore: remove trivial rewrite rules

---
 src/Cat/Internal/Functor/Outer.lagda.md | 22 ++++-----
 src/Cat/Internal/Opposite.lagda.md      | 26 ++++++----
 src/Data/Finset/Base.lagda.md           | 64 ++++++++++---------------
 src/Data/Nat/Base.lagda.md              |  2 -
 src/Homotopy/Space/Delooping.lagda.md   | 17 -------
 5 files changed, 51 insertions(+), 80 deletions(-)

diff --git a/src/Cat/Internal/Functor/Outer.lagda.md b/src/Cat/Internal/Functor/Outer.lagda.md
index 119c3f174..66db171c0 100644
--- a/src/Cat/Internal/Functor/Outer.lagda.md
+++ b/src/Cat/Internal/Functor/Outer.lagda.md
@@ -240,17 +240,17 @@ covariant construction, performed above.
       src-coh =
         sym (ap (src ∘_) p₁∘universal
         ∙ (homi (p₁ ∘ fₓ) ∘i op-ihom g) .has-src)
-    outf .P-id fₓ =
-      sym $ unique (sym (ap ihom (idri _))) (sym (!-unique _))
-    outf .P-∘ fₓ g h =
-      unique
-        (p₁∘universal
-         ∙ ap ihom (associ _ _ _)
-         ∙ ∘i-ihom refl
-             (sym (ap (src ∘_) p₁∘universal ∙ (homi (p₁ ∘ fₓ) ∘i op-ihom h) .has-src))
-             (sym (ap (tgt ∘_) p₁∘universal ∙ (homi (p₁ ∘ fₓ) ∘i op-ihom h) .has-tgt))
-             (sym p₁∘universal) refl)
-        p₂∘universal
+    outf .P-id fₓ = sym $ unique
+      (sym (ap ihom (ap₂ _∘i_ refl op-ihom-involutive ∙ idri _)))
+      (sym (!-unique _))
+    outf .P-∘ fₓ g h = unique
+      (p₁∘universal
+        ∙ ap ihom (ap₂ _∘i_ refl op-ihom-involutive ∙ associ _ _ _)
+        ∙ ∘i-ihom refl
+            (sym (ap (src ∘_) p₁∘universal ∙ (homi (p₁ ∘ fₓ) ∘i op-ihom h) .has-src))
+            (sym (ap (tgt ∘_) p₁∘universal ∙ (homi (p₁ ∘ fₓ) ∘i op-ihom h) .has-tgt))
+            (sym p₁∘universal) refl)
+      p₂∘universal
     outf .P₀-nat fₓ σ =
       sym (assoc _ _ _)
       ∙ ap (src ∘_) (sym (assoc _ _ _))
diff --git a/src/Cat/Internal/Opposite.lagda.md b/src/Cat/Internal/Opposite.lagda.md
index 2571ba8fb..b051ac42c 100644
--- a/src/Cat/Internal/Opposite.lagda.md
+++ b/src/Cat/Internal/Opposite.lagda.md
@@ -45,13 +45,11 @@ op-ihom-nat f _ = Internal-hom-path refl
 
 <!--
 ```agda
-private
-  op-ihom-involutive
-    : ∀ {C₀ C₁ Γ} {src tgt : Hom C₁ C₀} {x y : Hom Γ C₀}
-    → {f : Internal-hom src tgt x y}
-    → op-ihom (op-ihom f) ≡ f
-  op-ihom-involutive = Internal-hom-path refl
-{-# REWRITE op-ihom-involutive #-}
+op-ihom-involutive
+  : ∀ {C₀ C₁ Γ} {src tgt : Hom C₁ C₀} {x y : Hom Γ C₀}
+  → {f : Internal-hom src tgt x y}
+  → op-ihom (op-ihom f) ≡ f
+op-ihom-involutive = Internal-hom-path refl
 ```
 -->
 
@@ -69,9 +67,17 @@ Internal-cat-on-opi ℂ = icat-opi-on  where
   icat-opi-on : Internal-cat-on _ _
   icat-opi-on .idi x = op-ihom (ℂ.idi x)
   icat-opi-on ._∘i_ f g = op-ihom (op-ihom g ℂ.∘i op-ihom f)
-  icat-opi-on .idli f = ap op-ihom (ℂ.idri _)
-  icat-opi-on .idri f = ap op-ihom (ℂ.idli _)
-  icat-opi-on .associ f g h = ap op-ihom (sym (ℂ.associ _ _ _))
+  icat-opi-on .idli f =
+    op-ihom (op-ihom f ℂ.∘i ⌜ op-ihom (op-ihom (ℂ.idi _)) ⌝) ≡⟨ ap! op-ihom-involutive ⟩
+    op-ihom ⌜ op-ihom f ℂ.∘i ℂ.idi _ ⌝                       ≡⟨ ap! (ℂ.idri (op-ihom f)) ⟩
+    op-ihom (op-ihom f)                                      ≡⟨ op-ihom-involutive ⟩
+    f                                                        ∎
+  icat-opi-on .idri f = ap op-ihom (ap₂ ℂ._∘i_ op-ihom-involutive refl ∙ ℂ.idli _) ∙ op-ihom-involutive
+  icat-opi-on .associ f g h =
+    op-ihom (⌜ op-ihom (op-ihom (op-ihom h ℂ.∘i op-ihom g)) ⌝ ℂ.∘i op-ihom f) ≡⟨ ap! op-ihom-involutive ⟩
+    op-ihom ⌜ (op-ihom h ℂ.∘i op-ihom g) ℂ.∘i op-ihom f ⌝                     ≡⟨ ap! (sym (ℂ.associ _ _ _)) ⟩
+    op-ihom ⌜ op-ihom h ℂ.∘i op-ihom g ℂ.∘i op-ihom f ⌝                       ≡⟨ ap¡ (sym op-ihom-involutive) ⟩
+    op-ihom (op-ihom h ℂ.∘i ⌜ op-ihom (op-ihom (op-ihom g ℂ.∘i op-ihom f)) ⌝) ∎
   icat-opi-on .idi-nat σ =
     op-ihom-nat (ℂ.idi _) σ ∙ ap op-ihom (ℂ.idi-nat σ)
   icat-opi-on .∘i-nat f g σ =
diff --git a/src/Data/Finset/Base.lagda.md b/src/Data/Finset/Base.lagda.md
index 43d8d464c..0ce1b03a7 100644
--- a/src/Data/Finset/Base.lagda.md
+++ b/src/Data/Finset/Base.lagda.md
@@ -341,32 +341,29 @@ xs)$ has to be truncated.
       (finset-mem x xs) (finset-mem x ys)
       (λ i → finset-mem x (p i)) (λ i → finset-mem x (q i)) i j
 
-opaque
-  _∈ᶠˢ_ : A → Finset A → Type (level-of A)
-  x ∈ᶠˢ xs = ⌞ finset-mem x xs ⌟
-
-  hereₛ' : ∀ {x y : A} {xs} → x ≡ᵢ y → x ∈ᶠˢ (y ∷ xs)
-  hereₛ' p = inc (inl p)
+record _∈ᶠˢ_ (x : A) (xs : Finset A) : Type (level-of A) where
+  constructor lift
+  field
+    lower : ⌞ finset-mem x xs ⌟
 
-  thereₛ : ∀ {x y : A} {xs} → y ∈ᶠˢ xs → y ∈ᶠˢ (x ∷ xs)
-  thereₛ x = inc (inr x)
+open _∈ᶠˢ_ public
 
-  ¬mem-[] : {x : A} → ¬ (x ∈ᶠˢ [])
-  ¬mem-[] ()
+instance unquoteDecl H-Level-∈ᶠˢ = declare-record-hlevel 1 H-Level-∈ᶠˢ (quote _∈ᶠˢ_)
 
-  private
-    ∈ᶠˢ-hlevel : {x : A} {xs : Finset A} → ⊤ → is-prop (x ∈ᶠˢ xs)
-    ∈ᶠˢ-hlevel {x = x} {xs} _ = finset-mem x xs .is-tr
+hereₛ' : ∀ {x y : A} {xs} → x ≡ᵢ y → x ∈ᶠˢ (y ∷ xs)
+hereₛ' p = lift (inc (inl p))
 
 hereₛ : ∀ {x : A} {xs} → x ∈ᶠˢ (x ∷ xs)
 hereₛ = hereₛ' reflᵢ
 
-instance
-  hlevel-proj-∈ᶠˢ : hlevel-projection (quote _∈ᶠˢ_)
-  hlevel-proj-∈ᶠˢ .hlevel-projection.has-level = quote ∈ᶠˢ-hlevel
-  hlevel-proj-∈ᶠˢ .hlevel-projection.get-level x = pure (lit (nat 1))
-  hlevel-proj-∈ᶠˢ .hlevel-projection.get-argument x = pure (con₀ (quote tt))
+thereₛ : ∀ {x y : A} {xs} → y ∈ᶠˢ xs → y ∈ᶠˢ (x ∷ xs)
+thereₛ (lift x) = lift (inc (inr x))
 
+abstract
+  ¬mem-[] : {x : A} → ¬ (x ∈ᶠˢ [])
+  ¬mem-[] ()
+
+instance
   Membership-Finset : Membership A (Finset A) _
   Membership-Finset = record { _∈_ = _∈ᶠˢ_ }
 
@@ -379,33 +376,20 @@ We can then define a *case analysis* principle for membership in a
 finite set, as long as we're showing a proposition.
 
 ```agda
-opaque
-  unfolding _∈ᶠˢ_
-
-  ∈ᶠˢ-split
-    : ∀ {ℓp} {x y : A} {xs} {P : x ∈ᶠˢ (y ∷ xs) → Type ℓp} ⦃ _ : ∀ {x} → H-Level (P x) 1 ⦄
-    → ((p : x ≡ᵢ y) → P (hereₛ' p))
-    → ((w : x ∈ᶠˢ xs) → P (thereₛ w))
-    → (w : x ∈ᶠˢ (y ∷ xs)) → P w
-  ∈ᶠˢ-split ⦃ h ⦄ l r = ∥-∥-elim (λ x → hlevel 1 ⦃ h ⦄) λ where
+∈ᶠˢ-split
+  : ∀ {ℓp} {x y : A} {xs} {P : x ∈ᶠˢ (y ∷ xs) → Type ℓp} ⦃ _ : ∀ {x} → H-Level (P x) 1 ⦄
+  → ((p : x ≡ᵢ y) → P (hereₛ' p))
+  → ((w : x ∈ᶠˢ xs) → P (thereₛ w))
+  → (w : x ∈ᶠˢ (y ∷ xs)) → P w
+∈ᶠˢ-split {P = P} l r (lift x) = ∥-∥-elim {P = λ v → P (lift v)} (λ x → hlevel 1)
+  (λ where
     (inl a) → l a
-    (inr b) → r b
+    (inr b) → r (lift b))
+  x
 ```
 
 <!--
 ```agda
-  ∈ᶠˢ-split-here
-    : ∀ {ℓp} {x y : A} {xs} {P : Type ℓp} ⦃ _ : H-Level P 1 ⦄ {p : x ≡ᵢ y} (f : x ≡ᵢ y → P) (g : x ∈ᶠˢ xs → P)
-    → ∈ᶠˢ-split {xs = xs} f g (hereₛ' p) ≡ f p
-  ∈ᶠˢ-split-here f g = refl
-
-  ∈ᶠˢ-split-there
-    : ∀ {ℓp} {x y : A} {xs} {P : Type ℓp} ⦃ _ : H-Level P 1 ⦄ (f : x ≡ᵢ y → P) (g : x ∈ᶠˢ xs → P) (w : x ∈ᶠˢ xs)
-    → ∈ᶠˢ-split {y = y} {xs = xs} f g (thereₛ w) ≡ g w
-  ∈ᶠˢ-split-there f g w = refl
-
-  {-# REWRITE ∈ᶠˢ-split-here ∈ᶠˢ-split-there #-}
-
 there-cons-if : (d : Dec B) (x y : A) (xs : Finset A) → y ∈ xs → y ∈ cons-if d x xs
 there-cons-if (yes a) x y xs p = thereₛ p
 there-cons-if (no ¬a) x y xs p = p
diff --git a/src/Data/Nat/Base.lagda.md b/src/Data/Nat/Base.lagda.md
index 37ab91c71..824d8bab2 100644
--- a/src/Data/Nat/Base.lagda.md
+++ b/src/Data/Nat/Base.lagda.md
@@ -115,8 +115,6 @@ abstract
   from-prim-eq-refl {zero} = refl
   from-prim-eq-refl {suc x} = ap (ap suc) (from-prim-eq-refl {x})
 
-  {-# REWRITE from-prim-eq-refl #-}
-
   to-prim-eq : ∀ {x y} → x ≡ y → So (x == y)
   to-prim-eq {zero} {zero} p = oh
   to-prim-eq {zero} {suc y} p = absurd (zero≠suc p)
diff --git a/src/Homotopy/Space/Delooping.lagda.md b/src/Homotopy/Space/Delooping.lagda.md
index 0d6693fcd..a5efc34d7 100644
--- a/src/Homotopy/Space/Delooping.lagda.md
+++ b/src/Homotopy/Space/Delooping.lagda.md
@@ -462,23 +462,6 @@ We can then obtain a nice interface for working with `winding`{.Agda}.
 
 <!--
 ```agda
-  -- Want: pathᵇ base ≡ path, definitionally
-  -- Have: pathᵇ base is a projection from some opaque record
-  -- Soln: Evil hack!
-  opaque
-    unfolding winding-is-equiv
-
-    winding-is-equiv-base : winding-is-equiv base ≡ Equiv.inverse (G≃ΩB G) .snd
-    winding-is-equiv-base = prop!
-
-  {-# REWRITE winding-is-equiv-base #-}
-
-  _ : pathᵇ base ≡ path
-  _ = refl -- MUST check!
-
-  pathᵇᵀ : ∀ (x : Deloop G) g h → Triangle (pathᵇ x g) (pathᵇ x (g ⋆ h)) (pathᵇ x h)
-  pathᵇᵀ = Deloop-elim-prop G _ (λ x → hlevel 1) λ g h → pathᵀ g h
-
 Deloop-is-connected : ∀ {ℓ} {G : Group ℓ} → is-connected∙ (Deloop G , base)
 Deloop-is-connected = Deloop-elim-prop _ _ (λ _ → hlevel 1) (inc refl)
 ```

From 7ee7ae2f48016ab988dfdc97f4dc5d1dbf85279d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Am=C3=A9lia=20Liao?= <me@amelia.how>
Date: Mon, 13 Apr 2026 10:28:41 -0300
Subject: [PATCH 02/12] chore: remove --lossy-unification

---
 src/Algebra/Ring/Module/Multilinear.lagda.md | 122 +++++++++++--------
 src/Cat/Bi/Diagram/Monad/Spans.lagda.md      |   1 -
 src/Cat/Displayed/Univalence/Thin.lagda.md   |   5 +-
 src/Cat/Univalent/Rezk/Universal.lagda.md    |  27 ++--
 src/Order/Frame/Free.lagda.md                |   1 -
 5 files changed, 87 insertions(+), 69 deletions(-)

diff --git a/src/Algebra/Ring/Module/Multilinear.lagda.md b/src/Algebra/Ring/Module/Multilinear.lagda.md
index b6224938d..5079914cd 100644
--- a/src/Algebra/Ring/Module/Multilinear.lagda.md
+++ b/src/Algebra/Ring/Module/Multilinear.lagda.md
@@ -1,6 +1,5 @@
 <!--
 ```agda
-{-# OPTIONS --lossy-unification #-}
 open import Algebra.Ring.Module.Notation
 open import Algebra.Ring.Commutative
 open import Algebra.Group.Notation
@@ -143,6 +142,7 @@ to denote `updateₚ α i x` that fits well in the mathematical prose.
 open Multilinear-map
 open Multilinear-map using (map) public
 open Linear-map using (map)
+{-# INLINE Multilinear-map.constructor #-}
 
 private unquoteDecl eqv = declare-record-iso eqv (quote Multilinear-map)
 
@@ -168,6 +168,24 @@ Multilinear-map-path {N = N} {f = f} {g = g} p = go where
     (f .linearₚ) (g .linearₚ)
     i
 
+module
+  _ {n : Nat} {ℓₘ : Fin n → Level} {ℓₙ} {Ms : (i : Fin n) → Module R (ℓₘ i)} {N : Module R ℓₙ}
+    (map : Arrᶠ (λ i → ⌞ Ms i ⌟) ⌞ N ⌟)
+  where
+
+  private instance
+    _ = module-notation N
+    _ : ∀ {i : Fin n} → Module-notation R ⌞ Ms i ⌟
+    _ = module-notation (Ms _)
+
+  from-linear-at
+    : ( ∀ i (xs : Πᶠ λ j → ⌞ Ms j ⌟) (r : ⌞ R ⌟) (x y : ⌞ Ms i ⌟)
+      → applyᶠ map (updateₚ xs i (r ⋆ x + y))
+      ≡ r ⋆ applyᶠ map (updateₚ xs i x) + applyᶠ map (updateₚ xs i y))
+    → Multilinear-map n Ms N
+  {-# INLINE from-linear-at #-}
+  from-linear-at lin = record { map = map ; linearₚ = tabulateₚ lin }
+
 Multilinear-maps
   : ∀ {n} {ℓₘ : Fin n → Level}
       {Ms : (i : Fin n) → Module R (ℓₘ i)}
@@ -181,9 +199,6 @@ Multilinear-maps {n = n} {Ms = Ms} {N = N} = to-module-on mk where
     _ : ∀ {i : Fin n} → Module-notation R ⌞ Ms i ⌟
     _ = module-notation (Ms _)
 
-  -- Normally there would be no way in hell these helpers would ever
-  -- be useful... except this module needs lossy-unification for
-  -- performance reasonsl so we might as well abuse it for style!
   _⟨_⟩
     : Multilinear-map n Ms N
     → {_ : Πᶠ (λ i → ⌞ Ms i ⌟)} {i : Fin n} → ⌞ Ms i ⌟ → ⌞ N ⌟
@@ -215,15 +230,14 @@ through some nighmarish computations by hand.
 
 ```agda
   add : Multilinear-map n Ms N → Multilinear-map n Ms N → Multilinear-map n Ms N
-  add f g .Multilinear-map.map = zipᶠ _+_ (f .map) (g .map)
+  add f g .Multilinear-map.map = zipᶠ {P = λ i → ⌞ Ms i ⌟} _+_ (f .map) (g .map)
   add f g .Multilinear-map.linearₚ = tabulateₚ λ i xs r x y →
-    zipᶠ _+_ (f .map) (g .map) ⟨ r ⋆ x + y ⟩ᵤ         ≡⟨ apply-zipᶠ _ _ _ _ ⟩
+    zipᶠ _+_ (f .map) (g .map) ⟨ r ⋆ x + y ⟩ᵤ         ≡⟨ apply-zipᶠ {P = λ i → ⌞ Ms i ⌟} _ _ _ _ ⟩
     f ⟨ r ⋆ x + y ⟩ + g ⟨ r ⋆ x + y ⟩                 ≡⟨ ap₂ _+_ (linear-at f i xs r x y) (linear-at g i xs r x y) ⟩
     (r ⋆ f ⟨ x ⟩ + f ⟨ y ⟩) + (r ⋆ g ⟨ x ⟩ + g ⟨ y ⟩) ≡⟨ N.ab.extendr (N.ab.extendl N.+-comm) ⟩
     (r ⋆ f ⟨ x ⟩ + r ⋆ g ⟨ x ⟩) + (f ⟨ y ⟩ + g ⟨ y ⟩) ≡⟨ ap₂ _+_ (sym (⋆-distribl r _ _)) refl ⟩
-    r ⋆ (f ⟨ x ⟩ + g ⟨ x ⟩) + (f ⟨ y ⟩ + g ⟨ y ⟩)     ≡⟨ ap₂ N._+_ (ap (r N.⋆_) (sym (apply-zipᶠ _ _ _ _))) (sym (apply-zipᶠ _ _ _ _)) ⟩
-    r ⋆ (zipᶠ _+_ (f .map) (g .map) ⟨ x ⟩ᵤ)
-      + zipᶠ _+_ (f .map) (g .map) ⟨ y ⟩ᵤ             ∎
+    r ⋆ (f ⟨ x ⟩ + g ⟨ x ⟩) + (f ⟨ y ⟩ + g ⟨ y ⟩)     ≡⟨ ap₂ N._+_ (ap (r N.⋆_) (sym (apply-zipᶠ {P = λ i → ⌞ Ms i ⌟} _ _ _ _))) (sym (apply-zipᶠ {P = λ i → ⌞ Ms i ⌟} _ _ _ _)) ⟩
+    r ⋆ add f g .map ⟨ x ⟩ᵤ + add f g .map ⟨ y ⟩ᵤ     ∎
 ```
 
 The example of addition, above, is representative: The flow of these
@@ -240,20 +254,19 @@ spotlight.</summary>
   invm : Multilinear-map n Ms N → Multilinear-map n Ms N
   invm f .map     = mapᶠ N.-_ (f .map)
   invm f .linearₚ = tabulateₚ λ i xs r x y →
-    apply-mapᶠ _ _ _ ∙∙ ap N.-_ (linear-at f i xs r x y)
-    ∙∙ N.neg-comm
-    ∙∙ N.+-comm
-    ∙∙ sym (ap₂ N._+_ N.⋆-invr refl)
-     ∙ sym (ap₂ N._+_ (ap (r N.⋆_) (apply-mapᶠ _ _ _)) (apply-mapᶠ _ _ _))
+    apply-mapᶠ {P = λ i → ⌞ Ms i ⌟} _ _ _ ∙∙ ap N.-_ (linear-at f i xs r x y)
+    ∙∙ N.neg-comm ∙∙ N.+-comm ∙∙ sym (ap₂ N._+_ N.⋆-invr refl) ∙ sym (ap₂ N._+_
+      (ap (r N.⋆_) (apply-mapᶠ {P = λ i → ⌞ Ms i ⌟} _ _ _))
+      (apply-mapᶠ {P = λ i → ⌞ Ms i ⌟} _ _ _))
 
   scale : ⌞ R ⌟ → Multilinear-map n Ms N → Multilinear-map n Ms N
   scale r f .map = mapᶠ (r N.⋆_) (f .map)
   scale r f .linearₚ = tabulateₚ λ i xs s x y →
-    apply-mapᶠ _ _ _
-    ∙∙ ap (r N.⋆_) (linear-at f i xs s x y)
-    ∙∙ ⋆-distribl _ _ _
-     ∙ ap₂ N._+_ (N.⋆-assoc _ _ _ ∙∙ ap₂ N._⋆_ cr refl ∙∙ sym (N.⋆-assoc _ _ _) ∙ ap (s N.⋆_) (sym (apply-mapᶠ _ _ _)))
-                 (sym (apply-mapᶠ _ _ _))
+    apply-mapᶠ {P = λ i → ⌞ Ms i ⌟} _ _ _ ∙∙ ap (r N.⋆_) (linear-at f i xs s x y)
+    ∙∙ ⋆-distribl _ _ _ ∙ ap₂ N._+_
+      ( N.⋆-assoc _ _ _ ∙∙ ap₂ N._⋆_ cr refl ∙∙ sym (N.⋆-assoc _ _ _) ∙ ap (s N.⋆_)
+        (sym (apply-mapᶠ {P = λ i → ⌞ Ms i ⌟} _ _ _)))
+        (sym (apply-mapᶠ {P = λ i → ⌞ Ms i ⌟} _ _ _))
 
   open make-module hiding (_+_ ; _⋆_)
 
@@ -268,43 +281,52 @@ spotlight.</summary>
   mk .make-module._⋆_ = scale
   mk .0g .map = constᶠ N.0g
   mk .0g .linearₚ = tabulateₚ λ i xs r x y →
-    apply-constᶠ _ (updateₚ xs i (r ⋆ x + y)) ∙ sym (N.ab.elimr (apply-constᶠ _ _)
-    ∙ ap (r N.⋆_) (apply-constᶠ _ _) ∙ N.⋆-idr)
+      apply-constᶠ _ (updateₚ xs i (r ⋆ x + y))
+    ∙ sym (N.ab.elimr (apply-constᶠ {P = λ i → ⌞ Ms i ⌟} _ _)
+    ∙ ap (r N.⋆_) (apply-constᶠ {P = λ i → ⌞ Ms i ⌟} _ _) ∙ N.⋆-idr)
 
   -- Group laws
   mk .+-assoc x y z = Multilinear-map-path $ funextᶠ λ as →
         apply-zipᶠ _ _ _ as
-    ∙∙ ap₂ N._+_ refl (apply-zipᶠ _ _ _ _)
-    ∙∙ N.+-assoc ∙ ap₂ N._+_ (sym (apply-zipᶠ N._+_ _ _ _)) refl
-     ∙ sym (apply-zipᶠ N._+_ _ _ _)
+    ∙∙ ap₂ N._+_ refl (apply-zipᶠ {P = λ i → ⌞ Ms i ⌟} _ _ _ _)
+    ∙∙ N.+-assoc ∙ ap₂ N._+_ (sym (apply-zipᶠ {P = λ i → ⌞ Ms i ⌟} N._+_ _ _ _)) refl
+     ∙ sym (apply-zipᶠ {P = λ i → ⌞ Ms i ⌟} N._+_ _ _ _)
   mk .+-invl x = Multilinear-map-path $ funextᶠ λ as →
-       apply-zipᶠ _ _ _ _
-    ∙∙ ap₂ N._+_ (apply-mapᶠ _ _ _) refl
+       apply-zipᶠ {P = λ i → ⌞ Ms i ⌟} _ _ _ _
+    ∙∙ ap₂ N._+_ (apply-mapᶠ {P = λ i → ⌞ Ms i ⌟} _ _ _) refl
     ∙∙ N.+-invl
-     ∙ sym (apply-constᶠ _ _)
+     ∙ sym (apply-constᶠ {P = λ i → ⌞ Ms i ⌟} _ _)
   mk .+-idl x = Multilinear-map-path $ funextᶠ λ as →
-    apply-zipᶠ _ _ _ _ ∙ N.ab.eliml (apply-constᶠ _ _)
+      apply-zipᶠ {P = λ i → ⌞ Ms i ⌟} _ _ _ _
+    ∙ N.ab.eliml (apply-constᶠ {P = λ i → ⌞ Ms i ⌟} _ _)
   mk .+-comm x y = Multilinear-map-path $ funextᶠ λ as →
-    apply-zipᶠ _ _ _ _ ∙ N.+-comm ∙ sym (apply-zipᶠ N._+_ _ _ _)
+       apply-zipᶠ {P = λ i → ⌞ Ms i ⌟} _ _ _ _
+    ∙∙ N.+-comm
+    ∙∙ sym (apply-zipᶠ {P = λ i → ⌞ Ms i ⌟} N._+_ _ _ _)
 
   -- Action laws
   mk .⋆-distribl r x y = Multilinear-map-path $ funextᶠ λ as →
-        apply-mapᶠ _ _ _
-    ∙∙ ap (r N.⋆_) (apply-zipᶠ _ _ _ _)
+        apply-mapᶠ {P = λ i → ⌞ Ms i ⌟} _ _ _
+    ∙∙ ap (r N.⋆_) (apply-zipᶠ {P = λ i → ⌞ Ms i ⌟} _ _ _ _)
     ∙∙ N.⋆-distribl _ _ _
-    ∙∙ sym (ap₂ N._+_ (apply-mapᶠ _ _ _) (apply-mapᶠ _ _ _))
-    ∙∙ sym (apply-zipᶠ N._+_ _ _ _)
+    ∙∙ sym (ap₂ N._+_
+      (apply-mapᶠ {P = λ i → ⌞ Ms i ⌟} _ _ _)
+      (apply-mapᶠ {P = λ i → ⌞ Ms i ⌟} _ _ _))
+    ∙∙ sym (apply-zipᶠ {P = λ i → ⌞ Ms i ⌟} N._+_ _ _ _)
   mk .⋆-distribr r x y = Multilinear-map-path $ funextᶠ λ as →
-        apply-mapᶠ _ _ _
+        apply-mapᶠ {P = λ i → ⌞ Ms i ⌟} _ _ _
     ∙∙ N.⋆-distribr _ _ _
-    ∙∙ sym (ap₂ N._+_ (apply-mapᶠ (r N.⋆_) _ _) (apply-mapᶠ (x N.⋆_) _ _))
-      ∙ sym (apply-zipᶠ N._+_ _ _ _)
+    ∙∙ sym (ap₂ N._+_
+      (apply-mapᶠ {P = λ i → ⌞ Ms i ⌟} (r N.⋆_) _ _)
+      (apply-mapᶠ {P = λ i → ⌞ Ms i ⌟} (x N.⋆_) _ _))
+      ∙ sym (apply-zipᶠ {P = λ i → ⌞ Ms i ⌟} N._+_ _ _ _)
   mk .⋆-assoc r s x = Multilinear-map-path $ funextᶠ λ as →
-        apply-mapᶠ _ _ _
-    ∙∙ ap (r N.⋆_) (apply-mapᶠ _ _ _)
+        apply-mapᶠ {P = λ i → ⌞ Ms i ⌟} _ _ _
+    ∙∙ ap (r N.⋆_) (apply-mapᶠ {P = λ i → ⌞ Ms i ⌟} _ _ _)
     ∙∙ N.⋆-assoc _ _ _
-      ∙ sym (apply-mapᶠ _ _ _)
-  mk .⋆-id x = Multilinear-map-path $ funextᶠ λ as → apply-mapᶠ _ _ _ ∙ N.⋆-id _
+      ∙ sym (apply-mapᶠ {P = λ i → ⌞ Ms i ⌟} _ _ _)
+  mk .⋆-id x = Multilinear-map-path $ funextᶠ λ as →
+    apply-mapᶠ {P = λ i → ⌞ Ms i ⌟} _ _ _ ∙ N.⋆-id _
 ```
 </details>
 
@@ -353,12 +375,12 @@ proofs of linearity.
     → Multilinear-map (suc n) Ms N
   curry-multilinear-map lin = ml where
     ml : Multilinear-map (suc n) _ _
-    ml .map x = lin .map x .map
-    ml .linearₚ = tabulateₚ λ i xs r x y → case fin-view i of λ where
-      zero → ap (λ e → applyᶠ (e .map) (xs .snd)) (Linear-map.linear lin r x y)
-        ∙∙ apply-zipᶠ _ _ _ _
-        ∙∙ ap₂ N._+_ (apply-mapᶠ _ _ _) refl
-      (suc i) → linear-at (lin .map (xs .fst)) i (xs .snd) r x y
+    ml = from-linear-at (λ x → lin .map x .map) λ i xs r x y →
+      case fin-view i of λ where
+        zero → ap (λ e → applyᶠ (e .map) (xs .snd)) (Linear-map.linear lin r x y)
+          ∙∙ apply-zipᶠ {P = λ i → ⌞ Ms (fsuc i) ⌟} _ _ _ _
+          ∙∙ ap₂ N._+_ (apply-mapᶠ {P = λ i → ⌞ Ms (fsuc i) ⌟} _ _ _) refl
+        (suc i) → linear-at (lin .map (xs .fst)) i (xs .snd) r x y
 
   uncurry-multilinear-map
     : Multilinear-map (suc n) Ms N
@@ -369,10 +391,10 @@ proofs of linearity.
     uc .map x .linearₚ = tabulateₚ λ i xs →
       Multilinear-map.linear-at multi (fsuc i) (x , xs)
 
-    uc .lin .linear r s t =
-      Multilinear-map-path $ funextᶠ λ as →
+    uc .lin .linear r s t = Multilinear-map-path $ funextᶠ λ as →
         linear-at multi fzero (Ms.0g fzero , as) _ _ _
-        ∙ sym (apply-zipᶠ _ _ _ _ ∙ ap₂ N._+_ (apply-mapᶠ _ _ _) refl)
+      ∙ sym (apply-zipᶠ {P = λ i → ⌞ Ms (fsuc i) ⌟} _ _ _ _
+            ∙ ap₂ N._+_ (apply-mapᶠ {P = λ i → ⌞ Ms (fsuc i) ⌟} _ _ _) refl)
 ```
 
 To stress how well these constructions compute, note that, on the
@@ -384,7 +406,7 @@ definitionally isomorphisms.
   uncurry-ml-is-equiv = is-iso→is-equiv λ where
     .is-iso.from   → curry-multilinear-map
     .is-iso.rinv x → ext λ x → Multilinear-map-path refl
-    .is-iso.linv x → Multilinear-map-path $ funextᶠ λ as → refl
+    .is-iso.linv x → Multilinear-map-path $ funextᶠ {P = λ i → ⌞ Ms i ⌟} λ as → refl
 
   module
     Uncurry = Equiv (_ , uncurry-ml-is-equiv)
diff --git a/src/Cat/Bi/Diagram/Monad/Spans.lagda.md b/src/Cat/Bi/Diagram/Monad/Spans.lagda.md
index a231dd8ff..a28064a62 100644
--- a/src/Cat/Bi/Diagram/Monad/Spans.lagda.md
+++ b/src/Cat/Bi/Diagram/Monad/Spans.lagda.md
@@ -1,6 +1,5 @@
 <!--
 ```agda
-{-# OPTIONS --lossy-unification #-}
 open import Cat.Instances.Sets.Complete
 open import Cat.Bi.Instances.Spans
 open import Cat.Bi.Diagram.Monad
diff --git a/src/Cat/Displayed/Univalence/Thin.lagda.md b/src/Cat/Displayed/Univalence/Thin.lagda.md
index dc0c67976..0500baa79 100644
--- a/src/Cat/Displayed/Univalence/Thin.lagda.md
+++ b/src/Cat/Displayed/Univalence/Thin.lagda.md
@@ -1,6 +1,5 @@
 <!--
 ```agda
-{-# OPTIONS --lossy-unification #-}
 open import 1Lab.Function.Embedding
 
 open import Cat.Displayed.Univalence
@@ -161,9 +160,9 @@ record is-equational {ℓ o' ℓ'} {S : Type ℓ → Type o'} (spec : Thin-struc
     → (f : ⌞ a ⌟ ≃ ⌞ b ⌟)
     → ∣ spec .is-hom (Equiv.to f) (a .snd) (b .snd) ∣
     → a Som.≅ b
-  total-iso f e = Som.make-iso
+  total-iso {a = a} {b = b} f e = Som.make-iso
     (∫hom (Equiv.to f) e)
-    (∫hom (Equiv.from f) (equiv-hom→inverse-hom f e))
+    (∫hom (Equiv.from f) (equiv-hom→inverse-hom {a} {b} f e))
     (ext (Equiv.ε f))
     (ext (Equiv.η f))
 
diff --git a/src/Cat/Univalent/Rezk/Universal.lagda.md b/src/Cat/Univalent/Rezk/Universal.lagda.md
index 23df623ab..ab7c09ddd 100644
--- a/src/Cat/Univalent/Rezk/Universal.lagda.md
+++ b/src/Cat/Univalent/Rezk/Universal.lagda.md
@@ -1,6 +1,5 @@
 <!--
 ```agda
-{-# OPTIONS --lossy-unification #-}
 open import Cat.Functor.Equivalence
 open import Cat.Functor.Properties
 open import Cat.Instances.Functor
@@ -347,10 +346,11 @@ candidate over it.
 
 <!--
 ```agda
-    summon : ∀ {b} → ∥ Essential-fibre H b ∥ → is-contr (Obs b)
-    summon f = ∥-∥-out is-contr-is-prop do
-      f ← f
-      pure $ contr (obj' f) (Obs-is-prop f)
+    opaque
+      summon : ∀ {b} → ∥ Essential-fibre H b ∥ → is-contr (Obs b)
+      summon f = ∥-∥-out is-contr-is-prop do
+        f ← f
+        pure $ contr (obj' f) (Obs-is-prop f)
 
     G₀ : B.Ob → C.Ob
     G₀ b = summon {b = b} (H-eso b) .centre .fst
@@ -442,15 +442,14 @@ This proof _really_ isn't commented. I'm sorry.
       Homs-prop' (g₁ , w) = C.iso→epic (k a₀ h₀) _ _
         (sym (δ a₀ h₀ a₀' h₀' l₀ p ∙ w a₀ h₀ a₀' h₀' l₀ p))
 
-    Homs-contr' : ∀ {b b'} (f : B.Hom b b') → ∥ is-contr (Homs f) ∥
-    Homs-contr' {b = b} {b'} f = do
-      (a₀ , h)   ← H-eso b
-      (a₀' , h') ← H-eso b'
-      inc (contr (Homs-pt f a₀ h a₀' h') λ h' → Σ-prop-path!
-        (sym (Homs-prop' f _ _ _ _ h')))
-
-    Homs-contr : ∀ {b b'} (f : B.Hom b b') → is-contr (Homs f)
-    Homs-contr f = ∥-∥-out! (Homs-contr' f)
+    opaque
+      Homs-contr : ∀ {b b'} (f : B.Hom b b') → is-contr (Homs f)
+      Homs-contr {b = b} {b'} f = ∥-∥-out! do
+        (a₀ , h)   ← H-eso b
+        (a₀' , h') ← H-eso b'
+        pure record where
+          centre   = Homs-pt f a₀ h a₀' h'
+          paths h' = Σ-prop-path! (sym (Homs-prop' f _ _ _ _ h'))
 
     G₁ : ∀ {b b'} → B.Hom b b' → C.Hom (G₀ b) (G₀ b')
     G₁ f = Homs-contr f .centre .fst
diff --git a/src/Order/Frame/Free.lagda.md b/src/Order/Frame/Free.lagda.md
index d805c9352..48e108621 100644
--- a/src/Order/Frame/Free.lagda.md
+++ b/src/Order/Frame/Free.lagda.md
@@ -1,6 +1,5 @@
 <!--
 ```agda
-{-# OPTIONS --lossy-unification #-}
 open import Cat.Functor.Subcategory
 open import Cat.Functor.Adjoint
 open import Cat.Prelude

From 94d08a2b9bef68b6b3948d6333fdde079df8e85b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Am=C3=A9lia=20Liao?= <me@amelia.how>
Date: Mon, 13 Apr 2026 10:59:16 -0300
Subject: [PATCH 03/12] chore: remove stale comment

---
 src/Data/Rational/Base.lagda.md | 10 +++-------
 1 file changed, 3 insertions(+), 7 deletions(-)

diff --git a/src/Data/Rational/Base.lagda.md b/src/Data/Rational/Base.lagda.md
index 503c0ec00..6cac58e89 100644
--- a/src/Data/Rational/Base.lagda.md
+++ b/src/Data/Rational/Base.lagda.md
@@ -557,13 +557,9 @@ reduceℚ : Ratio → Fraction
 reduceℚ (inc x) = split.choose x
 
 splitℚ : (x : Ratio) → fibre toℚ x
-splitℚ (inc x) = record
-  { fst = split.choose x
-  -- The use of 'recover' here replaces the calculated proof that
-  -- is-split-congruence returns by an invocation of Discrete-ℚ. This
-  -- has much shorter normal forms when applied to concrete values.
-  ; snd = ap inc (split.splitting x .snd)
-  }
+splitℚ (inc x) = record where
+  fst = split.choose x
+  snd = ap inc (split.splitting x .snd)
 
 abstract
   reduce-injective : ∀ x y → reduceℚ x ≡ reduceℚ y → x ≡ y

From 4658a71a8ef57c25efbfa4863c0de5dacfd1354b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Anders=20=C3=85gren=20Thun=C3=A9?= <anders@aathn.org>
Date: Mon, 20 Apr 2026 23:03:38 +0200
Subject: [PATCH 04/12] Define Disc using inductive identity

---
 src/Cat/Abelian/Limits.lagda.md               |   6 +-
 src/Cat/Bi/Instances/Discrete.lagda.md        |  38 ++---
 src/Cat/Diagram/Colimit/Coproduct.lagda.md    |   6 +-
 src/Cat/Diagram/Limit/Product.lagda.md        |   6 +-
 src/Cat/Displayed/Cartesian/Indexing.lagda.md |  16 +-
 src/Cat/Displayed/Instances/Family.lagda.md   |  13 +-
 src/Cat/Instances/Discrete.lagda.md           | 161 ++++++------------
 src/Cat/Instances/Shape/Two.lagda.md          |  16 +-
 src/Cat/Instances/Slice.lagda.md              |  13 +-
 src/Cat/Instances/StrictCat/Cohesive.lagda.md |  52 ++----
 src/Data/Fin/Finite.lagda.md                  |  15 ++
 src/Data/Id/Base.lagda.md                     |   6 -
 12 files changed, 129 insertions(+), 219 deletions(-)

diff --git a/src/Cat/Abelian/Limits.lagda.md b/src/Cat/Abelian/Limits.lagda.md
index 312e00512..a826addff 100644
--- a/src/Cat/Abelian/Limits.lagda.md
+++ b/src/Cat/Abelian/Limits.lagda.md
@@ -167,8 +167,8 @@ $$.
     split-remark = ip.unique ip.π (λ _ → A.idr _) ∙ sym (ip.unique _ πΣδπ) where
       sum-δ-π : ∀ i → ∑ {I} _ (λ j → δ j i A.∘ ip.π j) ≡ ip.π i
       sum-δ-π i = ∑-diagonal-lemma (Abelian→Group-on (A.Abelian-group-on-hom _ _)) {I} i _
-        (A.eliml refl) λ j i≠j →
-          ap₂ A._∘_ (δᵢⱼ j i (λ e → i≠j (sym e)) (j ≡ᵢ? i)) refl ∙ A.∘-zero-l
+        (A.eliml (ap (δ' i i) (prop! {x = i ≡ᵢ? i} {yes reflᵢ})))
+        λ j i≠j → ap₂ A._∘_ (δᵢⱼ j i (λ e → i≠j (sym e)) (j ≡ᵢ? i)) refl ∙ A.∘-zero-l
 
       πΣδπ : ∀ i → ip.π i A.∘ split ≡ ip.π i
       πΣδπ i =
@@ -227,7 +227,7 @@ f\pi_i$, then we certainly have $(\sum_i f'_i) \iota_j$ = $f$!
       where
         remark = ∑-diagonal-lemma (Abelian→Group-on (A.Abelian-group-on-hom _ _)) {I} i
           (λ j → (f j A.∘ ip.π j) A.∘ ip.tuple (λ v → δ i v))
-          (A.cancelr ip.commute)
+          (A.cancelr (ip.commute ∙ ap (δ' i i) (prop! {x = i ≡ᵢ? i} {yes reflᵢ})))
           λ j i≠j → A.pullr (ip.commute ∙ δᵢⱼ i j i≠j (i ≡ᵢ? j))
                   ∙ A.∘-zero-r
 ```
diff --git a/src/Cat/Bi/Instances/Discrete.lagda.md b/src/Cat/Bi/Instances/Discrete.lagda.md
index f337b6dc0..e5a3b9ef2 100644
--- a/src/Cat/Bi/Instances/Discrete.lagda.md
+++ b/src/Cat/Bi/Instances/Discrete.lagda.md
@@ -38,8 +38,8 @@ Locally-discrete .Hom x y = Disc' (el (C.Hom x y) (C.Hom-set x y))
 Locally-discrete .id = C.id
 Locally-discrete .compose = make-bifunctor λ where
   .F₀ A B → A C.∘ B
-  .lmap → ap (C._∘ _)
-  .rmap → ap (_ C.∘_)
+  .lmap → apᵢ (C._∘ _)
+  .rmap → apᵢ (_ C.∘_)
   .lmap-id    → refl
   .rmap-id    → refl
   .lmap-∘ f g → prop!
@@ -47,25 +47,25 @@ Locally-discrete .compose = make-bifunctor λ where
   .lrmap  f g → prop!
 Locally-discrete .unitor-l = to-natural-iso ni where
   ni : make-natural-iso _ _
-  ni .make-natural-iso.eta x = sym (C.idl x)
-  ni .make-natural-iso.inv x = C.idl x
-  ni .make-natural-iso.eta∘inv x = ∙-invr (C.idl x)
-  ni .make-natural-iso.inv∘eta x = ∙-invl (C.idl x)
-  ni .make-natural-iso.natural x y f = C.Hom-set _ _ _ _ _ _
+  ni .make-natural-iso.eta x = Id≃path.from $ sym (C.idl x)
+  ni .make-natural-iso.inv x = Id≃path.from $ C.idl x
+  ni .make-natural-iso.eta∘inv x = prop!
+  ni .make-natural-iso.inv∘eta x = prop!
+  ni .make-natural-iso.natural x y f = prop!
 Locally-discrete .unitor-r = to-natural-iso ni where
   ni : make-natural-iso _ _
-  ni .make-natural-iso.eta x = sym (C.idr x)
-  ni .make-natural-iso.inv x = C.idr x
-  ni .make-natural-iso.eta∘inv x = ∙-invr (C.idr x)
-  ni .make-natural-iso.inv∘eta x = ∙-invl (C.idr x)
-  ni .make-natural-iso.natural x y f = C.Hom-set _ _ _ _ _ _
+  ni .make-natural-iso.eta x = Id≃path.from $ sym (C.idr x)
+  ni .make-natural-iso.inv x = Id≃path.from $ C.idr x
+  ni .make-natural-iso.eta∘inv x = prop!
+  ni .make-natural-iso.inv∘eta x = prop!
+  ni .make-natural-iso.natural x y f = prop!
 Locally-discrete .associator = to-natural-iso ni where
   ni : make-natural-iso _ _
-  ni .make-natural-iso.eta x = sym (C.assoc _ _ _)
-  ni .make-natural-iso.inv x = C.assoc _ _ _
-  ni .make-natural-iso.eta∘inv x = ∙-invr (C.assoc _ _ _)
-  ni .make-natural-iso.inv∘eta x = ∙-invl (C.assoc _ _ _)
-  ni .make-natural-iso.natural x y f = C.Hom-set _ _ _ _ _ _
-Locally-discrete .triangle f g = C.Hom-set _ _ _ _ _ _
-Locally-discrete .pentagon f g h i = C.Hom-set _ _ _ _ _ _
+  ni .make-natural-iso.eta x = Id≃path.from $ sym (C.assoc _ _ _)
+  ni .make-natural-iso.inv x = Id≃path.from $ C.assoc _ _ _
+  ni .make-natural-iso.eta∘inv x = prop!
+  ni .make-natural-iso.inv∘eta x = prop!
+  ni .make-natural-iso.natural x y f = prop!
+Locally-discrete .triangle f g = prop!
+Locally-discrete .pentagon f g h i = prop!
 ```
diff --git a/src/Cat/Diagram/Colimit/Coproduct.lagda.md b/src/Cat/Diagram/Colimit/Coproduct.lagda.md
index bbb4f846d..9860f0ca6 100644
--- a/src/Cat/Diagram/Colimit/Coproduct.lagda.md
+++ b/src/Cat/Diagram/Colimit/Coproduct.lagda.md
@@ -83,11 +83,9 @@ is-colimit→is-coproduct {a} {b} {K} {eta} colim = coprod where
   copair-commutes
     : ∀ {y} {p1 : Hom a y} {p2 : Hom b y}
     → {i j : Bool}
-    → (p : i ≡ j)
+    → (p : i ≡ᵢ j)
     → copair p1 p2 j ∘ D .F₁ p ≡ copair p1 p2 i
-  copair-commutes {p1 = p1} {p2 = p2} =
-      J (λ _ p → copair p1 p2 _ ∘ D .F₁ p ≡ copair p1 p2 _)
-        (elimr (D .F-id))
+  copair-commutes {p1 = p1} {p2 = p2} reflᵢ = elimr (D .F-id)
 
   coprod : is-coproduct C (eta .η true) (eta .η false)
   coprod .[_,_] f g = colim.universal (copair f g) copair-commutes
diff --git a/src/Cat/Diagram/Limit/Product.lagda.md b/src/Cat/Diagram/Limit/Product.lagda.md
index 3335bd952..36ee6a996 100644
--- a/src/Cat/Diagram/Limit/Product.lagda.md
+++ b/src/Cat/Diagram/Limit/Product.lagda.md
@@ -93,11 +93,9 @@ simple enough to establish by appropriately shuffling the data.
     pair-commutes
       : ∀ {y} {p1 : Hom y a} {p2 : Hom y b}
       → {i j : Bool}
-      → (p : i ≡ j)
+      → (p : i ≡ᵢ j)
       → D .F₁ p ∘ pair p1 p2 i ≡ pair p1 p2 j
-    pair-commutes {p1 = p1} {p2 = p2} =
-        J (λ _ p → D .F₁ p ∘ pair p1 p2 _ ≡ pair p1 p2 _)
-          (eliml (D .F-id))
+    pair-commutes {p1 = p1} {p2 = p2} reflᵢ = eliml (D .F-id)
 
     prod : is-product C (eps .η true) (eps .η false)
     prod .⟨_,_⟩ f g = lim.universal (pair f g) pair-commutes
diff --git a/src/Cat/Displayed/Cartesian/Indexing.lagda.md b/src/Cat/Displayed/Cartesian/Indexing.lagda.md
index f8ecb400e..67168cd57 100644
--- a/src/Cat/Displayed/Cartesian/Indexing.lagda.md
+++ b/src/Cat/Displayed/Cartesian/Indexing.lagda.md
@@ -193,15 +193,15 @@ base-changes
   → Functor
       (Locally-discrete (B ^op) .Prebicategory.Hom a b)
       Cat[ Fibre E a , Fibre E b ]
-base-changes = Disc'-adjunct base-change
+base-changes = Disc-diagram base-change
 
 base-change-coherence
-  : ∀ {a b} {b' : Ob[ b ]} {f g : Hom a b} (p : f ≡ g)
+  : ∀ {a b} {b' : Ob[ b ]} {f g : Hom a b} (p : f ≡ᵢ g)
   → π* g b' ∘' base-changes .F₁ p .η b'
-  ≡[ idr _ ∙ sym p ]
+  ≡[ idr _ ∙ sym (Id≃path.to p) ]
     π* f b'
-base-change-coherence {b' = b'} {f} = J
-  (λ g p → π* g b' ∘' base-changes .F₁ p .η b' ≡[ idr _ ∙ sym p ] π* f b')
+base-change-coherence {b' = b'} {f} = Jᵢ
+  (λ g p → π* g b' ∘' base-changes .F₁ p .η b' ≡[ idr _ ∙ sym (Id≃path.to p) ] π* f b')
   (elimr' refl Regularity.reduce!)
 ```
 
@@ -266,7 +266,7 @@ is by definition of the unitor.
 Fibres .lax .left-unit f = ext λ a' →
   π*.uniquep₂ _ refl refl _ _
     (begin
-      _ ≡[]⟨ Fib.pulllf (base-change-coherence _) ⟩
+      _ ≡[]⟨ Fib.pulllf (base-change-coherence (Id≃path.from (idr f))) ⟩
       _ ≡[]⟨ Fib.pulllf (π*.commutesv _) ⟩
       _ ≡[]⟨ pullr[] _ (π*.commutesv id') ⟩
       _ ∎[])
@@ -309,7 +309,7 @@ of the unitor, and the top square is by definition of `rebase`{.Agda}
 Fibres .lax .right-unit f = ext λ a' →
   π*.uniquep₂ _ refl refl _ _
     (begin
-      _ ≡[]⟨ Fib.pulllf (base-change-coherence _) ⟩
+      _ ≡[]⟨ Fib.pulllf (base-change-coherence (Id≃path.from (idl f))) ⟩
       _ ≡[]⟨ Fib.pulllf (π*.commutesv _) ⟩
       _ ≡[]⟨ extendr[] id-comm (π*.commutesp _ _) ⟩
       _ ≡[]⟨ eliml[] _ (π*.commutesv _) ⟩
@@ -368,7 +368,7 @@ lifts, by the commutativity of the following diagram.
 ```agda
 Fibres .lax .hexagon f g h = ext λ a' → π*.uniquep₂ _ refl _ _ _
   (begin
-    _ ≡[]⟨ Fib.pulllf (base-change-coherence _) ⟩
+    _ ≡[]⟨ Fib.pulllf (base-change-coherence (Id≃path.from (assoc _ _ _))) ⟩
     _ ≡[]⟨ Fib.pulllf (π*.commutesv _) ⟩
     _ ≡[]⟨ extendr[] _ (π*.commutesv _) ⟩
     _ ∎[]
diff --git a/src/Cat/Displayed/Instances/Family.lagda.md b/src/Cat/Displayed/Instances/Family.lagda.md
index 1e679c78d..0712ccbe8 100644
--- a/src/Cat/Displayed/Instances/Family.lagda.md
+++ b/src/Cat/Displayed/Instances/Family.lagda.md
@@ -151,15 +151,13 @@ the family fibration is fibrewise univalent whenever $\cC$ is.
 ```agda
 module _ {ℓ} (X : Set ℓ) where
   private
-    lift-f = Disc'-adjunct {C = C} {iss = is-hlevel-suc 2 (X .is-tr)}
+    lift-f = Disc-diagram {C = C} {iss = is-hlevel-suc 2 (X .is-tr)}
     module F = Cat.Reasoning (Fibre Family X)
 
   Families→functors : Functor (Fibre Family X) Cat[ Disc' X , C ]
-  Families→functors .F₀ = Disc'-adjunct
+  Families→functors .F₀ = Disc-diagram
   Families→functors .F₁ f .η = f
-  Families→functors .F₁ {X} {Y} f .is-natural x y =
-    J (λ y p → f y ∘ lift-f X .F₁ p ≡ lift-f Y .F₁ p ∘ f x)
-      (ap (f x ∘_) (lift-f X .F-id) ∙∙ id-comm ∙∙ ap (_∘ f x) (sym (lift-f Y .F-id)))
+  Families→functors .F₁ {X} {Y} f .is-natural x y reflᵢ = id-comm
   Families→functors .F-id = ext λ _ → refl
   Families→functors .F-∘ f g =
     ap (Families→functors .F₁) (transport-refl _) ∙ ext (λ i → refl)
@@ -172,9 +170,8 @@ module _ {ℓ} (X : Set ℓ) where
   Families→functors-is-iso : is-precat-iso Families→functors
   Families→functors-is-iso .has-is-ff = Families→functors-is-ff
   Families→functors-is-iso .has-is-iso = is-iso→is-equiv $ iso F₀
-    (λ x → Functor-path (λ _ → refl)
-      (J (λ _ p → lift-f (x .F₀) .F₁ p ≡ x .F₁ p)
-          (lift-f (x .F₀) .F-id ∙ sym (x .F-id))))
+    (λ x → Functor-path (λ _ → refl) λ where
+      reflᵢ → sym (x .F-id))
     (λ x → refl)
 
   Families-are-categories : is-category C → is-category (Fibre Family X)
diff --git a/src/Cat/Instances/Discrete.lagda.md b/src/Cat/Instances/Discrete.lagda.md
index 7b730ca5c..e5f70be42 100644
--- a/src/Cat/Instances/Discrete.lagda.md
+++ b/src/Cat/Instances/Discrete.lagda.md
@@ -8,6 +8,7 @@ open import Cat.Groupoid
 open import Cat.Morphism
 open import Cat.Prelude
 
+open import Data.Id.Properties
 open import Data.Id.Base
 open import Data.Dec
 
@@ -37,20 +38,22 @@ open _=>_
 Given a [[groupoid]] $A$, we can see $A$ as a [[category]] with
 space of objects $A$ and path types $x \equiv y$ as $\hom$-sets $x \to
 y$. When $A$ is a [[set]], we call this the **discrete category** on $A$.
+For technical reasons, we prefer to define this category using the
+[[inductive identity]] type instead of the path type.
 
 ```agda
 Disc : (A : Type ℓ) → is-groupoid A → Precategory ℓ ℓ
-Disc A A-grpd .Ob = A
-Disc A A-grpd .Hom = _≡_
-Disc A A-grpd .Hom-set = A-grpd
-Disc A A-grpd .id = refl
-Disc A A-grpd ._∘_ p q = q ∙ p
-Disc A A-grpd .idr _ = ∙-idl _
-Disc A A-grpd .idl _ = ∙-idr _
-Disc A A-grpd .assoc _ _ _ = sym (∙-assoc _ _ _)
+Disc A A-grpd .Ob          = A
+Disc A A-grpd .Hom         = _≡ᵢ_
+Disc A A-grpd .Hom-set     = ≡ᵢ-is-hlevel' {n = 2} A-grpd
+Disc A A-grpd .id          = reflᵢ
+Disc A A-grpd ._∘_ p q     = q ∙ᵢ p
+Disc A A-grpd .idr _       = refl
+Disc A A-grpd .idl _       = ∙ᵢ-idr _
+Disc A A-grpd .assoc p q r = sym (∙ᵢ-assoc r q p)
 
 Disc' : Set ℓ → Precategory ℓ ℓ
-Disc' A = Disc ∣ A ∣ h where abstract
+Disc' A = Disc ∣ A ∣ h module Disc' where abstract
   h : is-groupoid ∣ A ∣
   h = is-hlevel-suc 2 (A .is-tr)
 ```
@@ -60,26 +63,12 @@ By construction, this is a [[univalent|univalent category]]
 
 ```agda
 Disc-is-category : ∀ {A : Type ℓ} {A-grpd} → is-category (Disc A A-grpd)
-Disc-is-category .to-path is = is .to
-Disc-is-category .to-path-over is = ≅-pathp _ _ _ λ i j → is .to (i ∧ j)
+Disc-is-category .to-path is              = Id≃path.to (is .to)
+Disc-is-category .to-path-over {a = a} is with is .to in w
+... | reflᵢ = ≅-pathp _ _ _ (Id≃path.to (symᵢ w))
 
 Disc-is-groupoid : ∀ {A : Type ℓ} {A-grpd} → is-pregroupoid (Disc A A-grpd)
-Disc-is-groupoid p = make-invertible _ (sym p) (∙-invl p) (∙-invr p)
-```
-
-We can lift any function between the underlying types to a functor
-between discrete categories. This is because every function
-automatically respects equality in a functorial way.
-
-```agda
-lift-disc
-  : ∀ {A : Set ℓ} {B : Set ℓ'}
-  → (∣ A ∣ → ∣ B ∣)
-  → Functor (Disc' A) (Disc' B)
-lift-disc f .F₀ = f
-lift-disc f .F₁ = ap f
-lift-disc f .F-id = refl
-lift-disc f .F-∘ p q = ap-∙ f q p
+Disc-is-groupoid p = make-invertible _ (symᵢ p) (∙ᵢ-invl p) (∙ᵢ-invr p)
 ```
 
 <!--
@@ -98,106 +87,63 @@ Codisc' x .assoc _ _ _ = refl
 
 ## Diagrams in Disc(X)
 
-If $X$ is a [[discrete]] type, then it is in
-particular a [[set]], and we can make diagrams of shape
-$\rm{Disc}(X)$ in some category $\cC$, using the decidable
-equality on $X$ to improve computation. We note that the decidable
-equality is _superfluous_ information: the construction `Disc'`{.Agda}
-above extends into a [[left adjoint]] to the `Ob`{.Agda} functor.
+Because the morphisms in a discrete category are identifications, and
+functions respect equality, any function on objects out of a discrete
+category induces a functor.
 
 ```agda
 Disc-diagram
-  : ∀ {X : Set ℓ} ⦃ _ : Discrete ∣ X ∣ ⦄
-  → (∣ X ∣ → Ob C)
-  → Functor (Disc' X) C
-Disc-diagram {C = C} {X = X} ⦃ d ⦄ f = F where
+  : {X : Type ℓ} {iss : is-groupoid X}
+  → (X → Ob C)
+  → Functor (Disc X iss) C
+Disc-diagram {C = C} {X = X} f = F where
   module C = Precategory C
 
-  P : ∣ X ∣ → ∣ X ∣ → Type _
-  P x y = C.Hom (f x) (f y)
-
-  go : ∀ {x y : ∣ X ∣} → x ≡ y → Dec (x ≡ᵢ y) → P x y
-  go {x} {.x} p (yes reflᵢ) = C.id
-  go {x} {y}  p (no ¬p)     = absurd (¬p (Id≃path.from p))
+  F : Functor _ _
+  F .F₀       = f
+  F .F₁ reflᵢ = C.id
+  F .F-id     = refl
+  F .F-∘ reflᵢ reflᵢ = sym (C.idl C.id)
 ```
 
-The object part of the functor is the provided $f : X \to
-\rm{Ob}(\cC)$, and the decidable equality is used to prove that
-$f$ respects equality. This is why it's redundant: $f$ automatically
-respects equality, because it's a function! However, by using the
-decision procedure, we get better computational behaviour: Very often,
-$\rm{disc}(x,x)$ will be $\rm{yes}(\refl)$, and
-substitution along $\refl$ is easy to deal with.
-
+<!--
 ```agda
-  F : Functor _ _
-  F .F₀ = f
-  F .F₁ {x} {y} p = go p (x ≡ᵢ? y)
+Disc-diagram!
+  : ∀ ⦃ iss : H-Level {ℓ} X 3 ⦄
+  → (X → Ob C)
+  → Functor (Disc X (hlevel 3)) C
+Disc-diagram! = Disc-diagram
 ```
+-->
 
-Proving that our our $F_1$ is functorial involves a bunch of tedious
-computations with equalities and a whole waterfall of absurd cases:
+As a corollary, we can lift any function between underlying types to a
+functor between discrete categories.
 
 ```agda
-  F .F-id {x} = refl
-  F .F-∘  {x} {y} {z} f g =
-    J (λ y g → ∀ {z} (f : y ≡ z) → go (g ∙ f) (x ≡ᵢ? z) ≡ go f (y ≡ᵢ? z) C.∘ go g (x ≡ᵢ? y))
-      (λ f → J (λ z f → go (refl ∙ f) (x ≡ᵢ? z) ≡ go f (x ≡ᵢ? z) C.∘ C.id) (sym (C.idr _)) f)
-      g f
+lift-disc : {A : Set ℓ} {B : Set ℓ'} → (∣ A ∣ → ∣ B ∣) → Functor (Disc' A) (Disc' B)
+lift-disc {A = A} f = Disc-diagram f
 ```
 
 <!--
 ```agda
-Disc'-adjunct
-  : ∀ { iss : is-groupoid X}
-  → (X → Ob C)
-  → Functor (Disc X iss) C
-Disc'-adjunct {C = C} F .F₀ = F
-Disc'-adjunct {C = C} F .F₁ p = subst (C .Hom (F _) ⊙ F) p (C .id)
-Disc'-adjunct {C = C} F .F-id = transport-refl _
-Disc'-adjunct {C = C} {iss} F .F-∘ {x} {y} {z} f g = path where
-  import Cat.Reasoning C as C
-  go = Disc'-adjunct {C = C} {iss} F .F₁
-  abstract
-    path : go (g ∙ f) ≡ C ._∘_ (go f) (go g)
-    path =
-      J' (λ y z f → ∀ {x} (g : x ≡ y) → go (g ∙ f) ≡ go f C.∘ go g)
-        (λ x g → subst-∙ (C .Hom (F _) ⊙ F) _ _ _
-              ∙∙ transport-refl _
-              ∙∙ C.introl (transport-refl _))
-        f {x} g
-
-Disc-adjunct
-  : ∀ ⦃ iss : H-Level {ℓ} X 3 ⦄
-  → (X → Ob C)
-  → Functor (Disc X (hlevel 3)) C
-Disc-adjunct = Disc'-adjunct {iss = hlevel 3}
-
 Disc-into
   : ∀ {ℓ} (X : Set ℓ)
   → (F : C .Ob → ∣ X ∣)
-  → (F₁ : ∀ {x y} → C .Hom x y → F x ≡ F y)
+  → (F₁ : ∀ {x y} → C .Hom x y → F x ≡ᵢ F y)
   → Functor C (Disc' X)
-Disc-into X F F₁ .F₀ = F
-Disc-into X F F₁ .F₁ = F₁
-Disc-into X F F₁ .F-id = X .is-tr _ _ _ _
-Disc-into X F F₁ .F-∘ _ _ = X .is-tr _ _ _ _
-```
--->
+Disc-into X F F₁ .F₀      = F
+Disc-into X F F₁ .F₁      = F₁
+Disc-into X F F₁ .F-id    = ≡ᵢ-is-hlevel' {n = 1} (X .is-tr) _ _ _ _
+Disc-into X F F₁ .F-∘ _ _ = ≡ᵢ-is-hlevel' {n = 1} (X .is-tr) _ _ _ _
 
-<!--
-```agda
 Disc-natural
   : ∀ {X : Set ℓ}
   → {F G : Functor (Disc' X) C}
   → (∀ x → C .Hom (F .F₀ x) (G .F₀ x))
   → F => G
 Disc-natural fam .η = fam
-Disc-natural {C = C} {F = F} {G = G} fam .is-natural x y f =
-  J (λ y p → fam y C.∘ F .F₁ p ≡ G .F₁ p C.∘ fam x)
-    (C.elimr (F .F-id) ∙ C.introl (G .F-id))
-    f
-  where module C = Cat.Reasoning C
+Disc-natural {C = C} {F = F} {G = G} fam .is-natural x y reflᵢ =
+  C.elimr (F .F-id) ∙ C.introl (G .F-id) where module C = Cat.Reasoning C
 
 Disc-natural₂
   : ∀ {X : Type ℓ} {Y : Type ℓ'}
@@ -206,12 +152,8 @@ Disc-natural₂
   → ((x : X × Y) → C .Hom (F .F₀ x) (G .F₀ x))
   → F => G
 Disc-natural₂ fam .η = fam
-Disc-natural₂ {C = C} {F = F} {G = G} fam .is-natural x y (p , q) =
-  J (λ y' p' → fam y' C.∘ F .F₁ (ap fst p' , ap snd p')
-             ≡ G .F₁ (ap fst p' , ap snd p') C.∘ fam x)
-    (C.elimr (F .F-id) ∙ C.introl (G .F-id))
-    (Σ-pathp p q)
-  where module C = Cat.Reasoning C
+Disc-natural₂ {C = C} {F = F} {G = G} fam .is-natural x y (reflᵢ , reflᵢ) =
+  C.elimr (F .F-id) ∙ C.introl (G .F-id) where module C = Cat.Reasoning C
 
 open _≅_
 open Inverses
@@ -219,8 +161,9 @@ Disc-natural-iso : ∀ {X : Set ℓ}
   → {F G : Functor (Disc' X) C}
   → (∀ x → Isomorphism C (F .F₀ x) (G .F₀ x))
   → F ≅ⁿ G
-Disc-natural-iso isos .to = Disc-natural λ x → isos x .to
-Disc-natural-iso isos .from = Disc-natural λ x → isos x .from
-Disc-natural-iso isos .inverses = to-inversesⁿ (λ x → isos x .inverses .invl) (λ x → isos x .inverses .invr)
+Disc-natural-iso isos .to       = Disc-natural λ x → isos x .to
+Disc-natural-iso isos .from     = Disc-natural λ x → isos x .from
+Disc-natural-iso isos .inverses =
+  to-inversesⁿ (λ x → isos x .inverses .invl) (λ x → isos x .inverses .invr)
 ```
 -->
diff --git a/src/Cat/Instances/Shape/Two.lagda.md b/src/Cat/Instances/Shape/Two.lagda.md
index 40e8426d7..59cc3b758 100644
--- a/src/Cat/Instances/Shape/Two.lagda.md
+++ b/src/Cat/Instances/Shape/Two.lagda.md
@@ -62,17 +62,7 @@ defined above.
     p false = refl
     p true  = refl
 
-    q : ∀ {x y} (f : x ≡ y) → _
-    q {false} {false} p =
-      F .F₁ p           ≡⟨ ap (F .F₁) prop! ⟩
-      F .F₁ refl        ≡⟨ F .F-id ⟩
-      id                ≡˘⟨ transport-refl id ⟩
-      transport refl id ∎
-    q {true} {true} p =
-      F .F₁ p           ≡⟨ ap (F .F₁) prop! ⟩
-      F .F₁ refl        ≡⟨ F .F-id ⟩
-      id                ≡˘⟨ transport-refl id ⟩
-      transport refl id ∎
-    q {false} {true} p = absurd (true≠false (sym p))
-    q {true} {false} p = absurd (true≠false p)
+    q : ∀ {x y} (f : x ≡ᵢ y) → _
+    q {true}  reflᵢ = F .F-id
+    q {false} reflᵢ = F .F-id
 ```
diff --git a/src/Cat/Instances/Slice.lagda.md b/src/Cat/Instances/Slice.lagda.md
index 793f4262a..86f979d53 100644
--- a/src/Cat/Instances/Slice.lagda.md
+++ b/src/Cat/Instances/Slice.lagda.md
@@ -640,10 +640,10 @@ dependent function is automatically a natural transformation.
 
       nt : F => G
       nt .η = eta
-      nt .is-natural _ _ = J (λ _ p → eta _ ⊙ F .F₁ p ≡ G .F₁ p ⊙ eta _) $
-        eta _ ⊙ F .F₁ refl ≡⟨ ap (eta _ ⊙_) (F .F-id) ⟩
-        eta _              ≡˘⟨ ap (_⊙ eta _) (G .F-id) ⟩
-        G .F₁ refl ⊙ eta _ ∎
+      nt .is-natural _ _ reflᵢ =
+        eta _ ⊙ F .F₁ reflᵢ ≡⟨ ap (eta _ ⊙_) (F .F-id) ⟩
+        eta _               ≡˘⟨ ap (_⊙ eta _) (G .F-id) ⟩
+        G .F₁ reflᵢ ⊙ eta _ ∎
 ```
 
 <!--
@@ -665,10 +665,7 @@ _isomorphic_ to $p$ in $\Sets/I$, it's actually _identical_ to $p$!
   Total-space-is-eso : is-split-eso Total-space
   Total-space-is-eso fam = functor , path→iso path where
     functor : Functor _ _
-    functor .F₀ i    = el! (fibre (fam .map) i)
-    functor .F₁ p    = subst (fibre (fam .map)) p
-    functor .F-id    = funext transport-refl
-    functor .F-∘ f g = funext (subst-∙ (fibre (fam .map)) _ _)
+    functor = Disc-diagram (λ i → el! (fibre (fam .map) i))
 
     path : Total-space .F₀ functor ≡ fam
     path = /-Obj-path (n-ua (Total-equiv _  e⁻¹)) (ua→ λ a → sym (a .snd .snd))
diff --git a/src/Cat/Instances/StrictCat/Cohesive.lagda.md b/src/Cat/Instances/StrictCat/Cohesive.lagda.md
index 3f0a0e232..bcbb18341 100644
--- a/src/Cat/Instances/StrictCat/Cohesive.lagda.md
+++ b/src/Cat/Instances/StrictCat/Cohesive.lagda.md
@@ -79,8 +79,8 @@ functor `Γ`{.Agda} we defined above. Then we define the adjunction
 Disc : Functor (Sets ℓ) (Strict-cats ℓ ℓ)
 Disc .F₀ S = Disc' S , S .is-tr
 Disc .F₁ = lift-disc
-Disc .F-id = Functor-path (λ x → refl) λ f → refl
-Disc .F-∘ _ _ = Functor-path (λ x → refl) λ f → refl
+Disc .F-id = Functor-path (λ x → refl) λ f → prop!
+Disc .F-∘ _ _ = Functor-path (λ x → refl) λ f → prop!
 
 Disc⊣Γ : Disc {ℓ} ⊣ Γ
 Disc⊣Γ = adj where
@@ -121,38 +121,16 @@ morphisms in discrete categories are paths, for a map $x \equiv y$ (in
 identity map suffices.
 
 ```agda
-  adj .counit = NT (λ x → F x) nat where
-    F : (x : ⌞ Strict-cats ℓ ℓ ⌟)
-      → Functor (Disc' (el _ (x .snd))) _
-    F X .F₀ x = x
-    F X .F₁ p = subst (X .fst .Hom _) p (X .fst .id) {- 1 -}
-    F X .F-id = transport-refl _
-    F X .F-∘ = lemma {A = X}
+  adj .counit = record where
+    η x = Disc-diagram λ x → x
+    is-natural x y f = Functor-path (λ x → refl) λ where
+      reflᵢ → sym (f .F-id)
 ```
 
-<!--
-```agda
-    abstract
-      nat : (x y : ⌞ Strict-cats ℓ ℓ ⌟)
-            (f : Strict-cats ℓ ℓ .Precategory.Hom x y)
-          → (F y F∘ (Disc F∘ Γ) .F₁ f) ≡ (f F∘ F x)
-      nat x y f =
-        Functor-path (λ x → refl)
-           (J' (λ x y p → subst (Y.Hom _) (ap (f .F₀) p) Y.id
-                        ≡ f .F₁ (subst (X.Hom _) p X.id))
-               λ _ → transport-refl _
-                  ∙∙ sym (f .F-id)
-                  ∙∙ ap (f .F₁) (sym (transport-refl _)))
-         where
-           module X = Precategory (x .fst)
-           module Y = Precategory (y .fst)
-```
--->
-
 Fortunately the triangle identities are straightforwardly checked.
 
 ```agda
-  adj .zig {x} = Functor-path (λ x i → x) λ f → x .is-tr _ _ _ _
+  adj .zig {x} = Functor-path (λ x i → x) λ f → prop!
   adj .zag = refl
 ```
 
@@ -185,10 +163,10 @@ both directions:
 Γ⊣Codisc : Γ ⊣ Codisc {ℓ}
 Γ⊣Codisc = adj where
   adj : _ ⊣ _
-  adj .unit =
-    NT (λ x → record { F₀ = λ x → x ; F₁ = λ _ → lift tt
-                     ; F-id = refl ; F-∘ = λ _ _ → refl })
-       λ x y f → Functor-path (λ _ → refl) λ _ → refl
+  adj .unit = record where
+    η x = record
+      { F₀ = λ x → x ; F₁ = λ _ → lift tt ; F-id = refl ; F-∘ = λ _ _ → refl }
+    is-natural x y f = Functor-path (λ _ → refl) λ _ → refl
   adj .counit = NT (λ _ x → x) λ x y f i o → f o
   adj .zig = refl
   adj .zag = Functor-path (λ _ → refl) λ _ → refl
@@ -311,8 +289,8 @@ quotient.
 Π₀⊣Disc : Π₀ ⊣ Disc {ℓ}
 Π₀⊣Disc = adj where
   adj : _ ⊣ _
-  adj .unit .η x = Disc-into _ inc quot
-  adj .unit .is-natural x y f = Functor-path (λ x → refl) λ _ → squash _ _ _ _
+  adj .unit .η x = Disc-into _ inc λ m → Id≃path.from (quot m)
+  adj .unit .is-natural x y f = Functor-path (λ x → refl) λ _ → prop!
 ```
 
 The adjunction `counit`{.Agda} is an assignment of functions
@@ -321,7 +299,7 @@ isomorphism: the set of connected components of a discrete category is
 the same set we started with.
 
 ```agda
-  adj .counit .η X = Quot-elim (λ _ → X .is-tr) (λ x → x) λ x y r → r
+  adj .counit .η X = Quot-elim (λ _ → X .is-tr) (λ x → x) λ x y r → Id≃path.to r
   adj .counit .is-natural x y f = ext λ _ → refl
 ```
 
@@ -329,7 +307,7 @@ The triangle identities are again straightforwardly checked.
 
 ```agda
   adj .zig {x} = ext λ _ → refl
-  adj .zag = Functor-path (λ x → refl) λ f → refl
+  adj .zag = Functor-path (λ x → refl) λ f → prop!
 ```
 
 Furthermore, we can prove that the connected components of a product
diff --git a/src/Data/Fin/Finite.lagda.md b/src/Data/Fin/Finite.lagda.md
index 0f20d0d3c..9009fc0b5 100644
--- a/src/Data/Fin/Finite.lagda.md
+++ b/src/Data/Fin/Finite.lagda.md
@@ -304,6 +304,14 @@ complicated.</summary>
     abstract
       s : ∀ {i n} → H-Level (A i) (2 + n)
       s {i} = basic-instance 2 (Listing→is-set (coe (λ i → Listing (A i)) i1 i li))
+
+  Listing-≡ᵢ : ∀ {A : Type ℓ} ⦃ _ : Listing A ⦄ {x y : A} → Listing (x ≡ᵢ y)
+  Listing-≡ᵢ ⦃ l ⦄ {x} {y} = Listing-prop where
+    instance
+      _ = Listing→Discrete l
+      _ = basic-instance 2 (Listing→is-set l)
+      d : ∀ {x y} → Dec (x ≡ᵢ y)
+      d {x} {y} = x ≡ᵢ? y
 ```
 -->
 
@@ -612,6 +620,9 @@ instance
   Finite-PathP
     : ∀ {A : I → Type ℓ} ⦃ s : Finite (A i1) ⦄ {x y}
     → Finite (PathP A x y)
+  Finite-≡ᵢ
+    : ∀ {A : Type ℓ} ⦃ s : Finite A ⦄ {x y : A}
+    → Finite (x ≡ᵢ y)
 
   Finite-∥-∥ : ⦃ _ : Dec A ⦄ → Finite ∥ A ∥
 ```
@@ -651,6 +662,10 @@ instance
     a ← fa
     pure (Listing-PathP ⦃ a ⦄)
 
+  Finite-≡ᵢ ⦃ fa ⦄ = do
+    a ← fa
+    pure (Listing-≡ᵢ ⦃ a ⦄)
+
   Finite-Lift ⦃ fa ⦄ = do
     a ← fa
     pure (Listing-Lift ⦃ a ⦄)
diff --git a/src/Data/Id/Base.lagda.md b/src/Data/Id/Base.lagda.md
index 9414100a7..48bb6081b 100644
--- a/src/Data/Id/Base.lagda.md
+++ b/src/Data/Id/Base.lagda.md
@@ -159,12 +159,6 @@ abstract
   ≡?-no : ∀ {ℓ} {A : Type ℓ} ⦃ d : Discrete A ⦄ {x y : A} (p : x ≠ y) → d .decide x y ≡ᵢ no p
   ≡?-no = decide-no _
 
-  discrete-id-yes : ∀ {ℓ} {A : Type ℓ} ⦃ d : Discrete A ⦄ {x : A} (p : Dec (x ≡ x)) → discrete-id d p ≡ yes reflᵢ
-  discrete-id-yes {x = x} p
-    rewrite decide-yes ⦃ prop-instance (Discrete→is-set auto x x) ⦄ p refl =
-    ap yes (transport-refl _)
-
-{-# REWRITE discrete-id-yes #-}
 {-# DISPLAY discrete-id {ℓ} {A} {x} {y} d _ = _≡ᵢ?_ {ℓ} {A} x y ⦃ d ⦄ #-}
 
 Discrete-inj'

From a140940f7064e6bda1b5f096bef6beac2e93b0ed Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Am=C3=A9lia=20Liao?= <me@amelia.how>
Date: Mon, 20 Apr 2026 19:52:38 -0300
Subject: [PATCH 05/12] chore: actually remove --rewriting

---
 1lab.agda-lib         | 1 -
 src/Prim/Kan.lagda.md | 2 --
 2 files changed, 3 deletions(-)

diff --git a/1lab.agda-lib b/1lab.agda-lib
index 015a9c8f9..8eb5cba73 100644
--- a/1lab.agda-lib
+++ b/1lab.agda-lib
@@ -7,7 +7,6 @@ flags:
   --cubical
   --no-load-primitives
   --postfix-projections
-  --rewriting
   --guardedness
   --two-level
   -W noUnsupportedIndexedMatch
diff --git a/src/Prim/Kan.lagda.md b/src/Prim/Kan.lagda.md
index 76c2ae52e..89f223a27 100644
--- a/src/Prim/Kan.lagda.md
+++ b/src/Prim/Kan.lagda.md
@@ -64,8 +64,6 @@ _≡_ {A = A} = PathP (λ i → A)
 
 <!--
 ```agda
-{-# BUILTIN REWRITE _≡_ #-}
-
 caseⁱ_of_ : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (x : A) → ((y : A) → x ≡ y → B) → B
 caseⁱ x of f = f x (λ i → x)
 

From 194fecd070c035dd0420f5627910c9cad11d4acc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Am=C3=A9lia=20Liao?= <me@amelia.how>
Date: Mon, 20 Apr 2026 20:58:13 -0300
Subject: [PATCH 06/12] chore: use Prop over @irr for definitional irrelevance

---
 1lab.agda-lib                                 |   2 +
 src/1Lab/Type.lagda.md                        | 258 ++++++++++++++----
 src/1Lab/Univalence.lagda.md                  |  12 +-
 src/Algebra/Ring/Module/Multilinear.lagda.md  |   2 +-
 src/Cat/Bi/Instances/Discrete.lagda.md        |  32 ++-
 src/Cat/Displayed/Instances/Family.lagda.md   |   4 +-
 src/Cat/Instances/Discrete.lagda.md           |  89 +++---
 src/Cat/Instances/Shape/Two.lagda.md          |   2 +-
 src/Cat/Instances/Slice.lagda.md              |   2 +-
 src/Cat/Instances/StrictCat/Cohesive.lagda.md |   4 +-
 src/Data/Bool/Base.lagda.md                   |   2 +-
 src/Data/Bool/Order.lagda.md                  |  14 +-
 src/Data/Dec/Base.lagda.md                    |   5 -
 src/Data/Fin/Base.lagda.md                    |   4 +-
 src/Data/Int/HIT.lagda.md                     |  15 +-
 src/Data/Irr.lagda.md                         |  82 +++++-
 src/Data/Nat/DivMod.lagda.md                  |  47 ++--
 src/Data/Nat/Divisible/GCD.lagda.md           |   7 +-
 src/Data/Nat/Order.lagda.md                   |   4 +-
 src/Data/Nat/Range.lagda.md                   |   4 +-
 src/Data/Rational/Base.lagda.md               |  14 +-
 src/Homotopy/Space/Delooping.lagda.md         |  25 +-
 src/Logic/Propositional/Classical.lagda.md    |   8 +-
 src/Prim/Type.lagda.md                        |   4 +-
 24 files changed, 423 insertions(+), 219 deletions(-)

diff --git a/1lab.agda-lib b/1lab.agda-lib
index 8eb5cba73..c1c2dc9e9 100644
--- a/1lab.agda-lib
+++ b/1lab.agda-lib
@@ -5,6 +5,7 @@ include:
   _build
 flags:
   --cubical
+  --prop
   --no-load-primitives
   --postfix-projections
   --guardedness
@@ -12,3 +13,4 @@ flags:
   -W noUnsupportedIndexedMatch
   -W noRewriteVariablesBoundInSingleton
   --experimental-lazy-instances
+  --no-experimental-irrelevance
diff --git a/src/1Lab/Type.lagda.md b/src/1Lab/Type.lagda.md
index f53e383d7..e77359e36 100644
--- a/src/1Lab/Type.lagda.md
+++ b/src/1Lab/Type.lagda.md
@@ -4,57 +4,102 @@ module 1Lab.Type where
 
 # Universes {defines="universe"}
 
-A **universe** is a type whose inhabitants are types. In Agda, there is
-a family of universes, which, by default, is called `Set`. Rather
-recently, Agda gained a flag to make `Set` not act like a keyword, and
-allow renaming it in an import declaration from the `Agda.Primitive`
-module.
+A **universe** is a type whose inhabitants are types. In our type
+theory, the most common universe is `Type`{.Agda}, the
+[[univalent|univalence]] universe of [[fibrant]] types.
 
 ```agda
-open import Prim.Type hiding (Prop) public
+open import Prim.Type public
 ```
 
-`Type`{.Agda} is a type itself, so it's a natural question to ask: does
-it belong to a universe? The answer is _yes_. However, Type can not
-belong to itself, or we could reproduce [[Russell's paradox]].
-
-To prevent this, the universes are parametrised by a _`Level`{.Agda}_,
-where the collection of all `ℓ`-sized types is `Type (lsuc ℓ)`:
+Since `Type`{.Agda} is itself a fibrant type (with composition given by
+[[glueing]]), we might want for it to also live in a universe. However,
+a universe closed under `Σ`{.Agda} and [[W-types]], which `Type`{.Agda}
+is, can not code for itself: this is [[Russell's paradox]]. Instead,
+`Type`{.Agda} is parametrised by a _`Level`{.Agda}_, a technical gadget
+which serves to stratify a **hierarchy** of universes to prevent any
+given universe for belonging to itself. In particular, the type
+`Type`{.Agda} belongs to a *successor* universe `Type₁`{.Agda}, and, in
+general, the $\ell$-th universe lives in the $(\ell + 1)$st universe.
 
 ```agda
+_ : Type₁
+_ = Type
+
 _ : (ℓ : Level) → Type (lsuc ℓ)
 _ = λ ℓ → Type ℓ
+```
+
+Every fibrant type lives in exactly one universe, so we can recover by
+unification the `Level`{.Agda} of a given type.
 
+```agda
 level-of : {ℓ : Level} → Type ℓ → Level
 level-of {ℓ} _ = ℓ
 ```
 
-## Built-in types
+The built-in universes are furthermore all **predicative**, which in
+this context means that the *domain* of a family of types also
+influences the universe level at which the product of that family lives.
+To express this, `Level`{.Agda}s are closed under a binary "max"
+operator `_⊔_`{.Agda}.
 
-We re-export the following very important types:
+```agda
+_ : ∀ {ℓ ℓ'} (A : Type ℓ) → (A → Type ℓ') → Type (ℓ ⊔ ℓ')
+_ = λ A B → ((x : A) → B x)
+```
+
+## Lifting
+
+We have mentioned that every fibrant type lives in exactly one universe.
+This is to say that our universes are not **cumulative**. Instead, we
+can define (as a `record`{.Agda} type) a map which `Lift`{.Agda}s a type
+to a higher universe. Considered as a function between universes,
+`Lift`{.Agda} is an [[embedding]]. Moreover, the `Lift`{.Agda} of a type
+is *definitionally isomorphic* to that type.
 
 ```agda
-open import Prim.Data.Sigma public
-open import Prim.Data.Bool public
-open import Prim.Data.Nat hiding (_<_; _≤_) public
+record Lift {a} ℓ (A : Type a) : Type (a ⊔ ℓ) where
+  constructor lift
+  field
+    lower : A
+```
+
+<!--
+```agda
+open Lift public
+
+instance
+  Lift-instance : ∀ {ℓ ℓ'} {A : Type ℓ} → ⦃ A ⦄ → Lift ℓ' A
+  Lift-instance ⦃ x ⦄ = lift x
 ```
+-->
+
+## Built-in type formers
 
-Additionally, we define the empty type:
+The `Type`{.Agda} universes are closed under `Σ`{.Agda}, and the lowest
+universe contains both the [[natural numbers]] `Nat`{.Agda} and the
+[[booleans]] `Bool`{.Agda}.
 
+<!--
 ```agda
-data ⊥ : Type where
+open import Prim.Data.Sigma public
+open import Prim.Data.Bool public
+open import Prim.Data.Nat hiding (_<_; _≤_) public
 
-absurd : ∀ {ℓ} {A : Type ℓ} → .⊥ → A
-absurd ()
+_ = Bool
+_ = Nat
+```
+-->
 
-¬_ : ∀ {ℓ} → Type ℓ → Type ℓ
-¬ A = A → ⊥
-infix 6 ¬_
+```agda
+_ : ∀ {ℓ ℓ'} (A : Type ℓ) → (A → Type ℓ') → Type (ℓ ⊔ ℓ')
+_ = Σ
 ```
 
 :::{.definition #product-type}
-The non-dependent product type `_×_`{.Agda} can be defined in terms of
-the dependent sum type:
+The non-dependent **product type** `_×_`{.Agda} can be defined in terms
+of the dependent sum type, `Σ`{.Agda}.
 :::
 
 ```agda
@@ -64,51 +109,153 @@ A × B = Σ[ _ ∈ A ] B
 infixr 5 _×_
 ```
 
-## Lifting
+# Auxilliary universes
 
-There is a function which lifts a type to a higher universe:
+Our type theory has a couple more families of universes that serve to
+support the formalisation. Above, we wrote down a function type where
+the *universe* at which the codomain lives depends on the input value.
+These "large" products are classified in `Typeω`. These "limit"
+universes are themselves organised into a hierarchy, but, unlike
+`Type`{.Agda}, the indexing of this hierarchy is *external*: the
+subscript in `Typeω₁`{.Agda} is a literal number, and not shorthand for
+a value of some type.
 
 ```agda
-record Lift {a} ℓ (A : Type a) : Type (a ⊔ ℓ) where
-  constructor lift
-  field
-    lower : A
+_ : Typeω
+_ = (ℓ : Level) → Type (lsuc ℓ)
+
+_ : Typeω₁
+_ = Typeω
 ```
 
-<!--
+The `Type`{.Agda} universes also code for universes of **strict**
+[[propositions]], that is, types which have at most one inhabitant *up
+to definitional equality*. We write these universes as `SProp`{.Agda}.
+As with `Type`{.Agda}, these are *predicative*, in that, while the
+product of a `SProp`{.Agda}-valued family will again live in *a*
+`SProp`{.Agda}, the level of the result depends on both the domain and
+codomain.
+
 ```agda
-open Lift public
+_ : ∀ {ℓ} → Type (lsuc ℓ)
+_ = SProp _
+```
 
-instance
-  Lift-instance : ∀ {ℓ ℓ'} {A : Type ℓ} → ⦃ A ⦄ → Lift ℓ' A
-  Lift-instance ⦃ x ⦄ = lift x
+## Some strict propositions
+
+We populate the smallest `SProp`{.Agda} universe with analogues of the
+unit and empty types. These enjoy the property that any of their
+inhabitants, even hypothetical, are definitionally equal.
+
+```agda
+record ⊤ˢ : SProp where
+  instance constructor ttˢ
+
+data ⊥ˢ : SProp where
 ```
--->
 
-## Function composition
+The empty `Type`{.Agda}, `⊥`{.Agda}, is defined by lifting the empty
+`SProp`{.Agda}. Since `⊥`{.Agda} is an `eta-equality record`{.Agda}
+type, it "inherits" definitional irrelevance from `⊥ˢ`{.Agda}.
 
-Since the following definitions are fundamental, they deserve a place in
-this module:
+```agda
+record ⊥ : Type where
+  constructor liftˢ
+  field lowerˢ : ⊥ˢ
+```
+
+Even defined like this, the empty type has an elimination principle into
+arbitrary types. We define an eliminator `absurd`{.Agda} valued in small
+fibrant types. To demonstrate that the codomain can be arbitrary, we can
+also define `absurdω`{.Agda}.
 
 ```agda
-_∘_ : ∀ {ℓ₁ ℓ₂ ℓ₃} {A : Type ℓ₁} {B : A → Type ℓ₂} {C : (x : A) → B x → Type ℓ₃}
-    → (∀ {x} → (y : B x) → C x y)
-    → (f : ∀ x → B x)
-    → ∀ x → C x (f x)
-f ∘ g = λ z → f (g z)
+absurd : ∀ {ℓ} {A : Type ℓ} → ⊥ → A
+absurd ()
 
-infixr 40 _∘_
+absurdω : {A : Typeω} → ⊥ → A
+absurdω ()
+```
+
+The **negation** of a type $A$ is, as usual, the type of functions $A
+\to \bot$. With our setup, the negation of an arbitrary type is
+definitionally proof-irrelevant.
+
+```agda
+¬_ : ∀ {ℓ} → Type ℓ → Type ℓ
+¬ A = A → ⊥
+infix 6 ¬_
+```
+
+<!--
+```agda
+```
+-->
+
+
+# Basic syntactic niceties
+
+We close out this module with the definition of a couple helpers which
+do not depend on anything other than quantification over types. First,
+we have (dependent) function composition `_∘_`{.Agda}, and the identity
+function `id`{.Agda}.
+
+```agda
+_∘_
+  : ∀ {ℓ₁ ℓ₂ ℓ₃} {A : Type ℓ₁} {B : A → Type ℓ₂} {C : (x : A) → B x → Type ℓ₃}
+  → (f : ∀ {x} → (y : B x) → C x y) (g : ∀ x → B x)
+  → ∀ x → C x (g x)
+(f ∘ g) z = f (g z)
 
 id : ∀ {ℓ} {A : Type ℓ} → A → A
 id x = x
-{-# INLINE id #-}
+```
+
+We also define two helpers for function application. The first,
+`_$_`{.Agda}, is familiar from Haskell, and serves simply to adjust
+precedence: one can write `f $ g x` instead of `f (g x)`.
 
-infixr -1 _$_ _$ᵢ_ _$ₛ_
+```agda
+infixr -1 _$_
 
-_$_ : ∀ {ℓ₁ ℓ₂} {A : Type ℓ₁} {B : A → Type ℓ₂} → ((x : A) → B x) → ((x : A) → B x)
+_$_ : ∀ {a b} {A : Type a} {B : A → Type b} → ((x : A) → B x) → ((x : A) → B x)
 f $ x = f x
+```
+
+The second, `case_of_`{.Agda}, is a mixfix operator which constraints
+its function argument to be nondependent, which enables type inference.
+When given a pattern-matching lambda as its second argument,
+`case_of_`{.Agda} can be used to scrutinise a value in an expression
+context.
+
+```agda
+case_of_ : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → A → (A → B) → B
+case x of f = f x
+
+_ : Bool → Bool
+_ = λ x → case x of λ where
+  true  → false
+  false → true
+```
+
+Finally, the 1Lab makes extensive use of instance arguments for
+automation. A convenient entry point to this automation is the
+`auto`{.Agda} function, which can be used to call instance search where
+a visible argument is expected.
+
+```agda
+auto : ∀ {ℓ} {A : Type ℓ} → ⦃ A ⦄ → A
+auto ⦃ a ⦄ = a
+```
+
+<!--
+```agda
+{-# INLINE id #-}
 {-# INLINE _$_ #-}
 
+infixr 40 _∘_
+infixr -1 _$ᵢ_ _$ₛ_
+
 _$ᵢ_ : ∀ {ℓ₁ ℓ₂} {A : Type ℓ₁} {B : .A → Type ℓ₂} → (.(x : A) → B x) → (.(x : A) → B x)
 f $ᵢ x = f x
 {-# INLINE _$ᵢ_ #-}
@@ -117,6 +264,7 @@ _$ₛ_ : ∀ {ℓ₁ ℓ₂} {A : Type ℓ₁} {B : A → SSet ℓ₂} → ((x :
 f $ₛ x = f x
 {-# INLINE _$ₛ_ #-}
 ```
+-->
 
 <!--
 ```agda
@@ -129,11 +277,8 @@ open import Prim.Literals public
     {f : B → C} {g : A → B}
   → P f → P g → P (f ∘ g)
 
-auto : ∀ {ℓ} {A : Type ℓ} → ⦃ A ⦄ → A
-auto ⦃ a ⦄ = a
-
-case_of_ : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → A → (A → B) → B
-case x of f = f x
+caseω_of_ : ∀ {ℓ'} {A : Typeω} {B : Type ℓ'} → A → (A → B) → B
+caseω x of f = f x
 
 case_return_of_ : ∀ {ℓ ℓ'} {A : Type ℓ} (x : A) (B : A → Type ℓ') (f : (x : A) → B x) → B x
 case x return P of f = f x
@@ -146,9 +291,6 @@ instance
   Number-Lift {ℓ' = ℓ'} ⦃ a ⦄ .Number.Constraint n = Lift ℓ' (a .Number.Constraint n)
   Number-Lift ⦃ a ⦄ .Number.fromNat n ⦃ lift c ⦄ = lift (a .Number.fromNat n ⦃ c ⦄)
 
-absurdω : {A : Typeω} → .⊥ → A
-absurdω ()
-
 infixr -1 primForce
 primitive
   primForce : ∀ {a b} {A : Type a} {B : A → Type b} (x : A) (f : ∀ x → B x) → B x
diff --git a/src/1Lab/Univalence.lagda.md b/src/1Lab/Univalence.lagda.md
index f527f3d9f..fac10f597 100644
--- a/src/1Lab/Univalence.lagda.md
+++ b/src/1Lab/Univalence.lagda.md
@@ -746,9 +746,9 @@ unglue-is-equiv
   : ∀ {ℓ ℓ'} {A : Type ℓ} (φ : I)
   → {B : Partial φ (Σ (Type ℓ') (_≃ A))}
   → is-equiv {A = Glue A B} (unattach φ)
-unglue-is-equiv {A = A} φ {B = B} .is-eqv y = extend→is-contr ctr
-  where module _ (ψ : I) (par : Partial ψ (fibre (unattach φ) y)) where
-    fib : .(p : IsOne φ)
+unglue-is-equiv {A = A} φ {B = B} .is-eqv y = extend→is-contr ctr where
+  module _ (ψ : I) (par : Partial ψ (fibre (unattach φ) y)) where
+    fib : (p : IsOne φ)
         → fibre (B p .snd .fst) y
           [ (ψ ∧ φ) ↦ (λ { (ψ = i1) (φ = i1) → par 1=1 }) ]
     fib p = is-contr→extend (B p .snd .snd .is-eqv y) (ψ ∧ φ) _
@@ -758,9 +758,9 @@ unglue-is-equiv {A = A} φ {B = B} .is-eqv y = extend→is-contr ctr
     sys j (φ = i1) = outS (fib 1=1) .snd (~ j)
     sys j (ψ = i1) = par 1=1 .snd (~ j)
 
-    ctr = inS $ₛ attach φ (λ { (φ = i1) → outS (fib 1=1) .fst })
-                  (inS (hcomp (φ ∨ ψ) sys))
-               , (λ i → hfill (φ ∨ ψ) (~ i) sys)
+    ctr = inS $ₛ
+        attach φ (λ { (φ = i1) → outS (fib 1=1) .fst }) (inS (hcomp (φ ∨ ψ) sys))
+      , λ i → hfill (φ ∨ ψ) (~ i) sys
 
 ua-unglue-is-equiv
   : ∀ {ℓ} {A B : Type ℓ} (f : A ≃ B)
diff --git a/src/Algebra/Ring/Module/Multilinear.lagda.md b/src/Algebra/Ring/Module/Multilinear.lagda.md
index 5079914cd..9584f42ed 100644
--- a/src/Algebra/Ring/Module/Multilinear.lagda.md
+++ b/src/Algebra/Ring/Module/Multilinear.lagda.md
@@ -376,7 +376,7 @@ proofs of linearity.
   curry-multilinear-map lin = ml where
     ml : Multilinear-map (suc n) _ _
     ml = from-linear-at (λ x → lin .map x .map) λ i xs r x y →
-      case fin-view i of λ where
+      caseω fin-view i of λ where
         zero → ap (λ e → applyᶠ (e .map) (xs .snd)) (Linear-map.linear lin r x y)
           ∙∙ apply-zipᶠ {P = λ i → ⌞ Ms (fsuc i) ⌟} _ _ _ _
           ∙∙ ap₂ N._+_ (apply-mapᶠ {P = λ i → ⌞ Ms (fsuc i) ⌟} _ _ _) refl
diff --git a/src/Cat/Bi/Instances/Discrete.lagda.md b/src/Cat/Bi/Instances/Discrete.lagda.md
index e5a3b9ef2..b72b1176d 100644
--- a/src/Cat/Bi/Instances/Discrete.lagda.md
+++ b/src/Cat/Bi/Instances/Discrete.lagda.md
@@ -31,20 +31,26 @@ letting the hom-1-categories of $\bf{C}$ be the [[discrete categories]] on
 the Hom-sets of $\cC$.
 
 ```agda
-{-# TERMINATING #-}
+private
+  BHom : C.Ob → C.Ob → Precategory _ _
+  BHom x y = Disc! (C.Hom x y)
+
+  Bcompose : ∀ {x y z} → Bifunctor (BHom y z) (BHom x y) (BHom x z)
+  Bcompose = make-bifunctor λ where
+    .F₀ A B → A C.∘ B
+    .lmap → apᵢ (C._∘ _)
+    .rmap → apᵢ (_ C.∘_)
+    .lmap-id    → refl
+    .rmap-id    → refl
+    .lmap-∘ f g → prop!
+    .rmap-∘ f g → prop!
+    .lrmap  f g → prop!
+
 Locally-discrete : Prebicategory o ℓ ℓ
-Locally-discrete .Ob = C.Ob
-Locally-discrete .Hom x y = Disc' (el (C.Hom x y) (C.Hom-set x y))
-Locally-discrete .id = C.id
-Locally-discrete .compose = make-bifunctor λ where
-  .F₀ A B → A C.∘ B
-  .lmap → apᵢ (C._∘ _)
-  .rmap → apᵢ (_ C.∘_)
-  .lmap-id    → refl
-  .rmap-id    → refl
-  .lmap-∘ f g → prop!
-  .rmap-∘ f g → prop!
-  .lrmap  f g → prop!
+Locally-discrete .Ob  = C.Ob
+Locally-discrete .Hom = BHom
+Locally-discrete .id  = C.id
+Locally-discrete .compose = Bcompose
 Locally-discrete .unitor-l = to-natural-iso ni where
   ni : make-natural-iso _ _
   ni .make-natural-iso.eta x = Id≃path.from $ sym (C.idl x)
diff --git a/src/Cat/Displayed/Instances/Family.lagda.md b/src/Cat/Displayed/Instances/Family.lagda.md
index 0712ccbe8..d8f65bc6d 100644
--- a/src/Cat/Displayed/Instances/Family.lagda.md
+++ b/src/Cat/Displayed/Instances/Family.lagda.md
@@ -151,10 +151,10 @@ the family fibration is fibrewise univalent whenever $\cC$ is.
 ```agda
 module _ {ℓ} (X : Set ℓ) where
   private
-    lift-f = Disc-diagram {C = C} {iss = is-hlevel-suc 2 (X .is-tr)}
+    lift-f = Disc-diagram {C = C} {X = ⌞ X ⌟}
     module F = Cat.Reasoning (Fibre Family X)
 
-  Families→functors : Functor (Fibre Family X) Cat[ Disc' X , C ]
+  Families→functors : Functor (Fibre Family X) Cat[ Disc! X , C ]
   Families→functors .F₀ = Disc-diagram
   Families→functors .F₁ f .η = f
   Families→functors .F₁ {X} {Y} f .is-natural x y reflᵢ = id-comm
diff --git a/src/Cat/Instances/Discrete.lagda.md b/src/Cat/Instances/Discrete.lagda.md
index e5f70be42..c32150b52 100644
--- a/src/Cat/Instances/Discrete.lagda.md
+++ b/src/Cat/Instances/Discrete.lagda.md
@@ -43,27 +43,34 @@ For technical reasons, we prefer to define this category using the
 
 ```agda
 Disc : (A : Type ℓ) → is-groupoid A → Precategory ℓ ℓ
-Disc A A-grpd .Ob          = A
-Disc A A-grpd .Hom         = _≡ᵢ_
-Disc A A-grpd .Hom-set     = ≡ᵢ-is-hlevel' {n = 2} A-grpd
-Disc A A-grpd .id          = reflᵢ
-Disc A A-grpd ._∘_ p q     = q ∙ᵢ p
-Disc A A-grpd .idr _       = refl
-Disc A A-grpd .idl _       = ∙ᵢ-idr _
-Disc A A-grpd .assoc p q r = sym (∙ᵢ-assoc r q p)
-
-Disc' : Set ℓ → Precategory ℓ ℓ
-Disc' A = Disc ∣ A ∣ h module Disc' where abstract
-  h : is-groupoid ∣ A ∣
-  h = is-hlevel-suc 2 (A .is-tr)
+Disc A A-grpd = record where
+  Ob          = A
+  Hom         = _≡ᵢ_
+  Hom-set     = ≡ᵢ-is-hlevel' {n = 2} A-grpd
+  id          = reflᵢ
+  _∘_ p q     = q ∙ᵢ p
+  idr _       = refl
+  idl _       = ∙ᵢ-idr _
+  assoc p q r = sym (∙ᵢ-assoc r q p)
 ```
 
+<!--
+```agda
+Disc! : ∀ {ℓ} {U : Type ℓ} ⦃ _ : Underlying U ⦄ (T : U) ⦃ _ : H-Level ⌞ T ⌟ 3 ⦄ → Precategory _ _
+Disc! A = Disc ⌞ A ⌟ h module Disc! where abstract
+  h : is-groupoid ⌞ A ⌟
+  h = hlevel 3
+
+{-# DISPLAY Disc {ℓ} A (Disc!.h {_} _ ⦃ i ⦄) = Disc! {ℓ} A ⦃ i ⦄ #-}
+```
+-->
+
 By construction, this is a [[univalent|univalent category]]
 [[groupoid|pregroupoid]]:
 
 ```agda
 Disc-is-category : ∀ {A : Type ℓ} {A-grpd} → is-category (Disc A A-grpd)
-Disc-is-category .to-path is              = Id≃path.to (is .to)
+Disc-is-category .to-path is = Id≃path.to (is .to)
 Disc-is-category .to-path-over {a = a} is with is .to in w
 ... | reflᵢ = ≅-pathp _ _ _ (Id≃path.to (symᵢ w))
 
@@ -93,52 +100,40 @@ category induces a functor.
 
 ```agda
 Disc-diagram
-  : {X : Type ℓ} {iss : is-groupoid X}
+  : ∀ {X : Type ℓ} {xh}
   → (X → Ob C)
-  → Functor (Disc X iss) C
-Disc-diagram {C = C} {X = X} f = F where
-  module C = Precategory C
-
-  F : Functor _ _
-  F .F₀       = f
-  F .F₁ reflᵢ = C.id
-  F .F-id     = refl
-  F .F-∘ reflᵢ reflᵢ = sym (C.idl C.id)
+  → Functor (Disc X xh) C
+Disc-diagram {C = C} f .F₀       = f
+Disc-diagram {C = C} f .F₁ reflᵢ = C .id
+Disc-diagram {C = C} f .F-id = refl
+Disc-diagram {C = C} f .F-∘ reflᵢ reflᵢ = sym (C .idl _)
 ```
 
-<!--
-```agda
-Disc-diagram!
-  : ∀ ⦃ iss : H-Level {ℓ} X 3 ⦄
-  → (X → Ob C)
-  → Functor (Disc X (hlevel 3)) C
-Disc-diagram! = Disc-diagram
-```
--->
-
 As a corollary, we can lift any function between underlying types to a
 functor between discrete categories.
 
 ```agda
-lift-disc : {A : Set ℓ} {B : Set ℓ'} → (∣ A ∣ → ∣ B ∣) → Functor (Disc' A) (Disc' B)
+lift-disc
+  : ∀ {A : Type ℓ} {B : Type ℓ'} {ah bh} (f : A → B)
+  → Functor (Disc A ah) (Disc B bh)
 lift-disc {A = A} f = Disc-diagram f
 ```
 
 <!--
 ```agda
 Disc-into
-  : ∀ {ℓ} (X : Set ℓ)
-  → (F : C .Ob → ∣ X ∣)
+  : ∀ {ℓ} {X : Type ℓ} {xh} ⦃ _ : H-Level X 2 ⦄
+  → (F : C .Ob → ⌞ X ⌟)
   → (F₁ : ∀ {x y} → C .Hom x y → F x ≡ᵢ F y)
-  → Functor C (Disc' X)
-Disc-into X F F₁ .F₀      = F
-Disc-into X F F₁ .F₁      = F₁
-Disc-into X F F₁ .F-id    = ≡ᵢ-is-hlevel' {n = 1} (X .is-tr) _ _ _ _
-Disc-into X F F₁ .F-∘ _ _ = ≡ᵢ-is-hlevel' {n = 1} (X .is-tr) _ _ _ _
+  → Functor C (Disc X xh)
+Disc-into F F₁ .F₀      = F
+Disc-into F F₁ .F₁      = F₁
+Disc-into F F₁ .F-id    = hlevel!
+Disc-into F F₁ .F-∘ _ _ = hlevel!
 
 Disc-natural
-  : ∀ {X : Set ℓ}
-  → {F G : Functor (Disc' X) C}
+  : ∀ {X : Type ℓ} {xh}
+  → {F G : Functor (Disc X xh) C}
   → (∀ x → C .Hom (F .F₀ x) (G .F₀ x))
   → F => G
 Disc-natural fam .η = fam
@@ -157,8 +152,10 @@ Disc-natural₂ {C = C} {F = F} {G = G} fam .is-natural x y (reflᵢ , reflᵢ)
 
 open _≅_
 open Inverses
-Disc-natural-iso : ∀ {X : Set ℓ}
-  → {F G : Functor (Disc' X) C}
+
+Disc-natural-iso
+  : ∀ {X : Type ℓ} {xh}
+  → {F G : Functor (Disc X xh) C}
   → (∀ x → Isomorphism C (F .F₀ x) (G .F₀ x))
   → F ≅ⁿ G
 Disc-natural-iso isos .to       = Disc-natural λ x → isos x .to
diff --git a/src/Cat/Instances/Shape/Two.lagda.md b/src/Cat/Instances/Shape/Two.lagda.md
index 59cc3b758..f56cfb2ea 100644
--- a/src/Cat/Instances/Shape/Two.lagda.md
+++ b/src/Cat/Instances/Shape/Two.lagda.md
@@ -22,7 +22,7 @@ useful for expressing binary [[products]] and [[coproducts]] as
 
 ```agda
 2-object-category : Precategory _ _
-2-object-category = Disc' (el! Bool)
+2-object-category = Disc! Bool
 ```
 
 A diagram of shape $\twocat$ in $\cC$ simply consists of two objects of
diff --git a/src/Cat/Instances/Slice.lagda.md b/src/Cat/Instances/Slice.lagda.md
index 86f979d53..5d134fab0 100644
--- a/src/Cat/Instances/Slice.lagda.md
+++ b/src/Cat/Instances/Slice.lagda.md
@@ -604,7 +604,7 @@ Let's begin. The `Total-space`{.Agda} functor gets out of our way very
 fast:
 
 ```agda
-  Total-space : Functor Cat[ Disc' I , Sets ℓ ] (Slice (Sets ℓ) I)
+  Total-space : Functor Cat[ Disc! I , Sets ℓ ] (Slice (Sets ℓ) I)
   Total-space .F₀ F .dom = el! (Σ _ (∣_∣ ⊙ F₀ F))
   Total-space .F₀ F .map = fst
 
diff --git a/src/Cat/Instances/StrictCat/Cohesive.lagda.md b/src/Cat/Instances/StrictCat/Cohesive.lagda.md
index bcbb18341..12ab83349 100644
--- a/src/Cat/Instances/StrictCat/Cohesive.lagda.md
+++ b/src/Cat/Instances/StrictCat/Cohesive.lagda.md
@@ -77,7 +77,7 @@ functor `Γ`{.Agda} we defined above. Then we define the adjunction
 
 ```agda
 Disc : Functor (Sets ℓ) (Strict-cats ℓ ℓ)
-Disc .F₀ S = Disc' S , S .is-tr
+Disc .F₀ S = Disc! S , S .is-tr
 Disc .F₁ = lift-disc
 Disc .F-id = Functor-path (λ x → refl) λ f → prop!
 Disc .F-∘ _ _ = Functor-path (λ x → refl) λ f → prop!
@@ -289,7 +289,7 @@ quotient.
 Π₀⊣Disc : Π₀ ⊣ Disc {ℓ}
 Π₀⊣Disc = adj where
   adj : _ ⊣ _
-  adj .unit .η x = Disc-into _ inc λ m → Id≃path.from (quot m)
+  adj .unit .η x = Disc-into inc λ m → Id≃path.from (quot m)
   adj .unit .is-natural x y f = Functor-path (λ x → refl) λ _ → prop!
 ```
 
diff --git a/src/Data/Bool/Base.lagda.md b/src/Data/Bool/Base.lagda.md
index 4a5374de2..cfb5a7b07 100644
--- a/src/Data/Bool/Base.lagda.md
+++ b/src/Data/Bool/Base.lagda.md
@@ -98,7 +98,7 @@ Bool-elim A at af false = af
 record So (b : Bool) : Type where
   constructor oh
   field
-    @irr ⦃ is-so ⦄ : if b then ⊤ else ⊥
+    ⦃ is-so ⦄ : if b then ⊤ˢ else ⊥ˢ
 ```
 
 <!--
diff --git a/src/Data/Bool/Order.lagda.md b/src/Data/Bool/Order.lagda.md
index db418a4d3..979ec3fad 100644
--- a/src/Data/Bool/Order.lagda.md
+++ b/src/Data/Bool/Order.lagda.md
@@ -14,15 +14,15 @@ module Data.Bool.Order where
 
 ```agda
 private
-  R : Bool → Bool → Type
-  R false _     = ⊤
-  R true  true  = ⊤
-  R true  false = ⊥
+  R : Bool → Bool → SProp
+  R false _     = ⊤ˢ
+  R true  true  = ⊤ˢ
+  R true  false = ⊥ˢ
 
 record _≤_ (x y : Bool) : Type where
   constructor lift
   field
-    .lower : R x y
+    lower : R x y
 ```
 
 <!--
@@ -35,8 +35,8 @@ instance
 
 ```agda
 ≤-refl : ∀ {x} → x ≤ x
-≤-refl {true}  = lift tt
-≤-refl {false} = lift tt
+≤-refl {true}  = _
+≤-refl {false} = _
 
 ≤-trans : ∀ {x y z} → x ≤ y → y ≤ z → x ≤ z
 ≤-trans {true}  {true}  {true}  p q = _
diff --git a/src/Data/Dec/Base.lagda.md b/src/Data/Dec/Base.lagda.md
index 54943680f..c4e527679 100644
--- a/src/Data/Dec/Base.lagda.md
+++ b/src/Data/Dec/Base.lagda.md
@@ -5,7 +5,6 @@ open import 1Lab.Path
 open import 1Lab.Type
 
 open import Data.Sum.Base
-open import Data.Irr
 
 open import Meta.Invariant
 open import Meta.Idiom
@@ -46,10 +45,6 @@ Dec-rec = Dec-elim _
 
 <!--
 ```agda
-recover : ∀ {ℓ} {A : Type ℓ} ⦃ d : Dec A ⦄ → Irr A → A
-recover ⦃ yes x ⦄ _ = x
-recover ⦃ no ¬x ⦄ (forget x) = absurd (¬x x)
-
 dec→dne : ∀ {ℓ} {A : Type ℓ} ⦃ d : Dec A ⦄ → ¬ ¬ A → A
 dec→dne ⦃ yes x ⦄ _   = x
 dec→dne ⦃ no ¬x ⦄ ¬¬x = absurd (¬¬x ¬x)
diff --git a/src/Data/Fin/Base.lagda.md b/src/Data/Fin/Base.lagda.md
index a4f95a014..1da846b0b 100644
--- a/src/Data/Fin/Base.lagda.md
+++ b/src/Data/Fin/Base.lagda.md
@@ -110,7 +110,7 @@ that a type is inductively generated. We therefore expose a type
 of $\operatorname{Fin}(n)$ is `fzero`{.Agda} or `fsuc`{.Agda}.
 
 ```agda
-data Fin-view : {n : Nat} → Fin n → Type where
+data Fin-view : {n : Nat} → Fin n → Typeω where
   zero : ∀ {n}             → Fin-view {suc n} fzero
   suc  : ∀ {n} (i : Fin n) → Fin-view {suc n} (fsuc i)
 ```
@@ -123,7 +123,7 @@ fin-view : ∀ {n} (i : Fin n) → Fin-view i
 fin-view {suc n} fzero               = zero
 fin-view {suc n} (fin (suc i) ⦃ b ⦄) = suc (fin i ⦃ Nat.≤-peel b ⦄)
 
-fin-view {zero}  (fin _ ⦃ i<n ⦄) = absurd (Nat.¬suc≤0 i<n)
+fin-view {zero}  (fin _ ⦃ i<n ⦄) = absurdω (Nat.¬suc≤0 i<n)
 ```
 
 As a first application, we can prove that `Fin 0` is empty:
diff --git a/src/Data/Int/HIT.lagda.md b/src/Data/Int/HIT.lagda.md
index fad51ae2e..690545292 100644
--- a/src/Data/Int/HIT.lagda.md
+++ b/src/Data/Int/HIT.lagda.md
@@ -4,6 +4,7 @@ open import 1Lab.Prelude
 
 open import Data.Nat.Solver
 open import Data.Dec
+open import Data.Irr
 open import Data.Nat
 open import Data.Sum
 ```
@@ -235,15 +236,15 @@ Canonical n = Σ[ x ∈ Nat ] Σ[ y ∈ Nat ] (diff x y ≡ n)
 
 canonicalise : (n : Int) → Canonical n
 canonicalise = go where
-  lemma₁ : ∀ x y → x < y → diff 0 (y - x) ≡ diff x y
-  lemma₂ : ∀ x y → y < x → diff (x - y) 0 ≡ diff x y
-  lemma₃ : ∀ x y → @irr x ≡ y → diff 0 0       ≡ diff x y
+  lemma₁ : ∀ x y → x < y       → diff 0 (y - x) ≡ diff x y
+  lemma₂ : ∀ x y → y < x       → diff (x - y) 0 ≡ diff x y
+  lemma₃ : ∀ x y → Irr (x ≡ y) → diff 0 0       ≡ diff x y
 
   work : ∀ x y → Canonical (diff x y)
   work x y with ≤-split x y
   ... | inl p       = 0     , y - x , lemma₁ x y p
   ... | inr (inl p) = x - y , 0     , lemma₂ x y p
-  ... | inr (inr p) = 0     , 0     , lemma₃ x y p
+  ... | inr (inr p) = 0     , 0     , lemma₃ x y (forget p)
 ```
 
 It remains to show that the procedure `work`{.Agda} respects the
@@ -266,9 +267,9 @@ from this page. You can unfold it below if you dare:
   lemma₂ (suc x) (suc y) p = lemma₂ x y (≤-peel p) ∙ Int.quot x y
 
   lemma₃ zero zero p       = refl
-  lemma₃ zero (suc y) p    = absurd (zero≠suc p)
-  lemma₃ (suc x) zero p    = absurd (suc≠zero p)
-  lemma₃ (suc x) (suc y) p = lemma₃ x y (suc-inj p) ∙ Int.quot x y
+  lemma₃ zero (suc y) p    = absurd (zero≠suc (recover p))
+  lemma₃ (suc x) zero p    = absurd (suc≠zero (recover p))
+  lemma₃ (suc x) (suc y) p = lemma₃ x y (suc-inj <$> p) ∙ Int.quot x y
 
   abstract
     work-respects-quot
diff --git a/src/Data/Irr.lagda.md b/src/Data/Irr.lagda.md
index 2fb2c507b..7ee15b656 100644
--- a/src/Data/Irr.lagda.md
+++ b/src/Data/Irr.lagda.md
@@ -4,7 +4,10 @@ open import 1Lab.HLevel.Closure
 open import 1Lab.Path
 open import 1Lab.Type
 
+open import Data.Dec.Base
+
 open import Meta.Idiom
+open import Meta.Bind
 ```
 -->
 
@@ -22,25 +25,47 @@ private variable
 ```
 -->
 
-In Agda, it's possible to turn any type into one that *definitionally*
-has at most one inhabitant. We do this using a record containing an
-irrelevant field.
+As with how the [[propositional truncation]] freely generates a
+[[proposition]] from a type, we can define a *strict* truncation
+modality which freely generates a *definitionally irrelevant* type from
+a type.
+
+This is a secondary notion in our type theory, since this type former
+does not have a well-behaved elimination principle. However, its
+presence in the theory allows defining `record`{.Agda} types with finer
+control over definitional equality, which can be a notable optimisation;
+and the resulting types are essentially well-behaved as long as we only
+wrap [[decidable]] [[propositions]].
+
+The construction proceeds in two stages: first, we define `Irrˢ`{.Agda},
+living in `SProp`{.Agda}, generated by $A$. This type is then wrapped in
+the `record`{.Agda} `Irr`{.Agda} to bring it back to the correct
+universe of [[fibrant]] types.
 
 ```agda
+data Irrˢ {ℓ} (A : Type ℓ) : SProp ℓ where
+  forgetˢ : A → Irrˢ A
+
 record Irr {ℓ} (A : Type ℓ) : Type ℓ where
-  constructor forget
-  field
-    @irr lower : A
+  constructor liftˢ
+  field lowerˢ : Irrˢ A
+```
+
+<!--
+```agda
+open Irr public
+pattern forget s = liftˢ (forgetˢ s)
 ```
+-->
 
-The most important property of this type is that, given any $x, y$ in
-$\operatorname{Irr}(A)$, the constant path `refl`{.Agda} checks at type
-$x \is y$.
+As promised, `Irr`{.Agda} is definitionally irrelevant, as can be
+demonstrated by checking that the `refl`{.Agda}exive path connects the
+*a priori* distinct variables $x$ and $y$.
 
 ```agda
 instance
   H-Level-Irr : ∀ {n} → H-Level (Irr A) (suc n)
-  H-Level-Irr {n} = prop-instance λ _ _ → refl
+  H-Level-Irr {n} = prop-instance λ x y → refl
 ```
 
 <!--
@@ -51,9 +76,42 @@ instance
   {-# INCOHERENT make-irr #-}
 
   Map-Irr : Map (eff Irr)
-  Map-Irr = record { map = λ where f (forget x) → forget (f x) }
+  Map-Irr = record { map = λ f x → liftˢ (mapˢ f (x .lowerˢ)) } where
+    mapˢ : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → (A → B) → Irrˢ A → Irrˢ B
+    mapˢ f (forgetˢ x) = forgetˢ (f x)
 
   Idiom-Irr : Idiom (eff Irr)
-  Idiom-Irr = record { pure = λ x → forget x ; _<*>_ = λ where (forget f) (forget x) → forget (f x) }
+  Idiom-Irr = record { pure = λ x → forget x ; _<*>_ = λ f x → liftˢ (apˢ (f .lowerˢ) (x .lowerˢ)) } where
+    apˢ : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → Irrˢ (A → B) → Irrˢ A → Irrˢ B
+    apˢ (forgetˢ f) (forgetˢ x) = forgetˢ (f x)
+
+  Bind-Irr : Bind (eff Irr)
+  Bind-Irr = record { _>>=_ = λ x f → liftˢ (joinˢ (map f x .lowerˢ)) } where
+    joinˢ : ∀ {ℓ} {A : Type ℓ} → Irrˢ (Irr A) → Irrˢ A
+    joinˢ (forgetˢ (forget x)) = forgetˢ x
 ```
 -->
+
+## Recovering decidable propositions
+
+As mentioned above, `Irr`{.Agda} does not have a well-behaved
+elimination principle. However, since `⊥`{.Agda} is a strict
+proposition, we can show that $\operatorname{Irr}(A)$ implies $\neg \neg
+A$.
+
+```agda
+Irr→not-not : ∀ {ℓ} {A : Type ℓ} → Irr A → ¬ ¬ A
+Irr→not-not {A = A} (liftˢ aˢ) f = liftˢ (go aˢ f) where
+  go : Irrˢ A → (A → ⊥) → ⊥ˢ
+  go (forgetˢ a) ¬a = ¬a a .⊥.lowerˢ
+```
+
+Therefore, if the type being truncated is [[decidable]], we can recover
+a legitimate $A$ given only knowledge of $\operatorname{Irr}(A)$, using
+the result above to refute the `no`{.Agda} case.
+
+```agda
+recover : ∀ {ℓ} {A : Type ℓ} ⦃ d : Dec A ⦄ → Irr A → A
+recover ⦃ yes x ⦄ _   = x
+recover ⦃ no ¬x ⦄ ¬¬x = absurd (Irr→not-not ¬¬x ¬x)
+```
diff --git a/src/Data/Nat/DivMod.lagda.md b/src/Data/Nat/DivMod.lagda.md
index 9b607f82b..a6c47c8e6 100644
--- a/src/Data/Nat/DivMod.lagda.md
+++ b/src/Data/Nat/DivMod.lagda.md
@@ -80,8 +80,9 @@ $$
 $$
 
 ```agda
-  divide-pos (suc a) b | divmod q' r' (forget p) s | inl r'+1<b =
-    divmod q' (suc r') (forget (ap suc p ∙ sym (+-sucr (q' * b) r'))) r'+1<b
+  divide-pos (suc a) b | divmod q' r' p s | inl r'+1<b = divmod q' (suc r')
+    (forget (ap suc (recover p) ∙ sym (+-sucr (q' * b) r')))
+    r'+1<b
 ```
 
 The other case --- that in which $1 + r' = b$ --- is more interesting.
@@ -91,10 +92,10 @@ in this case, $q = 1 + q'$ and $r = 0$, which works out because ($0 < b$
 and) of some arithmetic. See for yourself:
 
 ```agda
-  divide-pos (suc a) (suc b') | divmod q' r' (forget p) s | inr (inr r'+1=b) =
+  divide-pos (suc a) (suc b') | divmod q' r' p s | inr (inr r'+1=b) =
     divmod (suc q') 0
       (forget $ᵢ
-        suc a                           ≡⟨ ap suc p ⟩
+        suc a                           ≡⟨ ap suc (recover p) ⟩
         suc (q' * (suc b') + r')        ≡˘⟨ ap (λ e → suc (q' * e + r')) r'+1=b ⟩
         suc (q' * (suc r') + r')        ≡⟨ nat! ⟩
         suc (r' + q' * (suc r') + zero) ≡⟨ ap (λ e → e + q' * e + 0) r'+1=b ⟩
@@ -154,8 +155,6 @@ div-helper k m (suc n) (suc j) = div-helper k       m n j
 {-# BUILTIN NATDIVSUCAUX div-helper #-}
 {-# BUILTIN NATMODSUCAUX mod-helper #-}
 
--- _ = {! mod-helper 0 0 4294967296 2  !}
-
 _/ₙ_ : (d1 d2 : Nat) ⦃ _ : Positive d2 ⦄ → Nat
 d1 /ₙ suc d2 = div-helper 0 d2 d1 d2
 
@@ -221,26 +220,21 @@ instance
         r' = s≤s (≤-trans (+-≤l y (z + y * z)) (≤-refl' (sym r)))
 
       lemma' : ∀ q q' b r r' → r' < r → r < b → q * b + r ≡ q' * b + r' → ⊥
-      lemma' q q' b r r' r'<r r<b β =
-        <-≤-asym q<q' q'≤q
-        where
-          r-r'<b : r - r' < b
-          r-r'<b = ≤-trans (s≤s (monus-≤ r r')) r<b
-
-          q<q' : q < q'
-          q<q' =
-            *-reflects-<r b ⦃ ≤-trans (s≤s 0≤x) r<b ⦄ $
-            +-balance-<l (q' * b) r' (q * b) r (sym β) (r'<r)
-
-          q'≤q : q' ≤ q
-          q'≤q =
-            monus-zero→≤ q' q $
-            lemma (r - r') b (q' - q) r-r'<b $
-            sym $ monus-swapr (b * (q' - q)) 0 (r - r') $
-              b * (q' - q) + 0 ≡⟨ +-zeror _ ∙ *-commutative b (q' - q) ⟩
-              (q' - q) * b     ≡⟨ monus-distribr q' q b ⟩
-              q' * b - q * b   ≡˘⟨ monus-swapl (q * b) (r - r') (q' * b) (monus-exchanger (q * b) r (q' * b) r' β (<-weaken r'<r)) ⟩
-              r - r'           ∎
+      lemma' q q' b r r' r'<r r<b β = <-≤-asym q<q' q'≤q where
+        r-r'<b : r - r' < b
+        r-r'<b = ≤-trans (s≤s (monus-≤ r r')) r<b
+
+        q<q' : q < q'
+        q<q' = *-reflects-<r b ⦃ ≤-trans (s≤s 0≤x) r<b ⦄ $
+          +-balance-<l (q' * b) r' (q * b) r (sym β) (r'<r)
+
+        q'≤q : q' ≤ q
+        q'≤q = monus-zero→≤ q' q $ lemma (r - r') b (q' - q) r-r'<b $ sym $
+          monus-swapr (b * (q' - q)) 0 (r - r') $
+            b * (q' - q) + 0 ≡⟨ +-zeror _ ∙ *-commutative b (q' - q) ⟩
+            (q' - q) * b     ≡⟨ monus-distribr q' q b ⟩
+            q' * b - q * b   ≡˘⟨ monus-swapl (q * b) (r - r') (q' * b) (monus-exchanger (q * b) r (q' * b) r' β (<-weaken r'<r)) ⟩
+            r - r'           ∎
 ```
 -->
 
@@ -255,4 +249,5 @@ instance
       n∣r : (q' - q) * n ≡ r
       n∣r = monus-distribr q' q n ∙ sym (monus-swapl _ _ _ (sym (p ∙ recover α)))
     in <-≤-asym β (m∣sn→m≤sn (q' - q , n∣r))
+  {-# INCOHERENT Dec-∣ #-}
 ```
diff --git a/src/Data/Nat/Divisible/GCD.lagda.md b/src/Data/Nat/Divisible/GCD.lagda.md
index 2d4aa7ab2..7cccf9e89 100644
--- a/src/Data/Nat/Divisible/GCD.lagda.md
+++ b/src/Data/Nat/Divisible/GCD.lagda.md
@@ -11,6 +11,7 @@ open import Data.Nat.Order
 open import Data.Dec.Base
 open import Data.Nat.Base
 open import Data.Sum.Base
+open import Data.Irr
 ```
 -->
 
@@ -165,10 +166,10 @@ sense of $<$) than the original input.
 ```agda
   euclid-< : ∀ y x → x < y → GCD y x
   euclid-< = Wf-induction _ <-wf _ λ where
-     x rec zero p    → x , is-gcd-0
-     x rec (suc y) p →
+    x rec zero p    → x , is-gcd-0
+    x rec (suc y) p →
       let (d , step) = rec (suc y) p (x % suc y) (x%y<y x (suc y))
-       in d , is-gcd-step step
+        in d , is-gcd-step step
 
 ```
 
diff --git a/src/Data/Nat/Order.lagda.md b/src/Data/Nat/Order.lagda.md
index 91715e088..af6610913 100644
--- a/src/Data/Nat/Order.lagda.md
+++ b/src/Data/Nat/Order.lagda.md
@@ -35,13 +35,13 @@ naturals automatically.
 
 <!--
 ```agda
-≤-refl' : ∀ {x y} → .(x ≡ y) → x ≤ y
+≤-refl' : ∀ {x y} → x ≡ y → x ≤ y
 ≤-refl' {zero} {zero} p = 0≤x
 ≤-refl' {zero} {suc y} p = absurd (zero≠suc p)
 ≤-refl' {suc x} {zero} p = absurd (suc≠zero p)
 ≤-refl' {suc x} {suc y} p = s≤s (≤-refl' (suc-inj p))
 
-≤-reflᵢ : ∀ {x y} → .(x ≡ᵢ y) → x ≤ y
+≤-reflᵢ : ∀ {x y} → x ≡ᵢ y → x ≤ y
 ≤-reflᵢ p = ≤-refl' (Id-identity-system .to-path p)
 ```
 -->
diff --git a/src/Data/Nat/Range.lagda.md b/src/Data/Nat/Range.lagda.md
index 9b12fada9..5a3e92527 100644
--- a/src/Data/Nat/Range.lagda.md
+++ b/src/Data/Nat/Range.lagda.md
@@ -217,7 +217,7 @@ range-upper
   → i ∈ range x y
   → i < y
 range-upper {x = x} {y = y} {i = i} i∈xy =
-  ≤-trans (count-up-upper i∈xy) $ ≤-refl' $ᵢ
+  ≤-trans (count-up-upper i∈xy) $ ≤-refl' $
     monus-+r-inverse y x $
     <-weaken (nonempty-range→< (has-member→nonempty i∈xy))
 ```
@@ -240,7 +240,7 @@ range-∈
   → x ≤ i → i < y
   → i ∈ range x y
 range-∈ {x = x} {y = y} {i = i} x≤i i<y =
-  count-up-∈ x≤i $ ≤-trans i<y $ ≤-refl' $ᵢ sym $
+  count-up-∈ x≤i $ ≤-trans i<y $ ≤-refl' $ sym $
     monus-+r-inverse y x (≤-trans x≤i (<-weaken i<y))
 ```
 
diff --git a/src/Data/Rational/Base.lagda.md b/src/Data/Rational/Base.lagda.md
index 6cac58e89..fc2b6db18 100644
--- a/src/Data/Rational/Base.lagda.md
+++ b/src/Data/Rational/Base.lagda.md
@@ -535,10 +535,14 @@ integer fractions.
 ```agda
 reduce-resp : (x y : Fraction) → x ≈ y → reduce-fraction x ≡ reduce-fraction y
 reduce-resp f@(x / s [ s≠0 ]) f'@(y / t [ t≠0 ]) p =
-  reduce-fraction (x / s [ s≠0 ])             ≡⟨ sym (reduce-*r x s t s≠0 t≠0) ⟩
-  reduce-fraction ((x *ℤ t) / (s *ℤ t) [ _ ]) ≡⟨ ap reduce-fraction (Fraction-path {x = _ / _ [ *ℤ-positive s≠0 t≠0 ]} {_ / _ [ *ℤ-positive t≠0 s≠0 ]} (from-same-rational p) (*ℤ-commutative s t)) ⟩
-  reduce-fraction ((y *ℤ s) / (t *ℤ s) [ _ ]) ≡⟨ reduce-*r y t s t≠0 s≠0 ⟩
-  reduce-fraction (y / t [ t≠0 ])             ∎
+  let
+    st≠0 = *ℤ-positive s≠0 t≠0
+    ts≠0 = *ℤ-positive t≠0 s≠0
+  in
+    reduce-fraction (x / s [ s≠0 ])                ≡⟨ sym (reduce-*r x s t s≠0 t≠0) ⟩
+    reduce-fraction ((x *ℤ t) / (s *ℤ t) [ st≠0 ]) ≡⟨ ap reduce-fraction (Fraction-path {x = _ / _ [ st≠0 ]} {y = _ / _ [ ts≠0 ]} (from-same-rational p) (*ℤ-commutative s t)) ⟩
+    reduce-fraction ((y *ℤ s) / (t *ℤ s) [ ts≠0 ]) ≡⟨ reduce-*r y t s t≠0 s≠0 ⟩
+    reduce-fraction (y / t [ t≠0 ])                ∎
 
 integer-frac-splits : is-split-congruence L.Fraction-congruence
 integer-frac-splits = record
@@ -673,7 +677,7 @@ record Nonzero (x : Ratio) : Type where
   -- with the overlap pragmas; and we need those if we're gonna have
   -- e.g. Nonzero (p * q) as an instance.
   field
-    .lower : x ≠ 0
+    lower : x ≠ 0
 
 instance
   H-Level-Nonzero : ∀ {x n} → H-Level (Nonzero x) (suc n)
diff --git a/src/Homotopy/Space/Delooping.lagda.md b/src/Homotopy/Space/Delooping.lagda.md
index a5efc34d7..f9d44c65b 100644
--- a/src/Homotopy/Space/Delooping.lagda.md
+++ b/src/Homotopy/Space/Delooping.lagda.md
@@ -274,7 +274,11 @@ group of `Deloop`{.Agda} is `G`, which is what we wanted.
 
 ```agda
   G≃ΩB : ⌞ G ⌟ ≃ (base ≡ base)
-  G≃ΩB = Iso→Equiv (decode base , iso (encode base) encode→decode (decode→encode base))
+  G≃ΩB .fst = decode base
+  G≃ΩB .snd = is-iso→is-equiv record where
+    from = encode base
+    rinv = encode→decode
+    linv = decode→encode base
 
   G≅π₁B : G Groups.≅ πₙ₊₁ 0 (Deloop , base)
   G≅π₁B = total-iso (_ , ∘-is-equiv (∥-∥₀-idempotent (squash base base)) (G≃ΩB .snd))
@@ -437,16 +441,15 @@ _that's_ an equivalence! A similar remark allows us to conclude that
 $\rm{winding}_x$ is a group homomorphism $\Loop (\B G, x) \to G$.
 
 ```agda
-  opaque
-    winding-is-equiv : ∀ x → is-equiv (winding {x})
-    winding-is-equiv = Deloop-elim-prop G _ (λ _ → hlevel 1) $
-      Equiv.inverse (G≃ΩB G) .snd
-
-    winding-is-group-hom : ∀ x →
-      is-group-hom (π₁Groupoid.on-Ω (Deloop G , x) (hlevel 3))
-        (G .snd) (winding {x})
-    winding-is-group-hom = Deloop-elim-prop G _ (λ x → hlevel 1) λ where
-      .pres-⋆ x y → encode.pres-⋆ G x y
+  winding-is-equiv : ∀ x → is-equiv (winding {x})
+  winding-is-equiv = Deloop-elim-prop G _ (λ _ → hlevel 1) $
+    Equiv.inverse (G≃ΩB G) .snd
+
+  winding-is-group-hom : ∀ x →
+    is-group-hom (π₁Groupoid.on-Ω (Deloop G , x) (hlevel 3))
+      (G .snd) (winding {x})
+  winding-is-group-hom = Deloop-elim-prop G _ (λ x → hlevel 1) λ where
+    .pres-⋆ x y → encode.pres-⋆ G x y
 ```
 
 We can then obtain a nice interface for working with `winding`{.Agda}.
diff --git a/src/Logic/Propositional/Classical.lagda.md b/src/Logic/Propositional/Classical.lagda.md
index 65ae945a8..90eb7feaf 100644
--- a/src/Logic/Propositional/Classical.lagda.md
+++ b/src/Logic/Propositional/Classical.lagda.md
@@ -624,9 +624,9 @@ tabulate-atom-true
   → ρ x ≡ true
   → tabulate ρ ⊢ atom x
 tabulate-atom-true i _ _ with fin-view i
-tabulate-atom-true {Γ = suc Γ} .fzero ρ x-true | zero with ρ 0
+tabulate-atom-true {Γ = suc Γ} .fzero ρ x-true | zero with ρ 0 in w
 ... | true  = hyp here
-... | false = absurd (true≠false $ sym x-true)
+... | false = absurd (true≠false (sym x-true ∙ Id≃path.to w))
 tabulate-atom-true {Γ = suc Γ} .(fsuc x) ρ x-true | suc x =
   rename (drop idrn) (bump-proof (tabulate-atom-true x (ρ ∘ fsuc) x-true))
 
@@ -636,9 +636,9 @@ tabulate-atom-false
   → ρ x ≡ false
   → tabulate ρ ⊢ “¬” atom x
 tabulate-atom-false i _ _ with fin-view i
-tabulate-atom-false {Γ = suc Γ} .fzero ρ x-false | zero with ρ 0
+tabulate-atom-false {Γ = suc Γ} .fzero ρ x-false | zero with ρ 0 in w
 ... | false = hyp here
-... | true  = absurd (true≠false x-false)
+... | true  = absurd (true≠false (sym (Id≃path.to w) ∙ x-false))
 tabulate-atom-false {Γ = suc Γ} .(fsuc x) ρ x-false | suc x =
   rename (drop idrn) (bump-proof (tabulate-atom-false x (ρ ∘ fsuc) x-false))
 ```
diff --git a/src/Prim/Type.lagda.md b/src/Prim/Type.lagda.md
index 8803026c8..81511d4e4 100644
--- a/src/Prim/Type.lagda.md
+++ b/src/Prim/Type.lagda.md
@@ -13,8 +13,8 @@ system. For more details about the use of universes, see
 {-# BUILTIN TYPE     Type  #-}
 {-# BUILTIN SETOMEGA Typeω #-}
 
-{-# BUILTIN PROP      Prop  #-}
-{-# BUILTIN PROPOMEGA Propω #-}
+{-# BUILTIN PROP      SProp  #-}
+{-# BUILTIN PROPOMEGA SPropω #-}
 
 {-# BUILTIN STRICTSET      SSet  #-}
 {-# BUILTIN STRICTSETOMEGA SSetω #-}

From 3f44de02f551a7c17b1230346f2ca44b6add202f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Am=C3=A9lia=20Liao?= <me@amelia.how>
Date: Tue, 5 May 2026 19:37:14 -0300
Subject: [PATCH 07/12] chore: avoid overload projection crimes

Mikan will 'ship' with a stricter implementation of overloaded
constructor/projection disambiguation than Agda, which requires that
copatterns actually be in scope *as projection functions*, instead of
possibly as fully instantiated values projected from a record.
---
 src/1Lab/Equiv.lagda.md                       |  4 +---
 src/1Lab/Reflection/Copattern.agda            |  6 +++---
 src/Algebra/Group/Subgroup.lagda.md           |  2 +-
 src/Cat/Base.lagda.md                         |  9 +++++----
 src/Cat/Displayed/Instances/Pullback.lagda.md | 20 +++++++++----------
 .../Displayed/Instances/Subobjects.lagda.md   |  2 +-
 src/Cat/Functor/Properties.lagda.md           |  8 ++++----
 src/Cat/Instances/Presheaf/Omega.lagda.md     |  6 +++---
 src/Cat/Morphism.lagda.md                     |  4 +---
 src/Prim/Interval.lagda.md                    |  2 +-
 10 files changed, 30 insertions(+), 33 deletions(-)

diff --git a/src/1Lab/Equiv.lagda.md b/src/1Lab/Equiv.lagda.md
index c6f756ad6..c5040e8a6 100644
--- a/src/1Lab/Equiv.lagda.md
+++ b/src/1Lab/Equiv.lagda.md
@@ -118,9 +118,7 @@ inverse is again an isomorphism.
 
 ```agda
   inverse : is-iso from
-  inverse .from = f
-  inverse .rinv = linv
-  inverse .linv = rinv
+  inverse = record { from = f ; rinv = linv ; linv = rinv }
 ```
 
 <!--
diff --git a/src/1Lab/Reflection/Copattern.agda b/src/1Lab/Reflection/Copattern.agda
index 437995884..85ba08b55 100644
--- a/src/1Lab/Reflection/Copattern.agda
+++ b/src/1Lab/Reflection/Copattern.agda
@@ -202,9 +202,9 @@ private module Test where
   module _ (r : Record Nat) where
     open Record r
     via-function : Record Nat
-    via-function .c = suc c
-    via-function .f = suc ∘ f
-    via-function .const = ap suc const
+    via-function .Record.c = suc c
+    via-function .Record.f = suc ∘ f
+    via-function .Record.const = ap suc const
 
   -- Also works when applied to the result of a function.
   unquoteDecl copat-decl-via-function = declare-copattern copat-decl-via-function (via-function via-ctor)
diff --git a/src/Algebra/Group/Subgroup.lagda.md b/src/Algebra/Group/Subgroup.lagda.md
index 7ed961305..f12c3a4db 100644
--- a/src/Algebra/Group/Subgroup.lagda.md
+++ b/src/Algebra/Group/Subgroup.lagda.md
@@ -25,7 +25,7 @@ module Algebra.Group.Subgroup where
 private variable
   ℓ ℓ' : Level
   G : Group ℓ
-private module _ {ℓ} where open Cat.Displayed.Instances.Subobjects (Groups ℓ) public
+private module _ {ℓ} where open Cat.Displayed.Instances.Subobjects (Groups ℓ) hiding (to ; from) public
 ```
 -->
 
diff --git a/src/Cat/Base.lagda.md b/src/Cat/Base.lagda.md
index 0e3cf9ab4..b1669e27b 100644
--- a/src/Cat/Base.lagda.md
+++ b/src/Cat/Base.lagda.md
@@ -288,10 +288,11 @@ C\op \to D\op$.
 
 ```agda
   op : Functor (C ^op) (D ^op)
-  op .F₀      = F₀
-  op .F₁      = F₁
-  op .F-id    = F-id
-  op .F-∘ f g = F-∘ g f
+  op = record where
+    F₀      = F₀
+    F₁      = F₁
+    F-id    = F-id
+    F-∘ f g = F-∘ g f
 ```
 
 <!--
diff --git a/src/Cat/Displayed/Instances/Pullback.lagda.md b/src/Cat/Displayed/Instances/Pullback.lagda.md
index a1e7d3943..6913e83ae 100644
--- a/src/Cat/Displayed/Instances/Pullback.lagda.md
+++ b/src/Cat/Displayed/Instances/Pullback.lagda.md
@@ -46,11 +46,11 @@ to $B$-indices. The same goes for indexing the displayed $\hom$-sets.
 
 ```agda
 Change-of-base : Displayed X o'' ℓ''
-Change-of-base .Ob[_] x      = E.Ob[ F₀ x ]
-Change-of-base .Hom[_] f x y = E.Hom[ F₁ f ] x y
-Change-of-base .Hom[_]-set f = E.Hom[ F₁ f ]-set
-Change-of-base .id'          = hom[ sym F-id ] E.id'
-Change-of-base ._∘'_ f' g'   = hom[ sym (F-∘ _ _) ] (f' E.∘' g')
+Change-of-base .Displayed.Ob[_] x      = E.Ob[ F₀ x ]
+Change-of-base .Displayed.Hom[_] f x y = E.Hom[ F₁ f ] x y
+Change-of-base .Displayed.Hom[_]-set f = E.Hom[ F₁ f ]-set
+Change-of-base .Displayed.id'          = hom[ sym F-id ] E.id'
+Change-of-base .Displayed._∘'_ f' g'   = hom[ sym (F-∘ _ _) ] (f' E.∘' g')
 ```
 
 Proving that the pullback $F^*(E)$ is indeed a displayed category is a
@@ -62,17 +62,17 @@ category reasoning combinators][dr] are here to help.
 [dr]: Cat.Displayed.Reasoning.html
 
 ```agda
-Change-of-base .idr' {f = f} f' = to-pathp[] $
+Change-of-base .Displayed.idr' {f = f} f' = to-pathp[] $
   hom[] (hom[ F-∘ _ _ ]⁻ (f' E.∘' hom[ F-id ]⁻ _)) ≡⟨ hom[]⟩⟨ smashr _ _ ⟩
   hom[] (hom[] (f' E.∘' E.id'))                    ≡⟨ Ds.disp! E ⟩
   f'                                               ∎
 
-Change-of-base .idl' f' = to-pathp[] $
+Change-of-base .Displayed.idl' f' = to-pathp[] $
   hom[] (hom[ F-∘ _ _ ]⁻ (hom[ F-id ]⁻ _ E.∘' f')) ≡⟨ hom[]⟩⟨ smashl _ _ ⟩
   hom[] (hom[] (E.id' E.∘' f'))                    ≡⟨ Ds.disp! E ⟩
   f'                                               ∎
 
-Change-of-base .assoc' f' g' h' = to-pathp[] $
+Change-of-base .Displayed.assoc' f' g' h' = to-pathp[] $
   hom[ ap F₁ _ ] (hom[ F-∘ _ _ ]⁻ (f' E.∘' hom[ F-∘ _ _ ]⁻ (g' E.∘' h')))   ≡⟨ hom[]⟩⟨ smashr _ _ ⟩
   hom[] (hom[] (f' E.∘' g' E.∘' h'))                                        ≡⟨ Ds.disp! E ⟩
   hom[ sym (F-∘ _ _) ] (hom[ sym (F-∘ _ _) ] (f' E.∘' g') E.∘' h')          ∎
@@ -80,8 +80,8 @@ Change-of-base .assoc' f' g' h' = to-pathp[] $
 
 <!--
 ```agda
-Change-of-base .hom[_] p f' = hom[ ap F₁ p ] f'
-Change-of-base .coh[_] p f' = coh[ ap F₁ p ] f'
+Change-of-base .Displayed.hom[_] p f' = hom[ ap F₁ p ] f'
+Change-of-base .Displayed.coh[_] p f' = coh[ ap F₁ p ] f'
 ```
 -->
 
diff --git a/src/Cat/Displayed/Instances/Subobjects.lagda.md b/src/Cat/Displayed/Instances/Subobjects.lagda.md
index 1440d0c80..d2598b91b 100644
--- a/src/Cat/Displayed/Instances/Subobjects.lagda.md
+++ b/src/Cat/Displayed/Instances/Subobjects.lagda.md
@@ -359,7 +359,7 @@ _≤ₘ_ = ≤-over id
 
 open Sub
   renaming (_≅_ to infix 7 _≅ₘ_)
-  using ()
+  using (to ; from ; inverses)
   public
 
 infix 7 _≤ₘ_
diff --git a/src/Cat/Functor/Properties.lagda.md b/src/Cat/Functor/Properties.lagda.md
index c08736c7e..b32248677 100644
--- a/src/Cat/Functor/Properties.lagda.md
+++ b/src/Cat/Functor/Properties.lagda.md
@@ -187,10 +187,10 @@ the domain category to serve as an inverse for $f$:
     open Cm.is-invertible (is-ff→is-conservative F ff (equiv→inverse ff to) D-inv')
 
     im' : _ Cm.≅ _
-    im' .to   = equiv→inverse ff to
-    im' .from = inv
-    im' .inverses .Cm.Inverses.invl = invl
-    im' .inverses .Cm.Inverses.invr = invr
+    im' .Cm.to   = equiv→inverse ff to
+    im' .Cm.from = inv
+    im' .Cm.inverses .Cm.Inverses.invl = invl
+    im' .Cm.inverses .Cm.Inverses.invr = invr
 ```
 
 ## Essential fibres {defines="essential-fibre"}
diff --git a/src/Cat/Instances/Presheaf/Omega.lagda.md b/src/Cat/Instances/Presheaf/Omega.lagda.md
index 6885ed849..19dadf73c 100644
--- a/src/Cat/Instances/Presheaf/Omega.lagda.md
+++ b/src/Cat/Instances/Presheaf/Omega.lagda.md
@@ -86,9 +86,9 @@ psh-name {P} so .is-natural x y f = ext λ x {V} f → Ω-ua
 PSh-omega : Subobject-classifier (PSh ℓ C)
 PSh-omega .Subobject-classifier.Ω = Sieves
 
-PSh-omega .Subobject-classifier.true .Sub.dom         = _
-PSh-omega .Subobject-classifier.true .Sub.map         = tru
-PSh-omega .Subobject-classifier.true .Sub.monic _ _ _ = ext λ _ _ → refl
+PSh-omega .Subobject-classifier.true .dom         = _
+PSh-omega .Subobject-classifier.true .map         = tru
+PSh-omega .Subobject-classifier.true .monic _ _ _ = ext λ _ _ → refl
 PSh-omega .generic .name = psh-name
 ```
 -->
diff --git a/src/Cat/Morphism.lagda.md b/src/Cat/Morphism.lagda.md
index 27558f84d..6651976c3 100644
--- a/src/Cat/Morphism.lagda.md
+++ b/src/Cat/Morphism.lagda.md
@@ -503,9 +503,7 @@ record is-invertible (f : Hom a b) : Type h where
   open Inverses inverses public
 
   op : is-invertible inv
-  op .inv = f
-  op .inverses .Inverses.invl = invr inverses
-  op .inverses .Inverses.invr = invl inverses
+  op = record { inv = f ; inverses = record { invl = invr inverses ; invr = invl inverses }}
 
 record _≅_ (a b : Ob) : Type h where
   field
diff --git a/src/Prim/Interval.lagda.md b/src/Prim/Interval.lagda.md
index 1d80e540d..c85889077 100644
--- a/src/Prim/Interval.lagda.md
+++ b/src/Prim/Interval.lagda.md
@@ -79,7 +79,7 @@ postulate
 
 The `IsOne`{.Agda} proposition is used as the domain of the type
 `Partial`{.Agda}, where `Partial φ A` is a refinement of the type
-`.(IsOne φ) → A`, where inhabitants `p, q : Partial φ A` are equal iff
+`(IsOne φ) → A`, where inhabitants `p, q : Partial φ A` are equal iff
 they agree on a decomposition of `φ` into DNF.
 
 ```agda

From a5e9baad62386bd2d8d4b3f7cbc0ddb1404d5c50 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Am=C3=A9lia=20Liao?= <me@amelia.how>
Date: Thu, 7 May 2026 15:57:23 -0300
Subject: [PATCH 08/12] chore: port 1lab-shake to Mikan

---
 .github/workflows/build.yml            |  4 +--
 1lab.agda-lib                          |  5 ---
 cabal.project                          |  4 +--
 default.nix                            |  2 +-
 shell.nix                              |  6 ++--
 support/nix/build-shake.nix            |  4 +--
 support/nix/dep/Agda/default.nix       |  2 --
 support/nix/dep/Agda/github.json       |  8 -----
 support/nix/dep/Agda/thunk.nix         | 12 --------
 support/nix/haskell-packages.nix       | 17 ++++++++---
 support/shake/1lab-shake.cabal         |  2 +-
 support/shake/app/Agda.hs              |  6 ++--
 support/shake/app/Definitions.hs       |  2 +-
 support/shake/app/HTML/Backend.hs      | 42 +++++++++++++-------------
 support/shake/app/HTML/Base.hs         | 16 +++++-----
 support/shake/app/HTML/Render.hs       | 12 ++++----
 support/shake/app/Shake/AgdaCompile.hs | 26 ++++++++--------
 17 files changed, 74 insertions(+), 96 deletions(-)
 delete mode 100644 support/nix/dep/Agda/default.nix
 delete mode 100644 support/nix/dep/Agda/github.json
 delete mode 100644 support/nix/dep/Agda/thunk.nix

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 7f305992a..1300a2439 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -58,7 +58,7 @@ jobs:
       - name: Typecheck 👩‍🏫
         run: |
           nix-shell --run "$build_command"
-        # Run Agda as a separate stage so it doesn't have to be subject to
+        # Run Mikan as a separate stage so it doesn't have to be subject to
         # the absolutely spartan GC tuning parameters we run the build in
         # CI with
         env:
@@ -66,7 +66,7 @@ jobs:
           build_command: |
             set -eu
             1lab-shake _build/all-pages.agda
-            agda-nodebug _build/all-pages.agda -j4 +RTS -s -RTS
+            mikan-nodebug _build/all-pages.agda -j4 +RTS -s -RTS
 
       - name: Build 🛠️
         run: |
diff --git a/1lab.agda-lib b/1lab.agda-lib
index c1c2dc9e9..5beab3325 100644
--- a/1lab.agda-lib
+++ b/1lab.agda-lib
@@ -4,13 +4,8 @@ include:
   wip
   _build
 flags:
-  --cubical
   --prop
   --no-load-primitives
   --postfix-projections
-  --guardedness
-  --two-level
   -W noUnsupportedIndexedMatch
-  -W noRewriteVariablesBoundInSingleton
   --experimental-lazy-instances
-  --no-experimental-irrelevance
diff --git a/cabal.project b/cabal.project
index ae9320da1..4b383a523 100644
--- a/cabal.project
+++ b/cabal.project
@@ -1,12 +1,12 @@
 packages: support/shake/1lab-shake.cabal
 
 -- To build outside of the Nix shell, uncomment the following stanza
--- and replace `master` with the `rev` field from `support/nix/dep/Agda/github.json`.
+-- and replace `main` with the `rev` field from `support/nix/dep/mikan/github.json`.
 --
 -- If you want to avoid polluting your Git tree, you can move this to
 -- `cabal.project.local`, which is ignored by Git.
 
 -- source-repository-package
 --   type: git
---   location: https://github.com/agda/agda.git
+--   location: https://codeberg.org/1lab/mikan.git
 --   tag: master
diff --git a/default.nix b/default.nix
index 42a6c5b31..e5762ab2e 100644
--- a/default.nix
+++ b/default.nix
@@ -98,7 +98,7 @@ in
 
     passthru = {
       inherit pkgs shakefile deps sort-imports nodeModules;
-      inherit (pkgs.labHaskellPackages) Agda;
+      inherit (pkgs.labHaskellPackages) Mikan;
       texlive = our-texlive;
     };
   }
diff --git a/shell.nix b/shell.nix
index c7127f62e..2cfc9e9bc 100644
--- a/shell.nix
+++ b/shell.nix
@@ -11,10 +11,10 @@ the1lab.overrideAttrs (old: {
 
   nativeBuildInputs = old.nativeBuildInputs or [] ++ [
     (with pkgs.labHaskellPackages; pkgs.symlinkJoin {
-      name  = "agda-nodebug";
-      paths = [ Agda sort-imports ];
+      name  = "mikan";
+      paths = [ Mikan sort-imports ];
       postBuild = ''
-        ln -sf ${Agda.nodebug}/bin/agda $out/bin/agda-nodebug
+        ln -sf ${Mikan.nodebug}/bin/mikan $out/bin/mikan-nodebug
       '';
     })
   ];
diff --git a/support/nix/build-shake.nix b/support/nix/build-shake.nix
index 57d6e3e60..254549a61 100644
--- a/support/nix/build-shake.nix
+++ b/support/nix/build-shake.nix
@@ -14,13 +14,13 @@ let
     aeson pandoc SHA pandoc-types HTTP
     js-flot js-jquery js-dgtable
 
-    Agda.nodebug
+    Mikan.nodebug
   ];
 
   root = nix-gitignore.gitignoreSource [] ../shake;
 in
   lib.pipe (labHaskellPackages.callCabal2nix "1lab-shake" root {
-    Agda = labHaskellPackages.Agda.nodebug;
+    Mikan = labHaskellPackages.Mikan.nodebug;
   }) [
     (hlib.addBuildTools [ removeReferencesTo ])
     (hlib.overrideCabal (drv: {
diff --git a/support/nix/dep/Agda/default.nix b/support/nix/dep/Agda/default.nix
deleted file mode 100644
index 2b4d4ab11..000000000
--- a/support/nix/dep/Agda/default.nix
+++ /dev/null
@@ -1,2 +0,0 @@
-# DO NOT HAND-EDIT THIS FILE
-import (import ./thunk.nix)
\ No newline at end of file
diff --git a/support/nix/dep/Agda/github.json b/support/nix/dep/Agda/github.json
deleted file mode 100644
index 802d76cb7..000000000
--- a/support/nix/dep/Agda/github.json
+++ /dev/null
@@ -1,8 +0,0 @@
-{
-  "owner": "agda",
-  "repo": "agda",
-  "branch": "master",
-  "private": false,
-  "rev": "295c60c79cd49e880b9f07add98462f1b82d26f2",
-  "sha256": "1rw76b77mkhjigpi81ddqi2vgjqh3qv3wwznlwd7fp1d0h71xglf"
-}
diff --git a/support/nix/dep/Agda/thunk.nix b/support/nix/dep/Agda/thunk.nix
deleted file mode 100644
index 20f2d28c2..000000000
--- a/support/nix/dep/Agda/thunk.nix
+++ /dev/null
@@ -1,12 +0,0 @@
-# DO NOT HAND-EDIT THIS FILE
-let fetch = { private ? false, fetchSubmodules ? false, owner, repo, rev, sha256, ... }:
-  if !fetchSubmodules && !private then builtins.fetchTarball {
-    url = "https://github.com/${owner}/${repo}/archive/${rev}.tar.gz"; inherit sha256;
-  } else (import (builtins.fetchTarball {
-  url = "https://github.com/NixOS/nixpkgs/archive/3aad50c30c826430b0270fcf8264c8c41b005403.tar.gz";
-  sha256 = "0xwqsf08sywd23x0xvw4c4ghq0l28w2ki22h0bdn766i16z9q2gr";
-}) {}).fetchFromGitHub {
-    inherit owner repo rev sha256 fetchSubmodules private;
-  };
-  json = builtins.fromJSON (builtins.readFile ./github.json);
-in fetch json
\ No newline at end of file
diff --git a/support/nix/haskell-packages.nix b/support/nix/haskell-packages.nix
index 3144835d3..b5c07066b 100644
--- a/support/nix/haskell-packages.nix
+++ b/support/nix/haskell-packages.nix
@@ -1,6 +1,5 @@
 pkgs: super:
 let
-  thunkSource = (import ./dep/nix-thunk { inherit pkgs; }).thunkSource;
   inherit (pkgs) lib;
   hlib = pkgs.haskell.lib.compose;
 
@@ -9,21 +8,29 @@ let
     doHaddock = false;
     testHaskellDepends = [];
   };
+
   noProfile = hlib.overrideCabal {
     enableExecutableProfiling = false;
     enableLibraryProfiling = false;
   };
 
-  agda = hsuper: suf: flags: noJunk (
-    hsuper.callCabal2nixWithOptions "Agda-${suf}" (thunkSource ./dep/Agda) flags {}
+  src = pkgs.fetchgit {
+    url             = "https://codeberg.org/1lab/mikan.git";
+    rev             = "2f4c616229bcd5b9ea926e5001bce5c00a1df2bb";
+    sha256          = "sha256-zCpJM+SpmRlsDxI1wXyNDxhWgEI/2oAXZhjP9G8SMaI=";
+    fetchSubmodules = false;
+  };
+
+  mikan = hsuper: suf: flags: noJunk (
+    hsuper.callCabal2nixWithOptions "Mikan-${suf}" src flags {}
   );
 in
   {
     labHaskellPackages = super.haskell.packages.ghc910.override (old: {
       overrides = hself: hsuper: {
-        Agda = (agda hsuper "debug" "-foptimise-heavily -fdebug").overrideAttrs (old: {
+        Mikan = (mikan hsuper "debug" "-foptimise-heavily -fdebug").overrideAttrs (old: {
           passthru = old.passthru // {
-            nodebug = noProfile (agda hsuper "nodebug" "-foptimise-heavily");
+            nodebug = noProfile (mikan hsuper "nodebug" "-foptimise-heavily");
           };
         });
       };
diff --git a/support/shake/1lab-shake.cabal b/support/shake/1lab-shake.cabal
index af9c415ac..2f93eb1f4 100644
--- a/support/shake/1lab-shake.cabal
+++ b/support/shake/1lab-shake.cabal
@@ -8,7 +8,7 @@ common common
   build-depends:
     base >=4.14.3.0,
     aeson,
-    Agda,
+    Mikan,
     blaze-html,
     blaze-markup,
     bytestring,
diff --git a/support/shake/app/Agda.hs b/support/shake/app/Agda.hs
index abb185ff0..658d5104a 100644
--- a/support/shake/app/Agda.hs
+++ b/support/shake/app/Agda.hs
@@ -1,9 +1,9 @@
 module Agda where
 
-import Agda.Interaction.Options
-import Agda.TypeChecking.Monad
+import Mikan.Interaction.Options
+import Mikan.TypeChecking.Monad
 import Control.Monad.IO.Class
-import Agda.Utils.FileName
+import Mikan.Utils.FileName
 
 import System.FilePath
 
diff --git a/support/shake/app/Definitions.hs b/support/shake/app/Definitions.hs
index 6066f6f3b..160b9d42f 100644
--- a/support/shake/app/Definitions.hs
+++ b/support/shake/app/Definitions.hs
@@ -13,7 +13,7 @@ module Definitions
   )
   where
 
-import Agda.Utils.Impossible
+import Mikan.Utils.Impossible
 
 import Control.Monad.IO.Class
 import Control.DeepSeq
diff --git a/support/shake/app/HTML/Backend.hs b/support/shake/app/HTML/Backend.hs
index b51ce74ca..533136e72 100644
--- a/support/shake/app/HTML/Backend.hs
+++ b/support/shake/app/HTML/Backend.hs
@@ -23,29 +23,29 @@ import Data.Foldable
 import Data.Text (Text)
 import Data.Set (Set)
 
-import Agda.Compiler.Backend hiding (topLevelModuleName)
-import Agda.Compiler.Common
+import Mikan.Compiler.Backend hiding (topLevelModuleName)
+import Mikan.Compiler.Common
 
 import Control.DeepSeq
 
-import qualified Agda.Syntax.Internal.Generic as I
-import qualified Agda.Syntax.Abstract.Views as A
-import qualified Agda.Syntax.Common.Aspect as Asp
-import qualified Agda.Syntax.Internal as I
-import qualified Agda.Syntax.Abstract as A
-
-import Agda.Syntax.Translation.InternalToAbstract ( Reify(reify) )
-import Agda.Syntax.Abstract.Pretty (prettyATop)
-import Agda.Syntax.Common.Pretty
-import Agda.Syntax.Abstract hiding (Type)
-import Agda.Syntax.Position
-import Agda.Syntax.Common
-import Agda.Syntax.Info
-
-import qualified Agda.TypeChecking.Monad.Base as I
-import qualified Agda.TypeChecking.Pretty as P
-import Agda.TypeChecking.Records (isRecord)
-import Agda.TypeChecking.Reduce (normalise)
+import qualified Mikan.Syntax.Internal.Generic as I
+import qualified Mikan.Syntax.Abstract.Views as A
+import qualified Mikan.Syntax.Common.Aspect as Asp
+import qualified Mikan.Syntax.Internal as I
+import qualified Mikan.Syntax.Abstract as A
+
+import Mikan.Syntax.Translation.InternalToAbstract ( Reify(reify) )
+import Mikan.Syntax.Abstract.Pretty (prettyATop)
+import Mikan.Syntax.Common.Pretty
+import Mikan.Syntax.Abstract hiding (Type)
+import Mikan.Syntax.Position
+import Mikan.Syntax.Common
+import Mikan.Syntax.Info
+
+import qualified Mikan.TypeChecking.Monad.Base as I
+import qualified Mikan.TypeChecking.Pretty as P
+import Mikan.TypeChecking.Records (isRecord)
+import Mikan.TypeChecking.Reduce (normalise)
 
 import HTML.Render
 
@@ -91,7 +91,7 @@ usedInstances :: I.TermLike a => a -> TCM (Set QName)
 usedInstances = I.foldTerm \case
   I.Def q _ -> do
     def <- getConstInfo q
-    case Agda.Compiler.Backend.defInstance def of
+    case Mikan.Compiler.Backend.defInstance def of
       Just c  -> Set.insert q <$> getClass (instanceClass c)
       Nothing -> pure mempty
   _ -> pure mempty
diff --git a/support/shake/app/HTML/Base.hs b/support/shake/app/HTML/Base.hs
index 7564b98c5..281168b4a 100644
--- a/support/shake/app/HTML/Base.hs
+++ b/support/shake/app/HTML/Base.hs
@@ -46,20 +46,20 @@ import Text.Blaze.Html.Renderer.Text ( renderHtml )
 
 -- import Paths_Agda
 
-import Agda.Interaction.Highlighting.Precise hiding (toList)
+import Mikan.Interaction.Highlighting.Precise hiding (toList)
 
-import Agda.Syntax.TopLevelModuleName (TopLevelModuleName)
-import Agda.Syntax.Common.Pretty
-import Agda.Syntax.Common
+import Mikan.Syntax.TopLevelModuleName (TopLevelModuleName)
+import Mikan.Syntax.Common.Pretty
+import Mikan.Syntax.Common
 
-import qualified Agda.TypeChecking.Monad as TCM
+import qualified Mikan.TypeChecking.Monad as TCM
   ( Interface(..)
   )
 
-import Agda.Utils.Function
-import qualified Agda.Utils.IO.UTF8 as UTF8
+import Mikan.Utils.Function
+import qualified Mikan.Utils.IO.UTF8 as UTF8
 
-import Agda.Utils.Impossible
+import Mikan.Utils.Impossible
 
 import HTML.Render
 
diff --git a/support/shake/app/HTML/Render.hs b/support/shake/app/HTML/Render.hs
index 8fbbfe1c7..6e648eca5 100644
--- a/support/shake/app/HTML/Render.hs
+++ b/support/shake/app/HTML/Render.hs
@@ -3,13 +3,13 @@ module HTML.Render where
 
 import Prelude hiding ((!!))
 
-import Agda.Syntax.TopLevelModuleName (TopLevelModuleName)
-import Agda.Syntax.Common.Aspect
-import Agda.Syntax.Common.Pretty
+import Mikan.Syntax.TopLevelModuleName (TopLevelModuleName)
+import Mikan.Syntax.Common.Aspect
+import Mikan.Syntax.Common.Pretty
 
-import Agda.Utils.Impossible (__IMPOSSIBLE__)
-import Agda.Utils.Function
-import Agda.Utils.DocTree
+import Mikan.Utils.Impossible (__IMPOSSIBLE__)
+import Mikan.Utils.Function
+import Mikan.Utils.DocTree
 
 import Control.DeepSeq
 import Control.Monad
diff --git a/support/shake/app/Shake/AgdaCompile.hs b/support/shake/app/Shake/AgdaCompile.hs
index cda9b23f2..2c16cd02f 100644
--- a/support/shake/app/Shake/AgdaCompile.hs
+++ b/support/shake/app/Shake/AgdaCompile.hs
@@ -10,7 +10,7 @@ import Control.Monad
 
 import qualified Data.IntMap.Strict as IntMap
 import qualified Data.List.NonEmpty as List1
-import qualified Agda.Utils.BiMap as BiMap
+import qualified Mikan.Utils.BiMap as BiMap
 import qualified Data.Binary as Binary
 import qualified Data.Aeson as Aeson
 import qualified Data.Text as T
@@ -27,22 +27,21 @@ import Development.Shake
 
 import Shake.Options (getSkipTypes, getWatching, getBaseUrl, getSkipAgda)
 
-import Agda.Compiler.Backend hiding (getEnv)
-import Agda.TypeChecking.Pretty.Warning
-import Agda.TypeChecking.Errors
-import Agda.Interaction.Imports hiding (getInterface)
-import Agda.Interaction.Options
-import Agda.Syntax.Common (Cubical(CFull))
-import Agda.Syntax.Common.Pretty
-import Agda.Syntax.TopLevelModuleName
+import Mikan.Compiler.Backend hiding (getEnv)
+import Mikan.TypeChecking.Pretty.Warning
+import Mikan.TypeChecking.Errors
+import Mikan.Interaction.Imports hiding (getInterface)
+import Mikan.Interaction.Options
+import Mikan.Syntax.Common.Pretty
+import Mikan.Syntax.TopLevelModuleName
   ( TopLevelModuleName'(..)
   , RawTopLevelModuleName(..)
   , hashRawTopLevelModuleName
   )
-import Agda.Syntax.Position (noRange)
-import Agda.Utils.FileName
-import Agda.Utils.Hash (Hash)
-import Agda.Utils.Lens ((^.))
+import Mikan.Syntax.Position (noRange)
+import Mikan.Utils.FileName
+import Mikan.Utils.Hash (Hash)
+import Mikan.Utils.Lens ((^.))
 
 import HTML.Backend
 import HTML.Render
@@ -195,7 +194,6 @@ compileAgda stateVar = do
       resetState
 
       -- Force Cubical even if we've not got a --cubical header.
-      stPragmaOptions `modifyTCLens` \ o -> o { _optCubical = Just CFull }
       setCommandLineOptions' baseDir defaultOptions
 
       for_ target \source -> do

From 2d4478b7c1e7ae3c25bf686ce431760ef660210d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Am=C3=A9lia=20Liao?= <me@amelia.how>
Date: Fri, 8 May 2026 20:16:30 -0300
Subject: [PATCH 09/12] chore: remove modalities
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-Authored-By: Naïm Favier <n@monade.li>
---
 src/1Lab/Reflection.lagda.md            | 14 ++---
 src/1Lab/Reflection/Deriving/Show.agda  |  7 +--
 src/1Lab/Reflection/Induction.agda      |  5 +-
 src/1Lab/Reflection/Record.agda         |  5 +-
 src/1Lab/Reflection/Regularity.agda     |  2 +-
 src/1Lab/Reflection/Signature.agda      | 26 +++------
 src/1Lab/Type.lagda.md                  |  6 +-
 src/1Lab/Univalence.lagda.md            |  6 +-
 src/Algebra/Group/Solver.agda           |  4 +-
 src/Algebra/Ring/Solver.agda            |  8 +--
 src/Cat/Bi/Solver.agda                  | 10 ++--
 src/Cat/Diagram/Product/Solver.lagda.md | 22 ++++----
 src/Cat/Displayed/Solver.agda           |  8 +--
 src/Cat/Functor/Solver.agda             |  4 +-
 src/Cat/Solver.lagda.md                 |  2 +-
 src/Data/Nat/DivMod.lagda.md            |  4 +-
 src/Data/Reflection/Argument.agda       | 74 ++++---------------------
 src/Data/Reflection/Term.agda           | 14 ++---
 src/Homotopy/Space/Delooping.lagda.md   |  2 +-
 src/Prim/Extension.lagda.md             |  4 +-
 src/Prim/Interval.lagda.md              |  3 +-
 support/nix/dep/nix-thunk/default.nix   |  2 -
 support/nix/dep/nix-thunk/github.json   |  8 ---
 support/nix/dep/nix-thunk/thunk.nix     | 12 ----
 support/nix/haskell-packages.nix        |  4 +-
 25 files changed, 81 insertions(+), 175 deletions(-)
 delete mode 100644 support/nix/dep/nix-thunk/default.nix
 delete mode 100644 support/nix/dep/nix-thunk/github.json
 delete mode 100644 support/nix/dep/nix-thunk/thunk.nix

diff --git a/src/1Lab/Reflection.lagda.md b/src/1Lab/Reflection.lagda.md
index b56463aaa..17ebd3bf6 100644
--- a/src/1Lab/Reflection.lagda.md
+++ b/src/1Lab/Reflection.lagda.md
@@ -103,9 +103,6 @@ private module P where
   -- "blocking" constraints.
     noConstraints : ∀ {a} {A : Type a} → TC A → TC A
 
-  -- Run the given computation at the type level, allowing use of erased things.
-    work-on-types : ∀ {a} {A : Type a} → TC A → TC A
-
   -- Run the given TC action and return the first component. Resets to
   -- the old TC state if the second component is 'false', or keep the
   -- new TC state if it is 'true'.
@@ -116,7 +113,7 @@ private module P where
     get-instances : Meta → TC (List Term)
 
     declareData      : Name → Nat → Term → TC ⊤
-    defineData       : Name → List (Name × Quantity × Term) → TC ⊤
+    defineData       : Name → List (Name × Term) → TC ⊤
 ```
 
 <details>
@@ -161,7 +158,6 @@ private module P where
   {-# BUILTIN AGDATCMASKEXPANDLAST     askExpandLast              #-}
   {-# BUILTIN AGDATCMASKREDUCEDEFS     askReduceDefs              #-}
   {-# BUILTIN AGDATCMNOCONSTRAINTS     noConstraints              #-}
-  {-# BUILTIN AGDATCMWORKONTYPES       work-on-types              #-}
   {-# BUILTIN AGDATCMRUNSPECULATIVE    run-speculative            #-}
   {-# BUILTIN AGDATCMGETINSTANCES      get-instances              #-}
   {-# BUILTIN AGDATCMDECLAREDATA       declareData                #-}
@@ -201,7 +197,7 @@ idfun : ∀ {ℓ} (A : Type ℓ) → A → A
 idfun A x = x
 
 under-abs : ∀ {ℓ} {A : Type ℓ} → Term → TC A → TC A
-under-abs (lam v (abs nm _)) m = extend-context nm (arg (arginfo v (modality relevant quantity-ω)) unknown) m
+under-abs (lam v (abs nm _)) m = extend-context nm (arg (arginfo v) unknown) m
 under-abs (pi a (abs nm _))  m = extend-context nm a m
 under-abs _ m = m
 
@@ -294,9 +290,9 @@ blocking-meta (lit l)          = nothing
 blocking-meta (meta x _)       = just (blocker-meta x)
 blocking-meta unknown          = nothing
 
-blocking-meta* (arg (arginfo visible _)   tm ∷ _) = blocking-meta tm
-blocking-meta* (arg (arginfo instance' _) tm ∷ _) = blocking-meta tm
-blocking-meta* (arg (arginfo hidden _)    tm ∷ as) = blocking-meta* as
+blocking-meta* (arg (arginfo visible)   tm ∷ _) = blocking-meta tm
+blocking-meta* (arg (arginfo instance') tm ∷ _) = blocking-meta tm
+blocking-meta* (arg (arginfo hidden)    tm ∷ as) = blocking-meta* as
 
 blocking-meta* [] = nothing
 
diff --git a/src/1Lab/Reflection/Deriving/Show.agda b/src/1Lab/Reflection/Deriving/Show.agda
index 9c965248e..f79c40424 100644
--- a/src/1Lab/Reflection/Deriving/Show.agda
+++ b/src/1Lab/Reflection/Deriving/Show.agda
@@ -105,14 +105,14 @@ private
 
   -- Create the clause of shows-prec for a constructor.
   show-clause : Constructor → TC Clause
-  show-clause (conhead conm _ _ args _) = do
+  show-clause (conhead conm _ args _) = do
     let
       -- We'll only show the visible arguments to the constructor.
       -- Moreover, since Agda can infer the types in the telescope
       -- better than we can specify them here, we replace everything
       -- with `unknown`.
       tele = map (λ (s , arg i t) → s , arg i unknown) $
-        filter (λ { (_ , arg (arginfo visible _) _) → true
+        filter (λ { (_ , arg (arginfo visible) _) → true
                   ; _ → false
                   })
           args
@@ -198,9 +198,6 @@ instance
 
   unquoteDecl Show-Literal    = derive-show Show-Literal    (quote Literal)
   unquoteDecl Show-Visibility = derive-show Show-Visibility (quote Visibility)
-  unquoteDecl Show-Relevance  = derive-show Show-Relevance  (quote Relevance)
-  unquoteDecl Show-Quantity   = derive-show Show-Quantity   (quote Quantity)
-  unquoteDecl Show-Modality   = derive-show Show-Modality   (quote Modality)
   unquoteDecl Show-ArgInfo    = derive-show Show-ArgInfo    (quote ArgInfo)
   unquoteDecl Show-Abs        = derive-show Show-Abs        (quote Abs)
   unquoteDecl Show-Arg        = derive-show Show-Arg        (quote Arg)
diff --git a/src/1Lab/Reflection/Induction.agda b/src/1Lab/Reflection/Induction.agda
index d688d07ae..39cb22278 100644
--- a/src/1Lab/Reflection/Induction.agda
+++ b/src/1Lab/Reflection/Induction.agda
@@ -234,8 +234,7 @@ private
           -- Otherwise, add m : T to the telescope and replace the corresponding
           -- constructor with m henceforth.
           method ← ("P" <>_) <$> render-name c
-          q ← get-con-quantity c
-          let argC = arg (arginfo visible (modality relevant q))
+          let argC = arg (arginfo visible)
           let
             ps = raise 1 ps
             P = raise 1 P
@@ -244,7 +243,7 @@ private
             ×-map₁₂ ((method , argC methodT) ∷_) (α ∷_)
 
 make-elim-with : Elim-options → Name → Name → TC ⊤
-make-elim-with opts elim D = work-on-types $ withNormalisation true do
+make-elim-with opts elim D = withNormalisation true do
   DT ← get-type D >>= normalise -- D : (ps : Γ) (is : Ξ) → Type _
   data-type pars cs ← get-definition D
     where _ → typeError [ "not a data type: " , nameErr D ]
diff --git a/src/1Lab/Reflection/Record.agda b/src/1Lab/Reflection/Record.agda
index 5c38b517a..12cb03fa0 100644
--- a/src/1Lab/Reflection/Record.agda
+++ b/src/1Lab/Reflection/Record.agda
@@ -154,7 +154,7 @@ make-record-iso-sigma declare? nm `R = do
 
   let fields = field-names→paths fields
 
-  when declare? $ work-on-types do
+  when declare? do
     `R-ty ← normalise =<< get-type `R
     con-ty ← normalise =<< get-type `R-con
     let con-ty = instantiate' `R-ty con-ty
@@ -210,8 +210,7 @@ make-record-path declare? nm `R = do
   let ps' = filter id ps
       n = length ps'
 
-  when declare? $ work-on-types do
-    declare (argN nm) ty
+  when declare? $ declare (argN nm) ty
 
   define-function nm
     [ clause
diff --git a/src/1Lab/Reflection/Regularity.agda b/src/1Lab/Reflection/Regularity.agda
index 577f57bea..debc11e39 100644
--- a/src/1Lab/Reflection/Regularity.agda
+++ b/src/1Lab/Reflection/Regularity.agda
@@ -189,7 +189,7 @@ module Regularity where
 -- Test cases.
 module
   _ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (f g : A → B) (x : A)
-    (a-loop : (i : I) → Type ℓ [ (i ∨ ~ i) ↦ (λ ._ → A) ])
+    (a-loop : (i : I) → Type ℓ [ (i ∨ ~ i) ↦ (λ _ → A) ])
   where private
 
   p : (h : ∀ x → f x ≡ g x)
diff --git a/src/1Lab/Reflection/Signature.agda b/src/1Lab/Reflection/Signature.agda
index a11956416..3884fd820 100644
--- a/src/1Lab/Reflection/Signature.agda
+++ b/src/1Lab/Reflection/Signature.agda
@@ -22,12 +22,6 @@ get-record-type n = get-definition n >>= λ where
   (record-type conm fields) → pure (conm , fields)
   _ → typeError [ "get-record-type: definition " , nameErr n , " is not a record type." ]
 
--- Look up a constructor's quantity in the signature.
-get-con-quantity : Name → TC Quantity
-get-con-quantity n = get-definition n >>= λ where
-  (data-cons _ q) → pure q
-  _ → typeError [ "get-con-erasure: definition " , nameErr n , " is not a constructor." ]
-
 -- Representation of a data/record constructor.
 record Constructor : Type where
   constructor conhead
@@ -38,9 +32,6 @@ record Constructor : Type where
     -- Name of the data type:
     con-data      : Name
 
-    -- Quantity of the constructor.
-    con-quantity  : Quantity
-
     -- Argument telescope for the constructor, with the datatype's
     -- parameters removed.
     con-arguments : Telescope
@@ -64,23 +55,22 @@ get-type-constructors n = datatype <|> recordtype where
   datatype = do
     (npars , cons) ← get-data-type n
     for cons λ qn → do
-      q ← get-con-quantity qn
       (args , ty) ← pi-view <$> get-type qn
-      pure (conhead qn n q (drop npars args) ty)
+      pure (conhead qn n (drop npars args) ty)
 
   recordtype = do
     (c  , _)    ← get-record-type n
     (np , _)    ← pi-view <$> get-type n
     (args , ty) ← pi-view <$> get-type c
-    pure ((conhead c n quantity-ω (drop (length np) args) ty) ∷ [])
+    pure ((conhead c n (drop (length np) args) ty) ∷ [])
 
 -- Look up a constructor in the signature.
 get-constructor : Name → TC Constructor
 get-constructor n = get-definition n >>= λ where
-  (data-cons t q) → do
+  (data-cons t) → do
     (npars , cons) ← get-data-type t
     (args , ty)    ← pi-view <$> get-type n
-    pure (conhead n t q (drop npars args) ty)
+    pure (conhead n t (drop npars args) ty)
   _ → typeError [ "get-constructor: " , nameErr n , " is not a data constructor." ]
 
 -- If a term reduces to an application of a record type, return
@@ -121,7 +111,7 @@ instance
 private
   it-worker : Name → TC Term
   it-worker n = get-definition n <&> λ where
-    (data-cons _ _) →
+    (data-cons _) →
       def₀ (quote Has-constr.from-constr) ##ₙ def₀ (quote auto) ##ₙ lit (name n)
     _ →
       def₀ (quote Has-def.from-def) ##ₙ def₀ (quote auto) ##ₙ lit (name n)
@@ -161,7 +151,7 @@ macro
     tm   ← it-worker n
     args ← get-argument-tele n
     let
-      args = filter (λ { (_ , arg (arginfo visible _) _) → true ; _ → false }) args
+      args = filter (λ { (_ , arg (arginfo visible) _) → true ; _ → false }) args
 
       tm = def (quote applyⁿᵉ) (argN tm ∷ argN (list-term (reverse (map-up (λ i _ → it argN ##ₙ var₀ i) 0 args))) ∷ [])
       tm = foldr (λ _ y → lam visible (abs "_" y)) tm args
@@ -190,8 +180,8 @@ render-name def-nm = do
   d ← is-defined def-nm
   let
     fancy = get-definition def-nm >>= λ where
-      (data-cons _ _) → formatErrorParts [ termErr (con₀ def-nm) ]
-      _               → formatErrorParts [ termErr (def₀ def-nm) ]
+      (data-cons _ ) → formatErrorParts [ termErr (con₀ def-nm) ]
+      _              → formatErrorParts [ termErr (def₀ def-nm) ]
     plain = show def-nm
   if d then fancy else pure plain
 
diff --git a/src/1Lab/Type.lagda.md b/src/1Lab/Type.lagda.md
index e77359e36..a44526743 100644
--- a/src/1Lab/Type.lagda.md
+++ b/src/1Lab/Type.lagda.md
@@ -254,11 +254,7 @@ auto ⦃ a ⦄ = a
 {-# INLINE _$_ #-}
 
 infixr 40 _∘_
-infixr -1 _$ᵢ_ _$ₛ_
-
-_$ᵢ_ : ∀ {ℓ₁ ℓ₂} {A : Type ℓ₁} {B : .A → Type ℓ₂} → (.(x : A) → B x) → (.(x : A) → B x)
-f $ᵢ x = f x
-{-# INLINE _$ᵢ_ #-}
+infixr -1 _$ₛ_
 
 _$ₛ_ : ∀ {ℓ₁ ℓ₂} {A : Type ℓ₁} {B : A → SSet ℓ₂} → ((x : A) → B x) → ((x : A) → B x)
 f $ₛ x = f x
diff --git a/src/1Lab/Univalence.lagda.md b/src/1Lab/Univalence.lagda.md
index fac10f597..b8776b167 100644
--- a/src/1Lab/Univalence.lagda.md
+++ b/src/1Lab/Univalence.lagda.md
@@ -127,7 +127,7 @@ Glue A {φ} Te = primGlue A tys eqvs module glue-sys where
   tys : Partial φ (Type _)
   tys (φ = i1) = Te 1=1 .fst
 
-  eqvs : PartialP φ (λ .o → tys _ ≃ A)
+  eqvs : PartialP φ (λ o → tys _ ≃ A)
   eqvs (φ = i1) = Te 1=1 .snd
 
 unattach
@@ -246,7 +246,7 @@ ua {A = A} {B} eqv i = primGlue B tys eqvs module ua-sys where
   tys (i = i0) = A
   tys (i = i1) = B
 
-  eqvs : PartialP (∂ i) (λ .o → tys o ≃ B)
+  eqvs : PartialP (∂ i) (λ o → tys o ≃ B)
   eqvs (i = i0) = eqv
   eqvs (i = i1) = id≃
 ```
@@ -816,7 +816,7 @@ sym-ua {A = A} {B = B} e i j = Glue B λ where
   (j = i1) → A , e
 
 ua-inc : ∀ {ℓ} {A₀ A₁ : Type ℓ} (e : A₀ ≃ A₁) (x : A₀) (i : I) → ua e i
-ua-inc e x i = ua-glue e i (λ ._ → x) (inS (e .fst x))
+ua-inc e x i = ua-glue e i (λ _ → x) (inS (e .fst x))
 
 ua→
   : ∀ {e : A₀ ≃ A₁} {B : (i : I) → ua e i → Type ℓ'} {f₀ f₁}
diff --git a/src/Algebra/Group/Solver.agda b/src/Algebra/Group/Solver.agda
index 1d643ac7b..efa46bacc 100644
--- a/src/Algebra/Group/Solver.agda
+++ b/src/Algebra/Group/Solver.agda
@@ -187,8 +187,8 @@ module _ {ℓ} {A : Type ℓ} (G : Group-on A) where
   expand e ρ = ⟦ eval e ⟧ᵥ ρ
 
 module Reflection where
-  pattern is-group-args args = (_ hm∷ _ hm∷ _ hm∷ _ v∷ args)
-  pattern group-args args = (_ hm∷ _ hm∷ _ v∷ args)
+  pattern is-group-args args = (_ h∷ _ h∷ _ h∷ _ v∷ args)
+  pattern group-args args = (_ h∷ _ h∷ _ v∷ args)
 
   pattern “unit” = def (quote is-group.unit) (is-group-args [])
   pattern “⋆” x y = def (quote Group-on._⋆_) (group-args (x v∷ y v∷ []))
diff --git a/src/Algebra/Ring/Solver.agda b/src/Algebra/Ring/Solver.agda
index a29aa20ad..a94d1d5e7 100644
--- a/src/Algebra/Ring/Solver.agda
+++ b/src/Algebra/Ring/Solver.agda
@@ -443,16 +443,16 @@ module Explicit {ℓ} (R : CRing ℓ) where
 
 module Reflection where
   private
-    pattern ring-args cring args = (_ hm∷ _ hm∷ cring v∷ args)
-    pattern is-ring-args is-ring args = (_ hm∷ _ hm∷ _ hm∷ _ hm∷ _ hm∷ is-ring v∷ args)
-    pattern is-group-args is-group args = (_ hm∷ _ hm∷ _ hm∷ is-group v∷ args)
+    pattern ring-args cring args = (_ h∷ _ h∷ cring v∷ args)
+    pattern is-ring-args is-ring args = (_ h∷ _ h∷ _ h∷ _ h∷ _ h∷ is-ring v∷ args)
+    pattern is-group-args is-group args = (_ h∷ _ h∷ _ h∷ is-group v∷ args)
     pattern ring-field field-name cring args =
       def field-name (ring-args (def (quote CRing-on.has-ring-on) (ring-args cring [])) args)
     pattern group-field field-name cring args =
       def field-name
         (is-group-args
           (def (quote (is-abelian-group.has-is-group))
-            (_ hm∷ _ hm∷ _ hm∷ def (quote is-ring.+-group)
+            (_ h∷ _ h∷ _ h∷ def (quote is-ring.+-group)
               (is-ring-args (ring-field (quote Ring-on.has-is-ring) cring []) []) v∷ []))
           args)
 
diff --git a/src/Cat/Bi/Solver.agda b/src/Cat/Bi/Solver.agda
index 5e9ccaf83..b87009e7c 100644
--- a/src/Cat/Bi/Solver.agda
+++ b/src/Cat/Bi/Solver.agda
@@ -446,11 +446,11 @@ module NbE {o ℓ ℓ'} (C : Prebicategory o ℓ ℓ') where
 
 module Reflection where
 
-  pattern category-args cat xs    = _ hm∷ _ hm∷ cat v∷ xs
+  pattern category-args cat xs    = _ h∷ _ h∷ cat v∷ xs
   pattern functor-args functor xs =
-    _ hm∷ _ hm∷ _ hm∷ _ hm∷ _ hm∷ _ hm∷ functor v∷ xs
-  pattern iso-args f xs = _ hm∷ _ hm∷ _ h∷ _ h∷ _ h∷ f v∷ xs
-  pattern nt-args nt xs = _ hm∷ _ hm∷ _ hm∷ _ hm∷ _ hm∷ _ hm∷ _ h∷ _ h∷ nt v∷ xs
+    _ h∷ _ h∷ _ h∷ _ h∷ _ h∷ _ h∷ functor v∷ xs
+  pattern iso-args f xs = _ h∷ _ h∷ _ h∷ _ h∷ _ h∷ f v∷ xs
+  pattern nt-args nt xs = _ h∷ _ h∷ _ h∷ _ h∷ _ h∷ _ h∷ _ h∷ _ h∷ nt v∷ xs
 
   pattern “F₀” functor x =
     def (quote Functor.F₀) (functor-args functor (x v∷ []))
@@ -458,7 +458,7 @@ module Reflection where
   pattern “F₁” functor x y f =
     def (quote Functor.F₁) (functor-args functor (x h∷ y h∷ f v∷ []))
 
-  pattern “,” x y = con (quote _,_) (_ hm∷ _ hm∷ _ h∷ _ h∷ x v∷ y v∷ [])
+  pattern “,” x y = con (quote _,_) (_ h∷ _ h∷ _ h∷ _ h∷ x v∷ y v∷ [])
 
   pattern “id₁” = def (quote Prebicategory.id) _
 
diff --git a/src/Cat/Diagram/Product/Solver.lagda.md b/src/Cat/Diagram/Product/Solver.lagda.md
index bb1caf76c..aa4961f36 100644
--- a/src/Cat/Diagram/Product/Solver.lagda.md
+++ b/src/Cat/Diagram/Product/Solver.lagda.md
@@ -271,25 +271,25 @@ of precategories, as well as objects + morphisms that arise from the product str
 
 The situation here is extremely fiddly when it comes to implicit arguments, as
 we not only need to get the number correct, but also their multiplicity. Record
-projections always mark the records parameters as `hidden`{.Agda} and
-`quantity-0`{.Agda}, so we need to take care to do the same in these patterns.
+projections always mark the records parameters as `hidden`{.Agda}, so we
+need to take care to do the same in these patterns.
 
 ```agda
 module Reflection where
   private
     pattern is-product-field X Y args =
-      _ hm∷ _ hm∷ _ hm∷ -- category args
-      X hm∷ Y hm∷       -- objects of product
-      _ hm∷             -- apex
-      _ hm∷ _ hm∷       -- projections
-      _ v∷              -- is-product record argument
+      _ h∷ _ h∷ _ h∷ -- category args
+      X h∷ Y h∷      -- objects of product
+      _ h∷           -- apex
+      _ h∷ _ h∷      -- projections
+      _ v∷           -- is-product record argument
       args
     pattern product-field X Y args =
-      _ hm∷ _ hm∷ _ hm∷ -- category args
-      X hm∷ Y hm∷       -- objects of product
-      _ v∷              -- product record argument
+      _ h∷ _ h∷ _ h∷ -- category args
+      X h∷ Y h∷      -- objects of product
+      _ v∷           -- product record argument
       args
-    pattern category-field args = _ hm∷ _ hm∷ _ v∷ args
+    pattern category-field args = _ h∷ _ h∷ _ v∷ args
 
     pattern “⊗” X Y =
       def (quote Product.apex) (product-field X Y [])
diff --git a/src/Cat/Displayed/Solver.agda b/src/Cat/Displayed/Solver.agda
index d9094fc27..f5e886773 100644
--- a/src/Cat/Displayed/Solver.agda
+++ b/src/Cat/Displayed/Solver.agda
@@ -138,10 +138,10 @@ module Reflection where
   module Cat = Cat.Solver.Reflection
 
   pattern displayed-field-args xs =
-    _ hm∷ _ hm∷ -- Base Levels
-    _ hm∷       -- Base Category
-    _ hm∷ _ hm∷ -- Displayed Levels
-    _ v∷ xs     -- Displayed Category
+    _ h∷ _ h∷ -- Base Levels
+    _ h∷      -- Base Category
+    _ h∷ _ h∷ -- Displayed Levels
+    _ v∷ xs   -- Displayed Category
 
   pattern displayed-fn-args xs =
     _ h∷ _ h∷ _ h∷ _ h∷ _ h∷ _ v∷ xs
diff --git a/src/Cat/Functor/Solver.agda b/src/Cat/Functor/Solver.agda
index 9f0700afb..3e34c6fa9 100644
--- a/src/Cat/Functor/Solver.agda
+++ b/src/Cat/Functor/Solver.agda
@@ -139,10 +139,10 @@ module NbE {o h o' h'} {𝒞 : Precategory o h} {𝒟 : Precategory o' h'} (F :
 
 module Reflection where
 
-  pattern category-args xs = _ hm∷ _ hm∷ _ v∷ xs
+  pattern category-args xs = _ h∷ _ h∷ _ v∷ xs
 
   pattern functor-args functor xs =
-    _ hm∷ _ hm∷ _ hm∷ _ hm∷ _ hm∷ _ hm∷ functor v∷ xs
+    _ h∷ _ h∷ _ h∷ _ h∷ _ h∷ _ h∷ functor v∷ xs
 
   pattern “id” =
     def (quote Precategory.id) (category-args (_ h∷ []))
diff --git a/src/Cat/Solver.lagda.md b/src/Cat/Solver.lagda.md
index 144e5df55..1978b2de2 100644
--- a/src/Cat/Solver.lagda.md
+++ b/src/Cat/Solver.lagda.md
@@ -129,7 +129,7 @@ hom-sets, then they represent the same morphism.
 module Reflection where
 
   pattern category-args xs =
-    _ hm∷ _ hm∷ _ v∷ xs
+    _ h∷ _ h∷ _ v∷ xs
 
   pattern “id” =
     def (quote Precategory.id) (category-args (_ h∷ []))
diff --git a/src/Data/Nat/DivMod.lagda.md b/src/Data/Nat/DivMod.lagda.md
index a6c47c8e6..3837ab6d6 100644
--- a/src/Data/Nat/DivMod.lagda.md
+++ b/src/Data/Nat/DivMod.lagda.md
@@ -94,12 +94,12 @@ and) of some arithmetic. See for yourself:
 ```agda
   divide-pos (suc a) (suc b') | divmod q' r' p s | inr (inr r'+1=b) =
     divmod (suc q') 0
-      (forget $ᵢ
+      (forget (
         suc a                           ≡⟨ ap suc (recover p) ⟩
         suc (q' * (suc b') + r')        ≡˘⟨ ap (λ e → suc (q' * e + r')) r'+1=b ⟩
         suc (q' * (suc r') + r')        ≡⟨ nat! ⟩
         suc (r' + q' * (suc r') + zero) ≡⟨ ap (λ e → e + q' * e + 0) r'+1=b ⟩
-        (suc b') + q' * (suc b') + 0    ∎ )
+        (suc b') + q' * (suc b') + 0    ∎ ))
       (s≤s 0≤x)
 ```
 
diff --git a/src/Data/Reflection/Argument.agda b/src/Data/Reflection/Argument.agda
index 5dacb3b54..f7a6105b8 100644
--- a/src/Data/Reflection/Argument.agda
+++ b/src/Data/Reflection/Argument.agda
@@ -15,28 +15,12 @@ module Data.Reflection.Argument where
 data Visibility : Type where
   visible hidden instance' : Visibility
 
-data Relevance : Type where
-  relevant irrelevant : Relevance
-
-data Quantity : Type where
-  quantity-0 quantity-ω : Quantity
-
-record Modality : Type where
-  constructor modality
-  field
-    r : Relevance
-    q : Quantity
-
-
-pattern default-modality = modality relevant quantity-ω
-
 record ArgInfo : Type where
   constructor arginfo
   field
     arg-vis : Visibility
-    arg-modality : Modality
 
-pattern default-ai = arginfo visible default-modality
+pattern default-ai = arginfo visible
 
 record Arg {a} (A : Type a) : Type a where
   constructor arg
@@ -48,30 +32,20 @@ record Arg {a} (A : Type a) : Type a where
 {-# BUILTIN VISIBLE              visible    #-}
 {-# BUILTIN HIDDEN               hidden     #-}
 {-# BUILTIN INSTANCE             instance'  #-}
-{-# BUILTIN RELEVANCE            Relevance  #-}
-{-# BUILTIN RELEVANT             relevant   #-}
-{-# BUILTIN IRRELEVANT           irrelevant #-}
-{-# BUILTIN QUANTITY             Quantity   #-}
-{-# BUILTIN QUANTITY-0           quantity-0 #-}
-{-# BUILTIN QUANTITY-ω           quantity-ω #-}
-{-# BUILTIN MODALITY             Modality   #-}
-{-# BUILTIN MODALITY-CONSTRUCTOR modality   #-}
 {-# BUILTIN ARGINFO              ArgInfo    #-}
 {-# BUILTIN ARGARGINFO           arginfo    #-}
 {-# BUILTIN ARG                  Arg        #-}
 {-# BUILTIN ARGARG               arg        #-}
 
-pattern _v∷_ t xs = arg (arginfo visible (modality relevant quantity-ω)) t ∷ xs
-pattern _h∷_ t xs = arg (arginfo hidden (modality relevant quantity-ω)) t ∷ xs
-pattern _i∷_ t xs = arg (arginfo instance' (modality relevant quantity-ω)) t ∷ xs
-pattern _hm∷_ t xs = arg (arginfo hidden (modality relevant _)) t ∷ xs
-infixr 20 _v∷_ _h∷_ _i∷_ _hm∷_
+pattern _v∷_ t xs = arg (arginfo visible) t ∷ xs
+pattern _h∷_ t xs = arg (arginfo hidden) t ∷ xs
+pattern _i∷_ t xs = arg (arginfo instance') t ∷ xs
+infixr 20 _v∷_ _h∷_ _i∷_
 
-argH0 argI argH argN : ∀ {ℓ} {A : Type ℓ} → A → Arg A
-argH  = arg (arginfo hidden (modality relevant quantity-ω))
-argH0 = arg (arginfo hidden (modality relevant quantity-0))
-argI  = arg (arginfo instance' (modality relevant quantity-ω))
-argN  = arg (arginfo visible (modality relevant quantity-ω))
+argI argH argN : ∀ {ℓ} {A : Type ℓ} → A → Arg A
+argH  = arg (arginfo hidden)
+argI  = arg (arginfo instance')
+argN  = arg (arginfo visible)
 
 instance
   Discrete-Visibility : Discrete Visibility
@@ -88,32 +62,8 @@ instance
     instance' hidden    → no (λ ())
     instance' instance' → yes reflᵢ
 
-  Discrete-Relevance : Discrete Relevance
-  Discrete-Relevance = Discreteᵢ→discrete λ where
-    relevant relevant   → yes reflᵢ
-    relevant irrelevant → no (λ ())
-
-    irrelevant relevant   → no (λ ())
-    irrelevant irrelevant → yes reflᵢ
-
-  Discrete-Quantity : Discrete Quantity
-  Discrete-Quantity = Discreteᵢ→discrete λ where
-    quantity-0 quantity-0 → yes reflᵢ
-    quantity-0 quantity-ω → no (λ ())
-    quantity-ω quantity-0 → no (λ ())
-    quantity-ω quantity-ω → yes reflᵢ
-
-  Discrete-Modality : Discrete Modality
-  Discrete-Modality = Discrete-inj
-    (λ (modality r q) → r , q)
-    (λ p → ap₂ modality (ap fst p) (ap snd p))
-    auto
-
   Discrete-ArgInfo : Discrete ArgInfo
-  Discrete-ArgInfo = Discrete-inj
-    (λ (arginfo r q) → r , q)
-    (λ p → ap₂ arginfo (ap fst p) (ap snd p))
-    auto
+  Discrete-ArgInfo = Discrete-inj (λ (arginfo r) → r) (λ p → ap arginfo p) auto
 
   Discrete-Arg : ∀ {ℓ} {A : Type ℓ} ⦃ _ : Discrete A ⦄ → Discrete (Arg A)
   Discrete-Arg = Discrete-inj
@@ -134,10 +84,10 @@ open Has-visibility ⦃ ... ⦄ public
 
 instance
   Has-visibility-ArgInfo : Has-visibility ArgInfo
-  Has-visibility-ArgInfo .set-visibility v (arginfo _ m) = arginfo v m
+  Has-visibility-ArgInfo .set-visibility v (arginfo _) = arginfo v
 
   Has-visibility-Arg : ∀ {ℓ} {A : Type ℓ} → Has-visibility (Arg A)
-  Has-visibility-Arg .set-visibility v (arg (arginfo _ m) x) = arg (arginfo v m) x
+  Has-visibility-Arg .set-visibility v (arg (arginfo _) x) = arg (arginfo v) x
 
   Has-visibility-Args : ∀ {ℓ} {A : Type ℓ} → Has-visibility (List (Arg A))
   Has-visibility-Args .set-visibility v l = set-visibility v <$> l
diff --git a/src/Data/Reflection/Term.agda b/src/Data/Reflection/Term.agda
index 68f69a4db..1a31eb38a 100644
--- a/src/Data/Reflection/Term.agda
+++ b/src/Data/Reflection/Term.agda
@@ -84,7 +84,7 @@ data Definition : Type where
   function    : (cs : List Clause) → Definition
   data-type   : (pars : Nat) (cs : List Name) → Definition
   record-type : (c : Name) (fs : List (Arg Name)) → Definition
-  data-cons   : (d : Name) (q : Quantity) → Definition
+  data-cons   : (d : Name) → Definition
   axiom       : Definition
   prim-fun    : Definition
 
@@ -361,7 +361,7 @@ pi-view (pi a (abs n b)) with pi-view b
 pi-view t = [] , t
 
 pi-impl-view : Term → Telescope × Term
-pi-impl-view t@(pi (arg (arginfo visible _) _) _) = [] , t
+pi-impl-view t@(pi (arg (arginfo visible) _) _) = [] , t
 pi-impl-view (pi a (abs n b)) with pi-impl-view b
 ... | tele , t = ((n , a) ∷ tele) , t
 pi-impl-view t = [] , t
@@ -371,8 +371,8 @@ unpi-view []            k = k
 unpi-view ((n , a) ∷ t) k = pi a (abs n (unpi-view t k))
 
 tel→lam : Telescope → Term → Term
-tel→lam []                               t = t
-tel→lam ((n , arg (arginfo v _) _) ∷ ts) t = lam v (abs n (tel→lam ts t))
+tel→lam []                             t = t
+tel→lam ((n , arg (arginfo v) _) ∷ ts) t = lam v (abs n (tel→lam ts t))
 
 {-
 Turn a telescope into a list of arguments, with arguments of implicit Π types
@@ -418,15 +418,15 @@ module _ {ℓ} {A : Type ℓ} ⦃ a : Has-neutrals A ⦄ (d : A) ⦃ _ : Has-neu
   _##_ : (arg : Arg A) → A
   _##_ x = Has-neutrals.applyⁿᵉ a d (x ∷ [])
 
--- Apply a neutral to an argument with the default information.
+-- Apply a neutral to a visible argument.
   _##ₙ_ : (arg : A) → A
   _##ₙ_ x = _##_ (argN x)
 
-  -- Apply a neutral to a hidden argument with the default modality.
+  -- Apply a neutral to a hidden argument.
   _##ₕ_ : (arg : A) → A
   _##ₕ_ x = _##_ (argH x)
 
-  -- Apply a neutral to an instance argument with the default modality.
+  -- Apply a neutral to an instance argument.
   _##ᵢ_ : (arg : A) → A
   _##ᵢ_ x = _##_ (argI x)
 
diff --git a/src/Homotopy/Space/Delooping.lagda.md b/src/Homotopy/Space/Delooping.lagda.md
index f9d44c65b..ee0a17ae1 100644
--- a/src/Homotopy/Space/Delooping.lagda.md
+++ b/src/Homotopy/Space/Delooping.lagda.md
@@ -356,7 +356,7 @@ of a loop with arbitrary base.
     interleaved mutual
       go   : (x : Deloop G) → x ≡ x → ⌞ G ⌟
 
-      coherence : Type _ [ i1 ↦ (λ ._ → (x : ⌞ G ⌟) → PathP (λ i → path {G = G} x i ≡ path x i → ⌞ G ⌟) (encode G base) (encode G base)) ]
+      coherence : Type _ [ i1 ↦ (λ _ → (x : ⌞ G ⌟) → PathP (λ i → path {G = G} x i ≡ path x i → ⌞ G ⌟) (encode G base) (encode G base)) ]
       coh : outS coherence
 ```
 -->
diff --git a/src/Prim/Extension.lagda.md b/src/Prim/Extension.lagda.md
index 3e1de7937..f06b8b14c 100644
--- a/src/Prim/Extension.lagda.md
+++ b/src/Prim/Extension.lagda.md
@@ -63,8 +63,8 @@ on the intersection `i ∧ j`.
 partial-pushout
   : ∀ {ℓ} (i j : I) {A : Partial (i ∨ j) (Type ℓ)}
     {ai : PartialP {a = ℓ} (i ∧ j) (λ { (j ∧ i = i1) → A 1=1 }) }
-  → (.(z : IsOne i) → A (leftIs1 i j z)  [ (i ∧ j) ↦ (λ { (i ∧ j = i1) → ai 1=1 }) ])
-  → (.(z : IsOne j) → A (rightIs1 i j z) [ (i ∧ j) ↦ (λ { (i ∧ j = i1) → ai 1=1 }) ])
+  → ((z : IsOne i) → A (leftIs1 i j z)  [ (i ∧ j) ↦ (λ { (i ∧ j = i1) → ai 1=1 }) ])
+  → ((z : IsOne j) → A (rightIs1 i j z) [ (i ∧ j) ↦ (λ { (i ∧ j = i1) → ai 1=1 }) ])
   → PartialP (i ∨ j) A
 partial-pushout i j u v = primPOr i j (λ z → outS (u z)) (λ z → outS (v z))
 ```
diff --git a/src/Prim/Interval.lagda.md b/src/Prim/Interval.lagda.md
index c85889077..fb52ffd2e 100644
--- a/src/Prim/Interval.lagda.md
+++ b/src/Prim/Interval.lagda.md
@@ -65,7 +65,8 @@ judgemental equality][sr].
 [sr]: https://github.com/agda/agda/issues/6016
 
 ```agda
-{-# BUILTIN ISONE IsOne #-}  -- IsOne : I → SSet
+{-# BUILTIN COFUNIV CofUniv #-} -- universe of cofibrations
+{-# BUILTIN ISONE   IsOne #-}   -- IsOne : I → CofUniv
 
 postulate
   1=1 : IsOne i1
diff --git a/support/nix/dep/nix-thunk/default.nix b/support/nix/dep/nix-thunk/default.nix
deleted file mode 100644
index 2b4d4ab11..000000000
--- a/support/nix/dep/nix-thunk/default.nix
+++ /dev/null
@@ -1,2 +0,0 @@
-# DO NOT HAND-EDIT THIS FILE
-import (import ./thunk.nix)
\ No newline at end of file
diff --git a/support/nix/dep/nix-thunk/github.json b/support/nix/dep/nix-thunk/github.json
deleted file mode 100644
index e14d21cd7..000000000
--- a/support/nix/dep/nix-thunk/github.json
+++ /dev/null
@@ -1,8 +0,0 @@
-{
-  "owner": "obsidiansystems",
-  "repo": "nix-thunk",
-  "branch": "master",
-  "private": false,
-  "rev": "bd0de53129ca4ac5ce313a3e021edf3638a3a22c",
-  "sha256": "0cn74ylcfr9v2w94jpga9v18jn6zafb9k996afszn59iqlcfi74q"
-}
diff --git a/support/nix/dep/nix-thunk/thunk.nix b/support/nix/dep/nix-thunk/thunk.nix
deleted file mode 100644
index 20f2d28c2..000000000
--- a/support/nix/dep/nix-thunk/thunk.nix
+++ /dev/null
@@ -1,12 +0,0 @@
-# DO NOT HAND-EDIT THIS FILE
-let fetch = { private ? false, fetchSubmodules ? false, owner, repo, rev, sha256, ... }:
-  if !fetchSubmodules && !private then builtins.fetchTarball {
-    url = "https://github.com/${owner}/${repo}/archive/${rev}.tar.gz"; inherit sha256;
-  } else (import (builtins.fetchTarball {
-  url = "https://github.com/NixOS/nixpkgs/archive/3aad50c30c826430b0270fcf8264c8c41b005403.tar.gz";
-  sha256 = "0xwqsf08sywd23x0xvw4c4ghq0l28w2ki22h0bdn766i16z9q2gr";
-}) {}).fetchFromGitHub {
-    inherit owner repo rev sha256 fetchSubmodules private;
-  };
-  json = builtins.fromJSON (builtins.readFile ./github.json);
-in fetch json
\ No newline at end of file
diff --git a/support/nix/haskell-packages.nix b/support/nix/haskell-packages.nix
index b5c07066b..c613460ff 100644
--- a/support/nix/haskell-packages.nix
+++ b/support/nix/haskell-packages.nix
@@ -16,8 +16,8 @@ let
 
   src = pkgs.fetchgit {
     url             = "https://codeberg.org/1lab/mikan.git";
-    rev             = "2f4c616229bcd5b9ea926e5001bce5c00a1df2bb";
-    sha256          = "sha256-zCpJM+SpmRlsDxI1wXyNDxhWgEI/2oAXZhjP9G8SMaI=";
+    rev             = "f56118785f5e78eca5592a7601a6f547353b8a06";
+    sha256          = "sha256-Z0SrRjmKj1Xrr7VBsyMjyEF2TCBNRhkolfBRWBrayg4=";
     fetchSubmodules = false;
   };
 

From 7083ec61b25f02a92fad968826226f0c58192549 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Am=C3=A9lia=20Liao?= <me@amelia.how>
Date: Mon, 25 May 2026 13:34:28 -0300
Subject: [PATCH 10/12] [ci skip] fix: remove Word64

---
 src/1Lab/Reflection.lagda.md     |  1 -
 src/Data/Float/Base.lagda.md     |  9 ++++----
 src/Data/Reflection/Literal.agda | 19 -----------------
 src/Data/Reflection/Name.agda    | 23 ++++++++++++--------
 src/Data/Reflection/Term.agda    |  1 -
 src/Data/String/Show.lagda.md    |  4 ----
 src/Data/Word/Base.lagda.md      | 36 --------------------------------
 7 files changed, 18 insertions(+), 75 deletions(-)
 delete mode 100644 src/Data/Word/Base.lagda.md

diff --git a/src/1Lab/Reflection.lagda.md b/src/1Lab/Reflection.lagda.md
index 17ebd3bf6..4609008ea 100644
--- a/src/1Lab/Reflection.lagda.md
+++ b/src/1Lab/Reflection.lagda.md
@@ -22,7 +22,6 @@ open import Data.String.Base public
 open import Meta.Traversable public
 open import Data.Float.Base public
 open import Data.Maybe.Base public
-open import Data.Word.Base public
 open import Meta.Idiom public
 open import Meta.Bind public
 open import Meta.Alt public
diff --git a/src/Data/Float/Base.lagda.md b/src/Data/Float/Base.lagda.md
index 227b65eac..e3f40a110 100644
--- a/src/Data/Float/Base.lagda.md
+++ b/src/Data/Float/Base.lagda.md
@@ -3,7 +3,6 @@
 open import 1Lab.Type
 
 open import Data.Maybe.Base
-open import Data.Word.Base
 open import Data.Dec.Base
 open import Data.Int.Base
 open import Data.Id.Base
@@ -30,8 +29,6 @@ private module P where primitive
   primFloatIsNegativeZero    : Float → Bool
   primFloatIsSafeInteger     : Float → Bool
   -- Conversions
-  primFloatToWord64          : Float → Maybe Word64
-  primFloatToWord64Injective : ∀ a b → primFloatToWord64 a ≡ᵢ primFloatToWord64 b → a ≡ᵢ b
   primNatToFloat             : Nat → Float
   primIntToFloat             : Int → Float
   primFloatRound             : Float → Maybe Int
@@ -75,7 +72,6 @@ open P public renaming
   ; primFloatIsNegativeZero to is-neg0?
   ; primFloatIsSafeInteger  to is-integer?
 
-  ; primFloatToWord64       to float→word64
   ; primNatToFloat          to nat→float
   ; primIntToFloat          to int→float
   ; primFloatRound          to round
@@ -94,9 +90,12 @@ open P public renaming
   )
   using ()
 
+-- TODO: this needs to be a primitive upstream.
+private postulate primFloatToRatioInjective : ∀ a b → float→ratio a ≡ᵢ float→ratio b → a ≡ᵢ b
+
 instance
   Discrete-Float : Discrete Float
-  Discrete-Float  = Discrete-inj' _ (P.primFloatToWord64Injective _ _)
+  Discrete-Float  = Discrete-inj' _ (primFloatToRatioInjective _ _)
 
   Number-Float : Number Float
   Number-Float .Number.Constraint _ = ⊤
diff --git a/src/Data/Reflection/Literal.agda b/src/Data/Reflection/Literal.agda
index 2e7dcadff..a494a3ac7 100644
--- a/src/Data/Reflection/Literal.agda
+++ b/src/Data/Reflection/Literal.agda
@@ -7,7 +7,6 @@ open import Data.Reflection.Name
 open import Data.String.Base
 open import Data.Float.Base
 open import Data.Char.Base
-open import Data.Word.Base
 open import Data.Dec.Base
 open import Data.Nat.Base
 open import Data.Id.Base
@@ -16,7 +15,6 @@ module Data.Reflection.Literal where
 
 data Literal : Type where
   nat    : (n : Nat)    → Literal
-  word64 : (n : Word64) → Literal
   float  : (x : Float)  → Literal
   char   : (c : Char)   → Literal
   string : (s : String) → Literal
@@ -25,7 +23,6 @@ data Literal : Type where
 
 {-# BUILTIN AGDALITERAL   Literal #-}
 {-# BUILTIN AGDALITNAT    nat     #-}
-{-# BUILTIN AGDALITWORD64 word64  #-}
 {-# BUILTIN AGDALITFLOAT  float   #-}
 {-# BUILTIN AGDALITCHAR   char    #-}
 {-# BUILTIN AGDALITSTRING string  #-}
@@ -38,9 +35,6 @@ instance
     (nat n) (nat n₁) → case n ≡ᵢ? n₁ of λ where
       (yes reflᵢ) → yes reflᵢ
       (no ¬p) → no λ { reflᵢ → ¬p reflᵢ }
-    (word64 n) (word64 n₁) → case n ≡ᵢ? n₁ of λ where
-      (yes reflᵢ) → yes reflᵢ
-      (no ¬p) → no λ { reflᵢ → ¬p reflᵢ }
     (float x) (float x₁) → case x ≡ᵢ? x₁ of λ where
       (yes reflᵢ) → yes reflᵢ
       (no ¬p) → no λ { reflᵢ → ¬p reflᵢ }
@@ -57,50 +51,37 @@ instance
       (yes reflᵢ) → yes reflᵢ
       (no ¬p) → no λ { reflᵢ → ¬p reflᵢ }
 
-    (nat n) (word64 n₁) → no (λ ())
     (nat n) (float x)   → no (λ ())
     (nat n) (char c)    → no (λ ())
     (nat n) (string s)  → no (λ ())
     (nat n) (name x)    → no (λ ())
     (nat n) (meta x)    → no (λ ())
 
-    (word64 n) (nat n₁)    → no (λ ())
-    (word64 n) (float x)   → no (λ ())
-    (word64 n) (char c)    → no (λ ())
-    (word64 n) (string s)  → no (λ ())
-    (word64 n) (name x)    → no (λ ())
-    (word64 n) (meta x)    → no (λ ())
-
     (float x) (nat n)    → no (λ ())
-    (float x) (word64 n) → no (λ ())
     (float x) (char c)   → no (λ ())
     (float x) (string s) → no (λ ())
     (float x) (name x₁)  → no (λ ())
     (float x) (meta x₁)  → no (λ ())
 
     (char c) (nat n)    → no (λ ())
-    (char c) (word64 n) → no (λ ())
     (char c) (float x)  → no (λ ())
     (char c) (string s) → no (λ ())
     (char c) (name x)   → no (λ ())
     (char c) (meta x)   → no (λ ())
 
     (string s) (nat n)     → no (λ ())
-    (string s) (word64 n)  → no (λ ())
     (string s) (float x)   → no (λ ())
     (string s) (char c)    → no (λ ())
     (string s) (name x)    → no (λ ())
     (string s) (meta x)    → no (λ ())
 
     (name x) (nat n)    → no (λ ())
-    (name x) (word64 n) → no (λ ())
     (name x) (float x₁) → no (λ ())
     (name x) (char c)   → no (λ ())
     (name x) (string s) → no (λ ())
     (name x) (meta x₁)  → no (λ ())
 
     (meta x) (nat n)    → no (λ ())
-    (meta x) (word64 n) → no (λ ())
     (meta x) (float x₁) → no (λ ())
     (meta x) (char c)   → no (λ ())
     (meta x) (string s) → no (λ ())
diff --git a/src/Data/Reflection/Name.agda b/src/Data/Reflection/Name.agda
index 6d9b80fd9..dfe3dc2ed 100644
--- a/src/Data/Reflection/Name.agda
+++ b/src/Data/Reflection/Name.agda
@@ -5,7 +5,6 @@ open import 1Lab.Type
 open import Data.Reflection.Fixity
 open import Data.String.Base
 open import Data.String.Show
-open import Data.Word.Base
 open import Data.Dec.Base
 open import Data.Id.Base
 
@@ -14,13 +13,15 @@ module Data.Reflection.Name where
 postulate Name : Type
 {-# BUILTIN QNAME Name #-}
 
-private module P where primitive
-  primQNameEquality           : Name → Name → Bool
-  primQNameLess               : Name → Name → Bool
-  primShowQName               : Name → String
-  primQNameToWord64s          : Name → Σ Word64 (λ _ → Word64)
-  primQNameToWord64sInjective : ∀ x y → primQNameToWord64s x ≡ᵢ primQNameToWord64s y → x ≡ᵢ y
-  primQNameFixity             : Name → Fixity
+private module P where
+  primitive
+    primQNameEquality           : Name → Name → Bool
+    primQNameLess               : Name → Name → Bool
+    primShowQName               : Name → String
+    primQNameFixity             : Name → Fixity
+  postulate
+    primQNameEqualityRefl  : ∀ x → primQNameEquality x x ≡ᵢ true
+    primQNameEqualitySound : ∀ x y → primQNameEquality x y ≡ᵢ true → x ≡ᵢ y
 
 open P
   renaming (primQNameFixity to name→fixity)
@@ -29,7 +30,11 @@ open P
 
 instance
   Discrete-Name : Discrete Name
-  Discrete-Name = Discrete-inj' _ (P.primQNameToWord64sInjective _ _)
+  Discrete-Name .decide x y with P.primQNameEquality x y in q
+  ... | true  = yes (Id≃path.to (P.primQNameEqualitySound x y q))
+  ... | false = no λ p → work (Id≃path.from p) q where
+    work : ∀ {x y} → x ≡ᵢ y → P.primQNameEquality x y ≡ᵢ false → ⊥
+    work {x} reflᵢ p rewrite P.primQNameEqualityRefl x with () ← p
 
   Show-Name : Show Name
   Show-Name = default-show P.primShowQName
diff --git a/src/Data/Reflection/Term.agda b/src/Data/Reflection/Term.agda
index 1a31eb38a..9dafe5fc5 100644
--- a/src/Data/Reflection/Term.agda
+++ b/src/Data/Reflection/Term.agda
@@ -10,7 +10,6 @@ open import Data.Reflection.Abs
 open import Data.String.Base
 open import Data.Float.Base
 open import Data.List.Base
-open import Data.Word.Base
 open import Data.Dec.Base
 open import Data.Nat.Base
 open import Data.Id.Base
diff --git a/src/Data/String/Show.lagda.md b/src/Data/String/Show.lagda.md
index 33e47b56a..0c3fe474a 100644
--- a/src/Data/String/Show.lagda.md
+++ b/src/Data/String/Show.lagda.md
@@ -7,7 +7,6 @@ open import Data.String.Base
 open import Data.Float.Base
 open import Data.Char.Base
 open import Data.List.Base
-open import Data.Word.Base
 
 open import Meta.Append
 ```
@@ -62,9 +61,6 @@ private module P where primitive
   primShowFloat      : Float  → String
 
 instance
-  Show-Word64 : Show Word64
-  Show-Word64 = default-show λ x → P.primShowNat (word64→nat x)
-
   Show-Nat : Show Nat
   Show-Nat = default-show P.primShowNat
 
diff --git a/src/Data/Word/Base.lagda.md b/src/Data/Word/Base.lagda.md
deleted file mode 100644
index 2b64ec145..000000000
--- a/src/Data/Word/Base.lagda.md
+++ /dev/null
@@ -1,36 +0,0 @@
-<!--
-```agda
-open import 1Lab.Type
-
-open import Data.Dec.Base
-open import Data.Nat.Base
-open import Data.Id.Base
-```
--->
-
-```agda
-module Data.Word.Base where
-```
-
-# Machine words
-
-```agda
-postulate Word64 : Type
-
-{-# BUILTIN WORD64 Word64 #-}
-
-private module P where primitive
-  primWord64ToNat          : Word64 → Nat
-  primWord64FromNat        : Nat → Word64
-  primWord64ToNatInjective : ∀ a b → primWord64ToNat a ≡ᵢ primWord64ToNat b → a ≡ᵢ b
-
-open P public renaming
-  ( primWord64FromNat to nat→word64
-  ; primWord64ToNat   to word64→nat
-  )
-  using ()
-
-instance
-  Discrete-Word64 : Discrete Word64
-  Discrete-Word64 = Discrete-inj' _ (P.primWord64ToNatInjective _ _)
-```

From 7a9e51fa7ddf2e8dae07dc63438b570f74f1b35f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Na=C3=AFm=20Camille=20Favier?= <n@monade.li>
Date: Wed, 20 May 2026 14:14:21 +0200
Subject: [PATCH 11/12] =?UTF-8?q?chore:=20`Set`=20=E2=86=92=20`Type`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/1Lab/Reflection/Induction.agda           |  2 +-
 src/1Lab/Reflection/Marker.agda              |  2 +-
 src/1Lab/Reflection/Subst.agda               |  2 +-
 src/Algebra/Ring/Module/Multilinear.lagda.md |  2 +-
 src/Data/Fin/Product.lagda.md                |  2 +-
 src/Data/Reflection/Term.agda                | 26 ++++++++++----------
 src/Prim/Type.lagda.md                       |  4 +--
 7 files changed, 20 insertions(+), 20 deletions(-)

diff --git a/src/1Lab/Reflection/Induction.agda b/src/1Lab/Reflection/Induction.agda
index 39cb22278..cd0e93ea9 100644
--- a/src/1Lab/Reflection/Induction.agda
+++ b/src/1Lab/Reflection/Induction.agda
@@ -259,7 +259,7 @@ make-elim-with opts elim D = withNormalisation true do
     argP = if hide-motive then argH else argN
     motiveTel = ("ℓ" , argH (quoteTerm Level))
               -- P : DTel → Type ℓ
-              ∷ ("P" , argP (unpi-view (PTel DTel) (agda-sort (set (var (length (PTel DTel)) [])))))
+              ∷ ("P" , argP (unpi-view (PTel DTel) (agda-sort (type (var (length (PTel DTel)) [])))))
               ∷ []
     DTel = raise 1 DTel
     -- We want to take is-hlevel as an argument, but we need to work in a context
diff --git a/src/1Lab/Reflection/Marker.agda b/src/1Lab/Reflection/Marker.agda
index 6cc18f9a8..59b668243 100644
--- a/src/1Lab/Reflection/Marker.agda
+++ b/src/1Lab/Reflection/Marker.agda
@@ -50,7 +50,7 @@ abstract-marker = go 0 where
     a ← go k a
     pure (pi (arg i a) (abs x t))
   go k (agda-sort s) with s
-  ... | set t = agda-sort ∘ set <$> go k t
+  ... | type t = agda-sort ∘ type <$> go k t
   ... | lit n = pure (agda-sort (lit n))
   ... | prop t = agda-sort ∘ prop <$> go k t
   ... | propLit n = pure (agda-sort (propLit n))
diff --git a/src/1Lab/Reflection/Subst.agda b/src/1Lab/Reflection/Subst.agda
index 0d3c18c83..13492e077 100644
--- a/src/1Lab/Reflection/Subst.agda
+++ b/src/1Lab/Reflection/Subst.agda
@@ -135,7 +135,7 @@ subst-tm ρ (pi (arg ι a) (abs n b)) = pi (arg ι (subst-tm ρ a)) (abs n (subs
 subst-tm ρ (lit l) = (lit l)
 subst-tm ρ unknown = unknown
 subst-tm ρ (agda-sort s) with s
-… | set t     = agda-sort (set (subst-tm ρ t))
+… | type t    = agda-sort (type (subst-tm ρ t))
 … | lit n     = agda-sort (lit n)
 … | prop t    = agda-sort (prop (subst-tm ρ t))
 … | propLit n = agda-sort (propLit n)
diff --git a/src/Algebra/Ring/Module/Multilinear.lagda.md b/src/Algebra/Ring/Module/Multilinear.lagda.md
index 9584f42ed..16f1888b1 100644
--- a/src/Algebra/Ring/Module/Multilinear.lagda.md
+++ b/src/Algebra/Ring/Module/Multilinear.lagda.md
@@ -136,7 +136,7 @@ to denote `updateₚ α i x` that fits well in the mathematical prose.
 -- XXX: Since we're already squishing down a type whose universe level
 -- Agda dislikes, one might wonder if we have to use the finitary
 -- products in the type of `pres-+ₚ`. The answer is yes, since
--- otherwise `linearᶠ` lives in Setω, which the declare-record-iso
+-- otherwise `linearᶠ` lives in Typeω, which the declare-record-iso
 -- tactic is very unhappy about.
 
 open Multilinear-map
diff --git a/src/Data/Fin/Product.lagda.md b/src/Data/Fin/Product.lagda.md
index f833e59f9..3d90cc1aa 100644
--- a/src/Data/Fin/Product.lagda.md
+++ b/src/Data/Fin/Product.lagda.md
@@ -20,7 +20,7 @@ with strictly curried (non-dependent) functions whose domain is a finite
 product. The construction is maximally universe-polymorphic, in that it
 supports sequences whose universe level varies between components, and
 is valued in their finite supremum, giving universes for products more
-precise than `Setω`{.Agda}.
+precise than `Typeω`{.Agda}.
 
 <!--
 ```agda
diff --git a/src/Data/Reflection/Term.agda b/src/Data/Reflection/Term.agda
index 9dafe5fc5..68ed19b92 100644
--- a/src/Data/Reflection/Term.agda
+++ b/src/Data/Reflection/Term.agda
@@ -37,7 +37,7 @@ data Term where
   unknown   : Term
 
 data Sort where
-  set     : (t : Term) → Sort
+  type    : (t : Term) → Sort
   lit     : (n : Nat) → Sort
   prop    : (t : Term) → Sort
   propLit : (n : Nat) → Sort
@@ -72,7 +72,7 @@ data Clause where
 {-# BUILTIN AGDATERMLIT         lit       #-}
 {-# BUILTIN AGDATERMUNSUPPORTED unknown   #-}
 
-{-# BUILTIN AGDASORTSET         set     #-}
+{-# BUILTIN AGDASORTTYPE        type    #-}
 {-# BUILTIN AGDASORTLIT         lit     #-}
 {-# BUILTIN AGDASORTPROP        prop    #-}
 {-# BUILTIN AGDASORTPROPLIT     propLit #-}
@@ -241,7 +241,7 @@ instance
     unknown unknown → yes reflᵢ
 
   Discrete-Sort = Discreteᵢ→discrete λ where
-    (set t) (set t₁)         → case t ≡ᵢ? t₁ of λ where
+    (type t) (type t₁)       → case t ≡ᵢ? t₁ of λ where
       (yes reflᵢ) → yes reflᵢ
       (no ¬a) → no λ { reflᵢ → ¬a reflᵢ }
     (lit n) (lit n₁)         → case n ≡ᵢ? n₁ of λ where
@@ -258,32 +258,32 @@ instance
       (no ¬a) → no λ { reflᵢ → ¬a reflᵢ }
     unknown unknown          → yes reflᵢ
 
-    (set t) (lit n) → no (λ ())
-    (set t) (prop t₁) → no (λ ())
-    (set t) (propLit n) → no (λ ())
-    (set t) (inf n) → no (λ ())
-    (set t) unknown → no (λ ())
-    (lit n) (set t) → no (λ ())
+    (type t) (lit n) → no (λ ())
+    (type t) (prop t₁) → no (λ ())
+    (type t) (propLit n) → no (λ ())
+    (type t) (inf n) → no (λ ())
+    (type t) unknown → no (λ ())
+    (lit n) (type t) → no (λ ())
     (lit n) (prop t) → no (λ ())
     (lit n) (propLit n₁) → no (λ ())
     (lit n) (inf n₁) → no (λ ())
     (lit n) unknown → no (λ ())
-    (prop t) (set t₁) → no (λ ())
+    (prop t) (type t₁) → no (λ ())
     (prop t) (lit n) → no (λ ())
     (prop t) (propLit n) → no (λ ())
     (prop t) (inf n) → no (λ ())
     (prop t) unknown → no (λ ())
-    (propLit n) (set t) → no (λ ())
+    (propLit n) (type t) → no (λ ())
     (propLit n) (lit n₁) → no (λ ())
     (propLit n) (prop t) → no (λ ())
     (propLit n) (inf n₁) → no (λ ())
     (propLit n) unknown → no (λ ())
-    (inf n) (set t) → no (λ ())
+    (inf n) (type t) → no (λ ())
     (inf n) (lit n₁) → no (λ ())
     (inf n) (prop t) → no (λ ())
     (inf n) (propLit n₁) → no (λ ())
     (inf n) unknown → no (λ ())
-    unknown (set t) → no (λ ())
+    unknown (type t) → no (λ ())
     unknown (lit n) → no (λ ())
     unknown (prop t) → no (λ ())
     unknown (propLit n) → no (λ ())
diff --git a/src/Prim/Type.lagda.md b/src/Prim/Type.lagda.md
index 81511d4e4..baa036e2f 100644
--- a/src/Prim/Type.lagda.md
+++ b/src/Prim/Type.lagda.md
@@ -10,8 +10,8 @@ system. For more details about the use of universes, see
 [`1Lab.Type`](1Lab.Type.html).
 
 ```agda
-{-# BUILTIN TYPE     Type  #-}
-{-# BUILTIN SETOMEGA Typeω #-}
+{-# BUILTIN TYPE      Type  #-}
+{-# BUILTIN TYPEOMEGA Typeω #-}
 
 {-# BUILTIN PROP      SProp  #-}
 {-# BUILTIN PROPOMEGA SPropω #-}

From aa022fda4df66b2fd32d63aad9b0c6b495573508 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Am=C3=A9lia=20Liao?= <me@amelia.how>
Date: Wed, 27 May 2026 14:03:01 -0300
Subject: [PATCH 12/12] chore: bump

---
 support/nix/haskell-packages.nix       | 4 ++--
 support/shake/app/Shake/AgdaCompile.hs | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/support/nix/haskell-packages.nix b/support/nix/haskell-packages.nix
index c613460ff..5d492e227 100644
--- a/support/nix/haskell-packages.nix
+++ b/support/nix/haskell-packages.nix
@@ -16,8 +16,8 @@ let
 
   src = pkgs.fetchgit {
     url             = "https://codeberg.org/1lab/mikan.git";
-    rev             = "f56118785f5e78eca5592a7601a6f547353b8a06";
-    sha256          = "sha256-Z0SrRjmKj1Xrr7VBsyMjyEF2TCBNRhkolfBRWBrayg4=";
+    rev             = "5fd3212d213bcd23c6c00c13bf487f253d63b48d";
+    sha256          = "sha256-q7OQkk+divJIoBWFiuE+3fkKrWzapIG7B2C2HRjNfHg=";
     fetchSubmodules = false;
   };
 
diff --git a/support/shake/app/Shake/AgdaCompile.hs b/support/shake/app/Shake/AgdaCompile.hs
index 2c16cd02f..481db374b 100644
--- a/support/shake/app/Shake/AgdaCompile.hs
+++ b/support/shake/app/Shake/AgdaCompile.hs
@@ -201,7 +201,7 @@ compileAgda stateVar = do
         source <- parseSource =<< srcFromPath absPath
         typeCheckMain TypeCheck source
 
-      modifyTCLens stVisitedModules (`Map.union` oldVisited)
+      modifyingTC stVisitedModules (`Map.union` oldVisited)
 
     writeIORef stateVar (Just state)