chore: bump to Agda >2.6.4 (#270)

Had to make a few things more explicit since I fixed the freezing of metas in opaque blocks
the1lab · Oct 11, 2023 · c6e0c3c · c6e0c3c
1 parent 0763927
commit c6e0c3c
Show file tree

Hide file tree

Showing 4 changed files with 7 additions and 6 deletions.
diff --git a/src/Cat/Displayed/Comprehension.lagda.md b/src/Cat/Displayed/Comprehension.lagda.md
@@ -297,10 +297,10 @@ $\pi$.
 
 ```agda
   δᶜ′-cartesian : ∀ {Γ x} → is-cartesian E (δᶜ {Γ} {x}) δᶜ′
-  δᶜ′-cartesian = cart where
+  δᶜ′-cartesian {Γ = Γ} {x = x} = cart where
     open is-cartesian
 
-    cart : is-cartesian E _ _
+    cart : is-cartesian E (δᶜ {Γ} {x}) δᶜ′
     cart .universal m h′ = hom[ cancell proj-dup ] (πᶜ′ ∘′ h′)
     cart .commutes m h′ = cast[] $
       unwrapr _

diff --git a/src/Order/DCPO.lagda.md b/src/Order/DCPO.lagda.md
@@ -151,7 +151,7 @@ $$
       is-lub.fam≤lub fs-lub (lift true)
       where
 
-        s : Lift _ Bool → P.Ob
+        s : Lift o Bool → P.Ob
         s (lift b) = if b then x else y
 
         sx≤sfalse : ∀ b → s b P.≤ s (lift false)

diff --git a/support/nix/dep/Agda/github.json b/support/nix/dep/Agda/github.json
@@ -3,6 +3,6 @@
   "repo": "agda",
   "branch": "master",
   "private": false,
-  "rev": "632954bf442192276ca9c84ca95991d1ffc7a410",
-  "sha256": "1ab88xqjfqkid5g0hdxb1w35nwr6ykvrl79c142a5v474k3d18sg"
+  "rev": "5c8116227e2d9120267aed43f0e545a65d9c2fe2",
+  "sha256": "11q0fa087wik8k0badpvifan70n8x666z8mvvxwb1vb0cbzz3av3"
 }
diff --git a/support/shake/app/Shake/AgdaCompile.hs b/support/shake/app/Shake/AgdaCompile.hs
@@ -30,7 +30,8 @@ import Agda.Interaction.Options
 import Agda.Syntax.Common (Cubical(CFull))
 import Agda.Syntax.Common.Pretty
 import Agda.Syntax.TopLevelModuleName
-  ( TopLevelModuleName(..)
+  ( TopLevelModuleName'(..)
+  , TopLevelModuleName
   , RawTopLevelModuleName(..)
   , hashRawTopLevelModuleName
   )