diff options
| -rw-r--r-- | Functor/Instance/Nat/Circ.agda | 64 | ||||
| -rw-r--r-- | Functor/Properties.agda | 77 |
2 files changed, 121 insertions, 20 deletions
diff --git a/Functor/Instance/Nat/Circ.agda b/Functor/Instance/Nat/Circ.agda index 36d726d..88a6ec6 100644 --- a/Functor/Instance/Nat/Circ.agda +++ b/Functor/Instance/Nat/Circ.agda @@ -1,32 +1,56 @@ {-# OPTIONS --without-K --safe #-} -open import Level using (Level; _⊔_; 0ℓ) +open import Level using (Level) module Functor.Instance.Nat.Circ {ℓ : Level} where -open import Data.Circuit {ℓ} using (Circuitₛ; mapₛ; mkCircuitₛ) -open import Data.Nat using (ℕ) -open import Relation.Binary using (Setoid) -open import Function using (Func) -open import Categories.Functor using (Functor; _∘F_) -open import Categories.Category.Instance.Setoids using (Setoids) +import Data.List.Relation.Binary.Permutation.Setoid as ↭ + open import Categories.Category.Instance.Nat using (Nat) -open import Data.Fin using (Fin) +open import Categories.Functor using (Functor; _∘F_) +open import Categories.Morphism.Notation using (_[_≅_]) +open import Category.Instance.Setoids.SymmetricMonoidal {ℓ} {ℓ} using (Setoids-×) +open import Data.Circuit using (mk≈) +open import Data.Circuit {ℓ} using (Circuitₛ; mkCircuitₛ; edgesₛ) open import Data.Circuit.Gate using (Gates) +open import Data.Nat using (ℕ) +open import Data.Opaque.Multiset using (Multisetₛ) +open import Data.Product using (proj₁; proj₂; Σ-syntax) +open import Functor.Free.Instance.CMonoid using (Free) open import Functor.Instance.Nat.Edge {ℓ} Gates using (Edge) -open import Functor.Instance.Multiset using (Multiset) +open import Functor.Properties using (define-by-pw-iso) + +open import Category.Construction.CMonoids Setoids-×.symmetric using (CMonoids) +open import Category.Construction.CMonoids.Properties Setoids-×.symmetric using (transport-by-iso) +open import Object.Monoid.Commutative Setoids-×.symmetric using (CommutativeMonoid) + +Edges : Functor Nat CMonoids +Edges = Free ∘F Edge + +module Edges = Functor Edges +module Edge = Functor Edge + +opaque + unfolding Multisetₛ + Edges≅Circₛ : (n : ℕ) → Setoids-×.U [ Multisetₛ (Edge.₀ n) ≅ Circuitₛ n ] + Edges≅Circₛ n = record + { from = mkCircuitₛ + ; to = edgesₛ + ; iso = record + { isoˡ = ↭.↭-refl (Edge.₀ n) + ; isoʳ = mk≈ (↭.↭-refl (Edge.₀ n)) + } + } -Multiset∘Edge : Functor Nat (Setoids ℓ ℓ) -Multiset∘Edge = Multiset ∘F Edge +private + Edges≅ : (n : ℕ) → Σ[ M ∈ CommutativeMonoid ] CMonoids [ Edges.₀ n ≅ M ] + Edges≅ n = transport-by-iso (Edges.₀ n) (Edges≅Circₛ n) -module Multiset∘Edge = Functor Multiset∘Edge +Circuitₘ : ℕ → CommutativeMonoid +Circuitₘ n = proj₁ (Edges≅ n) -open Func -open Functor +Edges≅Circₘ : (n : ℕ) → CMonoids [ Edges.₀ n ≅ Circuitₘ n ] +Edges≅Circₘ n = proj₂ (Edges≅ n) -Circ : Functor Nat (Setoids ℓ ℓ) -Circ .F₀ = Circuitₛ -Circ .F₁ = mapₛ -Circ .identity = cong mkCircuitₛ Multiset∘Edge.identity -Circ .homomorphism {f = f} {g = g} = cong mkCircuitₛ (Multiset∘Edge.homomorphism {f = f} {g = g}) -Circ .F-resp-≈ f≗g = cong mkCircuitₛ (Multiset∘Edge.F-resp-≈ f≗g) +Circ : Functor Nat CMonoids +Circ = proj₁ (define-by-pw-iso Edges Circuitₘ Edges≅Circₘ) diff --git a/Functor/Properties.agda b/Functor/Properties.agda new file mode 100644 index 0000000..1bd3ba6 --- /dev/null +++ b/Functor/Properties.agda @@ -0,0 +1,77 @@ +{-# OPTIONS --without-K --safe #-} + +module Functor.Properties where + +import Categories.Morphism.Reasoning as ⇒-Reasoning + +open import Categories.Category using (Category; _[_,_]) +open import Level using (Level) +open import Categories.Morphism.Notation using (_[_≅_]) +open import Categories.Morphism using (_≅_) +open import Categories.Functor using (Functor) +open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; niHelper) +open import Data.Product using (Σ-syntax; _,_) + +module _ + {o o′ ℓ ℓ′ e e′ : Level} + {𝒞 : Category o ℓ e} + {𝒟 : Category o′ ℓ′ e′} + where + + module 𝒞 = Category 𝒞 + module 𝒟 = Category 𝒟 + + define-by-pw-iso + : (F : Functor 𝒞 𝒟) + (G₀ : 𝒞.Obj → 𝒟.Obj) + → (let module F = Functor F) + → ((X : 𝒞.Obj) → 𝒟 [ F.₀ X ≅ G₀ X ]) + → Σ[ G ∈ Functor 𝒞 𝒟 ] F ≃ G + define-by-pw-iso F G₀ α = G , F≃G + where + open Functor + module F = Functor F + open 𝒟 + open _≅_ + open HomReasoning + open ⇒-Reasoning 𝒟 + + G-homo + : {X Y Z : 𝒞.Obj} + → (f : 𝒞 [ X , Y ]) + → (g : 𝒞 [ Y , Z ]) + → from (α Z) ∘ F.₁ (g 𝒞.∘ f) ∘ to (α X) + ≈ (from (α Z) ∘ F.₁ g ∘ to (α Y)) ∘ from (α Y) ∘ F.₁ f ∘ to (α X) + G-homo {X} {Y} {Z} f g = begin + from (α Z) ∘ F.₁ (g 𝒞.∘ f) ∘ to (α X) ≈⟨ extendʳ (pushʳ F.homomorphism) ⟩ + (from (α Z) ∘ F.₁ g) ∘ F.₁ f ∘ to (α X) ≈⟨ extendˡ (pushˡ (insertʳ (isoˡ (α Y)))) ⟩ + (from (α Z) ∘ F.₁ g ∘ to (α Y)) ∘ from (α Y) ∘ F.₁ f ∘ to (α X) ∎ + + G-resp-≈ + : {X Y : 𝒞.Obj} + → {f g : 𝒞 [ X , Y ]} + → f 𝒞.≈ g + → from (α Y) ∘ F.₁ f ∘ to (α X) + ≈ from (α Y) ∘ F.₁ g ∘ to (α X) + G-resp-≈ f≈g = refl⟩∘⟨ F.F-resp-≈ f≈g ⟩∘⟨refl + + G-identity : {X : 𝒞.Obj} → from (α X) ∘ F.₁ 𝒞.id ∘ to (α X) ≈ id + G-identity {X} = refl⟩∘⟨ (F.identity ⟩∘⟨refl ○ identityˡ) ○ isoʳ (α X) + + G : Functor 𝒞 𝒟 + G .F₀ = G₀ + G .F₁ {X} {Y} f = from (α Y) ∘ F.₁ f ∘ to (α X) + G .identity {X} = G-identity + G .homomorphism {f = f} {g} = G-homo f g + G .F-resp-≈ = G-resp-≈ + + commute : {X Y : 𝒞.Obj} (f : 𝒞 [ X , Y ]) → from (α Y) ∘ F.F₁ f ≈ (from (α Y) ∘ F.₁ f ∘ to (α X)) ∘ from (α X) + commute {X} {Y} f = pushʳ (insertʳ (isoˡ (α X))) + + F≃G : F ≃ G + F≃G = niHelper record + { η = λ X → from (α X) + ; η⁻¹ = λ X → to (α X) + ; commute = commute + ; iso = λ X → iso (α X) + } |