From f84a8d1bf9525aa9a005c1a31045b7685c6ac059 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Thu, 1 Jan 2026 14:31:42 -0600
Subject: Update push, pull, and sys functors

---
 Data/System.agda | 92 +++++++++++++++++++++++++++-----------------------------
 1 file changed, 45 insertions(+), 47 deletions(-)

(limited to 'Data/System.agda')

diff --git a/Data/System.agda b/Data/System.agda
index d71c2a8..d12fa12 100644
--- a/Data/System.agda
+++ b/Data/System.agda
@@ -66,53 +66,51 @@ module _ {n : ℕ} where
 
 open System
 
-private
-
-  module _ {n : ℕ} where
-
-    open _≤_
-
-    ≤-refl : Reflexive (_≤_ {n})
-    ⇒S ≤-refl = Id _
-    ≗-fₛ (≤-refl {x}) _ _ = S.refl x
-    ≗-fₒ ≤-refl _ = ≋.refl
-
-    ≡⇒≤ : _≡_ Rel.⇒ _≤_
-    ≡⇒≤ ≡.refl = ≤-refl
-
-    ≤-trans : Transitive _≤_
-    ⇒S (≤-trans a b) = ⇒S b ∙ ⇒S a
-    ≗-fₛ (≤-trans {x} {y} {z} a b) i s = let open ≈-Reasoning (S z) in begin
-        ⇒S b ⟨$⟩ (⇒S a ⟨$⟩ (fₛ′ x i s)) ≈⟨ cong (⇒S b) (≗-fₛ a i s) ⟩
-        ⇒S b ⟨$⟩ (fₛ′ y i (⇒S a ⟨$⟩ s)) ≈⟨ ≗-fₛ b i (⇒S a ⟨$⟩ s) ⟩
-        fₛ′ z i (⇒S b ⟨$⟩ (⇒S a ⟨$⟩ s)) ∎
-    ≗-fₒ (≤-trans {x} {y} {z} a b) s = let open ≈-Reasoning (Values n) in begin
-        fₒ′ x s                       ≈⟨ ≗-fₒ a s ⟩
-        fₒ′ y (⇒S a ⟨$⟩ s)            ≈⟨ ≗-fₒ b (⇒S a ⟨$⟩ s) ⟩
-        fₒ′ z (⇒S b ⟨$⟩ (⇒S a ⟨$⟩ s)) ∎
-
-    variable
-      A B C : System n
-
-    _≈_ : Rel (A ≤ B) 0ℓ
-    _≈_ {A} {B} ≤₁ ≤₂ = ⇒S ≤₁ A⇒B.≈ ⇒S ≤₂
-      where
-        module A⇒B = Setoid (S A ⇒ₛ S B)
-
-    open Rel.IsEquivalence
-
-    ≈-isEquiv : Rel.IsEquivalence (_≈_ {A} {B})
-    ≈-isEquiv {B = B} .refl = S.refl B
-    ≈-isEquiv {B = B} .sym a = S.sym B a
-    ≈-isEquiv {B = B} .trans a b = S.trans B a b
-
-    ≤-resp-≈ : {f h : B ≤ C} {g i : A ≤ B} → f ≈ h → g ≈ i → ≤-trans g f ≈ ≤-trans i h
-    ≤-resp-≈ {_} {C} {_} {f} {h} {g} {i} f≈h g≈i {x} = begin
-        ⇒S f ⟨$⟩ (⇒S g ⟨$⟩ x) ≈⟨ f≈h ⟩
-        ⇒S h ⟨$⟩ (⇒S g ⟨$⟩ x) ≈⟨ cong (⇒S h) g≈i ⟩
-        ⇒S h ⟨$⟩ (⇒S i ⟨$⟩ x) ∎
-      where
-        open ≈-Reasoning (System.S C)
+module _ {n : ℕ} where
+
+  open _≤_
+
+  ≤-refl : Reflexive (_≤_ {n})
+  ⇒S ≤-refl = Id _
+  ≗-fₛ (≤-refl {x}) _ _ = S.refl x
+  ≗-fₒ ≤-refl _ = ≋.refl
+
+  ≡⇒≤ : _≡_ Rel.⇒ _≤_
+  ≡⇒≤ ≡.refl = ≤-refl
+
+  ≤-trans : Transitive _≤_
+  ⇒S (≤-trans a b) = ⇒S b ∙ ⇒S a
+  ≗-fₛ (≤-trans {x} {y} {z} a b) i s = let open ≈-Reasoning (S z) in begin
+      ⇒S b ⟨$⟩ (⇒S a ⟨$⟩ (fₛ′ x i s)) ≈⟨ cong (⇒S b) (≗-fₛ a i s) ⟩
+      ⇒S b ⟨$⟩ (fₛ′ y i (⇒S a ⟨$⟩ s)) ≈⟨ ≗-fₛ b i (⇒S a ⟨$⟩ s) ⟩
+      fₛ′ z i (⇒S b ⟨$⟩ (⇒S a ⟨$⟩ s)) ∎
+  ≗-fₒ (≤-trans {x} {y} {z} a b) s = let open ≈-Reasoning (Values n) in begin
+      fₒ′ x s                       ≈⟨ ≗-fₒ a s ⟩
+      fₒ′ y (⇒S a ⟨$⟩ s)            ≈⟨ ≗-fₒ b (⇒S a ⟨$⟩ s) ⟩
+      fₒ′ z (⇒S b ⟨$⟩ (⇒S a ⟨$⟩ s)) ∎
+
+  variable
+    A B C : System n
+
+  _≈_ : Rel (A ≤ B) 0ℓ
+  _≈_ {A} {B} ≤₁ ≤₂ = ⇒S ≤₁ A⇒B.≈ ⇒S ≤₂
+    where
+      module A⇒B = Setoid (S A ⇒ₛ S B)
+
+  open Rel.IsEquivalence
+
+  ≈-isEquiv : Rel.IsEquivalence (_≈_ {A} {B})
+  ≈-isEquiv {B = B} .refl = S.refl B
+  ≈-isEquiv {B = B} .sym a = S.sym B a
+  ≈-isEquiv {B = B} .trans a b = S.trans B a b
+
+  ≤-resp-≈ : {f h : B ≤ C} {g i : A ≤ B} → f ≈ h → g ≈ i → ≤-trans g f ≈ ≤-trans i h
+  ≤-resp-≈ {_} {C} {_} {f} {h} {g} {i} f≈h g≈i {x} = begin
+      ⇒S f ⟨$⟩ (⇒S g ⟨$⟩ x) ≈⟨ f≈h ⟩
+      ⇒S h ⟨$⟩ (⇒S g ⟨$⟩ x) ≈⟨ cong (⇒S h) g≈i ⟩
+      ⇒S h ⟨$⟩ (⇒S i ⟨$⟩ x) ∎
+    where
+      open ≈-Reasoning (System.S C)
 
 System-≤ : ℕ → Preorder (suc 0ℓ) (suc 0ℓ) ℓ
 System-≤ n = record
-- 
cgit v1.2.3