From 67219ba84726ca83a91e3135f1c1f6e813f8adce Mon Sep 17 00:00:00 2001
From: jmchapman <james.chapman@iohk.io>
Date: Thu, 23 Apr 2026 12:59:22 +0100
Subject: [PATCH 1/7] bump agda + std-lib CI pin

---
 .github/workflows/agda-ci.yml | 4 ++--
 src/Main.agda-lib             | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/agda-ci.yml b/.github/workflows/agda-ci.yml
index 48531c4..3aee5ce 100644
--- a/.github/workflows/agda-ci.yml
+++ b/.github/workflows/agda-ci.yml
@@ -25,7 +25,7 @@ jobs:
         # - os: windows-latest
         #   agda: 2.6.2.2
         - os: ubuntu-latest
-          agda: 2.6.3
+          agda: 2.6.4
 
     steps:
 
@@ -38,7 +38,7 @@ jobs:
         with:
           agda-version: ${{ matrix.agda }}
           # agda-stdlib-version: recommended
-          agda-stdlib-version: '1.7.1'
+          agda-stdlib-version: '1.7.3'
           # agda-stdlib-default: true
 
       - name: Cache build
diff --git a/src/Main.agda-lib b/src/Main.agda-lib
index 70d4b8f..8af7e33 100644
--- a/src/Main.agda-lib
+++ b/src/Main.agda-lib
@@ -1,3 +1,3 @@
 include: .
-depend: standard-library-1.7.1
+depend: standard-library-1.7.3
 flags: --sized-types
\ No newline at end of file

From d57dc418e5c1c5d330503874a0325a64c6199811 Mon Sep 17 00:00:00 2001
From: jmchapman <james.chapman@iohk.io>
Date: Thu, 23 Apr 2026 13:03:55 +0100
Subject: [PATCH 2/7] bump action versions

---
 .github/workflows/agda-ci.yml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/agda-ci.yml b/.github/workflows/agda-ci.yml
index 3aee5ce..6a9e520 100644
--- a/.github/workflows/agda-ci.yml
+++ b/.github/workflows/agda-ci.yml
@@ -30,7 +30,7 @@ jobs:
     steps:
 
       # Checkout to $HOME empties $HOME so we have to do it before we put stuff there.
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
 
       - name: Setup Agda
         uses: wenkokke/setup-agda@latest
@@ -42,7 +42,7 @@ jobs:
           # agda-stdlib-default: true
 
       - name: Cache build
-        uses: actions/cache@v3
+        uses: actions/cache@v4
         id:   cache
         with:
           key: ${{ runner.os }}-agda-${{ steps.setup.outputs.agda-version }}
@@ -57,7 +57,7 @@ jobs:
         working-directory: src
         run: agda Everything.agda --html
 
-      - uses: actions/upload-pages-artifact@v1
+      - uses: actions/upload-pages-artifact@v3
         with:
           path: src/html
 

From 1bbf87fa2fc512a1df1a2dc5f3e10aa69501e659 Mon Sep 17 00:00:00 2001
From: jmchapman <james.chapman@iohk.io>
Date: Thu, 23 Apr 2026 14:43:20 +0100
Subject: [PATCH 3/7] further bump to agda 2.8.0 and std-lib 2.3

---
 .github/workflows/agda-ci.yml |  4 ++--
 flake.nix                     | 16 ++++++++++++++++
 src/Main.agda-lib             |  2 +-
 3 files changed, 19 insertions(+), 3 deletions(-)
 create mode 100644 flake.nix

diff --git a/.github/workflows/agda-ci.yml b/.github/workflows/agda-ci.yml
index 6a9e520..2094fe0 100644
--- a/.github/workflows/agda-ci.yml
+++ b/.github/workflows/agda-ci.yml
@@ -25,7 +25,7 @@ jobs:
         # - os: windows-latest
         #   agda: 2.6.2.2
         - os: ubuntu-latest
-          agda: 2.6.4
+          agda: 2.8.0
 
     steps:
 
@@ -38,7 +38,7 @@ jobs:
         with:
           agda-version: ${{ matrix.agda }}
           # agda-stdlib-version: recommended
-          agda-stdlib-version: '1.7.3'
+          agda-stdlib-version: '2.3'
           # agda-stdlib-default: true
 
       - name: Cache build
diff --git a/flake.nix b/flake.nix
new file mode 100644
index 0000000..865e89d
--- /dev/null
+++ b/flake.nix
@@ -0,0 +1,16 @@
+{
+    description = "Continuous normalization";
+
+    inputs.nixpkgs.url = "github:NixOS/nixpkgs/nixpkgs-unstable";
+
+    outputs = { self, nixpkgs }:
+      let
+        system = "x86_64-linux";
+        pkgs = nixpkgs.legacyPackages.${system};
+        agda = pkgs.agda.withPackages (p: [ p.standard-library ]);
+      in {
+        devShells.${system}.default = pkgs.mkShell {
+          buildInputs = [ agda ];
+        };
+      };
+}
diff --git a/src/Main.agda-lib b/src/Main.agda-lib
index 8af7e33..4be4657 100644
--- a/src/Main.agda-lib
+++ b/src/Main.agda-lib
@@ -1,3 +1,3 @@
 include: .
-depend: standard-library-1.7.3
+depend: standard-library-2.3
 flags: --sized-types
\ No newline at end of file

From 4485b53df723351bd4774e1b9e55ee14990e38da Mon Sep 17 00:00:00 2001
From: jmchapman <james.chapman@iohk.io>
Date: Thu, 23 Apr 2026 14:43:54 +0100
Subject: [PATCH 4/7] src fixes for agda 2.8.0+std-lib 2.3

---
 src/Delay.agda   | 16 +++++++++-------
 src/Library.agda |  4 ++--
 2 files changed, 11 insertions(+), 9 deletions(-)

diff --git a/src/Delay.agda b/src/Delay.agda
index cc7d20a..5973db5 100644
--- a/src/Delay.agda
+++ b/src/Delay.agda
@@ -1,10 +1,11 @@
 module Delay where
 
 open import Library
-open import Category.Applicative.Indexed
+open import Effect.Applicative.Indexed
+import Effect.Monad
 -- Coinductive delay monad.
 
-infix 10 _⇓_
+-- infix 10 _⇓_
 
 mutual
 
@@ -45,14 +46,15 @@ module Bind where
     force (x ∞>>= f) = force x >>= f
 
 delayMonad : ∀ {i} → RawMonad {f = lzero} (Delay i)
-delayMonad {i} = record
+delayMonad {i} = Effect.Monad.mkRawMonad (Delay i) now (_>>=_ {i}) where open Bind -- mkRawMonad return _>>=_
+{-delayMonad {i} = record
   { return = now
   ; _>>=_  = _>>=_ {i}
   } where open Bind
-
+-}
 module _ {i : Size} where
   open module DelayMonad = RawMonad (delayMonad {i = i})
-                           public renaming (_⊛_ to _<*>_)
+                           public
 open Bind public using (_∞>>=_)
 
 -- Map for ∞Delay
@@ -70,7 +72,6 @@ _=<<2_,_ : ∀ {i A B C} → (A → B → Delay i C) → Delay i A → Delay i B
 f =<<2 x , y = x >>= λ a → y >>= λ b → f a b
 
 -- Lifting a predicate to Delay (without convergence).
-
 mutual
   data Delay₁ i {A : Set} (P : A → Set) : Delay ∞ A → Set where
     now₁   : ∀{a}  → (p : P a) → Delay₁ i P (now a)
@@ -184,7 +185,7 @@ module ≈-Reasoning {i : Size} {A : Set} where
 
 module ∞≈-Reasoning {i : Size} {A : Set} where
   private module M = SetoidReasoning (∞≈setoid i A)
-  open M public using (begin_; _∎; _≡⟨⟩_; step-≡)
+  open M public using (begin_; _∎; step-≡-∣; step-≡)
   step-∞≈ = M.step-≈
   infixr 2 step-∞≈
   syntax step-∞≈ x y≈z x≈y = x ∞≈⟨ x≈y ⟩ y≈z
@@ -503,3 +504,4 @@ lifta2lem2 f g h a b = begin
   (((a >>= (now ∘ g)) >>= (now ∘ f)) >>= (λ f' → b >>= (now ∘ h) >>= now ∘ f'))
   ∎
   where open ≈-Reasoning
+-- -}
diff --git a/src/Library.agda b/src/Library.agda
index 175e3b1..a0b4168 100644
--- a/src/Library.agda
+++ b/src/Library.agda
@@ -3,14 +3,14 @@
 module Library where
 
 open import Function public
-  hiding (_∋_)
+  hiding (_∋_; force)
 
 open import Level public
   using (Level) renaming (zero to lzero; suc to lsuc)
 
 open import Size public
 
-open import Category.Monad public
+open import Effect.Monad public
   using (RawMonad; module RawMonad)
 
 open import Data.Empty public

From 7e9f0aa2efafe98cb3e741c03bc469c44d773440 Mon Sep 17 00:00:00 2001
From: jmchapman <james.chapman@iohk.io>
Date: Thu, 23 Apr 2026 15:28:52 +0100
Subject: [PATCH 5/7] switched to Andreas' runner

---
 .github/workflows/agda-ci.yml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/.github/workflows/agda-ci.yml b/.github/workflows/agda-ci.yml
index 2094fe0..293859f 100644
--- a/.github/workflows/agda-ci.yml
+++ b/.github/workflows/agda-ci.yml
@@ -33,19 +33,17 @@ jobs:
       - uses: actions/checkout@v4
 
       - name: Setup Agda
-        uses: wenkokke/setup-agda@latest
+        uses: agda/agda-setup-action@v1
         id:   setup
         with:
           agda-version: ${{ matrix.agda }}
-          # agda-stdlib-version: recommended
           agda-stdlib-version: '2.3'
-          # agda-stdlib-default: true
 
       - name: Cache build
         uses: actions/cache@v4
         id:   cache
         with:
-          key: ${{ runner.os }}-agda-${{ steps.setup.outputs.agda-version }}
+          key: ${{ runner.os }}-agda-${{ matrix.agda }}
           # Don't have version of standard library. :-(
           # -std-lib-${{ matrix.std-lib }}
           path: |

From f5748bb1dffc6b2a2e48cb62006ad99ac9c6f4e5 Mon Sep 17 00:00:00 2001
From: jmchapman <james.chapman@iohk.io>
Date: Thu, 23 Apr 2026 15:46:42 +0100
Subject: [PATCH 6/7] removed some commented out stuff

---
 src/Delay.agda | 9 ++-------
 1 file changed, 2 insertions(+), 7 deletions(-)

diff --git a/src/Delay.agda b/src/Delay.agda
index 5973db5..ce470a1 100644
--- a/src/Delay.agda
+++ b/src/Delay.agda
@@ -46,12 +46,8 @@ module Bind where
     force (x ∞>>= f) = force x >>= f
 
 delayMonad : ∀ {i} → RawMonad {f = lzero} (Delay i)
-delayMonad {i} = Effect.Monad.mkRawMonad (Delay i) now (_>>=_ {i}) where open Bind -- mkRawMonad return _>>=_
-{-delayMonad {i} = record
-  { return = now
-  ; _>>=_  = _>>=_ {i}
-  } where open Bind
--}
+delayMonad {i} = Effect.Monad.mkRawMonad (Delay i) now (_>>=_ {i}) where open Bind
+
 module _ {i : Size} where
   open module DelayMonad = RawMonad (delayMonad {i = i})
                            public
@@ -504,4 +500,3 @@ lifta2lem2 f g h a b = begin
   (((a >>= (now ∘ g)) >>= (now ∘ f)) >>= (λ f' → b >>= (now ∘ h) >>= now ∘ f'))
   ∎
   where open ≈-Reasoning
--- -}

From 13ce327d205d8acc94d3a4834a6899a365458dc5 Mon Sep 17 00:00:00 2001
From: jmchapman <james.chapman@iohk.io>
Date: Thu, 23 Apr 2026 15:49:42 +0100
Subject: [PATCH 7/7] added flake.lock to .gitignore

---
 .gitignore | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.gitignore b/.gitignore
index 129a373..3169db5 100644
--- a/.gitignore
+++ b/.gitignore
@@ -32,3 +32,4 @@
 *.tdo
 *.agdai
 *~
+flake.lock
\ No newline at end of file