Adds "pushforward" to Relation.Unary (#2840)

* add predicate pushforward

* update changelog

* update notation based on discussion

* Additional description

Co-authored-by: jamesmckinna <[email protected]>

---------

Co-authored-by: jamesmckinna <[email protected]>

Author: bsaul

CHANGELOG.md

@@ -238,6 +238,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

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