Mercurial > hg > Members > kono > Proof > category

annotate src/stdalone-kleisli.agda @ 1124:f683d96fbc93 default tip

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