diff --git a/CHANGELOG.md b/CHANGELOG.md
index 12039b4aed..c423a7ace8 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -180,6 +180,12 @@ Additions to existing modules
   contradiction′ : ¬ A → A → Whatever
   ```
 
+* In `Relation.Unary`
+  ```agda
+  ⟨_⟩⊢_ : (A → B) → Pred A ℓ → Pred B _
+  [_]⊢_ : (A → B) → Pred A ℓ → Pred B _
+  ```
+
 * In `System.Random`:
   ```agda
   randomIO : IO Bool
diff --git a/src/Relation/Unary.agda b/src/Relation/Unary.agda
index 86bb80f1bb..532f7b9bca 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,20 @@ P ⊥′ Q = P ∩ Q ⊆′ ∅
 _⊢_ : (A → B) → Pred B ℓ → Pred A ℓ
 f ⊢ P = λ x → P (f x)
 
+-- Diamond/Box: for given `f`, these are the left- and right adjoints to `f ⊢_`
+-- These are specialization of Diamond/Box in
+-- Relation.Unary.Closure.Base.
+
+-- 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