From b81cd4e48161c39aa903f6869a528fb3fe43aabb Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Mon, 8 Jun 2026 14:37:27 +0200
Subject: [PATCH 1/5] Add Properties of List actions on Bools

---
 src/Data/Bool/ListAction/Properties.agda | 86 ++++++++++++++++++++++++
 1 file changed, 86 insertions(+)
 create mode 100644 src/Data/Bool/ListAction/Properties.agda

diff --git a/src/Data/Bool/ListAction/Properties.agda b/src/Data/Bool/ListAction/Properties.agda
new file mode 100644
index 0000000000..9f7901f948
--- /dev/null
+++ b/src/Data/Bool/ListAction/Properties.agda
@@ -0,0 +1,86 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Booleans: properties of conjunction and disjunction of lists
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Bool.ListAction.Properties where
+
+open import Data.Bool.Base
+open import Data.Bool.Properties
+open import Data.Bool.ListAction
+open import Data.List.Base hiding (and; or; all; any)
+open import Data.List.Membership.Propositional using (_∈_)
+open import Data.List.Relation.Binary.Permutation.Propositional using (_↭_; ↭⇒↭ₛ)
+import Data.List.Relation.Binary.Permutation.Propositional.Properties as ↭
+open import Data.List.Relation.Binary.Permutation.Setoid.Properties
+open import Data.List.Relation.Unary.Any using (here; there)
+open import Relation.Binary.Core using (_Preserves_⟶_)
+open import Relation.Binary.PropositionalEquality.Core
+open import Relation.Binary.PropositionalEquality.Properties
+  using (module ≡-Reasoning)
+
+------------------------------------------------------------------------
+-- Properties
+
+-- and
+
+and-++ : ∀ bs cs → and (bs ++ cs) ≡ and bs ∧ and cs
+and-++ [] cs = refl
+and-++ (b ∷ bs) cs = begin
+  b ∧ and (bs ++ cs)    ≡⟨ cong (b ∧_) (and-++ bs cs) ⟩
+  b ∧ (and bs ∧ and cs) ≡⟨ ∧-assoc b (and bs) (and cs) ⟨
+  (b ∧ and bs) ∧ and cs ∎
+  where open ≡-Reasoning
+
+∨-distribˡ-and : ∀ b cs → b ∨ and cs ≡ all (b ∨_) cs
+∨-distribˡ-and b [] = ∨-zeroʳ b
+∨-distribˡ-and b (c ∷ cs) = trans (∨-distribˡ-∧ b c (and cs)) (cong ((b ∨ c) ∧_) (∨-distribˡ-and b cs))
+
+∨-distribʳ-and : ∀ b cs → and cs ∨ b ≡ all (_∨ b) cs
+∨-distribʳ-and b [] = ∨-zeroˡ b
+∨-distribʳ-and b (c ∷ cs) = trans (∨-distribʳ-∧ b c (and cs)) (cong ((c ∨ b) ∧_) (∨-distribʳ-and b cs))
+
+and-↭ : and Preserves _↭_ ⟶ _≡_
+and-↭ p = foldr-commMonoid ≡-setoid ∧-isCommutativeMonoid (↭⇒↭ₛ p)
+
+and-locate : ∀ bs → and bs ≡ false → false ∈ bs
+and-locate (false ∷ bs) p = here refl
+and-locate (true ∷ bs) p = there (and-locate bs p)
+
+-- or
+
+or-++ : ∀ bs cs → or (bs ++ cs) ≡ or bs ∨ or cs
+or-++ [] cs = refl
+or-++ (b ∷ bs) cs = begin
+  b ∨ or (bs ++ cs)   ≡⟨ cong (b ∨_) (or-++ bs cs) ⟩
+  b ∨ (or bs ∨ or cs) ≡⟨ ∨-assoc b (or bs) (or cs) ⟨
+  (b ∨ or bs) ∨ or cs ∎
+  where open ≡-Reasoning
+
+∧-distribˡ-or : ∀ b cs → b ∧ or cs ≡ any (b ∧_) cs
+∧-distribˡ-or b [] = ∧-zeroʳ b
+∧-distribˡ-or b (c ∷ cs) = trans (∧-distribˡ-∨ b c (or cs)) (cong ((b ∧ c) ∨_) (∧-distribˡ-or b cs))
+
+∧-distribʳ-or : ∀ b cs → or cs ∧ b ≡ any (_∧ b) cs
+∧-distribʳ-or b [] = ∧-zeroˡ b
+∧-distribʳ-or b (c ∷ cs) = trans (∧-distribʳ-∨ b c (or cs)) (cong ((c ∧ b) ∨_) (∧-distribʳ-or b cs))
+
+or-↭ : or Preserves _↭_ ⟶ _≡_
+or-↭ p = foldr-commMonoid ≡-setoid ∨-isCommutativeMonoid (↭⇒↭ₛ p)
+
+or-locate : ∀ bs → or bs ≡ true → true ∈ bs
+or-locate (false ∷ bs) p = there (or-locate bs p)
+or-locate (true ∷ bs) p = here p
+
+-- all
+
+all-↭ : ∀ {a} {A : Set a} (p : A → Bool) → all p Preserves _↭_ ⟶ _≡_
+all-↭ p xs↭ys = and-↭ (↭.map⁺ p xs↭ys)
+
+-- any
+
+any-↭ : ∀ {a} {A : Set a} (p : A → Bool) → any p Preserves _↭_ ⟶ _≡_
+any-↭ p xs↭ys = or-↭ (↭.map⁺ p xs↭ys)

From 2c2efdbd881b222bc30e0de626c74b73888cf295 Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Wed, 17 Jun 2026 07:50:25 +0200
Subject: [PATCH 2/5] Add changelog note

---
 CHANGELOG.md | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 98829d8e56..cc46fef801 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -89,6 +89,9 @@ New modules
 * `Codata.Guarded.Stream.Relation.Unary.Linked` for a proof that each pair
   of consecutive elements of a stream are related.
 
+* `Data.Bool.ListAction.Properties` for properties of conjunction and
+  disjuntion of lists.
+
 * A new type of lists that grow on the right.
   This is typically useful to model contexts of typing rules
   or type accumulators that need to be reversed in the base case.

From 184924c63138695eb87eeeb72e9dd5af12151811 Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Wed, 17 Jun 2026 14:57:39 +0200
Subject: [PATCH 3/5] Use function composition

---
 src/Data/Bool/ListAction/Properties.agda | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/Data/Bool/ListAction/Properties.agda b/src/Data/Bool/ListAction/Properties.agda
index 9f7901f948..1041c3b0b1 100644
--- a/src/Data/Bool/ListAction/Properties.agda
+++ b/src/Data/Bool/ListAction/Properties.agda
@@ -17,6 +17,7 @@ open import Data.List.Relation.Binary.Permutation.Propositional using (_↭_; 
 import Data.List.Relation.Binary.Permutation.Propositional.Properties as ↭
 open import Data.List.Relation.Binary.Permutation.Setoid.Properties
 open import Data.List.Relation.Unary.Any using (here; there)
+open import Function.Base using (_∘′_)
 open import Relation.Binary.Core using (_Preserves_⟶_)
 open import Relation.Binary.PropositionalEquality.Core
 open import Relation.Binary.PropositionalEquality.Properties
@@ -78,9 +79,9 @@ or-locate (true ∷ bs) p = here p
 -- all
 
 all-↭ : ∀ {a} {A : Set a} (p : A → Bool) → all p Preserves _↭_ ⟶ _≡_
-all-↭ p xs↭ys = and-↭ (↭.map⁺ p xs↭ys)
+all-↭ p = and-↭ ∘′ ↭.map⁺ p
 
 -- any
 
 any-↭ : ∀ {a} {A : Set a} (p : A → Bool) → any p Preserves _↭_ ⟶ _≡_
-any-↭ p xs↭ys = or-↭ (↭.map⁺ p xs↭ys)
+any-↭ p = or-↭ ∘′ ↭.map⁺ p

From e172c9ac3fc0a3acf5f4b3daaa8000830da78c16 Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Wed, 17 Jun 2026 14:57:53 +0200
Subject: [PATCH 4/5] Changelog typo

---
 CHANGELOG.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index cc46fef801..ef6c0b4657 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -90,7 +90,7 @@ New modules
   of consecutive elements of a stream are related.
 
 * `Data.Bool.ListAction.Properties` for properties of conjunction and
-  disjuntion of lists.
+  disjunction of lists.
 
 * A new type of lists that grow on the right.
   This is typically useful to model contexts of typing rules

From a624cbe58138c3c85fed13b0cb2ff8906acf622a Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Wed, 17 Jun 2026 19:25:36 +0200
Subject: [PATCH 5/5] without K

---
 src/Data/Bool/ListAction/Properties.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Bool/ListAction/Properties.agda b/src/Data/Bool/ListAction/Properties.agda
index 1041c3b0b1..7fd34e8260 100644
--- a/src/Data/Bool/ListAction/Properties.agda
+++ b/src/Data/Bool/ListAction/Properties.agda
@@ -4,7 +4,7 @@
 -- Booleans: properties of conjunction and disjunction of lists
 ------------------------------------------------------------------------
 
-{-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS --without-K --safe #-}
 
 module Data.Bool.ListAction.Properties where