diff options
Diffstat (limited to 'Adjoint')
| -rw-r--r-- | Adjoint/Instance/List.agda | 9 | ||||
| -rw-r--r-- | Adjoint/Instance/Multiset.agda | 7 |
2 files changed, 11 insertions, 5 deletions
diff --git a/Adjoint/Instance/List.agda b/Adjoint/Instance/List.agda index 1b65985..6837c8d 100644 --- a/Adjoint/Instance/List.agda +++ b/Adjoint/Instance/List.agda @@ -12,6 +12,7 @@ open import Category.Instance.Setoids.SymmetricMonoidal {ℓ} {ℓ} using (Setoi module S = SymmetricMonoidalCategory Setoids-× +open import Algebra.Morphism.Bundles using (MonoidHomomorphism) open import Categories.Adjoint using (_⊣_) open import Categories.Category.Construction.Monoids using (Monoids) open import Categories.Functor using (Functor; id; _∘F_) @@ -19,7 +20,7 @@ open import Categories.NaturalTransformation using (NaturalTransformation; ntHel open import Categories.Object.Monoid S.monoidal using (Monoid; IsMonoid; Monoid⇒) open import Data.Monoid using (toMonoid; toMonoid⇒) open import Data.Opaque.List using ([-]ₛ; Listₛ; mapₛ; foldₛ; ++ₛ-homo; []ₛ-homo; fold-mapₛ; fold) -open import Data.Product using (_,_; uncurry) +open import Data.Product using (_,_) open import Data.Setoid using (∣_∣) open import Function using (_⟶ₛ_; _⟨$⟩_) open import Functor.Forgetful.Instance.Monoid {suc ℓ} {ℓ} {ℓ} using () renaming (Forget to Forget′) @@ -70,10 +71,12 @@ opaque : {X Y : Monoid} (f : Monoid⇒ X Y) {x : ∣ Listₛ (Carrier X) ∣} - → (open Setoid (Carrier Y)) + (open Setoid (Carrier Y)) → arr (foldₘ Y) ⟨$⟩ (arr (mapₘ (arr f)) ⟨$⟩ x) ≈ arr f ⟨$⟩ (arr (foldₘ X) ⟨$⟩ x) - fold-mapₘ {X} {Y} f = uncurry (fold-mapₛ (toMonoid X) (toMonoid Y)) (toMonoid⇒ X Y f) + fold-mapₘ {X} {Y} f = fold-mapₛ (toMonoid X) (toMonoid Y) (record { cong = ⟦⟧-cong }) isMonoidHomomorphism + where + open MonoidHomomorphism (toMonoid⇒ X Y f) counit : NaturalTransformation (Free ∘F Forget) id counit = ntHelper record diff --git a/Adjoint/Instance/Multiset.agda b/Adjoint/Instance/Multiset.agda index c51baa9..5bc46ba 100644 --- a/Adjoint/Instance/Multiset.agda +++ b/Adjoint/Instance/Multiset.agda @@ -16,6 +16,7 @@ import Functor.Forgetful.Instance.CMonoid S.symmetric as CMonoid import Functor.Forgetful.Instance.Monoid S.monoidal as Monoid import Object.Monoid.Commutative S.symmetric as CMonoidObject +open import Algebra.Morphism.Bundles using (MonoidHomomorphism) open import Categories.Adjoint using (_⊣_) open import Categories.Category using (Category) open import Categories.Functor using (Functor; id; _∘F_) @@ -24,7 +25,7 @@ open import Category.Construction.CMonoids using (CMonoids) open import Data.CMonoid using (toCMonoid; toCMonoid⇒) open import Data.Monoid using (toMonoid; toMonoid⇒) open import Data.Opaque.Multiset using ([-]ₛ; Multisetₛ; foldₛ; ++ₛ-homo; []ₛ-homo; fold-mapₛ; fold) -open import Data.Product using (_,_; uncurry) +open import Data.Product using (_,_) open import Data.Setoid using (∣_∣) open import Function using (_⟶ₛ_; _⟨$⟩_) open import Functor.Free.Instance.CMonoid {ℓ} {ℓ} using (Multisetₘ; mapₘ; MultisetCMonoid) renaming (Free to Free′) @@ -78,7 +79,9 @@ opaque → (open Setoid (Carrier Y)) → arr (foldₘ Y) ⟨$⟩ (arr (mapₘ (arr f)) ⟨$⟩ x) ≈ arr f ⟨$⟩ (arr (foldₘ X) ⟨$⟩ x) - fold-mapₘ {X} {Y} f = uncurry (fold-mapₛ (toCMonoid X) (toCMonoid Y)) (toCMonoid⇒ X Y f) + fold-mapₘ {X} {Y} f = fold-mapₛ (toCMonoid X) (toCMonoid Y) (record { cong = ⟦⟧-cong }) isMonoidHomomorphism + where + open MonoidHomomorphism (toCMonoid⇒ X Y f) counit : NaturalTransformation (Free ∘F Forget) id counit = ntHelper record |