diff options
Diffstat (limited to 'Functor')
| -rw-r--r-- | Functor/Instance/Nat/Circ.agda | 22 | ||||
| -rw-r--r-- | Functor/Instance/Nat/Edge.agda | 20 | ||||
| -rw-r--r-- | Functor/Instance/Nat/System.agda | 10 | ||||
| -rw-r--r-- | Functor/Monoidal/Construction/ListOf.agda | 4 | ||||
| -rw-r--r-- | Functor/Monoidal/Construction/MultisetOf.agda | 4 | ||||
| -rw-r--r-- | Functor/Monoidal/Instance/Nat/System.agda | 36 |
6 files changed, 46 insertions, 50 deletions
diff --git a/Functor/Instance/Nat/Circ.agda b/Functor/Instance/Nat/Circ.agda index d5bcc9b..09bc495 100644 --- a/Functor/Instance/Nat/Circ.agda +++ b/Functor/Instance/Nat/Circ.agda @@ -2,9 +2,9 @@ open import Level using (Level; _⊔_; 0ℓ) -module Functor.Instance.Nat.Circ {c ℓ : Level} where +module Functor.Instance.Nat.Circ {ℓ : Level} where -open import Data.Circuit {c} {ℓ} using (Circuitₛ; mapₛ; mkCircuitₛ) +open import Data.Circuit {ℓ} using (Circuitₛ; mapₛ; mkCircuitₛ) open import Data.Nat using (ℕ) open import Relation.Binary using (Setoid) open import Function using (Func) @@ -13,20 +13,20 @@ open import Categories.Category.Instance.Setoids using (Setoids) open import Categories.Category.Instance.Nat using (Nat) open import Data.Fin using (Fin) open import Data.Circuit.Gate using (Gates) -open import Functor.Instance.Nat.Edge Gates using (Edge) -open import Functor.Instance.List using (List) +open import Functor.Instance.Nat.Edge {ℓ} Gates using (Edge) +open import Functor.Instance.Multiset using (Multiset) -List∘Edge : Functor Nat (Setoids 0ℓ 0ℓ) -List∘Edge = List ∘F Edge +Multiset∘Edge : Functor Nat (Setoids ℓ ℓ) +Multiset∘Edge = Multiset ∘F Edge -module List∘Edge = Functor List∘Edge +module Multiset∘Edge = Functor Multiset∘Edge open Func open Functor -Circ : Functor Nat (Setoids c ℓ) +Circ : Functor Nat (Setoids ℓ ℓ) Circ .F₀ = Circuitₛ Circ .F₁ = mapₛ -Circ .identity = cong mkCircuitₛ List∘Edge.identity -Circ .homomorphism = cong mkCircuitₛ List∘Edge.homomorphism -Circ .F-resp-≈ f≗g = cong mkCircuitₛ (List∘Edge.F-resp-≈ f≗g) +Circ .identity = cong mkCircuitₛ Multiset∘Edge.identity +Circ .homomorphism = cong mkCircuitₛ Multiset∘Edge.homomorphism +Circ .F-resp-≈ f≗g = cong mkCircuitₛ (Multiset∘Edge.F-resp-≈ f≗g) diff --git a/Functor/Instance/Nat/Edge.agda b/Functor/Instance/Nat/Edge.agda index f8d47c2..5de8f84 100644 --- a/Functor/Instance/Nat/Edge.agda +++ b/Functor/Instance/Nat/Edge.agda @@ -1,8 +1,9 @@ {-# OPTIONS --without-K --safe #-} open import Data.Hypergraph.Label using (HypergraphLabel) +open import Level using (Level; 0ℓ) -module Functor.Instance.Nat.Edge (HL : HypergraphLabel) where +module Functor.Instance.Nat.Edge {ℓ : Level} (HL : HypergraphLabel) where import Data.Vec as Vec import Data.Vec.Properties as VecProps @@ -11,10 +12,9 @@ open import Categories.Category.Instance.Nat using (Nat) open import Categories.Category.Instance.Setoids using (Setoids) open import Categories.Functor using (Functor) open import Data.Fin using (Fin) -open import Data.Hypergraph.Edge HL as Edge using (Edgeₛ; map; _≈_) +open import Data.Hypergraph.Edge {ℓ} HL as Edge using (Edgeₛ; map; mapₛ; _≈_) open import Data.Nat using (ℕ) -open import Data.Vec.Relation.Binary.Equality.Cast using (≈-cong′; ≈-reflexive) -open import Level using (0ℓ) +open import Data.Vec.Relation.Binary.Equality.Cast using (≈-reflexive) open import Function using (id; _∘_; Func; _⟶ₛ_) open import Relation.Binary using (Setoid) open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_) @@ -26,14 +26,6 @@ open Edge._≈_ open Func open Functor -Edge₁ : {n m : ℕ} → (Fin n → Fin m) → Edgeₛ n ⟶ₛ Edgeₛ m -Edge₁ f .to = map f -Edge₁ f .cong x≈y = record - { ≡arity = ≡arity x≈y - ; ≡label = ≡label x≈y - ; ≡ports = ≈-cong′ (Vec.map f) (≡ports x≈y) - } - map-id : {v : ℕ} {e : Edge.Edge v} → map id e ≈ e map-id .≡arity = ≡.refl map-id .≡label = HL.≈-reflexive ≡.refl @@ -59,9 +51,9 @@ map-resp-≗ f≗g .≡arity = ≡.refl map-resp-≗ f≗g .≡label = HL.≈-reflexive ≡.refl map-resp-≗ f≗g {e} .≡ports = ≈-reflexive (VecProps.map-cong f≗g (ports e)) -Edge : Functor Nat (Setoids 0ℓ 0ℓ) +Edge : Functor Nat (Setoids ℓ ℓ) Edge .F₀ = Edgeₛ -Edge .F₁ = Edge₁ +Edge .F₁ = mapₛ Edge .identity = map-id Edge .homomorphism = map-∘ _ _ Edge .F-resp-≈ = map-resp-≗ diff --git a/Functor/Instance/Nat/System.agda b/Functor/Instance/Nat/System.agda index 730f90d..00451ad 100644 --- a/Functor/Instance/Nat/System.agda +++ b/Functor/Instance/Nat/System.agda @@ -1,7 +1,8 @@ {-# OPTIONS --without-K --safe #-} -module Functor.Instance.Nat.System {ℓ} where +module Functor.Instance.Nat.System where +open import Level using (suc; 0ℓ) open import Categories.Category.Instance.Nat using (Nat) open import Categories.Category.Instance.Setoids using (Setoids) open import Categories.Functor.Core using (Functor) @@ -9,14 +10,13 @@ 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 {suc 0ℓ} 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 @@ -29,7 +29,7 @@ open Functor private variable A B C : ℕ -map : (Fin A → Fin B) → System {ℓ} A → System B +map : (Fin A → Fin B) → System A → System B map f X = record { S = S ; fₛ = fₛ ∙ Pull₁ f @@ -88,7 +88,7 @@ System-resp-≈ {A} {B} {f = f} {g} f≗g {X} = both f≗g , both (≡.sym ∘ f 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 : Functor Nat (Setoids (suc 0ℓ) (suc 0ℓ)) Sys .F₀ = Systemₛ Sys .F₁ = System₁ Sys .identity = id-x≤x , x≤id-x diff --git a/Functor/Monoidal/Construction/ListOf.agda b/Functor/Monoidal/Construction/ListOf.agda index 476939e..23c6ba8 100644 --- a/Functor/Monoidal/Construction/ListOf.agda +++ b/Functor/Monoidal/Construction/ListOf.agda @@ -8,9 +8,9 @@ open import Categories.Functor using (Functor) renaming (_∘F_ to _∙_) open import Level using (Level) module Functor.Monoidal.Construction.ListOf - {o ℓ e : Level} + {o o′ ℓ ℓ′ e e′ : Level} {𝒞 : CocartesianCategory o ℓ e} - {S : MonoidalCategory o ℓ e} + {S : MonoidalCategory o′ ℓ′ e′} (let module 𝒞 = CocartesianCategory 𝒞) (let module S = MonoidalCategory S) (G : Functor 𝒞.U S.U) diff --git a/Functor/Monoidal/Construction/MultisetOf.agda b/Functor/Monoidal/Construction/MultisetOf.agda index 6862b84..eca7b3a 100644 --- a/Functor/Monoidal/Construction/MultisetOf.agda +++ b/Functor/Monoidal/Construction/MultisetOf.agda @@ -10,9 +10,9 @@ open import Category.Construction.CMonoids using (CMonoids) open import Level using (Level) module Functor.Monoidal.Construction.MultisetOf - {o ℓ e : Level} + {o o′ ℓ ℓ′ e e′ : Level} {𝒞 : CocartesianCategory o ℓ e} - {S : SymmetricMonoidalCategory o ℓ e} + {S : SymmetricMonoidalCategory o′ ℓ′ e′} (let module 𝒞 = CocartesianCategory 𝒞) (let module S = SymmetricMonoidalCategory S) (G : Functor 𝒞.U S.U) diff --git a/Functor/Monoidal/Instance/Nat/System.agda b/Functor/Monoidal/Instance/Nat/System.agda index 1b3bb34..d86588f 100644 --- a/Functor/Monoidal/Instance/Nat/System.agda +++ b/Functor/Monoidal/Instance/Nat/System.agda @@ -1,25 +1,25 @@ {-# OPTIONS --without-K --safe #-} -open import Level using (Level; 0ℓ; suc) - -module Functor.Monoidal.Instance.Nat.System {ℓ : Level} where +module Functor.Monoidal.Instance.Nat.System where open import Function.Construct.Identity using () renaming (function to Id) import Function.Construct.Constant as Const +open import Level using (0ℓ; suc; Level) + 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 Category.Instance.Setoids.SymmetricMonoidal {suc 0ℓ} {suc 0ℓ} 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 {suc 0ℓ} 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 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) @@ -36,12 +36,12 @@ module _ where discrete .fₛ = Const.function (Values 0) (SingletonSetoid ⇒ₛ SingletonSetoid) (Id SingletonSetoid) discrete .fₒ = Const.function SingletonSetoid (Values 0) [] -Sys-ε : SingletonSetoid {suc ℓ} {ℓ} ⟶ₛ Systemₛ 0 +Sys-ε : SingletonSetoid {suc 0ℓ} {suc 0ℓ} ⟶ₛ 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 Cartesian (Setoids-Cartesian {suc 0ℓ} {suc 0ℓ}) using (products) open import Categories.Category.BinaryProducts using (module BinaryProducts) open BinaryProducts products using (-×-) open import Categories.Functor using (_∘F_) @@ -216,12 +216,14 @@ System-⊗-≥ {n} {n′} {m} {m′} X Y f g = record 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 Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using () renaming (products to prod) open BinaryProducts prod using () renaming (assocˡ to ×-assocˡ) module Pull,++,[] = SymmetricMonoidalFunctor Pull,++,[] + Pull,++,[]B : BraidedMonoidalFunctor + Pull,++,[]B = record { isBraidedMonoidal = Pull,++,[].isBraidedMonoidal } module Pull,++,[]B = BraidedMonoidalFunctor (record { isBraidedMonoidal = Pull,++,[].isBraidedMonoidal }) - open import Functor.Monoidal.Braided.Strong.Properties Pull,++,[].braidedMonoidalFunctor using (associativity-inv) + open import Functor.Monoidal.Braided.Strong.Properties Pull,++,[]B using (associativity-inv) module X = System X module Y = System Y @@ -238,7 +240,7 @@ System-⊗-≥ {n} {n′} {m} {m′} X Y f g = record ; ≗-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 Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) 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ʳ) @@ -323,7 +325,7 @@ 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 ε⇒) + (X.fₛ ×-⇒ Const.function (Values 0) (SingletonSetoid ⇒ₛ SingletonSetoid) (Id (SingletonSetoid {suc 0ℓ} {0ℓ})) ∙ Id (Values n) ×-function ε⇒) sym-split-unitaryʳ {s , tt} ; ≗-fₒ = λ s → sym-++-unitaryʳ {X.fₒ′ s , tt} @@ -371,8 +373,9 @@ Sys-braiding-compat-≤ {n} {m} X Y = record 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) + Pull,++,[]B : BraidedMonoidalFunctor + Pull,++,[]B = record { isBraidedMonoidal = Pull,++,[].isBraidedMonoidal } + open import Functor.Monoidal.Braided.Strong.Properties Pull,++,[]B using (braiding-compat-inv) open import Categories.Functor.Monoidal.Symmetric Nat,+,0 0ℓ-Setoids-× using (module Lax) module Push,++,[] = Lax.SymmetricMonoidalFunctor Push,++,[] @@ -389,8 +392,9 @@ Sys-braiding-compat-≥ {n} {m} X Y = record 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) + Pull,++,[]B : BraidedMonoidalFunctor + Pull,++,[]B = record { isBraidedMonoidal = Pull,++,[].isBraidedMonoidal } + open import Functor.Monoidal.Braided.Strong.Properties Pull,++,[]B using (braiding-compat-inv) open import Categories.Functor.Monoidal.Symmetric Nat,+,0 0ℓ-Setoids-× using (module Lax) module Push,++,[] = Lax.SymmetricMonoidalFunctor Push,++,[] |