Mercurial > hg > Members > kono > Proof > category

comparison monoid-monad.agda @ 129:fdf89038556a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
monoid monad
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 03 Aug 2013 10:12:00 +0900
parents
children 5f331dfc000b
comparison
equal deleted inserted replaced
128:276f33602700 129:fdf89038556a
1 open import Category -- https://github.com/konn/category-agda
2 open import Level
3 --open import Category.HomReasoning
4 open import HomReasoning
5 open import cat-utility
6 open import Category.Cat
7 open import Category.Sets
8 open import Algebra
9 open import Category.Monoid
10 open import Data.Product
11 open import Relation.Binary.Core
12 open import Relation.Binary
13
14 module monooid-monad {c c₁ c₂ ℓ : Level} { MS : Set ℓ } { Mono : Monoid c ℓ} {A : Category c₁ c₂ ℓ } where
15
16
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
35
36
37