blob: 88a6ec6d4c56c8ea40dcfd140e8f1297fc186fc8 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
|
{-# OPTIONS --without-K --safe #-}
open import Level using (Level)
module Functor.Instance.Nat.Circ {ℓ : Level} where
import Data.List.Relation.Binary.Permutation.Setoid as ↭
open import Categories.Category.Instance.Nat using (Nat)
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.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))
}
}
private
Edges≅ : (n : ℕ) → Σ[ M ∈ CommutativeMonoid ] CMonoids [ Edges.₀ n ≅ M ]
Edges≅ n = transport-by-iso (Edges.₀ n) (Edges≅Circₛ n)
Circuitₘ : ℕ → CommutativeMonoid
Circuitₘ n = proj₁ (Edges≅ n)
Edges≅Circₘ : (n : ℕ) → CMonoids [ Edges.₀ n ≅ Circuitₘ n ]
Edges≅Circₘ n = proj₂ (Edges≅ n)
Circ : Functor Nat CMonoids
Circ = proj₁ (define-by-pw-iso Edges Circuitₘ Edges≅Circₘ)
|
