diff options
| -rw-r--r-- | Category/Monoidal/Instance/Nat.agda | 71 | ||||
| -rw-r--r-- | Data/Circuit/Merge.agda | 341 | ||||
| -rw-r--r-- | Data/Circuit/Value.agda | 157 | ||||
| -rw-r--r-- | Data/Fin/Preimage.agda | 48 | ||||
| -rw-r--r-- | Data/Setoid.agda | 8 | ||||
| -rw-r--r-- | Data/Subset/Functional.agda | 162 | ||||
| -rw-r--r-- | Data/System.agda | 86 | ||||
| -rw-r--r-- | Data/System/Values.agda | 21 | ||||
| -rw-r--r-- | Data/Vector.agda | 82 | ||||
| -rw-r--r-- | Functor/Instance/Decorate.agda | 2 | ||||
| -rw-r--r-- | Functor/Instance/Nat/Preimage.agda | 65 | ||||
| -rw-r--r-- | Functor/Instance/Nat/Pull.agda | 63 | ||||
| -rw-r--r-- | Functor/Instance/Nat/Push.agda | 64 | ||||
| -rw-r--r-- | Functor/Instance/Nat/System.agda | 96 | ||||
| -rw-r--r-- | Functor/Monoidal/Braided/Strong/Properties.agda | 59 | ||||
| -rw-r--r-- | Functor/Monoidal/Instance/Nat/Preimage.agda | 164 | ||||
| -rw-r--r-- | Functor/Monoidal/Instance/Nat/Pull.agda | 192 | ||||
| -rw-r--r-- | Functor/Monoidal/Instance/Nat/Push.agda | 339 | ||||
| -rw-r--r-- | Functor/Monoidal/Instance/Nat/System.agda | 429 | ||||
| -rw-r--r-- | Functor/Monoidal/Strong/Properties.agda | 104 |
20 files changed, 2552 insertions, 1 deletions
diff --git a/Category/Monoidal/Instance/Nat.agda b/Category/Monoidal/Instance/Nat.agda new file mode 100644 index 0000000..24b30a6 --- /dev/null +++ b/Category/Monoidal/Instance/Nat.agda @@ -0,0 +1,71 @@ +{-# OPTIONS --without-K --safe #-} + +module Category.Monoidal.Instance.Nat where + +open import Level using (0ℓ) +open import Categories.Category.Monoidal.Bundle using (MonoidalCategory; SymmetricMonoidalCategory) +open import Categories.Category.Instance.Nat using (Nat; Nat-Cartesian; Nat-Cocartesian; Natop) +open import Categories.Category.Cartesian using (Cartesian) +open import Categories.Category.Cocartesian using (Cocartesian; module CocartesianMonoidal; module CocartesianSymmetricMonoidal) +open import Categories.Category.Cartesian.Monoidal using (module CartesianMonoidal) +open import Categories.Category.Duality using (coCartesian⇒Cocartesian; Cocartesian⇒coCartesian) + +import Categories.Category.Cartesian.SymmetricMonoidal as CartesianSymmetricMonoidal + +Natop-Cartesian : Cartesian Natop +Natop-Cartesian = Cocartesian⇒coCartesian Nat Nat-Cocartesian + +Natop-Cocartesian : Cocartesian Natop +Natop-Cocartesian = coCartesian⇒Cocartesian Natop Nat-Cartesian + +module Monoidal where + + open MonoidalCategory + open CartesianMonoidal using () renaming (monoidal to ×-monoidal) + open CocartesianMonoidal using (+-monoidal) + + Nat,+,0 : MonoidalCategory 0ℓ 0ℓ 0ℓ + Nat,+,0 .U = Nat + Nat,+,0 .monoidal = +-monoidal Nat Nat-Cocartesian + + Nat,×,1 : MonoidalCategory 0ℓ 0ℓ 0ℓ + Nat,×,1 .U = Nat + Nat,×,1 .monoidal = ×-monoidal Nat-Cartesian + + Natop,+,0 : MonoidalCategory 0ℓ 0ℓ 0ℓ + Natop,+,0 .U = Natop + Natop,+,0 .monoidal = ×-monoidal Natop-Cartesian + + Natop,×,1 : MonoidalCategory 0ℓ 0ℓ 0ℓ + Natop,×,1 .U = Natop + Natop,×,1 .monoidal = +-monoidal Natop Natop-Cocartesian + +module Symmetric where + + open SymmetricMonoidalCategory + open CartesianMonoidal using () renaming (monoidal to ×-monoidal) + open CocartesianMonoidal using (+-monoidal) + open CartesianSymmetricMonoidal using () renaming (symmetric to ×-symmetric) + open CocartesianSymmetricMonoidal using (+-symmetric) + + Nat,+,0 : SymmetricMonoidalCategory 0ℓ 0ℓ 0ℓ + Nat,+,0 .U = Nat + Nat,+,0 .monoidal = +-monoidal Nat Nat-Cocartesian + Nat,+,0 .symmetric = +-symmetric Nat Nat-Cocartesian + + Nat,×,1 : SymmetricMonoidalCategory 0ℓ 0ℓ 0ℓ + Nat,×,1 .U = Nat + Nat,×,1 .monoidal = ×-monoidal Nat-Cartesian + Nat,×,1 .symmetric = ×-symmetric Nat Nat-Cartesian + + Natop,+,0 : SymmetricMonoidalCategory 0ℓ 0ℓ 0ℓ + Natop,+,0 .U = Natop + Natop,+,0 .monoidal = ×-monoidal Natop-Cartesian + Natop,+,0 .symmetric = ×-symmetric Natop Natop-Cartesian + + Natop,×,1 : SymmetricMonoidalCategory 0ℓ 0ℓ 0ℓ + Natop,×,1 .U = Natop + Natop,×,1 .monoidal = +-monoidal Natop Natop-Cocartesian + Natop,×,1 .symmetric = +-symmetric Natop Natop-Cocartesian + +open Symmetric public diff --git a/Data/Circuit/Merge.agda b/Data/Circuit/Merge.agda new file mode 100644 index 0000000..82c0d92 --- /dev/null +++ b/Data/Circuit/Merge.agda @@ -0,0 +1,341 @@ +{-# OPTIONS --without-K --safe #-} + +module Data.Circuit.Merge where + +open import Data.Nat.Base using (ℕ) +open import Data.Fin.Base using (Fin; pinch; punchIn; punchOut) +open import Data.Fin.Properties using (punchInᵢ≢i; punchIn-punchOut) +open import Data.Bool.Properties using (if-eta) +open import Data.Bool using (Bool; if_then_else_) +open import Data.Circuit.Value using (Value; join; join-comm; join-assoc) +open import Data.Subset.Functional + using + ( Subset + ; ⁅_⁆ ; ⊥ ; ⁅⁆∘ρ + ; foldl ; foldl-cong₁ ; foldl-cong₂ + ; foldl-[] ; foldl-suc + ; foldl-⊥ ; foldl-⁅⁆ + ; foldl-fusion + ) +open import Data.Vector as V using (Vector; head; tail; removeAt) +open import Data.Fin.Permutation + using + ( Permutation + ; Permutation′ + ; _⟨$⟩ˡ_ ; _⟨$⟩ʳ_ + ; inverseˡ ; inverseʳ + ; id + ; flip + ; insert ; remove + ; punchIn-permute + ) +open import Data.Product using (Σ-syntax; _,_) +open import Data.Fin.Preimage using (preimage; preimage-cong₁; preimage-cong₂) +open import Function.Base using (∣_⟩-_; _∘_) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_) + +open Value using (U) +open ℕ +open Fin +open Bool + +_when_ : Value → Bool → Value +x when b = if b then x else U + +opaque + merge-with : {A : ℕ} → Value → Vector Value A → Subset A → Value + merge-with e v = foldl (∣ join ⟩- v) e + + merge-with-cong : {A : ℕ} {v₁ v₂ : Vector Value A} (e : Value) → v₁ ≗ v₂ → merge-with e v₁ ≗ merge-with e v₂ + merge-with-cong e v₁≗v₂ = foldl-cong₁ (λ x → ≡.cong (join x) ∘ v₁≗v₂) e + + merge-with-cong₂ : {A : ℕ} (e : Value) (v : Vector Value A) {S₁ S₂ : Subset A} → S₁ ≗ S₂ → merge-with e v S₁ ≡ merge-with e v S₂ + merge-with-cong₂ e v = foldl-cong₂ (∣ join ⟩- v) e + + merge-with-⊥ : {A : ℕ} (e : Value) (v : Vector Value A) → merge-with e v ⊥ ≡ e + merge-with-⊥ e v = foldl-⊥ (∣ join ⟩- v) e + + merge-with-[] : (e : Value) (v : Vector Value 0) (S : Subset 0) → merge-with e v S ≡ e + merge-with-[] e v = foldl-[] (∣ join ⟩- v) e + + merge-with-suc + : {A : ℕ} (e : Value) (v : Vector Value (suc A)) (S : Subset (suc A)) + → merge-with e v S + ≡ merge-with (if head S then join e (head v) else e) (tail v) (tail S) + merge-with-suc e v = foldl-suc (∣ join ⟩- v) e + + merge-with-join + : {A : ℕ} + (x y : Value) + (v : Vector Value A) + → merge-with (join x y) v ≗ join x ∘ merge-with y v + merge-with-join {A} x y v S = ≡.sym (foldl-fusion (join x) fuse y S) + where + fuse : (acc : Value) (k : Fin A) → join x (join acc (v k)) ≡ join (join x acc) (v k) + fuse acc k = ≡.sym (join-assoc x acc (v k)) + + merge-with-⁅⁆ : {A : ℕ} (e : Value) (v : Vector Value A) (x : Fin A) → merge-with e v ⁅ x ⁆ ≡ join e (v x) + merge-with-⁅⁆ e v = foldl-⁅⁆ (∣ join ⟩- v) e + +merge-with-U : {A : ℕ} (e : Value) (S : Subset A) → merge-with e (λ _ → U) S ≡ e +merge-with-U {zero} e S = merge-with-[] e (λ _ → U) S +merge-with-U {suc A} e S = begin + merge-with e (λ _ → U) S ≡⟨ merge-with-suc e (λ _ → U) S ⟩ + merge-with + (if head S then join e U else e) + (tail (λ _ → U)) (tail S) ≡⟨ ≡.cong (λ h → merge-with (if head S then h else e) _ _) (join-comm e U) ⟩ + merge-with + (if head S then e else e) + (tail (λ _ → U)) (tail S) ≡⟨ ≡.cong (λ h → merge-with h (λ _ → U) (tail S)) (if-eta (head S)) ⟩ + merge-with e (tail (λ _ → U)) (tail S) ≡⟨⟩ + merge-with e (λ _ → U) (tail S) ≡⟨ merge-with-U e (tail S) ⟩ + e ∎ + where + open ≡.≡-Reasoning + +merge : {A : ℕ} → Vector Value A → Subset A → Value +merge v = merge-with U v + +merge-cong₁ : {A : ℕ} {v₁ v₂ : Vector Value A} → v₁ ≗ v₂ → merge v₁ ≗ merge v₂ +merge-cong₁ = merge-with-cong U + +merge-cong₂ : {A : ℕ} (v : Vector Value A) {S₁ S₂ : Subset A} → S₁ ≗ S₂ → merge v S₁ ≡ merge v S₂ +merge-cong₂ = merge-with-cong₂ U + +merge-⊥ : {A : ℕ} (v : Vector Value A) → merge v ⊥ ≡ U +merge-⊥ = merge-with-⊥ U + +merge-[] : (v : Vector Value 0) (S : Subset 0) → merge v S ≡ U +merge-[] = merge-with-[] U + +merge-[]₂ : {v₁ v₂ : Vector Value 0} {S₁ S₂ : Subset 0} → merge v₁ S₁ ≡ merge v₂ S₂ +merge-[]₂ {v₁} {v₂} {S₁} {S₂} = ≡.trans (merge-[] v₁ S₁) (≡.sym (merge-[] v₂ S₂)) + +merge-⁅⁆ : {A : ℕ} (v : Vector Value A) (x : Fin A) → merge v ⁅ x ⁆ ≡ v x +merge-⁅⁆ = merge-with-⁅⁆ U + +join-merge : {A : ℕ} (e : Value) (v : Vector Value A) (S : Subset A) → join e (merge v S) ≡ merge-with e v S +join-merge e v S = ≡.sym (≡.trans (≡.cong (λ h → merge-with h v S) (join-comm U e)) (merge-with-join e U v S)) + +merge-suc + : {A : ℕ} (v : Vector Value (suc A)) (S : Subset (suc A)) + → merge v S + ≡ merge-with (head v when head S) (tail v) (tail S) +merge-suc = merge-with-suc U + +insert-f0-0 + : {A B : ℕ} + (f : Fin (suc A) → Fin (suc B)) + → Σ[ ρ ∈ Permutation′ (suc B) ] (ρ ⟨$⟩ʳ (f zero) ≡ zero) +insert-f0-0 f = insert (f zero) zero id , help + where + open import Data.Fin using (_≟_) + open import Relation.Nullary.Decidable using (yes; no) + help : insert (f zero) zero id ⟨$⟩ʳ f zero ≡ zero + help with f zero ≟ f zero + ... | yes _ = ≡.refl + ... | no f0≢f0 with () ← f0≢f0 ≡.refl + +merge-removeAt + : {A : ℕ} + (k : Fin (suc A)) + (v : Vector Value (suc A)) + (S : Subset (suc A)) + → merge v S ≡ join (v k when S k) (merge (removeAt v k) (removeAt S k)) +merge-removeAt {A} zero v S = begin + merge-with U v S ≡⟨ merge-suc v S ⟩ + merge-with (head v when head S) (tail v) (tail S) ≡⟨ join-merge (head v when head S) (tail v) (tail S) ⟨ + join (head v when head S) (merge-with U (tail v) (tail S)) ∎ + where + open ≡.≡-Reasoning +merge-removeAt {suc A} (suc k) v S = begin + merge-with U v S ≡⟨ merge-suc v S ⟩ + merge-with v0? (tail v) (tail S) ≡⟨ join-merge _ (tail v) (tail S) ⟨ + join v0? (merge (tail v) (tail S)) ≡⟨ ≡.cong (join v0?) (merge-removeAt k (tail v) (tail S)) ⟩ + join v0? (join vk? (merge (tail v-) (tail S-))) ≡⟨ join-assoc (head v when head S) _ _ ⟨ + join (join v0? vk?) (merge (tail v-) (tail S-)) ≡⟨ ≡.cong (λ h → join h (merge (tail v-) (tail S-))) (join-comm (head v- when head S-) _) ⟩ + join (join vk? v0?) (merge (tail v-) (tail S-)) ≡⟨ join-assoc (tail v k when tail S k) _ _ ⟩ + join vk? (join v0? (merge (tail v-) (tail S-))) ≡⟨ ≡.cong (join vk?) (join-merge _ (tail v-) (tail S-)) ⟩ + join vk? (merge-with v0? (tail v-) (tail S-)) ≡⟨ ≡.cong (join vk?) (merge-suc v- S-) ⟨ + join vk? (merge v- S-) ∎ + where + v0? vk? : Value + v0? = head v when head S + vk? = tail v k when tail S k + v- : Vector Value (suc A) + v- = removeAt v (suc k) + S- : Subset (suc A) + S- = removeAt S (suc k) + open ≡.≡-Reasoning + +import Function.Structures as FunctionStructures +open module FStruct {A B : Set} = FunctionStructures {_} {_} {_} {_} {A} _≡_ {B} _≡_ using (IsInverse) +open IsInverse using () renaming (inverseˡ to invˡ; inverseʳ to invʳ) + +merge-preimage-ρ + : {A B : ℕ} + → (ρ : Permutation A B) + → (v : Vector Value A) + (S : Subset B) + → merge v (preimage (ρ ⟨$⟩ʳ_) S) ≡ merge (v ∘ (ρ ⟨$⟩ˡ_)) S +merge-preimage-ρ {zero} {zero} ρ v S = merge-[]₂ +merge-preimage-ρ {zero} {suc B} ρ v S with () ← ρ ⟨$⟩ˡ zero +merge-preimage-ρ {suc A} {zero} ρ v S with () ← ρ ⟨$⟩ʳ zero +merge-preimage-ρ {suc A} {suc B} ρ v S = begin + merge v (preimage ρʳ S) ≡⟨ merge-removeAt (head ρˡ) v (preimage ρʳ S) ⟩ + join + (head (v ∘ ρˡ) when S (ρʳ (ρˡ zero))) + (merge v- [preimageρʳS]-) ≡⟨ ≡.cong (λ h → join h (merge v- [preimageρʳS]-)) ≡vρˡ0? ⟩ + join vρˡ0? (merge v- [preimageρʳS]-) ≡⟨ ≡.cong (join vρˡ0?) (merge-cong₂ v- preimage-) ⟩ + join vρˡ0? (merge v- (preimage ρʳ- S-)) ≡⟨ ≡.cong (join vρˡ0?) (merge-preimage-ρ ρ- v- S-) ⟩ + join vρˡ0? (merge (v- ∘ ρˡ-) S-) ≡⟨ ≡.cong (join vρˡ0?) (merge-cong₁ v∘ρˡ- S-) ⟩ + join vρˡ0? (merge (tail (v ∘ ρˡ)) S-) ≡⟨ join-merge vρˡ0? (tail (v ∘ ρˡ)) S- ⟩ + merge-with vρˡ0? (tail (v ∘ ρˡ)) S- ≡⟨ merge-suc (v ∘ ρˡ) S ⟨ + merge (v ∘ ρˡ) S ∎ + where + ρˡ : Fin (suc B) → Fin (suc A) + ρˡ = ρ ⟨$⟩ˡ_ + ρʳ : Fin (suc A) → Fin (suc B) + ρʳ = ρ ⟨$⟩ʳ_ + ρ- : Permutation A B + ρ- = remove (head ρˡ) ρ + ρˡ- : Fin B → Fin A + ρˡ- = ρ- ⟨$⟩ˡ_ + ρʳ- : Fin A → Fin B + ρʳ- = ρ- ⟨$⟩ʳ_ + v- : Vector Value A + v- = removeAt v (head ρˡ) + [preimageρʳS]- : Subset A + [preimageρʳS]- = removeAt (preimage ρʳ S) (head ρˡ) + S- : Subset B + S- = tail S + vρˡ0? : Value + vρˡ0? = head (v ∘ ρˡ) when head S + open ≡.≡-Reasoning + ≡vρˡ0? : head (v ∘ ρˡ) when S (ρʳ (head ρˡ)) ≡ head (v ∘ ρˡ) when head S + ≡vρˡ0? = ≡.cong ((head (v ∘ ρˡ) when_) ∘ S) (inverseʳ ρ) + v∘ρˡ- : v- ∘ ρˡ- ≗ tail (v ∘ ρˡ) + v∘ρˡ- x = begin + v- (ρˡ- x) ≡⟨⟩ + v (punchIn (head ρˡ) (punchOut {A} {head ρˡ} _)) ≡⟨ ≡.cong v (punchIn-punchOut _) ⟩ + v (ρˡ (punchIn (ρʳ (ρˡ zero)) x)) ≡⟨ ≡.cong (λ h → v (ρˡ (punchIn h x))) (inverseʳ ρ) ⟩ + v (ρˡ (punchIn zero x)) ≡⟨⟩ + v (ρˡ (suc x)) ≡⟨⟩ + tail (v ∘ ρˡ) x ∎ + preimage- : [preimageρʳS]- ≗ preimage ρʳ- S- + preimage- x = begin + [preimageρʳS]- x ≡⟨⟩ + removeAt (preimage ρʳ S) (head ρˡ) x ≡⟨⟩ + S (ρʳ (punchIn (head ρˡ) x)) ≡⟨ ≡.cong S (punchIn-permute ρ (head ρˡ) x) ⟩ + S (punchIn (ρʳ (head ρˡ)) (ρʳ- x)) ≡⟨⟩ + S (punchIn (ρʳ (ρˡ zero)) (ρʳ- x)) ≡⟨ ≡.cong (λ h → S (punchIn h (ρʳ- x))) (inverseʳ ρ) ⟩ + S (punchIn zero (ρʳ- x)) ≡⟨⟩ + S (suc (ρʳ- x)) ≡⟨⟩ + preimage ρʳ- S- x ∎ + +push-with : {A B : ℕ} → (e : Value) → Vector Value A → (Fin A → Fin B) → Vector Value B +push-with e v f = merge-with e v ∘ preimage f ∘ ⁅_⁆ + +push : {A B : ℕ} → Vector Value A → (Fin A → Fin B) → Vector Value B +push = push-with U + +mutual + merge-preimage + : {A B : ℕ} + (f : Fin A → Fin B) + → (v : Vector Value A) + (S : Subset B) + → merge v (preimage f S) ≡ merge (push v f) S + merge-preimage {zero} {zero} f v S = merge-[]₂ + merge-preimage {zero} {suc B} f v S = begin + merge v (preimage f S) ≡⟨ merge-[] v (preimage f S) ⟩ + U ≡⟨ merge-with-U U S ⟨ + merge (λ _ → U) S ≡⟨ merge-cong₁ (λ x → ≡.sym (merge-[] v (⁅ x ⁆ ∘ f))) S ⟩ + merge (push v f) S ∎ + where + open ≡.≡-Reasoning + merge-preimage {suc A} {zero} f v S with () ← f zero + merge-preimage {suc A} {suc B} f v S with insert-f0-0 f + ... | ρ , ρf0≡0 = begin + merge v (preimage f S) ≡⟨ merge-cong₂ v (preimage-cong₁ (λ x → inverseˡ ρ {f x}) S) ⟨ + merge v (preimage (ρˡ ∘ ρʳ ∘ f) S) ≡⟨⟩ + merge v (preimage (ρʳ ∘ f) (preimage ρˡ S)) ≡⟨ merge-preimage-f0≡0 (ρʳ ∘ f) ρf0≡0 v (preimage ρˡ S) ⟩ + merge (merge v ∘ preimage (ρʳ ∘ f) ∘ ⁅_⁆) (preimage ρˡ S) ≡⟨ merge-preimage-ρ (flip ρ) (merge v ∘ preimage (ρʳ ∘ f) ∘ ⁅_⁆) S ⟩ + merge (merge v ∘ preimage (ρʳ ∘ f) ∘ ⁅_⁆ ∘ ρʳ) S ≡⟨ merge-cong₁ (merge-cong₂ v ∘ preimage-cong₂ (ρʳ ∘ f) ∘ ⁅⁆∘ρ ρ) S ⟩ + merge (merge v ∘ preimage (ρʳ ∘ f) ∘ preimage ρˡ ∘ ⁅_⁆) S ≡⟨⟩ + merge (merge v ∘ preimage (ρˡ ∘ ρʳ ∘ f) ∘ ⁅_⁆) S ≡⟨ merge-cong₁ (merge-cong₂ v ∘ preimage-cong₁ (λ y → inverseˡ ρ {f y}) ∘ ⁅_⁆) S ⟩ + merge (merge v ∘ preimage f ∘ ⁅_⁆) S ∎ + where + open ≡.≡-Reasoning + ρʳ ρˡ : Fin (ℕ.suc B) → Fin (ℕ.suc B) + ρʳ = ρ ⟨$⟩ʳ_ + ρˡ = ρ ⟨$⟩ˡ_ + + merge-preimage-f0≡0 + : {A B : ℕ} + (f : Fin (ℕ.suc A) → Fin (ℕ.suc B)) + → f Fin.zero ≡ Fin.zero + → (v : Vector Value (ℕ.suc A)) + (S : Subset (ℕ.suc B)) + → merge v (preimage f S) ≡ merge (merge v ∘ preimage f ∘ ⁅_⁆) S + merge-preimage-f0≡0 {A} {B} f f0≡0 v S + using S0 , S- ← head S , tail S + using v0 , v- ← head v , tail v + using _ , f- ← head f , tail f + = begin + merge v f⁻¹[S] ≡⟨ merge-suc v f⁻¹[S] ⟩ + merge-with v0? v- f⁻¹[S]- ≡⟨ join-merge v0? v- f⁻¹[S]- ⟨ + join v0? (merge v- f⁻¹[S]-) ≡⟨ ≡.cong (join v0?) (merge-preimage f- v- S) ⟩ + join v0? (merge f[v-] S) ≡⟨ join-merge v0? f[v-] S ⟩ + merge-with v0? f[v-] S ≡⟨ merge-with-suc v0? f[v-] S ⟩ + merge-with v0?+[f[v-]0?] f[v-]- S- ≡⟨ ≡.cong (λ h → merge-with h f[v-]- S-) ≡f[v]0 ⟩ + merge-with f[v]0? f[v-]- S- ≡⟨ merge-with-cong f[v]0? ≡f[v]- S- ⟩ + merge-with f[v]0? f[v]- S- ≡⟨ merge-suc f[v] S ⟨ + merge f[v] S ∎ + where + f⁻¹[S] : Subset (suc A) + f⁻¹[S] = preimage f S + f⁻¹[S]- : Subset A + f⁻¹[S]- = tail f⁻¹[S] + f⁻¹[S]0 : Bool + f⁻¹[S]0 = head f⁻¹[S] + f[v] : Vector Value (suc B) + f[v] = push v f + f[v]- : Vector Value B + f[v]- = tail f[v] + f[v]0 : Value + f[v]0 = head f[v] + f[v-] : Vector Value (suc B) + f[v-] = push v- f- + f[v-]- : Vector Value B + f[v-]- = tail f[v-] + f[v-]0 : Value + f[v-]0 = head f[v-] + f⁻¹⁅0⁆ : Subset (suc A) + f⁻¹⁅0⁆ = preimage f ⁅ zero ⁆ + f⁻¹⁅0⁆- : Subset A + f⁻¹⁅0⁆- = tail f⁻¹⁅0⁆ + v0? v0?+[f[v-]0?] f[v]0? : Value + v0? = v0 when f⁻¹[S]0 + v0?+[f[v-]0?] = (if S0 then join v0? f[v-]0 else v0?) + f[v]0? = f[v]0 when S0 + open ≡.≡-Reasoning + ≡f[v]0 : v0?+[f[v-]0?] ≡ f[v]0? + ≡f[v]0 rewrite f0≡0 with S0 + ... | true = begin + join v0 (merge v- f⁻¹⁅0⁆-) ≡⟨ join-merge v0 v- (tail (preimage f ⁅ zero ⁆)) ⟩ + merge-with v0 v- f⁻¹⁅0⁆- ≡⟨ ≡.cong (λ h → merge-with (v0 when ⁅ zero ⁆ h) v- f⁻¹⁅0⁆-) f0≡0 ⟨ + merge-with v0?′ v- f⁻¹⁅0⁆- ≡⟨ merge-suc v (preimage f ⁅ zero ⁆) ⟨ + merge v f⁻¹⁅0⁆ ∎ + where + v0?′ : Value + v0?′ = v0 when head f⁻¹⁅0⁆ + ... | false = ≡.refl + ≡f[v]- : f[v-]- ≗ f[v]- + ≡f[v]- x = begin + push v- f- (suc x) ≡⟨ ≡.cong (λ h → merge-with (v0 when ⁅ suc x ⁆ h) v- (preimage f- ⁅ suc x ⁆)) f0≡0 ⟨ + push-with v0?′ v- f- (suc x) ≡⟨ merge-suc v (preimage f ⁅ suc x ⁆) ⟨ + push v f (suc x) ∎ + where + v0?′ : Value + v0?′ = v0 when head (preimage f ⁅ suc x ⁆) diff --git a/Data/Circuit/Value.agda b/Data/Circuit/Value.agda new file mode 100644 index 0000000..512a622 --- /dev/null +++ b/Data/Circuit/Value.agda @@ -0,0 +1,157 @@ +{-# OPTIONS --without-K --safe #-} + +module Data.Circuit.Value where + +open import Relation.Binary.Lattice.Bundles using (BoundedJoinSemilattice) +open import Data.Product.Base using (_×_; _,_) +open import Data.String.Base using (String) +open import Level using (0ℓ) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) + +data Value : Set where + U T F X : Value + +data ≤-Value : Value → Value → Set where + v≤v : {v : Value} → ≤-Value v v + U≤T : ≤-Value U T + U≤F : ≤-Value U F + U≤X : ≤-Value U X + T≤X : ≤-Value T X + F≤X : ≤-Value F X + +≤-reflexive : {x y : Value} → x ≡ y → ≤-Value x y +≤-reflexive ≡.refl = v≤v + +≤-transitive : {i j k : Value} → ≤-Value i j → ≤-Value j k → ≤-Value i k +≤-transitive v≤v y = y +≤-transitive x v≤v = x +≤-transitive U≤T T≤X = U≤X +≤-transitive U≤F F≤X = U≤X + +≤-antisymmetric : {i j : Value} → ≤-Value i j → ≤-Value j i → i ≡ j +≤-antisymmetric v≤v _ = ≡.refl + +showValue : Value → String +showValue U = "U" +showValue T = "T" +showValue F = "F" +showValue X = "X" + +join : Value → Value → Value +join U y = y +join x U = x +join T T = T +join T F = X +join F T = X +join F F = F +join X _ = X +join _ X = X + +≤-supremum + : (x y : Value) + → ≤-Value x (join x y) + × ≤-Value y (join x y) + × ((z : Value) → ≤-Value x z → ≤-Value y z → ≤-Value (join x y) z) +≤-supremum U U = v≤v , v≤v , λ _ U≤z _ → U≤z +≤-supremum U T = U≤T , v≤v , λ { z x≤z y≤z → y≤z } +≤-supremum U F = U≤F , v≤v , λ { z x≤z y≤z → y≤z } +≤-supremum U X = U≤X , v≤v , λ { z x≤z y≤z → y≤z } +≤-supremum T U = v≤v , U≤T , λ { z x≤z y≤z → x≤z } +≤-supremum T T = v≤v , v≤v , λ { z x≤z y≤z → x≤z } +≤-supremum T F = T≤X , F≤X , λ { X x≤z y≤z → v≤v } +≤-supremum T X = T≤X , v≤v , λ { z x≤z y≤z → y≤z } +≤-supremum F U = v≤v , U≤F , λ { z x≤z y≤z → x≤z } +≤-supremum F T = F≤X , T≤X , λ { X x≤z y≤z → v≤v } +≤-supremum F F = v≤v , v≤v , λ { z x≤z y≤z → x≤z } +≤-supremum F X = F≤X , v≤v , λ { z x≤z y≤z → y≤z } +≤-supremum X U = v≤v , U≤X , λ { z x≤z y≤z → x≤z } +≤-supremum X T = v≤v , T≤X , λ { z x≤z y≤z → x≤z } +≤-supremum X F = v≤v , F≤X , λ { z x≤z y≤z → x≤z } +≤-supremum X X = v≤v , v≤v , λ { z x≤z y≤z → x≤z } + +join-comm : (x y : Value) → join x y ≡ join y x +join-comm U U = ≡.refl +join-comm U T = ≡.refl +join-comm U F = ≡.refl +join-comm U X = ≡.refl +join-comm T U = ≡.refl +join-comm T T = ≡.refl +join-comm T F = ≡.refl +join-comm T X = ≡.refl +join-comm F U = ≡.refl +join-comm F T = ≡.refl +join-comm F F = ≡.refl +join-comm F X = ≡.refl +join-comm X U = ≡.refl +join-comm X T = ≡.refl +join-comm X F = ≡.refl +join-comm X X = ≡.refl + +join-assoc : (x y z : Value) → join (join x y) z ≡ join x (join y z) +join-assoc U y z = ≡.refl +join-assoc T U z = ≡.refl +join-assoc T T U = ≡.refl +join-assoc T T T = ≡.refl +join-assoc T T F = ≡.refl +join-assoc T T X = ≡.refl +join-assoc T F U = ≡.refl +join-assoc T F T = ≡.refl +join-assoc T F F = ≡.refl +join-assoc T F X = ≡.refl +join-assoc T X U = ≡.refl +join-assoc T X T = ≡.refl +join-assoc T X F = ≡.refl +join-assoc T X X = ≡.refl +join-assoc F U z = ≡.refl +join-assoc F T U = ≡.refl +join-assoc F T T = ≡.refl +join-assoc F T F = ≡.refl +join-assoc F T X = ≡.refl +join-assoc F F U = ≡.refl +join-assoc F F T = ≡.refl +join-assoc F F F = ≡.refl +join-assoc F F X = ≡.refl +join-assoc F X U = ≡.refl +join-assoc F X T = ≡.refl +join-assoc F X F = ≡.refl +join-assoc F X X = ≡.refl +join-assoc X U z = ≡.refl +join-assoc X T U = ≡.refl +join-assoc X T T = ≡.refl +join-assoc X T F = ≡.refl +join-assoc X T X = ≡.refl +join-assoc X F U = ≡.refl +join-assoc X F T = ≡.refl +join-assoc X F F = ≡.refl +join-assoc X F X = ≡.refl +join-assoc X X U = ≡.refl +join-assoc X X T = ≡.refl +join-assoc X X F = ≡.refl +join-assoc X X X = ≡.refl + +ValueLattice : BoundedJoinSemilattice 0ℓ 0ℓ 0ℓ +ValueLattice = record + { Carrier = Value + ; _≈_ = _≡_ + ; _≤_ = ≤-Value + ; _∨_ = join + ; ⊥ = U + ; isBoundedJoinSemilattice = record + { isJoinSemilattice = record + { isPartialOrder = record + { isPreorder = record + { isEquivalence = ≡.isEquivalence + ; reflexive = ≤-reflexive + ; trans = ≤-transitive + } + ; antisym = ≤-antisymmetric + } + ; supremum = ≤-supremum + } + ; minimum = λ where + U → v≤v + T → U≤T + F → U≤F + X → U≤X + } + } diff --git a/Data/Fin/Preimage.agda b/Data/Fin/Preimage.agda new file mode 100644 index 0000000..4f7ea43 --- /dev/null +++ b/Data/Fin/Preimage.agda @@ -0,0 +1,48 @@ +{-# OPTIONS --without-K --safe #-} + +module Data.Fin.Preimage where + +open import Data.Nat.Base using (ℕ) +open import Data.Fin.Base using (Fin) +open import Function.Base using (∣_⟩-_; _∘_) +open import Relation.Binary.PropositionalEquality as ≡ using (_≗_) +open import Data.Subset.Functional using (Subset; foldl; _∪_; ⊥; ⁅_⁆) + +private + variable A B C : ℕ + +preimage : (Fin A → Fin B) → Subset B → Subset A +preimage f Y = Y ∘ f + +⋃ : Subset A → (Fin A → Subset B) → Subset B +⋃ S f = foldl (∣ _∪_ ⟩- f) ⊥ S + +image : (Fin A → Fin B) → Subset A → Subset B +image f X = ⋃ X (⁅_⁆ ∘ f) + +preimage-cong₁ + : {f g : Fin A → Fin B} + → f ≗ g + → (S : Subset B) + → preimage f S ≗ preimage g S +preimage-cong₁ f≗g S x = ≡.cong S (f≗g x) + +preimage-cong₂ + : (f : Fin A → Fin B) + {S₁ S₂ : Subset B} + → S₁ ≗ S₂ + → preimage f S₁ ≗ preimage f S₂ +preimage-cong₂ f S₁≗S₂ = S₁≗S₂ ∘ f + +preimage-∘ + : (f : Fin A → Fin B) + (g : Fin B → Fin C) + (z : Fin C) + → preimage (g ∘ f) ⁅ z ⁆ ≗ preimage f (preimage g ⁅ z ⁆) +preimage-∘ f g S x = ≡.refl + +preimage-⊥ + : {n m : ℕ} + (f : Fin n → Fin m) + → preimage f ⊥ ≗ ⊥ +preimage-⊥ f x = ≡.refl diff --git a/Data/Setoid.agda b/Data/Setoid.agda new file mode 100644 index 0000000..454d276 --- /dev/null +++ b/Data/Setoid.agda @@ -0,0 +1,8 @@ +{-# OPTIONS --without-K --safe #-} + +module Data.Setoid where + +open import Relation.Binary using (Setoid) +open import Function.Construct.Setoid using () renaming (setoid to infixr 0 _⇒ₛ_) public + +open Setoid renaming (Carrier to ∣_∣) public diff --git a/Data/Subset/Functional.agda b/Data/Subset/Functional.agda new file mode 100644 index 0000000..33a6d8e --- /dev/null +++ b/Data/Subset/Functional.agda @@ -0,0 +1,162 @@ +{-# OPTIONS --without-K --safe #-} + +module Data.Subset.Functional where + +open import Data.Bool.Base using (Bool; _∨_; _∧_; if_then_else_) +open import Data.Bool.Properties using (if-float) +open import Data.Fin.Base using (Fin) +open import Data.Fin.Permutation using (Permutation′; _⟨$⟩ʳ_; _⟨$⟩ˡ_; inverseˡ; inverseʳ) +open import Data.Fin.Properties using (suc-injective; 0≢1+n) +open import Data.Nat.Base using (ℕ) +open import Function.Base using (∣_⟩-_; _∘_) +open import Function.Definitions using (Injective) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_; _≢_) +open import Data.Vector as V using (Vector; head; tail) + +open Bool +open Fin +open ℕ + +Subset : ℕ → Set +Subset = Vector Bool + +private + variable n A : ℕ + variable B C : Set + +⊥ : Subset n +⊥ _ = false + +_∪_ : Subset n → Subset n → Subset n +(A ∪ B) k = A k ∨ B k + +_∩_ : Subset n → Subset n → Subset n +(A ∩ B) k = A k ∧ B k + +⁅_⁆ : Fin n → Subset n +⁅_⁆ zero zero = true +⁅_⁆ zero (suc _) = false +⁅_⁆ (suc k) zero = false +⁅_⁆ (suc k) (suc i) = ⁅ k ⁆ i + +⁅⁆-refl : (k : Fin n) → ⁅ k ⁆ k ≡ true +⁅⁆-refl zero = ≡.refl +⁅⁆-refl (suc k) = ⁅⁆-refl k + +⁅x⁆y≡true + : (x y : Fin n) + → .(⁅ x ⁆ y ≡ true) + → x ≡ y +⁅x⁆y≡true zero zero prf = ≡.refl +⁅x⁆y≡true (suc x) (suc y) prf = ≡.cong suc (⁅x⁆y≡true x y prf) + +⁅x⁆y≡false + : (x y : Fin n) + → .(⁅ x ⁆ y ≡ false) + → x ≢ y +⁅x⁆y≡false zero (suc y) prf = 0≢1+n +⁅x⁆y≡false (suc x) zero prf = 0≢1+n ∘ ≡.sym +⁅x⁆y≡false (suc x) (suc y) prf = ⁅x⁆y≡false x y prf ∘ suc-injective + +f-⁅⁆ + : {n m : ℕ} + (f : Fin n → Fin m) + → Injective _≡_ _≡_ f + → (x y : Fin n) + → ⁅ x ⁆ y ≡ ⁅ f x ⁆ (f y) +f-⁅⁆ f f-inj zero zero = ≡.sym (⁅⁆-refl (f zero)) +f-⁅⁆ f f-inj zero (suc y) with ⁅ f zero ⁆ (f (suc y)) in eq +... | true with () ← f-inj (⁅x⁆y≡true (f zero) (f (suc y)) eq) +... | false = ≡.refl +f-⁅⁆ f f-inj (suc x) zero with ⁅ f (suc x) ⁆ (f zero) in eq +... | true with () ← f-inj (⁅x⁆y≡true (f (suc x)) (f zero) eq) +... | false = ≡.refl +f-⁅⁆ f f-inj (suc x) (suc y) = f-⁅⁆ (f ∘ suc) (suc-injective ∘ f-inj) x y + +⁅⁆∘ρ + : (ρ : Permutation′ (suc n)) + (x : Fin (suc n)) + → ⁅ ρ ⟨$⟩ʳ x ⁆ ≗ ⁅ x ⁆ ∘ (ρ ⟨$⟩ˡ_) +⁅⁆∘ρ {n} ρ x y = begin + ⁅ ρ ⟨$⟩ʳ x ⁆ y ≡⟨ f-⁅⁆ (ρ ⟨$⟩ˡ_) ρˡ-inj (ρ ⟨$⟩ʳ x) y ⟩ + ⁅ ρ ⟨$⟩ˡ (ρ ⟨$⟩ʳ x) ⁆ (ρ ⟨$⟩ˡ y) ≡⟨ ≡.cong (λ h → ⁅ h ⁆ (ρ ⟨$⟩ˡ y)) (inverseˡ ρ) ⟩ + ⁅ x ⁆ (ρ ⟨$⟩ˡ y) ∎ + where + open ≡.≡-Reasoning + ρˡ-inj : {x y : Fin (suc n)} → ρ ⟨$⟩ˡ x ≡ ρ ⟨$⟩ˡ y → x ≡ y + ρˡ-inj {x} {y} ρˡx≡ρˡy = begin + x ≡⟨ inverseʳ ρ ⟨ + ρ ⟨$⟩ʳ (ρ ⟨$⟩ˡ x) ≡⟨ ≡.cong (ρ ⟨$⟩ʳ_) ρˡx≡ρˡy ⟩ + ρ ⟨$⟩ʳ (ρ ⟨$⟩ˡ y) ≡⟨ inverseʳ ρ ⟩ + y ∎ + +opaque + -- TODO dependent fold + foldl : (B → Fin A → B) → B → Subset A → B + foldl {B = B} f = V.foldl (λ _ → B) (λ { {k} acc b → if b then f acc k else acc }) + + foldl-cong₁ + : {f g : B → Fin A → B} + → (∀ x y → f x y ≡ g x y) + → (e : B) + → (S : Subset A) + → foldl f e S ≡ foldl g e S + foldl-cong₁ {B = B} f≗g e S = V.foldl-cong (λ _ → B) (λ { {k} x y → ≡.cong (if y then_else x) (f≗g x k) }) e S + + foldl-cong₂ + : (f : B → Fin A → B) + (e : B) + {S₁ S₂ : Subset A} + → (S₁ ≗ S₂) + → foldl f e S₁ ≡ foldl f e S₂ + foldl-cong₂ {B = B} f e S₁≗S₂ = V.foldl-cong-arg (λ _ → B) (λ {n} acc b → if b then f acc n else acc) e S₁≗S₂ + + foldl-suc + : (f : B → Fin (suc A) → B) + → (e : B) + → (S : Subset (suc A)) + → foldl f e S ≡ foldl (∣ f ⟩- suc) (if head S then f e zero else e) (tail S) + foldl-suc f e S = ≡.refl + + foldl-⊥ + : {A : ℕ} + {B : Set} + (f : B → Fin A → B) + (e : B) + → foldl f e ⊥ ≡ e + foldl-⊥ {zero} _ _ = ≡.refl + foldl-⊥ {suc A} f e = foldl-⊥ (∣ f ⟩- suc) e + + foldl-⁅⁆ + : (f : B → Fin A → B) + (e : B) + (k : Fin A) + → foldl f e ⁅ k ⁆ ≡ f e k + foldl-⁅⁆ f e zero = foldl-⊥ f (f e zero) + foldl-⁅⁆ f e (suc k) = foldl-⁅⁆ (∣ f ⟩- suc) e k + + foldl-fusion + : (h : C → B) + {f : C → Fin A → C} + {g : B → Fin A → B} + → (∀ x n → h (f x n) ≡ g (h x) n) + → (e : C) + → h ∘ foldl f e ≗ foldl g (h e) + foldl-fusion {C = C} {A = A} h {f} {g} fuse e = V.foldl-fusion h ≡.refl fuse′ + where + open ≡.≡-Reasoning + fuse′ + : {k : Fin A} + (acc : C) + (b : Bool) + → h (if b then f acc k else acc) ≡ (if b then g (h acc) k else h acc) + fuse′ {k} acc b = begin + h (if b then f acc k else acc) ≡⟨ if-float h b ⟩ + (if b then h (f acc k) else h acc) ≡⟨ ≡.cong (if b then_else h acc) (fuse acc k) ⟩ + (if b then g (h acc) k else h acc) ∎ + +Subset0≗⊥ : (S : Subset 0) → S ≗ ⊥ +Subset0≗⊥ S () + +foldl-[] : (f : B → Fin 0 → B) (e : B) (S : Subset 0) → foldl f e S ≡ e +foldl-[] f e S = ≡.trans (foldl-cong₂ f e (Subset0≗⊥ S)) (foldl-⊥ f e) diff --git a/Data/System.agda b/Data/System.agda new file mode 100644 index 0000000..0361369 --- /dev/null +++ b/Data/System.agda @@ -0,0 +1,86 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level) + +module Data.System {ℓ : Level} where + +import Function.Construct.Identity as Id +import Relation.Binary.Properties.Preorder as PreorderProperties + +open import Data.Circuit.Value using (Value) +open import Data.Nat.Base using (ℕ) +open import Data.Setoid using (_⇒ₛ_; ∣_∣) +open import Data.System.Values Value using (Values; _≋_; module ≋) +open import Level using (Level; _⊔_; 0ℓ; suc) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) +open import Relation.Binary using (Reflexive; Transitive; Preorder; _⇒_; Setoid) +open import Function.Base using (_∘_) +open import Function.Bundles using (Func; _⟨$⟩_) +open import Function.Construct.Setoid using (_∙_) + +open Func + +record System (n : ℕ) : Set (suc ℓ) where + + field + S : Setoid ℓ ℓ + fₛ : ∣ Values n ⇒ₛ S ⇒ₛ S ∣ + fₒ : ∣ S ⇒ₛ Values n ∣ + + fₛ′ : ∣ Values n ∣ → ∣ S ∣ → ∣ S ∣ + fₛ′ = to ∘ to fₛ + + fₒ′ : ∣ S ∣ → ∣ Values n ∣ + fₒ′ = to fₒ + + open Setoid S public + +module _ {n : ℕ} where + + record ≤-System (a b : System n) : Set ℓ where + module A = System a + module B = System b + field + ⇒S : ∣ A.S ⇒ₛ B.S ∣ + ≗-fₛ + : (i : ∣ Values n ∣) (s : ∣ A.S ∣) + → ⇒S ⟨$⟩ (A.fₛ′ i s) B.≈ B.fₛ′ i (⇒S ⟨$⟩ s) + ≗-fₒ + : (s : ∣ A.S ∣) + → A.fₒ′ s ≋ B.fₒ′ (⇒S ⟨$⟩ s) + + open ≤-System + + ≤-refl : Reflexive ≤-System + ⇒S ≤-refl = Id.function _ + ≗-fₛ (≤-refl {x}) _ _ = System.refl x + ≗-fₒ (≤-refl {x}) _ = ≋.refl + + ≡⇒≤ : _≡_ ⇒ ≤-System + ≡⇒≤ ≡.refl = ≤-refl + + open System + + ≤-trans : Transitive ≤-System + ⇒S (≤-trans a b) = ⇒S b ∙ ⇒S a + ≗-fₛ (≤-trans {x} {y} {z} a b) i s = System.trans z (cong (⇒S b) (≗-fₛ a i s)) (≗-fₛ b i (⇒S a ⟨$⟩ s)) + ≗-fₒ (≤-trans a b) s = ≋.trans (≗-fₒ a s) (≗-fₒ b (⇒S a ⟨$⟩ s)) + + System-Preorder : Preorder (suc ℓ) (suc ℓ) ℓ + System-Preorder = record + { Carrier = System n + ; _≈_ = _≡_ + ; _≲_ = ≤-System + ; isPreorder = record + { isEquivalence = ≡.isEquivalence + ; reflexive = ≡⇒≤ + ; trans = ≤-trans + } + } + +module _ (n : ℕ) where + + open PreorderProperties (System-Preorder {n}) using (InducedEquivalence) + + Systemₛ : Setoid (suc ℓ) ℓ + Systemₛ = InducedEquivalence diff --git a/Data/System/Values.agda b/Data/System/Values.agda new file mode 100644 index 0000000..bf8fa38 --- /dev/null +++ b/Data/System/Values.agda @@ -0,0 +1,21 @@ +{-# OPTIONS --without-K --safe #-} + +module Data.System.Values (A : Set) where + +open import Data.Nat.Base using (ℕ) +open import Data.Vec.Functional using (Vector) +open import Level using (0ℓ) +open import Relation.Binary using (Rel; Setoid) +open import Data.Vec.Functional.Relation.Binary.Equality.Setoid using (≋-setoid) + +import Relation.Binary.PropositionalEquality as ≡ + +Values : ℕ → Setoid 0ℓ 0ℓ +Values = ≋-setoid (≡.setoid A) + +_≋_ : {n : ℕ} → Rel (Vector A n) 0ℓ +_≋_ {n} = Setoid._≈_ (Values n) + +infix 4 _≋_ + +module ≋ {n : ℕ} = Setoid (Values n) diff --git a/Data/Vector.agda b/Data/Vector.agda new file mode 100644 index 0000000..052f624 --- /dev/null +++ b/Data/Vector.agda @@ -0,0 +1,82 @@ +{-# OPTIONS --without-K --safe #-} + +module Data.Vector where + +open import Data.Nat.Base using (ℕ) +open import Data.Vec.Functional using (Vector; head; tail; []; removeAt; map) public +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_) +open import Function.Base using (∣_⟩-_; _∘_) +open import Data.Fin.Base using (Fin; toℕ) +open ℕ +open Fin + +foldl + : ∀ {n : ℕ} {A : Set} (B : ℕ → Set) + → (∀ {k : Fin n} → B (toℕ k) → A → B (suc (toℕ k))) + → B zero + → Vector A n + → B n +foldl {zero} B ⊕ e v = e +foldl {suc n} B ⊕ e v = foldl (B ∘ suc) ⊕ (⊕ e (head v)) (tail v) + +foldl-cong + : {n : ℕ} {A : Set} + (B : ℕ → Set) + {f g : ∀ {k : Fin n} → B (toℕ k) → A → B (suc (toℕ k))} + → (∀ {k} → ∀ x y → f {k} x y ≡ g {k} x y) + → (e : B zero) + → (v : Vector A n) + → foldl B f e v ≡ foldl B g e v +foldl-cong {zero} B f≗g e v = ≡.refl +foldl-cong {suc n} B {g = g} f≗g e v rewrite (f≗g e (head v)) = foldl-cong (B ∘ suc) f≗g (g e (head v)) (tail v) + +foldl-cong-arg + : {n : ℕ} {A : Set} + (B : ℕ → Set) + (f : ∀ {k : Fin n} → B (toℕ k) → A → B (suc (toℕ k))) + → (e : B zero) + → {v w : Vector A n} + → v ≗ w + → foldl B f e v ≡ foldl B f e w +foldl-cong-arg {zero} B f e v≗w = ≡.refl +foldl-cong-arg {suc n} B f e {w = w} v≗w rewrite v≗w zero = foldl-cong-arg (B ∘ suc) f (f e (head w)) (v≗w ∘ suc) + +foldl-map + : {n : ℕ} {A : ℕ → Set} {B C : Set} + (f : ∀ {k : Fin n} → A (toℕ k) → B → A (suc (toℕ k))) + (g : C → B) + (x : A zero) + (xs : Vector C n) + → foldl A f x (map g xs) + ≡ foldl A (∣ f ⟩- g) x xs +foldl-map {zero} f g e xs = ≡.refl +foldl-map {suc n} f g e xs = foldl-map f g (f e (g (head xs))) (tail xs) + +foldl-fusion + : {n : ℕ} + {A : Set} {B C : ℕ → Set} + (h : {k : ℕ} → B k → C k) + → {f : {k : Fin n} → B (toℕ k) → A → B (suc (toℕ k))} {d : B zero} + → {g : {k : Fin n} → C (toℕ k) → A → C (suc (toℕ k))} {e : C zero} + → (h d ≡ e) + → ({k : Fin n} (b : B (toℕ k)) (x : A) → h (f {k} b x) ≡ g (h b) x) + → h ∘ foldl B f d ≗ foldl C g e +foldl-fusion {zero} _ base _ _ = base +foldl-fusion {suc n} {A} h {f} {d} {g} {e} base fuse xs = foldl-fusion h eq fuse (tail xs) + where + x₀ : A + x₀ = head xs + open ≡.≡-Reasoning + eq : h (f d x₀) ≡ g e x₀ + eq = begin + h (f d x₀) ≡⟨ fuse d x₀ ⟩ + g (h d) x₀ ≡⟨ ≡.cong-app (≡.cong g base) x₀ ⟩ + g e x₀ ∎ + +foldl-[] + : {A : Set} + (B : ℕ → Set) + (f : {k : Fin 0} → B (toℕ k) → A → B (suc (toℕ k))) + {e : B 0} + → foldl B f e [] ≡ e +foldl-[] _ _ = ≡.refl diff --git a/Functor/Instance/Decorate.agda b/Functor/Instance/Decorate.agda index e87f20c..30cec87 100644 --- a/Functor/Instance/Decorate.agda +++ b/Functor/Instance/Decorate.agda @@ -40,7 +40,7 @@ module DecoratedCospans = Category DecoratedCospans module mc𝒞 = CocartesianMonoidal 𝒞.U 𝒞.cocartesian -- For every cospan there exists a free decorated cospan --- i.e. the original cospan with the empty decoration +-- i.e. the original cospan with the discrete decoration private variable diff --git a/Functor/Instance/Nat/Preimage.agda b/Functor/Instance/Nat/Preimage.agda new file mode 100644 index 0000000..7da00f4 --- /dev/null +++ b/Functor/Instance/Nat/Preimage.agda @@ -0,0 +1,65 @@ +{-# OPTIONS --without-K --safe #-} + +module Functor.Instance.Nat.Preimage where + +open import Categories.Category.Instance.Nat using (Natop) +open import Categories.Category.Instance.Setoids using (Setoids) +open import Categories.Functor using (Functor) +open import Data.Fin.Base using (Fin) +open import Data.Bool.Base using (Bool) +open import Data.Nat.Base using (ℕ) +open import Data.Subset.Functional using (Subset) +open import Data.Vec.Functional.Relation.Binary.Equality.Setoid using (≋-setoid) +open import Function.Base using (id; _∘_) +open import Function.Bundles using (Func; _⟶ₛ_) +open import Function.Construct.Identity using () renaming (function to Id) +open import Function.Construct.Setoid using (setoid; _∙_) +open import Level using (0ℓ) +open import Relation.Binary using (Rel; Setoid) +open import Relation.Binary.PropositionalEquality as ≡ using (_≗_) + +open Functor +open Func + +_≈_ : {X Y : Setoid 0ℓ 0ℓ} → Rel (X ⟶ₛ Y) 0ℓ +_≈_ {X} {Y} = Setoid._≈_ (setoid X Y) +infixr 4 _≈_ + +private + variable A B C : ℕ + +-- action on objects (Subset n) +Subsetₛ : ℕ → Setoid 0ℓ 0ℓ +Subsetₛ = ≋-setoid (≡.setoid Bool) + +-- action of Preimage on morphisms (contravariant) +Preimage₁ : (Fin A → Fin B) → Subsetₛ B ⟶ₛ Subsetₛ A +to (Preimage₁ f) i = i ∘ f +cong (Preimage₁ f) x≗y = x≗y ∘ f + +-- Preimage respects identity +Preimage-identity : Preimage₁ id ≈ Id (Subsetₛ A) +Preimage-identity {A} = Setoid.refl (Subsetₛ A) + +-- Preimage flips composition +Preimage-homomorphism + : {A B C : ℕ} + (f : Fin A → Fin B) + (g : Fin B → Fin C) + → Preimage₁ (g ∘ f) ≈ Preimage₁ f ∙ Preimage₁ g +Preimage-homomorphism {A} _ _ = Setoid.refl (Subsetₛ A) + +-- Preimage respects equality +Preimage-resp-≈ + : {f g : Fin A → Fin B} + → f ≗ g + → Preimage₁ f ≈ Preimage₁ g +Preimage-resp-≈ f≗g {v} = ≡.cong v ∘ f≗g + +-- the Preimage functor +Preimage : Functor Natop (Setoids 0ℓ 0ℓ) +F₀ Preimage = Subsetₛ +F₁ Preimage = Preimage₁ +identity Preimage = Preimage-identity +homomorphism Preimage {f = f} {g} {v} = Preimage-homomorphism g f {v} +F-resp-≈ Preimage = Preimage-resp-≈ diff --git a/Functor/Instance/Nat/Pull.agda b/Functor/Instance/Nat/Pull.agda new file mode 100644 index 0000000..5b74399 --- /dev/null +++ b/Functor/Instance/Nat/Pull.agda @@ -0,0 +1,63 @@ +{-# OPTIONS --without-K --safe #-} + +module Functor.Instance.Nat.Pull where + +open import Categories.Category.Instance.Nat using (Natop) +open import Categories.Category.Instance.Setoids using (Setoids) +open import Categories.Functor using (Functor) +open import Data.Fin.Base using (Fin) +open import Data.Nat.Base using (ℕ) +open import Function.Base using (id; _∘_) +open import Function.Bundles using (Func; _⟶ₛ_) +open import Function.Construct.Identity using () renaming (function to Id) +open import Function.Construct.Setoid using (setoid; _∙_) +open import Level using (0ℓ) +open import Relation.Binary using (Rel; Setoid) +open import Relation.Binary.PropositionalEquality as ≡ using (_≗_) +open import Data.Circuit.Value using (Value) +open import Data.System.Values Value using (Values) + +open Functor +open Func + +_≈_ : {X Y : Setoid 0ℓ 0ℓ} → Rel (X ⟶ₛ Y) 0ℓ +_≈_ {X} {Y} = Setoid._≈_ (setoid X Y) +infixr 4 _≈_ + +private + variable A B C : ℕ + + +-- action on objects is Values n (Vector Value n) + +-- action of Pull on morphisms (contravariant) +Pull₁ : (Fin A → Fin B) → Values B ⟶ₛ Values A +to (Pull₁ f) i = i ∘ f +cong (Pull₁ f) x≗y = x≗y ∘ f + +-- Pull respects identity +Pull-identity : Pull₁ id ≈ Id (Values A) +Pull-identity {A} = Setoid.refl (Values A) + +-- Pull flips composition +Pull-homomorphism + : {A B C : ℕ} + (f : Fin A → Fin B) + (g : Fin B → Fin C) + → Pull₁ (g ∘ f) ≈ Pull₁ f ∙ Pull₁ g +Pull-homomorphism {A} _ _ = Setoid.refl (Values A) + +-- Pull respects equality +Pull-resp-≈ + : {f g : Fin A → Fin B} + → f ≗ g + → Pull₁ f ≈ Pull₁ g +Pull-resp-≈ f≗g {v} = ≡.cong v ∘ f≗g + +-- the Pull functor +Pull : Functor Natop (Setoids 0ℓ 0ℓ) +F₀ Pull = Values +F₁ Pull = Pull₁ +identity Pull = Pull-identity +homomorphism Pull {f = f} {g} {v} = Pull-homomorphism g f {v} +F-resp-≈ Pull = Pull-resp-≈ diff --git a/Functor/Instance/Nat/Push.agda b/Functor/Instance/Nat/Push.agda new file mode 100644 index 0000000..53d0bef --- /dev/null +++ b/Functor/Instance/Nat/Push.agda @@ -0,0 +1,64 @@ +{-# OPTIONS --without-K --safe #-} + +module Functor.Instance.Nat.Push where + +open import Categories.Functor using (Functor) +open import Categories.Category.Instance.Nat using (Nat) +open import Categories.Category.Instance.Setoids using (Setoids) +open import Data.Circuit.Merge using (merge; merge-cong₁; merge-cong₂; merge-⁅⁆; merge-preimage) +open import Data.Fin.Base using (Fin) +open import Data.Fin.Preimage using (preimage; preimage-cong₁) +open import Data.Nat.Base using (ℕ) +open import Data.Subset.Functional using (⁅_⁆) +open import Function.Base using (id; _∘_) +open import Function.Bundles using (Func; _⟶ₛ_) +open import Function.Construct.Identity using () renaming (function to Id) +open import Function.Construct.Setoid using (setoid; _∙_) +open import Level using (0ℓ) +open import Relation.Binary using (Rel; Setoid) +open import Relation.Binary.PropositionalEquality as ≡ using (_≗_) +open import Data.Circuit.Value using (Value) +open import Data.System.Values Value using (Values) + +open Func +open Functor + +private + variable A B C : ℕ + +_≈_ : {X Y : Setoid 0ℓ 0ℓ} → Rel (X ⟶ₛ Y) 0ℓ +_≈_ {X} {Y} = Setoid._≈_ (setoid X Y) +infixr 4 _≈_ + +-- action of Push on objects is Values n (Vector Value n) + +-- action of Push on morphisms (covariant) +Push₁ : (Fin A → Fin B) → Values A ⟶ₛ Values B +to (Push₁ f) v = merge v ∘ preimage f ∘ ⁅_⁆ +cong (Push₁ f) x≗y = merge-cong₁ x≗y ∘ preimage f ∘ ⁅_⁆ + +-- Push respects identity +Push-identity : Push₁ id ≈ Id (Values A) +Push-identity {_} {v} = merge-⁅⁆ v + +-- Push respects composition +Push-homomorphism + : {f : Fin A → Fin B} + {g : Fin B → Fin C} + → Push₁ (g ∘ f) ≈ Push₁ g ∙ Push₁ f +Push-homomorphism {f = f} {g} {v} = merge-preimage f v ∘ preimage g ∘ ⁅_⁆ + +-- Push respects equality +Push-resp-≈ + : {f g : Fin A → Fin B} + → f ≗ g + → Push₁ f ≈ Push₁ g +Push-resp-≈ f≗g {v} = merge-cong₂ v ∘ preimage-cong₁ f≗g ∘ ⁅_⁆ + +-- the Push functor +Push : Functor Nat (Setoids 0ℓ 0ℓ) +F₀ Push = Values +F₁ Push = Push₁ +identity Push = Push-identity +homomorphism Push = Push-homomorphism +F-resp-≈ Push = Push-resp-≈ diff --git a/Functor/Instance/Nat/System.agda b/Functor/Instance/Nat/System.agda new file mode 100644 index 0000000..730f90d --- /dev/null +++ b/Functor/Instance/Nat/System.agda @@ -0,0 +1,96 @@ +{-# OPTIONS --without-K --safe #-} + +module Functor.Instance.Nat.System {ℓ} where + +open import Categories.Category.Instance.Nat using (Nat) +open import Categories.Category.Instance.Setoids using (Setoids) +open import Categories.Functor.Core using (Functor) +open import Data.Circuit.Value using (Value) +open import Data.Fin.Base using (Fin) +open import Data.Nat.Base using (ℕ) +open import Data.Product.Base using (_,_; _×_) +open import Data.System using (System; ≤-System; Systemₛ) +open import Data.System.Values Value using (module ≋) +open import Function.Bundles using (Func; _⟶ₛ_) +open import Function.Base using (id; _∘_) +open import Function.Construct.Setoid using (_∙_) +open import Functor.Instance.Nat.Pull using (Pull₁; Pull-resp-≈) +open import Functor.Instance.Nat.Push using (Push₁; Push-identity; Push-homomorphism; Push-resp-≈) +open import Level using (suc) +open import Relation.Binary.PropositionalEquality as ≡ using (_≗_) + +-- import Relation.Binary.Reasoning.Setoid as ≈-Reasoning +import Function.Construct.Identity as Id + +open Func +open ≤-System +open Functor + +private + variable A B C : ℕ + +map : (Fin A → Fin B) → System {ℓ} A → System B +map f X = record + { S = S + ; fₛ = fₛ ∙ Pull₁ f + ; fₒ = Push₁ f ∙ fₒ + } + where + open System X + +≤-cong : (f : Fin A → Fin B) {X Y : System A} → ≤-System Y X → ≤-System (map f Y) (map f X) +⇒S (≤-cong f x≤y) = ⇒S x≤y +≗-fₛ (≤-cong f x≤y) = ≗-fₛ x≤y ∘ to (Pull₁ f) +≗-fₒ (≤-cong f x≤y) = cong (Push₁ f) ∘ ≗-fₒ x≤y + +System₁ : (Fin A → Fin B) → Systemₛ A ⟶ₛ Systemₛ B +to (System₁ f) = map f +cong (System₁ f) (x≤y , y≤x) = ≤-cong f x≤y , ≤-cong f y≤x + +id-x≤x : {X : System A} → ≤-System (map id X) X +⇒S (id-x≤x) = Id.function _ +≗-fₛ (id-x≤x {_} {x}) i s = System.refl x +≗-fₒ (id-x≤x {A} {x}) s = Push-identity + +x≤id-x : {x : System A} → ≤-System x (map id x) +⇒S x≤id-x = Id.function _ +≗-fₛ (x≤id-x {A} {x}) i s = System.refl x +≗-fₒ (x≤id-x {A} {x}) s = ≋.sym Push-identity + + +System-homomorphism + : {f : Fin A → Fin B} + {g : Fin B → Fin C} + {X : System A} + → ≤-System (map (g ∘ f) X) (map g (map f X)) × ≤-System (map g (map f X)) (map (g ∘ f) X) +System-homomorphism {f = f} {g} {X} = left , right + where + open System X + left : ≤-System (map (g ∘ f) X) (map g (map f X)) + left .⇒S = Id.function S + left .≗-fₛ i s = refl + left .≗-fₒ s = Push-homomorphism + right : ≤-System (map g (map f X)) (map (g ∘ f) X) + right .⇒S = Id.function S + right .≗-fₛ i s = refl + right .≗-fₒ s = ≋.sym Push-homomorphism + +System-resp-≈ + : {f g : Fin A → Fin B} + → f ≗ g + → {X : System A} + → (≤-System (map f X) (map g X)) × (≤-System (map g X) (map f X)) +System-resp-≈ {A} {B} {f = f} {g} f≗g {X} = both f≗g , both (≡.sym ∘ f≗g) + where + open System X + both : {f g : Fin A → Fin B} → f ≗ g → ≤-System (map f X) (map g X) + both f≗g .⇒S = Id.function S + both f≗g .≗-fₛ i s = cong fₛ (Pull-resp-≈ f≗g {i}) + both {f} {g} f≗g .≗-fₒ s = Push-resp-≈ f≗g + +Sys : Functor Nat (Setoids (suc ℓ) ℓ) +Sys .F₀ = Systemₛ +Sys .F₁ = System₁ +Sys .identity = id-x≤x , x≤id-x +Sys .homomorphism {x = X} = System-homomorphism {X = X} +Sys .F-resp-≈ = System-resp-≈ diff --git a/Functor/Monoidal/Braided/Strong/Properties.agda b/Functor/Monoidal/Braided/Strong/Properties.agda new file mode 100644 index 0000000..66dc4c0 --- /dev/null +++ b/Functor/Monoidal/Braided/Strong/Properties.agda @@ -0,0 +1,59 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level) +open import Categories.Category.Monoidal using (BraidedMonoidalCategory) +open import Categories.Functor.Monoidal.Braided using (module Strong) +open Strong using (BraidedMonoidalFunctor) + +module Functor.Monoidal.Braided.Strong.Properties + {o o′ ℓ ℓ′ e e′ : Level} + {C : BraidedMonoidalCategory o ℓ e} + {D : BraidedMonoidalCategory o′ ℓ′ e′} + (F,φ,ε : BraidedMonoidalFunctor C D) where + +import Categories.Category.Construction.Core as Core +import Categories.Category.Monoidal.Utilities as ⊗-Utilities +import Functor.Monoidal.Strong.Properties as MonoidalProp + +open import Categories.Functor.Properties using ([_]-resp-≅) + +private + + module C = BraidedMonoidalCategory C + module D = BraidedMonoidalCategory D + +open D +open Core.Shorthands U using (_∘ᵢ_; idᵢ; _≈ᵢ_; ⌞_⌟; to-≈; _≅_; module HomReasoningᵢ) +open ⊗-Utilities monoidal using (_⊗ᵢ_) +open BraidedMonoidalFunctor F,φ,ε +open MonoidalProp monoidalFunctor public + +private + + variable + A B : Obj + X Y : C.Obj + + σ : A ⊗₀ B ≅ B ⊗₀ A + σ = braiding.FX≅GX + + σ⇐ : B ⊗₀ A ⇒ A ⊗₀ B + σ⇐ = braiding.⇐.η _ + + Fσ : F₀ (X C.⊗₀ Y) ≅ F₀ (Y C.⊗₀ X) + Fσ = [ F ]-resp-≅ C.braiding.FX≅GX + + Fσ⇐ : F₀ (Y C.⊗₀ X) ⇒ F₀ (X C.⊗₀ Y) + Fσ⇐ = F₁ (C.braiding.⇐.η _) + + φ : F₀ X ⊗₀ F₀ Y ≅ F₀ (X C.⊗₀ Y) + φ = ⊗-homo.FX≅GX + +open HomReasoning +open Shorthands using (φ⇐) + +braiding-compatᵢ : Fσ {X} {Y} ∘ᵢ φ ≈ᵢ φ ∘ᵢ σ +braiding-compatᵢ = ⌞ braiding-compat ⌟ + +braiding-compat-inv : φ⇐ ∘ Fσ⇐ {X} {Y} ≈ σ⇐ ∘ φ⇐ +braiding-compat-inv = to-≈ braiding-compatᵢ diff --git a/Functor/Monoidal/Instance/Nat/Preimage.agda b/Functor/Monoidal/Instance/Nat/Preimage.agda new file mode 100644 index 0000000..59c9391 --- /dev/null +++ b/Functor/Monoidal/Instance/Nat/Preimage.agda @@ -0,0 +1,164 @@ +{-# OPTIONS --without-K --safe #-} + +module Functor.Monoidal.Instance.Nat.Preimage where + +open import Category.Monoidal.Instance.Nat using (Natop,+,0; Natop-Cartesian) +open import Categories.Category.Instance.Nat using (Nat-Cocartesian) +open import Categories.Category.Instance.SingletonSet using (SingletonSetoid) +open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) +open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian) +open import Categories.Category.BinaryProducts using (module BinaryProducts) +open import Categories.Category.Cartesian using (Cartesian) +open import Categories.Category.Cocartesian using (Cocartesian; BinaryCoproducts) +open import Categories.Category.Product using (_⁂_) +open import Categories.Functor using (_∘F_) +open import Data.Subset.Functional using (Subset) +open import Data.Nat.Base using (ℕ; _+_) +open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_) +open import Data.Product.Base using (_,_; _×_; Σ) +open import Data.Vec.Functional using ([]; _++_) +open import Data.Vec.Functional.Properties using (++-cong) +open import Data.Vec.Functional using (Vector; []) +open import Function.Bundles using (Func; _⟶ₛ_) +open import Functor.Instance.Nat.Preimage using (Preimage; Subsetₛ) +open import Level using (0ℓ) + +open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using (products) +open BinaryProducts products using (-×-) +open Cocartesian Nat-Cocartesian using (module Dual; _+₁_; +-assocʳ; +-swap; +₁∘+-swap) +open Dual.op-binaryProducts using () renaming (-×- to -+-; assocˡ∘⟨⟩ to []∘assocʳ; swap∘⟨⟩ to []∘swap) + +open import Data.Fin.Base using (Fin; splitAt; join; _↑ˡ_; _↑ʳ_) +open import Data.Fin.Properties using (splitAt-join; splitAt-↑ˡ) +open import Data.Sum.Base using ([_,_]′; map; map₁; map₂; inj₁; inj₂) +open import Data.Sum.Properties using ([,]-map; [,]-cong; [-,]-cong; [,-]-cong; [,]-∘) +open import Data.Fin.Preimage using (preimage) +open import Function.Base using (_∘_; id) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_; module ≡-Reasoning) +open import Data.Bool.Base using (Bool) + +open Func +Preimage-ε : SingletonSetoid {0ℓ} {0ℓ} ⟶ₛ Subsetₛ 0 +to Preimage-ε x = [] +cong Preimage-ε x () + +++ₛ : {n m : ℕ} → Subsetₛ n ×ₛ Subsetₛ m ⟶ₛ Subsetₛ (n + m) +to ++ₛ (xs , ys) = xs ++ ys +cong ++ₛ (≗xs , ≗ys) = ++-cong _ _ ≗xs ≗ys + +preimage-++ + : {n n′ m m′ : ℕ} + (f : Fin n → Fin n′) + (g : Fin m → Fin m′) + {xs : Subset n′} + {ys : Subset m′} + → preimage f xs ++ preimage g ys ≗ preimage (f +₁ g) (xs ++ ys) +preimage-++ {n} {n′} {m} {m′} f g {xs} {ys} e = begin + (xs ∘ f ++ ys ∘ g) e ≡⟨ [,]-map (splitAt n e) ⟨ + [ xs , ys ]′ (map f g (splitAt n e)) ≡⟨ ≡.cong [ xs , ys ]′ (splitAt-join n′ m′ (map f g (splitAt n e))) ⟨ + [ xs , ys ]′ (splitAt n′ (join n′ m′ (map f g (splitAt n e)))) ≡⟨ ≡.cong ([ xs , ys ]′ ∘ splitAt n′) ([,]-map (splitAt n e)) ⟩ + [ xs , ys ]′ (splitAt n′ ((f +₁ g) e)) ∎ + where + open ≡-Reasoning + +⊗-homomorphism : NaturalTransformation (-×- ∘F (Preimage ⁂ Preimage)) (Preimage ∘F -+-) +⊗-homomorphism = ntHelper record + { η = λ (n , m) → ++ₛ {n} {m} + ; commute = λ { {n′ , m′} {n , m} (f , g) {xs , ys} e → preimage-++ f g e } + } + +open import Category.Instance.Setoids.SymmetricMonoidal {0ℓ} {0ℓ} using (Setoids-×) +open import Categories.Functor.Monoidal.Symmetric Natop,+,0 Setoids-× using (module Lax) +open Lax using (SymmetricMonoidalFunctor) + +++-assoc + : {m n o : ℕ} + (X : Subset m) + (Y : Subset n) + (Z : Subset o) + → ((X ++ Y) ++ Z) ∘ +-assocʳ {m} ≗ X ++ (Y ++ Z) +++-assoc {m} {n} {o} X Y Z i = begin + ((X ++ Y) ++ Z) (+-assocʳ {m} i) ≡⟨⟩ + [ [ X , Y ]′ ∘ splitAt m , Z ]′ (splitAt (m + n) (+-assocʳ {m} i)) ≡⟨ [,]-cong ([,]-cong (inv ∘ X) (inv ∘ Y) ∘ splitAt m) (inv ∘ Z) (splitAt (m + n) (+-assocʳ {m} i)) ⟨ + [ [ b ∘ X′ , b ∘ Y′ ]′ ∘ splitAt m , b ∘ Z′ ]′ (splitAt _ (+-assocʳ {m} i)) ≡⟨ [-,]-cong ([,]-∘ b ∘ splitAt m) (splitAt (m + n) (+-assocʳ {m} i)) ⟨ + [ b ∘ [ X′ , Y′ ]′ ∘ splitAt m , b ∘ Z′ ]′ (splitAt _ (+-assocʳ {m} i)) ≡⟨ [,]-∘ b (splitAt (m + n) (+-assocʳ {m} i)) ⟨ + b ([ [ X′ , Y′ ]′ ∘ splitAt m , Z′ ]′ (splitAt _ (+-assocʳ {m} i))) ≡⟨ ≡.cong b ([]∘assocʳ {2} {m} i) ⟩ + b ([ X′ , [ Y′ , Z′ ]′ ∘ splitAt n ]′ (splitAt m i)) ≡⟨ [,]-∘ b (splitAt m i) ⟩ + [ b ∘ X′ , b ∘ [ Y′ , Z′ ]′ ∘ splitAt n ]′ (splitAt m i) ≡⟨ [,-]-cong ([,]-∘ b ∘ splitAt n) (splitAt m i) ⟩ + [ b ∘ X′ , [ b ∘ Y′ , b ∘ Z′ ]′ ∘ splitAt n ]′ (splitAt m i) ≡⟨ [,]-cong (inv ∘ X) ([,]-cong (inv ∘ Y) (inv ∘ Z) ∘ splitAt n) (splitAt m i) ⟩ + [ X , [ Y , Z ]′ ∘ splitAt n ]′ (splitAt m i) ≡⟨⟩ + (X ++ (Y ++ Z)) i ∎ + where + open Bool + open Fin + f : Bool → Fin 2 + f false = zero + f true = suc zero + b : Fin 2 → Bool + b zero = false + b (suc zero) = true + inv : b ∘ f ≗ id + inv false = ≡.refl + inv true = ≡.refl + X′ : Fin m → Fin 2 + X′ = f ∘ X + Y′ : Fin n → Fin 2 + Y′ = f ∘ Y + Z′ : Fin o → Fin 2 + Z′ = f ∘ Z + open ≡-Reasoning + +Preimage-unitaryˡ + : {n : ℕ} + (X : Subset n) + → (X ++ []) ∘ (_↑ˡ 0) ≗ X +Preimage-unitaryˡ {n} X i = begin + [ X , [] ]′ (splitAt _ (i ↑ˡ 0)) ≡⟨ ≡.cong ([ X , [] ]′) (splitAt-↑ˡ n i 0) ⟩ + [ X , [] ]′ (inj₁ i) ≡⟨⟩ + X i ∎ + where + open ≡-Reasoning + +++-swap + : {n m : ℕ} + (X : Subset n) + (Y : Subset m) + → (X ++ Y) ∘ +-swap {n} ≗ Y ++ X +++-swap {n} {m} X Y i = begin + [ X , Y ]′ (splitAt n (+-swap {n} i)) ≡⟨ [,]-cong (inv ∘ X) (inv ∘ Y) (splitAt n (+-swap {n} i)) ⟨ + [ b ∘ X′ , b ∘ Y′ ]′ (splitAt n (+-swap {n} i)) ≡⟨ [,]-∘ b (splitAt n (+-swap {n} i)) ⟨ + b ([ X′ , Y′ ]′ (splitAt n (+-swap {n} i))) ≡⟨ ≡.cong b ([]∘swap {2} {n} i) ⟩ + b ([ Y′ , X′ ]′ (splitAt m i)) ≡⟨ [,]-∘ b (splitAt m i) ⟩ + [ b ∘ Y′ , b ∘ X′ ]′ (splitAt m i) ≡⟨ [,]-cong (inv ∘ Y) (inv ∘ X) (splitAt m i) ⟩ + [ Y , X ]′ (splitAt m i) ∎ + where + open Bool + open Fin + f : Bool → Fin 2 + f false = zero + f true = suc zero + b : Fin 2 → Bool + b zero = false + b (suc zero) = true + inv : b ∘ f ≗ id + inv false = ≡.refl + inv true = ≡.refl + X′ : Fin n → Fin 2 + X′ = f ∘ X + Y′ : Fin m → Fin 2 + Y′ = f ∘ Y + open ≡-Reasoning + +open SymmetricMonoidalFunctor +Preimage,++,[] : SymmetricMonoidalFunctor +Preimage,++,[] .F = Preimage +Preimage,++,[] .isBraidedMonoidal = record + { isMonoidal = record + { ε = Preimage-ε + ; ⊗-homo = ⊗-homomorphism + ; associativity = λ { {m} {n} {o} {(X , Y) , Z} i → ++-assoc X Y Z i } + ; unitaryˡ = λ _ → ≡.refl + ; unitaryʳ = λ { {n} {X , _} i → Preimage-unitaryˡ X i } + } + ; braiding-compat = λ { {n} {m} {X , Y} i → ++-swap X Y i } + } diff --git a/Functor/Monoidal/Instance/Nat/Pull.agda b/Functor/Monoidal/Instance/Nat/Pull.agda new file mode 100644 index 0000000..c2b6958 --- /dev/null +++ b/Functor/Monoidal/Instance/Nat/Pull.agda @@ -0,0 +1,192 @@ +{-# OPTIONS --without-K --safe #-} + +module Functor.Monoidal.Instance.Nat.Pull where + +open import Category.Monoidal.Instance.Nat using (Natop,+,0; Natop-Cartesian) +open import Categories.Category.Instance.Nat using (Nat-Cocartesian) +open import Categories.Category.Instance.SingletonSet using (SingletonSetoid) +open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) +open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism; niHelper) +open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian) +open import Categories.Category.BinaryProducts using (module BinaryProducts) +open import Categories.Category.Cartesian using (Cartesian) +open import Categories.Category.Cocartesian using (Cocartesian; BinaryCoproducts) +open import Categories.Category.Product using (_⁂_) +open import Categories.Functor using (_∘F_) +open import Data.Subset.Functional using (Subset) +open import Data.Nat.Base using (ℕ; _+_) +open import Relation.Binary using (Setoid) +open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_) +open import Data.Product.Base using (_,_; _×_; Σ) +open import Data.Vec.Functional using ([]; _++_) +open import Data.Vec.Functional.Properties using (++-cong) +open import Data.Vec.Functional using (Vector; []) +open import Function.Bundles using (Func; _⟶ₛ_; _⟨$⟩_) +open import Functor.Instance.Nat.Pull using (Pull; Pull₁) +open import Level using (0ℓ; Level) + +open import Data.Fin.Permutation using (Permutation; _⟨$⟩ʳ_; _⟨$⟩ˡ_) +open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using (products) +open BinaryProducts products using (-×-) +open Cocartesian Nat-Cocartesian using (module Dual; _+₁_; +-assocʳ; +-comm; +-swap; +₁∘+-swap; i₁; i₂) +open Dual.op-binaryProducts using () renaming (-×- to -+-; assocˡ∘⟨⟩ to []∘assocʳ; swap∘⟨⟩ to []∘swap) + +open import Data.Fin.Base using (Fin; splitAt; join; _↑ˡ_; _↑ʳ_) +open import Data.Fin.Properties using (splitAt-join; splitAt-↑ˡ; splitAt-↑ʳ; join-splitAt) +open import Data.Sum.Base using ([_,_]′; map; map₁; map₂; inj₁; inj₂) +open import Data.Sum.Properties using ([,]-map; [,]-cong; [-,]-cong; [,-]-cong; [,]-∘) +open import Data.Fin.Preimage using (preimage) +open import Function.Base using (_∘_; id) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_; module ≡-Reasoning) +open import Data.Bool.Base using (Bool) +open import Data.Setoid using (∣_∣) +open import Data.Circuit.Value using (Value) +open import Data.System.Values Value using (Values) + +open import Category.Instance.Setoids.SymmetricMonoidal {0ℓ} {0ℓ} using (Setoids-×) +open import Categories.Functor.Monoidal.Symmetric Natop,+,0 Setoids-× using (module Strong) +open Strong using (SymmetricMonoidalFunctor) +open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory) + +module Setoids-× = SymmetricMonoidalCategory Setoids-× +import Function.Construct.Constant as Const + +open Func + +module _ where + + open import Categories.Morphism (Setoids-×.U) using (_≅_; module Iso) + open import Data.Unit.Polymorphic using (tt) + open _≅_ + open Iso + + Pull-ε : SingletonSetoid ≅ Values 0 + from Pull-ε = Const.function SingletonSetoid (Values 0) [] + to Pull-ε = Const.function (Values 0) SingletonSetoid tt + isoˡ (iso Pull-ε) = tt + isoʳ (iso Pull-ε) () + +++ₛ : {n m : ℕ} → Values n ×ₛ Values m ⟶ₛ Values (n + m) +to ++ₛ (xs , ys) = xs ++ ys +cong ++ₛ (≗xs , ≗ys) = ++-cong _ _ ≗xs ≗ys + +splitₛ : {n m : ℕ} → Values (n + m) ⟶ₛ Values n ×ₛ Values m +to (splitₛ {n} {m}) v = v ∘ (_↑ˡ m) , v ∘ (n ↑ʳ_) +cong (splitₛ {n} {m}) v₁≋v₂ = v₁≋v₂ ∘ (_↑ˡ m) , v₁≋v₂ ∘ (n ↑ʳ_) + +Pull-++ + : {n n′ m m′ : ℕ} + (f : Fin n → Fin n′) + (g : Fin m → Fin m′) + {xs : ∣ Values n′ ∣} + {ys : ∣ Values m′ ∣} + → (Pull₁ f ⟨$⟩ xs) ++ (Pull₁ g ⟨$⟩ ys) ≗ Pull₁ (f +₁ g) ⟨$⟩ (xs ++ ys) +Pull-++ {n} {n′} {m} {m′} f g {xs} {ys} e = begin + (xs ∘ f ++ ys ∘ g) e ≡⟨ [,]-map (splitAt n e) ⟨ + [ xs , ys ]′ (map f g (splitAt n e)) ≡⟨ ≡.cong [ xs , ys ]′ (splitAt-join n′ m′ (map f g (splitAt n e))) ⟨ + [ xs , ys ]′ (splitAt n′ (join n′ m′ (map f g (splitAt n e)))) ≡⟨ ≡.cong ([ xs , ys ]′ ∘ splitAt n′) ([,]-map (splitAt n e)) ⟩ + [ xs , ys ]′ (splitAt n′ ((f +₁ g) e)) ∎ + where + open ≡-Reasoning + +⊗-homomorphism : NaturalIsomorphism (-×- ∘F (Pull ⁂ Pull)) (Pull ∘F -+-) +⊗-homomorphism = niHelper record + { η = λ (n , m) → ++ₛ {n} {m} + ; η⁻¹ = λ (n , m) → splitₛ {n} {m} + ; commute = λ (f , g) → Pull-++ f g + ; iso = λ (n , m) → record + { isoˡ = λ { {x , y} → (λ i → ≡.cong [ x , y ] (splitAt-↑ˡ n i m)) , (λ i → ≡.cong [ x , y ] (splitAt-↑ʳ n m i)) } + ; isoʳ = λ { {x} i → ≡.trans (≡.sym ([,]-∘ x (splitAt n i))) (≡.cong x (join-splitAt n m i)) } + } + } + where + open import Data.Sum.Base using ([_,_]) + open import Data.Product.Base using (proj₁; proj₂) + +++-↑ˡ + : {n m : ℕ} + (X : ∣ Values n ∣) + (Y : ∣ Values m ∣) + → (X ++ Y) ∘ i₁ ≗ X +++-↑ˡ {n} {m} X Y i = ≡.cong [ X , Y ]′ (splitAt-↑ˡ n i m) + +++-↑ʳ + : {n m : ℕ} + (X : ∣ Values n ∣) + (Y : ∣ Values m ∣) + → (X ++ Y) ∘ i₂ ≗ Y +++-↑ʳ {n} {m} X Y i = ≡.cong [ X , Y ]′ (splitAt-↑ʳ n m i) + +-- TODO move to Data.Vector +++-assoc + : {m n o : ℕ} + (X : ∣ Values m ∣) + (Y : ∣ Values n ∣) + (Z : ∣ Values o ∣) + → ((X ++ Y) ++ Z) ∘ +-assocʳ {m} ≗ X ++ (Y ++ Z) +++-assoc {m} {n} {o} X Y Z i = begin + ((X ++ Y) ++ Z) (+-assocʳ {m} i) ≡⟨⟩ + ((X ++ Y) ++ Z) ([ i₁ ∘ i₁ , _ ]′ (splitAt m i)) ≡⟨ [,]-∘ ((X ++ Y) ++ Z) (splitAt m i) ⟩ + [ ((X ++ Y) ++ Z) ∘ i₁ ∘ i₁ , _ ]′ (splitAt m i) ≡⟨ [-,]-cong (++-↑ˡ (X ++ Y) Z ∘ i₁) (splitAt m i) ⟩ + [ (X ++ Y) ∘ i₁ , _ ]′ (splitAt m i) ≡⟨ [-,]-cong (++-↑ˡ X Y) (splitAt m i) ⟩ + [ X , ((X ++ Y) ++ Z) ∘ [ _ , _ ]′ ∘ splitAt n ]′ (splitAt m i) ≡⟨ [,-]-cong ([,]-∘ ((X ++ Y) ++ Z) ∘ splitAt n) (splitAt m i) ⟩ + [ X , [ (_ ++ Z) ∘ i₁ ∘ i₂ {m} , _ ]′ ∘ splitAt n ]′ (splitAt m i) ≡⟨ [,-]-cong ([-,]-cong (++-↑ˡ (X ++ Y) Z ∘ i₂) ∘ splitAt n) (splitAt m i) ⟩ + [ X , [ (X ++ Y) ∘ i₂ , _ ]′ ∘ splitAt n ]′ (splitAt m i) ≡⟨ [,-]-cong ([-,]-cong (++-↑ʳ X Y) ∘ splitAt n) (splitAt m i) ⟩ + [ X , [ Y , ((X ++ Y) ++ Z) ∘ i₂ ]′ ∘ splitAt n ]′ (splitAt m i) ≡⟨ [,-]-cong ([,-]-cong (++-↑ʳ (X ++ Y) Z) ∘ splitAt n) (splitAt m i) ⟩ + [ X , [ Y , Z ]′ ∘ splitAt n ]′ (splitAt m i) ≡⟨⟩ + (X ++ (Y ++ Z)) i ∎ + where + open Bool + open Fin + open ≡-Reasoning + +-- TODO also Data.Vector +Pull-unitaryˡ + : {n : ℕ} + (X : ∣ Values n ∣) + → (X ++ []) ∘ i₁ ≗ X +Pull-unitaryˡ {n} X i = begin + [ X , [] ]′ (splitAt _ (i ↑ˡ 0)) ≡⟨ ≡.cong ([ X , [] ]′) (splitAt-↑ˡ n i 0) ⟩ + [ X , [] ]′ (inj₁ i) ≡⟨⟩ + X i ∎ + where + open ≡-Reasoning + +open import Function.Bundles using (Inverse) +open import Categories.Category.Instance.Nat using (Nat) +open import Categories.Morphism Nat using (_≅_) +Pull-swap + : {n m : ℕ} + (X : ∣ Values n ∣) + (Y : ∣ Values m ∣) + → (X ++ Y) ∘ (+-swap {n}) ≗ Y ++ X +Pull-swap {n} {m} X Y i = begin + ((X ++ Y) ∘ +-swap {n}) i ≡⟨ [,]-∘ (X ++ Y) (splitAt m i) ⟩ + [ (X ++ Y) ∘ i₂ , (X ++ Y) ∘ i₁ ]′ (splitAt m i) ≡⟨ [-,]-cong (++-↑ʳ X Y) (splitAt m i) ⟩ + [ Y , (X ++ Y) ∘ i₁ ]′ (splitAt m i) ≡⟨ [,-]-cong (++-↑ˡ X Y) (splitAt m i) ⟩ + [ Y , X ]′ (splitAt m i) ≡⟨⟩ + (Y ++ X) i ∎ + where + open ≡-Reasoning + open Inverse + module +-swap = _≅_ (+-comm {m} {n}) + n+m↔m+n : Permutation (n + m) (m + n) + n+m↔m+n .to = +-swap.to + n+m↔m+n .from = +-swap.from + n+m↔m+n .to-cong ≡.refl = ≡.refl + n+m↔m+n .from-cong ≡.refl = ≡.refl + n+m↔m+n .inverse = (λ { ≡.refl → +-swap.isoˡ _ }) , (λ { ≡.refl → +-swap.isoʳ _ }) + +open SymmetricMonoidalFunctor +Pull,++,[] : SymmetricMonoidalFunctor +Pull,++,[] .F = Pull +Pull,++,[] .isBraidedMonoidal = record + { isStrongMonoidal = record + { ε = Pull-ε + ; ⊗-homo = ⊗-homomorphism + ; associativity = λ { {m} {n} {o} {(X , Y) , Z} i → ++-assoc X Y Z i } + ; unitaryˡ = λ _ → ≡.refl + ; unitaryʳ = λ { {n} {X , _} i → Pull-unitaryˡ X i } + } + ; braiding-compat = λ { {n} {m} {X , Y} i → Pull-swap X Y i } + } diff --git a/Functor/Monoidal/Instance/Nat/Push.agda b/Functor/Monoidal/Instance/Nat/Push.agda new file mode 100644 index 0000000..30ed745 --- /dev/null +++ b/Functor/Monoidal/Instance/Nat/Push.agda @@ -0,0 +1,339 @@ +{-# OPTIONS --without-K --safe #-} + +module Functor.Monoidal.Instance.Nat.Push where + +open import Categories.Category.Instance.Nat using (Nat) +open import Data.Bool.Base using (Bool; false) +open import Data.Subset.Functional using (Subset; ⁅_⁆; ⊥) +open import Function.Base using (_∘_; case_of_; _$_; id) +open import Function.Bundles using (Func; _⟶ₛ_; _⟨$⟩_) +open import Level using (0ℓ; Level) +open import Relation.Binary using (Rel; Setoid) +open import Functor.Instance.Nat.Push using (Push; Push₁; Push-identity) +open import Categories.Category.Instance.SingletonSet using (SingletonSetoid) +open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) +open import Data.Vec.Functional using (Vector; []; _++_; head; tail) +open import Data.Vec.Functional.Properties using (++-cong) +open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian) +open import Categories.Category.BinaryProducts using (module BinaryProducts) +open import Categories.Category.Cartesian using (Cartesian) +open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using (products) +open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory) +open import Categories.Category.Instance.Nat using (Nat-Cocartesian) +open import Categories.Category.Cocartesian using (Cocartesian; module BinaryCoproducts) +open import Categories.Category.Product using (_⁂_) +open import Categories.Functor using () renaming (_∘F_ to _∘′_) +open Cocartesian Nat-Cocartesian using (module Dual; i₁; i₂; -+-; _+₁_; +-assoc; +-assocʳ; +-assocˡ; +-comm; +-swap; +₁∘+-swap) +open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_) +open import Data.Nat.Base using (ℕ; _+_) +open import Data.Fin.Base using (Fin) +open import Data.Product.Base using (_,_; _×_; Σ) +open import Data.Fin.Preimage using (preimage; preimage-⊥; preimage-cong₂) +open import Functor.Monoidal.Instance.Nat.Preimage using (preimage-++) +open import Data.Sum.Base using ([_,_]; [_,_]′; inj₁; inj₂) +open import Data.Sum.Properties using ([,]-cong; [,-]-cong; [-,]-cong; [,]-∘; [,]-map) +open import Data.Circuit.Merge using (merge-with; merge; merge-⊥; merge-[]; merge-cong₁; merge-cong₂; merge-suc; _when_; join-merge; merge-preimage-ρ; merge-⁅⁆) +open import Data.Circuit.Value using (Value; join; join-comm; join-assoc) +open import Data.Fin.Base using (splitAt; _↑ˡ_; _↑ʳ_) renaming (join to joinAt) +open import Data.Fin.Properties using (splitAt-↑ˡ; splitAt-↑ʳ; splitAt⁻¹-↑ˡ; splitAt⁻¹-↑ʳ; ↑ˡ-injective; ↑ʳ-injective; _≟_; 2↔Bool) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≢_; _≗_; module ≡-Reasoning) +open BinaryProducts products using (-×-) +open Value using (U) +open Bool using (false) + +open import Function.Bundles using (Equivalence) +open import Category.Monoidal.Instance.Nat using (Nat,+,0) +open import Category.Instance.Setoids.SymmetricMonoidal {0ℓ} {0ℓ} using (Setoids-×) +open import Categories.Functor.Monoidal.Symmetric Nat,+,0 Setoids-× using (module Lax) +open Lax using (SymmetricMonoidalFunctor) +open import Categories.Morphism Nat using (_≅_) +open import Function.Bundles using (Inverse) +open import Data.Fin.Permutation using (Permutation; _⟨$⟩ʳ_; _⟨$⟩ˡ_) +open Dual.op-binaryProducts using () renaming (assocˡ∘⟨⟩ to []∘assocʳ; swap∘⟨⟩ to []∘swap) +open import Relation.Nullary.Decidable using (does; does-⇔; dec-false) + +open import Data.System.Values Value using (Values) + +open Func +Push-ε : SingletonSetoid {0ℓ} {0ℓ} ⟶ₛ Values 0 +to Push-ε x = [] +cong Push-ε x () + +++ₛ : {n m : ℕ} → Values n ×ₛ Values m ⟶ₛ Values (n + m) +to ++ₛ (xs , ys) = xs ++ ys +cong ++ₛ (≗xs , ≗ys) = ++-cong _ _ ≗xs ≗ys + +∣_∣ : {c ℓ : Level} → Setoid c ℓ → Set c +∣_∣ = Setoid.Carrier + +open ℕ +merge-++ + : {n m : ℕ} + (xs : ∣ Values n ∣) + (ys : ∣ Values m ∣) + (S₁ : Subset n) + (S₂ : Subset m) + → merge (xs ++ ys) (S₁ ++ S₂) + ≡ join (merge xs S₁) (merge ys S₂) +merge-++ {zero} {m} xs ys S₁ S₂ = begin + merge (xs ++ ys) (S₁ ++ S₂) ≡⟨ merge-cong₂ (xs ++ ys) (λ _ → ≡.refl) ⟩ + merge (xs ++ ys) S₂ ≡⟨ merge-cong₁ (λ _ → ≡.refl) S₂ ⟩ + merge ys S₂ ≡⟨ ≡.cong (λ h → join h (merge ys S₂)) (merge-[] xs S₁) ⟨ + join (merge xs S₁) (merge ys S₂) ∎ + where + open ≡-Reasoning +merge-++ {suc n} {m} xs ys S₁ S₂ = begin + merge (xs ++ ys) (S₁ ++ S₂) ≡⟨ merge-suc (xs ++ ys) (S₁ ++ S₂) ⟩ + merge-with (head xs when head S₁) (tail (xs ++ ys)) (tail (S₁ ++ S₂)) ≡⟨ join-merge (head xs when head S₁) (tail (xs ++ ys)) (tail (S₁ ++ S₂)) ⟨ + join (head xs when head S₁) (merge (tail (xs ++ ys)) (tail (S₁ ++ S₂))) + ≡⟨ ≡.cong (join (head xs when head S₁)) (merge-cong₁ ([,]-map ∘ splitAt n) (tail (S₁ ++ S₂))) ⟩ + join (head xs when head S₁) (merge (tail xs ++ ys) (tail (S₁ ++ S₂))) + ≡⟨ ≡.cong (join (head xs when head S₁)) (merge-cong₂ (tail xs ++ ys) ([,]-map ∘ splitAt n)) ⟩ + join (head xs when head S₁) (merge (tail xs ++ ys) (tail S₁ ++ S₂)) ≡⟨ ≡.cong (join (head xs when head S₁)) (merge-++ (tail xs) ys (tail S₁) S₂) ⟩ + join (head xs when head S₁) (join (merge (tail xs) (tail S₁)) (merge ys S₂)) ≡⟨ join-assoc (head xs when head S₁) (merge (tail xs) (tail S₁)) _ ⟨ + join (join (head xs when head S₁) (merge (tail xs) (tail S₁))) (merge ys S₂) + ≡⟨ ≡.cong (λ h → join h (merge ys S₂)) (join-merge (head xs when head S₁) (tail xs) (tail S₁)) ⟩ + join (merge-with (head xs when head S₁) (tail xs) (tail S₁)) (merge ys S₂) ≡⟨ ≡.cong (λ h → join h (merge ys S₂)) (merge-suc xs S₁) ⟨ + join (merge xs S₁) (merge ys S₂) ∎ + where + open ≡-Reasoning + +open Fin +⁅⁆-≟ : {n : ℕ} (x y : Fin n) → ⁅ x ⁆ y ≡ does (x ≟ y) +⁅⁆-≟ zero zero = ≡.refl +⁅⁆-≟ zero (suc y) = ≡.refl +⁅⁆-≟ (suc x) zero = ≡.refl +⁅⁆-≟ (suc x) (suc y) = ⁅⁆-≟ x y + +Push-++ + : {n n′ m m′ : ℕ} + (f : Fin n → Fin n′) + (g : Fin m → Fin m′) + (xs : ∣ Values n ∣) + (ys : ∣ Values m ∣) + → merge xs ∘ preimage f ∘ ⁅_⁆ ++ merge ys ∘ preimage g ∘ ⁅_⁆ + ≗ merge (xs ++ ys) ∘ preimage (f +₁ g) ∘ ⁅_⁆ +Push-++ {n} {n′} {m} {m′} f g xs ys i = begin + ((merge xs ∘ preimage f ∘ ⁅_⁆) ++ (merge ys ∘ preimage g ∘ ⁅_⁆)) i ≡⟨⟩ + [ merge xs ∘ preimage f ∘ ⁅_⁆ , merge ys ∘ preimage g ∘ ⁅_⁆ ]′ (splitAt n′ i) + ≡⟨ [,]-cong left right (splitAt n′ i) ⟩ + [ (λ x → merge (xs ++ ys) _) , (λ x → merge (xs ++ ys) _) ]′ (splitAt n′ i) + ≡⟨ [,]-∘ (merge (xs ++ ys) ∘ (preimage (f +₁ g))) (splitAt n′ i) ⟨ + merge (xs ++ ys) (preimage (f +₁ g) ([ ⁅⁆++⊥ , ⊥++⁅⁆ ]′ (splitAt n′ i))) ≡⟨⟩ + merge (xs ++ ys) (preimage (f +₁ g) ((⁅⁆++⊥ ++ ⊥++⁅⁆) i)) ≡⟨ merge-cong₂ (xs ++ ys) (preimage-cong₂ (f +₁ g) (⁅⁆-++ i)) ⟩ + merge (xs ++ ys) (preimage (f +₁ g) ⁅ i ⁆) ∎ + where + open ≡-Reasoning + left : (x : Fin n′) → merge xs (preimage f ⁅ x ⁆) ≡ merge (xs ++ ys) (preimage (f +₁ g) (⁅ x ⁆ ++ ⊥)) + left x = begin + merge xs (preimage f ⁅ x ⁆) ≡⟨ join-comm U (merge xs (preimage f ⁅ x ⁆)) ⟩ + join (merge xs (preimage f ⁅ x ⁆)) U ≡⟨ ≡.cong (join (merge _ _)) (merge-⊥ ys) ⟨ + join (merge xs (preimage f ⁅ x ⁆)) (merge ys ⊥) ≡⟨ ≡.cong (join (merge _ _)) (merge-cong₂ ys (preimage-⊥ g)) ⟨ + join (merge xs (preimage f ⁅ x ⁆)) (merge ys (preimage g ⊥)) ≡⟨ merge-++ xs ys (preimage f ⁅ x ⁆) (preimage g ⊥) ⟨ + merge (xs ++ ys) ((preimage f ⁅ x ⁆) ++ (preimage g ⊥)) ≡⟨ merge-cong₂ (xs ++ ys) (preimage-++ f g) ⟩ + merge (xs ++ ys) (preimage (f +₁ g) (⁅ x ⁆ ++ ⊥)) ∎ + right : (x : Fin m′) → merge ys (preimage g ⁅ x ⁆) ≡ merge (xs ++ ys) (preimage (f +₁ g) (⊥ ++ ⁅ x ⁆)) + right x = begin + merge ys (preimage g ⁅ x ⁆) ≡⟨⟩ + join U (merge ys (preimage g ⁅ x ⁆)) ≡⟨ ≡.cong (λ h → join h (merge _ _)) (merge-⊥ xs) ⟨ + join (merge xs ⊥) (merge ys (preimage g ⁅ x ⁆)) ≡⟨ ≡.cong (λ h → join h (merge _ _)) (merge-cong₂ xs (preimage-⊥ f)) ⟨ + join (merge xs (preimage f ⊥)) (merge ys (preimage g ⁅ x ⁆)) ≡⟨ merge-++ xs ys (preimage f ⊥) (preimage g ⁅ x ⁆) ⟨ + merge (xs ++ ys) ((preimage f ⊥) ++ (preimage g ⁅ x ⁆)) ≡⟨ merge-cong₂ (xs ++ ys) (preimage-++ f g) ⟩ + merge (xs ++ ys) (preimage (f +₁ g) (⊥ ++ ⁅ x ⁆)) ∎ + ⁅⁆++⊥ : Vector (Subset (n′ + m′)) n′ + ⁅⁆++⊥ x = ⁅ x ⁆ ++ ⊥ + ⊥++⁅⁆ : Vector (Subset (n′ + m′)) m′ + ⊥++⁅⁆ x = ⊥ ++ ⁅ x ⁆ + + open ℕ + + open Equivalence + + ⁅⁆-++ + : (i : Fin (n′ + m′)) + → [ (λ x → ⁅ x ⁆ ++ ⊥) , (λ x → ⊥ ++ ⁅ x ⁆) ]′ (splitAt n′ i) ≗ ⁅ i ⁆ + ⁅⁆-++ i x with splitAt n′ i in eq₁ + ... | inj₁ i′ with splitAt n′ x in eq₂ + ... | inj₁ x′ = begin + ⁅ i′ ⁆ x′ ≡⟨ ⁅⁆-≟ i′ x′ ⟩ + does (i′ ≟ x′) ≡⟨ does-⇔ ⇔ (i′ ≟ x′) (i′ ↑ˡ m′ ≟ x′ ↑ˡ m′) ⟩ + does (i′ ↑ˡ m′ ≟ x′ ↑ˡ m′) ≡⟨ ⁅⁆-≟ (i′ ↑ˡ m′) (x′ ↑ˡ m′) ⟨ + ⁅ i′ ↑ˡ m′ ⁆ (x′ ↑ˡ m′) ≡⟨ ≡.cong₂ ⁅_⁆ (splitAt⁻¹-↑ˡ eq₁) (splitAt⁻¹-↑ˡ eq₂) ⟩ + ⁅ i ⁆ x ∎ + where + ⇔ : Equivalence (≡.setoid (i′ ≡ x′)) (≡.setoid (i′ ↑ˡ m′ ≡ x′ ↑ˡ m′)) + ⇔ .to = ≡.cong (_↑ˡ m′) + ⇔ .from = ↑ˡ-injective m′ i′ x′ + ⇔ .to-cong ≡.refl = ≡.refl + ⇔ .from-cong ≡.refl = ≡.refl + ... | inj₂ x′ = begin + false ≡⟨ dec-false (i′ ↑ˡ m′ ≟ n′ ↑ʳ x′) ↑ˡ≢↑ʳ ⟨ + does (i′ ↑ˡ m′ ≟ n′ ↑ʳ x′) ≡⟨ ⁅⁆-≟ (i′ ↑ˡ m′) (n′ ↑ʳ x′) ⟨ + ⁅ i′ ↑ˡ m′ ⁆ (n′ ↑ʳ x′) ≡⟨ ≡.cong₂ ⁅_⁆ (splitAt⁻¹-↑ˡ eq₁) (splitAt⁻¹-↑ʳ eq₂) ⟩ + ⁅ i ⁆ x ∎ + where + ↑ˡ≢↑ʳ : i′ ↑ˡ m′ ≢ n′ ↑ʳ x′ + ↑ˡ≢↑ʳ ≡ = case ≡.trans (≡.sym (splitAt-↑ˡ n′ i′ m′)) (≡.trans (≡.cong (splitAt n′) ≡) (splitAt-↑ʳ n′ m′ x′)) of λ { () } + ⁅⁆-++ i x | inj₂ i′ with splitAt n′ x in eq₂ + ⁅⁆-++ i x | inj₂ i′ | inj₁ x′ = ≡.trans (≡.cong ([ ⊥ , ⁅ i′ ⁆ ]′) eq₂) $ begin + false ≡⟨ dec-false (n′ ↑ʳ i′ ≟ x′ ↑ˡ m′) ↑ʳ≢↑ˡ ⟨ + does (n′ ↑ʳ i′ ≟ x′ ↑ˡ m′) ≡⟨ ⁅⁆-≟ (n′ ↑ʳ i′) (x′ ↑ˡ m′) ⟨ + ⁅ n′ ↑ʳ i′ ⁆ (x′ ↑ˡ m′) ≡⟨ ≡.cong₂ ⁅_⁆ (splitAt⁻¹-↑ʳ eq₁) (splitAt⁻¹-↑ˡ eq₂) ⟩ + ⁅ i ⁆ x ∎ + where + ↑ʳ≢↑ˡ : n′ ↑ʳ i′ ≢ x′ ↑ˡ m′ + ↑ʳ≢↑ˡ ≡ = case ≡.trans (≡.sym (splitAt-↑ʳ n′ m′ i′)) (≡.trans (≡.cong (splitAt n′) ≡) (splitAt-↑ˡ n′ x′ m′)) of λ { () } + ⁅⁆-++ i x | inj₂ i′ | inj₂ x′ = begin + [ ⊥ , ⁅ i′ ⁆ ] (splitAt n′ x) ≡⟨ ≡.cong ([ ⊥ , ⁅ i′ ⁆ ]) eq₂ ⟩ + ⁅ i′ ⁆ x′ ≡⟨ ⁅⁆-≟ i′ x′ ⟩ + does (i′ ≟ x′) ≡⟨ does-⇔ ⇔ (i′ ≟ x′) (n′ ↑ʳ i′ ≟ n′ ↑ʳ x′) ⟩ + does (n′ ↑ʳ i′ ≟ n′ ↑ʳ x′) ≡⟨ ⁅⁆-≟ (n′ ↑ʳ i′) (n′ ↑ʳ x′) ⟨ + ⁅ n′ ↑ʳ i′ ⁆ (n′ ↑ʳ x′) ≡⟨ ≡.cong₂ ⁅_⁆ (splitAt⁻¹-↑ʳ eq₁) (splitAt⁻¹-↑ʳ eq₂) ⟩ + ⁅ i ⁆ x ∎ + where + ⇔ : Equivalence (≡.setoid (i′ ≡ x′)) (≡.setoid (n′ ↑ʳ i′ ≡ n′ ↑ʳ x′)) + ⇔ .to = ≡.cong (n′ ↑ʳ_) + ⇔ .from = ↑ʳ-injective n′ i′ x′ + ⇔ .to-cong ≡.refl = ≡.refl + ⇔ .from-cong ≡.refl = ≡.refl + +⊗-homomorphism : NaturalTransformation (-×- ∘′ (Push ⁂ Push)) (Push ∘′ -+-) +⊗-homomorphism = ntHelper record + { η = λ (n , m) → ++ₛ {n} {m} + ; commute = λ { {n , m} {n′ , m′} (f , g) {xs , ys} i → Push-++ f g xs ys i } + } + +++-↑ˡ + : {n m : ℕ} + (X : ∣ Values n ∣) + (Y : ∣ Values m ∣) + → (X ++ Y) ∘ i₁ ≗ X +++-↑ˡ {n} {m} X Y i = ≡.cong [ X , Y ]′ (splitAt-↑ˡ n i m) + +++-↑ʳ + : {n m : ℕ} + (X : ∣ Values n ∣) + (Y : ∣ Values m ∣) + → (X ++ Y) ∘ i₂ ≗ Y +++-↑ʳ {n} {m} X Y i = ≡.cong [ X , Y ]′ (splitAt-↑ʳ n m i) + +++-assoc + : {m n o : ℕ} + (X : ∣ Values m ∣) + (Y : ∣ Values n ∣) + (Z : ∣ Values o ∣) + → ((X ++ Y) ++ Z) ∘ +-assocʳ {m} ≗ X ++ (Y ++ Z) +++-assoc {m} {n} {o} X Y Z i = begin + ((X ++ Y) ++ Z) (+-assocʳ {m} i) ≡⟨⟩ + ((X ++ Y) ++ Z) ([ i₁ ∘ i₁ , _ ]′ (splitAt m i)) ≡⟨ [,]-∘ ((X ++ Y) ++ Z) (splitAt m i) ⟩ + [ ((X ++ Y) ++ Z) ∘ i₁ ∘ i₁ , _ ]′ (splitAt m i) ≡⟨ [-,]-cong (++-↑ˡ (X ++ Y) Z ∘ i₁) (splitAt m i) ⟩ + [ (X ++ Y) ∘ i₁ , _ ]′ (splitAt m i) ≡⟨ [-,]-cong (++-↑ˡ X Y) (splitAt m i) ⟩ + [ X , ((X ++ Y) ++ Z) ∘ [ _ , _ ]′ ∘ splitAt n ]′ (splitAt m i) ≡⟨ [,-]-cong ([,]-∘ ((X ++ Y) ++ Z) ∘ splitAt n) (splitAt m i) ⟩ + [ X , [ (_ ++ Z) ∘ i₁ ∘ i₂ {m} , _ ]′ ∘ splitAt n ]′ (splitAt m i) ≡⟨ [,-]-cong ([-,]-cong (++-↑ˡ (X ++ Y) Z ∘ i₂) ∘ splitAt n) (splitAt m i) ⟩ + [ X , [ (X ++ Y) ∘ i₂ , _ ]′ ∘ splitAt n ]′ (splitAt m i) ≡⟨ [,-]-cong ([-,]-cong (++-↑ʳ X Y) ∘ splitAt n) (splitAt m i) ⟩ + [ X , [ Y , ((X ++ Y) ++ Z) ∘ i₂ ]′ ∘ splitAt n ]′ (splitAt m i) ≡⟨ [,-]-cong ([,-]-cong (++-↑ʳ (X ++ Y) Z) ∘ splitAt n) (splitAt m i) ⟩ + [ X , [ Y , Z ]′ ∘ splitAt n ]′ (splitAt m i) ≡⟨⟩ + (X ++ (Y ++ Z)) i ∎ + where + open Bool + open Fin + open ≡-Reasoning + +Preimage-unitaryˡ + : {n : ℕ} + (X : Subset n) + → (X ++ []) ∘ (_↑ˡ 0) ≗ X +Preimage-unitaryˡ {n} X i = begin + [ X , [] ]′ (splitAt _ (i ↑ˡ 0)) ≡⟨ ≡.cong ([ X , [] ]′) (splitAt-↑ˡ n i 0) ⟩ + [ X , [] ]′ (inj₁ i) ≡⟨⟩ + X i ∎ + where + open ≡-Reasoning + +Push-assoc + : {m n o : ℕ} + (X : ∣ Values m ∣) + (Y : ∣ Values n ∣) + (Z : ∣ Values o ∣) + → merge ((X ++ Y) ++ Z) ∘ preimage (+-assocˡ {m}) ∘ ⁅_⁆ + ≗ X ++ (Y ++ Z) +Push-assoc {m} {n} {o} X Y Z i = begin + merge ((X ++ Y) ++ Z) (preimage (+-assocˡ {m}) ⁅ i ⁆) ≡⟨ merge-preimage-ρ ↔-mno ((X ++ Y) ++ Z) ⁅ i ⁆ ⟩ + merge (((X ++ Y) ++ Z) ∘ (+-assocʳ {m})) (⁅ i ⁆) ≡⟨⟩ + merge (((X ++ Y) ++ Z) ∘ (+-assocʳ {m})) (preimage id ⁅ i ⁆) ≡⟨ merge-cong₁ (++-assoc X Y Z) (preimage id ⁅ i ⁆) ⟩ + merge (X ++ (Y ++ Z)) (preimage id ⁅ i ⁆) ≡⟨ Push-identity i ⟩ + (X ++ (Y ++ Z)) i ∎ + where + open Inverse + module +-assoc = _≅_ (+-assoc {m} {n} {o}) + ↔-mno : Permutation ((m + n) + o) (m + (n + o)) + ↔-mno .to = +-assocˡ {m} + ↔-mno .from = +-assocʳ {m} + ↔-mno .to-cong ≡.refl = ≡.refl + ↔-mno .from-cong ≡.refl = ≡.refl + ↔-mno .inverse = (λ { ≡.refl → +-assoc.isoˡ _ }) , λ { ≡.refl → +-assoc.isoʳ _ } + open ≡-Reasoning + +preimage-++′ + : {n m o : ℕ} + (f : Vector (Fin o) n) + (g : Vector (Fin o) m) + (S : Subset o) + → preimage (f ++ g) S ≗ preimage f S ++ preimage g S +preimage-++′ {n} f g S = [,]-∘ S ∘ splitAt n + +Push-unitaryʳ + : {n : ℕ} + (X : ∣ Values n ∣) + (i : Fin n) + → merge (X ++ []) (preimage (id ++ (λ ())) ⁅ i ⁆) ≡ X i +Push-unitaryʳ {n} X i = begin + merge (X ++ []) (preimage (id ++ (λ ())) ⁅ i ⁆) ≡⟨ merge-cong₂ (X ++ []) (preimage-++′ id (λ ()) ⁅ i ⁆) ⟩ + merge (X ++ []) (preimage id ⁅ i ⁆ ++ preimage (λ ()) ⁅ i ⁆) ≡⟨⟩ + merge (X ++ []) (⁅ i ⁆ ++ preimage (λ ()) ⁅ i ⁆) ≡⟨ merge-++ X [] ⁅ i ⁆ (preimage (λ ()) ⁅ i ⁆) ⟩ + join (merge X ⁅ i ⁆) (merge [] (preimage (λ ()) ⁅ i ⁆)) ≡⟨ ≡.cong (join (merge X ⁅ i ⁆)) (merge-[] [] (preimage (λ ()) ⁅ i ⁆)) ⟩ + join (merge X ⁅ i ⁆) U ≡⟨ join-comm (merge X ⁅ i ⁆) U ⟩ + merge X ⁅ i ⁆ ≡⟨ merge-⁅⁆ X i ⟩ + X i ∎ + where + open ≡-Reasoning + t : Fin (n + 0) → Fin n + t = id ++ (λ ()) + +Push-swap + : {n m : ℕ} + (X : ∣ Values n ∣) + (Y : ∣ Values m ∣) + → merge (X ++ Y) ∘ preimage (+-swap {m}) ∘ ⁅_⁆ ≗ Y ++ X +Push-swap {n} {m} X Y i = begin + merge (X ++ Y) (preimage (+-swap {m}) ⁅ i ⁆) ≡⟨ merge-preimage-ρ n+m↔m+n (X ++ Y) ⁅ i ⁆ ⟩ + merge ((X ++ Y) ∘ +-swap {n}) ⁅ i ⁆ ≡⟨ merge-⁅⁆ ((X ++ Y) ∘ (+-swap {n})) i ⟩ + ((X ++ Y) ∘ +-swap {n}) i ≡⟨ [,]-∘ (X ++ Y) (splitAt m i) ⟩ + [ (X ++ Y) ∘ i₂ , (X ++ Y) ∘ i₁ ]′ (splitAt m i) ≡⟨ [-,]-cong (++-↑ʳ X Y) (splitAt m i) ⟩ + [ Y , (X ++ Y) ∘ i₁ ]′ (splitAt m i) ≡⟨ [,-]-cong (++-↑ˡ X Y) (splitAt m i) ⟩ + [ Y , X ]′ (splitAt m i) ≡⟨⟩ + (Y ++ X) i ∎ + where + open ≡-Reasoning + open Inverse + module +-swap = _≅_ (+-comm {m} {n}) + n+m↔m+n : Permutation (n + m) (m + n) + n+m↔m+n .to = +-swap.to + n+m↔m+n .from = +-swap.from + n+m↔m+n .to-cong ≡.refl = ≡.refl + n+m↔m+n .from-cong ≡.refl = ≡.refl + n+m↔m+n .inverse = (λ { ≡.refl → +-swap.isoˡ _ }) , (λ { ≡.refl → +-swap.isoʳ _ }) + +open SymmetricMonoidalFunctor +Push,++,[] : SymmetricMonoidalFunctor +Push,++,[] .F = Push +Push,++,[] .isBraidedMonoidal = record + { isMonoidal = record + { ε = Push-ε + ; ⊗-homo = ⊗-homomorphism + ; associativity = λ { {m} {n} {o} {(X , Y) , Z} i → Push-assoc X Y Z i } + ; unitaryˡ = λ { {n} {_ , X} i → merge-⁅⁆ X i } + ; unitaryʳ = λ { {n} {X , _} i → Push-unitaryʳ X i } + } + ; braiding-compat = λ { {n} {m} {X , Y} i → Push-swap X Y i } + } diff --git a/Functor/Monoidal/Instance/Nat/System.agda b/Functor/Monoidal/Instance/Nat/System.agda new file mode 100644 index 0000000..1b3bb34 --- /dev/null +++ b/Functor/Monoidal/Instance/Nat/System.agda @@ -0,0 +1,429 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level; 0ℓ; suc) + +module Functor.Monoidal.Instance.Nat.System {ℓ : Level} where + +open import Function.Construct.Identity using () renaming (function to Id) +import Function.Construct.Constant as Const + +open import Category.Monoidal.Instance.Nat using (Nat,+,0; Natop,+,0) +open import Categories.Category.Instance.Nat using (Natop) +open import Category.Instance.Setoids.SymmetricMonoidal {suc ℓ} {ℓ} using (Setoids-×) +open import Categories.Category.Instance.SingletonSet using (SingletonSetoid) +open import Data.Circuit.Value using (Value) +open import Data.Setoid using (_⇒ₛ_; ∣_∣) +open import Data.System {ℓ} using (Systemₛ; System; ≤-System) +open import Data.System.Values Value using (Values; _≋_; module ≋) +open import Data.Unit.Polymorphic using (⊤; tt) +open import Data.Vec.Functional using ([]) +open import Relation.Binary using (Setoid) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_) +open import Functor.Instance.Nat.System {ℓ} using (Sys; map) +open import Function.Base using (_∘_) +open import Function.Bundles using (Func; _⟶ₛ_; _⟨$⟩_) +open import Function.Construct.Setoid using (setoid) +open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory; BraidedMonoidalCategory) + +open Func + +module _ where + + open System + + discrete : System 0 + discrete .S = SingletonSetoid + discrete .fₛ = Const.function (Values 0) (SingletonSetoid ⇒ₛ SingletonSetoid) (Id SingletonSetoid) + discrete .fₒ = Const.function SingletonSetoid (Values 0) [] + +Sys-ε : SingletonSetoid {suc ℓ} {ℓ} ⟶ₛ Systemₛ 0 +Sys-ε = Const.function SingletonSetoid (Systemₛ 0) discrete + +open import Categories.Category.Cartesian using (Cartesian) +open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian) +open Cartesian (Setoids-Cartesian {suc ℓ} {ℓ}) using (products) +open import Categories.Category.BinaryProducts using (module BinaryProducts) +open BinaryProducts products using (-×-) +open import Categories.Functor using (_∘F_) +open import Categories.Category.Product using (_⁂_) + +open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) +open import Categories.Category.Cocartesian using (Cocartesian) +open import Categories.Category.Instance.Nat using (Nat-Cocartesian) +open Cocartesian Nat-Cocartesian using (module Dual; i₁; i₂; -+-; _+₁_; +-assocʳ; +-assocˡ; +-comm; +-swap; +₁∘+-swap; +₁∘i₁; +₁∘i₂) +open Dual.op-binaryProducts using () renaming (×-assoc to +-assoc) +open import Data.Product.Base using (_,_; dmap) renaming (map to ×-map) + +open import Categories.Functor using (Functor) +open import Categories.Category.Product using (Product) +open import Categories.Category.Instance.Nat using (Nat) +open import Categories.Category.Instance.Setoids using (Setoids) + +open import Data.Fin using (_↑ˡ_; _↑ʳ_) +open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_) +open import Data.Nat using (ℕ; _+_) +open import Data.Product.Base using (_×_) + +private + + variable + n m o : ℕ + c₁ c₂ c₃ c₄ c₅ c₆ : Level + ℓ₁ ℓ₂ ℓ₃ ℓ₄ ℓ₅ ℓ₆ : Level + +open import Functor.Monoidal.Instance.Nat.Push using (++ₛ; Push,++,[]; Push-++; Push-assoc) +open import Functor.Monoidal.Instance.Nat.Pull using (splitₛ; Pull,++,[]; ++-assoc; Pull-unitaryˡ; Pull-ε) +open import Functor.Instance.Nat.Pull using (Pull; Pull₁; Pull-resp-≈; Pull-identity) +open import Functor.Instance.Nat.Push using (Push₁; Push-identity) + +open import Data.Product.Function.NonDependent.Setoid using (_×-function_; proj₁ₛ; proj₂ₛ; <_,_>ₛ; swapₛ) + +_×-⇒_ + : {A : Setoid c₁ ℓ₁} + {B : Setoid c₂ ℓ₂} + {C : Setoid c₃ ℓ₃} + {D : Setoid c₄ ℓ₄} + {E : Setoid c₅ ℓ₅} + {F : Setoid c₆ ℓ₆} + → A ⟶ₛ B ⇒ₛ C + → D ⟶ₛ E ⇒ₛ F + → A ×ₛ D ⟶ₛ B ×ₛ E ⇒ₛ C ×ₛ F +_×-⇒_ f g .to (x , y) = to f x ×-function to g y +_×-⇒_ f g .cong (x , y) = cong f x , cong g y + +open import Function.Construct.Setoid using (_∙_) + +⊗ : System n × System m → System (n + m) +⊗ {n} {m} (S₁ , S₂) = record + { S = S₁.S ×ₛ S₂.S + ; fₛ = S₁.fₛ ×-⇒ S₂.fₛ ∙ splitₛ + ; fₒ = ++ₛ ∙ S₁.fₒ ×-function S₂.fₒ + } + where + module S₁ = System S₁ + module S₂ = System S₂ + +open import Category.Instance.Setoids.SymmetricMonoidal {0ℓ} {0ℓ} using () renaming (Setoids-× to 0ℓ-Setoids-×) +module 0ℓ-Setoids-× = SymmetricMonoidalCategory 0ℓ-Setoids-× renaming (braidedMonoidalCategory to B) +open module ⇒ₛ {A} {B} = Setoid (setoid {0ℓ} {0ℓ} {0ℓ} {0ℓ} A B) using (_≈_) +open import Categories.Functor.Monoidal.Symmetric Natop,+,0 0ℓ-Setoids-× using (module Strong) +open SymmetricMonoidalCategory using () renaming (braidedMonoidalCategory to B) +module Natop,+,0 = SymmetricMonoidalCategory Natop,+,0 renaming (braidedMonoidalCategory to B) +open import Categories.Functor.Monoidal.Braided Natop,+,0.B 0ℓ-Setoids-×.B using () renaming (module Strong to StrongB) +open Strong using (SymmetricMonoidalFunctor) +open StrongB using (BraidedMonoidalFunctor) + +opaque + + _~_ : {A B : Setoid 0ℓ 0ℓ} → Func A B → Func A B → Set + _~_ = _≈_ + infix 4 _~_ + + sym-~ + : {A B : Setoid 0ℓ 0ℓ} + {x y : Func A B} + → x ~ y + → y ~ x + sym-~ {A} {B} {x} {y} = 0ℓ-Setoids-×.Equiv.sym {A} {B} {x} {y} + +⊗ₛ + : {n m : ℕ} + → Func (Systemₛ n ×ₛ Systemₛ m) (Systemₛ (n + m)) +⊗ₛ .to = ⊗ +⊗ₛ {n} {m} .cong {a , b} {c , d} ((a≤c , c≤a) , (b≤d , d≤b)) = left , right + where + module a = System a + module b = System b + module c = System c + module d = System d + open ≤-System + module a≤c = ≤-System a≤c + module b≤d = ≤-System b≤d + module c≤a = ≤-System c≤a + module d≤b = ≤-System d≤b + + open Setoid + open System + + open import Data.Product.Base using (dmap) + open import Data.Vec.Functional.Properties using (++-cong) + left : ≤-System (⊗ₛ .to (a , b)) (⊗ₛ .to (c , d)) + left = record + { ⇒S = a≤c.⇒S ×-function b≤d.⇒S + ; ≗-fₛ = λ i → dmap (a≤c.≗-fₛ (i ∘ i₁)) (b≤d.≗-fₛ (i ∘ i₂)) + ; ≗-fₒ = λ (s₁ , s₂) → ++-cong (a.fₒ′ s₁) (c.fₒ′ (a≤c.⇒S ⟨$⟩ s₁)) (a≤c.≗-fₒ s₁) (b≤d.≗-fₒ s₂) + } + + right : ≤-System (⊗ₛ .to (c , d)) (⊗ₛ .to (a , b)) + right = record + { ⇒S = c≤a.⇒S ×-function d≤b.⇒S + ; ≗-fₛ = λ i → dmap (c≤a.≗-fₛ (i ∘ i₁)) (d≤b.≗-fₛ (i ∘ i₂)) + ; ≗-fₒ = λ (s₁ , s₂) → ++-cong (c.fₒ′ s₁) (a.fₒ′ (c≤a.⇒S ⟨$⟩ s₁)) (c≤a.≗-fₒ s₁) (d≤b.≗-fₒ s₂) + } + +open import Data.Fin using (Fin) + +System-⊗-≤ + : {n n′ m m′ : ℕ} + (X : System n) + (Y : System m) + (f : Fin n → Fin n′) + (g : Fin m → Fin m′) + → ≤-System (⊗ (map f X , map g Y)) (map (f +₁ g) (⊗ (X , Y))) +System-⊗-≤ {n} {n′} {m} {m′} X Y f g = record + { ⇒S = Id (X.S ×ₛ Y.S) + ; ≗-fₛ = λ i _ → cong X.fₛ (≋.sym (≡.cong i ∘ +₁∘i₁)) , cong Y.fₛ (≋.sym (≡.cong i ∘ +₁∘i₂ {f = f})) + ; ≗-fₒ = λ (s₁ , s₂) → Push-++ f g (X.fₒ′ s₁) (Y.fₒ′ s₂) + } + where + module X = System X + module Y = System Y + +System-⊗-≥ + : {n n′ m m′ : ℕ} + (X : System n) + (Y : System m) + (f : Fin n → Fin n′) + (g : Fin m → Fin m′) + → ≤-System (map (f +₁ g) (⊗ (X , Y))) (⊗ (map f X , map g Y)) +System-⊗-≥ {n} {n′} {m} {m′} X Y f g = record + { ⇒S = Id (X.S ×ₛ Y.S) + -- ; ≗-fₛ = λ i _ → cong X.fₛ (≡.cong i ∘ +₁∘i₁) , cong Y.fₛ (≡.cong i ∘ +₁∘i₂ {f = f}) + ; ≗-fₛ = λ i _ → cong (X.fₛ ×-⇒ Y.fₛ) (Pull-resp-≈ (+₁∘i₁ {n′}) {i} , Pull-resp-≈ (+₁∘i₂ {f = f}) {i}) + ; ≗-fₒ = λ (s₁ , s₂) → ≋.sym (Push-++ f g (X.fₒ′ s₁) (Y.fₒ′ s₂)) + } + where + module X = System X + module Y = System Y + import Relation.Binary.PropositionalEquality as ≡ + +⊗-homomorphism : NaturalTransformation (-×- ∘F (Sys ⁂ Sys)) (Sys ∘F -+-) +⊗-homomorphism = ntHelper record + { η = λ (n , m) → ⊗ₛ {n} {m} + ; commute = λ { (f , g) {X , Y} → System-⊗-≤ X Y f g , System-⊗-≥ X Y f g } + } + +⊗-assoc-≤ + : (X : System n) + (Y : System m) + (Z : System o) + → ≤-System (map (+-assocˡ {n}) (⊗ (⊗ (X , Y) , Z))) (⊗ (X , ⊗ (Y , Z))) +⊗-assoc-≤ {n} {m} {o} X Y Z = record + { ⇒S = ×-assocˡ + ; ≗-fₛ = λ i ((s₁ , s₂) , s₃) → cong (X.fₛ ×-⇒ (Y.fₛ ×-⇒ Z.fₛ) ∙ assocˡ) (associativity-inv {x = i}) {s₁ , s₂ , s₃} + ; ≗-fₒ = λ ((s₁ , s₂) , s₃) → Push-assoc (X.fₒ′ s₁) (Y.fₒ′ s₂) (Z.fₒ′ s₃) + } + where + open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using () renaming (products to 0ℓ-products) + open BinaryProducts 0ℓ-products using (assocˡ) + open Cartesian (Setoids-Cartesian {ℓ} {ℓ}) using () renaming (products to prod) + open BinaryProducts prod using () renaming (assocˡ to ×-assocˡ) + module Pull,++,[] = SymmetricMonoidalFunctor Pull,++,[] + module Pull,++,[]B = BraidedMonoidalFunctor (record { isBraidedMonoidal = Pull,++,[].isBraidedMonoidal }) + + open import Functor.Monoidal.Braided.Strong.Properties Pull,++,[].braidedMonoidalFunctor using (associativity-inv) + + module X = System X + module Y = System Y + module Z = System Z + +⊗-assoc-≥ + : (X : System n) + (Y : System m) + (Z : System o) + → ≤-System (⊗ (X , ⊗ (Y , Z))) (map (+-assocˡ {n}) (⊗ (⊗ (X , Y) , Z))) +⊗-assoc-≥ {n} {m} {o} X Y Z = record + { ⇒S = ×-assocʳ + ; ≗-fₛ = λ i (s₁ , s₂ , s₃) → cong ((X.fₛ ×-⇒ Y.fₛ) ×-⇒ Z.fₛ) (sym-split-assoc {i}) {(s₁ , s₂) , s₃} + ; ≗-fₒ = λ (s₁ , s₂ , s₃) → sym-++-assoc {(X.fₒ′ s₁ , Y.fₒ′ s₂) , Z.fₒ′ s₃} + } + where + open Cartesian (Setoids-Cartesian {ℓ} {ℓ}) using () renaming (products to prod) + open BinaryProducts prod using () renaming (assocʳ to ×-assocʳ) + open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using () renaming (products to 0ℓ-products) + open BinaryProducts 0ℓ-products using (×-assoc; assocˡ; assocʳ) + + open import Categories.Morphism.Reasoning 0ℓ-Setoids-×.U using (switch-tofromʳ) + open import Categories.Functor.Monoidal.Symmetric using (module Lax) + module Lax₂ = Lax Nat,+,0 0ℓ-Setoids-× + module Pull,++,[] = Strong.SymmetricMonoidalFunctor Pull,++,[] + open import Functor.Monoidal.Strong.Properties Pull,++,[].monoidalFunctor using (associativity-inv) + module Push,++,[] = Lax₂.SymmetricMonoidalFunctor Push,++,[] + + +-assocℓ : Fin ((n + m) + o) → Fin (n + (m + o)) + +-assocℓ = +-assocˡ {n} {m} {o} + + opaque + + unfolding _~_ + + associativity-inv-~ : splitₛ ×-function Id (Values o) ∙ splitₛ ∙ Pull₁ +-assocℓ ~ assocʳ ∙ Id (Values n) ×-function splitₛ ∙ splitₛ + associativity-inv-~ {i} = associativity-inv {n} {m} {o} {i} + + associativity-~ : Push₁ (+-assocˡ {n} {m} {o}) ∙ ++ₛ ∙ ++ₛ ×-function Id (Values o) ~ ++ₛ ∙ Id (Values n) ×-function ++ₛ ∙ assocˡ + associativity-~ {i} = Push,++,[].associativity {n} {m} {o} {i} + + sym-split-assoc-~ : assocʳ ∙ Id (Values n) ×-function splitₛ ∙ splitₛ ~ splitₛ ×-function Id (Values o) ∙ splitₛ ∙ Pull₁ +-assocℓ + sym-split-assoc-~ = sym-~ associativity-inv-~ + + sym-++-assoc-~ : ++ₛ ∙ Id (Values n) ×-function ++ₛ ∙ assocˡ ~ Push₁ (+-assocˡ {n} {m} {o}) ∙ ++ₛ ∙ ++ₛ ×-function Id (Values o) + sym-++-assoc-~ = sym-~ associativity-~ + + opaque + + unfolding _~_ + + sym-split-assoc : assocʳ ∙ Id (Values n) ×-function splitₛ ∙ splitₛ ≈ splitₛ ×-function Id (Values o) ∙ splitₛ ∙ Pull₁ +-assocℓ + sym-split-assoc {i} = sym-split-assoc-~ {i} + + sym-++-assoc : ++ₛ ∙ Id (Values n) ×-function ++ₛ ∙ assocˡ ≈ Push₁ (+-assocˡ {n} {m} {o}) ∙ ++ₛ ∙ ++ₛ ×-function Id (Values o) + sym-++-assoc {i} = sym-++-assoc-~ + + module X = System X + module Y = System Y + module Z = System Z + +open import Function.Base using (id) +Sys-unitaryˡ-≤ : (X : System n) → ≤-System (map id (⊗ (discrete , X))) X +Sys-unitaryˡ-≤ X = record + { ⇒S = proj₂ₛ + ; ≗-fₛ = λ i (_ , s) → X.refl + ; ≗-fₒ = λ (_ , s) → Push-identity + } + where + module X = System X + +Sys-unitaryˡ-≥ : (X : System n) → ≤-System X (map id (⊗ (discrete , X))) +Sys-unitaryˡ-≥ {n} X = record + { ⇒S = < Const.function X.S SingletonSetoid tt , Id X.S >ₛ + ; ≗-fₛ = λ i s → tt , X.refl + ; ≗-fₒ = λ s → Equiv.sym {x = Push₁ id} {Id (Values n)} Push-identity + } + where + module X = System X + open SymmetricMonoidalCategory 0ℓ-Setoids-× using (module Equiv) + +open import Data.Vec.Functional using (_++_) + +Sys-unitaryʳ-≤ : (X : System n) → ≤-System (map (id ++ (λ ())) (⊗ {n} {0} (X , discrete))) X +Sys-unitaryʳ-≤ {n} X = record + { ⇒S = proj₁ₛ + ; ≗-fₛ = λ i (s , _) → cong (X.fₛ ∙ proj₁ₛ {B = SingletonSetoid {0ℓ}}) (unitaryʳ-inv {n} {i}) + ; ≗-fₒ = λ (s , _) → Push,++,[].unitaryʳ {n} {X.fₒ′ s , tt} + } + where + module X = System X + module Pull,++,[] = Strong.SymmetricMonoidalFunctor Pull,++,[] + open import Functor.Monoidal.Strong.Properties Pull,++,[].monoidalFunctor using (unitaryʳ-inv; module Shorthands) + open import Categories.Functor.Monoidal.Symmetric Nat,+,0 0ℓ-Setoids-× using (module Lax) + module Push,++,[] = Lax.SymmetricMonoidalFunctor Push,++,[] + +Sys-unitaryʳ-≥ : (X : System n) → ≤-System X (map (id ++ (λ ())) (⊗ {n} {0} (X , discrete))) +Sys-unitaryʳ-≥ {n} X = record + { ⇒S = < Id X.S , Const.function X.S SingletonSetoid tt >ₛ + ; ≗-fₛ = λ i s → + cong + (X.fₛ ×-⇒ Const.function (Values 0) (SingletonSetoid ⇒ₛ SingletonSetoid) (Id (SingletonSetoid {ℓ} {ℓ})) ∙ Id (Values n) ×-function ε⇒) + sym-split-unitaryʳ + {s , tt} + ; ≗-fₒ = λ s → sym-++-unitaryʳ {X.fₒ′ s , tt} + } + where + module X = System X + module Pull,++,[] = Strong.SymmetricMonoidalFunctor Pull,++,[] + open import Functor.Monoidal.Strong.Properties Pull,++,[].monoidalFunctor using (unitaryʳ-inv; module Shorthands) + open import Categories.Functor.Monoidal.Symmetric Nat,+,0 0ℓ-Setoids-× using (module Lax) + module Push,++,[] = Lax.SymmetricMonoidalFunctor Push,++,[] + import Categories.Category.Monoidal.Utilities 0ℓ-Setoids-×.monoidal as ⊗-Util + + open ⊗-Util.Shorthands using (ρ⇐) + open Shorthands using (ε⇐; ε⇒) + + sym-split-unitaryʳ + : ρ⇐ ≈ Id (Values n) ×-function ε⇐ ∙ splitₛ ∙ Pull₁ (id ++ (λ ())) + sym-split-unitaryʳ = + 0ℓ-Setoids-×.Equiv.sym + {Values n} + {Values n ×ₛ SingletonSetoid} + {Id (Values n) ×-function ε⇐ ∙ splitₛ ∙ Pull₁ (id ++ (λ ()))} + {ρ⇐} + (unitaryʳ-inv {n}) + + sym-++-unitaryʳ : proj₁ₛ {B = SingletonSetoid {0ℓ} {0ℓ}} ≈ Push₁ (id ++ (λ ())) ∙ ++ₛ ∙ Id (Values n) ×-function ε⇒ + sym-++-unitaryʳ = + 0ℓ-Setoids-×.Equiv.sym + {Values n ×ₛ SingletonSetoid} + {Values n} + {Push₁ (id ++ (λ ())) ∙ ++ₛ ∙ Id (Values n) ×-function ε⇒} + {proj₁ₛ} + (Push,++,[].unitaryʳ {n}) + +Sys-braiding-compat-≤ + : (X : System n) + (Y : System m) + → ≤-System (map (+-swap {m} {n}) (⊗ (X , Y))) (⊗ (Y , X)) +Sys-braiding-compat-≤ {n} {m} X Y = record + { ⇒S = swapₛ + ; ≗-fₛ = λ i (s₁ , s₂) → cong (Y.fₛ ×-⇒ X.fₛ ∙ swapₛ) (braiding-compat-inv {m} {n} {i}) {s₂ , s₁} + ; ≗-fₒ = λ (s₁ , s₂) → Push,++,[].braiding-compat {n} {m} {X.fₒ′ s₁ , Y.fₒ′ s₂} + } + where + module X = System X + module Y = System Y + module Pull,++,[] = SymmetricMonoidalFunctor Pull,++,[] + module Pull,++,[]B = BraidedMonoidalFunctor (record { isBraidedMonoidal = Pull,++,[].isBraidedMonoidal }) + open import Functor.Monoidal.Braided.Strong.Properties Pull,++,[].braidedMonoidalFunctor using (braiding-compat-inv) + open import Categories.Functor.Monoidal.Symmetric Nat,+,0 0ℓ-Setoids-× using (module Lax) + module Push,++,[] = Lax.SymmetricMonoidalFunctor Push,++,[] + +Sys-braiding-compat-≥ + : (X : System n) + (Y : System m) + → ≤-System (⊗ (Y , X)) (map (+-swap {m} {n}) (⊗ (X , Y))) +Sys-braiding-compat-≥ {n} {m} X Y = record + { ⇒S = swapₛ + ; ≗-fₛ = λ i (s₂ , s₁) → cong (X.fₛ ×-⇒ Y.fₛ) (sym-braiding-compat-inv {i}) + ; ≗-fₒ = λ (s₂ , s₁) → sym-braiding-compat-++ {X.fₒ′ s₁ , Y.fₒ′ s₂} + } + where + module X = System X + module Y = System Y + module Pull,++,[] = SymmetricMonoidalFunctor Pull,++,[] + module Pull,++,[]B = BraidedMonoidalFunctor (record { isBraidedMonoidal = Pull,++,[].isBraidedMonoidal }) + open import Functor.Monoidal.Braided.Strong.Properties Pull,++,[].braidedMonoidalFunctor using (braiding-compat-inv) + open import Categories.Functor.Monoidal.Symmetric Nat,+,0 0ℓ-Setoids-× using (module Lax) + module Push,++,[] = Lax.SymmetricMonoidalFunctor Push,++,[] + + sym-braiding-compat-inv : swapₛ ∙ splitₛ {m} ≈ splitₛ ∙ Pull₁ (+-swap {m} {n}) + sym-braiding-compat-inv {i} = + 0ℓ-Setoids-×.Equiv.sym + {Values (m + n)} + {Values n ×ₛ Values m} + {splitₛ ∙ Pull₁ (+-swap {m} {n})} + {swapₛ ∙ splitₛ {m}} + (λ {j} → braiding-compat-inv {m} {n} {j}) {i} + + sym-braiding-compat-++ : ++ₛ {m} ∙ swapₛ ≈ Push₁ (+-swap {m} {n}) ∙ ++ₛ + sym-braiding-compat-++ {i} = + 0ℓ-Setoids-×.Equiv.sym + {Values n ×ₛ Values m} + {Values (m + n)} + {Push₁ (+-swap {m} {n}) ∙ ++ₛ} + {++ₛ {m} ∙ swapₛ} + (Push,++,[].braiding-compat {n} {m}) + +open import Categories.Functor.Monoidal.Symmetric Nat,+,0 Setoids-× using (module Lax) +open Lax.SymmetricMonoidalFunctor + +Sys,⊗,ε : Lax.SymmetricMonoidalFunctor +Sys,⊗,ε .F = Sys +Sys,⊗,ε .isBraidedMonoidal = record + { isMonoidal = record + { ε = Sys-ε + ; ⊗-homo = ⊗-homomorphism + ; associativity = λ { {n} {m} {o} {(X , Y), Z} → ⊗-assoc-≤ X Y Z , ⊗-assoc-≥ X Y Z } + ; unitaryˡ = λ { {n} {_ , X} → Sys-unitaryˡ-≤ X , Sys-unitaryˡ-≥ X } + ; unitaryʳ = λ { {n} {X , _} → Sys-unitaryʳ-≤ X , Sys-unitaryʳ-≥ X } + } + ; braiding-compat = λ { {n} {m} {X , Y} → Sys-braiding-compat-≤ X Y , Sys-braiding-compat-≥ X Y } + } diff --git a/Functor/Monoidal/Strong/Properties.agda b/Functor/Monoidal/Strong/Properties.agda new file mode 100644 index 0000000..9eb7579 --- /dev/null +++ b/Functor/Monoidal/Strong/Properties.agda @@ -0,0 +1,104 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level) +open import Categories.Category.Monoidal using (MonoidalCategory) +open import Categories.Functor.Monoidal using (StrongMonoidalFunctor) + +module Functor.Monoidal.Strong.Properties + {o o′ ℓ ℓ′ e e′ : Level} + {C : MonoidalCategory o ℓ e} + {D : MonoidalCategory o′ ℓ′ e′} + (F,φ,ε : StrongMonoidalFunctor C D) where + +import Categories.Category.Monoidal.Utilities as ⊗-Utilities +import Categories.Category.Construction.Core as Core + +open import Categories.Functor.Monoidal using (StrongMonoidalFunctor) +open import Categories.Functor.Properties using ([_]-resp-≅) + +private + + module C where + open MonoidalCategory C public + open ⊗-Utilities.Shorthands monoidal public using (α⇐; λ⇐; ρ⇐) + + module D where + open MonoidalCategory D public + open ⊗-Utilities.Shorthands monoidal using (α⇐; λ⇐; ρ⇐) public + open Core.Shorthands U using (_∘ᵢ_; idᵢ; _≈ᵢ_; ⌞_⌟; to-≈; _≅_; module HomReasoningᵢ) public + open ⊗-Utilities monoidal using (_⊗ᵢ_) public + +open D + +open StrongMonoidalFunctor F,φ,ε + +private + + variable + X Y Z : C.Obj + + α : {A B C : Obj} → (A ⊗₀ B) ⊗₀ C ≅ A ⊗₀ (B ⊗₀ C) + α = associator + + Fα : F₀ ((X C.⊗₀ Y) C.⊗₀ Z) ≅ F₀ (X C.⊗₀ (Y C.⊗₀ Z)) + Fα = [ F ]-resp-≅ C.associator + + λ- : {A : Obj} → unit ⊗₀ A ≅ A + λ- = unitorˡ + + Fλ : F₀ (C.unit C.⊗₀ X) ≅ F₀ X + Fλ = [ F ]-resp-≅ C.unitorˡ + + ρ : {A : Obj} → A ⊗₀ unit ≅ A + ρ = unitorʳ + + Fρ : F₀ (X C.⊗₀ C.unit) ≅ F₀ X + Fρ = [ F ]-resp-≅ C.unitorʳ + + φ : F₀ X ⊗₀ F₀ Y ≅ F₀ (X C.⊗₀ Y) + φ = ⊗-homo.FX≅GX + +module Shorthands where + + φ⇒ : F₀ X ⊗₀ F₀ Y ⇒ F₀ (X C.⊗₀ Y) + φ⇒ = ⊗-homo.⇒.η _ + + φ⇐ : F₀ (X C.⊗₀ Y) ⇒ F₀ X ⊗₀ F₀ Y + φ⇐ = ⊗-homo.⇐.η _ + + ε⇒ : unit ⇒ F₀ C.unit + ε⇒ = ε.from + + ε⇐ : F₀ C.unit ⇒ unit + ε⇐ = ε.to + +open Shorthands +open HomReasoning + +associativityᵢ : Fα {X} {Y} {Z} ∘ᵢ φ ∘ᵢ φ ⊗ᵢ idᵢ ≈ᵢ φ ∘ᵢ idᵢ ⊗ᵢ φ ∘ᵢ α +associativityᵢ = ⌞ associativity ⌟ + +associativity-inv : φ⇐ ⊗₁ id ∘ φ⇐ ∘ F₁ (C.α⇐ {X} {Y} {Z}) ≈ α⇐ ∘ id ⊗₁ φ⇐ ∘ φ⇐ +associativity-inv = begin + φ⇐ ⊗₁ id ∘ φ⇐ ∘ F₁ C.α⇐ ≈⟨ sym-assoc ⟩ + (φ⇐ ⊗₁ id ∘ φ⇐) ∘ F₁ C.α⇐ ≈⟨ to-≈ associativityᵢ ⟩ + (α⇐ ∘ id ⊗₁ φ⇐) ∘ φ⇐ ≈⟨ assoc ⟩ + α⇐ ∘ id ⊗₁ φ⇐ ∘ φ⇐ ∎ + +unitaryˡᵢ : Fλ {X} ∘ᵢ φ ∘ᵢ ε ⊗ᵢ idᵢ ≈ᵢ λ- +unitaryˡᵢ = ⌞ unitaryˡ ⌟ + +unitaryˡ-inv : ε⇐ ⊗₁ id ∘ φ⇐ ∘ F₁ (C.λ⇐ {X}) ≈ λ⇐ +unitaryˡ-inv = begin + ε⇐ ⊗₁ id ∘ φ⇐ ∘ F₁ C.λ⇐ ≈⟨ sym-assoc ⟩ + (ε⇐ ⊗₁ id ∘ φ⇐) ∘ F₁ C.λ⇐ ≈⟨ to-≈ unitaryˡᵢ ⟩ + λ⇐ ∎ + +unitaryʳᵢ : Fρ {X} ∘ᵢ φ ∘ᵢ idᵢ ⊗ᵢ ε ≈ᵢ ρ +unitaryʳᵢ = ⌞ unitaryʳ ⌟ + +unitaryʳ-inv : id ⊗₁ ε⇐ ∘ φ⇐ ∘ F₁ (C.ρ⇐ {X}) ≈ ρ⇐ +unitaryʳ-inv = begin + id ⊗₁ ε⇐ ∘ φ⇐ ∘ F₁ C.ρ⇐ ≈⟨ sym-assoc ⟩ + (id ⊗₁ ε⇐ ∘ φ⇐) ∘ F₁ C.ρ⇐ ≈⟨ to-≈ unitaryʳᵢ ⟩ + ρ⇐ ∎ |