Mercurial > hg > Members > kono > Proof > category

comparison monoid-monad.agda @ 131:eb7ca6b9d327

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
trying..
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 11 Aug 2013 15:52:09 +0900
parents 5f331dfc000b
children 683d4e590762
comparison
equal deleted inserted replaced
130:5f331dfc000b 131:eb7ca6b9d327
1 open import Category -- https://github.com/konn/category-agda 1 open import Category -- https://github.com/konn/category-agda
2 open import Category.Monoid 2 open import Category.Monoid
3 open import Algebra 3 open import Algebra
4 open import Level 4 open import Level
5 module monoid-monad {c c₁ c₂ ℓ : Level} { MS : Set ℓ } { Mono : Monoid c ℓ} {A : Category c₁ c₂ ℓ } where 5 module monoid-monad {c₁ c₂ ℓ : Level} { M : Monoid c₁ ℓ} {A : Category c₁ c₂ ℓ } where
6 6
7 open import Category.HomReasoning
8 open import HomReasoning 7 open import HomReasoning
9 open import cat-utility 8 open import cat-utility
10 open import Category.Cat 9 open import Category.Cat
11 open import Category.Sets 10 open import Category.Sets
12 open import Data.Product 11
13 open import Relation.Binary.Core 12 -- T : A -> (M x A)
14 open import Relation.Binary 13 -- a -> m x a
14 -- m x a -> m' x (m x a)
15
16 data T1 {c₁ c₂ ℓ : Level} (M : Monoid c₁ ℓ ) ( A : Category c₁ c₂ ℓ ) : Set ( suc ( c₁ ⊔ c₂ ⊔ ℓ) ) where
17 T1a : Obj A -> T1 M A
18 T1t : Obj A -> T1 M A -> T1 M A
19
20 T1HomMap : {c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } {M : Monoid c₁ ℓ } (a : T1 {c₁} {c₂} {ℓ} M A ) (b : T1 {c₁} {c₂} {ℓ} M A) -> Set c₂
21 T1HomMap {c₁} {c₂} {ℓ } { A } (T1a a1 ) (T1a a2 ) = Hom A a1 a2
22 T1HomMap {c₁} {c₂} {ℓ } { A } (T1t a1 t1 ) (T1a a2 ) = Hom A a1 a2
23 T1HomMap {c₁} {c₂} {ℓ } { A } (T1a a1 ) (T1t a2 t2 ) = Hom A a1 a2
24 T1HomMap {c₁} {c₂} {ℓ } { A } (T1t a1 t1 ) (T1t a2 t2 ) = Hom A a1 a2
25
26 record T1Hom1 {c₁ c₂ ℓ : Level} { M : Monoid c₁ ℓ} { A : Category c₁ c₂ ℓ }
27 (a : T1 M A ) (b : T1 M A) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where
28 field
29 T1Map : T1HomMap a b
30
31 open T1Hom1
32 T1Hom = \(a b : T1 M A) -> T1Hom1 {c₁} {c₂} {ℓ} {M} {A} a b
33
34 _*_ : {c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } {M : Monoid c₁ ℓ } { a b c : T1 {c₁} {c₂} {ℓ } M A } -> T1Hom1 {c₁} {c₂} {ℓ} b c -> T1Hom1 {c₁} {c₂} {ℓ} a b -> T1Hom1 {c₁} {c₂} {ℓ} a c
35 _*_ {c₁} {c₂} {ℓ } {A} {M} {a} {b} {c} g f = record { T1Map = A [ T1Map g o T1Map f ] }
15 36
16 37
17 MC : Category (suc zero) c (suc (ℓ ⊔ c))
18 MC = MONOID Mono
19
20 -- T : A -> (M x A)
21
22 T : ∀{ℓ′} -> Functor (Sets {ℓ′}) (Sets {ℓ ⊔ ℓ′} )
23 T = record {
24 FObj = \a -> MS × a
25 ; FMap = \f -> map ( \x -> x ) f
26 ; isFunctor = record {
27 identity = IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory Sets ))
28 ; distr = (IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory Sets )))
29 ; ≈-cong = cong1
30 }
31 } where
32 cong1 : {ℓ′ : Level} -> {a b : Set ℓ′} { f g : Hom (Sets {ℓ′}) a b} -> Sets [ f ≈ g ] → Sets [ map (λ x → x) f ≈ map (λ x → x) g ]
33 cong1 refl = refl
34 38
35 39
36 -- Forgetful Functor
37 40
38 open Functor
39 F : Functor MC Sets
40 F = record {
41 FObj = \a -> { s : Obj Sets } -> s
42 ; FMap = \f -> ? -- {a : Obj Sets} { g : Hom Sets (FObj F *) (FObj F ((Mor MC f) *)) } -> g
43 ; isFunctor = record {
44 identity = IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory Sets ))
45 ; distr = (IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory Sets )))
46 -- ; ≈-cong = (IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory Sets )))
47 }
48 }
49 41
50 -- Gerator
51 42
52 G : Functor Sets MC 43
53 G = record { 44
54 FObj = \a -> *
55 ; FMap = \f -> { g : Hom MC * * } -> Mor MC
56 ; isFunctor = record {
57 identity = IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory MC ))
58 ; distr = (IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory MC )))
59 ; ≈-cong = (IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory MC )))
60 }
61 }