From f84a8d1bf9525aa9a005c1a31045b7685c6ac059 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Thu, 1 Jan 2026 14:31:42 -0600 Subject: Update push, pull, and sys functors --- Functor/Instance/Nat/Pull.agda | 123 +++++++++------- Functor/Instance/Nat/Push.agda | 115 ++++++++++----- Functor/Instance/Nat/System.agda | 304 +++++++++++++++++++++++++++++---------- 3 files changed, 374 insertions(+), 168 deletions(-) (limited to 'Functor') diff --git a/Functor/Instance/Nat/Pull.agda b/Functor/Instance/Nat/Pull.agda index b1764d9..c2a06c6 100644 --- a/Functor/Instance/Nat/Pull.agda +++ b/Functor/Instance/Nat/Pull.agda @@ -2,80 +2,99 @@ module Functor.Instance.Nat.Pull where +open import Level using (0ℓ) + +open import Category.Instance.Setoids.SymmetricMonoidal {0ℓ} {0ℓ} using (Setoids-×) + open import Categories.Category.Instance.Nat using (Natop) -open import Categories.Category.Instance.Setoids using (Setoids) open import Categories.Functor using (Functor) +open import Category.Construction.CMonoids Setoids-×.symmetric using (CMonoids) +open import Data.CMonoid using (fromCMonoid) +open import Data.Circuit.Value using (Monoid) open import Data.Fin.Base using (Fin) +open import Data.Monoid using (fromMonoid) open import Data.Nat.Base using (ℕ) +open import Data.Product using (_,_) +open import Data.Setoid using (∣_∣; _⇒ₛ_) +open import Data.System.Values Monoid using (Values; _⊕_; module Object) +open import Data.Unit using (⊤; tt) open import Function.Base using (id; _∘_) -open import Function.Bundles using (Func; _⟶ₛ_) +open import Function.Bundles using (Func; _⟶ₛ_; _⟨$⟩_) open import Function.Construct.Identity using () renaming (function to Id) open import Function.Construct.Setoid using (setoid; _∙_) -open import Level using (0ℓ) +open import Object.Monoid.Commutative Setoids-×.symmetric using (CommutativeMonoid; CommutativeMonoid⇒) open import Relation.Binary using (Rel; Setoid) open import Relation.Binary.PropositionalEquality as ≡ using (_≗_) -open import Data.Circuit.Value using (Monoid) -open import Data.System.Values Monoid using (Values) -open import Data.Unit using (⊤; tt) +open CommutativeMonoid using (Carrier; monoid) +open CommutativeMonoid⇒ using (arr) open Functor open Func - --- Pull takes a natural number n to the setoid Values n +open Object using (Valuesₘ) private variable A B C : ℕ - _≈_ : {X Y : Setoid 0ℓ 0ℓ} → Rel (X ⟶ₛ Y) 0ℓ - _≈_ {X} {Y} = Setoid._≈_ (setoid X Y) - - infixr 4 _≈_ - - opaque +-- Pull takes a natural number n to the commutative monoid Valuesₘ n - unfolding Values +Pull₀ : ℕ → CommutativeMonoid +Pull₀ n = Valuesₘ n - -- action of Pull on morphisms (contravariant) - Pull₁ : (Fin A → Fin B) → Values B ⟶ₛ Values A - to (Pull₁ f) i = i ∘ f - cong (Pull₁ f) x≗y = x≗y ∘ f - - -- Pull respects identity - Pull-identity : Pull₁ id ≈ Id (Values A) - Pull-identity {A} = Setoid.refl (Values A) - - opaque - - unfolding Pull₁ - - -- Pull flips composition - Pull-homomorphism - : (f : Fin A → Fin B) - (g : Fin B → Fin C) - → Pull₁ (g ∘ f) ≈ Pull₁ f ∙ Pull₁ g - Pull-homomorphism {A} _ _ = Setoid.refl (Values A) - - -- Pull respects equality - Pull-resp-≈ - : {f g : Fin A → Fin B} - → f ≗ g - → Pull₁ f ≈ Pull₁ g - Pull-resp-≈ f≗g {v} = ≡.cong v ∘ f≗g +-- action of Pull on morphisms (contravariant) +-- setoid morphism opaque + unfolding Valuesₘ Values + Pullₛ : (Fin A → Fin B) → Carrier (Pull₀ B) ⟶ₛ Carrier (Pull₀ A) + Pullₛ f .to x = x ∘ f + Pullₛ f .cong x≗y = x≗y ∘ f - unfolding Pull₁ - - Pull-defs : ⊤ - Pull-defs = tt +-- monoid morphism +opaque + unfolding _⊕_ Pullₛ + Pullₘ : (Fin A → Fin B) → CommutativeMonoid⇒ (Pull₀ B) (Pull₀ A) + Pullₘ {A} f = record + { monoid⇒ = record + { arr = Pullₛ f + ; preserves-μ = Setoid.refl (Values A) + ; preserves-η = Setoid.refl (Values A) + } + } + +-- Pull respects identity +opaque + unfolding Pullₘ + Pull-identity + : (open Setoid (Carrier (Pull₀ A) ⇒ₛ Carrier (Pull₀ A))) + → arr (Pullₘ id) ≈ Id (Carrier (Pull₀ A)) + Pull-identity {A} = Setoid.refl (Values A) --- the Pull functor -Pull : Functor Natop (Setoids 0ℓ 0ℓ) -F₀ Pull = Values -F₁ Pull = Pull₁ -identity Pull = Pull-identity -homomorphism Pull {f = f} {g} = Pull-homomorphism g f -F-resp-≈ Pull = Pull-resp-≈ +-- Pull flips composition +opaque + unfolding Pullₘ + Pull-homomorphism + : (f : Fin A → Fin B) + (g : Fin B → Fin C) + (open Setoid (Carrier (Pull₀ C) ⇒ₛ Carrier (Pull₀ A))) + → arr (Pullₘ (g ∘ f)) ≈ arr (Pullₘ f) ∙ arr (Pullₘ g) + Pull-homomorphism {A} _ _ = Setoid.refl (Values A) + +-- Pull respects equality +opaque + unfolding Pullₘ + Pull-resp-≈ + : {f g : Fin A → Fin B} + → f ≗ g + → (open Setoid (Carrier (Pull₀ B) ⇒ₛ Carrier (Pull₀ A))) + → arr (Pullₘ f) ≈ arr (Pullₘ g) + Pull-resp-≈ f≗g {v} = ≡.cong v ∘ f≗g + +Pull : Functor Natop CMonoids +Pull .F₀ = Pull₀ +Pull .F₁ = Pullₘ +Pull .identity = Pull-identity +Pull .homomorphism = Pull-homomorphism _ _ +Pull .F-resp-≈ = Pull-resp-≈ module Pull = Functor Pull diff --git a/Functor/Instance/Nat/Push.agda b/Functor/Instance/Nat/Push.agda index 8126006..71b9a63 100644 --- a/Functor/Instance/Nat/Push.agda +++ b/Functor/Instance/Nat/Push.agda @@ -2,78 +2,115 @@ module Functor.Instance.Nat.Push where -open import Categories.Functor using (Functor) +open import Level using (0ℓ) +open import Category.Instance.Setoids.SymmetricMonoidal {0ℓ} {0ℓ} using (Setoids-×) + open import Categories.Category.Instance.Nat using (Nat) open import Categories.Category.Instance.Setoids using (Setoids) -open import Data.Circuit.Merge using (merge; merge-cong₁; merge-cong₂; merge-⁅⁆; merge-preimage) -open import Data.Fin.Base using (Fin) +open import Categories.Functor using (Functor) +open import Category.Construction.CMonoids Setoids-×.symmetric using (CMonoids) +open import Data.Circuit.Value using (Monoid) +open import Data.Fin using (Fin) open import Data.Fin.Preimage using (preimage; preimage-cong₁) -open import Data.Nat.Base using (ℕ) +open import Data.Nat using (ℕ) +open import Data.Setoid using (∣_∣; _⇒ₛ_) open import Data.Subset.Functional using (⁅_⁆) -open import Function.Base using (id; _∘_) -open import Function.Bundles using (Func; _⟶ₛ_) +open import Data.System.Values Monoid using (Values; module Object; _⊕_; <ε>; _≋_; ≋-isEquiv; merge; push; merge-⊕; merge-<ε>; merge-cong; merge-⁅⁆; merge-push; merge-cong₂) +open import Function using (Func; _⟶ₛ_; _⟨$⟩_; _∘_; id) open import Function.Construct.Identity using () renaming (function to Id) -open import Function.Construct.Setoid using (setoid; _∙_) -open import Level using (0ℓ) -open import Relation.Binary using (Rel; Setoid) +open import Function.Construct.Setoid using (_∙_) +open import Object.Monoid.Commutative Setoids-×.symmetric using (CommutativeMonoid; CommutativeMonoid⇒) +open import Relation.Binary using (Setoid) open import Relation.Binary.PropositionalEquality as ≡ using (_≗_) -open import Data.Circuit.Value using (Monoid) -open import Data.System.Values Monoid using (Values) -open import Data.Unit using (⊤; tt) open Func open Functor - --- Push sends a natural number n to Values n +open Object using (Valuesₘ) private variable A B C : ℕ - _≈_ : {X Y : Setoid 0ℓ 0ℓ} → Rel (X ⟶ₛ Y) 0ℓ - _≈_ {X} {Y} = Setoid._≈_ (setoid X Y) - infixr 4 _≈_ + -- Push sends a natural number n to Values n + Push₀ : ℕ → CommutativeMonoid + Push₀ n = Valuesₘ n + + -- action of Push on morphisms (covariant) opaque unfolding Values - -- action of Push on morphisms (covariant) - Push₁ : (Fin A → Fin B) → Values A ⟶ₛ Values B - to (Push₁ f) v = merge v ∘ preimage f ∘ ⁅_⁆ - cong (Push₁ f) x≗y = merge-cong₁ x≗y ∘ preimage f ∘ ⁅_⁆ + open CommutativeMonoid using (Carrier) + open CommutativeMonoid⇒ using (arr) + + -- setoid morphism + Pushₛ : (Fin A → Fin B) → Values A ⟶ₛ Values B + Pushₛ f .to v = merge v ∘ preimage f ∘ ⁅_⁆ + Pushₛ f .cong x≗y i = merge-cong (preimage f ⁅ i ⁆) x≗y + + opaque + + unfolding Pushₛ _⊕_ + + Push-⊕ + : (f : Fin A → Fin B) + → (xs ys : ∣ Values A ∣) + → Pushₛ f ⟨$⟩ (xs ⊕ ys) + ≋ (Pushₛ f ⟨$⟩ xs) ⊕ (Pushₛ f ⟨$⟩ ys) + Push-⊕ f xs ys i = merge-⊕ xs ys (preimage f ⁅ i ⁆) + + Push-<ε> + : (f : Fin A → Fin B) + → Pushₛ f ⟨$⟩ <ε> ≋ <ε> + Push-<ε> f i = merge-<ε> (preimage f ⁅ i ⁆) + + opaque + + unfolding Push-⊕ ≋-isEquiv Valuesₘ + + -- monoid morphism + Pushₘ : (Fin A → Fin B) → CommutativeMonoid⇒ (Valuesₘ A) (Valuesₘ B) + Pushₘ f = record + { monoid⇒ = record + { arr = Pushₛ f + ; preserves-μ = Push-⊕ f _ _ + ; preserves-η = Push-<ε> f + } + } -- Push respects identity - Push-identity : Push₁ id ≈ Id (Values A) - Push-identity {_} {v} = merge-⁅⁆ v + Push-identity + : (open Setoid (Carrier (Push₀ A) ⇒ₛ Carrier (Push₀ A))) + → arr (Pushₘ id) ≈ Id (Carrier (Push₀ A)) + Push-identity {_} {v} i = merge-⁅⁆ v i + + opaque + + unfolding Pushₘ push -- Push respects composition Push-homomorphism : {f : Fin A → Fin B} {g : Fin B → Fin C} - → Push₁ (g ∘ f) ≈ Push₁ g ∙ Push₁ f - Push-homomorphism {f = f} {g} {v} = merge-preimage f v ∘ preimage g ∘ ⁅_⁆ + → (open Setoid (Carrier (Push₀ A) ⇒ₛ Carrier (Push₀ C))) + → arr (Pushₘ (g ∘ f)) ≈ arr (Pushₘ g) ∙ arr (Pushₘ f) + Push-homomorphism {f = f} {g} {v} = merge-push f g v -- Push respects equality Push-resp-≈ : {f g : Fin A → Fin B} → f ≗ g - → Push₁ f ≈ Push₁ g + → (open Setoid (Carrier (Push₀ A) ⇒ₛ Carrier (Push₀ B))) + → arr (Pushₘ f) ≈ arr (Pushₘ g) Push-resp-≈ f≗g {v} = merge-cong₂ v ∘ preimage-cong₁ f≗g ∘ ⁅_⁆ -opaque - - unfolding Push₁ - - Push-defs : ⊤ - Push-defs = tt - -- the Push functor -Push : Functor Nat (Setoids 0ℓ 0ℓ) -F₀ Push = Values -F₁ Push = Push₁ -identity Push = Push-identity -homomorphism Push = Push-homomorphism -F-resp-≈ Push = Push-resp-≈ +Push : Functor Nat CMonoids +Push .F₀ = Push₀ +Push .F₁ = Pushₘ +Push .identity = Push-identity +Push .homomorphism = Push-homomorphism +Push .F-resp-≈ = Push-resp-≈ module Push = Functor Push diff --git a/Functor/Instance/Nat/System.agda b/Functor/Instance/Nat/System.agda index 05e1e7b..4a651f2 100644 --- a/Functor/Instance/Nat/System.agda +++ b/Functor/Instance/Nat/System.agda @@ -1,110 +1,260 @@ {-# OPTIONS --without-K --safe #-} +{-# OPTIONS --hidden-argument-puns #-} module Functor.Instance.Nat.System where - open import Level using (suc; 0ℓ) open import Categories.Category.Instance.Nat using (Nat) -open import Categories.Category.Instance.Setoids using (Setoids) -open import Categories.Functor.Core using (Functor) +open import Categories.Category using (Category) +open import Categories.Category.Instance.Cats using (Cats) +open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; niHelper) +open import Categories.Functor using (Functor; _∘F_) renaming (id to idF) open import Data.Circuit.Value using (Monoid) -open import Data.Fin.Base using (Fin) -open import Data.Nat.Base using (ℕ) +open import Data.Fin using (Fin) +open import Data.Nat using (ℕ) open import Data.Product.Base using (_,_; _×_) -open import Data.System {suc 0ℓ} using (System; _≤_; Systemₛ) -open import Data.System.Values Monoid using (module ≋) -open import Data.Unit using (⊤; tt) -open import Function.Base using (id; _∘_) -open import Function.Bundles using (Func; _⟶ₛ_; _⟨$⟩_) +open import Data.Setoid using (∣_∣) +open import Data.System {suc 0ℓ} using (System; _≤_; Systemₛ; Systems; ≤-refl; ≤-trans; _≈_) +open import Data.System.Values Monoid using (module ≋; module Object; Values; ≋-isEquiv) +open import Relation.Binary using (Setoid) +open import Function using (Func; _⟶ₛ_; _⟨$⟩_; _∘_; id) open import Function.Construct.Identity using () renaming (function to Id) open import Function.Construct.Setoid using (_∙_) open import Functor.Instance.Nat.Pull using (Pull) open import Functor.Instance.Nat.Push using (Push) open import Relation.Binary.PropositionalEquality as ≡ using (_≗_) +open import Category.Instance.Setoids.SymmetricMonoidal {0ℓ} {0ℓ} using (Setoids-×) +open import Category.Construction.CMonoids Setoids-×.symmetric using (CMonoids) +open import Object.Monoid.Commutative Setoids-×.symmetric using (CommutativeMonoid; CommutativeMonoid⇒) + +open CommutativeMonoid⇒ using (arr) +open Object using (Valuesₘ) open Func open Functor open _≤_ private - variable A B C : ℕ - opaque +opaque + unfolding Valuesₘ ≋-isEquiv + map : (Fin A → Fin B) → System A → System B + map {A} {B} f X = let open System X in record + { S = S + ; fₛ = fₛ ∙ arr (Pull.₁ f) + ; fₒ = arr (Push.₁ f) ∙ fₒ + } + +opaque + unfolding map + open System + map-≤ : (f : Fin A → Fin B) {X Y : System A} → X ≤ Y → map f X ≤ map f Y + ⇒S (map-≤ f x≤y) = ⇒S x≤y + ≗-fₛ (map-≤ f x≤y) = ≗-fₛ x≤y ∘ to (arr (Pull.₁ f)) + ≗-fₒ (map-≤ f x≤y) = cong (arr (Push.₁ f)) ∘ ≗-fₒ x≤y + +opaque + unfolding map-≤ + map-≤-refl + : (f : Fin A → Fin B) + → {X : System A} + → map-≤ f (≤-refl {A} {X}) ≈ ≤-refl + map-≤-refl f {X} = Setoid.refl (S (map f X)) + +opaque + unfolding map-≤ + map-≤-trans + : (f : Fin A → Fin B) + → {X Y Z : System A} + → {h : X ≤ Y} + → {g : Y ≤ Z} + → map-≤ f (≤-trans h g) ≈ ≤-trans (map-≤ f h) (map-≤ f g) + map-≤-trans f {Z = Z} = Setoid.refl (S (map f Z)) - map : (Fin A → Fin B) → System A → System B - map f X = let open System X in record - { S = S - ; fₛ = fₛ ∙ Pull.₁ f - ; fₒ = Push.₁ f ∙ fₒ +opaque + unfolding map-≤ + map-≈ + : (f : Fin A → Fin B) + → {X Y : System A} + → {g h : X ≤ Y} + → h ≈ g + → map-≤ f h ≈ map-≤ f g + map-≈ f h≈g = h≈g + +Sys₁ : (Fin A → Fin B) → Functor (Systems A) (Systems B) +Sys₁ {A} {B} f = record + { F₀ = map f + ; F₁ = λ C≤D → map-≤ f C≤D + ; identity = map-≤-refl f + ; homomorphism = map-≤-trans f + ; F-resp-≈ = map-≈ f + } + +opaque + unfolding map + map-id-≤ : (X : System A) → map id X ≤ X + map-id-≤ X .⇒S = Id (S X) + map-id-≤ X .≗-fₛ i s = cong (fₛ X) Pull.identity + map-id-≤ X .≗-fₒ s = Push.identity + +opaque + unfolding map + map-id-≥ : (X : System A) → X ≤ map id X + map-id-≥ X .⇒S = Id (S X) + map-id-≥ X .≗-fₛ i s = cong (fₛ X) (≋.sym Pull.identity) + map-id-≥ X .≗-fₒ s = ≋.sym Push.identity + +opaque + unfolding map-≤ map-id-≤ + map-id-comm + : {X Y : System A} + (f : X ≤ Y) + → ≤-trans (map-≤ id f) (map-id-≤ Y) ≈ ≤-trans (map-id-≤ X) f + map-id-comm {Y} f = Setoid.refl (S Y) + +opaque + + unfolding map-id-≤ map-id-≥ + + map-id-isoˡ + : (X : System A) + → ≤-trans (map-id-≤ X) (map-id-≥ X) ≈ ≤-refl + map-id-isoˡ X = Setoid.refl (S X) + + map-id-isoʳ + : (X : System A) + → ≤-trans (map-id-≥ X) (map-id-≤ X) ≈ ≤-refl + map-id-isoʳ X = Setoid.refl (S X) + +Sys-identity : Sys₁ {A} id ≃ idF +Sys-identity = niHelper record + { η = map-id-≤ + ; η⁻¹ = map-id-≥ + ; commute = map-id-comm + ; iso = λ X → record + { isoˡ = map-id-isoˡ X + ; isoʳ = map-id-isoʳ X + } + } + +opaque + unfolding map + map-∘-≤ + : (f : Fin A → Fin B) + (g : Fin B → Fin C) + (X : System A) + → map (g ∘ f) X ≤ map g (map f X) + map-∘-≤ f g X .⇒S = Id (S X) + map-∘-≤ f g X .≗-fₛ i s = cong (fₛ X) Pull.homomorphism + map-∘-≤ f g X .≗-fₒ s = Push.homomorphism + +opaque + unfolding map + map-∘-≥ + : (f : Fin A → Fin B) + (g : Fin B → Fin C) + (X : System A) + → map g (map f X) ≤ map (g ∘ f) X + map-∘-≥ f g X .⇒S = Id (S X) + map-∘-≥ f g X .≗-fₛ i s = cong (fₛ X) (≋.sym Pull.homomorphism) + map-∘-≥ f g X .≗-fₒ s = ≋.sym Push.homomorphism + +Sys-homo + : (f : Fin A → Fin B) + (g : Fin B → Fin C) + → Sys₁ (g ∘ f) ≃ Sys₁ g ∘F Sys₁ f +Sys-homo {A} f g = niHelper record + { η = map-∘-≤ f g + ; η⁻¹ = map-∘-≥ f g + ; commute = map-∘-comm f g + ; iso = λ X → record + { isoˡ = isoˡ X + ; isoʳ = isoʳ X } + } + where + opaque + unfolding map-∘-≤ map-≤ + map-∘-comm + : (f : Fin A → Fin B) + (g : Fin B → Fin C) + → {X Y : System A} + (X≤Y : X ≤ Y) + → ≤-trans (map-≤ (g ∘ f) X≤Y) (map-∘-≤ f g Y) + ≈ ≤-trans (map-∘-≤ f g X) (map-≤ g (map-≤ f X≤Y)) + map-∘-comm f g {Y} X≤Y = Setoid.refl (S Y) + module _ (X : System A) where + opaque + unfolding map-∘-≤ map-∘-≥ + isoˡ : ≤-trans (map-∘-≤ f g X) (map-∘-≥ f g X) ≈ ≤-refl + isoˡ = Setoid.refl (S X) + isoʳ : ≤-trans (map-∘-≥ f g X) (map-∘-≤ f g X) ≈ ≤-refl + isoʳ = Setoid.refl (S X) - ≤-cong : (f : Fin A → Fin B) {X Y : System A} → Y ≤ X → map f Y ≤ map f X - ⇒S (≤-cong f x≤y) = ⇒S x≤y - ≗-fₛ (≤-cong f x≤y) = ≗-fₛ x≤y ∘ to (Pull.₁ f) - ≗-fₒ (≤-cong f x≤y) = cong (Push.₁ f) ∘ ≗-fₒ x≤y - System₁ : (Fin A → Fin B) → Systemₛ A ⟶ₛ Systemₛ B - to (System₁ f) = map f - cong (System₁ f) (x≤y , y≤x) = ≤-cong f x≤y , ≤-cong f y≤x +module _ {f g : Fin A → Fin B} (f≗g : f ≗ g) (X : System A) where opaque - unfolding System₁ - - id-x≤x : {X : System A} → System₁ id ⟨$⟩ X ≤ X - ⇒S (id-x≤x) = Id _ - ≗-fₛ (id-x≤x {_} {x}) i s = cong (System.fₛ x) Pull.identity - ≗-fₒ (id-x≤x {A} {x}) s = Push.identity - - x≤id-x : {x : System A} → x ≤ System₁ id ⟨$⟩ x - ⇒S x≤id-x = Id _ - ≗-fₛ (x≤id-x {A} {x}) i s = cong (System.fₛ x) (≋.sym Pull.identity) - ≗-fₒ (x≤id-x {A} {x}) s = ≋.sym Push.identity - - System-homomorphism - : {f : Fin A → Fin B} - {g : Fin B → Fin C}  - {X : System A} - → System₁ (g ∘ f) ⟨$⟩ X ≤ System₁ g ⟨$⟩ (System₁ f ⟨$⟩ X) - × System₁ g ⟨$⟩ (System₁ f ⟨$⟩ X) ≤ System₁ (g ∘ f) ⟨$⟩ X - System-homomorphism {f = f} {g} {X} = left , right - where - open System X - left : map (g ∘ f) X ≤ map g (map f X) - left .⇒S = Id S - left .≗-fₛ i s = cong fₛ Pull.homomorphism - left .≗-fₒ s = Push.homomorphism - right : map g (map f X) ≤ map (g ∘ f) X - right .⇒S = Id S - right .≗-fₛ i s = cong fₛ (≋.sym Pull.homomorphism) - right .≗-fₒ s = ≋.sym Push.homomorphism - - System-resp-≈ - : {f g : Fin A → Fin B} - → f ≗ g - → {X : System A} - → System₁ f ⟨$⟩ X ≤ System₁ g ⟨$⟩ X - × System₁ g ⟨$⟩ X ≤ System₁ f ⟨$⟩ X - System-resp-≈ {A} {B} {f = f} {g} f≗g {X} = both f≗g , both (≡.sym ∘ f≗g) - where - open System X - both : {f g : Fin A → Fin B} → f ≗ g → map f X ≤ map g X - both f≗g .⇒S = Id S - both f≗g .≗-fₛ i s = cong fₛ (Pull.F-resp-≈ f≗g {i}) - both {f} {g} f≗g .≗-fₒ s = Push.F-resp-≈ f≗g + unfolding map + + map-cong-≤ : map f X ≤ map g X + map-cong-≤ .⇒S = Id (S X) + map-cong-≤ .≗-fₛ i s = cong (fₛ X) (Pull.F-resp-≈ f≗g) + map-cong-≤ .≗-fₒ s = Push.F-resp-≈ f≗g + + map-cong-≥ : map g X ≤ map f X + map-cong-≥ .⇒S = Id (S X) + map-cong-≥ .≗-fₛ i s = cong (fₛ X) (Pull.F-resp-≈ (≡.sym ∘ f≗g)) + map-cong-≥ .≗-fₒ s = Push.F-resp-≈ (≡.sym ∘ f≗g) opaque - unfolding System₁ - Sys-defs : ⊤ - Sys-defs = tt - -Sys : Functor Nat (Setoids (suc 0ℓ) (suc 0ℓ)) -Sys .F₀ = Systemₛ -Sys .F₁ = System₁ -Sys .identity = id-x≤x , x≤id-x -Sys .homomorphism {x = X} = System-homomorphism {X = X} -Sys .F-resp-≈ = System-resp-≈ + unfolding map-≤ map-cong-≤ + map-cong-comm + : {f g : Fin A → Fin B} + (f≗g : f ≗ g) + {X Y : System A} + (h : X ≤ Y) + → ≤-trans (map-≤ f h) (map-cong-≤ f≗g Y) + ≈ ≤-trans (map-cong-≤ f≗g X) (map-≤ g h) + map-cong-comm f≗g {Y} h = Setoid.refl (S Y) + +opaque + + unfolding map-cong-≤ + + map-cong-isoˡ + : {f g : Fin A → Fin B} + (f≗g : f ≗ g) + (X : System A) + → ≤-trans (map-cong-≤ f≗g X) (map-cong-≥ f≗g X) ≈ ≤-refl + map-cong-isoˡ f≗g X = Setoid.refl (S X) + + map-cong-isoʳ + : {f g : Fin A → Fin B} + (f≗g : f ≗ g) + (X : System A) + → ≤-trans (map-cong-≥ f≗g X) (map-cong-≤ f≗g X) ≈ ≤-refl + map-cong-isoʳ f≗g X = Setoid.refl (S X) + +Sys-resp-≈ : {f g : Fin A → Fin B} → f ≗ g → Sys₁ f ≃ Sys₁ g +Sys-resp-≈ f≗g = niHelper record + { η = map-cong-≤ f≗g + ; η⁻¹ = map-cong-≥ f≗g + ; commute = map-cong-comm f≗g + ; iso = λ X → record + { isoˡ = map-cong-isoˡ f≗g X + ; isoʳ = map-cong-isoʳ f≗g X + } + } + +Sys : Functor Nat (Cats (suc 0ℓ) (suc 0ℓ) 0ℓ) +Sys .F₀ = Systems +Sys .F₁ = Sys₁ +Sys .identity = Sys-identity +Sys .homomorphism = Sys-homo _ _ +Sys .F-resp-≈ = Sys-resp-≈ module Sys = Functor Sys -- cgit v1.2.3