diff options
Diffstat (limited to 'DecorationFunctor')
| -rw-r--r-- | DecorationFunctor/Graph.agda | 565 | ||||
| -rw-r--r-- | DecorationFunctor/Hypergraph.agda | 653 | ||||
| -rw-r--r-- | DecorationFunctor/Hypergraph/Labeled.agda | 689 | ||||
| -rw-r--r-- | DecorationFunctor/Trivial.agda | 98 |
4 files changed, 1619 insertions, 386 deletions
diff --git a/DecorationFunctor/Graph.agda b/DecorationFunctor/Graph.agda index 7f05855..8b62430 100644 --- a/DecorationFunctor/Graph.agda +++ b/DecorationFunctor/Graph.agda @@ -4,62 +4,48 @@ module DecorationFunctor.Graph where import Categories.Morphism as Morphism +open import Level using (0ℓ) + open import Categories.Category.BinaryProducts using (module BinaryProducts) open import Categories.Category.Cartesian using (Cartesian) -open import Categories.Category.Cocartesian using (Cocartesian; module BinaryCoproducts) -open import Categories.Category.Core using (Category) -open import Categories.Category.Instance.Nat using (Nat-Cocartesian) open import Categories.Category.Instance.Nat using (Nat) open import Categories.Category.Instance.Setoids using (Setoids) -open import Categories.Category.Instance.SingletonSet using (SingletonSetoid) open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian) open import Categories.Category.Product using (_⁂_) open import Categories.Functor using () renaming (_∘F_ to _∘′_) open import Categories.Functor.Core using (Functor) open import Categories.Functor.Monoidal.Symmetric using (module Lax) -open import Categories.NaturalTransformation using (NaturalTransformation) - +open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory) -open import Category.Instance.Setoids.SymmetricMonoidal using (Setoids-×) open import Category.Instance.Nat.FinitelyCocomplete using (Nat-FinitelyCocomplete) - +open import Category.Instance.Setoids.SymmetricMonoidal {0ℓ} {0ℓ} using (Setoids-×; ×-symmetric′) open import Data.Empty using (⊥-elim) -open import Data.Fin using (#_) -open import Data.Fin.Base using (Fin; splitAt; join; zero; suc; _↑ˡ_; _↑ʳ_) +open import Data.Fin using (#_; Fin; splitAt; join; zero; suc; _↑ˡ_; _↑ʳ_) open import Data.Fin.Patterns using (0F; 1F) -open import Data.Fin.Properties using (splitAt-join; join-splitAt) +open import Data.Fin.Properties using (splitAt-join; join-splitAt; splitAt-↑ˡ; splitAt⁻¹-↑ˡ) open import Data.Nat using (ℕ; _+_) open import Data.Product.Base using (_,_) open import Data.Product.Relation.Binary.Pointwise.NonDependent using (×-setoid) +open import Data.Setoid.Unit {0ℓ} {0ℓ} using (⊤ₛ) open import Data.Sum.Base using (_⊎_; map; inj₁; inj₂; swap) renaming ([_,_]′ to [_,_]) open import Data.Sum.Properties using (map-map; [,]-map; [,]-∘; [-,]-cong; [,-]-cong; map-cong; swap-involutive) open import Data.Unit using (tt) -open import Data.Unit.Properties using () renaming (≡-setoid to ⊤-setoid) - -open import Function.Base using (_∘_; id; const; case_of_) -open import Function.Bundles using (Func; Inverse; _↔_; mk↔) +open import Function using (_∘_; id; const; Func; Inverse; _↔_; mk↔) open import Function.Construct.Composition using (_↔-∘_) +open import Function.Construct.Constant using () renaming (function to Const) open import Function.Construct.Identity using (↔-id) open import Function.Construct.Symmetry using (↔-sym) - -open import Level using (0ℓ; lift) - -open import Relation.Binary.Bundles using (Setoid) -open import Relation.Binary.PropositionalEquality using (_≗_) -open import Relation.Binary.PropositionalEquality.Core using (_≡_; erefl; refl; sym; trans; cong) +open import Relation.Binary using (Setoid) +open import Relation.Binary.PropositionalEquality using (_≗_; _≡_; erefl; refl; sym; trans; cong) open import Relation.Binary.PropositionalEquality.Properties using (isEquivalence; module ≡-Reasoning) open import Relation.Nullary.Negation.Core using (¬_) open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using (products) -open Cocartesian Nat-Cocartesian using (coproducts) open FinitelyCocompleteCategory Nat-FinitelyCocomplete - using () - renaming (symmetricMonoidalCategory to Nat-smc) -open Morphism (Setoids 0ℓ 0ℓ) using (_≅_) + using (-+-) + renaming (symmetricMonoidalCategory to Nat-smc; +-assoc to Nat-+-assoc) open Lax using (SymmetricMonoidalFunctor) - open BinaryProducts products using (-×-) -open BinaryCoproducts coproducts using (-+-) renaming (+-assoc to Nat-+-assoc) record Graph (v : ℕ) : Set where @@ -164,50 +150,33 @@ Graph-Func f = record F-resp-≈ : {f g : Fin n → Fin m} → (∀ (x : Fin n) → f x ≡ g x) - → Graph-same G G′ - → Graph-same (map-nodes f G) (map-nodes g G′) -F-resp-≈ {g = g} f≗g ≡G = record - { ↔e = ↔e - ; ≗s = λ { x → trans (f≗g (s x)) (cong g (≗s x)) } - ; ≗t = λ { x → trans (f≗g (t x)) (cong g (≗t x)) } + → Graph-same (map-nodes f G) (map-nodes g G) +F-resp-≈ {G = G} f≗g = record + { ↔e = ↔-id _ + ; ≗s = f≗g ∘ s + ; ≗t = f≗g ∘ t } where - open Graph-same ≡G + open Graph G F : Functor Nat (Setoids 0ℓ 0ℓ) F = record { F₀ = Graph-setoid ; F₁ = Graph-Func - ; identity = id - ; homomorphism = λ { {_} {_} {_} {f} {g} → homomorphism f g } + ; identity = Graph-same-refl + ; homomorphism = Graph-same-refl ; F-resp-≈ = λ f≗g → F-resp-≈ f≗g } - where - homomorphism - : (f : Fin n → Fin m) - → (g : Fin m → Fin o) - → Graph-same G G′ - → Graph-same (map-nodes (g ∘ f) G) (map-nodes g (map-nodes f G′)) - homomorphism f g ≡G = record - { ↔e = ↔e - ; ≗s = cong (g ∘ f) ∘ ≗s - ; ≗t = cong (g ∘ f) ∘ ≗t - } - where - open Graph-same ≡G -empty-graph : Graph 0 -empty-graph = record +discrete : {n : ℕ} → Graph n +discrete = record { e = 0 ; s = λ () ; t = λ () } -ε : Func (SingletonSetoid {0ℓ} {0ℓ}) (Graph-setoid 0) -ε = record - { to = const empty-graph - ; cong = const Graph-same-refl - } +ε : Func ⊤ₛ (Graph-setoid 0) +ε = Const ⊤ₛ (Graph-setoid 0) discrete together : Graph n → Graph m → Graph (n + m) together {n} {m} G₁ G₂ = record @@ -313,77 +282,67 @@ together-resp-same {n} {m} ≡G₁ ≡G₂ = record commute : ∀ {n n′ m m′} - → {G₁ G₁′ : Graph n} - → {G₂ G₂′ : Graph m} + → {G₁ : Graph n} + → {G₂ : Graph m} → (f : Fin n → Fin n′) → (g : Fin m → Fin m′) - → Graph-same G₁ G₁′ - → Graph-same G₂ G₂′ → Graph-same (together (map-nodes f G₁) (map-nodes g G₂)) - (map-nodes ([ (_↑ˡ m′) ∘ f , (n′ ↑ʳ_) ∘ g ] ∘ splitAt n) (together G₁′ G₂′)) -commute {n} {n′} {m} {m′} f g ≡G₁ ≡G₂ = record - { ↔e = +-resp-↔ ≡G₁.↔e ≡G₂.↔e + (map-nodes ([ (_↑ˡ m′) ∘ f , (n′ ↑ʳ_) ∘ g ] ∘ splitAt n) (together G₁ G₂)) +commute {n} {n′} {m} {m′} {G₁} {G₂} f g = record + { ↔e = ↔e ; ≗s = source-commute ; ≗t = target-commute } where - ≡fG₁ : Graph-same (map-nodes f _) (map-nodes f _) - ≡fG₁ = F-resp-≈ (erefl ∘ f) ≡G₁ - ≡gG₂ : Graph-same (map-nodes g _) (map-nodes g _) - ≡gG₂ = F-resp-≈ (erefl ∘ g) ≡G₂ - module ≡G₁ = Graph-same ≡G₁ - module ≡G₂ = Graph-same ≡G₂ - module ≡fG₁ = Graph-same ≡fG₁ - module ≡fG₂ = Graph-same ≡gG₂ - module ≡G₁+G₂ = Graph-same (together-resp-same ≡G₁ ≡G₂) - module ≡fG₁+gG₂ = Graph-same (together-resp-same ≡fG₁ ≡gG₂) + open Graph-same (Graph-same-refl {_} {together G₁ G₂}) + module G₁ = Graph G₁ + module G₂ = Graph G₂ + module fG₁ = Graph (map-nodes f G₁) + module gG₂ = Graph (map-nodes g G₂) + module G₁+G₂ = Graph (together G₁ G₂) + module fG₁+gG₂ = Graph (together (map-nodes f G₁) (map-nodes g G₂)) open ≡-Reasoning source-commute - : ≡fG₁+gG₂.s + : fG₁+gG₂.s ≗ [ (_↑ˡ m′) ∘ f , (n′ ↑ʳ_) ∘ g ] ∘ splitAt n - ∘ ≡G₁+G₂.s′ - ∘ ≡fG₁+gG₂.to + ∘ G₁+G₂.s + ∘ to source-commute x = begin - ≡fG₁+gG₂.s x - ≡⟨ ≡fG₁+gG₂.≗s x ⟩ - (≡fG₁+gG₂.s′ ∘ ≡fG₁+gG₂.to) x + fG₁+gG₂.s x ≡⟨⟩ - (join n′ m′ ∘ map ≡fG₁.s′ ≡fG₂.s′ ∘ splitAt ≡G₁.e′ ∘ ≡fG₁+gG₂.to) x - ≡⟨ cong (join n′ m′) (map-map ((splitAt ≡G₁.e′ ∘ ≡fG₁+gG₂.to) x)) ⟨ - (join n′ m′ ∘ map f g ∘ map ≡G₁.s′ ≡G₂.s′ ∘ splitAt ≡G₁.e′ ∘ ≡fG₁+gG₂.to) x - ≡⟨ [,]-map ((map ≡G₁.s′ ≡G₂.s′ ∘ splitAt ≡G₁.e′ ∘ ≡fG₁+gG₂.to) x) ⟩ - ([ (_↑ˡ m′) ∘ f , (n′ ↑ʳ_) ∘ g ] ∘ map ≡G₁.s′ ≡G₂.s′ ∘ splitAt ≡G₁.e′ ∘ ≡fG₁+gG₂.to) x - ≡⟨ cong [ (_↑ˡ m′) ∘ f , (n′ ↑ʳ_) ∘ g ] (splitAt-join n m (map ≡G₁.s′ ≡G₂.s′ (splitAt ≡G₁.e′ (≡fG₁+gG₂.to x)))) ⟨ - ([ (_↑ˡ m′) ∘ f , (n′ ↑ʳ_) ∘ g ] ∘ splitAt n ∘ join n m ∘ map ≡G₁.s′ ≡G₂.s′ ∘ splitAt ≡G₁.e′ ∘ ≡fG₁+gG₂.to) x + (join n′ m′ ∘ map fG₁.s gG₂.s ∘ splitAt G₁.e ∘ to) x + ≡⟨ cong (join n′ m′) (map-map ((splitAt G₁.e ∘ to) x)) ⟨ + (join n′ m′ ∘ map f g ∘ map G₁.s G₂.s ∘ splitAt fG₁.e ∘ to) x + ≡⟨ [,]-map ((map G₁.s G₂.s ∘ splitAt fG₁.e ∘ to) x) ⟩ + ([ (_↑ˡ m′) ∘ f , (n′ ↑ʳ_) ∘ g ] ∘ map G₁.s G₂.s ∘ splitAt fG₁.e ∘ to) x + ≡⟨ cong [ (_↑ˡ m′) ∘ f , (n′ ↑ʳ_) ∘ g ] (splitAt-join n m (map G₁.s G₂.s (splitAt fG₁.e (to x)))) ⟨ + ([ (_↑ˡ m′) ∘ f , (n′ ↑ʳ_) ∘ g ] ∘ splitAt n ∘ join n m ∘ map G₁.s G₂.s ∘ splitAt fG₁.e ∘ to) x ≡⟨⟩ - ([ (_↑ˡ m′) ∘ f , (n′ ↑ʳ_) ∘ g ] ∘ splitAt n ∘ ≡G₁+G₂.s′ ∘ ≡fG₁+gG₂.to) x ∎ + ([ (_↑ˡ m′) ∘ f , (n′ ↑ʳ_) ∘ g ] ∘ splitAt n ∘ G₁+G₂.s ∘ to) x ∎ target-commute - : ≡fG₁+gG₂.t + : fG₁+gG₂.t ≗ [ (_↑ˡ m′) ∘ f , (n′ ↑ʳ_) ∘ g ] ∘ splitAt n - ∘ ≡G₁+G₂.t′ - ∘ ≡fG₁+gG₂.to + ∘ G₁+G₂.t + ∘ to target-commute x = begin - ≡fG₁+gG₂.t x - ≡⟨ ≡fG₁+gG₂.≗t x ⟩ - (≡fG₁+gG₂.t′ ∘ ≡fG₁+gG₂.to) x + fG₁+gG₂.t x ≡⟨⟩ - (join n′ m′ ∘ map ≡fG₁.t′ ≡fG₂.t′ ∘ splitAt ≡G₁.e′ ∘ ≡fG₁+gG₂.to) x - ≡⟨ cong (join n′ m′) (map-map ((splitAt ≡G₁.e′ ∘ ≡fG₁+gG₂.to) x)) ⟨ - (join n′ m′ ∘ map f g ∘ map ≡G₁.t′ ≡G₂.t′ ∘ splitAt ≡G₁.e′ ∘ ≡fG₁+gG₂.to) x - ≡⟨ [,]-map ((map ≡G₁.t′ ≡G₂.t′ ∘ splitAt ≡G₁.e′ ∘ ≡fG₁+gG₂.to) x) ⟩ - ([ (_↑ˡ m′) ∘ f , (n′ ↑ʳ_) ∘ g ] ∘ map ≡G₁.t′ ≡G₂.t′ ∘ splitAt ≡G₁.e′ ∘ ≡fG₁+gG₂.to) x - ≡⟨ cong [ (_↑ˡ m′) ∘ f , (n′ ↑ʳ_) ∘ g ] (splitAt-join n m (map ≡G₁.t′ ≡G₂.t′ (splitAt ≡G₁.e′ (≡fG₁+gG₂.to x)))) ⟨ - ([ (_↑ˡ m′) ∘ f , (n′ ↑ʳ_) ∘ g ] ∘ splitAt n ∘ join n m ∘ map ≡G₁.t′ ≡G₂.t′ ∘ splitAt ≡G₁.e′ ∘ ≡fG₁+gG₂.to) x + (join n′ m′ ∘ map fG₁.t gG₂.t ∘ splitAt G₁.e ∘ to) x + ≡⟨ cong (join n′ m′) (map-map ((splitAt G₁.e ∘ to) x)) ⟨ + (join n′ m′ ∘ map f g ∘ map G₁.t G₂.t ∘ splitAt fG₁.e ∘ to) x + ≡⟨ [,]-map ((map G₁.t G₂.t ∘ splitAt fG₁.e ∘ to) x) ⟩ + ([ (_↑ˡ m′) ∘ f , (n′ ↑ʳ_) ∘ g ] ∘ map G₁.t G₂.t ∘ splitAt fG₁.e ∘ to) x + ≡⟨ cong [ (_↑ˡ m′) ∘ f , (n′ ↑ʳ_) ∘ g ] (splitAt-join n m (map G₁.t G₂.t (splitAt fG₁.e (to x)))) ⟨ + ([ (_↑ˡ m′) ∘ f , (n′ ↑ʳ_) ∘ g ] ∘ splitAt n ∘ join n m ∘ map G₁.t G₂.t ∘ splitAt fG₁.e ∘ to) x ≡⟨⟩ - ([ (_↑ˡ m′) ∘ f , (n′ ↑ʳ_) ∘ g ] ∘ splitAt n ∘ ≡G₁+G₂.t′ ∘ ≡fG₁+gG₂.to) x ∎ + ([ (_↑ˡ m′) ∘ f , (n′ ↑ʳ_) ∘ g ] ∘ splitAt n ∘ G₁+G₂.t ∘ to) x ∎ ⊗-homomorphism : NaturalTransformation (-×- ∘′ (F ⁂ F)) (F ∘′ -+-) -⊗-homomorphism = record +⊗-homomorphism = ntHelper record { η = λ { (n , m) → η {n} {m} } - ; commute = λ { (f , g) (≡G₁ , ≡G₂) → commute f g ≡G₁ ≡G₂ } - ; sym-commute = λ { (f , g) (≡G₁ , ≡G₂) → Graph-same-sym (commute f g (Graph-same-sym ≡G₁) (Graph-same-sym ≡G₂)) } + ; commute = λ { (f , g) {G₁ , G₂} → commute {G₁ = G₁} {G₂ = G₂} f g } } where η : Func (×-setoid (Graph-setoid n) (Graph-setoid m)) (Graph-setoid (n + m)) @@ -406,155 +365,150 @@ commute {n} {n′} {m} {m′} f g ≡G₁ ≡G₂ = record associativity : {X Y Z : ℕ} - → {G₁ G₁′ : Graph X} - → {G₂ G₂′ : Graph Y} - → {G₃ G₃′ : Graph Z} - → Graph-same G₁ G₁′ - → Graph-same G₂ G₂′ - → Graph-same G₃ G₃′ + → (G₁ : Graph X) + → (G₂ : Graph Y) + → (G₃ : Graph Z) → Graph-same (map-nodes (Inverse.to (+-assoc-↔ X Y Z)) (together (together G₁ G₂) G₃)) - (together G₁′ (together G₂′ G₃′)) -associativity {X} {Y} {Z} ≡G₁ ≡G₂ ≡G₃ = record + (together G₁ (together G₂ G₃)) +associativity {X} {Y} {Z} G₁ G₂ G₃ = record { ↔e = ↔e ; ≗s = ≗s ; ≗t = ≗t } where - module ≡G₁ = Graph-same ≡G₁ - module ≡G₂ = Graph-same ≡G₂ - module ≡G₃ = Graph-same ≡G₃ - module ≡G₂+G₃ = Graph-same (together-resp-same ≡G₂ ≡G₃) - module ≡G₁+[G₂+G₃] = Graph-same (together-resp-same ≡G₁ (together-resp-same ≡G₂ ≡G₃)) - module ≡G₁+G₂+G₃ = Graph-same (together-resp-same (together-resp-same ≡G₁ ≡G₂) ≡G₃) - ↔e : Fin (≡G₁.e + ≡G₂.e + ≡G₃.e) ↔ Fin (≡G₁.e′ + (≡G₂.e′ + ≡G₃.e′)) - ↔e = +-resp-↔ ≡G₁.↔e (+-resp-↔ ≡G₂.↔e ≡G₃.↔e) ↔-∘ (+-assoc-↔ ≡G₁.e ≡G₂.e ≡G₃.e) + module G₁ = Graph G₁ + module G₂ = Graph G₂ + module G₃ = Graph G₃ + module G₂+G₃ = Graph (together G₂ G₃) + module G₁+[G₂+G₃] = Graph (together G₁ (together G₂ G₃)) + module G₁+G₂+G₃ = Graph (together (together G₁ G₂) G₃) + ↔e : Fin (G₁.e + G₂.e + G₃.e) ↔ Fin (G₁.e + (G₂.e + G₃.e)) + ↔e = +-assoc-↔ G₁.e G₂.e G₃.e open ≡-Reasoning open Inverse - ≗s : to (+-assoc-↔ X Y Z) ∘ ≡G₁+G₂+G₃.s ≗ ≡G₁+[G₂+G₃].s′ ∘ ≡G₁+[G₂+G₃].to ∘ to (+-assoc-↔ ≡G₁.e ≡G₂.e ≡G₃.e) + ≗s : to (+-assoc-↔ X Y Z) ∘ G₁+G₂+G₃.s ≗ G₁+[G₂+G₃].s ∘ to ↔e ≗s x = begin - (to (+-assoc-↔ X Y Z) ∘ ≡G₁+G₂+G₃.s) x ≡⟨⟩ - ([ [ join X (Y + Z) ∘ inj₁ , join X (Y + Z) ∘ inj₂ ∘ _ ] ∘ splitAt X , _ ] ∘ splitAt (X + Y) ∘ ≡G₁+G₂+G₃.s) x - ≡⟨ [-,]-cong ([,]-∘ (join X (Y + Z)) ∘ splitAt X) (splitAt (X + Y) (≡G₁+G₂+G₃.s x)) ⟨ - ([ join X (Y + Z) ∘ map id _ ∘ splitAt X , join X (Y + Z) ∘ inj₂ ∘ _ ] ∘ splitAt (X + Y) ∘ ≡G₁+G₂+G₃.s) x - ≡⟨ [,]-∘ (join X (Y + Z)) (splitAt (X + Y) (≡G₁+G₂+G₃.s x)) ⟨ - (join X (Y + Z) ∘ [ map id _ ∘ splitAt X , inj₂ ∘ join Y Z ∘ inj₂ ] ∘ splitAt (X + Y) ∘ ≡G₁+G₂+G₃.s) x ≡⟨⟩ - (join X (Y + Z) ∘ [ map id _ ∘ splitAt X , inj₂ ∘ join Y Z ∘ inj₂ ] ∘ splitAt (X + Y) ∘ join (X + Y) Z ∘ map _ ≡G₃.s ∘ splitAt _) x + (to (+-assoc-↔ X Y Z) ∘ G₁+G₂+G₃.s) x ≡⟨⟩ + ([ [ join X (Y + Z) ∘ inj₁ , join X (Y + Z) ∘ inj₂ ∘ _ ] ∘ splitAt X , _ ] ∘ splitAt (X + Y) ∘ G₁+G₂+G₃.s) x + ≡⟨ [-,]-cong ([,]-∘ (join X (Y + Z)) ∘ splitAt X) (splitAt (X + Y) (G₁+G₂+G₃.s x)) ⟨ + ([ join X (Y + Z) ∘ map id _ ∘ splitAt X , join X (Y + Z) ∘ inj₂ ∘ _ ] ∘ splitAt (X + Y) ∘ G₁+G₂+G₃.s) x + ≡⟨ [,]-∘ (join X (Y + Z)) (splitAt (X + Y) (G₁+G₂+G₃.s x)) ⟨ + (join X (Y + Z) ∘ [ map id _ ∘ splitAt X , inj₂ ∘ join Y Z ∘ inj₂ ] ∘ splitAt (X + Y) ∘ G₁+G₂+G₃.s) x ≡⟨⟩ + (join X (Y + Z) ∘ [ map id _ ∘ splitAt X , inj₂ ∘ join Y Z ∘ inj₂ ] ∘ splitAt (X + Y) ∘ join (X + Y) Z ∘ map _ G₃.s ∘ splitAt _) x ≡⟨ cong (join X (Y + Z) ∘ [ map id _ ∘ splitAt X , inj₂ ∘ join Y Z ∘ inj₂ ]) - (splitAt-join (X + Y) Z (map _ ≡G₃.s (splitAt _ x))) ⟩ - (join X (Y + Z) ∘ [ map id _ ∘ splitAt X , inj₂ ∘ join Y Z ∘ inj₂ ] ∘ map _ ≡G₃.s ∘ splitAt _) x - ≡⟨ cong (join X (Y + Z)) ([,]-map (splitAt (≡G₁.e + ≡G₂.e) x)) ⟩ - (join X (Y + Z) ∘ [ map id _ ∘ splitAt X ∘ join X Y ∘ map ≡G₁.s ≡G₂.s ∘ splitAt _ , inj₂ ∘ join Y Z ∘ inj₂ ∘ ≡G₃.s ] ∘ splitAt _) x + (splitAt-join (X + Y) Z (map _ G₃.s (splitAt _ x))) ⟩ + (join X (Y + Z) ∘ [ map id _ ∘ splitAt X , inj₂ ∘ join Y Z ∘ inj₂ ] ∘ map _ G₃.s ∘ splitAt _) x + ≡⟨ cong (join X (Y + Z)) ([,]-map (splitAt (G₁.e + G₂.e) x)) ⟩ + (join X (Y + Z) ∘ [ map id _ ∘ splitAt X ∘ join X Y ∘ map G₁.s G₂.s ∘ splitAt _ , inj₂ ∘ join Y Z ∘ inj₂ ∘ G₃.s ] ∘ splitAt _) x ≡⟨ cong (join X (Y + Z)) ([-,]-cong - (cong (map id (_↑ˡ Z)) ∘ splitAt-join X Y ∘ map ≡G₁.s ≡G₂.s ∘ splitAt ≡G₁.e) - (splitAt (≡G₁.e + ≡G₂.e) x)) ⟩ - (join X (Y + Z) ∘ [ map id _ ∘ map ≡G₁.s ≡G₂.s ∘ splitAt _ , inj₂ ∘ join Y Z ∘ inj₂ ∘ ≡G₃.s ] ∘ splitAt _) x - ≡⟨ cong (join X (Y + Z)) ([-,]-cong (map-map ∘ splitAt ≡G₁.e) (splitAt _ x)) ⟩ - (join X (Y + Z) ∘ [ map ≡G₁.s (join Y Z ∘ inj₁ ∘ ≡G₂.s) ∘ splitAt _ , inj₂ ∘ _ ] ∘ splitAt _) x ≡⟨⟩ - (join X (Y + Z) ∘ [ map ≡G₁.s (join Y Z ∘ map ≡G₂.s ≡G₃.s ∘ inj₁) ∘ splitAt _ , _ ] ∘ splitAt _) x + (cong (map id (_↑ˡ Z)) ∘ splitAt-join X Y ∘ map G₁.s G₂.s ∘ splitAt G₁.e) + (splitAt (G₁.e + G₂.e) x)) ⟩ + (join X (Y + Z) ∘ [ map id _ ∘ map G₁.s G₂.s ∘ splitAt _ , inj₂ ∘ join Y Z ∘ inj₂ ∘ G₃.s ] ∘ splitAt _) x + ≡⟨ cong (join X (Y + Z)) ([-,]-cong (map-map ∘ splitAt G₁.e) (splitAt _ x)) ⟩ + (join X (Y + Z) ∘ [ map G₁.s (join Y Z ∘ inj₁ ∘ G₂.s) ∘ splitAt _ , inj₂ ∘ _ ] ∘ splitAt _) x ≡⟨⟩ + (join X (Y + Z) ∘ [ map G₁.s (join Y Z ∘ map G₂.s G₃.s ∘ inj₁) ∘ splitAt _ , _ ] ∘ splitAt _) x ≡⟨ cong (join X (Y + Z)) ([-,]-cong - (map-cong (cong ≡G₁.s ∘ erefl) (cong (join Y Z ∘ map ≡G₂.s ≡G₃.s) ∘ splitAt-join ≡G₂.e ≡G₃.e ∘ inj₁) ∘ splitAt _) - (splitAt (≡G₁.e + ≡G₂.e) x)) ⟨ - (join X (Y + Z) ∘ [ map ≡G₁.s (join Y Z ∘ map ≡G₂.s ≡G₃.s ∘ splitAt ≡G₂.e ∘ _) ∘ splitAt _ , _ ] ∘ splitAt _) x ≡⟨⟩ - (join X (Y + Z) ∘ [ map ≡G₁.s (≡G₂+G₃.s ∘ _) ∘ splitAt _ , inj₂ ∘ join Y Z ∘ inj₂ ∘ ≡G₃.s ] ∘ splitAt _) x ≡⟨⟩ - (join X (Y + Z) ∘ [ map ≡G₁.s (≡G₂+G₃.s ∘ _) ∘ splitAt _ , inj₂ ∘ join Y Z ∘ map ≡G₂.s ≡G₃.s ∘ inj₂ ] ∘ splitAt _) x + (map-cong (cong G₁.s ∘ erefl) (cong (join Y Z ∘ map G₂.s G₃.s) ∘ splitAt-join G₂.e G₃.e ∘ inj₁) ∘ splitAt _) + (splitAt (G₁.e + G₂.e) x)) ⟨ + (join X (Y + Z) ∘ [ map G₁.s (join Y Z ∘ map G₂.s G₃.s ∘ splitAt G₂.e ∘ _) ∘ splitAt _ , _ ] ∘ splitAt _) x ≡⟨⟩ + (join X (Y + Z) ∘ [ map G₁.s (G₂+G₃.s ∘ _) ∘ splitAt _ , inj₂ ∘ join Y Z ∘ inj₂ ∘ G₃.s ] ∘ splitAt _) x ≡⟨⟩ + (join X (Y + Z) ∘ [ map G₁.s (G₂+G₃.s ∘ _) ∘ splitAt _ , inj₂ ∘ join Y Z ∘ map G₂.s G₃.s ∘ inj₂ ] ∘ splitAt _) x ≡⟨ cong (join X (Y + Z)) ([,-]-cong - (cong (inj₂ ∘ join Y Z ∘ map ≡G₂.s ≡G₃.s) ∘ splitAt-join ≡G₂.e ≡G₃.e ∘ inj₂) - (splitAt (≡G₁.e + ≡G₂.e) x)) ⟨ - (join X (Y + Z) ∘ [ map ≡G₁.s _ ∘ splitAt _ , inj₂ ∘ join Y Z ∘ map ≡G₂.s ≡G₃.s ∘ splitAt ≡G₂.e ∘ (≡G₂.e ↑ʳ_) ] ∘ splitAt _) x ≡⟨⟩ - (join X (Y + Z) ∘ [ map ≡G₁.s _ ∘ splitAt _ , inj₂ ∘ ≡G₂+G₃.s ∘ (≡G₂.e ↑ʳ_) ] ∘ splitAt _) x ≡⟨⟩ - (join X (Y + Z) ∘ [ map ≡G₁.s _ ∘ splitAt _ , map ≡G₁.s ≡G₂+G₃.s ∘ inj₂ ∘ (≡G₂.e ↑ʳ_) ] ∘ splitAt _) x + (cong (inj₂ ∘ join Y Z ∘ map G₂.s G₃.s) ∘ splitAt-join G₂.e G₃.e ∘ inj₂) + (splitAt (G₁.e + G₂.e) x)) ⟨ + (join X (Y + Z) ∘ [ map G₁.s _ ∘ splitAt _ , inj₂ ∘ join Y Z ∘ map G₂.s G₃.s ∘ splitAt G₂.e ∘ (G₂.e ↑ʳ_) ] ∘ splitAt _) x ≡⟨⟩ + (join X (Y + Z) ∘ [ map G₁.s _ ∘ splitAt _ , inj₂ ∘ G₂+G₃.s ∘ (G₂.e ↑ʳ_) ] ∘ splitAt _) x ≡⟨⟩ + (join X (Y + Z) ∘ [ map G₁.s _ ∘ splitAt _ , map G₁.s G₂+G₃.s ∘ inj₂ ∘ (G₂.e ↑ʳ_) ] ∘ splitAt _) x ≡⟨ cong (join X (Y + Z)) ([-,]-cong - (map-map ∘ splitAt ≡G₁.e) - (splitAt (≡G₁.e + ≡G₂.e) x)) ⟨ - (join X (Y + Z) ∘ [ map ≡G₁.s ≡G₂+G₃.s ∘ map id (_↑ˡ ≡G₃.e) ∘ splitAt _ , map ≡G₁.s ≡G₂+G₃.s ∘ inj₂ ∘ (≡G₂.e ↑ʳ_) ] ∘ splitAt _) x - ≡⟨ cong (join X (Y + Z)) ([,]-∘ (map ≡G₁.s ≡G₂+G₃.s) (splitAt (≡G₁.e + ≡G₂.e) x)) ⟨ - (join X (Y + Z) ∘ map ≡G₁.s ≡G₂+G₃.s ∘ [ map id (_↑ˡ ≡G₃.e) ∘ splitAt _ , inj₂ ∘ (≡G₂.e ↑ʳ_) ] ∘ splitAt _) x + (map-map ∘ splitAt G₁.e) + (splitAt (G₁.e + G₂.e) x)) ⟨ + (join X (Y + Z) ∘ [ map G₁.s G₂+G₃.s ∘ map id (_↑ˡ G₃.e) ∘ splitAt _ , map G₁.s G₂+G₃.s ∘ inj₂ ∘ (G₂.e ↑ʳ_) ] ∘ splitAt _) x + ≡⟨ cong (join X (Y + Z)) ([,]-∘ (map G₁.s G₂+G₃.s) (splitAt (G₁.e + G₂.e) x)) ⟨ + (join X (Y + Z) ∘ map G₁.s G₂+G₃.s ∘ [ map id (_↑ˡ G₃.e) ∘ splitAt _ , inj₂ ∘ (G₂.e ↑ʳ_) ] ∘ splitAt _) x ≡⟨ cong - (join X (Y + Z) ∘ map ≡G₁.s ≡G₂+G₃.s) - (splitAt-join ≡G₁.e ≡G₂+G₃.e (([ map id _ ∘ splitAt _ , inj₂ ∘ (≡G₂.e ↑ʳ_) ] ∘ splitAt _) x)) ⟨ - (join X (Y + Z) ∘ map ≡G₁.s ≡G₂+G₃.s ∘ splitAt ≡G₁.e ∘ join ≡G₁.e ≡G₂+G₃.e ∘ [ map id _ ∘ splitAt _ , inj₂ ∘ (≡G₂.e ↑ʳ_) ] ∘ splitAt _) x ≡⟨⟩ - (≡G₁+[G₂+G₃].s ∘ join ≡G₁.e ≡G₂+G₃.e ∘ [ map id _ ∘ splitAt _ , inj₂ ∘ (≡G₂.e ↑ʳ_) ] ∘ splitAt _) x - ≡⟨ cong ≡G₁+[G₂+G₃].s ([,]-∘ (join ≡G₁.e ≡G₂+G₃.e) (splitAt (≡G₁.e + ≡G₂.e) x)) ⟩ - (≡G₁+[G₂+G₃].s ∘ [ join ≡G₁.e ≡G₂+G₃.e ∘ map id (_↑ˡ ≡G₃.e) ∘ splitAt _ , join ≡G₁.e ≡G₂+G₃.e ∘ inj₂ ∘ (≡G₂.e ↑ʳ_) ] ∘ splitAt _) x - ≡⟨ cong ≡G₁+[G₂+G₃].s ([-,]-cong ([,]-map ∘ splitAt ≡G₁.e) (splitAt (≡G₁.e + ≡G₂.e) x)) ⟩ - (≡G₁+[G₂+G₃].s ∘ [ [ _↑ˡ ≡G₂.e + ≡G₃.e , (≡G₁.e ↑ʳ_) ∘ (_↑ˡ ≡G₃.e) ] ∘ splitAt ≡G₁.e , (≡G₁.e ↑ʳ_) ∘ (≡G₂.e ↑ʳ_) ] ∘ splitAt _) x ≡⟨⟩ - (≡G₁+[G₂+G₃].s ∘ to (+-assoc-↔ ≡G₁.e ≡G₂.e ≡G₃.e)) x ≡⟨ ≡G₁+[G₂+G₃].≗s (to (+-assoc-↔ ≡G₁.e ≡G₂.e ≡G₃.e) x) ⟩ - (≡G₁+[G₂+G₃].s′ ∘ ≡G₁+[G₂+G₃].to ∘ to (+-assoc-↔ ≡G₁.e ≡G₂.e ≡G₃.e)) x ∎ - ≗t : to (+-assoc-↔ X Y Z) ∘ ≡G₁+G₂+G₃.t ≗ ≡G₁+[G₂+G₃].t′ ∘ ≡G₁+[G₂+G₃].to ∘ to (+-assoc-↔ ≡G₁.e ≡G₂.e ≡G₃.e) + (join X (Y + Z) ∘ map G₁.s G₂+G₃.s) + (splitAt-join G₁.e G₂+G₃.e (([ map id _ ∘ splitAt _ , inj₂ ∘ (G₂.e ↑ʳ_) ] ∘ splitAt _) x)) ⟨ + (join X (Y + Z) ∘ map G₁.s G₂+G₃.s ∘ splitAt G₁.e ∘ join G₁.e G₂+G₃.e ∘ [ map id _ ∘ splitAt _ , inj₂ ∘ (G₂.e ↑ʳ_) ] ∘ splitAt _) x ≡⟨⟩ + (G₁+[G₂+G₃].s ∘ join G₁.e G₂+G₃.e ∘ [ map id _ ∘ splitAt _ , inj₂ ∘ (G₂.e ↑ʳ_) ] ∘ splitAt _) x + ≡⟨ cong G₁+[G₂+G₃].s ([,]-∘ (join G₁.e G₂+G₃.e) (splitAt (G₁.e + G₂.e) x)) ⟩ + (G₁+[G₂+G₃].s ∘ [ join G₁.e G₂+G₃.e ∘ map id (_↑ˡ G₃.e) ∘ splitAt _ , join G₁.e G₂+G₃.e ∘ inj₂ ∘ (G₂.e ↑ʳ_) ] ∘ splitAt _) x + ≡⟨ cong G₁+[G₂+G₃].s ([-,]-cong ([,]-map ∘ splitAt G₁.e) (splitAt (G₁.e + G₂.e) x)) ⟩ + (G₁+[G₂+G₃].s ∘ [ [ _↑ˡ G₂.e + G₃.e , (G₁.e ↑ʳ_) ∘ (_↑ˡ G₃.e) ] ∘ splitAt G₁.e , (G₁.e ↑ʳ_) ∘ (G₂.e ↑ʳ_) ] ∘ splitAt _) x ≡⟨⟩ + (G₁+[G₂+G₃].s ∘ to (+-assoc-↔ G₁.e G₂.e G₃.e)) x ∎ + ≗t : to (+-assoc-↔ X Y Z) ∘ G₁+G₂+G₃.t ≗ G₁+[G₂+G₃].t ∘ to ↔e ≗t x = begin - (to (+-assoc-↔ X Y Z) ∘ ≡G₁+G₂+G₃.t) x ≡⟨⟩ - ([ [ join X (Y + Z) ∘ inj₁ , join X (Y + Z) ∘ inj₂ ∘ _ ] ∘ splitAt X , _ ] ∘ splitAt (X + Y) ∘ ≡G₁+G₂+G₃.t) x - ≡⟨ [-,]-cong ([,]-∘ (join X (Y + Z)) ∘ splitAt X) (splitAt (X + Y) (≡G₁+G₂+G₃.t x)) ⟨ - ([ join X (Y + Z) ∘ map id _ ∘ splitAt X , join X (Y + Z) ∘ inj₂ ∘ _ ] ∘ splitAt (X + Y) ∘ ≡G₁+G₂+G₃.t) x - ≡⟨ [,]-∘ (join X (Y + Z)) (splitAt (X + Y) (≡G₁+G₂+G₃.t x)) ⟨ - (join X (Y + Z) ∘ [ map id _ ∘ splitAt X , inj₂ ∘ join Y Z ∘ inj₂ ] ∘ splitAt (X + Y) ∘ ≡G₁+G₂+G₃.t) x ≡⟨⟩ - (join X (Y + Z) ∘ [ map id _ ∘ splitAt X , inj₂ ∘ join Y Z ∘ inj₂ ] ∘ splitAt (X + Y) ∘ join (X + Y) Z ∘ map _ ≡G₃.t ∘ splitAt _) x + (to (+-assoc-↔ X Y Z) ∘ G₁+G₂+G₃.t) x ≡⟨⟩ + ([ [ join X (Y + Z) ∘ inj₁ , join X (Y + Z) ∘ inj₂ ∘ _ ] ∘ splitAt X , _ ] ∘ splitAt (X + Y) ∘ G₁+G₂+G₃.t) x + ≡⟨ [-,]-cong ([,]-∘ (join X (Y + Z)) ∘ splitAt X) (splitAt (X + Y) (G₁+G₂+G₃.t x)) ⟨ + ([ join X (Y + Z) ∘ map id _ ∘ splitAt X , join X (Y + Z) ∘ inj₂ ∘ _ ] ∘ splitAt (X + Y) ∘ G₁+G₂+G₃.t) x + ≡⟨ [,]-∘ (join X (Y + Z)) (splitAt (X + Y) (G₁+G₂+G₃.t x)) ⟨ + (join X (Y + Z) ∘ [ map id _ ∘ splitAt X , inj₂ ∘ join Y Z ∘ inj₂ ] ∘ splitAt (X + Y) ∘ G₁+G₂+G₃.t) x ≡⟨⟩ + (join X (Y + Z) ∘ [ map id _ ∘ splitAt X , inj₂ ∘ join Y Z ∘ inj₂ ] ∘ splitAt (X + Y) ∘ join (X + Y) Z ∘ map _ G₃.t ∘ splitAt _) x ≡⟨ cong (join X (Y + Z) ∘ [ map id _ ∘ splitAt X , inj₂ ∘ join Y Z ∘ inj₂ ]) - (splitAt-join (X + Y) Z (map _ ≡G₃.t (splitAt _ x))) ⟩ - (join X (Y + Z) ∘ [ map id _ ∘ splitAt X , inj₂ ∘ join Y Z ∘ inj₂ ] ∘ map _ ≡G₃.t ∘ splitAt _) x - ≡⟨ cong (join X (Y + Z)) ([,]-map (splitAt (≡G₁.e + ≡G₂.e) x)) ⟩ - (join X (Y + Z) ∘ [ map id _ ∘ splitAt X ∘ join X Y ∘ map ≡G₁.t ≡G₂.t ∘ splitAt _ , inj₂ ∘ join Y Z ∘ inj₂ ∘ ≡G₃.t ] ∘ splitAt _) x + (splitAt-join (X + Y) Z (map _ G₃.t (splitAt _ x))) ⟩ + (join X (Y + Z) ∘ [ map id _ ∘ splitAt X , inj₂ ∘ join Y Z ∘ inj₂ ] ∘ map _ G₃.t ∘ splitAt _) x + ≡⟨ cong (join X (Y + Z)) ([,]-map (splitAt (G₁.e + G₂.e) x)) ⟩ + (join X (Y + Z) ∘ [ map id _ ∘ splitAt X ∘ join X Y ∘ map G₁.t G₂.t ∘ splitAt _ , inj₂ ∘ join Y Z ∘ inj₂ ∘ G₃.t ] ∘ splitAt _) x ≡⟨ cong (join X (Y + Z)) ([-,]-cong - (cong (map id (_↑ˡ Z)) ∘ splitAt-join X Y ∘ map ≡G₁.t ≡G₂.t ∘ splitAt ≡G₁.e) - (splitAt (≡G₁.e + ≡G₂.e) x)) ⟩ - (join X (Y + Z) ∘ [ map id _ ∘ map ≡G₁.t ≡G₂.t ∘ splitAt _ , inj₂ ∘ join Y Z ∘ inj₂ ∘ ≡G₃.t ] ∘ splitAt _) x - ≡⟨ cong (join X (Y + Z)) ([-,]-cong (map-map ∘ splitAt ≡G₁.e) (splitAt _ x)) ⟩ - (join X (Y + Z) ∘ [ map ≡G₁.t (join Y Z ∘ inj₁ ∘ ≡G₂.t) ∘ splitAt _ , inj₂ ∘ _ ] ∘ splitAt _) x ≡⟨⟩ - (join X (Y + Z) ∘ [ map ≡G₁.t (join Y Z ∘ map ≡G₂.t ≡G₃.t ∘ inj₁) ∘ splitAt _ , _ ] ∘ splitAt _) x + (cong (map id (_↑ˡ Z)) ∘ splitAt-join X Y ∘ map G₁.t G₂.t ∘ splitAt G₁.e) + (splitAt (G₁.e + G₂.e) x)) ⟩ + (join X (Y + Z) ∘ [ map id _ ∘ map G₁.t G₂.t ∘ splitAt _ , inj₂ ∘ join Y Z ∘ inj₂ ∘ G₃.t ] ∘ splitAt _) x + ≡⟨ cong (join X (Y + Z)) ([-,]-cong (map-map ∘ splitAt G₁.e) (splitAt _ x)) ⟩ + (join X (Y + Z) ∘ [ map G₁.t (join Y Z ∘ inj₁ ∘ G₂.t) ∘ splitAt _ , inj₂ ∘ _ ] ∘ splitAt _) x ≡⟨⟩ + (join X (Y + Z) ∘ [ map G₁.t (join Y Z ∘ map G₂.t G₃.t ∘ inj₁) ∘ splitAt _ , _ ] ∘ splitAt _) x ≡⟨ cong (join X (Y + Z)) ([-,]-cong - (map-cong (cong ≡G₁.t ∘ erefl) (cong (join Y Z ∘ map ≡G₂.t ≡G₃.t) ∘ splitAt-join ≡G₂.e ≡G₃.e ∘ inj₁) ∘ splitAt _) - (splitAt (≡G₁.e + ≡G₂.e) x)) ⟨ - (join X (Y + Z) ∘ [ map ≡G₁.t (join Y Z ∘ map ≡G₂.t ≡G₃.t ∘ splitAt ≡G₂.e ∘ _) ∘ splitAt _ , _ ] ∘ splitAt _) x ≡⟨⟩ - (join X (Y + Z) ∘ [ map ≡G₁.t (≡G₂+G₃.t ∘ _) ∘ splitAt _ , inj₂ ∘ join Y Z ∘ inj₂ ∘ ≡G₃.t ] ∘ splitAt _) x ≡⟨⟩ - (join X (Y + Z) ∘ [ map ≡G₁.t (≡G₂+G₃.t ∘ _) ∘ splitAt _ , inj₂ ∘ join Y Z ∘ map ≡G₂.t ≡G₃.t ∘ inj₂ ] ∘ splitAt _) x + (map-cong (cong G₁.t ∘ erefl) (cong (join Y Z ∘ map G₂.t G₃.t) ∘ splitAt-join G₂.e G₃.e ∘ inj₁) ∘ splitAt _) + (splitAt (G₁.e + G₂.e) x)) ⟨ + (join X (Y + Z) ∘ [ map G₁.t (join Y Z ∘ map G₂.t G₃.t ∘ splitAt G₂.e ∘ _) ∘ splitAt _ , _ ] ∘ splitAt _) x ≡⟨⟩ + (join X (Y + Z) ∘ [ map G₁.t (G₂+G₃.t ∘ _) ∘ splitAt _ , inj₂ ∘ join Y Z ∘ inj₂ ∘ G₃.t ] ∘ splitAt _) x ≡⟨⟩ + (join X (Y + Z) ∘ [ map G₁.t (G₂+G₃.t ∘ _) ∘ splitAt _ , inj₂ ∘ join Y Z ∘ map G₂.t G₃.t ∘ inj₂ ] ∘ splitAt _) x ≡⟨ cong (join X (Y + Z)) ([,-]-cong - (cong (inj₂ ∘ join Y Z ∘ map ≡G₂.t ≡G₃.t) ∘ splitAt-join ≡G₂.e ≡G₃.e ∘ inj₂) - (splitAt (≡G₁.e + ≡G₂.e) x)) ⟨ - (join X (Y + Z) ∘ [ map ≡G₁.t _ ∘ splitAt _ , inj₂ ∘ join Y Z ∘ map ≡G₂.t ≡G₃.t ∘ splitAt ≡G₂.e ∘ (≡G₂.e ↑ʳ_) ] ∘ splitAt _) x ≡⟨⟩ - (join X (Y + Z) ∘ [ map ≡G₁.t _ ∘ splitAt _ , inj₂ ∘ ≡G₂+G₃.t ∘ (≡G₂.e ↑ʳ_) ] ∘ splitAt _) x ≡⟨⟩ - (join X (Y + Z) ∘ [ map ≡G₁.t _ ∘ splitAt _ , map ≡G₁.t ≡G₂+G₃.t ∘ inj₂ ∘ (≡G₂.e ↑ʳ_) ] ∘ splitAt _) x + (cong (inj₂ ∘ join Y Z ∘ map G₂.t G₃.t) ∘ splitAt-join G₂.e G₃.e ∘ inj₂) + (splitAt (G₁.e + G₂.e) x)) ⟨ + (join X (Y + Z) ∘ [ map G₁.t _ ∘ splitAt _ , inj₂ ∘ join Y Z ∘ map G₂.t G₃.t ∘ splitAt G₂.e ∘ (G₂.e ↑ʳ_) ] ∘ splitAt _) x ≡⟨⟩ + (join X (Y + Z) ∘ [ map G₁.t _ ∘ splitAt _ , inj₂ ∘ G₂+G₃.t ∘ (G₂.e ↑ʳ_) ] ∘ splitAt _) x ≡⟨⟩ + (join X (Y + Z) ∘ [ map G₁.t _ ∘ splitAt _ , map G₁.t G₂+G₃.t ∘ inj₂ ∘ (G₂.e ↑ʳ_) ] ∘ splitAt _) x ≡⟨ cong (join X (Y + Z)) ([-,]-cong - (map-map ∘ splitAt ≡G₁.e) - (splitAt (≡G₁.e + ≡G₂.e) x)) ⟨ - (join X (Y + Z) ∘ [ map ≡G₁.t ≡G₂+G₃.t ∘ map id (_↑ˡ ≡G₃.e) ∘ splitAt _ , map ≡G₁.t ≡G₂+G₃.t ∘ inj₂ ∘ (≡G₂.e ↑ʳ_) ] ∘ splitAt _) x - ≡⟨ cong (join X (Y + Z)) ([,]-∘ (map ≡G₁.t ≡G₂+G₃.t) (splitAt (≡G₁.e + ≡G₂.e) x)) ⟨ - (join X (Y + Z) ∘ map ≡G₁.t ≡G₂+G₃.t ∘ [ map id (_↑ˡ ≡G₃.e) ∘ splitAt _ , inj₂ ∘ (≡G₂.e ↑ʳ_) ] ∘ splitAt _) x + (map-map ∘ splitAt G₁.e) + (splitAt (G₁.e + G₂.e) x)) ⟨ + (join X (Y + Z) ∘ [ map G₁.t G₂+G₃.t ∘ map id (_↑ˡ G₃.e) ∘ splitAt _ , map G₁.t G₂+G₃.t ∘ inj₂ ∘ (G₂.e ↑ʳ_) ] ∘ splitAt _) x + ≡⟨ cong (join X (Y + Z)) ([,]-∘ (map G₁.t G₂+G₃.t) (splitAt (G₁.e + G₂.e) x)) ⟨ + (join X (Y + Z) ∘ map G₁.t G₂+G₃.t ∘ [ map id (_↑ˡ G₃.e) ∘ splitAt _ , inj₂ ∘ (G₂.e ↑ʳ_) ] ∘ splitAt _) x ≡⟨ cong - (join X (Y + Z) ∘ map ≡G₁.t ≡G₂+G₃.t) - (splitAt-join ≡G₁.e ≡G₂+G₃.e (([ map id _ ∘ splitAt _ , inj₂ ∘ (≡G₂.e ↑ʳ_) ] ∘ splitAt _) x)) ⟨ - (join X (Y + Z) ∘ map ≡G₁.t ≡G₂+G₃.t ∘ splitAt ≡G₁.e ∘ join ≡G₁.e ≡G₂+G₃.e ∘ [ map id _ ∘ splitAt _ , inj₂ ∘ (≡G₂.e ↑ʳ_) ] ∘ splitAt _) x ≡⟨⟩ - (≡G₁+[G₂+G₃].t ∘ join ≡G₁.e ≡G₂+G₃.e ∘ [ map id _ ∘ splitAt _ , inj₂ ∘ (≡G₂.e ↑ʳ_) ] ∘ splitAt _) x - ≡⟨ cong ≡G₁+[G₂+G₃].t ([,]-∘ (join ≡G₁.e ≡G₂+G₃.e) (splitAt (≡G₁.e + ≡G₂.e) x)) ⟩ - (≡G₁+[G₂+G₃].t ∘ [ join ≡G₁.e ≡G₂+G₃.e ∘ map id (_↑ˡ ≡G₃.e) ∘ splitAt _ , join ≡G₁.e ≡G₂+G₃.e ∘ inj₂ ∘ (≡G₂.e ↑ʳ_) ] ∘ splitAt _) x - ≡⟨ cong ≡G₁+[G₂+G₃].t ([-,]-cong ([,]-map ∘ splitAt ≡G₁.e) (splitAt (≡G₁.e + ≡G₂.e) x)) ⟩ - (≡G₁+[G₂+G₃].t ∘ [ [ _↑ˡ ≡G₂.e + ≡G₃.e , (≡G₁.e ↑ʳ_) ∘ (_↑ˡ ≡G₃.e) ] ∘ splitAt ≡G₁.e , (≡G₁.e ↑ʳ_) ∘ (≡G₂.e ↑ʳ_) ] ∘ splitAt _) x ≡⟨⟩ - (≡G₁+[G₂+G₃].t ∘ to (+-assoc-↔ ≡G₁.e ≡G₂.e ≡G₃.e)) x ≡⟨ ≡G₁+[G₂+G₃].≗t (to (+-assoc-↔ ≡G₁.e ≡G₂.e ≡G₃.e) x) ⟩ - (≡G₁+[G₂+G₃].t′ ∘ ≡G₁+[G₂+G₃].to ∘ to (+-assoc-↔ ≡G₁.e ≡G₂.e ≡G₃.e)) x ∎ - -unitaryˡ : Graph-same G G′ → Graph-same (together empty-graph G) G′ -unitaryˡ ≡G = ≡G - -n+0↔0 : ∀ n → Fin (n + 0) ↔ Fin n -n+0↔0 n = record + (join X (Y + Z) ∘ map G₁.t G₂+G₃.t) + (splitAt-join G₁.e G₂+G₃.e (([ map id _ ∘ splitAt _ , inj₂ ∘ (G₂.e ↑ʳ_) ] ∘ splitAt _) x)) ⟨ + (join X (Y + Z) ∘ map G₁.t G₂+G₃.t ∘ splitAt G₁.e ∘ join G₁.e G₂+G₃.e ∘ [ map id _ ∘ splitAt _ , inj₂ ∘ (G₂.e ↑ʳ_) ] ∘ splitAt _) x ≡⟨⟩ + (G₁+[G₂+G₃].t ∘ join G₁.e G₂+G₃.e ∘ [ map id _ ∘ splitAt _ , inj₂ ∘ (G₂.e ↑ʳ_) ] ∘ splitAt _) x + ≡⟨ cong G₁+[G₂+G₃].t ([,]-∘ (join G₁.e G₂+G₃.e) (splitAt (G₁.e + G₂.e) x)) ⟩ + (G₁+[G₂+G₃].t ∘ [ join G₁.e G₂+G₃.e ∘ map id (_↑ˡ G₃.e) ∘ splitAt _ , join G₁.e G₂+G₃.e ∘ inj₂ ∘ (G₂.e ↑ʳ_) ] ∘ splitAt _) x + ≡⟨ cong G₁+[G₂+G₃].t ([-,]-cong ([,]-map ∘ splitAt G₁.e) (splitAt (G₁.e + G₂.e) x)) ⟩ + (G₁+[G₂+G₃].t ∘ [ [ _↑ˡ G₂.e + G₃.e , (G₁.e ↑ʳ_) ∘ (_↑ˡ G₃.e) ] ∘ splitAt G₁.e , (G₁.e ↑ʳ_) ∘ (G₂.e ↑ʳ_) ] ∘ splitAt _) x ≡⟨⟩ + (G₁+[G₂+G₃].t ∘ to (+-assoc-↔ G₁.e G₂.e G₃.e)) x ∎ + +unitaryˡ : Graph-same (together (discrete {0}) G) G +unitaryˡ = Graph-same-refl + +n+0↔n : ∀ n → Fin (n + 0) ↔ Fin n +n+0↔n n = record { to = to ; from = from ; to-cong = λ { refl → refl } @@ -562,63 +516,33 @@ n+0↔0 n = record ; inverse = (λ { refl → to∘from _ }) , λ { refl → from∘to _ } } where - to : ∀ {n} → Fin (n + 0) → Fin n - to {ℕ.suc ℕ.zero} n = n - to {ℕ.suc (ℕ.suc n)} zero = zero - to {ℕ.suc (ℕ.suc n)} (suc z) = suc (to z) - from : ∀ {n} → Fin n → Fin (n + 0) - from {ℕ.suc ℕ.zero} n = n - from {ℕ.suc (ℕ.suc n)} zero = zero - from {ℕ.suc (ℕ.suc n)} (suc z) = suc (from z) - from∘to : ∀ {n} → ∀ (x : Fin (n + 0)) → from (to x) ≡ x - from∘to {ℕ.suc ℕ.zero} zero = refl - from∘to {ℕ.suc (ℕ.suc n)} zero = refl - from∘to {ℕ.suc (ℕ.suc n)} (suc x) = cong suc (from∘to x) - to∘from : ∀ {n} → ∀ (x : Fin n) → to (from x) ≡ x - to∘from {ℕ.suc ℕ.zero} zero = refl - to∘from {ℕ.suc (ℕ.suc n)} zero = refl - to∘from {ℕ.suc (ℕ.suc n)} (suc x) = cong suc (to∘from x) + to : Fin (n + 0) → Fin n + to x with inj₁ x₁ ← splitAt n x = x₁ + from : Fin n → Fin (n + 0) + from x = x ↑ˡ 0 + from∘to : (x : Fin (n + 0)) → from (to x) ≡ x + from∘to x with inj₁ x₁ ← splitAt n x in eq = splitAt⁻¹-↑ˡ eq + to∘from : (x : Fin n) → to (from x) ≡ x + to∘from x rewrite splitAt-↑ˡ n x 0 = refl unitaryʳ - : {G G′ : Graph n} - → Graph-same G G′ - → Graph-same (map-nodes ([ (λ x → x) , (λ ()) ] ∘ splitAt n) (together G empty-graph)) G′ -unitaryʳ {n} {G} {G′} ≡G = record - { ↔e = e+0↔e′ + : {G : Graph n} + → Graph-same (map-nodes ([ (λ x → x) , (λ ()) ] ∘ splitAt n) (together G discrete)) G +unitaryʳ {n} {G} = record + { ↔e = e+0↔e ; ≗s = ≗s+0 ; ≗t = ≗t+0 } where - open Graph-same ≡G + open Graph G open ≡-Reasoning - e+0↔e′ : Fin (e + 0) ↔ Fin e′ - e+0↔e′ = ↔e ↔-∘ n+0↔0 e - module e+0↔e′ = Inverse e+0↔e′ - open Inverse - ↑ˡ-0 : ∀ e → (x : Fin e) → x ≡ to (n+0↔0 e) (x ↑ˡ 0) - ↑ˡ-0 (ℕ.suc ℕ.zero) zero = refl - ↑ˡ-0 (ℕ.suc (ℕ.suc e)) zero = refl - ↑ˡ-0 (ℕ.suc (ℕ.suc e)) (suc x) = cong suc (↑ˡ-0 (ℕ.suc e) x) - ≗s+0 : [ id , (λ ()) ] ∘ splitAt n ∘ join n 0 ∘ map s (λ ()) ∘ splitAt e ≗ s′ ∘ e+0↔e′.to - ≗s+0 x+0 with splitAt e x+0 in eq - ... | inj₁ x = begin - [ id , (λ ()) ] (splitAt n (join n 0 (inj₁ (s x)))) ≡⟨ cong [ id , (λ ()) ] (splitAt-join n 0 (inj₁ (s x))) ⟩ - s x ≡⟨ cong s (↑ˡ-0 e x) ⟩ - s (to (n+0↔0 e) (x ↑ˡ 0)) ≡⟨⟩ - s (to (n+0↔0 e) (join e 0 (inj₁ x))) ≡⟨ cong (s ∘ to (n+0↔0 e) ∘ join e 0) eq ⟨ - s (to (n+0↔0 e) (join e 0 (splitAt e x+0))) ≡⟨ cong (s ∘ to (n+0↔0 e)) (join-splitAt e 0 x+0) ⟩ - s (to (n+0↔0 e) x+0) ≡⟨ ≗s (to (n+0↔0 e) x+0) ⟩ - s′ (e+0↔e′.to x+0) ∎ - ≗t+0 : [ id , (λ ()) ] ∘ splitAt n ∘ join n 0 ∘ map t (λ ()) ∘ splitAt e ≗ t′ ∘ e+0↔e′.to - ≗t+0 x+0 with splitAt e x+0 in eq - ... | inj₁ x = begin - [ id , (λ ()) ] (splitAt n (join n 0 (inj₁ (t x)))) ≡⟨ cong [ id , (λ ()) ] (splitAt-join n 0 (inj₁ (t x))) ⟩ - t x ≡⟨ cong t (↑ˡ-0 e x) ⟩ - t (to (n+0↔0 e) (x ↑ˡ 0)) ≡⟨⟩ - t (to (n+0↔0 e) (join e 0 (inj₁ x))) ≡⟨ cong (t ∘ to (n+0↔0 e) ∘ join e 0) eq ⟨ - t (to (n+0↔0 e) (join e 0 (splitAt e x+0))) ≡⟨ cong (t ∘ to (n+0↔0 e)) (join-splitAt e 0 x+0) ⟩ - t (to (n+0↔0 e) x+0) ≡⟨ ≗t (to (n+0↔0 e) x+0) ⟩ - t′ (e+0↔e′.to x+0) ∎ + e+0↔e : Fin (e + 0) ↔ Fin e + e+0↔e = n+0↔n e + module e+0↔e = Inverse e+0↔e + ≗s+0 : [ id , (λ ()) ] ∘ splitAt n ∘ join n 0 ∘ map s (λ ()) ∘ splitAt e ≗ s ∘ e+0↔e.to + ≗s+0 x+0 with inj₁ x ← splitAt e x+0 = cong [ id , (λ ()) ] (splitAt-↑ˡ n (s x) 0) + ≗t+0 : [ id , (λ ()) ] ∘ splitAt n ∘ join n 0 ∘ map t (λ ()) ∘ splitAt e ≗ t ∘ e+0↔e.to + ≗t+0 x+0 with inj₁ x ← splitAt e x+0 = cong [ id , (λ ()) ] (splitAt-↑ˡ n (t x) 0) +-comm-↔ : ∀ (n m : ℕ) → Fin (n + m) ↔ Fin (m + n) +-comm-↔ n m = record @@ -655,85 +579,68 @@ join-swap (inj₁ x) = refl join-swap (inj₂ y) = refl braiding - : {G₁ G₁′ : Graph n} - → {G₂ G₂′ : Graph m} - → Graph-same G₁ G₁′ - → Graph-same G₂ G₂′ - → Graph-same (map-nodes ([ m ↑ʳ_ , _↑ˡ n ] ∘ splitAt n) (together G₁ G₂)) (together G₂′ G₁′) -braiding {n} {m} ≡G₁ ≡G₂ = record - { ↔e = +-comm-↔ ≡G₁.e′ ≡G₂.e′ ↔-∘ +-resp-↔ ≡G₁.↔e ≡G₂.↔e + : {G₁ : Graph n} + → {G₂ : Graph m} + → Graph-same (map-nodes ([ m ↑ʳ_ , _↑ˡ n ] ∘ splitAt n) (together G₁ G₂)) (together G₂ G₁) +braiding {n} {m} {G₁} {G₂} = record + { ↔e = +-comm-↔ G₁.e G₂.e ; ≗s = ≗s ; ≗t = ≗t } where open ≡-Reasoning - module ≡G₁ = Graph-same ≡G₁ - module ≡G₂ = Graph-same ≡G₂ + module G₁ = Graph G₁ + module G₂ = Graph G₂ ≗s : [ m ↑ʳ_ , _↑ˡ n ] ∘ splitAt n - ∘ join n m ∘ map ≡G₁.s ≡G₂.s ∘ splitAt ≡G₁.e - ≗ join m n ∘ map ≡G₂.s′ ≡G₁.s′ ∘ splitAt ≡G₂.e′ - ∘ join ≡G₂.e′ ≡G₁.e′ ∘ swap ∘ splitAt ≡G₁.e′ - ∘ join ≡G₁.e′ ≡G₂.e′ ∘ map ≡G₁.to ≡G₂.to ∘ splitAt ≡G₁.e + ∘ join n m ∘ map G₁.s G₂.s ∘ splitAt G₁.e + ≗ join m n ∘ map G₂.s G₁.s ∘ splitAt G₂.e + ∘ Inverse.to (+-comm-↔ G₁.e G₂.e) ≗s x = begin - ([ m ↑ʳ_ , _↑ˡ n ] ∘ splitAt n ∘ join n m ∘ map ≡G₁.s ≡G₂.s ∘ splitAt ≡G₁.e) x - ≡⟨ (join-swap ∘ splitAt n ∘ join n m ∘ map ≡G₁.s ≡G₂.s ∘ splitAt ≡G₁.e) x ⟨ - (join m n ∘ swap ∘ splitAt n ∘ join n m ∘ map ≡G₁.s ≡G₂.s ∘ splitAt ≡G₁.e) x - ≡⟨ (cong (join m n ∘ swap) ∘ splitAt-join n m ∘ map ≡G₁.s ≡G₂.s ∘ splitAt ≡G₁.e) x ⟩ - (join m n ∘ swap ∘ map ≡G₁.s ≡G₂.s ∘ splitAt ≡G₁.e) x - ≡⟨ (cong (join m n ∘ swap) ∘ map-cong ≡G₁.≗s ≡G₂.≗s ∘ splitAt ≡G₁.e) x ⟩ - (join m n ∘ swap ∘ map (≡G₁.s′ ∘ ≡G₁.to) (≡G₂.s′ ∘ ≡G₂.to) ∘ splitAt ≡G₁.e) x - ≡⟨ (cong (join m n ∘ swap) ∘ map-map ∘ splitAt ≡G₁.e) x ⟨ - (join m n ∘ swap ∘ map ≡G₁.s′ ≡G₂.s′ ∘ map ≡G₁.to ≡G₂.to ∘ splitAt ≡G₁.e) x - ≡⟨ (cong (join m n) ∘ swap-map ∘ map ≡G₁.to ≡G₂.to ∘ splitAt ≡G₁.e) x ⟩ - (join m n ∘ map ≡G₂.s′ ≡G₁.s′ ∘ swap ∘ map ≡G₁.to ≡G₂.to ∘ splitAt ≡G₁.e) x - ≡⟨ (cong (join m n ∘ map ≡G₂.s′ ≡G₁.s′ ∘ swap) ∘ splitAt-join ≡G₁.e′ ≡G₂.e′ ∘ map ≡G₁.to ≡G₂.to ∘ splitAt ≡G₁.e) x ⟨ - (join m n ∘ map ≡G₂.s′ ≡G₁.s′ ∘ swap ∘ splitAt ≡G₁.e′ ∘ join ≡G₁.e′ ≡G₂.e′ ∘ map ≡G₁.to ≡G₂.to ∘ splitAt ≡G₁.e) x - ≡⟨ (cong (join m n ∘ map ≡G₂.s′ ≡G₁.s′) ∘ splitAt-join ≡G₂.e′ ≡G₁.e′ ∘ swap ∘ splitAt ≡G₁.e′ ∘ join ≡G₁.e′ ≡G₂.e′ ∘ map ≡G₁.to ≡G₂.to ∘ splitAt ≡G₁.e) x ⟨ - (join m n ∘ map ≡G₂.s′ ≡G₁.s′ ∘ splitAt ≡G₂.e′ ∘ join ≡G₂.e′ ≡G₁.e′ ∘ swap ∘ splitAt ≡G₁.e′ ∘ join ≡G₁.e′ ≡G₂.e′ ∘ map ≡G₁.to ≡G₂.to ∘ splitAt ≡G₁.e) x ∎ + ([ m ↑ʳ_ , _↑ˡ n ] ∘ splitAt n ∘ join n m ∘ map G₁.s G₂.s ∘ splitAt G₁.e) x + ≡⟨ (join-swap ∘ splitAt n ∘ join n m ∘ map G₁.s G₂.s ∘ splitAt G₁.e) x ⟨ + (join m n ∘ swap ∘ splitAt n ∘ join n m ∘ map G₁.s G₂.s ∘ splitAt G₁.e) x + ≡⟨ (cong (join m n ∘ swap) ∘ splitAt-join n m ∘ map G₁.s G₂.s ∘ splitAt G₁.e) x ⟩ + (join m n ∘ swap ∘ map G₁.s G₂.s ∘ splitAt G₁.e) x + ≡⟨ (cong (join m n) ∘ swap-map ∘ splitAt G₁.e) x ⟩ + (join m n ∘ map G₂.s G₁.s ∘ swap ∘ splitAt G₁.e) x + ≡⟨ (cong (join m n ∘ map G₂.s G₁.s) ∘ splitAt-join G₂.e G₁.e ∘ swap ∘ splitAt G₁.e) x ⟨ + (join m n ∘ map G₂.s G₁.s ∘ splitAt G₂.e ∘ join G₂.e G₁.e ∘ swap ∘ splitAt G₁.e) x ∎ ≗t : [ m ↑ʳ_ , _↑ˡ n ] ∘ splitAt n - ∘ join n m ∘ map ≡G₁.t ≡G₂.t ∘ splitAt ≡G₁.e - ≗ join m n ∘ map ≡G₂.t′ ≡G₁.t′ ∘ splitAt ≡G₂.e′ - ∘ join ≡G₂.e′ ≡G₁.e′ ∘ swap ∘ splitAt ≡G₁.e′ - ∘ join ≡G₁.e′ ≡G₂.e′ ∘ map ≡G₁.to ≡G₂.to ∘ splitAt ≡G₁.e + ∘ join n m ∘ map G₁.t G₂.t ∘ splitAt G₁.e + ≗ join m n ∘ map G₂.t G₁.t ∘ splitAt G₂.e + ∘ Inverse.to (+-comm-↔ G₁.e G₂.e) ≗t x = begin - ([ m ↑ʳ_ , _↑ˡ n ] ∘ splitAt n ∘ join n m ∘ map ≡G₁.t ≡G₂.t ∘ splitAt ≡G₁.e) x - ≡⟨ (join-swap ∘ splitAt n ∘ join n m ∘ map ≡G₁.t ≡G₂.t ∘ splitAt ≡G₁.e) x ⟨ - (join m n ∘ swap ∘ splitAt n ∘ join n m ∘ map ≡G₁.t ≡G₂.t ∘ splitAt ≡G₁.e) x - ≡⟨ (cong (join m n ∘ swap) ∘ splitAt-join n m ∘ map ≡G₁.t ≡G₂.t ∘ splitAt ≡G₁.e) x ⟩ - (join m n ∘ swap ∘ map ≡G₁.t ≡G₂.t ∘ splitAt ≡G₁.e) x - ≡⟨ (cong (join m n ∘ swap) ∘ map-cong ≡G₁.≗t ≡G₂.≗t ∘ splitAt ≡G₁.e) x ⟩ - (join m n ∘ swap ∘ map (≡G₁.t′ ∘ ≡G₁.to) (≡G₂.t′ ∘ ≡G₂.to) ∘ splitAt ≡G₁.e) x - ≡⟨ (cong (join m n ∘ swap) ∘ map-map ∘ splitAt ≡G₁.e) x ⟨ - (join m n ∘ swap ∘ map ≡G₁.t′ ≡G₂.t′ ∘ map ≡G₁.to ≡G₂.to ∘ splitAt ≡G₁.e) x - ≡⟨ (cong (join m n) ∘ swap-map ∘ map ≡G₁.to ≡G₂.to ∘ splitAt ≡G₁.e) x ⟩ - (join m n ∘ map ≡G₂.t′ ≡G₁.t′ ∘ swap ∘ map ≡G₁.to ≡G₂.to ∘ splitAt ≡G₁.e) x - ≡⟨ (cong (join m n ∘ map ≡G₂.t′ ≡G₁.t′ ∘ swap) ∘ splitAt-join ≡G₁.e′ ≡G₂.e′ ∘ map ≡G₁.to ≡G₂.to ∘ splitAt ≡G₁.e) x ⟨ - (join m n ∘ map ≡G₂.t′ ≡G₁.t′ ∘ swap ∘ splitAt ≡G₁.e′ ∘ join ≡G₁.e′ ≡G₂.e′ ∘ map ≡G₁.to ≡G₂.to ∘ splitAt ≡G₁.e) x - ≡⟨ (cong (join m n ∘ map ≡G₂.t′ ≡G₁.t′) ∘ splitAt-join ≡G₂.e′ ≡G₁.e′ ∘ swap ∘ splitAt ≡G₁.e′ ∘ join ≡G₁.e′ ≡G₂.e′ ∘ map ≡G₁.to ≡G₂.to ∘ splitAt ≡G₁.e) x ⟨ - (join m n ∘ map ≡G₂.t′ ≡G₁.t′ ∘ splitAt ≡G₂.e′ ∘ join ≡G₂.e′ ≡G₁.e′ ∘ swap ∘ splitAt ≡G₁.e′ ∘ join ≡G₁.e′ ≡G₂.e′ ∘ map ≡G₁.to ≡G₂.to ∘ splitAt ≡G₁.e) x ∎ - -graph : SymmetricMonoidalFunctor Nat-smc (Setoids-× {0ℓ}) -graph = record - { F = F - ; isBraidedMonoidal = record - { isMonoidal = record - { ε = ε - ; ⊗-homo = ⊗-homomorphism - ; associativity = λ { ((≡G₁ , ≡G₂) , ≡G₃) → associativity ≡G₁ ≡G₂ ≡G₃ } - ; unitaryˡ = λ { (lift tt , ≡G) → unitaryˡ ≡G } - ; unitaryʳ = λ { (≡G , lift tt) → unitaryʳ ≡G } - } - ; braiding-compat = λ { (≡G₁ , ≡G₂) → braiding ≡G₁ ≡G₂ } - } - } + ([ m ↑ʳ_ , _↑ˡ n ] ∘ splitAt n ∘ join n m ∘ map G₁.t G₂.t ∘ splitAt G₁.e) x + ≡⟨ (join-swap ∘ splitAt n ∘ join n m ∘ map G₁.t G₂.t ∘ splitAt G₁.e) x ⟨ + (join m n ∘ swap ∘ splitAt n ∘ join n m ∘ map G₁.t G₂.t ∘ splitAt G₁.e) x + ≡⟨ (cong (join m n ∘ swap) ∘ splitAt-join n m ∘ map G₁.t G₂.t ∘ splitAt G₁.e) x ⟩ + (join m n ∘ swap ∘ map G₁.t G₂.t ∘ splitAt G₁.e) x + ≡⟨ (cong (join m n) ∘ swap-map ∘ splitAt G₁.e) x ⟩ + (join m n ∘ map G₂.t G₁.t ∘ swap ∘ splitAt G₁.e) x + ≡⟨ (cong (join m n ∘ map G₂.t G₁.t) ∘ splitAt-join G₂.e G₁.e ∘ swap ∘ splitAt G₁.e) x ⟨ + (join m n ∘ map G₂.t G₁.t ∘ splitAt G₂.e ∘ join G₂.e G₁.e ∘ swap ∘ splitAt G₁.e) x ∎ + +opaque + unfolding ×-symmetric′ + graph : SymmetricMonoidalFunctor Nat-smc Setoids-× + graph = record + { F = F + ; isBraidedMonoidal = record + { isMonoidal = record + { ε = ε + ; ⊗-homo = ⊗-homomorphism + ; associativity = λ { {x} {y} {z} {(G₁ , G₂) , G₃} → associativity G₁ G₂ G₃ } + ; unitaryˡ = unitaryˡ + ; unitaryʳ = unitaryʳ + } + ; braiding-compat = λ { {x} {y} {G₁ , G₂} → braiding {G₁ = G₁} {G₂ = G₂} } + } + } module F = SymmetricMonoidalFunctor graph -and-gate : Func (SingletonSetoid {0ℓ} {0ℓ}) (F.₀ 3) -and-gate = record - { to = λ { (lift tt) → and-graph } - ; cong = λ { (lift tt) → Graph-same-refl } - } +and-gate : Func ⊤ₛ (Graph-setoid 3) +and-gate = Const ⊤ₛ (Graph-setoid 3) and-graph where and-graph : Graph 3 and-graph = record diff --git a/DecorationFunctor/Hypergraph.agda b/DecorationFunctor/Hypergraph.agda new file mode 100644 index 0000000..2f61bc3 --- /dev/null +++ b/DecorationFunctor/Hypergraph.agda @@ -0,0 +1,653 @@ +{-# OPTIONS --without-K --safe #-} + +module DecorationFunctor.Hypergraph where + +import Categories.Morphism as Morphism +open import Level using (0ℓ) + +open import Categories.Category.BinaryProducts using (module BinaryProducts) +open import Categories.Category.Cartesian using (Cartesian) +open import Categories.Category.Core using (Category) +open import Categories.Category.Instance.Nat using (Nat) +open import Categories.Category.Instance.Setoids using (Setoids) +open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian) +open import Categories.Category.Product using (_⁂_) +open import Categories.Functor using () renaming (_∘F_ to _∘′_) +open import Categories.Functor.Core using (Functor) +open import Categories.Functor.Monoidal.Symmetric using (module Lax) +open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) +open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory) +open import Category.Instance.Nat.FinitelyCocomplete using (Nat-FinitelyCocomplete) +open import Category.Instance.Setoids.SymmetricMonoidal {0ℓ} {0ℓ} using (Setoids-×; ×-symmetric′) +open import Data.Empty using (⊥-elim) +open import Data.Fin using (#_; Fin; splitAt; join; zero; suc; _↑ˡ_; _↑ʳ_; toℕ; cast) +open import Data.Fin.Patterns using (0F; 1F; 2F) +open import Data.Fin.Properties using (splitAt-join; join-splitAt; cast-is-id; cast-trans; toℕ-cast; subst-is-cast; splitAt-↑ˡ; splitAt-↑ʳ; splitAt⁻¹-↑ˡ; ↑ˡ-injective) +open import Data.Nat using (ℕ; _+_) +open import Data.Product.Base using (_,_; Σ) +open import Data.Setoid using (∣_∣) +open import Data.Setoid.Unit {0ℓ} {0ℓ} using (⊤ₛ) +open import Data.Sum using (_⊎_; map; inj₁; inj₂; swap; map₂) renaming ([_,_]′ to [_,_]) +open import Data.Sum.Properties using (map-map; [,]-map; [,]-∘; [-,]-cong; [,-]-cong; [,]-cong; map-cong; swap-involutive) +open import Data.Unit using (tt) +open import Function using (_∘_; id; const; Func; Inverse; _↔_; mk↔; _⟨$⟩_) +open import Function.Construct.Composition using (_↔-∘_) +open import Function.Construct.Constant using () renaming (function to Const) +open import Function.Construct.Identity using (↔-id) renaming (function to Id) +open import Function.Construct.Symmetry using (↔-sym) +open import Relation.Binary using (Setoid) +open import Relation.Binary.PropositionalEquality.Core using (_≗_; _≡_; erefl; refl; sym; trans; cong; cong₂; subst; cong-app) +open import Relation.Binary.PropositionalEquality.Properties using (isEquivalence; module ≡-Reasoning; dcong₂; subst-∘) +open import Relation.Nullary.Negation.Core using (¬_) + +open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using (products) +open FinitelyCocompleteCategory Nat-FinitelyCocomplete + using (-+-; _+₁_) + renaming (symmetricMonoidalCategory to Nat-smc; +-assoc to Nat-+-assoc) +open Morphism (Setoids 0ℓ 0ℓ) using (_≅_) +open Lax using (SymmetricMonoidalFunctor) + +open BinaryProducts products using (-×-) + +record Hypergraph (v : ℕ) : Set where + + field + h : ℕ + a : Fin h → ℕ + + arity : Fin h → ℕ + arity = ℕ.suc ∘ a + + field + j : ∀ (e : Fin h) → Fin (arity e) → Fin v + +record Hypergraph-same {n : ℕ} (H H′ : Hypergraph n) : Set where + + open Hypergraph H public + open Hypergraph H′ renaming (h to h′; a to a′; arity to arity′; j to j′) public + + field + ↔h : Fin h ↔ Fin h′ + + open Inverse ↔h public + + field + ≗a : a ≗ a′ ∘ to + + ≗arity : arity ≗ arity′ ∘ to + ≗arity e = cong ℕ.suc (≗a e) + + field + ≗j : (e : Fin h) + (i : Fin (arity e)) + → j e i + ≡ j′ (to e) (cast (≗arity e) i) + +private + + variable + n n′ m m′ o : ℕ + H H′ H″ H₁ H₁′ : Hypergraph n + H₂ H₂′ : Hypergraph m + H₃ : Hypergraph o + +Hypergraph-same-refl : Hypergraph-same H H +Hypergraph-same-refl {_} {H} = record + { ↔h = ↔-id (Fin h) + ; ≗a = cong a ∘ erefl + ; ≗j = λ e i → cong (j e) (sym (cast-is-id refl i)) + } + where + open Hypergraph H + +Hypergraph-same-sym : Hypergraph-same H H′ → Hypergraph-same H′ H +Hypergraph-same-sym {V} {H} {H′} ≡H = record + { ↔h = ↔-sym ↔h + ; ≗a = sym ∘ a∘from≗a′ + ; ≗j = ≗j′ + } + where + open Hypergraph-same ≡H + open ≡-Reasoning + a∘from≗a′ : a ∘ from ≗ a′ + a∘from≗a′ x = begin + (a ∘ from) x ≡⟨ (≗a ∘ from) x ⟩ + (a′ ∘ to ∘ from) x ≡⟨ (cong a′ ∘ inverseˡ ∘ erefl ∘ from) x ⟩ + a′ x ∎ + id≗to∘from : id ≗ to ∘ from + id≗to∘from e = sym (inverseˡ refl) + ≗arity′ : arity′ ≗ arity ∘ from + ≗arity′ e = cong ℕ.suc (sym (a∘from≗a′ e)) + ≗arity- : arity′ ≗ arity′ ∘ to ∘ from + ≗arity- e = cong arity′ (id≗to∘from e) + ≗j′ : (e : Fin h′) (i : Fin (arity′ e)) → j′ e i ≡ j (from e) (cast (≗arity′ e) i) + ≗j′ e i = begin + j′ e i ≡⟨ dcong₂ j′ (id≗to∘from e) (subst-∘ (id≗to∘from e)) ⟩ + j′ (to (from e)) (subst Fin (cong arity′ (id≗to∘from e)) i) ≡⟨ cong (j′ (to (from e))) (subst-is-cast (cong arity′ (id≗to∘from e)) i) ⟩ + j′ (to (from e)) (cast (cong arity′ (id≗to∘from e)) i) ≡⟨⟩ + j′ (to (from e)) (cast (trans (≗arity′ e) (≗arity (from e))) i) ≡⟨ cong (j′ (to (from e))) (cast-trans (≗arity′ e) (≗arity (from e)) i) ⟨ + j′ (to (from e)) (cast (≗arity (from e)) (cast (≗arity′ e) i)) ≡⟨ ≗j (from e) (cast (≗arity′ e) i) ⟨ + j (from e) (cast (≗arity′ e) i) ∎ + +Hypergraph-same-trans : Hypergraph-same H H′ → Hypergraph-same H′ H″ → Hypergraph-same H H″ +Hypergraph-same-trans ≡H₁ ≡H₂ = record + { ↔h = ↔h ≡H₂ ↔-∘ ↔h ≡H₁ + ; ≗a = λ { x → trans (≗a ≡H₁ x) (≗a ≡H₂ (to (↔h ≡H₁) x)) } + ; ≗j = λ { e i → trans (≗j ≡H₁ e i) (≗j₂ e i) } + } + where + open Hypergraph-same + open Inverse + open ≡-Reasoning + ≗j₂ : (e : Fin (h ≡H₁)) + (i : Fin (arity ≡H₁ e)) + → j ≡H₂ (to (↔h ≡H₁) e) (cast (≗arity ≡H₁ e) i) + ≡ j′ ≡H₂ (to (↔h ≡H₂) (to (↔h ≡H₁) e)) (cast (trans (≗arity ≡H₁ e) (≗arity ≡H₂ (to (↔h ≡H₁) e))) i) + ≗j₂ e i = begin + j ≡H₂ (to (↔h ≡H₁) e) (cast (≗arity ≡H₁ e) i) + ≡⟨ ≗j ≡H₂ (to (↔h ≡H₁) e) (cast (≗arity ≡H₁ e) i) ⟩ + j′ ≡H₂ (to (↔h ≡H₂) (to (↔h ≡H₁) e)) (cast (≗arity ≡H₂ (to (↔h ≡H₁) e)) (cast (≗arity ≡H₁ e) i)) + ≡⟨ cong (j′ ≡H₂ (to (↔h ≡H₂) (to (↔h ≡H₁) e))) (cast-trans (≗arity ≡H₁ e) (≗arity ≡H₂ (to (↔h ≡H₁) e)) i) ⟩ + j′ ≡H₂ (to (↔h ≡H₂) (to (↔h ≡H₁) e)) (cast (trans (≗arity ≡H₁ e) (≗arity ≡H₂ (to (↔h ≡H₁) e))) i) ∎ + +Hypergraphₛ : ℕ → Setoid 0ℓ 0ℓ +Hypergraphₛ p = record + { Carrier = Hypergraph p + ; _≈_ = Hypergraph-same + ; isEquivalence = record + { refl = Hypergraph-same-refl + ; sym = Hypergraph-same-sym + ; trans = Hypergraph-same-trans + } + } + +map-nodes : (Fin n → Fin m) → Hypergraph n → Hypergraph m +map-nodes f H = record + { h = h + ; a = a + ; j = λ e i → f (j e i) + } + where + open Hypergraph H + +Hypergraph-same-cong + : (f : Fin n → Fin m) + → Hypergraph-same H H′ + → Hypergraph-same (map-nodes f H) (map-nodes f H′) +Hypergraph-same-cong f ≡H = record + { ↔h = ↔h + ; ≗a = ≗a + ; ≗j = λ e i → cong f (≗j e i) + } + where + open Hypergraph-same ≡H + +Hypergraph-Func : (Fin n → Fin m) → Func (Hypergraphₛ n) (Hypergraphₛ m) +Hypergraph-Func f = record + { to = map-nodes f + ; cong = Hypergraph-same-cong f + } + +F-resp-≈ + : {f g : Fin n → Fin m} + → f ≗ g + → Hypergraph-same (map-nodes f H) (map-nodes g H) +F-resp-≈ {g = g} f≗g = record + { ↔h = ↔h + ; ≗a = ≗a + ; ≗j = λ { e i → trans (f≗g (j e i)) (cong g (≗j e i)) } + } + where + open Hypergraph-same Hypergraph-same-refl + +homomorphism + : (f : Fin n → Fin m) + → (g : Fin m → Fin o) + → Hypergraph-same (map-nodes (g ∘ f) H) (map-nodes g (map-nodes f H)) +homomorphism {n} {m} {o} {H} f g = record + { ↔h = ↔h + ; ≗a = ≗a + ; ≗j = λ e i → cong (g ∘ f) (≗j e i) + } + where + open Hypergraph-same Hypergraph-same-refl + +F : Functor Nat (Setoids 0ℓ 0ℓ) +F = record + { F₀ = Hypergraphₛ + ; F₁ = Hypergraph-Func + ; identity = λ { {n} {H} → Hypergraph-same-refl {H = H} } + ; homomorphism = λ { {f = f} {g = g} → homomorphism f g } + ; F-resp-≈ = λ f≗g → F-resp-≈ f≗g + } + +-- monoidal structure + +discrete : {n : ℕ} → Hypergraph n +discrete {n} = record + { h = 0 + ; a = λ () + ; j = λ () + } + +opaque + unfolding ×-symmetric′ + + ε : Func Setoids-×.unit (Hypergraphₛ 0) + ε = Const ⊤ₛ (Hypergraphₛ 0) discrete + +module _ (H₁ : Hypergraph n) (H₂ : Hypergraph m) where + private + module H₁ = Hypergraph H₁ + module H₂ = Hypergraph H₂ + j+j : (e : Fin (H₁.h + H₂.h)) + → Fin (ℕ.suc ([ H₁.a , H₂.a ] (splitAt H₁.h e))) + → Fin (n + m) + j+j e i with splitAt H₁.h e + ... | inj₁ e₁ = H₁.j e₁ i ↑ˡ m + ... | inj₂ e₂ = n ↑ʳ H₂.j e₂ i + +together : Hypergraph n → Hypergraph m → Hypergraph (n + m) +together {n} {m} H₁ H₂ = record + { h = h H₁ + h H₂ + ; a = [ a H₁ , a H₂ ] ∘ splitAt (h H₁) + ; j = j+j H₁ H₂ + } + where + open Hypergraph + ++-resp-↔ + : {n n′ m m′ : ℕ} + → Fin n ↔ Fin n′ + → Fin m ↔ Fin m′ + → Fin (n + m) ↔ Fin (n′ + m′) ++-resp-↔ {n} {n′} {m} {m′} ↔n ↔m = record + { to = join n′ m′ ∘ map ↔n.to ↔m.to ∘ splitAt n + ; from = join n m ∘ map ↔n.from ↔m.from ∘ splitAt n′ + ; to-cong = cong (join n′ m′ ∘ map ↔n.to ↔m.to ∘ splitAt n) + ; from-cong = cong (join n m ∘ map ↔n.from ↔m.from ∘ splitAt n′) + ; inverse = (λ { refl → to∘from _ }) , λ { refl → from∘to _ } + } + where + module ↔n = Inverse ↔n + module ↔m = Inverse ↔m + open ≡-Reasoning + to∘from : join n′ m′ ∘ map ↔n.to ↔m.to ∘ splitAt n ∘ join n m ∘ map ↔n.from ↔m.from ∘ splitAt n′ ≗ id + to∘from x = begin + (join n′ m′ ∘ map ↔n.to ↔m.to ∘ splitAt n ∘ join n m ∘ map ↔n.from ↔m.from ∘ splitAt n′) x + ≡⟨ cong + (join n′ m′ ∘ map ↔n.to ↔m.to) + (splitAt-join n m (map ↔n.from ↔m.from (splitAt n′ x))) ⟩ + (join n′ m′ ∘ map ↔n.to ↔m.to ∘ map ↔n.from ↔m.from ∘ splitAt n′) x + ≡⟨ cong (join n′ m′) (map-map (splitAt n′ x)) ⟩ + (join n′ m′ ∘ map (↔n.to ∘ ↔n.from) (↔m.to ∘ ↔m.from) ∘ splitAt n′) x + ≡⟨ cong + (join n′ m′) + (map-cong + (λ _ → ↔n.inverseˡ refl) + (λ _ → ↔m.inverseˡ refl) + (splitAt n′ x)) ⟩ + (join n′ m′ ∘ map id id ∘ splitAt n′) x ≡⟨ [,]-map (splitAt n′ x) ⟩ + (join n′ m′ ∘ splitAt n′) x ≡⟨ join-splitAt n′ m′ x ⟩ + x ∎ + from∘to : join n m ∘ map ↔n.from ↔m.from ∘ splitAt n′ ∘ join n′ m′ ∘ map ↔n.to ↔m.to ∘ splitAt n ≗ id + from∘to x = begin + (join n m ∘ map ↔n.from ↔m.from ∘ splitAt n′ ∘ join n′ m′ ∘ map ↔n.to ↔m.to ∘ splitAt n) x + ≡⟨ cong + (join n m ∘ map ↔n.from ↔m.from) + (splitAt-join n′ m′ (map ↔n.to ↔m.to (splitAt n x))) ⟩ + (join n m ∘ map ↔n.from ↔m.from ∘ map ↔n.to ↔m.to ∘ splitAt n) x + ≡⟨ cong (join n m) (map-map (splitAt n x)) ⟩ + (join n m ∘ map (↔n.from ∘ ↔n.to) (↔m.from ∘ ↔m.to) ∘ splitAt n) x + ≡⟨ cong + (join n m) + (map-cong + (λ _ → ↔n.inverseʳ refl) + (λ _ → ↔m.inverseʳ refl) + (splitAt n x)) ⟩ + (join n m ∘ map id id ∘ splitAt n) x ≡⟨ [,]-map (splitAt n x) ⟩ + (join n m ∘ splitAt n) x ≡⟨ join-splitAt n m x ⟩ + x ∎ + +together-resp-same + : Hypergraph-same H₁ H₁′ + → Hypergraph-same H₂ H₂′ + → Hypergraph-same (together H₁ H₂) (together H₁′ H₂′) +together-resp-same {n} {H₁} {H₁′} {m} {H₂} {H₂′} ≡H₁ ≡H₂ = record + { ↔h = +-resp-↔ ≡H₁.↔h ≡H₂.↔h + ; ≗a = ≗a + ; ≗j = ≗j + } + where + module ≡H₁ = Hypergraph-same ≡H₁ + module ≡H₂ = Hypergraph-same ≡H₂ + module H₁+H₂ = Hypergraph (together H₁ H₂) + module H₁+H₂′ = Hypergraph (together H₁′ H₂′) + open ≡-Reasoning + open Inverse + open Hypergraph + ≗a : [ ≡H₁.a , ≡H₂.a ] ∘ splitAt ≡H₁.h + ≗ [ ≡H₁.a′ , ≡H₂.a′ ] ∘ splitAt ≡H₁.h′ + ∘ join ≡H₁.h′ ≡H₂.h′ ∘ map ≡H₁.to ≡H₂.to ∘ splitAt ≡H₁.h + ≗a e = begin + [ ≡H₁.a , ≡H₂.a ] (splitAt ≡H₁.h e) ≡⟨ [,]-cong ≡H₁.≗a ≡H₂.≗a (splitAt ≡H₁.h e) ⟩ + ([ ≡H₁.a′ ∘ ≡H₁.to , ≡H₂.a′ ∘ ≡H₂.to ] ∘ splitAt ≡H₁.h) e ≡⟨ [,]-map (splitAt ≡H₁.h e) ⟨ + ([ ≡H₁.a′ , ≡H₂.a′ ] ∘ map ≡H₁.to ≡H₂.to ∘ splitAt ≡H₁.h) e ≡⟨ (cong [ ≡H₁.a′ , ≡H₂.a′ ] ∘ splitAt-join ≡H₁.h′ ≡H₂.h′ ∘ map ≡H₁.to ≡H₂.to ∘ splitAt ≡H₁.h) e ⟨ + ([ ≡H₁.a′ , ≡H₂.a′ ] ∘ splitAt ≡H₁.h′ ∘ join ≡H₁.h′ ≡H₂.h′ ∘ map ≡H₁.to ≡H₂.to ∘ splitAt ≡H₁.h) e ∎ + ≗arity : H₁+H₂.arity ≗ H₁+H₂′.arity ∘ join ≡H₁.h′ ≡H₂.h′ ∘ map ≡H₁.to ≡H₂.to ∘ splitAt ≡H₁.h + ≗arity = cong ℕ.suc ∘ ≗a + ≗j : (e : Fin H₁+H₂.h) + (i : Fin (H₁+H₂.arity e)) + → H₁+H₂.j e i + ≡ H₁+H₂′.j (to (+-resp-↔ ≡H₁.↔h ≡H₂.↔h) e) (cast (cong ℕ.suc (≗a e)) i) + ≗j e i with splitAt ≡H₁.h e + ... | inj₁ e₁ rewrite splitAt-↑ˡ ≡H₁.h′ (≡H₁.to e₁) ≡H₂.h′ = cong (_↑ˡ m) (≡H₁.≗j e₁ i) + ... | inj₂ e₂ rewrite splitAt-↑ʳ ≡H₁.h′ ≡H₂.h′ (≡H₂.to e₂) = cong (n ↑ʳ_) (≡H₂.≗j e₂ i) + +commute + : (f : Fin n → Fin n′) + → (g : Fin m → Fin m′) + → Hypergraph-same + (together (map-nodes f H₁) (map-nodes g H₂)) + (map-nodes (f +₁ g) (together H₁ H₂)) +commute {n} {n′} {m} {m′} {H₁} {H₂} f g = record + { ↔h = ≡H₁+H₂.↔h + ; ≗a = ≡H₁+H₂.≗a + ; ≗j = ≗j + } + where + module H₁ = Hypergraph H₁ + module H₂ = Hypergraph H₂ + module H₁+H₂ = Hypergraph (together H₁ H₂) + module ≡H₁+H₂ = Hypergraph-same {H = together H₁ H₂} Hypergraph-same-refl + open Hypergraph + open ≡-Reasoning + ≗j : (e : Fin (H₁.h + H₂.h)) + (i : Fin ((ℕ.suc ∘ [ H₁.a , H₂.a ] ∘ splitAt H₁.h) e)) + → j (together (map-nodes f H₁) (map-nodes g H₂)) e i + ≡ j (map-nodes (f +₁ g) (together H₁ H₂)) (≡H₁+H₂.to e) (cast refl i) + ≗j e i with splitAt H₁.h e + ... | inj₁ e₁ rewrite splitAt-↑ˡ n (H₁.j e₁ (cast refl i)) m = cong ((_↑ˡ m′) ∘ f ∘ H₁.j e₁) (sym (cast-is-id refl i)) + ... | inj₂ e₂ rewrite splitAt-↑ʳ n m (H₂.j e₂ (cast refl i)) = cong ((n′ ↑ʳ_) ∘ g ∘ H₂.j e₂) (sym (cast-is-id refl i)) + +open Setoids-× using (_⊗₀_; _⊗₁_) +opaque + unfolding ×-symmetric′ + η : Func (Hypergraphₛ n ⊗₀ Hypergraphₛ m) (Hypergraphₛ (n + m)) + η = record + { to = λ (H₁ , H₂) → together H₁ H₂ + ; cong = λ (≡H₁ , ≡H₂) → together-resp-same ≡H₁ ≡H₂ + } + +opaque + unfolding η + commute′ + : (f : Fin n → Fin n′) + → (g : Fin m → Fin m′) + → {x : ∣ Hypergraphₛ n ⊗₀ Hypergraphₛ m ∣} + → Hypergraph-same + (η ⟨$⟩ (Hypergraph-Func f ⊗₁ Hypergraph-Func g ⟨$⟩ x)) + (map-nodes (f +₁ g) (η ⟨$⟩ x)) + commute′ f g {H₁ , H₂} = commute {H₁ = H₁} {H₂} f g + +⊗-homomorphism : NaturalTransformation (Setoids-×.⊗ ∘′ (F ⁂ F)) (F ∘′ -+-) +⊗-homomorphism = ntHelper record + { η = λ (n , m) → η {n} {m} + ; commute = λ (f , g) → commute′ f g + } + ++-assoc-↔ : ∀ (x y z : ℕ) → Fin (x + y + z) ↔ Fin (x + (y + z)) ++-assoc-↔ x y z = record + { to = to + ; from = from + ; to-cong = λ { refl → refl } + ; from-cong = λ { refl → refl } + ; inverse = (λ { refl → isoˡ _ }) , λ { refl → isoʳ _ } + } + where + module Nat = Morphism Nat + open Nat._≅_ (Nat-+-assoc {x} {y} {z}) + +associativity + : {X Y Z : ℕ} + → (H₁ : Hypergraph X) + → (H₂ : Hypergraph Y) + → (H₃ : Hypergraph Z) + → Hypergraph-same + (map-nodes (Inverse.to (+-assoc-↔ X Y Z)) (together (together H₁ H₂) H₃)) + (together H₁ (together H₂ H₃)) +associativity {X} {Y} {Z} H₁ H₂ H₃ = record + { ↔h = ↔h + ; ≗a = ≗a + ; ≗j = ≗j + } + where + module H₁ = Hypergraph H₁ + module H₂ = Hypergraph H₂ + module H₃ = Hypergraph H₃ + open ≡-Reasoning + open Hypergraph + ↔h : Fin (H₁.h + H₂.h + H₃.h) ↔ Fin (H₁.h + (H₂.h + H₃.h)) + ↔h = +-assoc-↔ H₁.h H₂.h H₃.h + ≗a : (x : Fin (H₁.h + H₂.h + H₃.h)) + → [ [ H₁.a , H₂.a ] ∘ splitAt H₁.h , H₃.a ] (splitAt (H₁.h + H₂.h) x) + ≡ [ H₁.a , [ H₂.a , H₃.a ] ∘ splitAt H₂.h ] (splitAt H₁.h ([ [ _↑ˡ H₂.h + H₃.h , (H₁.h ↑ʳ_) ∘ (_↑ˡ H₃.h) ] ∘ splitAt H₁.h , (H₁.h ↑ʳ_) ∘ (H₂.h ↑ʳ_) ] (splitAt (H₁.h + H₂.h) x))) + ≗a x = begin + ([ [ H₁.a , H₂.a ] ∘ splitAt H₁.h , H₃.a ] ∘ splitAt (H₁.h + H₂.h)) x + ≡⟨⟩ + ([ [ H₁.a , [ H₂.a , H₃.a ] ∘ inj₁ ] ∘ splitAt H₁.h , H₃.a ] ∘ splitAt (H₁.h + H₂.h)) x + ≡⟨ [-,]-cong ([,-]-cong (cong [ H₂.a , H₃.a ] ∘ (λ i → splitAt-↑ˡ H₂.h i H₃.h)) ∘ splitAt H₁.h) (splitAt (H₁.h + H₂.h) x) ⟨ + ([ [ H₁.a , [ H₂.a , H₃.a ] ∘ splitAt H₂.h ∘ (_↑ˡ H₃.h) ] ∘ splitAt H₁.h , H₃.a ] ∘ splitAt (H₁.h + H₂.h)) x + ≡⟨ [-,]-cong ([,]-∘ [ H₁.a , [ H₂.a , H₃.a ] ∘ splitAt H₂.h ] ∘ splitAt H₁.h) (splitAt (H₁.h + H₂.h) x) ⟨ + ([ [ H₁.a , [ H₂.a , H₃.a ] ∘ splitAt H₂.h ] ∘ map₂ (_↑ˡ H₃.h) ∘ splitAt H₁.h , H₃.a ] ∘ splitAt (H₁.h + H₂.h)) x + ≡⟨⟩ + ([ [ H₁.a , [ H₂.a , H₃.a ] ∘ splitAt H₂.h ] ∘ map₂ (_↑ˡ H₃.h) ∘ splitAt H₁.h , [ H₂.a , H₃.a ] ∘ inj₂ ] ∘ splitAt (H₁.h + H₂.h)) x + ≡⟨ [,-]-cong (cong [ H₂.a , H₃.a ] ∘ splitAt-↑ʳ H₂.h H₃.h) (splitAt (H₁.h + H₂.h) x) ⟨ + ([ [ H₁.a , [ H₂.a , H₃.a ] ∘ splitAt H₂.h ] ∘ map₂ (_↑ˡ H₃.h) ∘ splitAt H₁.h , [ H₂.a , H₃.a ] ∘ splitAt H₂.h ∘ (H₂.h ↑ʳ_) ] ∘ splitAt (H₁.h + H₂.h)) x + ≡⟨⟩ + ([ [ H₁.a , [ H₂.a , H₃.a ] ∘ splitAt H₂.h ] ∘ map₂ (_↑ˡ H₃.h) ∘ splitAt H₁.h , [ H₁.a , [ H₂.a , H₃.a ] ∘ splitAt H₂.h ] ∘ inj₂ ∘ (H₂.h ↑ʳ_) ] ∘ splitAt (H₁.h + H₂.h)) x + ≡⟨ [,]-∘ [ H₁.a , [ H₂.a , H₃.a ] ∘ splitAt H₂.h ] (splitAt (H₁.h + H₂.h) x) ⟨ + ([ H₁.a , [ H₂.a , H₃.a ] ∘ splitAt H₂.h ] ∘ [ map₂ (_↑ˡ H₃.h) ∘ splitAt H₁.h , inj₂ ∘ (H₂.h ↑ʳ_) ] ∘ splitAt (H₁.h + H₂.h)) x + ≡⟨ cong [ H₁.a , [ H₂.a , H₃.a ] ∘ splitAt H₂.h ] ([,-]-cong (splitAt-↑ʳ H₁.h (H₂.h + H₃.h) ∘ (H₂.h ↑ʳ_)) (splitAt (H₁.h + H₂.h) x)) ⟨ + ([ H₁.a , [ H₂.a , H₃.a ] ∘ splitAt H₂.h ] ∘ [ map₂ (_↑ˡ H₃.h) ∘ splitAt H₁.h , splitAt H₁.h ∘ (H₁.h ↑ʳ_) ∘ (H₂.h ↑ʳ_) ] ∘ splitAt (H₁.h + H₂.h)) x + ≡⟨ cong [ H₁.a , [ H₂.a , H₃.a ] ∘ splitAt H₂.h ] ([-,]-cong (splitAt-join H₁.h (H₂.h + H₃.h) ∘ map₂ (_↑ˡ H₃.h) ∘ splitAt H₁.h) (splitAt (H₁.h + H₂.h) x)) ⟨ + ([ H₁.a , [ H₂.a , H₃.a ] ∘ splitAt H₂.h ] ∘ [ splitAt H₁.h ∘ join H₁.h (H₂.h + H₃.h) ∘ map₂ (_↑ˡ H₃.h) ∘ splitAt H₁.h , splitAt H₁.h ∘ (H₁.h ↑ʳ_) ∘ (H₂.h ↑ʳ_) ] ∘ splitAt (H₁.h + H₂.h)) x + ≡⟨ cong [ H₁.a , [ H₂.a , H₃.a ] ∘ splitAt H₂.h ] ([,]-∘ (splitAt H₁.h) (splitAt (H₁.h + H₂.h) x)) ⟨ + ([ H₁.a , [ H₂.a , H₃.a ] ∘ splitAt H₂.h ] ∘ splitAt H₁.h ∘ [ join H₁.h (H₂.h + H₃.h) ∘ map₂ (_↑ˡ H₃.h) ∘ splitAt H₁.h , (H₁.h ↑ʳ_) ∘ (H₂.h ↑ʳ_) ] ∘ splitAt (H₁.h + H₂.h)) x + ≡⟨⟩ + ([ H₁.a , [ H₂.a , H₃.a ] ∘ splitAt H₂.h ] ∘ splitAt H₁.h ∘ [ [ _↑ˡ H₂.h + H₃.h , H₁.h ↑ʳ_ ] ∘ [ inj₁ , inj₂ ∘ (_↑ˡ H₃.h) ] ∘ splitAt H₁.h , (H₁.h ↑ʳ_) ∘ (H₂.h ↑ʳ_) ] ∘ splitAt (H₁.h + H₂.h)) x + ≡⟨ cong ([ H₁.a , [ H₂.a , H₃.a ] ∘ splitAt H₂.h ] ∘ splitAt H₁.h) ([-,]-cong ([,]-∘ [ _↑ˡ H₂.h + H₃.h , H₁.h ↑ʳ_ ] ∘ splitAt H₁.h) (splitAt (H₁.h + H₂.h) x)) ⟩ + ([ H₁.a , [ H₂.a , H₃.a ] ∘ splitAt H₂.h ] ∘ splitAt H₁.h ∘ [ [ _↑ˡ H₂.h + H₃.h , (H₁.h ↑ʳ_) ∘ (_↑ˡ H₃.h) ] ∘ splitAt H₁.h , (H₁.h ↑ʳ_) ∘ (H₂.h ↑ʳ_) ] ∘ splitAt (H₁.h + H₂.h)) x ∎ + + ≗j : (e : Fin (H₁.h + H₂.h + H₃.h)) + (i : Fin (ℕ.suc ([ [ H₁.a , H₂.a ] ∘ splitAt H₁.h , H₃.a ] (splitAt (H₁.h + H₂.h) e)))) + → Inverse.to (+-assoc-↔ X Y Z) (j+j (together H₁ H₂) H₃ e i) + ≡ j+j H₁ (together H₂ H₃) (Inverse.to ↔h e) (cast (cong ℕ.suc (≗a e)) i) + ≗j e i with splitAt (H₁.h + H₂.h) e + ≗j e i | inj₁ e₁₂ with splitAt H₁.h e₁₂ + ≗j e i | inj₁ e₁₂ | inj₁ e₁ + rewrite splitAt-↑ˡ H₁.h e₁ (H₂.h + H₃.h) + rewrite splitAt-↑ˡ (X + Y) (H₁.j e₁ i ↑ˡ Y) Z + rewrite splitAt-↑ˡ X (H₁.j e₁ i) Y = cong ((_↑ˡ Y + Z) ∘ H₁.j e₁) (sym (cast-is-id refl i)) + ≗j e i | inj₁ e₁₂ | inj₂ e₂ + rewrite splitAt-↑ʳ H₁.h (H₂.h + H₃.h) (e₂ ↑ˡ H₃.h) + rewrite splitAt-↑ˡ H₂.h e₂ H₃.h + rewrite splitAt-↑ˡ (X + Y) (X ↑ʳ H₂.j e₂ i) Z + rewrite splitAt-↑ʳ X Y (H₂.j e₂ i) = cong ((X ↑ʳ_) ∘ (_↑ˡ Z) ∘ H₂.j e₂) (sym (cast-is-id refl i)) + ≗j e i | inj₂ e₃ + rewrite splitAt-↑ʳ H₁.h (H₂.h + H₃.h) (H₂.h ↑ʳ e₃) + rewrite splitAt-↑ʳ H₂.h H₃.h e₃ + rewrite splitAt-↑ʳ (X + Y) Z (H₃.j e₃ i) = cong ((X ↑ʳ_) ∘ (Y ↑ʳ_) ∘ H₃.j e₃) (sym (cast-is-id refl i)) + +n+0↔n : ∀ n → Fin (n + 0) ↔ Fin n +n+0↔n n = record + { to = to + ; from = from + ; to-cong = λ { refl → refl } + ; from-cong = λ { refl → refl } + ; inverse = (λ { refl → to∘from _ }) , λ { refl → from∘to _ } + } + where + to : Fin (n + 0) → Fin n + to x with inj₁ x₁ ← splitAt n x = x₁ + from : Fin n → Fin (n + 0) + from x = x ↑ˡ 0 + from∘to : (x : Fin (n + 0)) → from (to x) ≡ x + from∘to x with inj₁ x₁ ← splitAt n x in eq = splitAt⁻¹-↑ˡ eq + to∘from : (x : Fin n) → to (from x) ≡ x + to∘from x rewrite splitAt-↑ˡ n x 0 = refl + +unitaryʳ : Hypergraph-same (map-nodes ([ id , (λ ()) ] ∘ splitAt n) (together H discrete)) H +unitaryʳ {n} {H} = record + { ↔h = h+0↔h + ; ≗a = ≗a + ; ≗j = ≗j + } + where + module H = Hypergraph H + module H+0 = Hypergraph (together {n} {0} H discrete) + h+0↔h : Fin H+0.h ↔ Fin H.h + h+0↔h = n+0↔n H.h + ≗a : (e : Fin (H.h + 0)) → [ H.a , (λ ()) ] (splitAt H.h e) ≡ H.a (Inverse.to h+0↔h e) + ≗a e with inj₁ e₁ ← splitAt H.h e in eq = refl + ≗j : (e : Fin (H.h + 0)) + (i : Fin (ℕ.suc ([ H.a , (λ ()) ] (splitAt H.h e)))) + → [ (λ x → x) , (λ ()) ] (splitAt n (j+j H discrete e i)) + ≡ H.j (Inverse.to h+0↔h e) (cast (cong ℕ.suc (≗a e)) i) + ≗j e i = ≗j-aux (splitAt H.h e) refl (j+j H discrete e) refl (≗a e) i + where + ≗j-aux + : (w : Fin H.h ⊎ Fin 0) + → (eq₁ : splitAt H.h e ≡ w) + → (w₁ : Fin (ℕ.suc ([ H.a , (λ ()) ] w)) → Fin (n + 0)) + → j+j H discrete e ≡ subst (λ hole → Fin (ℕ.suc ([ H.a , (λ ()) ] hole)) → Fin (n + 0)) (sym eq₁) w₁ + → (w₂ : [ H.a , (λ ()) ] w ≡ H.a (Inverse.to h+0↔h e)) + (i : Fin (ℕ.suc ([ H.a , (λ ()) ] w))) + → [ (λ x → x) , (λ ()) ] (splitAt n (w₁ i)) + ≡ H.j (Inverse.to h+0↔h e) (cast (cong ℕ.suc w₂) i) + ≗j-aux (inj₁ e₁) eq w₁ eq₁ w₂ i + with (inj₁ x) ← splitAt n (w₁ i) in eq₂ + rewrite eq = trans + (↑ˡ-injective 0 x (H.j e₁ i) (trans (splitAt⁻¹-↑ˡ eq₂) (sym (cong-app eq₁ i)))) + (cong (H.j e₁) (sym (cast-is-id refl i))) + ++-comm-↔ : ∀ (n m : ℕ) → Fin (n + m) ↔ Fin (m + n) ++-comm-↔ n m = record + { to = join m n ∘ swap ∘ splitAt n + ; from = join n m ∘ swap ∘ splitAt m + ; to-cong = λ { refl → refl } + ; from-cong = λ { refl → refl } + ; inverse = (λ { refl → to∘from _ }) , λ { refl → from∘to _ } + } + where + open ≡-Reasoning + to∘from : join m n ∘ swap ∘ splitAt n ∘ join n m ∘ swap ∘ splitAt m ≗ id + to∘from x = begin + (join m n ∘ swap ∘ splitAt n ∘ join n m ∘ swap ∘ splitAt m) x ≡⟨ (cong (join m n ∘ swap) ∘ splitAt-join n m ∘ swap ∘ splitAt m) x ⟩ + (join m n ∘ swap ∘ swap ∘ splitAt m) x ≡⟨ (cong (join m n) ∘ swap-involutive ∘ splitAt m) x ⟩ + (join m n ∘ splitAt m) x ≡⟨ join-splitAt m n x ⟩ + x ∎ + from∘to : join n m ∘ swap ∘ splitAt m ∘ join m n ∘ swap ∘ splitAt n ≗ id + from∘to x = begin + (join n m ∘ swap ∘ splitAt m ∘ join m n ∘ swap ∘ splitAt n) x ≡⟨ (cong (join n m ∘ swap) ∘ splitAt-join m n ∘ swap ∘ splitAt n) x ⟩ + (join n m ∘ swap ∘ swap ∘ splitAt n) x ≡⟨ (cong (join n m) ∘ swap-involutive ∘ splitAt n) x ⟩ + (join n m ∘ splitAt n) x ≡⟨ join-splitAt n m x ⟩ + x ∎ + +[,]∘swap : {A B C : Set} {f : A → C} {g : B → C} → [ f , g ] ∘ swap ≗ [ g , f ] +[,]∘swap (inj₁ x) = refl +[,]∘swap (inj₂ y) = refl + +braiding + : {n m : ℕ} + {H₁ : Hypergraph n} + {H₂ : Hypergraph m} + → Hypergraph-same (map-nodes ([ m ↑ʳ_ , _↑ˡ n ] ∘ splitAt n) (together H₁ H₂)) (together H₂ H₁) +braiding {n} {m} {H₁} {H₂} = record + { ↔h = +-comm-↔ H₁.h H₂.h + ; ≗a = ≗a + ; ≗j = ≗j + } + where + open ≡-Reasoning + module H₁ = Hypergraph H₁ + module H₂ = Hypergraph H₂ + ≗a : (e : Fin (H₁.h + H₂.h)) + → [ H₁.a , H₂.a ] (splitAt H₁.h e) + ≡ [ H₂.a , H₁.a ] (splitAt H₂.h (join H₂.h H₁.h (swap (splitAt H₁.h e)))) + ≗a e = begin + [ H₁.a , H₂.a ] (splitAt H₁.h e) ≡⟨ [,]∘swap (splitAt H₁.h e) ⟨ + [ H₂.a , H₁.a ] (swap (splitAt H₁.h e)) ≡⟨ cong [ H₂.a , H₁.a ] (splitAt-join H₂.h H₁.h (swap (splitAt H₁.h e))) ⟨ + [ H₂.a , H₁.a ] (splitAt H₂.h (join H₂.h H₁.h (swap (splitAt H₁.h e)))) ∎ + ≗j : (e : Fin (Hypergraph.h (map-nodes ([ m ↑ʳ_ , _↑ˡ n ] ∘ splitAt n) (together H₁ H₂)))) + (i : Fin (Hypergraph.arity (map-nodes ([ m ↑ʳ_ , _↑ˡ n ] ∘ splitAt n) (together H₁ H₂)) e)) + → Hypergraph.j (map-nodes ([ _↑ʳ_ m , _↑ˡ n ] ∘ splitAt n) (together H₁ H₂)) e i + ≡ Hypergraph.j (together H₂ H₁) (Inverse.to (+-comm-↔ H₁.h H₂.h) e) (cast (cong ℕ.suc (≗a e)) i) + ≗j e i with splitAt H₁.h e + ≗j e i | inj₁ e₁ + rewrite splitAt-↑ˡ n (H₁.j e₁ i) m + rewrite splitAt-↑ʳ H₂.h H₁.h e₁ = cong ((m ↑ʳ_) ∘ H₁.j e₁) (sym (cast-is-id refl i)) + ≗j e i | inj₂ e₂ + rewrite splitAt-↑ʳ n m (H₂.j e₂ i) + rewrite splitAt-↑ˡ H₂.h e₂ H₁.h = cong ((_↑ˡ n) ∘ H₂.j e₂) (sym (cast-is-id refl i)) + +opaque + unfolding η ε + + associativity′ + : {n m o : ℕ} + → {x : ∣ (Hypergraphₛ n ⊗₀ Hypergraphₛ m) ⊗₀ Hypergraphₛ o ∣} + → Hypergraph-same + (map-nodes (Inverse.to (+-assoc-↔ n m o)) (η {n + m} {o} ⟨$⟩ ((η {n} {m} ⊗₁ (Id _)) ⟨$⟩ x))) + (η {n} {m + o} ⟨$⟩ ((Id _ ⊗₁ η {m} {o}) ⟨$⟩ (Setoids-×.associator.from ⟨$⟩ x))) + associativity′ {n} {m} {o} {(x , y) , z} = associativity x y z + + unitaryˡ′ + : {X : ∣ Setoids-×.unit ⊗₀ Hypergraphₛ n ∣} + → Hypergraph-same (η {0} {n} ⟨$⟩ ((ε ⊗₁ Id _) ⟨$⟩ X)) (Setoids-×.unitorˡ.from ⟨$⟩ X) + unitaryˡ′ = Hypergraph-same-refl + + unitaryʳ′ + : {X : ∣ Hypergraphₛ n ⊗₀ Setoids-×.unit ∣} + → Hypergraph-same (map-nodes ([ id , (λ ()) ] ∘ splitAt n) (η {n} {0} ⟨$⟩ ((Id _ ⊗₁ ε) ⟨$⟩ X))) (Setoids-×.unitorʳ.from ⟨$⟩ X) + unitaryʳ′ = unitaryʳ + + braiding-compat + : {n m : ℕ} + → {X : ∣ Hypergraphₛ n ⊗₀ Hypergraphₛ m ∣} + → Hypergraph-same + (map-nodes ([ m ↑ʳ_ , _↑ˡ n ] ∘ splitAt n) (η {n} {m} ⟨$⟩ X)) + (η {m} {n} ⟨$⟩ (Setoids-×.braiding.⇒.η (Hypergraphₛ n , Hypergraphₛ m) ⟨$⟩ X)) + braiding-compat {n} {m} {H₁ , H₂} = braiding {n} {m} {H₁} {H₂} + +hypergraph : SymmetricMonoidalFunctor Nat-smc Setoids-× +hypergraph = record + { F = F + ; isBraidedMonoidal = record + { isMonoidal = record + { ε = ε + ; ⊗-homo = ⊗-homomorphism + ; associativity = associativity′ + ; unitaryˡ = unitaryˡ′ + ; unitaryʳ = unitaryʳ′ + } + ; braiding-compat = braiding-compat + } + } + +module F = SymmetricMonoidalFunctor hypergraph + +and-gate : Func ⊤ₛ (F.₀ 3) +and-gate = Const ⊤ₛ (Hypergraphₛ 3) and-graph + where + and-graph : Hypergraph 3 + and-graph = record + { h = 1 + ; a = λ { 0F → 2 } + ; j = λ { 0F → id } + } + where + edge-0-nodes : Fin 3 → Fin 3 + edge-0-nodes 0F = # 0 + edge-0-nodes 1F = # 1 + edge-0-nodes 2F = # 2 diff --git a/DecorationFunctor/Hypergraph/Labeled.agda b/DecorationFunctor/Hypergraph/Labeled.agda new file mode 100644 index 0000000..31402b1 --- /dev/null +++ b/DecorationFunctor/Hypergraph/Labeled.agda @@ -0,0 +1,689 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level) + +module DecorationFunctor.Hypergraph.Labeled {c ℓ : Level} where + +import Categories.Morphism as Morphism + +open import Categories.Category.BinaryProducts using (module BinaryProducts) +open import Categories.Category.Cartesian using (Cartesian) +open import Categories.Category.Core using (Category) +open import Categories.Category.Instance.Nat using (Nat) +open import Categories.Category.Instance.Setoids using (Setoids) +open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian) +open import Categories.Category.Product using (_⁂_) +open import Categories.Functor using () renaming (_∘F_ to _∘′_) +open import Categories.Functor.Core using (Functor) +open import Categories.Functor.Monoidal.Symmetric using (module Lax) +open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) +open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory) +open import Category.Instance.Nat.FinitelyCocomplete using (Nat-FinitelyCocomplete) +open import Category.Instance.Setoids.SymmetricMonoidal {c} {ℓ} using (Setoids-×; ×-symmetric′) +open import Data.Fin using (#_; Fin; splitAt; join; zero; suc; _↑ˡ_; _↑ʳ_; cast) +open import Data.Fin.Patterns using (0F; 1F; 2F) +open import Data.Fin.Properties + using + ( splitAt-join ; join-splitAt + ; cast-is-id ; cast-trans ; subst-is-cast + ; splitAt-↑ˡ ; splitAt-↑ʳ + ; splitAt⁻¹-↑ˡ ; ↑ˡ-injective + ) +open import Data.Nat using (ℕ; _+_) +open import Data.Product.Base using (_,_; Σ) +open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_) +open import Data.Setoid.Unit {c} {ℓ} using (⊤ₛ) +open import Data.Sum.Base using (_⊎_; map; inj₁; inj₂; swap; map₂) renaming ([_,_]′ to [_,_]) +open import Data.Sum.Properties using (map-map; [,]-map; [,]-∘; [-,]-cong; [,-]-cong; [,]-cong; map-cong; swap-involutive) +open import Data.Unit.Properties using () renaming (≡-setoid to ⊤-setoid) +open import Function using (_∘_; id; const; Func; Inverse; _↔_; mk↔; _⟶ₛ_) +open import Function.Construct.Composition using (_↔-∘_) +open import Function.Construct.Constant using () renaming (function to Const) +open import Function.Construct.Identity using (↔-id) +open import Function.Construct.Symmetry using (↔-sym) +open import Relation.Binary using (Setoid) +open import Relation.Binary.PropositionalEquality using (_≗_; _≡_; erefl; refl; sym; trans; cong; cong₂; subst; cong-app) +open import Relation.Binary.PropositionalEquality.Properties using (isEquivalence; module ≡-Reasoning; dcong; dcong₂; subst-∘; subst-subst; sym-cong; subst-subst-sym; trans-cong; cong-∘; trans-reflʳ) +open import Relation.Nullary.Negation.Core using (¬_) + +open Cartesian (Setoids-Cartesian {c} {ℓ}) using (products) +open FinitelyCocompleteCategory Nat-FinitelyCocomplete + using (-+-) + renaming (symmetricMonoidalCategory to Nat-smc; +-assoc to Nat-+-assoc) +open import Category.Monoidal.Instance.Nat using (Nat,+,0) +open Morphism (Setoids c ℓ) using (_≅_) +open Lax using (SymmetricMonoidalFunctor) + +open BinaryProducts products using (-×-) + +open import Data.Circuit.Gate using (Gate; cast-gate; cast-gate-trans; cast-gate-is-id; subst-is-cast-gate) + +record Hypergraph (v : ℕ) : Set c where + + field + h : ℕ + a : Fin h → ℕ + j : (e : Fin h) → Fin (a e) → Fin v + l : (e : Fin h) → Gate (a e) + +record Hypergraph-same {n : ℕ} (H H′ : Hypergraph n) : Set ℓ where + + open Hypergraph H public + open Hypergraph H′ renaming (h to h′; a to a′; j to j′; l to l′) public + + field + ↔h : Fin h ↔ Fin h′ + + open Inverse ↔h public + + field + ≗a : a ≗ a′ ∘ to + ≗j : (e : Fin h) + (i : Fin (a e)) + → j e i + ≡ j′ (to e) (cast (≗a e) i) + ≗l : (e : Fin h) + → l e + ≡ cast-gate (sym (≗a e)) (l′ (to e)) + +private + + variable + n n′ m m′ o : ℕ + H H′ H″ H₁ H₁′ : Hypergraph n + H₂ H₂′ : Hypergraph m + H₃ : Hypergraph o + +Hypergraph-same-refl : Hypergraph-same H H +Hypergraph-same-refl {_} {H} = record + { ↔h = ↔-id (Fin h) + ; ≗a = cong a ∘ erefl + ; ≗j = λ e i → cong (j e) (sym (cast-is-id refl i)) + ; ≗l = λ { e → sym (cast-gate-is-id refl (l e)) } + } + where + open Hypergraph H + +sym-sym : {A : Set} {x y : A} (p : x ≡ y) → sym (sym p) ≡ p +sym-sym refl = refl + +Hypergraph-same-sym : Hypergraph-same H H′ → Hypergraph-same H′ H +Hypergraph-same-sym {V} {H} {H′} ≡H = record + { ↔h = ↔-sym ↔h + ; ≗a = sym ∘ a∘from≗a′ + ; ≗j = ≗j′ + ; ≗l = ≗l′ + } + where + open Hypergraph-same ≡H + open ≡-Reasoning + a∘from≗a′ : a ∘ from ≗ a′ + a∘from≗a′ x = begin + (a ∘ from) x ≡⟨ (≗a ∘ from) x ⟩ + (a′ ∘ to ∘ from) x ≡⟨ (cong a′ ∘ inverseˡ ∘ erefl ∘ from) x ⟩ + a′ x ∎ + id≗to∘from : id ≗ to ∘ from + id≗to∘from e = sym (inverseˡ refl) + ≗arity′ : a′ ≗ a ∘ from + ≗arity′ e = sym (a∘from≗a′ e) + ≗arity- : a′ ≗ a′ ∘ to ∘ from + ≗arity- e = cong a′ (id≗to∘from e) + + ≗j′ : (e : Fin h′) (i : Fin (a′ e)) → j′ e i ≡ j (from e) (cast (≗arity′ e) i) + ≗j′ e i = begin + j′ e i ≡⟨ dcong₂ j′ (id≗to∘from e) (subst-∘ (id≗to∘from e)) ⟩ + j′ (to (from e)) (subst Fin (cong a′ (id≗to∘from e)) i) ≡⟨ cong (j′ (to (from e))) (subst-is-cast (cong a′ (id≗to∘from e)) i) ⟩ + j′ (to (from e)) (cast (cong a′ (id≗to∘from e)) i) ≡⟨⟩ + j′ (to (from e)) (cast (trans (≗arity′ e) (≗a (from e))) i) ≡⟨ cong (j′ (to (from e))) (cast-trans (≗arity′ e) (≗a (from e)) i) ⟨ + j′ (to (from e)) (cast (≗a (from e)) (cast (≗arity′ e) i)) ≡⟨ ≗j (from e) (cast (≗arity′ e) i) ⟨ + j (from e) (cast (≗arity′ e) i) ∎ + + ≗l′ : (e : Fin h′) → l′ e ≡ cast-gate (sym (sym (a∘from≗a′ e))) (l (from e)) + ≗l′ e = begin + l′ e ≡⟨ dcong l′ (sym (id≗to∘from e)) ⟨ + subst (Gate ∘ a′) (sym (id≗to∘from e)) (l′ (to (from e))) ≡⟨ subst-∘ (sym (id≗to∘from e)) ⟩ + subst Gate (cong a′ (sym (id≗to∘from e))) (l′ (to (from e))) ≡⟨ subst-is-cast-gate (cong a′ (sym (id≗to∘from e))) (l′ (to (from e))) ⟩ + cast-gate _ (l′ (to (from e))) ≡⟨ cast-gate-trans _ (sym (sym (a∘from≗a′ e))) (l′ (to (from e))) ⟨ + cast-gate (sym (sym (a∘from≗a′ e))) (cast-gate _ (l′ (to (from e)))) ≡⟨ cong (cast-gate (sym (sym (a∘from≗a′ e)))) (≗l (from e)) ⟨ + cast-gate (sym (sym (a∘from≗a′ e))) (l (from e)) ∎ + +Hypergraph-same-trans : Hypergraph-same H H′ → Hypergraph-same H′ H″ → Hypergraph-same H H″ +Hypergraph-same-trans ≡H₁ ≡H₂ = record + { ↔h = ↔h ≡H₂ ↔-∘ ↔h ≡H₁ + ; ≗a = λ { x → trans (≗a ≡H₁ x) (≗a ≡H₂ (to (↔h ≡H₁) x)) } + ; ≗j = λ { e i → trans (≗j ≡H₁ e i) (≗j₂ e i) } + ; ≗l = λ { e → trans (≗l ≡H₁ e) (≗l₂ e) } + } + where + open Hypergraph-same + open Inverse + open ≡-Reasoning + ≗j₂ : (e : Fin (h ≡H₁)) + (i : Fin (a ≡H₁ e)) + → j ≡H₂ (to (↔h ≡H₁) e) (cast (≗a ≡H₁ e) i) + ≡ j′ ≡H₂ (to (↔h ≡H₂) (to (↔h ≡H₁) e)) (cast (trans (≗a ≡H₁ e) (≗a ≡H₂ (to (↔h ≡H₁) e))) i) + ≗j₂ e i = begin + j ≡H₂ (to (↔h ≡H₁) e) (cast (≗a ≡H₁ e) i) + ≡⟨ ≗j ≡H₂ (to (↔h ≡H₁) e) (cast (≗a ≡H₁ e) i) ⟩ + j′ ≡H₂ (to (↔h ≡H₂) (to (↔h ≡H₁) e)) (cast (≗a ≡H₂ (to (↔h ≡H₁) e)) (cast (≗a ≡H₁ e) i)) + ≡⟨ cong (j′ ≡H₂ (to (↔h ≡H₂) (to (↔h ≡H₁) e))) (cast-trans (≗a ≡H₁ e) (≗a ≡H₂ (to (↔h ≡H₁) e)) i) ⟩ + j′ ≡H₂ (to (↔h ≡H₂) (to (↔h ≡H₁) e)) (cast (trans (≗a ≡H₁ e) (≗a ≡H₂ (to (↔h ≡H₁) e))) i) ∎ + ≗l₂ : (e : Fin (h ≡H₁)) → cast-gate _ (l′ ≡H₁ (to ≡H₁ e)) ≡ cast-gate _ (l′ ≡H₂ (to ≡H₂ (to ≡H₁ e))) + ≗l₂ e = trans (cong (cast-gate _) (≗l ≡H₂ (to ≡H₁ e))) (cast-gate-trans _ (sym (≗a ≡H₁ e)) (l′ ≡H₂ (to ≡H₂ (to ≡H₁ e)))) + +Hypergraph-setoid : ℕ → Setoid c ℓ +Hypergraph-setoid p = record + { Carrier = Hypergraph p + ; _≈_ = Hypergraph-same + ; isEquivalence = record + { refl = Hypergraph-same-refl + ; sym = Hypergraph-same-sym + ; trans = Hypergraph-same-trans + } + } + +map-nodes : (Fin n → Fin m) → Hypergraph n → Hypergraph m +map-nodes f H = record + { h = h + ; a = a + ; j = λ e i → f (j e i) + ; l = l + } + where + open Hypergraph H + +Hypergraph-same-cong + : (f : Fin n → Fin m) + → Hypergraph-same H H′ + → Hypergraph-same (map-nodes f H) (map-nodes f H′) +Hypergraph-same-cong f ≡H = record + { ↔h = ↔h + ; ≗a = ≗a + ; ≗j = λ { e i → cong f (≗j e i) } + ; ≗l = ≗l + } + where + open Hypergraph-same ≡H + +Hypergraph-Func : (Fin n → Fin m) → Hypergraph-setoid n ⟶ₛ Hypergraph-setoid m +Hypergraph-Func f = record + { to = map-nodes f + ; cong = Hypergraph-same-cong f + } + +F-resp-≈ + : {f g : Fin n → Fin m} + → f ≗ g + → Hypergraph-same (map-nodes f H) (map-nodes g H) +F-resp-≈ {g = g} f≗g = record + { ↔h = ↔h + ; ≗a = ≗a + ; ≗j = λ { e i → trans (f≗g (j e i)) (cong g (≗j e i)) } + ; ≗l = ≗l + } + where + open Hypergraph-same Hypergraph-same-refl + +homomorphism + : (f : Fin n → Fin m) + → (g : Fin m → Fin o) + → Hypergraph-same (map-nodes (g ∘ f) H) (map-nodes g (map-nodes f H)) +homomorphism {n} {m} {o} {H} f g = record + { ↔h = ↔h + ; ≗a = ≗a + ; ≗j = λ e i → cong (g ∘ f) (≗j e i) + ; ≗l = ≗l + } + where + open Hypergraph-same Hypergraph-same-refl + +F : Functor Nat (Setoids c ℓ) +F = record + { F₀ = λ n → Hypergraph-setoid n + ; F₁ = Hypergraph-Func + ; identity = λ { {n} {H} → Hypergraph-same-refl {H = H} } + ; homomorphism = λ { {f = f} {g = g} → homomorphism f g } + ; F-resp-≈ = λ f≗g → F-resp-≈ f≗g + } + +-- monoidal structure + +discrete : {n : ℕ} → Hypergraph n +discrete = record + { h = 0 + ; a = λ () + ; j = λ () + ; l = λ () + } + +ε : ⊤ₛ ⟶ₛ Hypergraph-setoid 0 +ε = Const ⊤ₛ (Hypergraph-setoid 0) discrete + +module _ (H₁ : Hypergraph n) (H₂ : Hypergraph m) where + private + module H₁ = Hypergraph H₁ + module H₂ = Hypergraph H₂ + j+j : (e : Fin (H₁.h + H₂.h)) + → Fin ([ H₁.a , H₂.a ] (splitAt H₁.h e)) + → Fin (n + m) + j+j e i with splitAt H₁.h e + ... | inj₁ e₁ = H₁.j e₁ i ↑ˡ m + ... | inj₂ e₂ = n ↑ʳ H₂.j e₂ i + l+l : (e : Fin (H₁.h + H₂.h)) → Gate ([ H₁.a , H₂.a ] (splitAt H₁.h e)) + l+l e with splitAt H₁.h e + ... | inj₁ e₁ = H₁.l e₁ + ... | inj₂ e₂ = H₂.l e₂ + +together : Hypergraph n → Hypergraph m → Hypergraph (n + m) +together {n} {m} H₁ H₂ = record + { h = h H₁ + h H₂ + ; a = [ a H₁ , a H₂ ] ∘ splitAt (h H₁) + ; j = j+j H₁ H₂ + ; l = l+l H₁ H₂ + } + where + open Hypergraph + ++-resp-↔ + : {n n′ m m′ : ℕ} + → Fin n ↔ Fin n′ + → Fin m ↔ Fin m′ + → Fin (n + m) ↔ Fin (n′ + m′) ++-resp-↔ {n} {n′} {m} {m′} ↔n ↔m = record + { to = join n′ m′ ∘ map ↔n.to ↔m.to ∘ splitAt n + ; from = join n m ∘ map ↔n.from ↔m.from ∘ splitAt n′ + ; to-cong = cong (join n′ m′ ∘ map ↔n.to ↔m.to ∘ splitAt n) + ; from-cong = cong (join n m ∘ map ↔n.from ↔m.from ∘ splitAt n′) + ; inverse = (λ { refl → to∘from _ }) , λ { refl → from∘to _ } + } + where + module ↔n = Inverse ↔n + module ↔m = Inverse ↔m + open ≡-Reasoning + to∘from : join n′ m′ ∘ map ↔n.to ↔m.to ∘ splitAt n ∘ join n m ∘ map ↔n.from ↔m.from ∘ splitAt n′ ≗ id + to∘from x = begin + (join n′ m′ ∘ map ↔n.to ↔m.to ∘ splitAt n ∘ join n m ∘ map ↔n.from ↔m.from ∘ splitAt n′) x + ≡⟨ cong + (join n′ m′ ∘ map ↔n.to ↔m.to) + (splitAt-join n m (map ↔n.from ↔m.from (splitAt n′ x))) ⟩ + (join n′ m′ ∘ map ↔n.to ↔m.to ∘ map ↔n.from ↔m.from ∘ splitAt n′) x + ≡⟨ cong (join n′ m′) (map-map (splitAt n′ x)) ⟩ + (join n′ m′ ∘ map (↔n.to ∘ ↔n.from) (↔m.to ∘ ↔m.from) ∘ splitAt n′) x + ≡⟨ cong + (join n′ m′) + (map-cong + (λ _ → ↔n.inverseˡ refl) + (λ _ → ↔m.inverseˡ refl) + (splitAt n′ x)) ⟩ + (join n′ m′ ∘ map id id ∘ splitAt n′) x ≡⟨ [,]-map (splitAt n′ x) ⟩ + (join n′ m′ ∘ splitAt n′) x ≡⟨ join-splitAt n′ m′ x ⟩ + x ∎ + from∘to : join n m ∘ map ↔n.from ↔m.from ∘ splitAt n′ ∘ join n′ m′ ∘ map ↔n.to ↔m.to ∘ splitAt n ≗ id + from∘to x = begin + (join n m ∘ map ↔n.from ↔m.from ∘ splitAt n′ ∘ join n′ m′ ∘ map ↔n.to ↔m.to ∘ splitAt n) x + ≡⟨ cong + (join n m ∘ map ↔n.from ↔m.from) + (splitAt-join n′ m′ (map ↔n.to ↔m.to (splitAt n x))) ⟩ + (join n m ∘ map ↔n.from ↔m.from ∘ map ↔n.to ↔m.to ∘ splitAt n) x + ≡⟨ cong (join n m) (map-map (splitAt n x)) ⟩ + (join n m ∘ map (↔n.from ∘ ↔n.to) (↔m.from ∘ ↔m.to) ∘ splitAt n) x + ≡⟨ cong + (join n m) + (map-cong + (λ _ → ↔n.inverseʳ refl) + (λ _ → ↔m.inverseʳ refl) + (splitAt n x)) ⟩ + (join n m ∘ map id id ∘ splitAt n) x ≡⟨ [,]-map (splitAt n x) ⟩ + (join n m ∘ splitAt n) x ≡⟨ join-splitAt n m x ⟩ + x ∎ + +together-resp-same + : Hypergraph-same H₁ H₁′ + → Hypergraph-same H₂ H₂′ + → Hypergraph-same (together H₁ H₂) (together H₁′ H₂′) +together-resp-same {n} {H₁} {H₁′} {m} {H₂} {H₂′} ≡H₁ ≡H₂ = record + { ↔h = +-resp-↔ ≡H₁.↔h ≡H₂.↔h + ; ≗a = ≗a + ; ≗j = ≗j + ; ≗l = ≗l + } + where + module ≡H₁ = Hypergraph-same ≡H₁ + module ≡H₂ = Hypergraph-same ≡H₂ + module H₁+H₂ = Hypergraph (together H₁ H₂) + module H₁+H₂′ = Hypergraph (together H₁′ H₂′) + open ≡-Reasoning + open Inverse + open Hypergraph + ≗a : [ ≡H₁.a , ≡H₂.a ] ∘ splitAt ≡H₁.h + ≗ [ ≡H₁.a′ , ≡H₂.a′ ] ∘ splitAt ≡H₁.h′ + ∘ join ≡H₁.h′ ≡H₂.h′ ∘ map ≡H₁.to ≡H₂.to ∘ splitAt ≡H₁.h + ≗a e = begin + [ ≡H₁.a , ≡H₂.a ] (splitAt ≡H₁.h e) ≡⟨ [,]-cong ≡H₁.≗a ≡H₂.≗a (splitAt ≡H₁.h e) ⟩ + ([ ≡H₁.a′ ∘ ≡H₁.to , ≡H₂.a′ ∘ ≡H₂.to ] ∘ splitAt ≡H₁.h) e ≡⟨ [,]-map (splitAt ≡H₁.h e) ⟨ + ([ ≡H₁.a′ , ≡H₂.a′ ] ∘ map ≡H₁.to ≡H₂.to ∘ splitAt ≡H₁.h) e ≡⟨ (cong [ ≡H₁.a′ , ≡H₂.a′ ] ∘ splitAt-join ≡H₁.h′ ≡H₂.h′ ∘ map ≡H₁.to ≡H₂.to ∘ splitAt ≡H₁.h) e ⟨ + ([ ≡H₁.a′ , ≡H₂.a′ ] ∘ splitAt ≡H₁.h′ ∘ join ≡H₁.h′ ≡H₂.h′ ∘ map ≡H₁.to ≡H₂.to ∘ splitAt ≡H₁.h) e ∎ + ≗j : (e : Fin H₁+H₂.h) + (i : Fin (H₁+H₂.a e)) + → H₁+H₂.j e i + ≡ H₁+H₂′.j (to (+-resp-↔ ≡H₁.↔h ≡H₂.↔h) e) (cast (≗a e) i) + ≗j e i with splitAt ≡H₁.h e + ... | inj₁ e₁ rewrite splitAt-↑ˡ ≡H₁.h′ (≡H₁.to e₁) ≡H₂.h′ = cong (_↑ˡ m) (≡H₁.≗j e₁ i) + ... | inj₂ e₂ rewrite splitAt-↑ʳ ≡H₁.h′ ≡H₂.h′ (≡H₂.to e₂) = cong (n ↑ʳ_) (≡H₂.≗j e₂ i) + ≗l : (e : Fin H₁+H₂.h) → l+l H₁ H₂ e ≡ cast-gate (sym (≗a e)) (l+l H₁′ H₂′ (to (+-resp-↔ ≡H₁.↔h ≡H₂.↔h) e)) + ≗l e with splitAt ≡H₁.h e | .{≗a e} + ... | inj₁ e₁ rewrite splitAt-↑ˡ ≡H₁.h′ (≡H₁.to e₁) ≡H₂.h′ = ≡H₁.≗l e₁ + ... | inj₂ e₂ rewrite splitAt-↑ʳ ≡H₁.h′ ≡H₂.h′ (≡H₂.to e₂) = ≡H₂.≗l e₂ + +commute + : (f : Fin n → Fin n′) + → (g : Fin m → Fin m′) + → Hypergraph-same + (together (map-nodes f H₁) (map-nodes g H₂)) + (map-nodes ([ (_↑ˡ m′) ∘ f , (n′ ↑ʳ_) ∘ g ] ∘ splitAt n) (together H₁ H₂)) +commute {n} {n′} {m} {m′} {H₁} {H₂} f g = record + { ↔h = ≡H₁+H₂.↔h + ; ≗a = ≡H₁+H₂.≗a + ; ≗j = ≗j + ; ≗l = ≗l + } + where + module H₁ = Hypergraph H₁ + module H₂ = Hypergraph H₂ + module H₁+H₂ = Hypergraph (together H₁ H₂) + module ≡H₁+H₂ = Hypergraph-same {H = together H₁ H₂} Hypergraph-same-refl + open Hypergraph + open ≡-Reasoning + ≗j : (e : Fin (H₁.h + H₂.h)) + (i : Fin (([ H₁.a , H₂.a ] ∘ splitAt H₁.h) e)) + → j (together (map-nodes f H₁) (map-nodes g H₂)) e i + ≡ j (map-nodes ([ (_↑ˡ m′) ∘ f , (n′ ↑ʳ_) ∘ g ] ∘ splitAt n) (together H₁ H₂)) (≡H₁+H₂.to e) (cast refl i) + ≗j e i rewrite (cast-is-id refl i) with splitAt H₁.h e + ... | inj₁ e₁ rewrite splitAt-↑ˡ n (H₁.j e₁ i) m = refl + ... | inj₂ e₂ rewrite splitAt-↑ʳ n m (H₂.j e₂ i) = refl + ≗l : (e : Fin (H₁.h + H₂.h)) + → l+l (map-nodes f H₁) (map-nodes g H₂) e + ≡ cast-gate refl (l+l H₁ H₂ (≡H₁+H₂.to e)) + ≗l e rewrite cast-gate-is-id refl (l+l H₁ H₂ (≡H₁+H₂.to e)) with splitAt H₁.h e + ... | inj₁ e₁ = refl + ... | inj₂ e₁ = refl + +⊗-homomorphism : NaturalTransformation (-×- ∘′ (F ⁂ F)) (F ∘′ -+-) +⊗-homomorphism = record + { η = λ { (m , n) → η } + ; commute = λ { (f , g) {H₁ , H₂} → commute {H₁ = H₁} {H₂ = H₂} f g } + ; sym-commute = λ { (f , g) {H₁ , H₂} → Hypergraph-same-sym (commute {H₁ = H₁} {H₂ = H₂} f g) } + } + where + η : Hypergraph-setoid n ×ₛ Hypergraph-setoid m ⟶ₛ Hypergraph-setoid (n + m) + η = record + { to = λ { (H₁ , H₂) → together H₁ H₂ } + ; cong = λ { (≡H₁ , ≡H₂) → together-resp-same ≡H₁ ≡H₂ } + } + ++-assoc-↔ : ∀ (x y z : ℕ) → Fin (x + y + z) ↔ Fin (x + (y + z)) ++-assoc-↔ x y z = record + { to = to + ; from = from + ; to-cong = λ { refl → refl } + ; from-cong = λ { refl → refl } + ; inverse = (λ { refl → isoˡ _ }) , λ { refl → isoʳ _ } + } + where + module Nat = Morphism Nat + open Nat._≅_ (Nat-+-assoc {x} {y} {z}) + +associativity + : {X Y Z : ℕ} + → {H₁ : Hypergraph X} + → {H₂ : Hypergraph Y} + → {H₃ : Hypergraph Z} + → Hypergraph-same + (map-nodes (Inverse.to (+-assoc-↔ X Y Z)) (together (together H₁ H₂) H₃)) + (together H₁ (together H₂ H₃)) +associativity {X} {Y} {Z} {H₁} {H₂} {H₃} = record + { ↔h = ↔h + ; ≗a = ≗a + ; ≗j = ≗j + ; ≗l = ≗l + } + where + module H₁ = Hypergraph H₁ + module H₂ = Hypergraph H₂ + module H₃ = Hypergraph H₃ + open ≡-Reasoning + open Hypergraph + ↔h : Fin (H₁.h + H₂.h + H₃.h) ↔ Fin (H₁.h + (H₂.h + H₃.h)) + ↔h = +-assoc-↔ H₁.h H₂.h H₃.h + ≗a : (x : Fin (H₁.h + H₂.h + H₃.h)) + → [ [ H₁.a , H₂.a ] ∘ splitAt H₁.h , H₃.a ] (splitAt (H₁.h + H₂.h) x) + ≡ [ H₁.a , [ H₂.a , H₃.a ] ∘ splitAt H₂.h ] (splitAt H₁.h ([ [ _↑ˡ H₂.h + H₃.h , (H₁.h ↑ʳ_) ∘ (_↑ˡ H₃.h) ] ∘ splitAt H₁.h , (H₁.h ↑ʳ_) ∘ (H₂.h ↑ʳ_) ] (splitAt (H₁.h + H₂.h) x))) + ≗a x = begin + ([ [ H₁.a , H₂.a ] ∘ splitAt H₁.h , H₃.a ] ∘ splitAt (H₁.h + H₂.h)) x + ≡⟨⟩ + ([ [ H₁.a , [ H₂.a , H₃.a ] ∘ inj₁ ] ∘ splitAt H₁.h , H₃.a ] ∘ splitAt (H₁.h + H₂.h)) x + ≡⟨ [-,]-cong ([,-]-cong (cong [ H₂.a , H₃.a ] ∘ (λ i → splitAt-↑ˡ H₂.h i H₃.h)) ∘ splitAt H₁.h) (splitAt (H₁.h + H₂.h) x) ⟨ + ([ [ H₁.a , [ H₂.a , H₃.a ] ∘ splitAt H₂.h ∘ (_↑ˡ H₃.h) ] ∘ splitAt H₁.h , H₃.a ] ∘ splitAt (H₁.h + H₂.h)) x + ≡⟨ [-,]-cong ([,]-∘ [ H₁.a , [ H₂.a , H₃.a ] ∘ splitAt H₂.h ] ∘ splitAt H₁.h) (splitAt (H₁.h + H₂.h) x) ⟨ + ([ [ H₁.a , [ H₂.a , H₃.a ] ∘ splitAt H₂.h ] ∘ map₂ (_↑ˡ H₃.h) ∘ splitAt H₁.h , H₃.a ] ∘ splitAt (H₁.h + H₂.h)) x + ≡⟨⟩ + ([ [ H₁.a , [ H₂.a , H₃.a ] ∘ splitAt H₂.h ] ∘ map₂ (_↑ˡ H₃.h) ∘ splitAt H₁.h , [ H₂.a , H₃.a ] ∘ inj₂ ] ∘ splitAt (H₁.h + H₂.h)) x + ≡⟨ [,-]-cong (cong [ H₂.a , H₃.a ] ∘ splitAt-↑ʳ H₂.h H₃.h) (splitAt (H₁.h + H₂.h) x) ⟨ + ([ [ H₁.a , [ H₂.a , H₃.a ] ∘ splitAt H₂.h ] ∘ map₂ (_↑ˡ H₃.h) ∘ splitAt H₁.h , [ H₂.a , H₃.a ] ∘ splitAt H₂.h ∘ (H₂.h ↑ʳ_) ] ∘ splitAt (H₁.h + H₂.h)) x + ≡⟨⟩ + ([ [ H₁.a , [ H₂.a , H₃.a ] ∘ splitAt H₂.h ] ∘ map₂ (_↑ˡ H₃.h) ∘ splitAt H₁.h , [ H₁.a , [ H₂.a , H₃.a ] ∘ splitAt H₂.h ] ∘ inj₂ ∘ (H₂.h ↑ʳ_) ] ∘ splitAt (H₁.h + H₂.h)) x + ≡⟨ [,]-∘ [ H₁.a , [ H₂.a , H₃.a ] ∘ splitAt H₂.h ] (splitAt (H₁.h + H₂.h) x) ⟨ + ([ H₁.a , [ H₂.a , H₃.a ] ∘ splitAt H₂.h ] ∘ [ map₂ (_↑ˡ H₃.h) ∘ splitAt H₁.h , inj₂ ∘ (H₂.h ↑ʳ_) ] ∘ splitAt (H₁.h + H₂.h)) x + ≡⟨ cong [ H₁.a , [ H₂.a , H₃.a ] ∘ splitAt H₂.h ] ([,-]-cong (splitAt-↑ʳ H₁.h (H₂.h + H₃.h) ∘ (H₂.h ↑ʳ_)) (splitAt (H₁.h + H₂.h) x)) ⟨ + ([ H₁.a , [ H₂.a , H₃.a ] ∘ splitAt H₂.h ] ∘ [ map₂ (_↑ˡ H₃.h) ∘ splitAt H₁.h , splitAt H₁.h ∘ (H₁.h ↑ʳ_) ∘ (H₂.h ↑ʳ_) ] ∘ splitAt (H₁.h + H₂.h)) x + ≡⟨ cong [ H₁.a , [ H₂.a , H₃.a ] ∘ splitAt H₂.h ] ([-,]-cong (splitAt-join H₁.h (H₂.h + H₃.h) ∘ map₂ (_↑ˡ H₃.h) ∘ splitAt H₁.h) (splitAt (H₁.h + H₂.h) x)) ⟨ + ([ H₁.a , [ H₂.a , H₃.a ] ∘ splitAt H₂.h ] ∘ [ splitAt H₁.h ∘ join H₁.h (H₂.h + H₃.h) ∘ map₂ (_↑ˡ H₃.h) ∘ splitAt H₁.h , splitAt H₁.h ∘ (H₁.h ↑ʳ_) ∘ (H₂.h ↑ʳ_) ] ∘ splitAt (H₁.h + H₂.h)) x + ≡⟨ cong [ H₁.a , [ H₂.a , H₃.a ] ∘ splitAt H₂.h ] ([,]-∘ (splitAt H₁.h) (splitAt (H₁.h + H₂.h) x)) ⟨ + ([ H₁.a , [ H₂.a , H₃.a ] ∘ splitAt H₂.h ] ∘ splitAt H₁.h ∘ [ join H₁.h (H₂.h + H₃.h) ∘ map₂ (_↑ˡ H₃.h) ∘ splitAt H₁.h , (H₁.h ↑ʳ_) ∘ (H₂.h ↑ʳ_) ] ∘ splitAt (H₁.h + H₂.h)) x + ≡⟨⟩ + ([ H₁.a , [ H₂.a , H₃.a ] ∘ splitAt H₂.h ] ∘ splitAt H₁.h ∘ [ [ _↑ˡ H₂.h + H₃.h , H₁.h ↑ʳ_ ] ∘ [ inj₁ , inj₂ ∘ (_↑ˡ H₃.h) ] ∘ splitAt H₁.h , (H₁.h ↑ʳ_) ∘ (H₂.h ↑ʳ_) ] ∘ splitAt (H₁.h + H₂.h)) x + ≡⟨ cong ([ H₁.a , [ H₂.a , H₃.a ] ∘ splitAt H₂.h ] ∘ splitAt H₁.h) ([-,]-cong ([,]-∘ [ _↑ˡ H₂.h + H₃.h , H₁.h ↑ʳ_ ] ∘ splitAt H₁.h) (splitAt (H₁.h + H₂.h) x)) ⟩ + ([ H₁.a , [ H₂.a , H₃.a ] ∘ splitAt H₂.h ] ∘ splitAt H₁.h ∘ [ [ _↑ˡ H₂.h + H₃.h , (H₁.h ↑ʳ_) ∘ (_↑ˡ H₃.h) ] ∘ splitAt H₁.h , (H₁.h ↑ʳ_) ∘ (H₂.h ↑ʳ_) ] ∘ splitAt (H₁.h + H₂.h)) x ∎ + ≗j : (e : Fin (H₁.h + H₂.h + H₃.h)) + (i : Fin ([ [ H₁.a , H₂.a ] ∘ splitAt H₁.h , H₃.a ] (splitAt (H₁.h + H₂.h) e))) + → Inverse.to (+-assoc-↔ X Y Z) (j+j (together H₁ H₂) H₃ e i) + ≡ j+j H₁ (together H₂ H₃) (Inverse.to ↔h e) (cast (≗a e) i) + ≗j e i with splitAt (H₁.h + H₂.h) e + ≗j e i | inj₁ e₁₂ with splitAt H₁.h e₁₂ + ≗j e i | inj₁ e₁₂ | inj₁ e₁ + rewrite splitAt-↑ˡ H₁.h e₁ (H₂.h + H₃.h) + rewrite splitAt-↑ˡ (X + Y) (H₁.j e₁ i ↑ˡ Y) Z + rewrite splitAt-↑ˡ X (H₁.j e₁ i) Y = cong ((_↑ˡ Y + Z) ∘ H₁.j e₁) (sym (cast-is-id refl i)) + ≗j e i | inj₁ e₁₂ | inj₂ e₂ + rewrite splitAt-↑ʳ H₁.h (H₂.h + H₃.h) (e₂ ↑ˡ H₃.h) + rewrite splitAt-↑ˡ H₂.h e₂ H₃.h + rewrite splitAt-↑ˡ (X + Y) (X ↑ʳ H₂.j e₂ i) Z + rewrite splitAt-↑ʳ X Y (H₂.j e₂ i) = cong ((X ↑ʳ_) ∘ (_↑ˡ Z) ∘ H₂.j e₂) (sym (cast-is-id refl i)) + ≗j e i | inj₂ e₃ + rewrite splitAt-↑ʳ H₁.h (H₂.h + H₃.h) (H₂.h ↑ʳ e₃) + rewrite splitAt-↑ʳ H₂.h H₃.h e₃ + rewrite splitAt-↑ʳ (X + Y) Z (H₃.j e₃ i) = cong ((X ↑ʳ_) ∘ (Y ↑ʳ_) ∘ H₃.j e₃) (sym (cast-is-id refl i)) + ≗l : (e : Fin (H₁.h + H₂.h + H₃.h)) + → l (map-nodes (Inverse.to (+-assoc-↔ X Y Z)) (together (together H₁ H₂) H₃)) e + ≡ cast-gate (sym (≗a e)) (l (together H₁ (together H₂ H₃)) (Inverse.to ↔h e)) + ≗l e with splitAt (H₁.h + H₂.h) e + ≗l e | inj₁ e₁₂ with splitAt H₁.h e₁₂ + ≗l e | inj₁ e₁₂ | inj₁ e₁ + rewrite splitAt-↑ˡ H₁.h e₁ (H₂.h + H₃.h) = sym (cast-gate-is-id refl (H₁.l e₁)) + ≗l e | inj₁ e₁₂ | inj₂ e₂ + rewrite splitAt-↑ʳ H₁.h (H₂.h + H₃.h) (e₂ ↑ˡ H₃.h) + rewrite splitAt-↑ˡ H₂.h e₂ H₃.h = sym (cast-gate-is-id refl (H₂.l e₂)) + ≗l e | inj₂ e₃ + rewrite splitAt-↑ʳ H₁.h (H₂.h + H₃.h) (H₂.h ↑ʳ e₃) + rewrite splitAt-↑ʳ H₂.h H₃.h e₃ = sym (cast-gate-is-id refl (H₃.l e₃)) + +n+0↔n : ∀ n → Fin (n + 0) ↔ Fin n +n+0↔n n = record + { to = to + ; from = from + ; to-cong = λ { refl → refl } + ; from-cong = λ { refl → refl } + ; inverse = (λ { refl → to∘from _ }) , λ { refl → from∘to _ } + } + where + to : Fin (n + 0) → Fin n + to x with inj₁ x₁ ← splitAt n x = x₁ + from : Fin n → Fin (n + 0) + from x = x ↑ˡ 0 + from∘to : (x : Fin (n + 0)) → from (to x) ≡ x + from∘to x with inj₁ x₁ ← splitAt n x in eq = splitAt⁻¹-↑ˡ eq + to∘from : (x : Fin n) → to (from x) ≡ x + to∘from x rewrite splitAt-↑ˡ n x 0 = refl + +unitaryʳ : Hypergraph-same (map-nodes ([ id , (λ ()) ] ∘ splitAt n) (together H (discrete {0}))) H +unitaryʳ {n} {H} = record + { ↔h = h+0↔h + ; ≗a = ≗a + ; ≗j = ≗j + ; ≗l = ≗l + } + where + module H = Hypergraph H + module H+0 = Hypergraph (together H (discrete {0})) + h+0↔h : Fin H+0.h ↔ Fin H.h + h+0↔h = n+0↔n H.h + ≗a : (e : Fin (H.h + 0)) → [ H.a , (λ ()) ] (splitAt H.h e) ≡ H.a (Inverse.to h+0↔h e) + ≗a e with inj₁ e₁ ← splitAt H.h e in eq = refl + ≗j : (e : Fin (H.h + 0)) + (i : Fin ([ H.a , (λ ()) ] (splitAt H.h e))) + → [ (λ x → x) , (λ ()) ] (splitAt n (j+j H discrete e i)) + ≡ H.j (Inverse.to h+0↔h e) (cast (≗a e) i) + ≗j e i = ≗j-aux (splitAt H.h e) refl (j+j H discrete e) refl (≗a e) i + where + ≗j-aux + : (w : Fin H.h ⊎ Fin 0) + → (eq₁ : splitAt H.h e ≡ w) + → (w₁ : Fin ([ H.a , (λ ()) ] w) → Fin (n + 0)) + → j+j H discrete e ≡ subst (λ hole → Fin ([ H.a , (λ ()) ] hole) → Fin (n + 0)) (sym eq₁) w₁ + → (w₂ : [ H.a , (λ ()) ] w ≡ H.a (Inverse.to h+0↔h e)) + (i : Fin ([ H.a , (λ ()) ] w)) + → [ (λ x → x) , (λ ()) ] (splitAt n (w₁ i)) + ≡ H.j (Inverse.to h+0↔h e) (cast w₂ i) + ≗j-aux (inj₁ e₁) eq w₁ eq₁ w₂ i + with (inj₁ x) ← splitAt n (w₁ i) in eq₂ + rewrite eq = trans + (↑ˡ-injective 0 x (H.j e₁ i) (trans (splitAt⁻¹-↑ˡ eq₂) (sym (cong-app eq₁ i)))) + (cong (H.j e₁) (sym (cast-is-id refl i))) + ≗l : (e : Fin (H.h + 0)) + → l+l H discrete e + ≡ cast-gate (sym (≗a e)) (H.l (Inverse.to h+0↔h e)) + ≗l e with splitAt H.h e | {(≗a e)} + ... | inj₁ e₁ = sym (cast-gate-is-id refl (H.l e₁)) + ++-comm-↔ : ∀ (n m : ℕ) → Fin (n + m) ↔ Fin (m + n) ++-comm-↔ n m = record + { to = join m n ∘ swap ∘ splitAt n + ; from = join n m ∘ swap ∘ splitAt m + ; to-cong = λ { refl → refl } + ; from-cong = λ { refl → refl } + ; inverse = (λ { refl → to∘from _ }) , λ { refl → from∘to _ } + } + where + open ≡-Reasoning + to∘from : join m n ∘ swap ∘ splitAt n ∘ join n m ∘ swap ∘ splitAt m ≗ id + to∘from x = begin + (join m n ∘ swap ∘ splitAt n ∘ join n m ∘ swap ∘ splitAt m) x ≡⟨ (cong (join m n ∘ swap) ∘ splitAt-join n m ∘ swap ∘ splitAt m) x ⟩ + (join m n ∘ swap ∘ swap ∘ splitAt m) x ≡⟨ (cong (join m n) ∘ swap-involutive ∘ splitAt m) x ⟩ + (join m n ∘ splitAt m) x ≡⟨ join-splitAt m n x ⟩ + x ∎ + from∘to : join n m ∘ swap ∘ splitAt m ∘ join m n ∘ swap ∘ splitAt n ≗ id + from∘to x = begin + (join n m ∘ swap ∘ splitAt m ∘ join m n ∘ swap ∘ splitAt n) x ≡⟨ (cong (join n m ∘ swap) ∘ splitAt-join m n ∘ swap ∘ splitAt n) x ⟩ + (join n m ∘ swap ∘ swap ∘ splitAt n) x ≡⟨ (cong (join n m) ∘ swap-involutive ∘ splitAt n) x ⟩ + (join n m ∘ splitAt n) x ≡⟨ join-splitAt n m x ⟩ + x ∎ + +[,]∘swap : {A B C : Set} {f : A → C} {g : B → C} → [ f , g ] ∘ swap ≗ [ g , f ] +[,]∘swap (inj₁ x) = refl +[,]∘swap (inj₂ y) = refl + +braiding + : {n m : ℕ} + {H₁ : Hypergraph n} + {H₂ : Hypergraph m} + → Hypergraph-same (map-nodes ([ m ↑ʳ_ , _↑ˡ n ] ∘ splitAt n) (together H₁ H₂)) (together H₂ H₁) +braiding {n} {m} {H₁} {H₂} = record + { ↔h = +-comm-↔ H₁.h H₂.h + ; ≗a = ≗a + ; ≗j = ≗j + ; ≗l = ≗l + } + where + open ≡-Reasoning + module H₁ = Hypergraph H₁ + module H₂ = Hypergraph H₂ + ≗a : (e : Fin (H₁.h + H₂.h)) + → [ H₁.a , H₂.a ] (splitAt H₁.h e) + ≡ [ H₂.a , H₁.a ] (splitAt H₂.h (join H₂.h H₁.h (swap (splitAt H₁.h e)))) + ≗a e = begin + [ H₁.a , H₂.a ] (splitAt H₁.h e) ≡⟨ [,]∘swap (splitAt H₁.h e) ⟨ + [ H₂.a , H₁.a ] (swap (splitAt H₁.h e)) ≡⟨ cong [ H₂.a , H₁.a ] (splitAt-join H₂.h H₁.h (swap (splitAt H₁.h e))) ⟨ + [ H₂.a , H₁.a ] (splitAt H₂.h (join H₂.h H₁.h (swap (splitAt H₁.h e)))) ∎ + ≗j : (e : Fin (Hypergraph.h (map-nodes ([ m ↑ʳ_ , _↑ˡ n ] ∘ splitAt n) (together H₁ H₂)))) + (i : Fin (Hypergraph.a (map-nodes ([ m ↑ʳ_ , _↑ˡ n ] ∘ splitAt n) (together H₁ H₂)) e)) + → Hypergraph.j (map-nodes ([ _↑ʳ_ m , _↑ˡ n ] ∘ splitAt n) (together H₁ H₂)) e i + ≡ Hypergraph.j (together H₂ H₁) (Inverse.to (+-comm-↔ H₁.h H₂.h) e) (cast (≗a e) i) + ≗j e i with splitAt H₁.h e + ≗j e i | inj₁ e₁ + rewrite splitAt-↑ˡ n (H₁.j e₁ i) m + rewrite splitAt-↑ʳ H₂.h H₁.h e₁ = cong ((m ↑ʳ_) ∘ H₁.j e₁) (sym (cast-is-id refl i)) + ≗j e i | inj₂ e₂ + rewrite splitAt-↑ʳ n m (H₂.j e₂ i) + rewrite splitAt-↑ˡ H₂.h e₂ H₁.h = cong ((_↑ˡ n) ∘ H₂.j e₂) (sym (cast-is-id refl i)) + ≗l : (e : Fin (H₁.h + H₂.h)) + → l+l H₁ H₂ e + ≡ cast-gate (sym (≗a e)) (l+l H₂ H₁ (Inverse.to (+-comm-↔ H₁.h H₂.h) e)) + ≗l e with splitAt H₁.h e | .{≗a e} + ≗l e | inj₁ e₁ rewrite splitAt-↑ʳ H₂.h H₁.h e₁ = sym (cast-gate-is-id refl (H₁.l e₁)) + ≗l e | inj₂ e₂ rewrite splitAt-↑ˡ H₂.h e₂ H₁.h = sym (cast-gate-is-id refl (H₂.l e₂)) + +opaque + unfolding ×-symmetric′ + Circ : SymmetricMonoidalFunctor Nat,+,0 Setoids-× + Circ = record + { F = F + ; isBraidedMonoidal = record + { isMonoidal = record + { ε = ε + ; ⊗-homo = ntHelper record + { η = λ { (m , n) → η } + ; commute = λ { (f , g) {H₁ , H₂} → commute {H₁ = H₁} {H₂ = H₂} f g } + } + ; associativity = λ { {X} {Y} {Z} {(H₁ , H₂) , H₃} → associativity {X} {Y} {Z} {H₁} {H₂} {H₃} } + ; unitaryˡ = Hypergraph-same-refl + ; unitaryʳ = unitaryʳ + } + ; braiding-compat = λ { {X} {Y} {H₁ , H₂} → braiding {X} {Y} {H₁} {H₂} } + } + } + where + η : Hypergraph-setoid n ×ₛ Hypergraph-setoid m ⟶ₛ Hypergraph-setoid (n + m) + η = record + { to = λ { (H₁ , H₂) → together H₁ H₂ } + ; cong = λ { (≡H₁ , ≡H₂) → together-resp-same ≡H₁ ≡H₂ } + } + +module F = SymmetricMonoidalFunctor Circ + +open Gate + +and-gate : ⊤ₛ ⟶ₛ Hypergraph-setoid 3 +and-gate = Const ⊤ₛ (Hypergraph-setoid 3) and-graph + where + and-graph : Hypergraph 3 + and-graph = record + { h = 1 + ; a = λ { 0F → 3 } + ; j = λ { 0F → edge-0-nodes } + ; l = λ { 0F → AND } + } + where + edge-0-nodes : Fin 3 → Fin 3 + edge-0-nodes 0F = # 0 + edge-0-nodes 1F = # 1 + edge-0-nodes 2F = # 2 diff --git a/DecorationFunctor/Trivial.agda b/DecorationFunctor/Trivial.agda index dee7c2e..6278d05 100644 --- a/DecorationFunctor/Trivial.agda +++ b/DecorationFunctor/Trivial.agda @@ -2,86 +2,70 @@ module DecorationFunctor.Trivial where -import Categories.Morphism as Morphism +open import Level using (0ℓ) open import Categories.Category.BinaryProducts using (module BinaryProducts) open import Categories.Category.Cartesian using (Cartesian) -open import Categories.Category.Cocartesian using (Cocartesian; module BinaryCoproducts) -open import Categories.Category.Core using (Category) -open import Categories.Category.Instance.Nat using (Nat-Cocartesian) open import Categories.Category.Instance.Nat using (Nat) open import Categories.Category.Instance.Setoids using (Setoids) -open import Categories.Category.Instance.SingletonSet using (SingletonSetoid) open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian) open import Categories.Category.Product using (_⁂_) -open import Categories.Functor using () renaming (_∘F_ to _∘_) -open import Categories.Functor.Core using (Functor) +open import Categories.Functor using (Functor) renaming (_∘F_ to _∘_) open import Categories.Functor.Monoidal.Symmetric using (module Lax) -open import Categories.NaturalTransformation using (NaturalTransformation) +open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory) -open import Category.Instance.Setoids.SymmetricMonoidal using (Setoids-×) open import Category.Instance.Nat.FinitelyCocomplete using (Nat-FinitelyCocomplete) -open import Data.Nat using (ℕ) -open import Data.Product.Base using (_,_) +open import Category.Instance.Setoids.SymmetricMonoidal {0ℓ} {0ℓ} using (Setoids-×; ×-symmetric′) +open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_) +open import Data.Setoid.Unit {0ℓ} {0ℓ} using (⊤ₛ) open import Data.Unit using (tt) -open import Data.Unit.Properties using () renaming (≡-setoid to ⊤-setoid) -open import Function.Base using (const) -open import Function.Bundles using (Func) -open import Level using (0ℓ; suc; lift) -open import Relation.Binary.Bundles using (Setoid) +open import Data.Unit.Properties using () renaming (≡-setoid to ⊤-≡ₛ) +open import Function using (Func; const) +open import Function.Construct.Constant using () renaming (function to Const) open import Relation.Binary.PropositionalEquality.Core using (refl) open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using (products) -open Cocartesian Nat-Cocartesian using (coproducts) +open BinaryProducts products using (-×-) open FinitelyCocompleteCategory Nat-FinitelyCocomplete - using () - renaming (symmetricMonoidalCategory to Nat-smc) -open Morphism (Setoids 0ℓ 0ℓ) using (_≅_) + using (-+-) + renaming (symmetricMonoidalCategory to Nat-smc) open Lax using (SymmetricMonoidalFunctor) -open BinaryProducts products using (-×-) -open BinaryCoproducts coproducts using (-+-) - - F : Functor Nat (Setoids 0ℓ 0ℓ) F = record - { F₀ = const (⊤-setoid) - ; F₁ = const (record { to = const tt ; cong = const refl }) - ; identity = const refl - ; homomorphism = const refl - ; F-resp-≈ = const (const refl) + { F₀ = const ⊤-≡ₛ + ; F₁ = const (Const ⊤-≡ₛ ⊤-≡ₛ tt) + ; identity = refl + ; homomorphism = refl + ; F-resp-≈ = const refl } -ε : Func (SingletonSetoid {0ℓ} {0ℓ}) ⊤-setoid -ε = record - { to = const tt - ; cong = const refl - } +ε : Func ⊤ₛ ⊤-≡ₛ +ε = Const ⊤ₛ ⊤-≡ₛ tt ⊗-homomorphism : NaturalTransformation (-×- ∘ (F ⁂ F)) (F ∘ -+-) -⊗-homomorphism = record - { η = const (record { to = const tt ; cong = const refl }) - ; commute = const (const refl) - ; sym-commute = const (const refl) +⊗-homomorphism = ntHelper record + { η = const (Const (⊤-≡ₛ ×ₛ ⊤-≡ₛ) ⊤-≡ₛ tt) + ; commute = const refl } -trivial : SymmetricMonoidalFunctor Nat-smc (Setoids-× {0ℓ}) -trivial = record - { F = F - ; isBraidedMonoidal = record - { isMonoidal = record - { ε = ε - ; ⊗-homo = ⊗-homomorphism - ; associativity = const refl - ; unitaryˡ = const refl - ; unitaryʳ = const refl - } - ; braiding-compat = const refl - } - } +opaque + unfolding ×-symmetric′ -and-gate : Func (SingletonSetoid {0ℓ} {0ℓ}) ⊤-setoid -and-gate = record - { to = const tt - ; cong = const refl - } + trivial : SymmetricMonoidalFunctor Nat-smc Setoids-× + trivial = record + { F = F + ; isBraidedMonoidal = record + { isMonoidal = record + { ε = ε + ; ⊗-homo = ⊗-homomorphism + ; associativity = refl + ; unitaryˡ = refl + ; unitaryʳ = refl + } + ; braiding-compat = refl + } + } + +and-gate : Func ⊤ₛ ⊤-≡ₛ +and-gate = Const ⊤ₛ ⊤-≡ₛ tt |