diff --git a/src/1Lab/Type.lagda.md b/src/1Lab/Type.lagda.md
index 7e564842e..2564a2aa7 100644
--- a/src/1Lab/Type.lagda.md
+++ b/src/1Lab/Type.lagda.md
@@ -138,5 +138,8 @@ instance
   Number-Lift : ∀ {ℓ ℓ'} {A : Type ℓ} → ⦃ Number A ⦄ → Number (Lift ℓ' A)
   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ω ()
 ```
 -->
diff --git a/src/Cat/Instances/Simplex.lagda.md b/src/Cat/Instances/Simplex.lagda.md
index 7456e99bf..47badd23c 100644
--- a/src/Cat/Instances/Simplex.lagda.md
+++ b/src/Cat/Instances/Simplex.lagda.md
@@ -46,7 +46,7 @@ unquoteDecl H-Level-Δ-map = declare-record-hlevel 2 H-Level-Δ-map (quote Δ-ma
   → f ≡ g
 Δ-map-path p i .map x = p x i
 Δ-map-path {f = f} {g} p i .ascending x y w =
-  is-prop→pathp (λ j → Nat.≤-is-prop {to-nat (p x j)} {to-nat (p y j)})
+  is-prop→pathp (λ j → Nat.≤-is-prop {p x j .lower} {p y j .lower})
     (f .ascending x y w) (g .ascending x y w) i
 ```
 -->
diff --git a/src/Data/Fin/Base.lagda.md b/src/Data/Fin/Base.lagda.md
index bbbb82daf..27225e65a 100644
--- a/src/Data/Fin/Base.lagda.md
+++ b/src/Data/Fin/Base.lagda.md
@@ -42,17 +42,29 @@ would like to enforce that constructions on $\operatorname{Fin}(n)$
 wrapped it in `Irr`{.Agda}.
 
 In dependent type theory, it's common to instead define the finite sets
-as a family indexed over `Nat`{.Agda}. However, we prefer the definition
-above because it lets us `cast`{.Agda} elements of
-$\operatorname{Fin}(n)$ along a path $n = m$ in a way that
-definitionally preserves the underlying number:
+as an inductive family indexed over `Nat`{.Agda}. However, in cubical
+type theory, there is a good reason to avoid inductive families: they
+have `subst`{.Agda} as an additional constructor, *including* along
+constant paths. This makes the normal form of any expression involving
+substitution in an indexed family, even if the thing being transported
+is a constructor form, very bad.
+
+Instead, we would like the `subst`{.Agda} operation on `Fin`{.Agda} to
+definitionally commute with the constructors, and (if possible) to
+definitionally preserve the underlying numeric value. Defining
+`Fin`{.Agda} as an indexed type with an irrelevant proof field achieves
+exactly this:
 
 ```agda
-cast : ∀ {m n} → m ≡ n → Fin m → Fin n
-cast p (fin n ⦃ i ⦄) = record
-  { lower   = n
-  ; bounded = subst (n Nat.<_) p <$> i
-  }
+private
+  cast : ∀ {m n} → m ≡ n → Fin m → Fin n
+  cast p (fin n ⦃ i ⦄) = record
+    { lower   = n
+    ; bounded = subst (n Nat.<_) p <$> i
+    }
+
+  _ : ∀ {m n} {p : m ≡ n} {x : Fin m} → subst Fin p x ≡ cast p x
+  _ = refl
 ```
 
 <!--
@@ -141,15 +153,6 @@ Fin-elim P pfzero pfsuc i with fin-view i
 ```agda
 fin-ap : ∀ {n} {x y : Fin n} → x .lower ≡ y .lower → x ≡ y
 fin-ap p = ap₂ (λ x y → fin x ⦃ y ⦄) p (to-pathp refl)
-
-cast-uncast : ∀ {m n} → (p : m ≡ n) → ∀ x → cast (sym p) (cast p x) ≡ x
-cast-uncast p x = refl
-
-cast-is-equiv : ∀ {m n} (p : m ≡ n) → is-equiv (cast p)
-cast-is-equiv p = is-iso→is-equiv $ iso
-  (cast (sym p))
-  (cast-uncast (sym p))
-  (cast-uncast p)
 ```
 -->
 
diff --git a/src/Data/Fin/Closure.lagda.md b/src/Data/Fin/Closure.lagda.md
index b12d66962..7eca9cf9b 100644
--- a/src/Data/Fin/Closure.lagda.md
+++ b/src/Data/Fin/Closure.lagda.md
@@ -116,7 +116,7 @@ binary products:
 Finite-multiply : (Fin n × Fin m) ≃ Fin (n * m)
 Finite-multiply {n} {m} =
   (Fin n × Fin m)       ≃⟨ Finite-sum (λ _ → m) ⟩
-  Fin (sum n (λ _ → m)) ≃⟨ cast (sum≡* n m) , cast-is-equiv (sum≡* n m) ⟩
+  Fin (sum n (λ _ → m)) ≃⟨ path→equiv (ap Fin (sum≡* n m)) ⟩
   Fin (n * m)           ≃∎
   where
     sum≡* : ∀ n m → sum n (λ _ → m) ≡ n * m
diff --git a/src/Data/Fin/Finite.lagda.md b/src/Data/Fin/Finite.lagda.md
index b00b62a5c..c85e1b9fa 100644
--- a/src/Data/Fin/Finite.lagda.md
+++ b/src/Data/Fin/Finite.lagda.md
@@ -160,7 +160,7 @@ same-cardinality→equiv
 same-cardinality→equiv ⦃ fa ⦄ ⦃ fb ⦄ p = do
   ea ← fa .Finite.enumeration
   eb ← fb .Finite.enumeration
-  pure (ea ∙e (_ , cast-is-equiv p) ∙e eb e⁻¹)
+  pure (ea ∙e path→equiv (ap Fin p) ∙e eb e⁻¹)
 
 module _ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} ⦃ fb : Finite B ⦄
   (e : ∥ A ≃ B ∥) (f : A → B) where
diff --git a/src/Data/List/Membership.lagda.md b/src/Data/List/Membership.lagda.md
index 38091b692..ab910e5e8 100644
--- a/src/Data/List/Membership.lagda.md
+++ b/src/Data/List/Membership.lagda.md
@@ -184,13 +184,13 @@ member→member-nub {xs = x ∷ xs} (there α) with elem? x (nub xs)
 
 <!--
 ```agda
-!-tabulate : ∀ {n} (f : Fin n → A) i → tabulate f ! i ≡ f (cast (length-tabulate f) i)
+!-tabulate : ∀ {n} (f : Fin n → A) i → tabulate f ! i ≡ f (subst Fin (length-tabulate f) i)
 !-tabulate _ ix with fin-view ix
 !-tabulate {n = suc n} f _ | zero  = refl
 !-tabulate {n = suc n} f _ | suc i = !-tabulate (f ∘ fsuc) i
 
 !-tabulate-fibre : ∀ {n} (f : Fin n → A) x → fibre (tabulate f !_) x ≃ fibre f x
-!-tabulate-fibre f x = Σ-ap (cast (length-tabulate f) , cast-is-equiv (length-tabulate f)) λ i →
+!-tabulate-fibre f x = Σ-ap (path→equiv (ap Fin (length-tabulate f))) λ i →
   path→equiv (ap (_≡ x) (!-tabulate f i))
 
 member-tabulate : ∀ {n} (f : Fin n → A) x → (x ∈ tabulate f) ≃ fibre f x
diff --git a/src/Data/Nat/Prime.lagda.md b/src/Data/Nat/Prime.lagda.md
index 52234a99f..da27bdf9b 100644
--- a/src/Data/Nat/Prime.lagda.md
+++ b/src/Data/Nat/Prime.lagda.md
@@ -150,7 +150,7 @@ distinct-primes→coprime {a@(suc a')} {b@(suc b')} apr bpr a≠b = record
 ```agda
 is-prime-or-composite : ∀ n → 1 < n → is-prime n ⊎ is-composite n
 is-prime-or-composite n@(suc (suc m)) (s≤s p)
-  with Fin-omniscience {n = n} (λ k → 1 < to-nat k × to-nat k ∣ n)
+  with Fin-omniscience {n = n} (λ k → 1 < k .lower × k .lower ∣ n)
 ... | inr prime = inl record { prime≠1 = suc≠zero ∘ suc-inj ; primality = no-divisors→prime } where
   no-divisors→prime : ∀ d → d ∣ n → d ≡ 1 ⊎ d ≡ n
   no-divisors→prime d div with d ≡? 1
@@ -172,18 +172,18 @@ is-prime-or-composite n@(suc (suc m)) (s≤s p)
   open Σ (∣→fibre div) renaming (fst to quot ; snd to path)
 
   abstract
-    least' : (p' : Nat) → 1 < p' → p' ∣ n → to-nat ix ≤ p'
+    least' : (p' : Nat) → 1 < p' → p' ∣ n → ix .lower ≤ p'
     least' p' x div with ≤-strengthen (m∣n→m≤n div)
-    ... | inl same = ≤-trans ≤-ascend (subst (to-nat ix <_) (sym same) (to-ℕ< ix .snd))
+    ... | inl same = ≤-trans ≤-ascend (subst (ix .lower <_) (sym same) (to-ℕ< ix .snd))
     ... | inr less = least (from-ℕ< (p' , less)) (x , div)
 
-  prime : is-prime (to-nat ix)
-  prime = least-divisor→is-prime (to-nat ix) n proper div least'
+  prime : is-prime (ix .lower)
+  prime = least-divisor→is-prime (ix .lower) n proper div least'
 
   proper' : 1 < quot
   proper' with quot | path
   ... | 0 | q = absurd (<-irrefl q (s≤s 0≤x))
-  ... | 1 | q = absurd (<-irrefl (sym (+-zeror (to-nat ix)) ∙ q) (to-ℕ< ix .snd))
+  ... | 1 | q = absurd (<-irrefl (sym (+-zeror (ix .lower)) ∙ q) (to-ℕ< ix .snd))
   ... | suc (suc n) | p = s≤s (s≤s 0≤x)
 
 record Factorisation (n : Nat) : Type where