add: functoriality proofs

Author: jamesmckinna

CHANGELOG.md

@@ -229,10 +229,13 @@ Additions to existing modules
 
 * In `Relation.Unary.Properties`
   ```agda
-  ⟨_⟩⊢ˡ : (f : A → B) → ⟨ f ⟩⊢ P ⊆ Q → P ⊆ f ⊢ Q
-  ⟨_⟩⊢ʳ : (f : A → B) → P ⊆ f ⊢ Q → ⟨ f ⟩⊢ P ⊆ Q
-  [_]⊢ˡ : (f : A → B) → Q ⊆ [ f ]⊢ P → f ⊢ Q ⊆ P
-  [_]⊢ʳ : (f : A → B) → f ⊢ Q ⊆ P → Q ⊆ [ f ]⊢ P
+  _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`:

src/Relation/Unary.agda

@@ -273,7 +273,10 @@ 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`
+-- `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.
+
 ⟨_⟩⊢_ : (A → B) → Pred A ℓ → Pred B _
 ⟨ f ⟩⊢ P = λ y → ∃ λ x → f x ≡ y × P x
 

src/Relation/Unary/Properties.agda

@@ -221,21 +221,35 @@ U-Universal = λ _ → _
 ⊥⇒¬≬ P⊥Q = P⊥Q ∘ Product.proj₂
 
 ------------------------------------------------------------------------
--- Adjoint properties for change-of-base
+-- 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 A ℓ₂} (f : A → B) where
+
+  map-⟨_⟩⊢_ : P ⊆ Q → ⟨ f ⟩⊢ P ⊆ ⟨ f ⟩⊢ Q
+  map-⟨_⟩⊢_ P⊆Q (_ , refl , Px) = (_ , refl , P⊆Q  Px)
+
+  map-[_]⊢_ : P ⊆ Q → [ f ]⊢ P ⊆ [ f ]⊢ Q
+  map-[_]⊢_ P⊆Q Px refl = P⊆Q (Px refl)
 
 module _ {P : Pred A ℓ₁} {Q : Pred B ℓ₂} (f : A → B) where
 
-  ⟨_⟩⊢ˡ : ⟨ f ⟩⊢ P ⊆ Q → P ⊆ f ⊢ Q
-  ⟨_⟩⊢ˡ ⟨f⟩⊢P⊆Q Px = ⟨f⟩⊢P⊆Q (_ , refl , Px)
+  ⟨_⟩⊢⁻_ : ⟨ 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
 
-  ⟨_⟩⊢ʳ : P ⊆ f ⊢ Q → ⟨ f ⟩⊢ P ⊆ Q
-  ⟨_⟩⊢ʳ P⊆f⊢Q (x , refl , Px) = P⊆f⊢Q Px
+  [_]⊢⁻_ : Q ⊆ [ f ]⊢ P → f ⊢ Q ⊆ P
+  [_]⊢⁻_ Q⊆[f]⊢P Qfx = Q⊆[f]⊢P Qfx refl
 
-  [_]⊢ˡ : 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
 
-  [_]⊢ʳ : f ⊢ Q ⊆ P → Q ⊆ [ f ]⊢ P
-  [_]⊢ʳ f⊢Q⊆P Qfx refl = f⊢Q⊆P Qfx
 
 ------------------------------------------------------------------------
 -- Decidability properties