Mercurial > hg > Members > kono > Proof > category

annotate stdalone-kleisli.agda @ 774:f3a493da92e8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add simple category version
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 13 Jun 2018 12:56:38 +0900
parents
children 06a7831cf6ce
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
774
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 module stdalone-kleisli where
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import Level
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 open import Relation.Binary
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open import Relation.Binary.Core
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 -- h g f
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 -- a ---→ b ---→ c ---→ d
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 --
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 record IsCategory {l : Level} ( Obj : Set (suc l) ) (Hom : Obj → Obj → Set l )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 ( _o_ : { a b c : Obj } → Hom b c → Hom a b → Hom a c )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 ( id : ( a : Obj ) → Hom a a )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 : Set (suc l) where
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 field
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 idL : { a b : Obj } { f : Hom a b } → ( id b o f ) ≡ f
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 idR : { a b : Obj } { f : Hom a b } → ( f o id a ) ≡ f
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 assoc : { a b c d : Obj } { f : Hom c d }{ g : Hom b c }{ h : Hom a b } → f o ( g o h ) ≡ ( f o g ) o h
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 record Category {l : Level} : Set (suc (suc l)) where
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 field
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 Obj : Set (suc l)
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 Hom : Obj → Obj → Set l
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 _o_ : { a b c : Obj } → Hom b c → Hom a b → Hom a c
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 id : ( a : Obj ) → Hom a a
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 isCategory : IsCategory Obj Hom _o_ id
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 Sets : Category
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 Sets = record {
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 Obj = Set
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 ; Hom = λ a b → a → b
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 ; _o_ = λ f g x → f ( g x )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 ; id = λ A x → x
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 ; isCategory = record {
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 idL = refl
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 ; idR = refl
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 ; assoc = refl
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 }
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 }
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 open Category
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 _[_o_] : {l : Level} (C : Category {l} ) → {a b c : Obj C} → Hom C b c → Hom C a b → Hom C a c
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 C [ f o g ] = Category._o_ C f g
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47 --
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 -- f g
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 -- a ----→ b -----→ c
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50 -- | | |
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51 -- T| T| T|
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52 -- | | |
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53 -- v v v
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 -- Ta ----→ Tb ----→ Tc
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
55 -- Tf Tg
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
57
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58 record IsFunctor {l : Level} (C D : Category {l} )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59 (FObj : Obj C → Obj D)
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60 (FMap : {A B : Obj C} → Hom C A B → Hom D (FObj A) (FObj B))
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
61 : Set (suc l ) where
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62 field
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63 identity : {A : Obj C} → FMap (id C A) ≡ id D (FObj A)
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64 distr : {a b c : Obj C} {f : Hom C a b} {g : Hom C b c}
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
65 → FMap ( C [ g o f ]) ≡ (D [ FMap g o FMap f ] )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
66
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
67 record Functor {l : Level} (domain codomain : Category {l} )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
68 : Set (suc l) where
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69 field
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
70 FObj : Obj domain → Obj codomain
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
71 FMap : {A B : Obj domain} → Hom domain A B → Hom codomain (FObj A) (FObj B)
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
72 isFunctor : IsFunctor domain codomain FObj FMap
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
73
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
74 open Functor
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
75
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
76 idFunctor : {l : Level } { C : Category {l} } → Functor C C
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
77 idFunctor = record {
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
78 FObj = λ x → x
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
79 ; FMap = λ f → f
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
80 ; isFunctor = record {
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
81 identity = refl
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
82 ; distr = refl
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
83 }
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
84 }
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
85
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
86 open import Relation.Binary.PropositionalEquality hiding ( [_] )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
87
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
88
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
89 _●_ : {l : Level} { A B C : Category {l} } → ( S : Functor B C ) ( T : Functor A B ) → Functor A C
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
90 _●_ {l} {A} {B} {C} S T = record {
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
91 FObj = λ x → FObj S ( FObj T x )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
92 ; FMap = λ f → FMap S ( FMap T f )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
93 ; isFunctor = record {
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
94 identity = λ {a} → identity a
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
95 ; distr = λ {a} {b} {c} {f} {g} → distr
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
96 }
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
97 } where
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
98 identity : (a : Obj A) → FMap S (FMap T (id A a)) ≡ id C (FObj S (FObj T a))
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
99 identity a = let open ≡-Reasoning in begin
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
100 FMap S (FMap T (id A a))
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
101 ≡⟨ cong ( λ z → FMap S z ) ( IsFunctor.identity (isFunctor T ) ) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
102 FMap S (id B (FObj T a) )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
103 ≡⟨ IsFunctor.identity (isFunctor S ) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
104 id C (FObj S (FObj T a))
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
105 ∎
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
106 distr : {a b c : Obj A} { f : Hom A a b } { g : Hom A b c } → FMap S (FMap T (A [ g o f ])) ≡ (C [ FMap S (FMap T g) o FMap S (FMap T f) ])
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
107 distr {a} {b} {c} {f} {g} = let open ≡-Reasoning in begin
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
108 FMap S (FMap T (A [ g o f ]))
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
109 ≡⟨ cong ( λ z → FMap S z ) ( IsFunctor.distr (isFunctor T ) ) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
110 FMap S ( B [ FMap T g o FMap T f ] )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
111 ≡⟨ IsFunctor.distr (isFunctor S ) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
112 C [ FMap S (FMap T g) o FMap S (FMap T f) ]
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
113 ∎
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
114
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
115
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
116 -- {A : Set c₁ } {B : Set c₂ } → { f g : A → B } → f x ≡ g x → f ≡ g
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
117 postulate extensionality : { c₁ c₂ : Level} → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
118
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
119 --
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
120 -- t a
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
121 -- F a -----→ G a
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
122 -- | |
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
123 -- Ff | | Gf
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
124 -- v v
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
125 -- F b ------→ G b
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
126 -- t b
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
127 --
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
128
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
129 record IsNTrans { l : Level } (D C : Category {l} ) ( F G : Functor D C )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
130 (TMap : (A : Obj D) → Hom C (FObj F A) (FObj G A))
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
131 : Set (suc l) where
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
132 field
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
133 commute : {a b : Obj D} {f : Hom D a b}
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
134 → C [ ( FMap G f ) o ( TMap a ) ] ≡ C [ (TMap b ) o (FMap F f) ]
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
135
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
136 record NTrans {l : Level} {domain codomain : Category {l} } (F G : Functor domain codomain )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
137 : Set (suc l) where
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
138 field
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
139 TMap : (A : Obj domain) → Hom codomain (FObj F A) (FObj G A)
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
140 isNTrans : IsNTrans domain codomain F G TMap
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
141
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
142
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
143
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
144 open NTrans
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
145
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
146 --
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
147 --
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
148 -- η : 1 ------→ T
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
149 -- μ : TT -----→ T
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
150 --
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
151 -- η μT
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
152 -- T -----→ TT TTT ------→ TT
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
153 -- | | | |
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
154 -- Tη | |μ Tμ | |Tμ
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
155 -- v | v v
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
156 -- TT -----→ T TT -------→ T
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
157 -- μ μT
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
158
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
159
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
160 record IsMonad {l : Level} { C : Category {l} } (T : Functor C C) ( η : NTrans idFunctor T ) ( μ : NTrans (T ● T) T )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
161 : Set (suc l) where
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
162 field
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
163 assoc : {a : Obj C} → C [ TMap μ a o TMap μ ( FObj T a ) ] ≡ C [ TMap μ a o FMap T (TMap μ a) ]
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
164 unity1 : {a : Obj C} → C [ TMap μ a o TMap η ( FObj T a ) ] ≡ id C (FObj T a)
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
165 unity2 : {a : Obj C} → C [ TMap μ a o (FMap T (TMap η a ))] ≡ id C (FObj T a)
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
166
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
167
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
168 record Monad {l : Level} { C : Category {l} } (T : Functor C C) : Set (suc l) where
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
169 field
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
170 η : NTrans idFunctor T
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
171 μ : NTrans (T ● T) T
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
172 isMonad : IsMonad T η μ
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
173
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
174 record KleisliHom { c : Level} { A : Category {c} } { T : Functor A A } (a : Obj A) (b : Obj A)
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
175 : Set c where
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
176 field
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
177 KMap : Hom A a ( FObj T b )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
178
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
179 open KleisliHom
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
180
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
181
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
182 left : {l : Level} (C : Category {l} ) {a b c : Obj C } {f f' : Hom C b c } {g : Hom C a b } → f ≡ f' → C [ f o g ] ≡ C [ f' o g ]
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
183 left {l} C {a} {b} {c} {f} {f'} {g} refl = cong ( λ z → C [ z o g ] ) refl
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
184
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
185 right : {l : Level} (C : Category {l} ) {a b c : Obj C } {f : Hom C b c } {g g' : Hom C a b } → g ≡ g' → C [ f o g ] ≡ C [ f o g' ]
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
186 right {l} C {a} {b} {c} {f} {g} {g'} refl = cong ( λ z → C [ f o z ] ) refl
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
187
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
188 Assoc : {l : Level} (C : Category {l} ) {a b c d : Obj C } {f : Hom C c d } {g : Hom C b c } { h : Hom C a b }
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
189 → C [ f o C [ g o h ] ] ≡ C [ C [ f o g ] o h ]
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
190 Assoc {l} C = IsCategory.assoc ( isCategory C )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
191
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
192
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
193 Kleisli : {l : Level} (C : Category {l} ) (T : Functor C C ) ( M : Monad T ) → Category {l}
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
194 Kleisli C T M = record {
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
195 Obj = Obj C
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
196 ; Hom = λ a b → KleisliHom {_} {C} {T} a b
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
197 ; _o_ = λ {a} {b} {c} f g → join {a} {b} {c} f g
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
198 ; id = λ a → record { KMap = TMap (Monad.η M) a }
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
199 ; isCategory = record {
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
200 idL = idL
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
201 ; idR = idR
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
202 ; assoc = assoc
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
203 }
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
204 } where
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
205 join : { a b c : Obj C } → KleisliHom b c → KleisliHom a b → KleisliHom a c
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
206 join {a} {b} {c} f g = record { KMap = ( C [ TMap (Monad.μ M) c o C [ FMap T ( KMap f ) o KMap g ] ] ) }
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
207 idL : {a b : Obj C} {f : KleisliHom a b} → join (record { KMap = TMap (Monad.η M) b }) f ≡ f
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
208 idL {a} {b} {f} = let open ≡-Reasoning in begin
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
209 record { KMap = C [ TMap (Monad.μ M) b o C [ FMap T (TMap (Monad.η M) b) o KMap f ] ] }
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
210 ≡⟨ cong ( λ z → record { KMap = z } ) ( begin
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
211 C [ TMap (Monad.μ M) b o C [ FMap T (TMap (Monad.η M) b) o KMap f ] ]
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
212 ≡⟨ IsCategory.assoc ( isCategory C ) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
213 C [ C [ TMap (Monad.μ M) b o FMap T (TMap (Monad.η M) b) ] o KMap f ]
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
214 ≡⟨ cong ( λ z → C [ z o KMap f ] ) ( IsMonad.unity2 (Monad.isMonad M ) ) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
215 C [ id C (FObj T b) o KMap f ]
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
216 ≡⟨ IsCategory.idL ( isCategory C ) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
217 KMap f
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
218 ∎ ) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
219 record { KMap = KMap f }
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
220 ∎
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
221 idR : {a b : Obj C} {f : KleisliHom a b} → join f (record { KMap = TMap (Monad.η M) a }) ≡ f
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
222 idR {a} {b} {f} = let open ≡-Reasoning in begin
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
223 record { KMap = C [ TMap (Monad.μ M) b o C [ FMap T (KMap f) o TMap (Monad.η M) a ] ] }
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
224 ≡⟨ cong ( λ z → record { KMap = z } ) ( begin
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
225 C [ TMap (Monad.μ M) b o C [ FMap T (KMap f) o TMap (Monad.η M) a ] ]
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
226 ≡⟨ cong ( λ z → C [ TMap (Monad.μ M) b o z ] ) ( IsNTrans.commute (isNTrans (Monad.η M) )) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
227 C [ TMap (Monad.μ M) b o C [ TMap (Monad.η M) (FObj T b) o KMap f ] ]
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
228 ≡⟨ IsCategory.assoc ( isCategory C ) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
229 C [ C [ TMap (Monad.μ M) b o TMap (Monad.η M) (FObj T b) ] o KMap f ]
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
230 ≡⟨ cong ( λ z → C [ z o KMap f ] ) ( IsMonad.unity1 (Monad.isMonad M ) ) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
231 C [ id C (FObj T b) o KMap f ]
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
232 ≡⟨ IsCategory.idL ( isCategory C ) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
233 KMap f
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
234 ∎ ) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
235 record { KMap = KMap f }
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
236 ∎
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
237 --
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
238 -- TMap (Monad.μ M) d ・ ( FMap T (KMap f) ・ ( TMap (Monad.μ M) c ・ ( FMap T (KMap g) ・ KMap h ) ) ) )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
239 --
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
240 -- h T g μ c
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
241 -- a ---→ T b -----------------→ T T c -------------------------→ T c
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
242 -- | | |
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
243 -- | | |
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
244 -- | | T T f NAT μ | T f
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
245 -- | | |
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
246 -- | v μ (T d) v
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
247 -- | distr T T T T d -------------------------→ T T d
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
248 -- | | |
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
249 -- | | |
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
250 -- | | T μ d Monad-assoc | μ d
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
251 -- | | |
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
252 -- | v v
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
253 -- +------------------→ T T d -------------------------→ T d
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
254 -- T (μ d・T f・g) μ d
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
255 --
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
256 -- TMap (Monad.μ M) d ・ ( FMap T (( TMap (Monad.μ M) d ・ ( FMap T (KMap f) ・ KMap g ) ) ) ・ KMap h ) )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
257 --
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
258 _・_ : {a b c : Obj C } ( f : Hom C b c ) ( g : Hom C a b ) → Hom C a c
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
259 f ・ g = C [ f o g ]
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
260 assoc : {a b c d : Obj C} {f : KleisliHom c d} {g : KleisliHom b c} {h : KleisliHom a b} → join f (join g h) ≡ join (join f g) h
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
261 assoc {a} {b} {c} {d} {f} {g} {h} = let open ≡-Reasoning in begin
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
262 join f (join g h)
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
263 ≡⟨⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
264 record { KMap = TMap (Monad.μ M) d ・ ( FMap T (KMap f) ・ ( TMap (Monad.μ M) c ・ ( FMap T (KMap g) ・ KMap h ))) }
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
265 ≡⟨ cong ( λ z → record { KMap = z } ) ( begin
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
266 ( TMap (Monad.μ M) d ・ ( FMap T (KMap f) ・ ( TMap (Monad.μ M) c ・ ( FMap T (KMap g) ・ KMap h ) ) ) )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
267 ≡⟨ right C ( right C (Assoc C)) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
268 ( TMap (Monad.μ M) d ・ ( FMap T (KMap f) ・ ( ( TMap (Monad.μ M) c ・ FMap T (KMap g) ) ・ KMap h ) ) )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
269 ≡⟨ Assoc C ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
270 ( ( TMap (Monad.μ M) d ・ FMap T (KMap f) ) ・ ( ( TMap (Monad.μ M) c ・ FMap T (KMap g) ) ・ KMap h ) )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
271 ≡⟨ Assoc C ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
272 ( ( ( TMap (Monad.μ M) d ・ FMap T (KMap f) ) ・ ( TMap (Monad.μ M) c ・ FMap T (KMap g) ) ) ・ KMap h )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
273 ≡⟨ sym ( left C (Assoc C )) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
274 ( ( TMap (Monad.μ M) d ・ ( FMap T (KMap f) ・ ( TMap (Monad.μ M) c ・ FMap T (KMap g) ) ) ) ・ KMap h )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
275 ≡⟨ left C ( right C (Assoc C)) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
276 ( ( TMap (Monad.μ M) d ・ ( ( FMap T (KMap f) ・ TMap (Monad.μ M) c ) ・ FMap T (KMap g) ) ) ・ KMap h )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
277 ≡⟨ left C (Assoc C)⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
278 ( ( ( TMap (Monad.μ M) d ・ ( FMap T (KMap f) ・ TMap (Monad.μ M) c ) ) ・ FMap T (KMap g) ) ・ KMap h )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
279 ≡⟨ left C ( left C ( right C ( IsNTrans.commute (isNTrans (Monad.μ M) ) ) )) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
280 ( ( ( TMap (Monad.μ M) d ・ ( TMap (Monad.μ M) (FObj T d) ・ FMap (T ● T) (KMap f) ) ) ・ FMap T (KMap g) ) ・ KMap h )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
281 ≡⟨ sym ( left C (Assoc C)) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
282 ( ( TMap (Monad.μ M) d ・ ( ( TMap (Monad.μ M) (FObj T d) ・ FMap (T ● T) (KMap f) ) ・ FMap T (KMap g) ) ) ・ KMap h )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
283 ≡⟨ sym ( left C ( right C (Assoc C))) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
284 ( ( TMap (Monad.μ M) d ・ ( TMap (Monad.μ M) (FObj T d) ・ ( FMap (T ● T) (KMap f) ・ FMap T (KMap g) ) ) ) ・ KMap h )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
285 ≡⟨ sym ( left C ( right C (right C (IsFunctor.distr (isFunctor T ) ) ) )) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
286 ( ( TMap (Monad.μ M) d ・ ( TMap (Monad.μ M) (FObj T d) ・ FMap T (( FMap T (KMap f) ・ KMap g )) ) ) ・ KMap h )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
287 ≡⟨ left C (Assoc C) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
288 ( ( ( TMap (Monad.μ M) d ・ TMap (Monad.μ M) (FObj T d) ) ・ FMap T (( FMap T (KMap f) ・ KMap g )) ) ・ KMap h )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
289 ≡⟨ left C (left C ( IsMonad.assoc (Monad.isMonad M ) ) ) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
290 ( ( ( TMap (Monad.μ M) d ・ FMap T (TMap (Monad.μ M) d) ) ・ FMap T (( FMap T (KMap f) ・ KMap g )) ) ・ KMap h )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
291 ≡⟨ sym ( left C (Assoc C)) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
292 ( ( TMap (Monad.μ M) d ・ ( FMap T (TMap (Monad.μ M) d) ・ FMap T (( FMap T (KMap f) ・ KMap g )) ) ) ・ KMap h )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
293 ≡⟨ sym (Assoc C) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
294 ( TMap (Monad.μ M) d ・ ( ( FMap T (TMap (Monad.μ M) d) ・ FMap T (( FMap T (KMap f) ・ KMap g )) ) ・ KMap h ) )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
295 ≡⟨ sym (right C ( left C (IsFunctor.distr (isFunctor T )))) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
296 ( TMap (Monad.μ M) d ・ ( FMap T (( TMap (Monad.μ M) d ・ ( FMap T (KMap f) ・ KMap g ) ) ) ・ KMap h ) )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
297 ∎ ) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
298 record { KMap = ( TMap (Monad.μ M) d ・ ( FMap T (( TMap (Monad.μ M) d ・ ( FMap T (KMap f) ・ KMap g ) ) ) ・ KMap h ) ) }
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
299 ≡⟨⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
300 join (join f g) h
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
301 ∎
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
302
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
303 --
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
304 -- U : Kleisli Sets
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
305 -- F : Sets Kleisli
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
306 --
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
307 -- Hom Klei a b ←---→ Hom Sets a (U●F b )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
308 --
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
309 -- Hom Klei (F a) (F b) ←---→ Hom Sets a (U●F b )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
310 --
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
311 -- Hom Klei (F a) b ←---→ Hom Sets a U(b) Hom Klei (F a) b ←---→ Hom Sets a U(b)
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
312 -- | | | |
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
313 -- Ff| f| |f |Uf
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
314 -- | | | |
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
315 -- ↓ ↓ ↓ ↓
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
316 -- Hom Klei (F (f a)) b ←---→ Hom Sets (f a) U(b) Hom Klei (F a) (f b) ←---→ Hom Sets a U(f b)
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
317 --
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
318 --
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
319
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
320 record UnityOfOppsite ( Kleisli : Category ) ( U : Functor Kleisli Sets ) ( F : Functor Sets Kleisli ) : Set (suc zero) where
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
321 field
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
322 hom-right : {a : Obj Sets} { b : Obj Kleisli } → Hom Sets a ( FObj U b ) → Hom Kleisli (FObj F a) b
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
323 hom-left : {a : Obj Sets} { b : Obj Kleisli } → Hom Kleisli (FObj F a) b → Hom Sets a ( FObj U b )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
324 hom-right-injective : {a : Obj Sets} { b : Obj Kleisli } → {f : Hom Sets a (FObj U b) } → hom-left ( hom-right f ) ≡ f
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
325 hom-left-injective : {a : Obj Sets} { b : Obj Kleisli } → {f : Hom Kleisli (FObj F a) b } → hom-right ( hom-left f ) ≡ f
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
326 --- naturality of Φ
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
327 hom-left-commute1 : {a : Obj Sets} {b b' : Obj Kleisli } →
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
328 { f : Hom Kleisli (FObj F a) b } → { k : Hom Kleisli b b' } →
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
329 hom-left ( Kleisli [ k o f ] ) ≡ Sets [ FMap U k o hom-left f ]
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
330 hom-left-commute2 : {a a' : Obj Sets} {b : Obj Kleisli } →
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
331 { f : Hom Kleisli (FObj F a) b } → { h : Hom Sets a' a } →
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
332 hom-left ( Kleisli [ f o FMap F h ] ) ≡ Sets [ hom-left f o h ]
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
333 hom-right-commute1 : {a : Obj Sets} {b b' : Obj Kleisli } →
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
334 { g : Hom Sets a (FObj U b)} → { k : Hom Kleisli b b' } →
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
335 Kleisli [ k o hom-right g ] ≡ hom-right ( Sets [ FMap U k o g ] )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
336 hom-right-commute1 {a} {b} {b'} {g} {k} = let open ≡-Reasoning in begin
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
337 Kleisli [ k o hom-right g ]
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
338 ≡⟨ sym hom-left-injective ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
339 hom-right ( hom-left ( Kleisli [ k o hom-right g ] ) )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
340 ≡⟨ cong ( λ z → hom-right z ) hom-left-commute1 ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
341 hom-right (Sets [ FMap U k o hom-left (hom-right g) ])
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
342 ≡⟨ cong ( λ z → hom-right ( Sets [ FMap U k o z ] )) hom-right-injective ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
343 hom-right ( Sets [ FMap U k o g ] )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
344 ∎
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
345 hom-right-commute2 : {a a' : Obj Sets} {b : Obj Kleisli } →
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
346 { g : Hom Sets a (FObj U b) } → { h : Hom Sets a' a } →
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
347 Kleisli [ hom-right g o FMap F h ] ≡ hom-right ( Sets [ g o h ] )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
348 hom-right-commute2 {a} {a'} {b} {g} {h} = let open ≡-Reasoning in begin
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
349 Kleisli [ hom-right g o FMap F h ]
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
350 ≡⟨ sym hom-left-injective ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
351 hom-right (hom-left (Kleisli [ hom-right g o FMap F h ]))
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
352 ≡⟨ cong ( λ z → hom-right z ) hom-left-commute2 ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
353 hom-right (Sets [ hom-left (hom-right g) o h ])
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
354 ≡⟨ cong ( λ z → hom-right ( Sets [ z o h ] )) hom-right-injective ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
355 hom-right (Sets [ g o h ])
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
356 ∎
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
357
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
358
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
359
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
360
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
361 _・_ : {a b c : Obj Sets } ( f : Hom Sets b c ) ( g : Hom Sets a b ) → Hom Sets a c
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
362 f ・ g = Sets [ f o g ]
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
363
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
364 U : ( T : Functor Sets Sets ) → { m : Monad T } → Functor (Kleisli Sets T m) Sets
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
365 U T {m} = record {
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
366 FObj = FObj T
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
367 ; FMap = λ {a} {b} f x → TMap ( μ m ) b ( FMap T ( KMap f ) x )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
368 ; isFunctor = record { identity = IsMonad.unity2 (isMonad m) ; distr = distr }
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
369 } where
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
370 open Monad
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
371 distr : {a b c : Obj (Kleisli Sets T m)} {f : Hom (Kleisli Sets T m) a b} {g : Hom (Kleisli Sets T m) b c} →
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
372 (λ x → TMap (μ m) c (FMap T (KMap (Kleisli Sets T m [ g o f ])) x))
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
373 ≡ (Sets [ (λ x → TMap (μ m) c (FMap T (KMap g) x)) o (λ x → TMap (μ m) b (FMap T (KMap f) x)) ])
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
374 distr {a} {b} {c} {f} {g} = let open ≡-Reasoning in begin
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
375 Sets [ TMap (μ m) c o FMap T (KMap (Kleisli Sets T m [ g o f ])) ]
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
376 ≡⟨⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
377 Sets [ TMap (μ m) c o FMap T ( Sets [ TMap (μ m) c o Sets [ FMap T ( KMap g ) o KMap f ] ] ) ]
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
378 ≡⟨ right Sets {_} {_} {_} {TMap (μ m) c} {_} {_} ( IsFunctor.distr (Functor.isFunctor T) ) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
379 Sets [ TMap (μ m) c o Sets [ FMap T ( TMap (μ m) c) o FMap T ( Sets [ FMap T (KMap g) o KMap f ] ) ] ]
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
380 ≡⟨ sym ( left Sets (IsMonad.assoc (isMonad m ))) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
381 Sets [ Sets [ TMap (μ m) c o TMap (μ m) (FObj T c) ] o (FMap T (Sets [ FMap T (KMap g) o KMap f ])) ]
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
382 ≡⟨ right Sets {_} {_} {_} {TMap (μ m) c} ( right Sets {_} {_} {_} {TMap (μ m) (FObj T c)} ( IsFunctor.distr (Functor.isFunctor T) ) ) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
383 Sets [ Sets [ TMap (μ m) c o TMap (μ m) (FObj T c) ] o Sets [ FMap T ( FMap T (KMap g)) o FMap T ( KMap f ) ] ]
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
384 ≡⟨ sym ( right Sets {_} {_} {_} {TMap (μ m) c} ( left Sets (IsNTrans.commute ( NTrans.isNTrans (μ m))))) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
385 Sets [ Sets [ TMap (μ m) c o FMap T (KMap g) ] o Sets [ TMap (μ m) b o FMap T (KMap f) ] ]
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
386 ∎
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
387
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
388
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
389 F : ( T : Functor Sets Sets ) → {m : Monad T} → Functor Sets ( Kleisli Sets T m)
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
390 F T {m} = record {
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
391 FObj = λ a → a ; FMap = λ {a} {b} f → record { KMap = λ x → TMap (η m) b (f x) }
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
392 ; isFunctor = record { identity = refl ; distr = distr }
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
393 } where
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
394 open Monad
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
395 distr : {a b c : Obj Sets} {f : Hom Sets a b} {g : Hom Sets b c} → record { KMap = λ x → TMap (η m) c ((Sets [ g o f ]) x) } ≡
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
396 Kleisli Sets T m [ record { KMap = λ x → TMap (η m) c (g x) } o record { KMap = λ x → TMap (η m) b (f x) } ]
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
397 distr {a} {b} {c} {f} {g} = let open ≡-Reasoning in ( cong ( λ z → record { KMap = z } ) ( begin
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
398 Sets [ TMap (η m) c o Sets [ g o f ] ]
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
399 ≡⟨ left Sets {_} {_} {_} {Sets [ TMap (η m) c o g ] } ( sym ( IsNTrans.commute ( NTrans.isNTrans (η m) ) )) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
400 Sets [ Sets [ FMap T g o TMap (η m) b ] o f ]
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
401 ≡⟨ sym ( IsCategory.idL ( Category.isCategory Sets )) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
402 Sets [ ( λ x → x ) o Sets [ Sets [ FMap T g o TMap (η m) b ] o f ] ]
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
403 ≡⟨ sym ( left Sets (IsMonad.unity2 (isMonad m ))) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
404 Sets [ Sets [ TMap (μ m) c o FMap T (TMap (η m) c) ] o Sets [ FMap T g o Sets [ TMap (η m) b o f ] ] ]
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
405 ≡⟨ sym ( right Sets {_} {_} {_} {TMap (μ m) c} {_} ( left Sets {_} {_} {_} { FMap T (Sets [ TMap (η m) c o g ] )} ( IsFunctor.distr (Functor.isFunctor T) ))) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
406 Sets [ TMap (μ m) c o ( Sets [ FMap T (Sets [ TMap (η m) c o g ] ) o Sets [ TMap (η m) b o f ] ] ) ]
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
407 ∎ ))
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
408
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
409 --
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
410 -- Hom Sets a (FObj U b) = Hom Sets a (T b)
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
411 -- Hom Kleisli (FObj F a) b = Hom Sets a (T b)
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
412 --
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
413
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
414 lemma→ : ( T : Functor Sets Sets ) → (m : Monad T ) → UnityOfOppsite (Kleisli Sets T m) (U T {m} ) (F T {m})
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
415 lemma→ T m =
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
416 let open Monad in
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
417 record {
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
418 hom-right = λ {a} {b} f → record { KMap = f }
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
419 ; hom-left = λ {a} {b} f x → TMap (μ m) b ( TMap ( η m ) (FObj T b) ( (KMap f) x ) )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
420 ; hom-right-injective = hom-right-injective
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
421 ; hom-left-injective = hom-left-injective
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
422 ; hom-left-commute1 = hom-left-commute1
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
423 ; hom-left-commute2 = hom-left-commute2
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
424 } where
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
425 open Monad
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
426 hom-right-injective : {a : Obj Sets} {b : Obj (Kleisli Sets T m)}
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
427 {f : Hom Sets a (FObj (U T {m}) b)} → (λ x → TMap (μ m) b (TMap (η m) (FObj T b) (f x))) ≡ f
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
428 hom-right-injective {a} {b} {f} = let open ≡-Reasoning in begin
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
429 Sets [ TMap (μ m) b o Sets [ TMap (η m) (FObj T b) o f ] ]
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
430 ≡⟨ left Sets ( IsMonad.unity1 ( isMonad m ) ) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
431 Sets [ id Sets (FObj (U T {m}) b) o f ]
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
432 ≡⟨ IsCategory.idL ( isCategory Sets ) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
433 f
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
434 ∎
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
435 hom-left-injective : {a : Obj Sets} {b : Obj (Kleisli Sets T m)} {f : Hom (Kleisli Sets T m) (FObj (F T {m}) a) b}
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
436 → record { KMap = λ x → TMap (μ m) b (TMap (η m) (FObj T b) (KMap f x)) } ≡ f
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
437 hom-left-injective {a} {b} {f} = let open ≡-Reasoning in cong ( λ z → record { KMap = z } ) ( begin
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
438 Sets [ TMap (μ m) b o Sets [ TMap (η m) (FObj T b) o KMap f ] ]
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
439 ≡⟨ left Sets ( IsMonad.unity1 ( isMonad m ) ) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
440 KMap f
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
441 ∎ )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
442 hom-left-commute1 : {a : Obj Sets} {b b' : Obj (Kleisli Sets T m)} {f : Hom (Kleisli Sets T m) (FObj (F T {m}) a) b} {k : Hom (Kleisli Sets T m) b b'} →
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
443 (λ x → TMap (μ m) b' (TMap (η m) (FObj T b') (KMap (Kleisli Sets T m [ k o f ]) x)))
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
444 ≡ (Sets [ FMap (U T {m}) k o (λ x → TMap (μ m) b (TMap (η m) (FObj T b) (KMap f x))) ])
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
445 hom-left-commute1 {a} {b} {b'} {f} {k} = let open ≡-Reasoning in begin
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
446 Sets [ TMap (μ m) b' o Sets [ TMap (η m) (FObj T b') o KMap (Kleisli Sets T m [ k o f ] ) ] ]
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
447 ≡⟨⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
448 TMap (μ m) b' ・ ( TMap (η m) (FObj T b') ・ ( TMap (μ m) b' ・ ( FMap T (KMap k) ・ KMap f )))
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
449 ≡⟨ left Sets ( IsMonad.unity1 ( isMonad m )) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
450 TMap (μ m) b' ・ ( FMap T (KMap k) ・ KMap f )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
451 ≡⟨ right Sets {_} {_} {_} {TMap ( μ m ) b' ・ FMap T ( KMap k )} ( left Sets ( sym ( IsMonad.unity1 ( isMonad m ) ) ) ) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
452 ( TMap ( μ m ) b' ・ FMap T ( KMap k ) ) ・ ( TMap (μ m) b ・ ( TMap (η m) (FObj T b) ・ KMap f ) )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
453 ≡⟨⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
454 Sets [ FMap (U T {m}) k o Sets [ TMap (μ m) b o Sets [ TMap (η m) (FObj T b) o KMap f ] ] ]
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
455 ∎
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
456 hom-left-commute2 : {a a' : Obj Sets} {b : Obj (Kleisli Sets T m)} {f : Hom (Kleisli Sets T m) (FObj (F T {m}) a) b} {h : Hom Sets a' a} →
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
457 (λ x → TMap (μ m) b (TMap (η m) (FObj T b) (KMap (Kleisli Sets T m [ f o FMap (F T {m}) h ]) x)))
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
458 ≡ (Sets [ (λ x → TMap (μ m) b (TMap (η m) (FObj T b) (KMap f x))) o h ])
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
459 hom-left-commute2 {a} {a'} {b} {f} {h} = let open ≡-Reasoning in begin
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
460 TMap (μ m) b ・ (TMap (η m) (FObj T b) ・ (KMap (Kleisli Sets T m [ f o FMap (F T {m}) h ])))
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
461 ≡⟨⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
462 TMap (μ m) b ・ (TMap (η m) (FObj T b) ・ ( (TMap (μ m) b ・ FMap T (KMap f) ) ・ ( TMap (η m) a ・ h )))
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
463 ≡⟨ left Sets (IsMonad.unity1 ( isMonad m )) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
464 (TMap (μ m) b ・ FMap T (KMap f) ) ・ ( TMap (η m) a ・ h )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
465 ≡⟨ right Sets {_} {_} {_} {TMap (μ m) b} ( left Sets ( IsNTrans.commute ( isNTrans (η m) ))) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
466 TMap (μ m) b ・ (( TMap (η m) (FObj T b)・ KMap f ) ・ h )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
467 ∎
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
468
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
469
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
470
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
471 lemma← : ( U F : Functor Sets Sets ) → UnityOfOppsite Sets U F → Monad ( U ● F )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
472 lemma← U F uo = record {
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
473 η = η
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
474 ; μ = μ
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
475 ; isMonad = record {
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
476 unity1 = unity1
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
477 ; unity2 = unity2
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
478 ; assoc = assoc
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
479 }
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
480 } where
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
481 open UnityOfOppsite
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
482 T = U ● F
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
483 η-comm : {a b : Obj Sets} {f : Hom Sets a b} → Sets [ FMap (U ● F) f o (λ x → hom-left uo (λ x₁ → x₁) x) ]
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
484 ≡ Sets [ (λ x → hom-left uo (λ x₁ → x₁) x) o FMap (idFunctor {_} {Sets} ) f ]
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
485 η-comm {a} {b} {f} = let open ≡-Reasoning in begin
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
486 FMap (U ● F) f ・ (hom-left uo (λ x₁ → x₁) )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
487 ≡⟨ sym (hom-left-commute1 uo) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
488 hom-left uo ( FMap F f ・ (λ x₁ → x₁) )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
489 ≡⟨ hom-left-commute2 uo ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
490 hom-left uo (λ x₁ → x₁) ・ FMap ( idFunctor {_} {Sets} ) f
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
491 ∎
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
492 η : NTrans (idFunctor {_} {Sets}) T
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
493 η = record { TMap = λ a x → (hom-left uo) (λ x → x ) x ; isNTrans = record { commute = η-comm } }
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
494 μ-comm : {a b : Obj Sets} {f : Hom Sets a b} → (Sets [ FMap T f o (λ x → FMap U (hom-right uo (λ x₁ → x₁)) x) ])
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
495 ≡ (Sets [ (λ x → FMap U (hom-right uo (λ x₁ → x₁)) x) o FMap (T ● T) f ])
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
496 μ-comm {a} {b} {f} = let open ≡-Reasoning in begin
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
497 FMap T f ・ FMap U (hom-right uo (λ x₁ → x₁))
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
498 ≡⟨⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
499 FMap U (FMap F f ) ・ FMap U (hom-right uo (λ x₁ → x₁))
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
500 ≡⟨ sym ( IsFunctor.distr ( Functor.isFunctor U)) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
501 FMap U (FMap F f ・ hom-right uo (λ x₁ → x₁))
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
502 ≡⟨ cong ( λ z → FMap U z ) (hom-right-commute1 uo) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
503 FMap U ( hom-right uo (FMap U (FMap F f) ・ (λ x₁ → x₁) ) )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
504 ≡⟨ sym ( cong ( λ z → FMap U z ) (hom-right-commute2 uo)) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
505 FMap U ((hom-right uo (λ x₁ → x₁)) ・ (FMap F (FMap U (FMap F f ))))
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
506 ≡⟨ IsFunctor.distr ( Functor.isFunctor U) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
507 FMap U (hom-right uo (λ x₁ → x₁)) ・ FMap U (FMap F (FMap U (FMap F f )))
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
508 ≡⟨⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
509 FMap U (hom-right uo (λ x₁ → x₁)) ・ FMap (T ● T) f
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
510 ∎
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
511 μ : NTrans (T ● T) T
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
512 μ = record { TMap = λ a x → FMap U ( hom-right uo (λ x → x)) x ; isNTrans = record { commute = μ-comm } }
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
513 unity1 : {a : Obj Sets} → (Sets [ TMap μ a o TMap η (FObj (U ● F) a) ]) ≡ id Sets (FObj (U ● F) a)
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
514 unity1 {a} = let open ≡-Reasoning in begin
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
515 TMap μ a ・ TMap η (FObj (U ● F) a)
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
516 ≡⟨⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
517 FMap U (hom-right uo (λ x₁ → x₁)) ・ hom-left uo (λ x₁ → x₁)
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
518 ≡⟨ sym (hom-left-commute1 uo ) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
519 hom-left uo ( hom-right uo (λ x₁ → x₁) ・ (λ x₁ → x₁) )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
520 ≡⟨ hom-right-injective uo ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
521 id Sets (FObj (U ● F) a)
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
522 ∎
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
523 unity2 : {a : Obj Sets} → (Sets [ TMap μ a o FMap (U ● F) (TMap η a) ]) ≡ id Sets (FObj (U ● F) a)
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
524 unity2 {a} = let open ≡-Reasoning in begin
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
525 TMap μ a ・ FMap (U ● F) (TMap η a)
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
526 ≡⟨⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
527 FMap U (hom-right uo (λ x₁ → x₁)) ・ FMap U (FMap F (hom-left uo (λ x₁ → x₁)))
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
528 ≡⟨ sym ( IsFunctor.distr (isFunctor U)) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
529 FMap U (hom-right uo (λ x₁ → x₁) ・ FMap F (hom-left uo (λ x₁ → x₁)))
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
530 ≡⟨ cong ( λ z → FMap U z ) (hom-right-commute2 uo) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
531 FMap U (hom-right uo ((λ x₁ → x₁) ・ hom-left uo (λ x₁ → x₁) ))
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
532 ≡⟨ cong ( λ z → FMap U z ) (hom-left-injective uo) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
533 FMap U ( id Sets (FObj F a) )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
534 ≡⟨ IsFunctor.identity (isFunctor U) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
535 id Sets (FObj (U ● F) a)
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
536 ∎
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
537 assoc : {a : Obj Sets} → (Sets [ TMap μ a o TMap μ (FObj (U ● F) a) ]) ≡ (Sets [ TMap μ a o FMap (U ● F) (TMap μ a) ])
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
538 assoc {a} = let open ≡-Reasoning in begin
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
539 TMap μ a ・ TMap μ (FObj (U ● F) a)
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
540 ≡⟨⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
541 FMap U (hom-right uo (λ x₁ → x₁)) ・ FMap U (hom-right uo (λ x₁ → x₁))
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
542 ≡⟨ sym ( IsFunctor.distr (isFunctor U )) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
543 FMap U (hom-right uo (λ x₁ → x₁) ・ hom-right uo (λ x₁ → x₁))
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
544 ≡⟨ cong ( λ z → FMap U z ) ( hom-right-commute1 uo ) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
545 FMap U (hom-right uo ((λ x₁ → x₁) ・ FMap U (hom-right uo (λ x₁ → x₁))) )
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
546 ≡⟨ sym ( cong ( λ z → FMap U z ) ( hom-right-commute2 uo ) ) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
547 FMap U (hom-right uo (λ x₁ → x₁) ・ FMap F (FMap U (hom-right uo (λ x₁ → x₁))))
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
548 ≡⟨ IsFunctor.distr (isFunctor U ) ⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
549 FMap U (hom-right uo (λ x₁ → x₁)) ・ FMap U (FMap F (FMap U (hom-right uo (λ x₁ → x₁))))
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
550 ≡⟨⟩
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
551 TMap μ a ・ FMap (U ● F) (TMap μ a)
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
552 ∎
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
553
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
554
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
555
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
556
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
557
f3a493da92e8 add simple category version
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
558