chore: bump agda

Author: plt-amy

1lab.agda-lib

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

src/1Lab/HLevel.lagda.md

@@ -140,6 +140,12 @@ record is-contr {ℓ} (A : Type ℓ) : Type ℓ where
 open is-contr public
 ```
 
+<!--
+```agda
+{-# INLINE contr #-}
+```
+-->
+
 We can now write down the definition of `is-hlevel`{.Agda}, as a
 function of the type *and* the specific level. Note that, even though
 that being a proposition is equivalent to having contractible identity

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

@@ -152,15 +152,15 @@ paper, following the ring laws.
 
   open is-ring-hom
 
-  z-natdiff : ∀ x y → ℤ↪R (x ℕ- y) ≡ e x R.- e y
-  z-natdiff x zero = R.intror R.inv-unit
-  z-natdiff zero (suc y) = R.introl refl
-  z-natdiff (suc x) (suc y) = z-natdiff x y ∙ e-tr x y
+  z-nat-diff : ∀ x y → ℤ↪R (x ℕ- y) ≡ e x R.- e y
+  z-nat-diff x zero = R.intror R.inv-unit
+  z-nat-diff zero (suc y) = R.introl refl
+  z-nat-diff (suc x) (suc y) = z-nat-diff x y ∙ e-tr x y
 
   z-add : ∀ x y → ℤ↪R (x +ℤ y) ≡ ℤ↪R x R.+ ℤ↪R y
   z-add (pos x) (pos y) = e-add x y
-  z-add (pos x) (negsuc y) = z-natdiff x (suc y)
-  z-add (negsuc x) (pos y) = z-natdiff y (suc x) ∙ R.+-commutes
+  z-add (pos x) (negsuc y) = z-nat-diff x (suc y)
+  z-add (negsuc x) (pos y) = z-nat-diff y (suc x) ∙ R.+-commutes
   z-add (negsuc x) (negsuc y) =
     R.- (e 1 R.+ e (suc x Nat.+ y))         ≡⟨ ap R.-_ (ap₂ R._+_ refl (e-add (suc x) y) ∙ R.extendl R.+-commutes) ⟩
     R.- (e (suc x) R.+ (e 1 R.+ e y))       ≡⟨ R.a.inv-comm ⟩

src/Data/Finset/Properties.agda

@@ -17,7 +17,9 @@ private variable
   ℓ ℓ' ℓ'' : Level
   A B C : Type ℓ
 
-∈ᶠˢ-map : (f : A → B) {x : B} (xs : Finset A) → x ∈ mapᶠˢ f xs → ∃[ (y , _) ∈ fibreᵢ f x ] y ∈ xs
+∈ᶠˢ-map
+  : {A : Type ℓ} {B : Type ℓ'} (f : A → B) {x : B}
+  → (xs : Finset A) → x ∈ mapᶠˢ f xs → ∃[ (y , _) ∈ fibreᵢ f x ] y ∈ xs
 ∈ᶠˢ-map f {x} xs w = Finset-elim-prop (λ xs → x ∈ mapᶠˢ f xs → ∃[ (y , _) ∈ fibreᵢ f x ] y ∈ xs)
   (λ w → absurd (¬mem-[] w))
   (λ y ind → ∈ᶠˢ-split (λ { p → inc ((y , symᵢ p) , hereₛ) }) λ w → case ind w of λ x p h → inc ((x , p) , thereₛ h))

src/Data/Int/Order.lagda.md

@@ -253,6 +253,9 @@ abstract
   *ℤ-cancel-≤r {possuc x} {y = negsuc y} {negsuc z} ⦃ pos _ ⦄ p = neg≤neg
     (Nat.*-cancel-≤r (suc x) (Nat.+-reflects-≤l (z * suc x) (y * suc x) x (unneg≤neg p)))
 
+  *ℤ-cancel-≤l : ∀ {x y z} ⦃ _ : Positive x ⦄ → (x *ℤ y) ≤ (x *ℤ z) → y ≤ z
+  *ℤ-cancel-≤l {x} {y} {z} p = *ℤ-cancel-≤r {x} {y} {z} (≤-trans (≤-refl' (*ℤ-commutative y x)) (≤-trans p (≤-refl' (*ℤ-commutative x z))))
+
   *ℤ-preserves-≤r : ∀ {x y} z ⦃ _ : Positive z ⦄ → x ≤ y → (x *ℤ z) ≤ (y *ℤ z)
   *ℤ-preserves-≤r {pos x} {pos y} (possuc z) ⦃ pos z ⦄ p = apos≤apos {x * suc z} {y * suc z} (Nat.*-preserves-≤r x y (suc z) (unpos≤pos p))
   *ℤ-preserves-≤r {negsuc x} {pos y} (possuc z) ⦃ pos z ⦄ p = ≤-trans neg≤pos (≤-refl' (sym (assign-pos (y * suc z))))

src/Data/Rational/Base.lagda.md

@@ -96,9 +96,8 @@ _*ℚ_ (inc x) (inc y) = inc (x L.*ₗ y)
 -- The requirement of having a proper match means we can't use a record
 -- (even a no-eta pattern record), since Agda doesn't count those as
 -- proper. Therefore, we have to use a data type.
-private
-  unℚ : ℚ → ⌞ L.S⁻¹R ⌟
-  unℚ (inc x) = x
+unℚ : ℚ → ⌞ L.S⁻¹R ⌟
+unℚ (inc x) = x
 ```
 -->
 

src/Data/Rational/Order.lagda.md

@@ -383,6 +383,12 @@ abstract
   ... | inl x=y = absurd (x≠y x=y)
   ... | inr x<y = x<y
 
+  *ℚ-cancel-<l : ∀ {x y r} ⦃ _ : Positive r ⦄ → (r *ℚ x) < (r *ℚ y) → x < y
+  unquoteDef *ℚ-cancel-<l = do
+    by-elim-ℚ *ℚ-cancel-<l λ d x y r ⦃ rpos ⦄ α →
+      let instance _ = rpos .lower in
+      common-denom-< (ℤ.*ℤ-cancel-<l {x = r} (<-common-denom ⦃ _ ⦄ α))
+
 absℚ : ℚ → ℚ
 absℚ (inc x) = ℚ.inc $ ℚ-rec absᶠ absᶠ-resp (inc x) where
   absᶠ : Fraction → _

src/Data/Rational/Properties.lagda.md

@@ -3,6 +3,7 @@
 open import 1Lab.Prelude
 
 open import Algebra.Ring.Commutative
+open import Algebra.Ring.Solver
 open import Algebra.Monoid
 
 open import Data.Rational.Reflection
@@ -14,7 +15,7 @@ import Algebra.Ring.Reasoning as Kit
 
 import Data.Int.Properties as ℤ
 import Data.Int.Order as ℤ
-import Data.Int.Base as ℤ
+import Data.Int.Base as ℤ renaming (_+ℤ_ to _+_ ; _-ℤ_ to _-_ ; _*ℤ_ to _*_)
 ```
 -->
 
@@ -26,6 +27,8 @@ module Data.Rational.Properties where
 
 <!--
 ```agda
+open Explicit ℤ-comm
+
 private module ℚr = Kit (ℚ-ring .fst , record { CRing-on (ℚ-ring .snd) })
 open ℚr renaming (*-negater to *ℚ-negater ; *-negatel to *ℚ-negatel) using () public
 
@@ -173,6 +176,17 @@ abstract
       ∙ /ℚ-scaler ∙ ap (λ e → e /ℚ d) (*ℚ-associative _ _ d) ∙ /ℚ-factorr)
 ```
 
+## Operations with same denominator
+
+```agda
+abstract
+  +ℚ-common-denom : ∀ d x y ⦃ _ : ℤ.Positive d ⦄ → (x / d) +ℚ (y / d) ≡ (x ℤ.+ y) / d
+  +ℚ-common-denom d x y = ext (solve 3 (λ x y d → ((x :* d) :+ (y :* d)) :* d ≔ (x :+ y) :* (d :* d)) x y d refl)
+
+  -ℚ-common-denom : ∀ d x y ⦃ _ : ℤ.Positive d ⦄ → (x / d) -ℚ (y / d) ≡ (x ℤ.- y) / d
+  -ℚ-common-denom d x y = ext (solve 3 (λ x y d → ((x :* d) :+ ((:- y) :* d)) :* d ≔ (x :+ (:- y)) :* (d :* d)) x y d refl)
+```
+
 ## Positivity
 
 ```agda
@@ -189,8 +203,8 @@ abstract
       d@(ℤ.possuc d') ⦃ ℤ.pos .d' ⦄ (ℤ.possuc x) px → inc (ℤ.pos d')
 
     by-elim-ℚ +ℚ-nonneg-positive λ where
-      d (ℤ.posz) b (inc x) (inc y) → inc (subst ℤ.Positive (sym (ℤ.+ℤ-zerol (b ℤ.*ℤ d))) (ℤ.*ℤ-positive y auto))
-      d (ℤ.possuc a) b (inc x) (inc y) → inc (ℤ.+ℤ-positive {ℤ.possuc a ℤ.*ℤ d} {b ℤ.*ℤ d} (ℤ.*ℤ-positive (ℤ.pos a) auto) (ℤ.*ℤ-positive y auto))
+      d (ℤ.posz) b (inc x) (inc y) → inc (subst ℤ.Positive (sym (ℤ.+ℤ-zerol (b ℤ.* d))) (ℤ.*ℤ-positive y auto))
+      d (ℤ.possuc a) b (inc x) (inc y) → inc (ℤ.+ℤ-positive {ℤ.possuc a ℤ.* d} {b ℤ.* d} (ℤ.*ℤ-positive (ℤ.pos a) auto) (ℤ.*ℤ-positive y auto))
 
   /ℚ-positive : ∀ {x y} (p : Positive x) (q : Positive y) → Positive ((x /ℚ y) ⦃ inc (positive→nonzero q) ⦄)
   /ℚ-positive {y = y} p q = subst Positive

support/nix/dep/Agda/github.json

@@ -3,6 +3,6 @@
   "repo": "agda",
   "branch": "master",
   "private": false,
-  "rev": "3bcf0086b1ac20f6900ba270510b28f0b25406a9",
-  "sha256": "191mr86zkd402spl66sjwsrq1f9k0l31zwjdw1f04sm61xs5kiwf"
+  "rev": "93af60bf20f1d2887b2642e2297f99f3c18035f3",
+  "sha256": "15pmlg8zhaxfp1w20mplqvn425drb90bcslqvn3j1nf4wlcnchjs"
 }

support/shake/app/Shake/AgdaCompile.hs

@@ -28,7 +28,7 @@ import Agda.Interaction.FindFile (SourceFile(..))
 import Agda.TypeChecking.Monad.Base (srcFromPath)
 import Agda.TypeChecking.Pretty.Warning
 import Agda.TypeChecking.Errors
-import Agda.Interaction.Imports
+import Agda.Interaction.Imports hiding (getInterface)
 import Agda.Interaction.Options
 import Agda.Syntax.Common (Cubical(CFull))
 import Agda.Syntax.Common.Pretty