[ add ] PartialOrder structure/bundle on _→_ (fixes issue #2820)

CHANGELOG.md

@@ -99,6 +99,16 @@ Additions to existing modules
                     updateAt (padRight m≤n x xs) (inject≤ i m≤n) f ≡ padRight m≤n x (updateAt xs i f)
   ```
 
+* In `Function.Properties`: the `_→_` (pseudo-)type constructor defines a `PartialOrder`,
+  with `Level`-polymorphic and monomorphic versions
+  ```agda
+  →-refl   : Reflexive {A = Set a} _→_
+  →-trans  : Trans {A = Set a} {B = Set b} {C = Set c} _→_ _→_ _→_
+  →-refl′  : Reflexive {A = Set a} _→_
+  →-trans′ : Transitive {A = Set a} _→_
+  →-poset  : Poset (suc a) _ _
+  ```
+
 * In `Relation.Nullary.Negation.Core`
   ```agda
   ¬¬-η : A → ¬ ¬ A

src/Function/Properties.agda

@@ -9,9 +9,16 @@
 module Function.Properties where
 
 open import Axiom.Extensionality.Propositional using (Extensionality)
-open import Function.Base using (flip; _∘_)
+open import Function.Base using (id; flip; _∘_; _∘′_)
 open import Function.Bundles using (_↔_; mk↔ₛ′; Inverse)
-open import Level using (Level)
+open import Level using (Level; suc; _⊔_)
+open import Relation.Binary.Bundles
+  using (Poset)
+open import Relation.Binary.Construct.Interior.Symmetric
+  using (SymInterior; poset)
+open import Relation.Binary.Core using (REL; Rel)
+open import Relation.Binary.Definitions
+  using (Reflexive; Trans; Transitive)
 open import Relation.Binary.PropositionalEquality.Core
   using (trans; cong; cong′)
 
@@ -46,3 +53,36 @@ private
   (λ h → extBD λ x → trans (C↔D.strictlyInverseˡ _) (cong h (A↔B.strictlyInverseˡ x)))
   (λ g → extAC λ x → trans (C↔D.strictlyInverseʳ _) (cong g (A↔B.strictlyInverseʳ x)))
   where module A↔B = Inverse A↔B; module C↔D = Inverse C↔D
+
+------------------------------------------------------------------------
+-- _→_ defines a PartialOrder
+
+module _ where
+
+  private
+    Arrow : REL (Set a) (Set b) (a ⊔ b)
+    Arrow A B = A → B
+
+  →-refl : Reflexive {A = Set a} Arrow
+  →-refl = id
+
+  →-trans : Trans {A = Set a} {B = Set b} {C = Set c} Arrow Arrow Arrow
+  →-trans = flip _∘′_
+
+module _ {a} where
+
+  private
+    Arrow′ : Rel (Set a) a
+    Arrow′ S T = S → T
+
+  →-refl′ : Reflexive Arrow′
+  →-refl′ = id
+
+  →-trans′ : Transitive Arrow′
+  →-trans′ = flip _∘′_
+
+  →-poset : Poset (suc a) _ _
+  →-poset = poset (λ {x = S} → →-refl′ {x = S}) →-trans′
+
+  open Poset →-poset public
+    using (isPartialOrder; isPreorder; isEquivalence)