diff options
| -rw-r--r-- | Functor/Instance/WiringDiagram/System.agda | 131 |
1 files changed, 46 insertions, 85 deletions
diff --git a/Functor/Instance/WiringDiagram/System.agda b/Functor/Instance/WiringDiagram/System.agda index 753f0f0..80a4fe5 100644 --- a/Functor/Instance/WiringDiagram/System.agda +++ b/Functor/Instance/WiringDiagram/System.agda @@ -2,8 +2,6 @@ open import Categories.Category using (Category) open import Categories.Category.Cartesian.Bundle using (CartesianCategory) -open import Categories.Category.Cartesian.Monoidal using (module CartesianMonoidal) -open import Categories.Category.Cocartesian.Monoidal using (module CocartesianMonoidal) open import Categories.Category.Instance.Cats using (Cats) open import Categories.Functor using (Functor; _∘F_) renaming (id to IdF) open import Categories.Functor.Cartesian using (CartesianF) @@ -12,9 +10,6 @@ open import Category.Dagger.Semiadditive using (IdempotentSemiadditiveDagger) open import Category.Instance.CMonoids using (CMonoids; CMonoidHomomorphism) open import Level using (Level; suc) -open CartesianMonoidal using (monoidal) -open CocartesianMonoidal using (+-monoidal) - module Functor.Instance.WiringDiagram.System {o ℓ e o′ ℓ′ e′ : Level} {c : Level} @@ -47,8 +42,8 @@ open import Data.Setoid using (_⇒ₛ_; ∣_∣) open import Data.Setoid.Unit using (⊤ₛ) open import Data.System using (System; _≤_; Systems[_,_]; Systems-SMC; discrete) open import Data.Unit.Polymorphic using (tt) -open import Data.WiringDiagram.Core S using (Box; WiringDiagram; _□_; _⧈_; _⌻_; _≈-⧈_) -open import Data.WiringDiagram.Directed S using (DWD; Pulsh) +open import Data.WiringDiagram.Core S.semiadditiveDagger using (Box; WiringDiagram; _□_; _⧈_; _⌻_; _≈-⧈_) +open import Data.WiringDiagram.Directed S.semiadditiveDagger using (DWD; Pulsh) open import Function using (Func; _⟶ₛ_; _⟨$⟩_; id; _$_) open import Function.Construct.Identity using () renaming (function to Id) open import Function.Construct.Setoid using (_∙_) @@ -62,19 +57,17 @@ open CMonoidHomomorphism open Category 𝒞 using (Obj; _⇒_; _∘_) open CommutativeMonoid using (setoid; Carrier; refl; sym) open Func -open IdempotentSemiadditiveDagger S using (_⊕₀_; _⊕₁_; △) -open Shorthands (+-monoidal S.cocartesian) using (α⇒) -open Shorthands (monoidal S.cartesian) using () renaming (α⇒ to α⇒′) +open IdempotentSemiadditiveDagger S using (_⊕_; _×₁_) open WiringDiagram using (input; output) -_⟦⊕⟧_ : {A B : Obj} → Carrier (F.₀ A) → Carrier (F.₀ B) → Carrier (F.₀ (A ⊕₀ B)) +_⟦⊕⟧_ : {A B : Obj} → Carrier (F.₀ A) → Carrier (F.₀ B) → Carrier (F.₀ (A ⊕ B)) _⟦⊕⟧_ {A} {B} a b = ⟦ F.×-iso.to A B ⟧ (a , b) ⟦⊕⟧-cong : {A B : Obj} (let module FA = CommutativeMonoid (F.₀ A)) (let module FB = CommutativeMonoid (F.₀ B)) - (let module F[A+B] = CommutativeMonoid (F.₀ (A ⊕₀ B))) + (let module F[A+B] = CommutativeMonoid (F.₀ (A ⊕ B))) {a a′ : Carrier (F.₀ A)} {b b′ : Carrier (F.₀ B)} → a FA.≈ a′ @@ -88,50 +81,14 @@ _⟦⊕⟧_ {A} {B} a b = ⟦ F.×-iso.to A B ⟧ (a , b) {g : C ⇒ D} (a : Carrier (F.₀ A)) (c : Carrier (F.₀ C)) - → (let open CommutativeMonoid (F.₀ (B ⊕₀ D)) using (_≈_)) - → ⟦ F.₁ (f ⊕₁ g) ⟧ (a ⟦⊕⟧ c) ≈ ⟦ F.₁ f ⟧ a ⟦⊕⟧ ⟦ F.₁ g ⟧ c + → (let open CommutativeMonoid (F.₀ (B ⊕ D)) using (_≈_)) + → ⟦ F.₁ (f ×₁ g) ⟧ (a ⟦⊕⟧ c) ≈ ⟦ F.₁ f ⟧ a ⟦⊕⟧ ⟦ F.₁ g ⟧ c ⟦⊕⟧-commute {A} {B} {C} {D} {f} {g} a c- = begin - ⟦ F.₁ (f ⊕₁ g) ⟧ (a ⟦⊕⟧ c-) ≈⟨ F.F-resp-≈ (S.×₁-⊕₁ f g) (a ⟦⊕⟧ c-) ⟨ ⟦ F.₁ (f ×₁ g) ⟧ (a ⟦⊕⟧ c-) ≈⟨ ⊗-F.⊗-homo.sym-commute (f , g) (a , c-) ⟩ ⟦ F.₁ f ⟧ a ⟦⊕⟧ ⟦ F.₁ g ⟧ c- ∎ where - open ≈-Reasoning (setoid (F.₀ (B ⊕₀ D))) - open CommutativeMonoid (F.₀ (B ⊕₀ D)) using (_≈_) - module 𝒞-CC = CartesianCategory 𝒞-CC - open 𝒞-CC using (_×₁_) - ⊗-F : MonoidalFunctor 𝒞-CC.monoidalCategory (CMonoids-CC.monoidalCategory {c} {c}) - ⊗-F = isMonoidalFunctor {C = 𝒞-CC} {CMonoids-CC {c} {c}} F - module ⊗-F = MonoidalFunctor ⊗-F - -⟦△⟧ : {A : Obj} - (a : Carrier (F.₀ A)) - → (let open CommutativeMonoid (F.₀ (A ⊕₀ A)) using (_≈_)) - → ⟦ F.₁ △ ⟧ a ≈ a ⟦⊕⟧ a -⟦△⟧ {A} a = begin - ⟦ F.₁ △ ⟧ a ≈⟨ F.identity ((⟦ F.₁ △ ⟧ a)) ⟨ - ⟦ F.₁ 𝒞.id ⟧ (⟦ F.₁ △ ⟧ a) ≈⟨ F.F-resp-≈ ⊕.identity (⟦ F.₁ △ ⟧ a) ⟨ - ⟦ F.₁ (𝒞.id ⊕₁ 𝒞.id) ⟧ (⟦ F.₁ △ ⟧ a) ≈⟨ F.homomorphism a ⟨ - ⟦ F.₁ (𝒞.id ⊕₁ 𝒞.id ∘ △) ⟧ a ≈⟨ switch-fromtoˡ (F.×-iso A A) {h = F.₁ (𝒞.id ⊕₁ 𝒞.id ∘ △)} {k = CMonoids-CC.⟨ F.₁ 𝒞.id , F.₁ 𝒞.id ⟩} (F.F-resp-⟨⟩ 𝒞.id 𝒞.id) a ⟩ - ⟦ F.₁ 𝒞.id ⟧ a ⟦⊕⟧ ⟦ F.₁ 𝒞.id ⟧ a ≈⟨ ⟦⊕⟧-cong (F.identity a) (F.identity a) ⟩ - a ⟦⊕⟧ a ∎ - where - open ≈-Reasoning (setoid (F.₀ (A ⊕₀ A))) - open Product (F.F-prod A A) using (⟨⟩-cong₂) - module ⊕ = Functor S.⊕ - -⟦α⇒⟧ - : {A B C : Obj} - (a : Carrier (F.₀ A)) - (b : Carrier (F.₀ B)) - (c : Carrier (F.₀ C)) - → (let open CommutativeMonoid (F.₀ (A ⊕₀ (B ⊕₀ C))) using (_≈_)) - → ⟦ F.₁ α⇒ ⟧ ((a ⟦⊕⟧ b) ⟦⊕⟧ c) ≈ a ⟦⊕⟧ (b ⟦⊕⟧ c) -⟦α⇒⟧ {A} {B} {C} a b c- = begin - ⟦ F.₁ α⇒ ⟧ ((a ⟦⊕⟧ b) ⟦⊕⟧ c-) ≈⟨ F.F-resp-≈ S.≈α⇒ ((a ⟦⊕⟧ b) ⟦⊕⟧ c-) ⟨ - ⟦ F.₁ α⇒′ ⟧ ((a ⟦⊕⟧ b) ⟦⊕⟧ c-) ≈⟨ ⊗-F.associativity ((a , b) , c-) ⟩ - a ⟦⊕⟧ (b ⟦⊕⟧ c-) ∎ - where - open ≈-Reasoning (setoid (F.₀ (A ⊕₀ (B ⊕₀ C)))) + open ≈-Reasoning (setoid (F.₀ (B ⊕ D))) + open CommutativeMonoid (F.₀ (B ⊕ D)) using (_≈_) module 𝒞-CC = CartesianCategory 𝒞-CC ⊗-F : MonoidalFunctor 𝒞-CC.monoidalCategory (CMonoids-CC.monoidalCategory {c} {c}) ⊗-F = isMonoidalFunctor {C = 𝒞-CC} {CMonoids-CC {c} {c}} F @@ -140,7 +97,7 @@ _⟦⊕⟧_ {A} {B} a b = ⟦ F.×-iso.to A B ⟧ (a , b) ⟦⊕⟧-congˡ : {A B : Obj} (let module FB = CommutativeMonoid (F.₀ B)) - (let module F[A+B] = CommutativeMonoid (F.₀ (A ⊕₀ B))) + (let module F[A+B] = CommutativeMonoid (F.₀ (A ⊕ B))) {a : Carrier (F.₀ A)} {b b′ : Carrier (F.₀ B)} → b FB.≈ b′ @@ -151,14 +108,14 @@ _⟦⊕⟧_ {A} {B} a b = ⟦ F.×-iso.to A B ⟧ (a , b) ⟦⊕⟧-congʳ : {A B : Obj} (let module FA = CommutativeMonoid (F.₀ A)) - (let module F[A+B] = CommutativeMonoid (F.₀ (A ⊕₀ B))) + (let module F[A+B] = CommutativeMonoid (F.₀ (A ⊕ B))) {a a′ : Carrier (F.₀ A)} {b : Carrier (F.₀ B)} → a FA.≈ a′ → a ⟦⊕⟧ b F[A+B].≈ a′ ⟦⊕⟧ b ⟦⊕⟧-congʳ {B = B} ≈a = ⟦⊕⟧-cong ≈a (refl (F.₀ B)) -module _ {Aᵢ Aₒ Bᵢ Bₒ : Obj} (i : Aₒ ⊕₀ Bᵢ ⇒ Aᵢ) (o : Aₒ ⇒ Bₒ) where +module _ {Aᵢ Aₒ Bᵢ Bₒ : Obj} (i : Aₒ ⊕ Bᵢ ⇒ Aᵢ) (o : Aₒ ⇒ Bₒ) where A-System B-System : Set (suc c) A-System = System (setoid (F.₀ Aᵢ)) (F.₀ Aₒ) @@ -168,7 +125,7 @@ module _ {Aᵢ Aₒ Bᵢ Bₒ : Obj} (i : Aₒ ⊕₀ Bᵢ ⇒ Aᵢ) (o : Aₒ A-Systems = Systems[ setoid (F.₀ Aᵢ) , F.₀ Aₒ ] B-Systems = Systems[ setoid (F.₀ Bᵢ) , F.₀ Bₒ ] - I⇒ : CMonoidHomomorphism c c (F.₀ (Aₒ ⊕₀ Bᵢ)) (F.₀ Aᵢ) + I⇒ : CMonoidHomomorphism c c (F.₀ (Aₒ ⊕ Bᵢ)) (F.₀ Aᵢ) I⇒ = F.₁ i O⇒ : CMonoidHomomorphism c c (F.₀ Aₒ) (F.₀ Bₒ) @@ -223,7 +180,7 @@ module _ {Aᵢ Aₒ Bᵢ Bₒ : Obj} (i : Aₒ ⊕₀ Bᵢ ⇒ Aᵢ) (o : Aₒ ; F-resp-≈ = id } -identity : {Aᵢ Aₒ : Obj} → Wire {Aᵢ} {Aₒ} S.p₂ 𝒞.id ≃ IdF +identity : {Aᵢ Aₒ : Obj} → Wire {Aᵢ} {Aₒ} S.π₂ 𝒞.id ≃ IdF identity {Aᵢ} {Aₒ} = niHelper record { η = ≤X ; η⁻¹ = ≥X @@ -237,13 +194,13 @@ identity {Aᵢ} {Aₒ} = niHelper record module _ (X : System (setoid (F.₀ Aᵢ)) (F.₀ Aₒ)) where module X = System X open IsProduct F.F-resp-× using (project₂) - ≤X : wire S.p₂ 𝒞.id X ≤ X + ≤X : wire S.π₂ 𝒞.id X ≤ X ≤X = record { ⇒S = Id X.S ; ≗-fₛ = λ i s → cong X.fₛ (project₂ (X.fₒ′ s , i)) ; ≗-fₒ = λ s → F.identity (X.fₒ′ s) } - ≥X : X ≤ wire S.p₂ 𝒞.id X + ≥X : X ≤ wire S.π₂ 𝒞.id X ≥X = record { ⇒S = Id X.S ; ≗-fₛ = λ i s → X.S.sym (cong X.fₛ (project₂ (X.fₒ′ s , i))) @@ -252,9 +209,9 @@ identity {Aᵢ} {Aₒ} = niHelper record homomorphism : {Xᵢ Xₒ Yᵢ Yₒ Zᵢ Zₒ : Obj} - {fᵢ : Xₒ ⊕₀ Yᵢ ⇒ Xᵢ} + {fᵢ : Xₒ ⊕ Yᵢ ⇒ Xᵢ} {fₒ : Xₒ ⇒ Yₒ} - {gᵢ : Yₒ ⊕₀ Zᵢ ⇒ Yᵢ} + {gᵢ : Yₒ ⊕ Zᵢ ⇒ Yᵢ} {gₒ : Yₒ ⇒ Zₒ} → Wire (input ((gᵢ ⧈ gₒ) ⌻ (fᵢ ⧈ fₒ))) (output ((gᵢ ⧈ gₒ) ⌻ (fᵢ ⧈ fₒ))) ≃ Wire gᵢ gₒ ∘F Wire fᵢ fₒ @@ -273,45 +230,49 @@ homomorphism {Xᵢ} {Xₒ} {Yᵢ} {Yₒ} {Zᵢ} {Zₒ} {fᵢ} {fₒ} {gᵢ} {g module _ (i : Carrier (F.₀ Zᵢ)) (s : ∣ X.S ∣) where lem₁ : (let open CommutativeMonoid (F.₀ Yᵢ) using (_≈_)) - → ⟦ F.₁ (gᵢ ∘ fₒ ⊕₁ 𝒞.id) ⟧ (X.fₒ′ s ⟦⊕⟧ i) ≈ ⟦ F.₁ gᵢ ⟧ (⟦ F.₁ fₒ ⟧ (X.fₒ′ s) ⟦⊕⟧ i) + → ⟦ F.₁ (gᵢ ∘ fₒ ×₁ 𝒞.id) ⟧ (X.fₒ′ s ⟦⊕⟧ i) ≈ ⟦ F.₁ gᵢ ⟧ (⟦ F.₁ fₒ ⟧ (X.fₒ′ s) ⟦⊕⟧ i) lem₁ = begin - ⟦ F.₁ (gᵢ ∘ fₒ ⊕₁ 𝒞.id) ⟧ (X.fₒ′ s ⟦⊕⟧ i) ≈⟨ F.homomorphism (X.fₒ′ s ⟦⊕⟧ i) ⟩ - ⟦ F.₁ gᵢ ⟧ (⟦ F.₁ (fₒ ⊕₁ 𝒞.id) ⟧ (X.fₒ′ s ⟦⊕⟧ i)) ≈⟨ ⟦⟧-cong (F.₁ gᵢ) (⟦⊕⟧-commute (X.fₒ′ s) i) ⟩ + ⟦ F.₁ (gᵢ ∘ fₒ ×₁ 𝒞.id) ⟧ (X.fₒ′ s ⟦⊕⟧ i) ≈⟨ F.homomorphism (X.fₒ′ s ⟦⊕⟧ i) ⟩ + ⟦ F.₁ gᵢ ⟧ (⟦ F.₁ (fₒ ×₁ 𝒞.id) ⟧ (X.fₒ′ s ⟦⊕⟧ i)) ≈⟨ ⟦⟧-cong (F.₁ gᵢ) (⟦⊕⟧-commute (X.fₒ′ s) i) ⟩ ⟦ F.₁ gᵢ ⟧ (⟦ F.₁ fₒ ⟧ (X.fₒ′ s) ⟦⊕⟧ ⟦ F.₁ 𝒞.id ⟧ i) ≈⟨ ⟦⟧-cong (F.₁ gᵢ) (⟦⊕⟧-congˡ (F.identity i)) ⟩ ⟦ F.₁ gᵢ ⟧ (⟦ F.₁ fₒ ⟧ (X.fₒ′ s) ⟦⊕⟧ i) ∎ where open ≈-Reasoning (setoid (F.₀ Yᵢ)) lem₂ - : (let open CommutativeMonoid (F.₀ (Xₒ ⊕₀ (Xₒ ⊕₀ Zᵢ))) using (_≈_)) - → ⟦ F.₁ (α⇒ 𝒞.∘ △ ⊕₁ 𝒞.id) ⟧ (X.fₒ′ s ⟦⊕⟧ i) + : (let open CommutativeMonoid (F.₀ (Xₒ ⊕ (Xₒ ⊕ Zᵢ))) using (_≈_)) + → ⟦ F.₁ S.⟨ S.π₁ , 𝒞.id ⟩ ⟧ (X.fₒ′ s ⟦⊕⟧ i) ≈ X.fₒ′ s ⟦⊕⟧ (X.fₒ′ s ⟦⊕⟧ i) lem₂ = begin - ⟦ F.₁ (α⇒ 𝒞.∘ △ ⊕₁ 𝒞.id) ⟧ (X.fₒ′ s ⟦⊕⟧ i) ≈⟨ F.homomorphism (X.fₒ′ s ⟦⊕⟧ i) ⟩ - ⟦ F.₁ α⇒ ⟧ (⟦ F.₁ (△ ⊕₁ 𝒞.id) ⟧ (X.fₒ′ s ⟦⊕⟧ i)) ≈⟨ ⟦⟧-cong (F.₁ α⇒) (⟦⊕⟧-commute (X.fₒ′ s) i) ⟩ - ⟦ F.₁ α⇒ ⟧ (⟦ F.₁ △ ⟧ (X.fₒ′ s) ⟦⊕⟧ ⟦ F.₁ 𝒞.id ⟧ i) ≈⟨ ⟦⟧-cong (F.₁ α⇒) (⟦⊕⟧-cong (⟦△⟧ (X.fₒ′ s)) (F.identity i)) ⟩ - ⟦ F.₁ α⇒ ⟧ ((X.fₒ′ s ⟦⊕⟧ X.fₒ′ s) ⟦⊕⟧ i) ≈⟨ ⟦α⇒⟧ (X.fₒ′ s) (X.fₒ′ s) i ⟩ - X.fₒ′ s ⟦⊕⟧ (X.fₒ′ s ⟦⊕⟧ i) ∎ + ⟦ F.₁ S.⟨ S.π₁ , 𝒞.id ⟩ ⟧ (X.fₒ′ s ⟦⊕⟧ i) ≈⟨ switch-fromtoˡ (F.×-iso Xₒ (Xₒ ⊕ Zᵢ)) {h = h} {k = k} (F.F-resp-⟨⟩ S.π₁ 𝒞.id) (X.fₒ′ s ⟦⊕⟧ i) ⟩ + ⟦ F.₁ S.π₁ ⟧ (X.fₒ′ s ⟦⊕⟧ i) ⟦⊕⟧ ⟦ F.₁ 𝒞.id ⟧ (X.fₒ′ s ⟦⊕⟧ i) ≈⟨ ⟦⊕⟧-cong (F.F-resp-×.project₁ (X.fₒ′ s , i)) (F.identity (X.fₒ′ s ⟦⊕⟧ i)) ⟩ + X.fₒ′ s ⟦⊕⟧ (X.fₒ′ s ⟦⊕⟧ i) ∎ where - open ≈-Reasoning (setoid (F.₀ (Xₒ ⊕₀ (Xₒ ⊕₀ Zᵢ)))) + h : CMonoidHomomorphism c c (F.₀ (Xₒ ⊕ Zᵢ)) (F.₀ (Xₒ ⊕ (Xₒ ⊕ Zᵢ))) + h = F.₁ _ + k : CMonoidHomomorphism c c (F.₀ (Xₒ ⊕ Zᵢ)) _ + k = CMonoids-CC.⟨ F.₁ _ , F.₁ _ ⟩ + open ≈-Reasoning (setoid (F.₀ (Xₒ ⊕ (Xₒ ⊕ Zᵢ)))) lem₃ - : (let open CommutativeMonoid (F.₀ (Xₒ ⊕₀ Yᵢ)) using (_≈_)) - → ⟦ F.₁ (𝒞.id ⊕₁ (gᵢ ∘ fₒ ⊕₁ 𝒞.id) 𝒞.∘ α⇒ 𝒞.∘ △ ⊕₁ 𝒞.id) ⟧ (X.fₒ′ s ⟦⊕⟧ i) + : (let open CommutativeMonoid (F.₀ (Xₒ ⊕ Yᵢ)) using (_≈_)) + → ⟦ F.₁ S.⟨ S.π₁ , gᵢ ∘ fₒ ×₁ 𝒞.id ⟩ ⟧ (X.fₒ′ s ⟦⊕⟧ i) ≈ (X.fₒ′ s ⟦⊕⟧ (⟦ F.₁ gᵢ ⟧ (⟦ F.₁ fₒ ⟧ (X.fₒ′ s) ⟦⊕⟧ i))) lem₃ = begin - ⟦ F.₁ (𝒞.id ⊕₁ (gᵢ ∘ fₒ ⊕₁ 𝒞.id) 𝒞.∘ α⇒ 𝒞.∘ △ ⊕₁ 𝒞.id) ⟧ (X.fₒ′ s ⟦⊕⟧ i) ≈⟨ F.homomorphism (X.fₒ′ s ⟦⊕⟧ i) ⟩ - ⟦ F.₁ (𝒞.id ⊕₁ (gᵢ ∘ fₒ ⊕₁ 𝒞.id)) ⟧ (⟦ F.₁ (α⇒ 𝒞.∘ △ ⊕₁ 𝒞.id) ⟧ (X.fₒ′ s ⟦⊕⟧ i)) ≈⟨ ⟦⟧-cong (F.₁ (𝒞.id ⊕₁ (gᵢ ∘ fₒ ⊕₁ 𝒞.id))) lem₂ ⟩ - ⟦ F.₁ (𝒞.id ⊕₁ (gᵢ ∘ fₒ ⊕₁ 𝒞.id)) ⟧ (X.fₒ′ s ⟦⊕⟧ (X.fₒ′ s ⟦⊕⟧ i)) ≈⟨ ⟦⊕⟧-commute (X.fₒ′ s) (X.fₒ′ s ⟦⊕⟧ i) ⟩ - ⟦ F.₁ 𝒞.id ⟧ (X.fₒ′ s) ⟦⊕⟧ ⟦ F.₁ (gᵢ ∘ fₒ ⊕₁ 𝒞.id) ⟧ (X.fₒ′ s ⟦⊕⟧ i) ≈⟨ ⟦⊕⟧-cong (F.identity (X.fₒ′ s)) lem₁ ⟩ - X.fₒ′ s ⟦⊕⟧ ⟦ F.₁ gᵢ ⟧ (⟦ F.₁ fₒ ⟧ (X.fₒ′ s) ⟦⊕⟧ i) ∎ + ⟦ F.₁ S.⟨ S.π₁ , gᵢ ∘ fₒ ×₁ 𝒞.id ⟩ ⟧ (X.fₒ′ s ⟦⊕⟧ i) ≈⟨ F.F-resp-≈ (S.⟨⟩-congˡ 𝒞.identityʳ) (X.fₒ′ s ⟦⊕⟧ i) ⟨ + ⟦ F.₁ S.⟨ S.π₁ , (gᵢ ∘ fₒ ×₁ 𝒞.id) ∘ 𝒞.id ⟩ ⟧ (X.fₒ′ s ⟦⊕⟧ i) ≈⟨ F.F-resp-≈ S.second∘⟨⟩ (X.fₒ′ s ⟦⊕⟧ i) ⟨ + ⟦ F.₁ (𝒞.id ×₁ (gᵢ ∘ fₒ ×₁ 𝒞.id) ∘ S.⟨ S.π₁ , 𝒞.id ⟩) ⟧ (X.fₒ′ s ⟦⊕⟧ i) ≈⟨ F.homomorphism (X.fₒ′ s ⟦⊕⟧ i) ⟩ + ⟦ F.₁ (𝒞.id ×₁ (gᵢ ∘ fₒ ×₁ 𝒞.id)) ⟧ (⟦ F.₁ S.⟨ S.π₁ , 𝒞.id ⟩ ⟧ (X.fₒ′ s ⟦⊕⟧ i)) ≈⟨ ⟦⟧-cong (F.₁ (𝒞.id ×₁ (gᵢ ∘ fₒ ×₁ 𝒞.id))) lem₂ ⟩ + ⟦ F.₁ (𝒞.id ×₁ (gᵢ ∘ fₒ ×₁ 𝒞.id)) ⟧ (X.fₒ′ s ⟦⊕⟧ (X.fₒ′ s ⟦⊕⟧ i)) ≈⟨ ⟦⊕⟧-commute (X.fₒ′ s) (X.fₒ′ s ⟦⊕⟧ i) ⟩ + ⟦ F.₁ 𝒞.id ⟧ (X.fₒ′ s) ⟦⊕⟧ ⟦ F.₁ (gᵢ ∘ fₒ ×₁ 𝒞.id) ⟧ (X.fₒ′ s ⟦⊕⟧ i) ≈⟨ ⟦⊕⟧-cong (F.identity (X.fₒ′ s)) lem₁ ⟩ + X.fₒ′ s ⟦⊕⟧ ⟦ F.₁ gᵢ ⟧ (⟦ F.₁ fₒ ⟧ (X.fₒ′ s) ⟦⊕⟧ i) ∎ where - open ≈-Reasoning (setoid (F.₀ (Xₒ ⊕₀ Yᵢ))) + open ≈-Reasoning (setoid (F.₀ (Xₒ ⊕ Yᵢ))) ≗-fₛ - : X.fₛ′ (⟦ F.₁ (fᵢ ∘ 𝒞.id ⊕₁ (gᵢ ∘ fₒ ⊕₁ 𝒞.id) 𝒞.∘ α⇒ 𝒞.∘ △ ⊕₁ 𝒞.id) ⟧ (X.fₒ′ s ⟦⊕⟧ i)) s X.S.≈ + : X.fₛ′ (⟦ F.₁ (fᵢ ∘ S.⟨ S.π₁ , gᵢ ∘ fₒ ×₁ 𝒞.id ⟩) ⟧ (X.fₒ′ s ⟦⊕⟧ i)) s X.S.≈ X.fₛ′ (⟦ F.₁ fᵢ ⟧ (X.fₒ′ s ⟦⊕⟧ (⟦ F.₁ gᵢ ⟧ (⟦ F.₁ fₒ ⟧ (X.fₒ′ s) ⟦⊕⟧ i)))) s ≗-fₛ = cong X.fₛ $ begin - ⟦ F.₁ (fᵢ ∘ 𝒞.id ⊕₁ (gᵢ ∘ fₒ ⊕₁ 𝒞.id) 𝒞.∘ α⇒ 𝒞.∘ △ ⊕₁ 𝒞.id) ⟧ (X.fₒ′ s ⟦⊕⟧ i) ≈⟨ F.homomorphism (X.fₒ′ s ⟦⊕⟧ i) ⟩ - ⟦ F.₁ fᵢ ⟧ (⟦ F.₁ (𝒞.id ⊕₁ (gᵢ ∘ fₒ ⊕₁ 𝒞.id) 𝒞.∘ α⇒ 𝒞.∘ △ ⊕₁ 𝒞.id) ⟧ (X.fₒ′ s ⟦⊕⟧ i)) ≈⟨ ⟦⟧-cong (F.₁ fᵢ) lem₃ ⟩ - ⟦ F.₁ fᵢ ⟧ (X.fₒ′ s ⟦⊕⟧ ⟦ F.₁ gᵢ ⟧ (⟦ F.₁ fₒ ⟧ (X.fₒ′ s) ⟦⊕⟧ i)) ∎ + ⟦ F.₁ (fᵢ ∘ S.⟨ S.π₁ , gᵢ ∘ fₒ ×₁ 𝒞.id ⟩) ⟧ (X.fₒ′ s ⟦⊕⟧ i) ≈⟨ F.homomorphism (X.fₒ′ s ⟦⊕⟧ i) ⟩ + ⟦ F.₁ fᵢ ⟧ (⟦ F.₁ S.⟨ S.π₁ , gᵢ ∘ fₒ ×₁ 𝒞.id ⟩ ⟧ (X.fₒ′ s ⟦⊕⟧ i)) ≈⟨ ⟦⟧-cong (F.₁ fᵢ) lem₃ ⟩ + ⟦ F.₁ fᵢ ⟧ (X.fₒ′ s ⟦⊕⟧ ⟦ F.₁ gᵢ ⟧ (⟦ F.₁ fₒ ⟧ (X.fₒ′ s) ⟦⊕⟧ i)) ∎ where open ≈-Reasoning (setoid (F.₀ Xᵢ)) η : wire (input ((gᵢ ⧈ gₒ) ⌻ (fᵢ ⧈ fₒ))) (output ((gᵢ ⧈ gₒ) ⌻ (fᵢ ⧈ fₒ))) X ≤ wire gᵢ gₒ (wire fᵢ fₒ X) @@ -346,7 +307,7 @@ Sys-resp-≈ {A} {B} {f} {g} f≈g = niHelper record module B = Box B module _ (X : System (setoid (F.₀ A.ᵢ)) (F.₀ A.ₒ)) where - fᵢ gᵢ : A.ₒ ⊕₀ B.ᵢ ⇒ A.ᵢ + fᵢ gᵢ : A.ₒ ⊕ B.ᵢ ⇒ A.ᵢ fᵢ = input f gᵢ = input g |