From 6e8f05fb0329423e18a67d8d4c86cc67ddba8b80 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sun, 31 Aug 2025 15:31:17 +0100
Subject: [PATCH 1/2] [ fix ] issue #2820

---
 src/Function/Properties.agda | 44 ++++++++++++++++++++++++++++++++++--
 1 file changed, 42 insertions(+), 2 deletions(-)

diff --git a/src/Function/Properties.agda b/src/Function/Properties.agda
index bddb573e46..3916162e1d 100644
--- a/src/Function/Properties.agda
+++ b/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)

From b01331382cb66c2fde15f5f73b9b4883a7245451 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 3 Sep 2025 13:32:18 +0100
Subject: [PATCH 2/2] fix: `CHANGELOG`, modulo exports

---
 CHANGELOG.md | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 081dda5b66..9b8f9ff4fe 100644
--- a/CHANGELOG.md
+++ b/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