chore: bump (#483)

A lot of code movement because of the new warnings re. private/abstract

Author: plt-amy

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

@@ -54,7 +54,7 @@ open is-group-hom
 module _ {ℓ} (T : Type ℓ) (t-set : is-set T) where
   function→free-ab-hom : (G : Abelian-group ℓ) → (T → ⌞ G ⌟) → Ab.Hom (Free-abelian T) G
   function→free-ab-hom G fn = morp where
-    private module G = Abelian-group-on (G .snd)
+    module G = Abelian-group-on (G .snd)
     go₀ : Free-group T → ⌞ G ⌟
     go₀ = fold-free-group {G = G .fst , G.Abelian→Group-on} fn .hom
 

src/Algebra/Quasigroup.lagda.md

@@ -245,7 +245,7 @@ is-right-quasigroup-hom-is-prop {T = T} =
   Iso→is-hlevel! 1 eqv
   where
     open Right-quasigroup-on T
-    private unquoteDecl eqv = declare-record-iso eqv (quote is-right-quasigroup-hom)
+    unquoteDecl eqv = declare-record-iso eqv (quote is-right-quasigroup-hom)
 
 instance
   H-Level-is-right-quasigroup-hom
@@ -424,7 +424,7 @@ is-left-quasigroup≃op-is-right-quasigroup =
         let open is-left-quasigroup ⋆-left-quasi in
         Iso.injective eqv (refl ,ₚ prop!))
     where
-      private unquoteDecl eqv = declare-record-iso eqv (quote is-left-quasigroup)
+      unquoteDecl eqv = declare-record-iso eqv (quote is-left-quasigroup)
 ```
 </details>
 
@@ -537,7 +537,7 @@ is-left-quasigroup-hom-is-prop {T = T} =
   Iso→is-hlevel! 1 eqv
   where
     open Left-quasigroup-on T
-    private unquoteDecl eqv = declare-record-iso eqv (quote is-left-quasigroup-hom)
+    unquoteDecl eqv = declare-record-iso eqv (quote is-left-quasigroup-hom)
 
 instance
   H-Level-is-left-quasigroup-hom
@@ -771,7 +771,7 @@ is-quasigroup-hom-is-prop {T = T} =
   Iso→is-hlevel! 1 eqv
   where
     open Quasigroup-on T
-    private unquoteDecl eqv = declare-record-iso eqv (quote is-quasigroup-hom)
+    unquoteDecl eqv = declare-record-iso eqv (quote is-quasigroup-hom)
 
 instance
   H-Level-is-quasigroup-hom

src/Algebra/Ring/Module/Multilinear.lagda.md

@@ -174,29 +174,28 @@ Multilinear-maps
       {N : Module R ℓn}
   → Module-on R (Multilinear-map n Ms N)
 Multilinear-maps {n = n} {Ms = Ms} {N = N} = to-module-on mk where
-  private
-    module Ms i = Module-on (Ms i .snd)
-    module N    = Module-on (N .snd)
-    instance
-      _ = module-notation N
-      _ : ∀ {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 ⌟
-    _⟨_⟩ f {xs} {i} x = applyᶠ (f .map) (updateₚ xs i x)
-
-    _⟨_⟩ᵤ
-      : ∀ {n ℓ'} {ℓ : Fin n → Level} {P : (i : Fin n) → Type (ℓ i)} {X : Type ℓ'}
-      → Arrᶠ P X → {_ : Πᶠ P} {i : Fin n} → P i → X
-    _⟨_⟩ᵤ f {xs} {i} x = applyᶠ f (updateₚ xs i x)
-
-    infix 300 _⟨_⟩
-    infix 300 _⟨_⟩ᵤ
+  module Ms i = Module-on (Ms i .snd)
+  module N    = Module-on (N .snd)
+  instance
+    _ = module-notation N
+    _ : ∀ {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 ⌟
+  _⟨_⟩ f {xs} {i} x = applyᶠ (f .map) (updateₚ xs i x)
+
+  _⟨_⟩ᵤ
+    : ∀ {n ℓ'} {ℓ : Fin n → Level} {P : (i : Fin n) → Type (ℓ i)} {X : Type ℓ'}
+    → Arrᶠ P X → {_ : Πᶠ P} {i : Fin n} → P i → X
+  _⟨_⟩ᵤ f {xs} {i} x = applyᶠ f (updateₚ xs i x)
+
+  infix 300 _⟨_⟩
+  infix 300 _⟨_⟩ᵤ
 ```
 -->
 

src/Algebra/Ring/Solver.agda

@@ -448,8 +448,9 @@ module Reflection where
     pattern group-field field-name cring args =
       def field-name
         (is-group-args
-          (def (quote is-ring.+-group)
-            (is-ring-args (ring-field (quote Ring-on.has-is-ring) cring []) []))
+          (def (quote (is-abelian-group.has-is-group))
+            (_ hm∷ _ hm∷ _ hm∷ def (quote is-ring.+-group)
+              (is-ring-args (ring-field (quote Ring-on.has-is-ring) cring []) []) v∷ []))
           args)
 
     mk-cring-args : Term → List (Arg Term) → List (Arg Term)
@@ -458,8 +459,8 @@ module Reflection where
     pattern “1” cring = ring-field (quote Ring-on.1r) cring []
     pattern “*” cring x y = ring-field (quote Ring-on._*_) cring (x v∷ y v∷ [])
     pattern “+” cring x y = ring-field (quote Ring-on._+_) cring (x v∷ y v∷ [])
-    pattern “0” cring = group-field (quote is-abelian-group.1g) cring []
-    pattern “-” cring x = group-field (quote is-abelian-group.inverse) cring (x v∷ [])
+    pattern “0” cring = group-field (quote is-group.unit) cring []
+    pattern “-” cring x = group-field (quote is-group.inverse) cring (x v∷ [])
 
   “expand” : Term → Term → Term → Term
   “expand” cring p env = def (quote Impl.expand) (mk-cring-args cring (unknown h∷ p v∷ env v∷ []))
@@ -498,9 +499,7 @@ module Reflection where
   dont-reduce : List Name
   dont-reduce =
     quote Number.fromNat ∷
-    quote is-abelian-group.1g ∷
     quote Ring-on.1r ∷
-    quote is-abelian-group.inverse ∷
     quote Ring-on._*_ ∷
     quote Ring-on._+_ ∷
     []

src/Cat/Bi/Diagram/Monad.lagda.md

@@ -109,7 +109,7 @@ module _ {o ℓ} {C : Precategory o ℓ} where
 
   Bicat-monad→monad : Monad (Cat _ _) C → Cat.Monad C
   Bicat-monad→monad monad = _ , monad' where
-    private module M = Monad monad
+    module M = Monad monad
 
     monad' : Cat.Monad-on M.M
     monad' .unit = M.η
@@ -127,7 +127,7 @@ module _ {o ℓ} {C : Precategory o ℓ} where
 
   Monad→bicat-monad : Cat.Monad C → Monad (Cat _ _) C
   Monad→bicat-monad (M , monad) = monad' where
-    private module M = Cat.Monad-on (monad)
+    module M = Cat.Monad-on (monad)
 
     monad' : Monad (Cat _ _) C
     monad' .Monad.M = M

src/Cat/Bi/Instances/Relations.lagda.md

@@ -187,35 +187,34 @@ into a subobject.]
   → (χ : a ↬ b)
   → (∘-rel φ (∘-rel ψ χ)) Sub.≅ (∘-rel (∘-rel φ ψ) χ)
 ∘-rel-assoc {a} {b} {c} {d} r s t = done where
-  private
-    module rs = ∘-rel r s
-    module st = ∘-rel s t
-    module [rs]t = ∘-rel (∘-rel r s) t
-    module r[st] = ∘-rel r (∘-rel s t)
-    v₂ = rs.inter .p₂
-    v₁ = rs.inter .p₁
+  module rs = ∘-rel r s
+  module st = ∘-rel s t
+  module [rs]t = ∘-rel (∘-rel r s) t
+  module r[st] = ∘-rel r (∘-rel s t)
+  v₂ = rs.inter .p₂
+  v₁ = rs.inter .p₁
 
-    u₂ = st.inter .p₂
-    u₁ = st.inter .p₁
-    open Relation r renaming (src to r₁ ; tgt to r₂) hiding (rel)
-    open Relation s renaming (src to s₁ ; tgt to s₂) hiding (rel)
-    open Relation t renaming (src to t₁ ; tgt to t₂) hiding (rel)
+  u₂ = st.inter .p₂
+  u₁ = st.inter .p₁
+  open Relation r renaming (src to r₁ ; tgt to r₂) hiding (rel)
+  open Relation s renaming (src to s₁ ; tgt to s₂) hiding (rel)
+  open Relation t renaming (src to t₁ ; tgt to t₂) hiding (rel)
 
-    i : ∀ {x y} {f : Hom x y} → Hom im[ f ] y
-    i = factor _ .forget
+  i : ∀ {x y} {f : Hom x y} → Hom im[ f ] y
+  i = factor _ .forget
 
-    q : ∀ {x y} {f : Hom x y} → Hom x im[ f ]
-    q = factor _ .mediate
+  q : ∀ {x y} {f : Hom x y} → Hom x im[ f ]
+  q = factor _ .mediate
 
-    ξ₁ = [rs]t.inter .p₁
-    ξ₂ = [rs]t.inter .p₂
+  ξ₁ = [rs]t.inter .p₁
+  ξ₂ = [rs]t.inter .p₂
 
-    ζ₁ = r[st].inter .p₁
-    ζ₂ = r[st].inter .p₂
+  ζ₁ = r[st].inter .p₁
+  ζ₂ = r[st].inter .p₂
 
   X : Pullback C (rs.inter .p₁) (st.inter .p₂)
   X = lex.pullbacks (rs.inter .p₁) (st.inter .p₂)
-  private module X = Pullback X renaming (p₂ to x₁ ; p₁ to x₂)
+  module X = Pullback X renaming (p₂ to x₁ ; p₁ to x₂)
   open X using (x₂ ; x₁)
 ```
 -->

src/Cat/Bi/Instances/Spans.lagda.md

@@ -149,10 +149,10 @@ module _ (pb : ∀ {a b c} (f : Hom a b) (g : Hom c b) → Pullback C f g) where
       module x = Pullback (pb (x1 .left) (x2 .right))
       module y = Pullback (pb (y1 .left) (y2 .right))
 
+      open Pullback
       x→y : Hom x.apex y.apex
       x→y = y.universal {p₁' = f .map ∘ x.p₁} {p₂' = g .map ∘ x.p₂} comm
         where abstract
-          open Pullback
           comm : y1 .left ∘ f .map ∘ x.p₁ ≡ y2 .right ∘ g .map ∘ x.p₂
           comm = pulll (sym (f .left)) ∙ x.square ∙ pushl (g .right)
 

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

@@ -449,7 +449,7 @@ this witness lives in a proposition (it is a pair of propositions), so
 it survives automatically.
 
 ```agda
-    private unquoteDecl eqv = declare-record-iso eqv (quote is-discrete-cartesian-fibration)
+    unquoteDecl eqv = declare-record-iso eqv (quote is-discrete-cartesian-fibration)
     hl : ∀ x → is-prop _
     hl x = Iso→is-hlevel! 1 eqv
 ```

src/Cat/Displayed/Morphism.lagda.md

@@ -299,9 +299,14 @@ record _≅[_]_
     inverses' : Inverses[ i .inverses ] to' from'
 
   open Inverses[_] inverses' public
+```
 
+<!--
+```agda
 open _≅[_]_ public
+{-# INLINE _≅[_]_.constructor #-}
 ```
+-->
 
 Since isomorphisms over the identity map will be of particular
 importance, we also define their own type: they are the _vertical
@@ -374,10 +379,8 @@ make-iso[_]
   → f' ∘' g' ≡[ iso .invl ] id'
   → g' ∘' f' ≡[ iso .invr ] id'
   → a' ≅[ iso ] b'
-make-iso[ inv ] f' g' p q .to' = f'
-make-iso[ inv ] f' g' p q .from' = g'
-make-iso[ inv ] f' g' p q .inverses' .Inverses[_].invl' = p
-make-iso[ inv ] f' g' p q .inverses' .Inverses[_].invr' = q
+{-# INLINE make-iso[_] #-}
+make-iso[ inv ] f' g' p q = record { to' = f' ; from' = g' ; inverses' = record { invl' = p ; invr' = q }}
 
 make-invertible[_]
   : ∀ {a b a' b'} {f : Hom a b} {f' : Hom[ f ] a' b'}

src/Cat/Displayed/Total.lagda.md

@@ -122,17 +122,17 @@ isomorphisms in $B$ and $E$.
 
   total-iso→iso : ∀ {x y} → x ∫E.≅ y → x .fst ≅ y .fst
   total-iso→iso f = make-iso
-      (∫E._≅_.to f .hom)
-      (∫E._≅_.from f .hom)
-      (ap hom $ ∫E._≅_.invl f)
-      (ap hom $ ∫E._≅_.invr f)
+    (∫E._≅_.to f .hom)
+    (∫E._≅_.from f .hom)
+    (ap hom $ ∫E._≅_.invl f)
+    (ap hom $ ∫E._≅_.invr f)
 
   total-iso→iso[] : ∀ {x y} → (f : x ∫E.≅ y) → x .snd ≅[ total-iso→iso f ] y .snd
   total-iso→iso[] f = make-iso[ total-iso→iso f ]
-      (∫E._≅_.to f .preserves)
-      (∫E._≅_.from f .preserves)
-      (ap preserves $ ∫E._≅_.invl f)
-      (ap preserves $ ∫E._≅_.invr f)
+    (∫E._≅_.to f .preserves)
+    (∫E._≅_.from f .preserves)
+    (ap preserves $ ∫E._≅_.invl f)
+    (ap preserves $ ∫E._≅_.invr f)
 ```
 
 ## Pullbacks in the total category