chore: rename 'cast-is' functions to 'subst-is'

src/Cat/Functor/Adjoint/Conservative.lagda.md

@@ -125,7 +125,7 @@ strong epis.
       f-strong-epi : D.is-strong-epi f
       f-strong-epi =
         D.strong-epi-cancelr f (ε x) $
-        D.cast-is-strong-epi (counit.is-natural x y f) $
+        D.subst-is-strong-epi (counit.is-natural x y f) $
         D.strong-epi-∘ (ε y) (L.₁ (R.₁ f))
           ε-strong-epi
           (D.invertible→strong-epi (L.F-map-invertible Rf-inv))

src/Cat/Functor/Adjoint/Epireflective.lagda.md

@@ -149,7 +149,7 @@ is reflective!
       unit-strong-mono : C.is-strong-mono (η x)
       unit-strong-mono =
         C.strong-mono-cancell (R.₁ (L.₁ f)) (η x) $
-        C.cast-is-strong-mono (unit.is-natural _ _ _) $
+        C.subst-is-strong-mono (unit.is-natural _ _ _) $
         C.strong-mono-∘ (η (R.₀ a)) f
           (C.invertible→strong-mono (is-reflective→unit-G-is-iso L⊣R reflective))
           f-strong-mono
@@ -224,7 +224,7 @@ $L \dashv R$ is reflective.
       RL[m]∘RL[e]-invertible
         : C.is-invertible (R.₁ (L.₁ m) C.∘ R.₁ (L.₁ e))
       RL[m]∘RL[e]-invertible =
-        C.cast-is-invertible (R.expand (L.expand factors)) $
+        C.subst-is-invertible (R.expand (L.expand factors)) $
         R.F-map-invertible $
         is-reflective→F-unit-is-iso L⊣R reflective
 ```
@@ -249,7 +249,7 @@ right-cancellation of epis to deduce that $R(L(e))$ must be epic.
       RL[e]-epic : C.is-epic (R.₁ (L.₁ e))
       RL[e]-epic =
         C.epic-cancelr $
-        C.cast-is-epic (unit.is-natural _ _ _) $
+        C.subst-is-epic (unit.is-natural _ _ _) $
         C.epic-∘
           (C.invertible→epic unit-im-invertible)
           (□-out! e-epi)
@@ -283,7 +283,7 @@ itself be invertible, so $m$ is invertible via 2-out-of-3.
       m-invertible =
         C.invertible-cancelr
           (is-reflective→unit-G-is-iso L⊣R reflective)
-          (C.cast-is-invertible (sym (unit.is-natural _ _ _)) $
+          (C.subst-is-invertible (sym (unit.is-natural _ _ _)) $
              C.invertible-∘ RL[m]-invertible unit-im-invertible)
 ```
 
@@ -293,7 +293,7 @@ so it must also be an epi.
 ```agda
       unit-epic : C.is-epic (η x)
       unit-epic =
-        C.cast-is-epic (sym factors) $
+        C.subst-is-epic (sym factors) $
         C.epic-∘
           (C.invertible→epic m-invertible)
           (□-out! e-epi)
@@ -336,7 +336,7 @@ diagram chase; we will spare the innocent reader the details.
       unit-mono : C.is-monic (η x)
       unit-mono =
         C.monic-cancell $
-        C.cast-is-monic (unit.is-natural _ _ _) $
+        C.subst-is-monic (unit.is-natural _ _ _) $
         C.monic-∘
           (C.invertible→monic (is-reflective→unit-G-is-iso L⊣R reflective))
           f-mono
@@ -359,7 +359,7 @@ diagram chase; we will spare the innocent reader the details.
       RL[m]∘RL[e]-invertible
         : C.is-invertible (R.₁ (L.₁ m) C.∘ R.₁ (L.₁ e))
       RL[m]∘RL[e]-invertible =
-        C.cast-is-invertible (R.expand (L.expand factors)) $
+        C.subst-is-invertible (R.expand (L.expand factors)) $
         R.F-map-invertible $
         is-reflective→F-unit-is-iso L⊣R reflective
 
@@ -372,7 +372,7 @@ diagram chase; we will spare the innocent reader the details.
       RL[e]-strong-epi : C.is-strong-epi (R.₁ (L.₁ e))
       RL[e]-strong-epi =
         C.strong-epi-cancelr _ _ $
-        C.cast-is-strong-epi (unit.is-natural _ _ _) $
+        C.subst-is-strong-epi (unit.is-natural _ _ _) $
         C.strong-epi-∘ _ _
           (C.invertible→strong-epi unit-im-invertible)
           (□-out! e-strong-epi)
@@ -392,12 +392,12 @@ diagram chase; we will spare the innocent reader the details.
       m-invertible =
         C.invertible-cancelr
           (is-reflective→unit-G-is-iso L⊣R reflective)
-          (C.cast-is-invertible (sym (unit.is-natural _ _ _)) $
+          (C.subst-is-invertible (sym (unit.is-natural _ _ _)) $
              C.invertible-∘ RL[m]-invertible unit-im-invertible)
 
       unit-strong-epi : C.is-strong-epi (η x)
       unit-strong-epi =
-        C.cast-is-strong-epi (sym factors) $
+        C.subst-is-strong-epi (sym factors) $
         C.strong-epi-∘ _ _
           (C.invertible→strong-epi m-invertible)
           (□-out! e-strong-epi)

src/Cat/Morphism.lagda.md

@@ -157,20 +157,20 @@ epic-precomp-embedding epic =
 
 <!--
 ```agda
-cast-is-monic
+subst-is-monic
   : ∀ {a b} {f g : Hom a b}
   → f ≡ g
   → is-monic f
   → is-monic g
-cast-is-monic f=g f-monic h i p =
+subst-is-monic f=g f-monic h i p =
   f-monic h i (ap (_∘ h) f=g ·· p ·· ap (_∘ i) (sym f=g))
 
-cast-is-epic
+subst-is-epic
   : ∀ {a b} {f g : Hom a b}
   → f ≡ g
   → is-epic f
   → is-epic g
-cast-is-epic f=g f-epic h i p =
+subst-is-epic f=g f-epic h i p =
   f-epic h i (ap (h ∘_) f=g ·· p ·· ap (i ∘_) (sym f=g))
 ```
 -->
@@ -259,13 +259,13 @@ has-section→epic {f = f} f-sect g h p =
 
 <!--
 ```agda
-cast-section
+subst-section
   : ∀ {a b} {f g : Hom a b}
   → f ≡ g
   → has-section f
   → has-section g
-cast-section p s .section = s .section
-cast-section p s .is-section = ap₂ _∘_ (sym p) refl ∙ s .is-section
+subst-section p s .section = s .section
+subst-section p s .is-section = ap₂ _∘_ (sym p) refl ∙ s .is-section
 ```
 -->
 
@@ -711,12 +711,12 @@ abstract
       (g .epic)
       i
 
-cast-is-invertible
+subst-is-invertible
   : ∀ {x y} {f g : Hom x y}
   → f ≡ g
   → is-invertible f
   → is-invertible g
-cast-is-invertible f=g f-inv =
+subst-is-invertible f=g f-inv =
   make-invertible f.inv
     (ap (_∘ f.inv) (sym f=g) ∙ f.invl)
     (ap (f.inv ∘_) (sym f=g) ∙ f.invr)

src/Cat/Morphism/Strong/Epi.lagda.md

@@ -498,13 +498,13 @@ invertible→strong-epi f-inv =
   invertible→epic f-inv , λ m →
   invertible→left-orthogonal C (m .mor) f-inv
 
-cast-is-strong-epi
+subst-is-strong-epi
   : ∀ {a b} {f g : Hom a b}
   → f ≡ g
   → is-strong-epi f
   → is-strong-epi g
-cast-is-strong-epi f=g f-strong-epi =
-  lifts→is-strong-epi (cast-is-epic f=g (f-strong-epi .fst)) λ m vg=mu →
+subst-is-strong-epi f=g f-strong-epi =
+  lifts→is-strong-epi (subst-is-epic f=g (f-strong-epi .fst)) λ m vg=mu →
     let (h , hf=u , mh=v) = f-strong-epi .snd m (ap₂ _∘_ refl f=g ∙ vg=mu) .centre
     in h , ap (h ∘_) (sym f=g) ∙ hf=u , mh=v
 ```

src/Cat/Morphism/Strong/Mono.lagda.md

@@ -160,13 +160,13 @@ strong-mono+epi→invertible {f = f} (_ , strong) epi =
 
 <!--
 ```agda
-cast-is-strong-mono
+subst-is-strong-mono
   : ∀ {a b} {f g : Hom a b}
   → f ≡ g
   → is-strong-mono f
   → is-strong-mono g
-cast-is-strong-mono f=g f-strong-mono =
-  lifts→is-strong-mono (cast-is-monic f=g (f-strong-mono .fst)) λ e vg=mu →
+subst-is-strong-mono f=g f-strong-mono =
+  lifts→is-strong-mono (subst-is-monic f=g (f-strong-mono .fst)) λ e vg=mu →
     let (h , he=u , fh=v) = f-strong-mono .snd e (vg=mu ∙ ap₂ _∘_ (sym f=g) refl) .centre
     in h , he=u , ap (_∘ h) (sym f=g) ∙ fh=v
 ```

src/Cat/Regular.lagda.md

@@ -352,7 +352,7 @@ construction, so $k = l$ --- so $g$ is _also_ monic.
 
 ```agda
         rem₅ : is-strong-epi 𝒞 d×d
-        rem₅ = cast-is-strong-epi 𝒞 rem₄ (strong-epi-∘ 𝒞 _ _ rem₃ rem₂)
+        rem₅ = subst-is-strong-epi 𝒞 rem₄ (strong-epi-∘ 𝒞 _ _ rem₃ rem₂)
 
         rem₆ : is-strong-epi 𝒞 p
         rem₆ = r.stable _ _ rem₅ pb.has-is-pb