add: adjoint properties for agda#2840

Author: jamesmckinna

CHANGELOG.md

@@ -221,6 +221,20 @@ 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 `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
+  ```
+
 * In `System.Random`:
   ```agda
   randomIO : IO Bool

src/Function/Related/TypeIsomorphisms.agda

@@ -39,6 +39,8 @@ 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 using (⟨_⟩⊢_)
+open import Relation.Unary.Properties using (⟨_⟩⊢ˡ; ⟨_⟩⊢ʳ)
 
 private
   variable
@@ -359,7 +361,7 @@ Related-cong {A = A} {B = B} {C = C} {D = D} A≈B C≈D = mk⇔
 -- Relating a predicate to an existentially quantified one with the
 -- 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 : A → Set b) {x} → P x ↔ (⟨ id ⟩⊢ P) x
+∃-≡ P {x} = mk↔ₛ′ (⟨ id ⟩⊢ˡ id) (⟨ id ⟩⊢ʳ id) 
   (λ where (_ , refl , _) → refl) (λ where _ → refl)
 

src/Relation/Unary.agda

@@ -261,11 +261,25 @@ P ⊥ Q = P ∩ Q ⊆ ∅
 _⊥′_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
 P ⊥′ Q = P ∩ Q ⊆′ ∅
 
--- Update.
+-- 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
+-- "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`
+⟨_⟩⊢_ : (A → B) → Pred A ℓ → Pred B _
+⟨ f ⟩⊢ P = λ y → ∃ λ x → f x ≡ y × P x
+
+[_]⊢_ : (A → B) → Pred A ℓ → Pred B _
+[ f ]⊢ P = λ y → ∀ {x} → f x ≡ y → P x
+
 ------------------------------------------------------------------------
 -- Predicate combinators
 

src/Relation/Unary/Properties.agda

@@ -220,6 +220,23 @@ U-Universal = λ _ → _
 ⊥⇒¬≬ : Binary._⇒_ {A = Pred A ℓ₁} {B = Pred A ℓ₂} _⊥_ (¬_ ∘₂ _≬_)
 ⊥⇒¬≬ P⊥Q = P⊥Q ∘ Product.proj₂
 
+------------------------------------------------------------------------
+-- Adjoint properties for change-of-base
+
+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)
+
+  ⟨_⟩⊢ʳ : 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
+
+  [_]⊢ʳ : f ⊢ Q ⊆ P → Q ⊆ [ f ]⊢ P
+  [_]⊢ʳ f⊢Q⊆P Qfx refl = f⊢Q⊆P Qfx
+
 ------------------------------------------------------------------------
 -- Decidability properties