Update to Agda 2.7 (#564)

default.nix

@@ -40,12 +40,12 @@ let
   agdaStdlibMeta = customAgda.agdaPackages.mkDerivation {
     inherit (locales) LANG LC_ALL LOCALE_ARCHIVE;
     pname = "agda-stdlib-meta";
-    version = "2.0";
+    version = "2.1.1";
     src = fetchFromGitHub {
       repo = "stdlib-meta";
-      owner = "input-output-hk";
-      rev = "4fc4b1ed6e47d180516917d04be87cbacbf7d314";
-      sha256 = "T+9vwccbDO1IGBcGLjgV/fOt+IN14KEV9ct/J6nQCsM=";
+      owner = "omelkonian";
+      rev = "v2.1.1";
+      sha256 = "qOoThYMG0dzjKvwmzzVZmGcerfb++MApbaGRzLEq3/4=";
     };
     meta = { };
     libraryFile = "agda-stdlib-meta.agda-lib";

nix/sources.json

@@ -5,10 +5,10 @@
         "homepage": "",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "7148a46c2a1163faecb2915f5f1e6e6c43bcd3ee",
-        "sha256": "1aygdbj86xiyalgy21xk4gzgvjphhm7dr0ni1j4n32rmziwr4r97",
+        "rev": "7438ebd9431243aa0b01502fae89c022e4facb0c",
+        "sha256": "0vp87mp4zjxsxji5h8wjlj4agr82cnk3fbjrz265g340446m2bqq",
         "type": "tarball",
-        "url": "https://github.com/NixOS/nixpkgs/archive/7148a46c2a1163faecb2915f5f1e6e6c43bcd3ee.tar.gz",
+        "url": "https://github.com/NixOS/nixpkgs/archive/7438ebd9431243aa0b01502fae89c022e4facb0c.tar.gz",
         "url_template": "https://github.com/<owner>/<repo>/archive/<rev>.tar.gz"
     },
     "nixpkgs": {

src/Axiom/Set/Properties.agda

@@ -185,7 +185,7 @@ map-∪ {X = X} {Y} f = from ≡ᵉ⇔≡ᵉ' λ b →
     (∃[ a ] b ≡ f a × (a ∈ X ⊎ a ∈ Y))
       ↔⟨ ∃-cong′ ×-distribˡ-⊎' ⟩
     (∃[ a ] (b ≡ f a × a ∈ X ⊎ b ≡ f a × a ∈ Y))
-      ↔⟨ ∃-distrib-⊎' ⟩
+      ↔⟨ ∃-distrib-⊎ ⟩
     (∃[ a ] b ≡ f a × a ∈ X ⊎ ∃[ a ] b ≡ f a × a ∈ Y)
       ∼⟨ ∈-map ⊎-cong ∈-map ⟩
     (b ∈ map f X ⊎ b ∈ map f Y)

src/Axiom/Set/Rel.agda

@@ -17,7 +17,7 @@ open import Data.List.Ext.Properties using (_⊎-cong_)
 open import Data.These hiding (map)
 open import Data.Maybe.Base using () renaming (map to map?)
 open import Data.Product.Properties using (,-injectiveˡ; ×-≡,≡→≡)
-open import Data.Product.Properties.Ext using (∃-cong′; ∃-distrib-⊎')
+open import Data.Product.Properties.Ext using (∃-cong′; ∃-distrib-⊎)
 open import Relation.Unary using (Decidable)
 open import Relation.Nullary using (yes; no)
 open import Relation.Binary using (_Preserves_⟶_)
@@ -118,7 +118,7 @@ dom∪ : dom (R ∪ R') ≡ᵉ dom R ∪ dom R'
 dom∪ {R = R} {R'} = from ≡ᵉ⇔≡ᵉ' λ a →
   a ∈ dom (R ∪ R')                           ∼⟨ R.SK-sym dom∈ ⟩
   (∃[ b ] (a , b) ∈ R ∪ R')                  ∼⟨ ∃-cong′ (R.SK-sym ∈-∪) ⟩
-  (∃[ b ] ((a , b) ∈ R ⊎ (a , b) ∈ R'))      ↔⟨ ∃-distrib-⊎' ⟩
+  (∃[ b ] ((a , b) ∈ R ⊎ (a , b) ∈ R'))      ↔⟨ ∃-distrib-⊎ ⟩
   (∃[ b ] (a , b) ∈ R ⊎ ∃[ b ] (a , b) ∈ R') ∼⟨ dom∈ ⊎-cong dom∈ ⟩
   (a ∈ dom R ⊎ a ∈ dom R')                   ∼⟨ ∈-∪ ⟩
   a ∈ dom R ∪ dom R'                         ∎

src/Data/Product/Properties/Ext.agda

@@ -3,7 +3,7 @@
 module Data.Product.Properties.Ext where
 
 open import Data.Product
-open import Data.Product.Function.Dependent.Propositional using (cong)
+open import Data.Product.Function.Dependent.Propositional renaming (cong to ∃-cong)
 open import Function
 open import Function.Related.Propositional
 open import Level
@@ -13,38 +13,29 @@ open import Data.Sum.Base
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 
 private variable
-  ℓ : Level
+  ℓ ℓ′ : Level
   A B C : Set ℓ
   a a₁ a₂ b₁ b₂ : Level
   k : Kind
 
-∃-cong : {A₁ : Set a₁} {A₂ : Set a₂} {B₁ : A₁ → Set b₁} {B₂ : A₂ → Set b₂} (A₁↔A₂ : A₁ ↔ A₂)
-       → (∀ {x} → B₁ x ∼[ k ] B₂ (Inverse.to A₁↔A₂ x))
-       → Σ A₁ B₁ ∼[ k ] Σ A₂ B₂
-∃-cong A₁↔A₂ h = cong A₁↔A₂ h
-
 ∃-cong′ : {A : Set a} {B₁ : A → Set b₁} {B₂ : A → Set b₂}
         → (∀ {x} → B₁ x ∼[ k ] B₂ x)
         → Σ A B₁ ∼[ k ] Σ A B₂
-∃-cong′ h = ∃-cong (mk↔ (id , id)) h
+∃-cong′ = ∃-cong (mk↔ (id , id))
 
 ∃-≡ : ∀ {A : Set a₁} (P : A → Set a₂) {x} → P x ⇔ (∃[ y ] y ≡ x × P y)
 ∃-≡ P {x} = mk⇔ (λ Px → x , refl , Px) (λ where (y , (refl , Py)) → Py)
 
--- the version in Function.Related.TypeIsomorphisms isn't level-polymorphic enough
-×-distribˡ-⊎' : (A × (B ⊎ C)) ↔ (A × B ⊎ A × C)
-×-distribˡ-⊎' = mk↔ₛ′
+∃-distrib-⊎ : {P : A → Set ℓ} {Q : A → Set ℓ′} → (∃[ a ] (P a ⊎ Q a)) ↔ (∃[ a ] P a ⊎ ∃[ a ] Q a)
+∃-distrib-⊎ = mk↔ₛ′
   (uncurry λ x → [ inj₁ ∘′ (x ,_) , inj₂ ∘′ (x ,_) ]′)
   [ Prod.map₂ inj₁ , Prod.map₂ inj₂ ]′
   [ (λ _ → P.refl) , (λ _ → P.refl) ]
   (uncurry λ _ → [ (λ _ → P.refl) , (λ _ → P.refl) ])
 
-∃-distrib-⊎' : {P Q : A → Set ℓ} → (∃[ a ] (P a ⊎ Q a)) ↔ (∃[ a ] P a ⊎ ∃[ a ] Q a)
-∃-distrib-⊎' = mk↔ₛ′
-  (uncurry λ x → [ inj₁ ∘′ (x ,_) , inj₂ ∘′ (x ,_) ]′)
-  [ Prod.map₂ inj₁ , Prod.map₂ inj₂ ]′
-  [ (λ _ → P.refl) , (λ _ → P.refl) ]
-  (uncurry λ _ → [ (λ _ → P.refl) , (λ _ → P.refl) ])
+-- the version in Function.Related.TypeIsomorphisms isn't level-polymorphic enough
+×-distribˡ-⊎' : (A × (B ⊎ C)) ↔ (A × B ⊎ A × C)
+×-distribˡ-⊎' = ∃-distrib-⊎
 
 ×-⇔-swap : (A × B × C) ⇔ (B × A × C)
 ×-⇔-swap {A = A}{B = B}{C = C} = let open EquationalReasoning in

src/Ledger/Utxo/Properties.lagda

@@ -38,6 +38,7 @@ module Ledger.Utxo.Properties
 
 open import Ledger.Utxo txs abs
 open import Ledger.ScriptValidation txs abs
+open import Algebra.Definitions.RawMagma +-rawMagma using () renaming (_,_ to _,≤_)
 
 instance
   _ = TokenAlgebra.Value-CommutativeMonoid tokenAlgebra
@@ -341,7 +342,7 @@ module DepositHelpers
 
   ref≤dep : ref ≤ dep
   ref≤dep with ref ≟ 0
-  ... | no ¬p = ≤″⇒≤ $ ℕ.less-than-or-equal $ begin
+  ... | no ¬p = ≤″⇒≤ $ _ ,≤_ $ begin
     ref + uDep ≡⟨ +-comm ref uDep ⟩
     uDep + ref ≡⟨ dep-ref $ ref-tot-0 ¬p ⟩
     dep        ∎

src/checkTypeChecked.sh

@@ -2,7 +2,7 @@
 
 echo "Checking that all Agda files have been typechecked..."
 for agdaFn in $(find . -name '*.*agda'); do
-  agdaiFn="_build/2.6.4.3/agda/${agdaFn%.*agda}.agdai"
+  agdaiFn="_build/2.7.0/agda/${agdaFn%.*agda}.agdai"
   if [ "$(( $(stat -c "%Y" $agdaiFn) - $(stat -c "%Y" $agdaFn) ))" -lt "0" ]; then
     echo "        FAIL: $agdaiFn is not up-to-date"
     exit 1