From bc1d7950baa49a5d3542779275a6ed5c3ea46a62 Mon Sep 17 00:00:00 2001
From: Bradley Saul <bradleysaul@fastmail.com>
Date: Wed, 22 Oct 2025 13:20:26 -0400
Subject: [PATCH 1/3] add predicate pushforward

---
 src/Relation/Unary.agda | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/Relation/Unary.agda b/src/Relation/Unary.agda
index 86bb80f1bb..a36547affd 100644
--- a/src/Relation/Unary.agda
+++ b/src/Relation/Unary.agda
@@ -202,7 +202,7 @@ Decidable P = ∀ x → Dec (P x)
 -- Operations on sets
 
 infix 10 ⋃ ⋂
-infixr 9 _⊢_
+infixr 9 _⊢_ _⊣_
 infixr 8 _⇒_
 infixr 7 _∩_
 infixr 6 _∪_
@@ -266,6 +266,11 @@ P ⊥′ Q = P ∩ Q ⊆′ ∅
 _⊢_ : (A → B) → Pred B ℓ → Pred A ℓ
 f ⊢ P = λ x → P (f x)
 
+-- Pushforward.
+
+_⊣_ : (A → B) → Pred A ℓ → Pred B _
+f ⊣ P = λ b → ∃ λ a → f a ≡ b × P a
+
 ------------------------------------------------------------------------
 -- Predicate combinators
 

From 648d3a84f68d33357095e648891ee3d013d73d41 Mon Sep 17 00:00:00 2001
From: Bradley Saul <bradleysaul@fastmail.com>
Date: Wed, 22 Oct 2025 13:20:35 -0400
Subject: [PATCH 2/3] update changelog

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 12039b4aed..99616b2df2 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -180,6 +180,11 @@ Additions to existing modules
   contradiction′ : ¬ A → A → Whatever
   ```
 
+* In `Relation.Unary`
+  ```agda
+  _⊣_ : (A → B) → Pred A ℓ → Pred B _
+  ```
+
 * In `System.Random`:
   ```agda
   randomIO : IO Bool

From 7238414254147cdfb822d598efa9777e4597c211 Mon Sep 17 00:00:00 2001
From: Bradley Saul <bradleysaul@fastmail.com>
Date: Wed, 5 Nov 2025 12:38:35 -0500
Subject: [PATCH 3/3] update notation based on discussion

---
 CHANGELOG.md            |  3 ++-
 src/Relation/Unary.agda | 17 +++++++++++++----
 2 files changed, 15 insertions(+), 5 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 99616b2df2..c423a7ace8 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -182,7 +182,8 @@ Additions to existing modules
 
 * In `Relation.Unary`
   ```agda
-  _⊣_ : (A → B) → Pred A ℓ → Pred B _
+  ⟨_⟩⊢_ : (A → B) → Pred A ℓ → Pred B _
+  [_]⊢_ : (A → B) → Pred A ℓ → Pred B _
   ```
 
 * In `System.Random`:
diff --git a/src/Relation/Unary.agda b/src/Relation/Unary.agda
index a36547affd..f320da95a8 100644
--- a/src/Relation/Unary.agda
+++ b/src/Relation/Unary.agda
@@ -202,7 +202,7 @@ Decidable P = ∀ x → Dec (P x)
 -- Operations on sets
 
 infix 10 ⋃ ⋂
-infixr 9 _⊢_ _⊣_
+infixr 9 _⊢_ ⟨_⟩⊢_ [_]⊢_
 infixr 8 _⇒_
 infixr 7 _∩_
 infixr 6 _∪_
@@ -266,10 +266,19 @@ P ⊥′ Q = P ∩ Q ⊆′ ∅
 _⊢_ : (A → B) → Pred B ℓ → Pred A ℓ
 f ⊢ P = λ x → P (f x)
 
--- Pushforward.
+-- Diamond/Box
+-- These are specialization of Diamond/Box in
+-- Relation.Unary.Closure.Base.
 
-_⊣_ : (A → B) → Pred A ℓ → Pred B _
-f ⊣ P = λ b → ∃ λ a → f a ≡ b × P a
+-- Diamond
+
+⟨_⟩⊢_ : (A → B) → Pred A ℓ → Pred B _
+⟨ f ⟩⊢ P = λ b → ∃ λ a → f a ≡ b × P a
+
+-- Box
+
+[_]⊢_ : (A → B) → Pred A ℓ → Pred B _
+[ f ]⊢ P = λ b → ∀ a → f a ≡ b → P a
 
 ------------------------------------------------------------------------
 -- Predicate combinators