WIP: Bump past agda/agda#8367

1lab.agda-lib

@@ -12,4 +12,5 @@ flags:
   --guardedness
   --two-level
   -W noUnsupportedIndexedMatch
+  -W noRewriteVariablesBoundInSingleton
   --experimental-lazy-instances

src/Algebra/Group/Concrete.lagda.md

@@ -258,9 +258,9 @@ The following construction is adapted from [@Symmetry, §6.5]:
   record C (x : ⌞ G ⌟) : Type ℓ where
     constructor mk
     field
-      y : ⌞ H ⌟
-      p : pt G ≡ x → pt H ≡ y
-      f-p : (ω : pt G ≡ pt G) (α : pt G ≡ x) → p (ω ∙ α) ≡ f · ω ∙ p α
+      y   : ⌞ H ⌟
+      p   : pt G ≡ x → pt H ≡ y
+      f-p : ∀ ω α → p (ω ∙ α) ≡ f · ω ∙ p α
 ```
 
 Our family sends a point $x : \B{G}$ to a point $y : \B{H}$ with a function $p$ that
@@ -326,7 +326,7 @@ Since $g$ is pointed by $p(\refl)$, this lets us conclude that we have found a
 right inverse to $\Pi_1$:
 
 ```agda
-  f≡apg : (ω : pt G ≡ pt G) → Square (p refl) (f · ω) (ap (g .fst) ω) (p refl)
+  f≡apg : ∀ ω → Square (p refl) (f · ω) (ap (g .fst) ω) (p refl)
   f≡apg ω = commutes→square $
     p refl ∙ ap (g .fst) ω ≡˘⟨ p-g refl ω ⟩
     p (refl ∙ ω)           ≡˘⟨ ap p ∙-id-comm ⟩

src/Algebra/Group/Free/Product.lagda.md

@@ -71,7 +71,7 @@ be [[group homomorphisms]] and to make the pushout square commute...
     inr : ⌞ B ⌟ → Amalgamated
     inr-hom : ∀ b b' → inr (b B.⋆ b') ≡ inr b ◆ inr b'
 
-    glue : (c : ⌞ C ⌟) → inl (f · c) ≡ inr (g · c)
+    glue : ∀ c → inl (f · c) ≡ inr (g · c)
 ```
 
 ...finally, we truncate the resulting type to a set.

src/Algebra/Group/Free/Words.lagda.md

@@ -600,7 +600,7 @@ Finally, we can put this together for an arbitrary reduced word, using
 the lemmas above for each case.
 
 ```agda
-  uniq : ∀ xs (α : Reduced xs) → g · (xs , α) ≡ go xs
+  uniq : ∀ xs α → g · (xs , α) ≡ go xs
   uniq xs nil     = g.pres-id
   uniq xs (one a) =
     g · (a ∷ [] , one a)    ≡⟨ g-cons _ _ (one a) ⟩

src/Algebra/Group/Homotopy.lagda.md

@@ -81,12 +81,12 @@ opaque
   πₙ-def A n = n-Tr-set ∙e n-Tr-Ωⁿ A 1 (suc n) .fst , n-Tr-Ωⁿ A 1 (suc n) .snd
 
   πₙ-def-inc
-    : ∀ {ℓ} (A : Type∙ ℓ) n → (l : ⌞ Ωⁿ (1 + n) A ⌟)
+    : ∀ {ℓ} (A : Type∙ ℓ) n l
     → πₙ-def A n · inc l ≡ Ωⁿ-map (1 + n) inc∙ · l
   πₙ-def-inc A n l = n-Tr-Ωⁿ-inc A 1 (suc n) ·ₚ l
 
   πₙ-def-∙
-    : ∀ {ℓ} (A : Type∙ ℓ) n → (p q : ⌞ Ωⁿ (1 + n) A ⌟)
+    : ∀ {ℓ} (A : Type∙ ℓ) n p q
     → πₙ-def A n · inc (p ∙ q) ≡ πₙ-def A n · inc p ∙ πₙ-def A n · inc q
   πₙ-def-∙ A = n-Tr-Ωⁿ-∙ A 1
 ```

src/Algebra/Group/Instances/Cyclic.lagda.md

@@ -77,17 +77,16 @@ $n$ when $n \geq 1$, and is the infinite cyclic group when $n = 0$.
 
 ```agda
 infix 30 _·ℤ
-_·ℤ : ∀ (n : Nat) → normal-subgroup ℤ λ i → el (n ∣ℤ i) (∣ℤ-is-prop n i)
+_·ℤ : ∀ n → normal-subgroup ℤ λ i → el (n ∣ℤ i) (∣ℤ-is-prop n i)
 (n ·ℤ) .has-rep .has-unit = ∣ℤ-zero
 (n ·ℤ) .has-rep .has-⋆ = ∣ℤ-+
 (n ·ℤ) .has-rep .has-inv = ∣ℤ-negℤ
-(n ·ℤ) .has-conjugate {x} {y} = subst (n ∣ℤ_) x≡y+x-y
-  where
-    x≡y+x-y : x ≡ y +ℤ (x -ℤ y)
-    x≡y+x-y =
-      x                  ≡⟨ ℤ.insertl {y} (ℤ.inverser {x = y}) ⟩
-      y +ℤ (negℤ y +ℤ x) ≡⟨ ap (y +ℤ_) (+ℤ-commutative (negℤ y) x) ⟩
-      y +ℤ (x -ℤ y)      ∎
+(n ·ℤ) .has-conjugate {x} {y} = subst (n ∣ℤ_) x≡y+x-y where
+  x≡y+x-y : x ≡ y +ℤ (x -ℤ y)
+  x≡y+x-y =
+    x                  ≡⟨ ℤ.insertl {y} (ℤ.inverser {x = y}) ⟩
+    y +ℤ (negℤ y +ℤ x) ≡⟨ ap (y +ℤ_) (+ℤ-commutative (negℤ y) x) ⟩
+    y +ℤ (x -ℤ y)      ∎
 
 infix 25 ℤ/_
 ℤ/_ : Nat → Group lzero

src/Algebra/Group/Instances/Integers.lagda.md

@@ -193,15 +193,15 @@ one generator.
 ```agda
 instance
   Extensional-ℤ-Hom
-    : ∀ {ℓ ℓr} {G : Group ℓ} ⦃ _ : Extensional ⌞ G ⌟ ℓr ⦄
+    : ∀ {ℓ ℓr G} ⦃ _ : Extensional ⌞ G ⌟ ℓr ⦄
     → Extensional (Groups.Hom (Lift-group ℓ ℤ) G) ℓr
   Extensional-ℤ-Hom ⦃ e ⦄ = injection→extensional! {f = λ h → h · 1} (pow-unique₂ _ _ _) e
 
   Extensional-Ab-ℤ-Hom
-    : ∀ {ℓ ℓr} {G : ⌞ Ab ℓ ⌟} ⦃ _ : Extensional ⌞ G ⌟ ℓr ⦄
+    : ∀ {ℓ ℓr G} ⦃ _ : Extensional ⌞ G ⌟ ℓr ⦄
     → Extensional (Ab.Hom (Lift-ab ℓ ℤ-ab) G) ℓr
   Extensional-Ab-ℤ-Hom {ℓ = ℓ} {G = G} ⦃ ef ⦄ = injection→extensional! {f = λ h → h · 1} inj ef where
-    inj : {x y : Ab.Hom (Lift-ab ℓ ℤ-ab) G} → x · 1 ≡ y · 1 → x ≡ y
+    inj : ∀ {x y} → x · 1 ≡ y · 1 → x ≡ y
     inj {x} {y} p = Structured-hom-path _ (ap fst (pow-unique₂ G' x' y' p)) where
       G' : Group ℓ
       G' .fst = G .fst

src/Algebra/Group/Subgroup.lagda.md

@@ -62,7 +62,8 @@ group homomorphism.
 
 ```agda
 rep-subgroup→group-on
-  : (H : ℙ ⌞ G ⌟) → represents-subgroup G H → Group-on (Σ[ x ∈ G ] x ∈ H)
+  : {G : Group ℓ} (H : ℙ ⌞ G ⌟)
+  → represents-subgroup G H → Group-on (Σ[ x ∈ G ] x ∈ H)
 rep-subgroup→group-on {G = G} H sg = to-group-on sg' where
   open Group-on (G .snd)
   open represents-subgroup sg

src/Algebra/Ring/Cat/Initial.lagda.md

@@ -224,7 +224,7 @@ evaluates to on $n$. So we're done!
     f-pos zero = sym f.pres-0
     f-pos (suc x) = e-suc x ∙ sym (f.pres-+ (lift 1) (lift (pos x)) ∙ ap₂ R._+_ f.pres-id (sym (f-pos x)))
 
-    lemma : (i : Int) → z→r · lift i ≡ f · lift i
+    lemma : ∀ i → z→r · lift i ≡ f · lift i
     lemma (pos x) = f-pos x
     lemma (negsuc x) = sym (f.pres-neg {lift (possuc x)} ∙ ap R.-_ (sym (f-pos (suc x))))
 ```

src/Algebra/Ring/Solver.agda

@@ -52,7 +52,10 @@ module Impl {ℓ} {R : Type ℓ} (cring : CRing-on R) where
   embed-coe : Int → R
   embed-coe x = ℤ↪R-rh .fst (lift x)
 
-  embed-lemma : {h' : Int → R} → is-ring-hom (Liftℤ {ℓ} .snd) (R' .snd) (h' ⊙ lower) → ∀ x → embed-coe x ≡ h' x
+  embed-lemma
+    : {h' : Int → R}
+    → is-ring-hom (Liftℤ {ℓ} .snd) (R' .snd) (h' ⊙ lower)
+    → ∀ x → embed-coe x ≡ h' x
   embed-lemma p x = Int-is-initial R' .paths (∫hom _ p) ·ₚ lift x
 
   data Poly   : Nat → Type ℓ

src/Cat/Base.lagda.md

@@ -581,7 +581,7 @@ instance
   Extensional-natural-transformation
     : ∀ {o ℓ o' ℓ' ℓr} {C : Precategory o ℓ} {D : Precategory o' ℓ'}
     → {F G : Functor C D}
-    → ⦃ sa : {x : ⌞ C ⌟} → Extensional (D .Hom (F · x) (G · x)) ℓr ⦄
+    → ⦃ sa : ∀ {x} → Extensional (D .Hom (F · x) (G · x)) ℓr ⦄
     → Extensional (F => G) (o ⊔ ℓr)
   Extensional-natural-transformation ⦃ sa ⦄ .Pathᵉ f g = ∀ i → Pathᵉ sa (f .η i) (g .η i)
   Extensional-natural-transformation ⦃ sa ⦄ .reflᵉ x i = reflᵉ sa (x .η i)

src/Cat/CartesianClosed/Free.lagda.md

@@ -236,7 +236,7 @@ interpretation $f$ of the base types in $\cD$.
 
 ```agda
     (cco  : Cartesian-closed-over D cart Free-closed)
-    (f : (x : Node) → D ʻ (` x))
+    (f : ∀ x → D ʻ (` x))
   where
 ```
 
@@ -252,7 +252,7 @@ This lets us construct a section of the objects of $\cD$, i.e. a method
 that turns any type $\tau$ into an object $S(\tau) \liesover \tau$.
 
 ```agda
-  Ty-elim : (x : Ty) → D ʻ x
+  Ty-elim : ∀ x → D ʻ x
   Ty-elim `⊤       = top'
   Ty-elim (` x)    = f x
   Ty-elim (τ `× σ) = Ty-elim τ ⊗₀' Ty-elim σ
@@ -268,10 +268,10 @@ basic term $e$.
 
 ```agda
   base-method : Type _
-  base-method = ∀ {x y} (e : Edge x y) → Hom[ ` e ] (Ty-elim x) (f y)
+  base-method = ∀ {x y} e → Hom[ ` e ] (Ty-elim x) (f y)
 
   private module _ (h : base-method) where
-    go : ∀ {x y} (m : Mor x y) → Hom[ m ] (Ty-elim x) (Ty-elim y)
+    go : ∀ {x y} m → Hom[ m ] (Ty-elim x) (Ty-elim y)
 ```
 
 By a long and uninteresting case bash, we can extend
@@ -1270,16 +1270,16 @@ These are required to make the following triangles commute.
 :::
 
 ```agda
-    com₀ : {Γ : Cx} (n : Ne Γ τ)     → ⟦ reflect n ⟧ₚ ≡ ⟦ n ⟧ₛ
-    com₁ : {Γ : Cx} (x : P .dom ʻ Γ) → ⟦ x ⟧ₚ ≡ ⟦ reify x ⟧ₙ
+    com₀ : ∀ {Γ} (n : Ne Γ τ)     → ⟦ reflect n ⟧ₚ ≡ ⟦ n ⟧ₛ
+    com₁ : ∀ {Γ} (x : P .dom ʻ Γ) → ⟦ x ⟧ₚ ≡ ⟦ reify x ⟧ₙ
 ```
 
 <!--
 ```agda
   reifyₙ : ∀ {Γ Δ} {ρ : Ren Γ Δ} {x : P .dom ʻ Δ} → reify (P .dom ⟪ ρ ⟫ x) ≡ ren-nf ρ (reify x)
   reifyₙ {Γ} {Δ} {ρ} {x} = reifies .is-natural Δ Γ ρ $ₚ x
 
-  reflectₙ : ∀ {Γ Δ} {ρ : Ren Γ Δ} {x : Ne Δ τ} → reflect (ren-ne ρ x) ≡ P .dom ⟪ ρ ⟫ (reflect x)
+  reflectₙ : ∀ {Γ Δ} {ρ : Ren Γ Δ} {x} → reflect (ren-ne ρ x) ≡ P .dom ⟪ ρ ⟫ (reflect x)
   reflectₙ {Γ} {Δ} {ρ} {x} = reflects .is-natural Δ Γ ρ $ₚ x
 
 GlTm-closed = Gl-closed PSh-closed Free-closed PSh-pullbacks
@@ -1295,7 +1295,7 @@ map --- embedding neutrals into normals --- is not literally the identity
 function, but an inductive constructor instead.
 
 ```agda
-Gl-base : (n : Node) → Gl ʻ (` n)
+Gl-base : ∀ n → Gl ʻ (` n)
 Gl-base x = cut (rnf {` x})
 
 base-nfa : ∀ {x} → Nfa (Gl-base x)
@@ -1502,9 +1502,7 @@ into normals, namely `reifies`{.Agda}.
 
 ```agda
   private
-    terms
-      : ∀ {x : Ty} {y : Node} (e : Edge x y)
-      → Gl.Hom[ (` e) ] (Ty-nf x) (Gl-base y)
+    terms : ∀ {x y} e → Gl.Hom[ (` e) ] (Ty-nf x) (Gl-base y)
     terms {x = x} {y = y} e .map =
           NT (λ Γ x → ne (hom e x)) (λ x y f → refl)
       ∘nt Nfa.reifies (normalisation x)
@@ -1540,8 +1538,8 @@ $$
 which is exactly what we wanted! We're finally `done`{.Agda}.
 
 ```agda
-idsec : (Γ : Cx) → ⟦ ⟦ Γ ⟧ᶜ ⟧₀ .dom ʻ Γ
-idsecβ : (Γ : Cx) → ⟦ ⟦ Γ ⟧ᶜ ⟧₀ .map .η Γ (idsec Γ) ≡ `id
+idsec  : ∀ Γ → ⟦ ⟦ Γ ⟧ᶜ ⟧₀ .dom ʻ Γ
+idsecβ : ∀ Γ → ⟦ ⟦ Γ ⟧ᶜ ⟧₀ .map .η Γ (idsec Γ) ≡ `id
 ```
 
 <!--

src/Cat/Displayed/Base.lagda.md

@@ -182,9 +182,10 @@ record Trivially-graded {o ℓ} (B : Precategory o ℓ) (o' ℓ' : Level) : Type
     Ob[_]  : Ob → Type o'
     Hom[_] : ∀ {x y} → Hom x y → Ob[ x ] → Ob[ y ] → Type ℓ'
 
-    ⦃ H-Level-Hom[_] ⦄
-      : ∀ {a b} {f : Hom a b} {x : Ob[ a ]} {y : Ob[ b ]}
-      → H-Level (Hom[ f ] x y) 2
+    instance
+      ⦃ H-Level-Hom[_] ⦄
+        : ∀ {a b} {f : Hom a b} {x : Ob[ a ]} {y : Ob[ b ]}
+        → H-Level (Hom[ f ] x y) 2
 
     id'  : ∀ {a} {x : Ob[ a ]} → Hom[ id ] x x
     _∘'_ : ∀ {a b c x y z} {f : Hom b c} {g : Hom a b}
@@ -212,9 +213,10 @@ record Thinly-displayed {o ℓ} (B : Precategory o ℓ) (o' ℓ' : Level) : Type
     Ob[_]  : Ob → Type o'
     Hom[_] : ∀ {x y} → Hom x y → Ob[ x ] → Ob[ y ] → Type ℓ'
 
-    ⦃ H-Level-Hom[_] ⦄
-      : ∀ {a b} {f : Hom a b} {x : Ob[ a ]} {y : Ob[ b ]}
-      → H-Level (Hom[ f ] x y) 1
+    instance
+      ⦃ H-Level-Hom[_] ⦄
+        : ∀ {a b} {f : Hom a b} {x : Ob[ a ]} {y : Ob[ b ]}
+        → H-Level (Hom[ f ] x y) 1
 
     id'  : ∀ {a} {x : Ob[ a ]} → Hom[ id ] x x
     _∘'_ : ∀ {a b c x y z} {f : Hom b c} {g : Hom a b}
@@ -230,14 +232,14 @@ with-trivial-grading triv = record
   ; hom[_]     = subst (λ e → Hom[ e ] _ _)
   ; coh[_]     = λ p → transport-filler _
   }
-  where open Trivially-graded triv using (Hom[_])
+  where open Trivially-graded triv using (Hom[_] ; H-Level-Hom[_])
 
 with-thin-display
   : ∀ {o ℓ} {B : Precategory o ℓ} {o' ℓ' : Level} → Thinly-displayed B o' ℓ'
   → Displayed B o' ℓ'
 {-# INLINE with-thin-display #-}
 with-thin-display triv = with-trivial-grading record where
-  open Thinly-displayed triv using (Ob[_] ; Hom[_] ; id' ; _∘'_)
+  open Thinly-displayed triv using (Ob[_] ; Hom[_] ; id' ; _∘'_) renaming (H-Level-Hom[_] to i)
   H-Level-Hom[_] = basic-instance 2 $ is-prop→is-set (hlevel 1)
   idr'   f     = prop!
   idl'   f     = prop!

src/Cat/Displayed/Cartesian/Joint.lagda.md

@@ -753,18 +753,14 @@ postcompose-equiv→jointly-cartesian {a = a} {uᵢ = uᵢ} fᵢ eqv = fᵢ-cart
   open is-jointly-cartesian
 
   fᵢ-cart : is-jointly-cartesian uᵢ fᵢ
-  fᵢ-cart .universal v hᵢ =
-    eqv.from hᵢ
-  fᵢ-cart .commutes v hᵢ ix =
-    eqv.ε hᵢ ·ₚ ix
-  fᵢ-cart .unique {hᵢ = hᵢ} other p =
-    sym (eqv.η other) ∙ ap eqv.from (ext p)
+  fᵢ-cart .universal v hᵢ = eqv.from hᵢ
+  fᵢ-cart .commutes v hᵢ ix = eqv.ε hᵢ ·ₚ ix
+  fᵢ-cart .unique {hᵢ = hᵢ} other p = sym (eqv.η other) ∙ ap eqv.from (ext p)
 
 jointly-cartesian→postcompose-equiv {uᵢ = uᵢ} {fᵢ = fᵢ} fᵢ-cart v x' .is-eqv hᵢ =
   contr (fᵢ.universal v hᵢ , ext (fᵢ.commutes v hᵢ)) λ fib →
     Σ-prop-pathp! (sym (fᵢ.unique (fib .fst) (λ ix → fib .snd ·ₚ ix)))
-  where
-    module fᵢ = is-jointly-cartesian fᵢ-cart
+  where module fᵢ = is-jointly-cartesian fᵢ-cart
 ```
 </details>
 

src/Cat/Displayed/Diagram/Total/Exponential.lagda.md

@@ -50,7 +50,7 @@ the corresponding constructions in $\cB$, and this is equivalent to the
 <!--
 ```agda
 module
-  _ {A B B^A : Ob} {ev : Hom (B^A ⊗₀ A) B}
+  _ {A B B^A} {ev : Hom (B^A ⊗₀ A) B}
     (exp : is-exponential _ bcart B^A ev)
     {A' : E ʻ A} {B' : E ʻ B} (B^A' : E ʻ B^A)
   where

src/Cat/Displayed/Diagram/Total/Product.lagda.md

@@ -192,7 +192,7 @@ has-products-over
   → Displayed B o' ℓ'
   → has-products B
   → Type _
-has-products-over {B = B} E prod = ∀ {a b : ⌞ B ⌟} (x : E ʻ a) (y : E ʻ b) → ProductP E (prod a b) x y
+has-products-over {B = B} E prod = ∀ {a b} (x : E ʻ a) (y : E ʻ b) → ProductP E (prod a b) x y
 ```
 -->
 

src/Cat/Displayed/Diagram/Total/Terminal.lagda.md

@@ -36,8 +36,8 @@ displayed over $!$.
 record is-terminal-over {top} (term : is-terminal B top) (top' : E ʻ top) : Type (o ⊔ o' ⊔ ℓ') where
   open Terminal {C = B} record{ has⊤ = term } hiding (top)
   field
-    !'        : {y : ⌞ B ⌟} {y' : E ʻ y} → E.Hom[ ! ] y' top'
-    !-unique' : {y : ⌞ B ⌟} {y' : E ʻ y} (h : E.Hom[ ! ] y' top') → !' ≡ h
+    !'        : ∀ {y} {y' : E ʻ y} → E.Hom[ ! ] y' top'
+    !-unique' : ∀ {y} {y' : E ʻ y} (h : E.Hom[ ! ] y' top') → !' ≡ h
 
   opaque
     !ₚ : ∀ {y} {m : B.Hom y top} {y' : E ʻ y} → E.Hom[ m ] y' top'

src/Cat/Displayed/Doctrine/Logic.lagda.md

@@ -413,7 +413,7 @@ private variable
   Φ Ψ φ ψ θ φ' ψ' : Formula Γ
   t t₁ s s₁ : Tm Γ τ
 
-wk : ∀ {Γ} (φ : Formula Γ) {τ : Ty} → Formula (Γ ʻ τ)
+wk : ∀ {Γ} (φ : Formula Γ) {τ} → Formula (Γ ʻ τ)
 wk φ = sub-prop (drop stop) φ
 ```
 -->

src/Cat/Displayed/Instances/Scone.lagda.md

@@ -100,11 +100,11 @@ private module Scones = Displayed Scones
 -->
 
 ```agda
-scone : ∀ {X} → (U : Set ℓ) → (∣ U ∣ → Hom top X) → Scones ʻ X
+scone : ∀ {X} U → (∣ U ∣ → Hom top X) → Scones ʻ X
 scone U s = cut {dom = U} s
 
 scone-hom
-  : ∀ {X Y} {f : Hom X Y} {U V : Set ℓ}
+  : ∀ {X Y} {f : Hom X Y} {U V}
   → {su : ∣ U ∣ → Hom top X} {sv : ∣ V ∣ → Hom top Y}
   → (uv : ∣ U ∣ → ∣ V ∣)
   → (∀ u → sv (uv u) ≡ f ∘ (su u))

src/Cat/Displayed/Section.lagda.md

@@ -39,11 +39,13 @@ arguments.
 ```agda
   record Section : Type (o ⊔ ℓ ⊔ o' ⊔ ℓ') where
     field
-      S₀ : (x : ⌞ B ⌟) → E ʻ x
-      S₁ : {x y : ⌞ B ⌟} (f : B.Hom x y) → E.Hom[ f ] (S₀ x) (S₀ y)
+      S₀ : ∀ x → E ʻ x
+      S₁ : ∀ {x y} (f : B.Hom x y) → E.Hom[ f ] (S₀ x) (S₀ y)
 
-      S-id : {x : ⌞ B ⌟} → S₁ {x} {x} B.id ≡ E.id'
-      S-∘  : {x y z : ⌞ B ⌟} (f : B.Hom y z) (g : B.Hom x y) → S₁ (f B.∘ g) ≡ S₁ f E.∘' S₁ g
+      S-id : ∀ {x} → S₁ {x} {x} B.id ≡ E.id'
+      S-∘
+        : ∀ {x y z} (f : B.Hom y z) (g : B.Hom x y)
+        → S₁ (f B.∘ g) ≡ S₁ f E.∘' S₁ g
 ```
 
 <details>
@@ -100,8 +102,8 @@ to work with sections instead.
       module Q = Section Q
 
     field
-      map : (x : ⌞ B ⌟) → E.Hom[ B.id ] (P · x) (Q · x)
-      com : (x y : ⌞ B ⌟) (f : B.Hom x y)
+      map : ∀ x → E.Hom[ B.id ] (P · x) (Q · x)
+      com : ∀ x y (f : B.Hom x y)
           → map y E.∘' P.S₁ f E.≡[ B.id-comm-sym ] Q.S₁ f E.∘' map x
 ```
 
@@ -116,7 +118,7 @@ to work with sections instead.
     H-Level-Natₛ = basic-instance 2 (Iso→is-hlevel 2 eqv (hlevel 2))
 
     Extensional-Natₛ
-      : ∀ {P Q ℓr} ⦃ _ : Extensional ((x : ⌞ B ⌟) → E.Hom[ B.id ] (P · x) (Q · x)) ℓr ⦄
+      : ∀ {P Q ℓr} ⦃ _ : Extensional (∀ x → E.Hom[ B.id ] (P · x) (Q · x)) ℓr ⦄
       → Extensional (P =>s Q) ℓr
     Extensional-Natₛ = injection→extensional! (λ p → Iso.injective eqv (p ,ₚ prop!)) auto
 

src/Cat/Displayed/Univalence/Thin.lagda.md

@@ -133,7 +133,7 @@ module _ {ℓ o' ℓ'} {S : Type ℓ → Type o'} {spec : Thin-structure ℓ' S}
       (Structured-hom-path spec) sa
 
   Homomorphism-monic
-    : ∀ {x y : So.Ob} (f : So.Hom x y)
+    : ∀ {x y} (f : So.Hom x y)
     → (∀ {x y} (p : f · x ≡ f · y) → x ≡ y)
     → Som.is-monic f
   Homomorphism-monic f wit g h p = ext λ x → wit (ap fst p $ₚ x)