From e8b419993eb42be6fa5e07100d0ffee3e5dea306 Mon Sep 17 00:00:00 2001
From: Leon Vatthauer <leon.vatthauer@fau.de>
Date: Thu, 23 May 2024 11:10:37 +0200
Subject: [PATCH 1/3] add restriction order

---
 .../Restriction/Properties/Poset.agda         | 50 +++++++++++++++++++
 1 file changed, 50 insertions(+)
 create mode 100644 src/Categories/Category/Restriction/Properties/Poset.agda

diff --git a/src/Categories/Category/Restriction/Properties/Poset.agda b/src/Categories/Category/Restriction/Properties/Poset.agda
new file mode 100644
index 000000000..bd0215dce
--- /dev/null
+++ b/src/Categories/Category/Restriction/Properties/Poset.agda
@@ -0,0 +1,50 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category.Core using (Category)
+open import Categories.Category.Restriction using (Restriction)
+open import Relation.Binary.Bundles using (Poset)
+open import Relation.Binary.Structures using (IsPartialOrder)
+
+import Categories.Morphism.Reasoning as MR
+
+-- Every restriction category induces a partial order (the restriction order) on hom-sets
+
+module Categories.Category.Restriction.Properties.Poset {o ℓ e} {𝒞 : Category o ℓ e} (R : Restriction 𝒞) where  
+  open Category 𝒞
+  open Restriction R
+  open Equiv
+  open HomReasoning
+  open MR 𝒞 using (pullʳ; pullˡ)
+
+  poset : (A B : Obj) → Poset ℓ e e
+  poset A B = record 
+    { Carrier = A ⇒ B 
+    ; _≈_ = _≈_ 
+    ; _≤_ = λ f g → f ≈ g ∘ f ↓
+    ; isPartialOrder = record 
+      { isPreorder = record 
+        { isEquivalence = record 
+          { refl = refl 
+          ; sym = sym 
+          ; trans = trans 
+          } 
+        ; reflexive = λ {x} {y} x≈y → begin 
+          x       ≈˘⟨ pidʳ ⟩ 
+          x ∘ x ↓ ≈⟨ x≈y ⟩∘⟨refl ⟩
+          y ∘ x ↓ ∎
+        ; trans = λ {i} {j} {k} i≈j∘i↓ j≈k∘j↓ → begin 
+          i               ≈⟨ i≈j∘i↓ ⟩ 
+          j ∘ i ↓         ≈⟨ j≈k∘j↓ ⟩∘⟨refl ⟩ 
+          (k ∘ j ↓) ∘ i ↓ ≈⟨ pullʳ (sym ↓-denestʳ) ⟩ 
+          k ∘ (j ∘ i ↓) ↓ ≈⟨ refl⟩∘⟨ ↓-cong (sym i≈j∘i↓) ⟩ 
+          k ∘ i ↓         ∎ 
+        } 
+      ; antisym = λ {i} {j} i≈j∘i↓ j≈i∘j↓ → begin 
+        i               ≈⟨ i≈j∘i↓ ⟩ 
+        j ∘ i ↓         ≈⟨ j≈i∘j↓ ⟩∘⟨refl ⟩ 
+        (i ∘ j ↓) ∘ i ↓ ≈⟨ pullʳ ↓-comm ⟩ 
+        i ∘ i ↓ ∘ j ↓   ≈⟨ pullˡ pidʳ ⟩
+        i ∘ j ↓         ≈˘⟨ j≈i∘j↓ ⟩
+        j               ∎ 
+      } 
+    }

From 73a544978ab24b6153ae0b65d4581b66ef71d133 Mon Sep 17 00:00:00 2001
From: Leon Vatthauer <leon.vatthauer@fau.de>
Date: Thu, 23 May 2024 11:19:17 +0200
Subject: [PATCH 2/3] move imports

---
 .../Category/Restriction/Properties.agda           | 14 ++++++--------
 1 file changed, 6 insertions(+), 8 deletions(-)

diff --git a/src/Categories/Category/Restriction/Properties.agda b/src/Categories/Category/Restriction/Properties.agda
index fd01c8ac1..cc19c8ea5 100644
--- a/src/Categories/Category/Restriction/Properties.agda
+++ b/src/Categories/Category/Restriction/Properties.agda
@@ -1,22 +1,20 @@
 {-# OPTIONS --without-K --safe #-}
 
--- Some properties of Restriction Categories
-
--- The first few lemmas are from Cocket & Lack, Lemma 2.1 and 2.2
-module Categories.Category.Restriction.Properties where
-
+open import Categories.Category.Core using (Category)
+open import Categories.Category.Restriction using (Restriction)
 open import Data.Product using (Σ; _,_)
 open import Level using (Level; _⊔_)
 
-open import Categories.Category.Core using (Category)
-open import Categories.Category.Restriction using (Restriction)
 open import Categories.Category.SubCategory
 open import Categories.Morphism using (Mono)
 open import Categories.Morphism.Idempotent using (Idempotent)
 open import Categories.Morphism.Properties using (Mono-id)
 import Categories.Morphism.Reasoning as MR
 
-module _ {o ℓ e : Level} {𝒞 : Category o ℓ e} (R : Restriction 𝒞) where
+-- Some properties of Restriction Categories
+
+-- The first few lemmas are from Cocket & Lack, Lemma 2.1 and 2.2
+module Categories.Category.Restriction.Properties {o ℓ e} {𝒞 : Category o ℓ e} (R : Restriction 𝒞) where
   open Category 𝒞
   open Restriction R
   open HomReasoning

From 13426962f854457c6723d77dddd5f4470263856e Mon Sep 17 00:00:00 2001
From: Leon Vatthauer <leon.vatthauer@fau.de>
Date: Thu, 23 May 2024 12:27:44 +0200
Subject: [PATCH 3/3] use equiv from Category

---
 src/Categories/Category/Restriction/Properties/Poset.agda | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

diff --git a/src/Categories/Category/Restriction/Properties/Poset.agda b/src/Categories/Category/Restriction/Properties/Poset.agda
index bd0215dce..820216b12 100644
--- a/src/Categories/Category/Restriction/Properties/Poset.agda
+++ b/src/Categories/Category/Restriction/Properties/Poset.agda
@@ -23,11 +23,7 @@ module Categories.Category.Restriction.Properties.Poset {o ℓ e} {𝒞 : Catego
     ; _≤_ = λ f g → f ≈ g ∘ f ↓
     ; isPartialOrder = record 
       { isPreorder = record 
-        { isEquivalence = record 
-          { refl = refl 
-          ; sym = sym 
-          ; trans = trans 
-          } 
+        { isEquivalence = equiv
         ; reflexive = λ {x} {y} x≈y → begin 
           x       ≈˘⟨ pidʳ ⟩ 
           x ∘ x ↓ ≈⟨ x≈y ⟩∘⟨refl ⟩