diff options
Diffstat (limited to 'DecorationFunctor')
| -rw-r--r-- | DecorationFunctor/Graph.agda | 743 | ||||
| -rw-r--r-- | DecorationFunctor/Trivial.agda | 87 |
2 files changed, 830 insertions, 0 deletions
diff --git a/DecorationFunctor/Graph.agda b/DecorationFunctor/Graph.agda new file mode 100644 index 0000000..b92ed05 --- /dev/null +++ b/DecorationFunctor/Graph.agda @@ -0,0 +1,743 @@ +{-# OPTIONS --without-K --safe #-} + +module DecorationFunctor.Graph 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.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 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.Empty using (⊥-elim) +open import Data.Fin using (#_) +open import Data.Fin.Base 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.Nat using (ℕ; _+_) +open import Data.Product.Base using (_,_) +open import Data.Product.Relation.Binary.Pointwise.NonDependent using (×-setoid) +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.Construct.Composition using (_↔-∘_) +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.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 (_≅_) +open Lax using (SymmetricMonoidalFunctor) + +open BinaryProducts products using (-×-) +open BinaryCoproducts coproducts using (-+-) renaming (+-assoc to Nat-+-assoc) + +record Graph (v : ℕ) : Set where + + field + e : ℕ + s : Fin e → Fin v + t : Fin e → Fin v + +record Graph-same {n : ℕ} (G G′ : Graph n) : Set where + + open Graph G public + open Graph G′ renaming (e to e′; s to s′; t to t′) public + + field + ↔e : Fin e ↔ Fin e′ + + open Inverse ↔e public + + field + ≗s : s ≗ s′ ∘ to + ≗t : t ≗ t′ ∘ to + +private + + variable + n m o : ℕ + G G′ G″ G₁ G₁′ : Graph n + G₂ G₂′ : Graph m + G₃ : Graph o + +Graph-same-refl : Graph-same G G +Graph-same-refl = record + { ↔e = ↔-id _ + ; ≗s = λ _ → refl + ; ≗t = λ _ → refl + } + +Graph-same-sym : Graph-same G G′ → Graph-same G′ G +Graph-same-sym ≡G = record + { ↔e = ↔-sym ↔e + ; ≗s = sym ∘ s∘from≗s′ + ; ≗t = sym ∘ t∘from≗t′ + } + where + open ≡-Reasoning + open Graph-same ≡G + s∘from≗s′ : s ∘ from ≗ s′ + s∘from≗s′ x = begin + s (from x) ≡⟨ ≗s (from x) ⟩ + s′ (to (from x)) ≡⟨ cong s′ (inverseˡ refl) ⟩ + s′ x ∎ + t∘from≗t′ : t ∘ from ≗ t′ + t∘from≗t′ x = begin + t (from x) ≡⟨ ≗t (from x) ⟩ + t′ (to (from x)) ≡⟨ cong t′ (inverseˡ refl) ⟩ + t′ x ∎ + +Graph-same-trans : Graph-same G G′ → Graph-same G′ G″ → Graph-same G G″ +Graph-same-trans ≡G₁ ≡G₂ = record + { ↔e = ↔e ≡G₂ ↔-∘ ↔e ≡G₁ + ; ≗s = λ x → trans (≗s ≡G₁ x) (≗s ≡G₂ _) + ; ≗t = λ x → trans (≗t ≡G₁ x) (≗t ≡G₂ _) + } + where + open Graph-same + +Graph-setoid : ℕ → Setoid 0ℓ 0ℓ +Graph-setoid p = record + { Carrier = Graph p + ; _≈_ = Graph-same + ; isEquivalence = record + { refl = Graph-same-refl + ; sym = Graph-same-sym + ; trans = Graph-same-trans + } + } + +map-nodes : (Fin n → Fin m) → Graph n → Graph m +map-nodes f G = record + { e = e + ; s = f ∘ s + ; t = f ∘ t + } + where + open Graph G + +Graph-same-cong : (f : Fin n → Fin m) → Graph-same G G′ → Graph-same (map-nodes f G) (map-nodes f G′) +Graph-same-cong f ≡G = record + { ↔e = ↔e + ; ≗s = cong f ∘ ≗s + ; ≗t = cong f ∘ ≗t + } + where + open Graph-same ≡G + +Graph-Func : (Fin n → Fin m) → Func (Graph-setoid n) (Graph-setoid m) +Graph-Func f = record + { to = map-nodes f + ; cong = Graph-same-cong f + } + +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)) } + } + where + open Graph-same ≡G + +F : Functor Nat (Setoids 0ℓ 0ℓ) +F = record + { F₀ = Graph-setoid + ; F₁ = Graph-Func + ; identity = id + ; homomorphism = λ { {_} {_} {_} {f} {g} → homomorphism f g } + ; 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 + { e = 0 + ; s = λ () + ; t = λ () + } + +ε : Func (SingletonSetoid {0ℓ} {0ℓ}) (Graph-setoid 0) +ε = record + { to = const empty-graph + ; cong = const Graph-same-refl + } + +together : Graph n → Graph m → Graph (n + m) +together {n} {m} G₁ G₂ = record + { e = e G₁ + e G₂ + ; s = join n m ∘ map (s G₁) (s G₂) ∘ splitAt (e G₁) + ; t = join n m ∘ map (t G₁) (t G₂) ∘ splitAt (e G₁) + } + where + open Graph + ++-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 + : ∀ {n m : ℕ} {G₁ G₁′ : Graph n} {G₂ G₂′ : Graph m} + → Graph-same G₁ G₁′ + → Graph-same G₂ G₂′ + → Graph-same (together G₁ G₂) (together G₁′ G₂′) +together-resp-same {n} {m} ≡G₁ ≡G₂ = record + { ↔e = +-resp-↔ ≡G₁.↔e ≡G₂.↔e + ; ≗s = ≗s + ; ≗t = ≗t + } + where + module ≡G₁ = Graph-same ≡G₁ + module ≡G₂ = Graph-same ≡G₂ + open ≡-Reasoning + module ↔e₁+e₂ = Inverse (+-resp-↔ ≡G₁.↔e ≡G₂.↔e) + ≗s : join n m ∘ map ≡G₁.s ≡G₂.s ∘ splitAt ≡G₁.e ≗ join n m ∘ map ≡G₁.s′ ≡G₂.s′ ∘ splitAt ≡G₁.e′ ∘ ↔e₁+e₂.to + ≗s x = begin + (join n m ∘ map ≡G₁.s ≡G₂.s ∘ splitAt ≡G₁.e) x + ≡⟨ cong (join n m) (map-cong ≡G₁.≗s ≡G₂.≗s (splitAt ≡G₁.e x)) ⟩ + (join n m ∘ map (≡G₁.s′ ∘ ≡G₁.to) (≡G₂.s′ ∘ ≡G₂.to) ∘ splitAt ≡G₁.e) x + ≡⟨ cong (join n m) (map-map (splitAt ≡G₁.e x)) ⟨ + (join n m ∘ map ≡G₁.s′ ≡G₂.s′ ∘ map ≡G₁.to ≡G₂.to ∘ splitAt ≡G₁.e) x + ≡⟨ cong + (join n m ∘ map ≡G₁.s′ ≡G₂.s′) + (splitAt-join ≡G₁.e′ ≡G₂.e′ (map ≡G₁.to ≡G₂.to (splitAt ≡G₁.e x))) ⟨ + (join n m ∘ map ≡G₁.s′ ≡G₂.s′ ∘ splitAt ≡G₁.e′ ∘ join ≡G₁.e′ ≡G₂.e′ ∘ map ≡G₁.to ≡G₂.to ∘ splitAt ≡G₁.e) x ≡⟨⟩ + (join n m ∘ map ≡G₁.s′ ≡G₂.s′ ∘ splitAt ≡G₁.e′ ∘ ↔e₁+e₂.to) x ∎ + ≗t : join n m ∘ map ≡G₁.t ≡G₂.t ∘ splitAt ≡G₁.e ≗ join n m ∘ map ≡G₁.t′ ≡G₂.t′ ∘ splitAt ≡G₁.e′ ∘ ↔e₁+e₂.to + ≗t x = begin + (join n m ∘ map ≡G₁.t ≡G₂.t ∘ splitAt ≡G₁.e) x + ≡⟨ cong (join n m) (map-cong ≡G₁.≗t ≡G₂.≗t (splitAt ≡G₁.e x)) ⟩ + (join n m ∘ map (≡G₁.t′ ∘ ≡G₁.to) (≡G₂.t′ ∘ ≡G₂.to) ∘ splitAt ≡G₁.e) x + ≡⟨ cong (join n m) (map-map (splitAt ≡G₁.e x)) ⟨ + (join n m ∘ map ≡G₁.t′ ≡G₂.t′ ∘ map ≡G₁.to ≡G₂.to ∘ splitAt ≡G₁.e) x + ≡⟨ cong + (join n m ∘ map ≡G₁.t′ ≡G₂.t′) + (splitAt-join ≡G₁.e′ ≡G₂.e′ (map ≡G₁.to ≡G₂.to (splitAt ≡G₁.e x))) ⟨ + (join n m ∘ map ≡G₁.t′ ≡G₂.t′ ∘ splitAt ≡G₁.e′ ∘ join ≡G₁.e′ ≡G₂.e′ ∘ map ≡G₁.to ≡G₂.to ∘ splitAt ≡G₁.e) x ≡⟨⟩ + (join n m ∘ map ≡G₁.t′ ≡G₂.t′ ∘ splitAt ≡G₁.e′ ∘ ↔e₁+e₂.to) x ∎ + +commute + : ∀ {n n′ m m′} + → {G₁ G₁′ : Graph n} + → {G₂ 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 + ; ≗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 ≡-Reasoning + source-commute + : ≡fG₁+gG₂.s + ≗ [ (_↑ˡ m′) ∘ f , (n′ ↑ʳ_) ∘ g ] ∘ splitAt n + ∘ ≡G₁+G₂.s′ + ∘ ≡fG₁+gG₂.to + source-commute x = begin + ≡fG₁+gG₂.s x + ≡⟨ ≡fG₁+gG₂.≗s x ⟩ + (≡fG₁+gG₂.s′ ∘ ≡fG₁+gG₂.to) 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 + ≡⟨⟩ + ([ (_↑ˡ m′) ∘ f , (n′ ↑ʳ_) ∘ g ] ∘ splitAt n ∘ ≡G₁+G₂.s′ ∘ ≡fG₁+gG₂.to) x ∎ + target-commute + : ≡fG₁+gG₂.t + ≗ [ (_↑ˡ m′) ∘ f , (n′ ↑ʳ_) ∘ g ] ∘ splitAt n + ∘ ≡G₁+G₂.t′ + ∘ ≡fG₁+gG₂.to + target-commute x = begin + ≡fG₁+gG₂.t x + ≡⟨ ≡fG₁+gG₂.≗t x ⟩ + (≡fG₁+gG₂.t′ ∘ ≡fG₁+gG₂.to) 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 + ≡⟨⟩ + ([ (_↑ˡ m′) ∘ f , (n′ ↑ʳ_) ∘ g ] ∘ splitAt n ∘ ≡G₁+G₂.t′ ∘ ≡fG₁+gG₂.to) x ∎ + + +⊗-homomorphism : NaturalTransformation (-×- ∘′ (F ⁂ F)) (F ∘′ -+-) +⊗-homomorphism = 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₂)) } + } + where + η : Func (×-setoid (Graph-setoid n) (Graph-setoid m)) (Graph-setoid (n + m)) + η = record + { to = λ { (G₁ , G₂) → together G₁ G₂ } + ; cong = λ { (≡G₁ , ≡G₂) → together-resp-same ≡G₁ ≡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 : ℕ} + → {G₁ G₁′ : Graph X} + → {G₂ G₂′ : Graph Y} + → {G₃ G₃′ : Graph Z} + → Graph-same G₁ G₁′ + → Graph-same G₂ G₂′ + → Graph-same G₃ G₃′ + → 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 + { ↔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) + 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 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 + ≡⟨ 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 + ≡⟨ 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 + (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 + ≡⟨ 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 + (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 + ≡⟨ 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) + ≗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 + ≡⟨ 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 + ≡⟨ 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 + (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 + ≡⟨ 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 + (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 + ≡⟨ 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 + { to = to + ; from = from + ; to-cong = λ { refl → refl } + ; from-cong = λ { refl → refl } + ; 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) + +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′ + ; ≗s = ≗s+0 + ; ≗t = ≗t+0 + } + where + open Graph-same ≡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 + bruh : ∀ e → (x : Fin e) → x ≡ to (n+0↔0 e) (x ↑ˡ 0) + bruh (ℕ.suc ℕ.zero) zero = refl + bruh (ℕ.suc (ℕ.suc e)) zero = refl + bruh (ℕ.suc (ℕ.suc e)) (suc x) = cong suc (bruh (ℕ.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 (bruh 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 (bruh 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) ∎ + ++-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-map + : {A B C D : Set} + → {f : A → C} {g : B → D} + → swap ∘ map f g ≗ map g f ∘ swap +swap-map (inj₁ _) = refl +swap-map (inj₂ _) = refl + +final-lemma : ∀ {x y : ℕ} → [ x ↑ʳ_ , _↑ˡ y ] ≗ join x y ∘ swap +final-lemma (inj₁ x) = refl +final-lemma (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 + ; ≗s = ≗s + ; ≗t = ≗t + } + where + open ≡-Reasoning + module ≡G₁ = Graph-same ≡G₁ + module ≡G₂ = Graph-same ≡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 + ≗s x = begin + ([ m ↑ʳ_ , _↑ˡ n ] ∘ splitAt n ∘ join n m ∘ map ≡G₁.s ≡G₂.s ∘ splitAt ≡G₁.e) x + ≡⟨ (final-lemma ∘ 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 ∎ + ≗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 + ≗t x = begin + ([ m ↑ʳ_ , _↑ˡ n ] ∘ splitAt n ∘ join n m ∘ map ≡G₁.t ≡G₂.t ∘ splitAt ≡G₁.e) x + ≡⟨ (final-lemma ∘ 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₂ } + } + } + +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 } + } + where + and-graph : Graph 3 + and-graph = record + { e = 2 + ; s = λ { 0F → # 0 ; 1F → # 1 } + ; t = λ { 0F → # 2 ; 1F → # 2 } + } diff --git a/DecorationFunctor/Trivial.agda b/DecorationFunctor/Trivial.agda new file mode 100644 index 0000000..dee7c2e --- /dev/null +++ b/DecorationFunctor/Trivial.agda @@ -0,0 +1,87 @@ +{-# OPTIONS --without-K --safe #-} + +module DecorationFunctor.Trivial 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.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 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 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 Relation.Binary.PropositionalEquality.Core using (refl) + +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 (_≅_) +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) + } + +ε : Func (SingletonSetoid {0ℓ} {0ℓ}) ⊤-setoid +ε = record + { to = const tt + ; cong = const refl + } + +⊗-homomorphism : NaturalTransformation (-×- ∘ (F ⁂ F)) (F ∘ -+-) +⊗-homomorphism = record + { η = const (record { to = const tt ; cong = const refl }) + ; commute = const (const refl) + ; sym-commute = const (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 + } + } + +and-gate : Func (SingletonSetoid {0ℓ} {0ℓ}) ⊤-setoid +and-gate = record + { to = const tt + ; cong = const refl + } |