diff options
| -rw-r--r-- | Data/Circuit.agda | 10 | ||||
| -rw-r--r-- | Data/Hypergraph.agda | 27 | ||||
| -rw-r--r-- | Data/Hypergraph/Edge.agda | 7 | ||||
| -rw-r--r-- | Functor/Instance/FreeMonoid.agda | 64 | ||||
| -rw-r--r-- | Functor/Instance/List.agda | 14 | ||||
| -rw-r--r-- | Functor/Instance/Nat/Circ.agda | 32 | ||||
| -rw-r--r-- | Functor/Instance/Nat/Edge.agda | 5 | ||||
| -rw-r--r-- | NaturalTransformation/Instance/EmptyList.agda | 23 | ||||
| -rw-r--r-- | NaturalTransformation/Instance/ListAppend.agda | 46 |
9 files changed, 211 insertions, 17 deletions
diff --git a/Data/Circuit.agda b/Data/Circuit.agda index 0be86f9..09dfb2e 100644 --- a/Data/Circuit.agda +++ b/Data/Circuit.agda @@ -12,15 +12,16 @@ open import Data.Fin using (Fin) open import Data.Hypergraph {c} {ℓ} Gates using ( Hypergraph - ; mkHypergraph ; Hypergraphₛ + ; mkHypergraphₛ + ; List∘Edgeₛ ; module Edge - ; normalize + ; mkHypergraph ; _≈_ ; mk≈ ) open import Data.Nat using (ℕ) -open import Relation.Binary using (Rel; Setoid) +open import Relation.Binary using (Setoid) open import Function.Bundles using (Func; _⟶ₛ_) open List using (List) @@ -35,6 +36,9 @@ map f (mkHypergraph edges) = mkHypergraph (List.map (Edge.map f) edges) Circuitₛ : ℕ → Setoid c (c ⊔ ℓ) Circuitₛ = Hypergraphₛ +mkCircuitₛ : {n : ℕ} → List∘Edgeₛ n ⟶ₛ Circuitₛ n +mkCircuitₛ = mkHypergraphₛ + open Func open Edge.Sort using (sort) diff --git a/Data/Hypergraph.agda b/Data/Hypergraph.agda index 2e8498c..18a259b 100644 --- a/Data/Hypergraph.agda +++ b/Data/Hypergraph.agda @@ -6,9 +6,32 @@ open import Data.Hypergraph.Label using (HypergraphLabel) module Data.Hypergraph {c ℓ : Level} (HL : HypergraphLabel) where +import Data.List.Relation.Binary.Pointwise as PW +import Data.Hypergraph.Edge HL as HypergraphEdge +import Function.Reasoning as →-Reasoning +import Relation.Binary.PropositionalEquality as ≡ + open import Data.Hypergraph.Base {c} HL public open import Data.Hypergraph.Setoid {c} {ℓ} HL public - -import Data.Hypergraph.Edge HL as HypergraphEdge +open import Data.Nat using (ℕ) +open import Function using (_∘_; _⟶ₛ_; Func) +open import Level using (0ℓ) +open import Relation.Binary using (Setoid) module Edge = HypergraphEdge + +open Edge using (Edgeₛ; ≈-Edge⇒≡) +open Func + +List∘Edgeₛ : (n : ℕ) → Setoid 0ℓ 0ℓ +List∘Edgeₛ = PW.setoid ∘ Edgeₛ + +mkHypergraphₛ : {n : ℕ} → List∘Edgeₛ n ⟶ₛ Hypergraphₛ n +mkHypergraphₛ .to = mkHypergraph +mkHypergraphₛ {n} .cong ≋-edges = ≋-edges + |> PW.map ≈-Edge⇒≡ + |> PW.Pointwise-≡⇒≡ + |> ≡.cong mkHypergraph + |> Setoid.reflexive (Hypergraphₛ n) + where + open →-Reasoning diff --git a/Data/Hypergraph/Edge.agda b/Data/Hypergraph/Edge.agda index 7d0fa7c..ee32393 100644 --- a/Data/Hypergraph/Edge.agda +++ b/Data/Hypergraph/Edge.agda @@ -25,8 +25,7 @@ open import Data.String using (String; _<+>_) open import Data.Vec.Relation.Binary.Pointwise.Inductive using (≡⇒Pointwise-≡; Pointwise-≡⇒≡) open import Data.Vec.Show using () renaming (show to showVec) open import Level using (0ℓ) -open import Relation.Binary.Bundles using (DecTotalOrder; StrictTotalOrder) -open import Relation.Binary.Structures using (IsEquivalence) +open import Relation.Binary using (Setoid; DecTotalOrder; StrictTotalOrder; IsEquivalence) open import Relation.Nullary using (¬_) @@ -89,7 +88,6 @@ record ≈-Edge {n : ℕ} (E E′ : Edge n) : Set where module i≈j = ≈-Edge i≈j module j≈k = ≈-Edge j≈k -open import Relation.Binary using (IsEquivalence) ≈-Edge-IsEquivalence : {v : ℕ} → IsEquivalence (≈-Edge {v}) ≈-Edge-IsEquivalence = record { refl = ≈-Edge-refl @@ -345,3 +343,6 @@ open module STOP′ {v} = STOP (strictTotalOrder {v}) using (decTotalOrder) publ module Sort {v} = ListSort (decTotalOrder {v}) open Sort using (sort) public + +Edgeₛ : (v : ℕ) → Setoid 0ℓ 0ℓ +Edgeₛ v = record { isEquivalence = ≈-Edge-IsEquivalence {v} } diff --git a/Functor/Instance/FreeMonoid.agda b/Functor/Instance/FreeMonoid.agda new file mode 100644 index 0000000..bb26fd4 --- /dev/null +++ b/Functor/Instance/FreeMonoid.agda @@ -0,0 +1,64 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level; _⊔_) + +module Functor.Instance.FreeMonoid {c ℓ : Level} where + +import Categories.Object.Monoid as MonoidObject + +open import Categories.Category.Construction.Monoids using (Monoids) +open import Categories.Category.Instance.Setoids using (Setoids) +open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory) +open import Categories.Functor using (Functor) +open import Categories.NaturalTransformation using (NaturalTransformation) +open import Category.Instance.Setoids.SymmetricMonoidal {c} {c ⊔ ℓ} using (Setoids-×) +open import Data.List.Properties using (++-assoc; ++-identityˡ; ++-identityʳ) +open import Data.Product using (_,_) +open import Function using (_⟶ₛ_) +open import Functor.Instance.List {c} {ℓ} using (List) +open import NaturalTransformation.Instance.EmptyList {c} {ℓ} using (⊤⇒[]) +open import NaturalTransformation.Instance.ListAppend {c} {ℓ} using (++) +open import Relation.Binary using (Setoid) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) + +module List = Functor List +module Setoids-× = SymmetricMonoidalCategory Setoids-× +module ++ = NaturalTransformation ++ +module ⊤⇒[] = NaturalTransformation ⊤⇒[] + +open Functor +open MonoidObject Setoids-×.monoidal using (Monoid; IsMonoid; Monoid⇒) +open IsMonoid + +module _ (X : Setoid c ℓ) where + + private + module X = Setoid X + module ListX = Setoid (List.₀ X) + + ListMonoid : IsMonoid (List.₀ X) + ListMonoid .μ = ++.η X + ListMonoid .η = ⊤⇒[].η X + ListMonoid .assoc {(x , y) , z} = ListX.reflexive (++-assoc x y z) + ListMonoid .identityˡ {_ , x} = ListX.reflexive (++-identityˡ x) + ListMonoid .identityʳ {x , _} = ListX.reflexive (≡.sym (++-identityʳ x)) + +FreeMonoid₀ : (X : Setoid c ℓ) → Monoid +FreeMonoid₀ X = record { isMonoid = ListMonoid X } + +FreeMonoid₁ + : {A B : Setoid c ℓ} + (f : A ⟶ₛ B) + → Monoid⇒ (FreeMonoid₀ A) (FreeMonoid₀ B) +FreeMonoid₁ f = record + { arr = List.₁ f + ; preserves-μ = λ {x,y} → ++.sym-commute f {x,y} + ; preserves-η = ⊤⇒[].commute f + } + +FreeMonoid : Functor (Setoids c ℓ) (Monoids Setoids-×.monoidal) +FreeMonoid .F₀ = FreeMonoid₀ +FreeMonoid .F₁ = FreeMonoid₁ +FreeMonoid .identity {X} = List.identity {X} +FreeMonoid .homomorphism {X} {Y} {Z} {f} {g} = List.homomorphism {X} {Y} {Z} {f} {g} +FreeMonoid .F-resp-≈ {A} {B} {f} {g} = List.F-resp-≈ {A} {B} {f} {g} diff --git a/Functor/Instance/List.agda b/Functor/Instance/List.agda index 05db349..b40670d 100644 --- a/Functor/Instance/List.agda +++ b/Functor/Instance/List.agda @@ -16,7 +16,7 @@ open import Function.Bundles using (Func; _⟶ₛ_; _⟨$⟩_) open import Relation.Binary using (Setoid) open Functor -open Setoid +open Setoid using (reflexive) open Func private @@ -36,15 +36,19 @@ mapₛ : A ⟶ₛ B → Listₛ A ⟶ₛ Listₛ B mapₛ f .to = List.map (to f) mapₛ f .cong = PW.map⁺ (to f) (to f) ∘ PW.map (cong f) -map-id : (xs : ∣ Listₛ A ∣) → PW.Pointwise (_≈_ A) (List.map id xs) xs -map-id {A} = PW.map (reflexive A) ∘ PW.≡⇒Pointwise-≡ ∘ ListProps.map-id +map-id + : (xs : ∣ Listₛ A ∣) + → (open Setoid (Listₛ A)) + → List.map id xs ≈ xs +map-id {A} = reflexive (Listₛ A) ∘ ListProps.map-id List-homo : (f : A ⟶ₛ B) (g : B ⟶ₛ C) → (xs : ∣ Listₛ A ∣) - → PW.Pointwise (_≈_ C) (List.map (to g ∘ to f) xs) (List.map (to g) (List.map (to f) xs)) -List-homo {C = C} f g = PW.map (reflexive C) ∘ PW.≡⇒Pointwise-≡ ∘ ListProps.map-∘ + → (open Setoid (Listₛ C)) + → List.map (to g ∘ to f) xs ≈ List.map (to g) (List.map (to f) xs) +List-homo {C = C} f g = reflexive (Listₛ C) ∘ ListProps.map-∘ List : Functor (Setoids c ℓ) (Setoids c (c ⊔ ℓ)) List .F₀ = Listₛ diff --git a/Functor/Instance/Nat/Circ.agda b/Functor/Instance/Nat/Circ.agda new file mode 100644 index 0000000..0f18c4c --- /dev/null +++ b/Functor/Instance/Nat/Circ.agda @@ -0,0 +1,32 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level; _⊔_; 0ℓ) + +module Functor.Instance.Nat.Circ {c ℓ : Level} where + +open import Data.Circuit {c} {ℓ} 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) +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) + +List∘Edge : Functor Nat (Setoids 0ℓ 0ℓ) +List∘Edge = List ∘F Edge + +module List∘Edge = Functor List∘Edge + +open Func +open Functor + +Circ : Functor Nat (Setoids c (c ⊔ ℓ)) +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) diff --git a/Functor/Instance/Nat/Edge.agda b/Functor/Instance/Nat/Edge.agda index ee54f2e..618807d 100644 --- a/Functor/Instance/Nat/Edge.agda +++ b/Functor/Instance/Nat/Edge.agda @@ -11,7 +11,7 @@ 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-IsEquivalence; map; ≈-Edge) +open import Data.Hypergraph.Edge HL as Edge using (≈-Edge-IsEquivalence; map; ≈-Edge; Edgeₛ) open import Data.Nat using (ℕ) open import Data.Vec.Relation.Binary.Equality.Cast using (≈-cong′; ≈-reflexive) open import Level using (0ℓ) @@ -27,9 +27,6 @@ open Functor open Setoid open ≈-Edge -Edgeₛ : (v : ℕ) → Setoid 0ℓ 0ℓ -Edgeₛ v = record { isEquivalence = ≈-Edge-IsEquivalence {v} } - Edge₁ : {n m : ℕ} → (Fin n → Fin m) → Edgeₛ n ⟶ₛ Edgeₛ m Edge₁ f .to = map f Edge₁ f .cong x≈y = record diff --git a/NaturalTransformation/Instance/EmptyList.agda b/NaturalTransformation/Instance/EmptyList.agda new file mode 100644 index 0000000..9a558a2 --- /dev/null +++ b/NaturalTransformation/Instance/EmptyList.agda @@ -0,0 +1,23 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level) + +module NaturalTransformation.Instance.EmptyList {c ℓ : Level} where + +import Function.Construct.Constant as Const + +open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) +open import Categories.Functor using (Functor) +open import Categories.Category.Instance.SingletonSet using (SingletonSetoid) +open import Categories.Functor.Construction.Constant using (const) +open import Data.List using ([]) +open import Functor.Instance.List {c} {ℓ} using (List) +open import Relation.Binary using (Setoid) + +module List = Functor List + +⊤⇒[] : NaturalTransformation (const SingletonSetoid) List +⊤⇒[] = ntHelper record + { η = λ X → Const.function SingletonSetoid (List.₀ X) [] + ; commute = λ {_} {B} f → Setoid.refl (List.₀ B) + } diff --git a/NaturalTransformation/Instance/ListAppend.agda b/NaturalTransformation/Instance/ListAppend.agda new file mode 100644 index 0000000..05a31f5 --- /dev/null +++ b/NaturalTransformation/Instance/ListAppend.agda @@ -0,0 +1,46 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level; _⊔_) + +module NaturalTransformation.Instance.ListAppend {c ℓ : Level} where + +open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) +open import Categories.Category.Product using (_※_) +open import Categories.Category.BinaryProducts using (module BinaryProducts) +open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian) +open import Categories.Category.Cartesian using (Cartesian) +open import Categories.Functor using (Functor; _∘F_) +open import Data.List using (_++_; map) +open import Data.List.Properties using (map-++) +open import Data.List.Relation.Binary.Pointwise using (++⁺) +open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_) +open import Data.Product using (_,_) +open import Functor.Instance.List {c} {ℓ} using (List) +open import Function using (Func; _⟶ₛ_) +open import Relation.Binary using (Setoid) + +module List = Functor List + +open Cartesian (Setoids-Cartesian {c} {c ⊔ ℓ}) using (products) +open BinaryProducts products using (-×-) +open Func + +++ₛ : {X : Setoid c ℓ} → List.₀ X ×ₛ List.₀ X ⟶ₛ List.₀ X +++ₛ .to (xs , ys) = xs ++ ys +++ₛ .cong (≈xs , ≈ys) = ++⁺ ≈xs ≈ys + +map-++ₛ + : {A B : Setoid c ℓ} + (f : Func A B) + (xs ys : Data.List.List (Setoid.Carrier A)) + → (open Setoid (List.₀ B)) + → map (to f) xs ++ map (to f) ys ≈ map (to f) (xs ++ ys) +map-++ₛ {_} {B} f xs ys = ListB.sym (ListB.reflexive (map-++ (to f) xs ys)) + where + module ListB = Setoid (List.₀ B) + +++ : NaturalTransformation (-×- ∘F (List ※ List)) List +++ = ntHelper record + { η = λ X → ++ₛ {X} + ; commute = λ { {A} {B} f {xs , ys} → map-++ₛ f xs ys } + } |