diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3eb803ac39..c3e04267d8 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -244,6 +244,17 @@ Additions to existing modules
   [_]⊢_ : (A → B) → Pred A ℓ → Pred B _
   ```
 
+* In `Relation.Unary.Properties`
+  ```agda
+  _map-⊢_   : P ⊆ Q → f ⊢ P ⊆ f ⊢ Q
+  map-⟨_⟩⊢_ : P ⊆ Q → ⟨ f ⟩⊢ P ⊆ ⟨ f ⟩⊢ Q
+  map-[_]⊢_ : P ⊆ Q → [ f ]⊢ P ⊆ [ f ]⊢ Q
+  ⟨_⟩⊢⁻_    : ⟨ f ⟩⊢ P ⊆ Q → P ⊆ f ⊢ Q
+  ⟨_⟩⊢⁺_    : P ⊆ f ⊢ Q → ⟨ f ⟩⊢ P ⊆ Q
+  [_]⊢⁻_    : Q ⊆ [ f ]⊢ P → f ⊢ Q ⊆ P
+  [_]⊢⁺_    : f ⊢ Q ⊆ P → Q ⊆ [ f ]⊢ P
+  ```
+
 * In `System.Random`:
   ```agda
   randomIO : IO Bool
diff --git a/src/Function/Related/TypeIsomorphisms.agda b/src/Function/Related/TypeIsomorphisms.agda
index b1549ef14d..1f7e0d7110 100644
--- a/src/Function/Related/TypeIsomorphisms.agda
+++ b/src/Function/Related/TypeIsomorphisms.agda
@@ -39,6 +39,7 @@ open import Relation.Binary.PropositionalEquality.Properties
   using (module ≡-Reasoning)
 open import Relation.Nullary.Negation.Core using (¬_)
 import Relation.Nullary.Indexed as I
+open import Relation.Unary.Properties using (⟨_⟩⊢⁻_; ⟨_⟩⊢⁺_)
 
 private
   variable
@@ -360,6 +361,6 @@ Related-cong {A = A} {B = B} {C = C} {D = D} A≈B C≈D = mk⇔
 -- restriction that the quantified variable is equal to the given one
 
 ∃-≡ : ∀ (P : A → Set b) {x} → P x ↔ (∃[ y ] y ≡ x × P y)
-∃-≡ P {x} = mk↔ₛ′ (λ Px → x , refl , Px) (λ where (_ , refl , Py) → Py)
+∃-≡ P {x} = mk↔ₛ′ (⟨ id ⟩⊢⁻ id) (⟨ id ⟩⊢⁺ id)
   (λ where (_ , refl , _) → refl) (λ where _ → refl)
 
diff --git a/src/Relation/Unary.agda b/src/Relation/Unary.agda
index 532f7b9bca..95d9792882 100644
--- a/src/Relation/Unary.agda
+++ b/src/Relation/Unary.agda
@@ -261,24 +261,36 @@ P ⊥ Q = P ∩ Q ⊆ ∅
 _⊥′_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
 P ⊥′ Q = P ∩ Q ⊆′ ∅
 
--- Update.
+-- Update/preimage/inverse image/functorial change-of-base
+--
+-- The notation, which elsewhere might be rendered
+-- * `f⁻¹ P`, for preimage/inverse image
+-- * `f* P`, for change-of-base/pullback along `f`
+-- captures the Martin-Löf tradition of only mentioning updates to
+-- the ambient context when describing a context-indexed family P:
+-- e.g. (_, σ) ⊢ Tm τ is
+-- "a term of type τ in the ambient context extended with a fresh σ".
 
 _⊢_ : (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.
+-- Change-of-base has left- and right- adjoints (Lawvere).
+--
+-- We borrow the 'diamond'/'box' notation from modal logic, cf.
+-- `Relation.Unary.Closure.Base`, rather than Lawvere's ∃f, ∀f.
+-- In some settings (eg statistics/probability), the left adjoint
+-- is called 'image' or 'pushforward', but the right adjoint
+-- doesn't seem to have a non-symbolic name.
 
 -- Diamond
 
 ⟨_⟩⊢_ : (A → B) → Pred A ℓ → Pred B _
-⟨ f ⟩⊢ P = λ b → ∃ λ a → f a ≡ b × P a
+⟨ f ⟩⊢ P = λ y → ∃ λ x → f x ≡ y × P x
 
 -- Box
 
 [_]⊢_ : (A → B) → Pred A ℓ → Pred B _
-[ f ]⊢ P = λ b → ∀ a → f a ≡ b → P a
+[ f ]⊢ P = λ y → ∀ {x} → f x ≡ y → P x
 
 ------------------------------------------------------------------------
 -- Predicate combinators
diff --git a/src/Relation/Unary/Properties.agda b/src/Relation/Unary/Properties.agda
index 63a75e4cff..986a05da45 100644
--- a/src/Relation/Unary/Properties.agda
+++ b/src/Relation/Unary/Properties.agda
@@ -220,6 +220,43 @@ U-Universal = λ _ → _
 ⊥⇒¬≬ : Binary._⇒_ {A = Pred A ℓ₁} {B = Pred A ℓ₂} _⊥_ (¬_ ∘₂ _≬_)
 ⊥⇒¬≬ P⊥Q = P⊥Q ∘ Product.proj₂
 
+------------------------------------------------------------------------
+-- Properties of adjoints to update: functoriality and adjointness
+
+module _ {P : Pred B ℓ₁} {Q : Pred B ℓ₂} where
+
+  _map-⊢_ : (f : A → B) → P ⊆ Q → f ⊢ P ⊆ f ⊢ Q
+  f map-⊢ P⊆Q = P⊆Q
+
+module _ {P : Pred A ℓ₁} {Q : Pred B ℓ₂} (f : A → B) where
+
+-- ⟨ f ⟩⊢_ is left adjoint to f ⊢_ for given f
+
+  ⟨_⟩⊢⁻_ : ⟨ f ⟩⊢ P ⊆ Q → P ⊆ f ⊢ Q
+  ⟨_⟩⊢⁻_ ⟨f⟩⊢P⊆Q Px = ⟨f⟩⊢P⊆Q (_ , refl , Px)
+
+  ⟨_⟩⊢⁺_ : P ⊆ f ⊢ Q → ⟨ f ⟩⊢ P ⊆ Q
+  ⟨_⟩⊢⁺_ P⊆f⊢Q (_ , refl , Px) = P⊆f⊢Q Px
+
+-- [ f ]⊢_ is right adjoint to f ⊢_ for given f
+
+  [_]⊢⁻_ : Q ⊆ [ f ]⊢ P → f ⊢ Q ⊆ P
+  [_]⊢⁻_ Q⊆[f]⊢P Qfx = Q⊆[f]⊢P Qfx refl
+
+  [_]⊢⁺_ : f ⊢ Q ⊆ P → Q ⊆ [ f ]⊢ P
+  [_]⊢⁺_ f⊢Q⊆P Qfx refl = f⊢Q⊆P Qfx
+
+module _ {P : Pred A ℓ₁} {Q : Pred A ℓ₂} (f : A → B) where
+
+  map-⟨_⟩⊢_ : P ⊆ Q → ⟨ f ⟩⊢ P ⊆ ⟨ f ⟩⊢ Q
+  map-⟨_⟩⊢_ P⊆Q = ⟨ f ⟩⊢⁺ ⊆-trans {k = f ⊢ ⟨f⟩⊢Q} P⊆Q (⟨ f ⟩⊢⁻ ⊆-refl {x = ⟨f⟩⊢Q})
+    where ⟨f⟩⊢Q = ⟨ f ⟩⊢ Q
+
+  map-[_]⊢_ : P ⊆ Q → [ f ]⊢ P ⊆ [ f ]⊢ Q
+  map-[_]⊢_ P⊆Q = [ f ]⊢⁺ ⊆-trans {i = f ⊢ [f]⊢P} ([ f ]⊢⁻ ⊆-refl {x = [f]⊢P}) P⊆Q
+    where [f]⊢P = [ f ]⊢ P
+
+
 ------------------------------------------------------------------------
 -- Decidability properties