add: more commentary text

Author: jamesmckinna

src/Relation/Unary.agda

@@ -261,21 +261,26 @@ P ⊥ Q = P ∩ Q ⊆ ∅
 _⊥′_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
 P ⊥′ Q = P ∩ Q ⊆′ ∅
 
--- Update/functorial change-of-base
-
--- The notation 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
+-- 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)
 
 -- 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, the left adjoint is called 'image' or 'pushforward',
--- but the right adjoint doesn't seem to have a non-symbolic name.
+-- 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
 

src/Relation/Unary/Properties.agda

@@ -230,12 +230,16 @@ module _ {P : Pred B ℓ₁} {Q : Pred B ℓ₂} where
 
 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