Mercurial > hg > Members > kono > Proof > category

annotate universal-mapping.agda @ 804:2716d2945730

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 25 Apr 2019 12:22:03 +0900
parents 06a7831cf6ce
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
31
17b8bafebad7 add universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 module universal-mapping where
17b8bafebad7 add universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2
56
83ff8d48fdca add unitility
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 55
diff changeset
3 -- Shinji KONO <kono@ie.u-ryukyu.ac.jp>
83ff8d48fdca add unitility
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 55
diff changeset
4
31
17b8bafebad7 add universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open import Category -- https://github.com/konn/category-agda
17b8bafebad7 add universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 open import Level
56
83ff8d48fdca add unitility
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 55
diff changeset
7 open import HomReasoning
159
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 130
diff changeset
8 open import cat-utility
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 130
diff changeset
9 open import Category.Cat
31
17b8bafebad7 add universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10
17b8bafebad7 add universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 open Functor
32
7862ad3b000f Adjoint
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 31
diff changeset
12 open NTrans
7862ad3b000f Adjoint
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 31
diff changeset
13
43
5506abc832c7 uniqness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
14 --
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
15 -- Adjunction yields solution of universal mapping
43
5506abc832c7 uniqness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
16 --
5506abc832c7 uniqness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
17 --
5506abc832c7 uniqness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
18
56
83ff8d48fdca add unitility
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 55
diff changeset
19 Adj2UM : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
690
3d41a8edbf63 fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 689
diff changeset
20 → (adj : Adjunction A B ) → UniversalMapping A B (Adjunction.U adj)
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
21 Adj2UM A B adj = record {
690
3d41a8edbf63 fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 689
diff changeset
22 F = FObj (Adjunction.F adj) ;
3d41a8edbf63 fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 689
diff changeset
23 η = TMap (Adjunction.η adj) ;
43
5506abc832c7 uniqness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
24 _* = solution ;
36
ad997bd9788b isUniversalMapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 35
diff changeset
25 isUniversalMapping = record {
43
5506abc832c7 uniqness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
26 universalMapping = universalMapping;
172
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 171
diff changeset
27 uniquness = uniqueness
36
ad997bd9788b isUniversalMapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 35
diff changeset
28 }
ad997bd9788b isUniversalMapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 35
diff changeset
29 } where
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
30 U : Functor B A
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
31 U = Adjunction.U adj
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
32 F : Functor A B
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
33 F = Adjunction.F adj
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
34 η : NTrans A A identityFunctor ( U ○ F )
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
35 η = Adjunction.η adj
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
36 ε : NTrans B B ( F ○ U ) identityFunctor
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
37 ε = Adjunction.ε adj
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
38 solution : { a : Obj A} { b : Obj B} → ( f : Hom A a (FObj U b) ) → Hom B (FObj F a ) b
43
5506abc832c7 uniqness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
39 solution {_} {b} f = B [ TMap ε b o FMap F f ]
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
40 universalMapping : {a' : Obj A} { b' : Obj B } → { f : Hom A a' (FObj U b') } →
43
5506abc832c7 uniqness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
41 A [ A [ FMap U ( solution f) o TMap η a' ] ≈ f ]
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
42 universalMapping {a} {b} {f} =
38
999e637d14c7 reasoning
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
43 let open ≈-Reasoning (A) in
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
44 begin
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
45 FMap U ( solution f) o TMap η a
39
77c3a5292a2f Reasoning
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
46 ≈⟨⟩
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
47 FMap U ( B [ TMap ε b o FMap F f ] ) o TMap η a
66
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
48 ≈⟨ car (distr U ) ⟩
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
49 ( (FMap U (TMap ε b)) o (FMap U ( FMap F f )) ) o TMap η a
40
c34b1cfe9fdc Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 39
diff changeset
50 ≈⟨ sym assoc ⟩
c34b1cfe9fdc Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 39
diff changeset
51 (FMap U (TMap ε b)) o ((FMap U ( FMap F f )) o TMap η a )
66
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
52 ≈⟨ cdr (nat η) ⟩
40
c34b1cfe9fdc Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 39
diff changeset
53 (FMap U (TMap ε b)) o ((TMap η (FObj U b )) o f )
c34b1cfe9fdc Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 39
diff changeset
54 ≈⟨ assoc ⟩
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
55 ((FMap U (TMap ε b)) o (TMap η (FObj U b))) o f
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
56 ≈⟨ car ( IsAdjunction.adjoint1 ( Adjunction.isAdjunction adj)) ⟩
40
c34b1cfe9fdc Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 39
diff changeset
57 id (FObj U b) o f
c34b1cfe9fdc Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 39
diff changeset
58 ≈⟨ idL ⟩
38
999e637d14c7 reasoning
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
59 f
999e637d14c7 reasoning
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
60 ∎
56
83ff8d48fdca add unitility
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 55
diff changeset
61 lemma1 : (a : Obj A) ( b : Obj B ) ( f : Hom A a (FObj U b) ) → ( g : Hom B (FObj F a) b) →
83ff8d48fdca add unitility
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 55
diff changeset
62 A [ A [ FMap U g o TMap η a ] ≈ f ] →
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
63 B [ (FMap F (A [ FMap U g o TMap η a ] )) ≈ FMap F f ]
44
a626fdd909c3 f replacement
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 43
diff changeset
64 lemma1 a b f g k = IsFunctor.≈-cong (isFunctor F) k
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
65 uniqueness : {a' : Obj A} { b' : Obj B } → { f : Hom A a' (FObj U b') } → { g : Hom B (FObj F a') b'} →
56
83ff8d48fdca add unitility
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 55
diff changeset
66 A [ A [ FMap U g o TMap η a' ] ≈ f ] → B [ solution f ≈ g ]
172
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 171
diff changeset
67 uniqueness {a} {b} {f} {g} k = let open ≈-Reasoning (B) in
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
68 begin
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
69 solution f
44
a626fdd909c3 f replacement
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 43
diff changeset
70 ≈⟨⟩
a626fdd909c3 f replacement
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 43
diff changeset
71 TMap ε b o FMap F f
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
72 ≈⟨ cdr (sym ( lemma1 a b f g k )) ⟩
44
a626fdd909c3 f replacement
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 43
diff changeset
73 TMap ε b o FMap F ( A [ FMap U g o TMap η a ] )
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
74 ≈⟨ cdr (distr F ) ⟩
45
659b8a21caf7 uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
75 TMap ε b o ( FMap F ( FMap U g) o FMap F ( TMap η a ) )
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
76 ≈⟨ assoc ⟩
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
77 ( TMap ε b o FMap F ( FMap U g) ) o FMap F ( TMap η a )
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
78 ≈⟨ sym ( car ( nat ε )) ⟩
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
79 ( g o TMap ε ( FObj F a) ) o FMap F ( TMap η a )
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
80 ≈⟨ sym assoc ⟩
45
659b8a21caf7 uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
81 g o ( TMap ε ( FObj F a) o FMap F ( TMap η a ) )
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
82 ≈⟨ cdr ( IsAdjunction.adjoint2 ( Adjunction.isAdjunction adj )) ⟩
45
659b8a21caf7 uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
83 g o id (FObj F a)
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
84 ≈⟨ idR ⟩
44
a626fdd909c3 f replacement
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 43
diff changeset
85 g
a626fdd909c3 f replacement
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 43
diff changeset
86 ∎
a626fdd909c3 f replacement
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 43
diff changeset
87
43
5506abc832c7 uniqness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
88 --
5506abc832c7 uniqness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
89 --
5506abc832c7 uniqness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
90 -- Universal mapping yields Adjunction
5506abc832c7 uniqness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
91 --
5506abc832c7 uniqness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
92 --
5506abc832c7 uniqness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
93
5506abc832c7 uniqness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
94
5506abc832c7 uniqness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
95 --
5506abc832c7 uniqness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
96 -- F is an functor
5506abc832c7 uniqness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
97 --
5506abc832c7 uniqness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
98
54
5d2a33bb1291 cleanup
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
99 FunctorF : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
690
3d41a8edbf63 fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 689
diff changeset
100 { U : Functor B A }
3d41a8edbf63 fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 689
diff changeset
101 → UniversalMapping A B U → Functor A B
3d41a8edbf63 fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 689
diff changeset
102 FunctorF A B {U} um = record {
41
e9fa5c95eff7 isFunctor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
103 FObj = F;
42
9694f93977ca Functor Identity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
104 FMap = myFMap ;
9694f93977ca Functor Identity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
105 isFunctor = myIsFunctor
41
e9fa5c95eff7 isFunctor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
106 } where
690
3d41a8edbf63 fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 689
diff changeset
107 F : Obj A → Obj B
3d41a8edbf63 fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 689
diff changeset
108 F = UniversalMapping.F um
3d41a8edbf63 fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 689
diff changeset
109 η : (a : Obj A) → Hom A a ( FObj U (F a) )
3d41a8edbf63 fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 689
diff changeset
110 η = UniversalMapping.η um
3d41a8edbf63 fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 689
diff changeset
111 _* : (UniversalMapping A B U ) → { a : Obj A} { b : Obj B} → ( Hom A a (FObj U b) ) → Hom B (F a ) b
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
112 _* _ = UniversalMapping._* um
56
83ff8d48fdca add unitility
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 55
diff changeset
113 myFMap : {a b : Obj A} → Hom A a b → Hom B (F a) (F b)
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
114 myFMap f = (_* um) (A [ η (Category.cod A f ) o f ])
56
83ff8d48fdca add unitility
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 55
diff changeset
115 lemma-id1 : {a : Obj A} → A [ A [ FMap U (id1 B (F a)) o η a ] ≈ (A [ (η a) o (id1 A a) ]) ]
46
5d1b0fd2ad21 Functor cong done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
116 lemma-id1 {a} = let open ≈-Reasoning (A) in
42
9694f93977ca Functor Identity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
117 begin
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
118 FMap U (id1 B (F a)) o η a
42
9694f93977ca Functor Identity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
119 ≈⟨ ( car ( IsFunctor.identity ( isFunctor U ))) ⟩
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
120 id (FObj U ( F a )) o η a
42
9694f93977ca Functor Identity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
121 ≈⟨ idL ⟩
9694f93977ca Functor Identity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
122 η a
9694f93977ca Functor Identity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
123 ≈⟨ sym idR ⟩
46
5d1b0fd2ad21 Functor cong done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
124 η a o id a
42
9694f93977ca Functor Identity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
125 ∎
46
5d1b0fd2ad21 Functor cong done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
126 lemma-id : {a : Obj A} → B [ ( (_* um) (A [ (η a) o (id1 A a)] )) ≈ (id1 B (F a)) ]
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
127 lemma-id {a} = ( IsUniversalMapping.uniquness ( UniversalMapping.isUniversalMapping um ) ) lemma-id1
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
128 lemma-cong2 : (a b : Obj A) (f g : Hom A a b) → A [ f ≈ g ] →
46
5d1b0fd2ad21 Functor cong done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
129 A [ A [ FMap U ((_* um) (A [ η b o g ]) ) o η a ] ≈ A [ η b o f ] ]
5d1b0fd2ad21 Functor cong done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
130 lemma-cong2 a b f g eq = let open ≈-Reasoning (A) in
5d1b0fd2ad21 Functor cong done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
131 begin
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
132 ( FMap U ((_* um) (A [ η b o g ]) )) o η a
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
133 ≈⟨ ( IsUniversalMapping.universalMapping ( UniversalMapping.isUniversalMapping um )) ⟩
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
134 η b o g
46
5d1b0fd2ad21 Functor cong done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
135 ≈⟨ ( IsCategory.o-resp-≈ ( Category.isCategory A ) (sym eq) (refl-hom) ) ⟩
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
136 η b o f
46
5d1b0fd2ad21 Functor cong done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
137 ∎
5d1b0fd2ad21 Functor cong done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
138 lemma-cong1 : (a b : Obj A) (f g : Hom A a b) → A [ f ≈ g ] → B [ (_* um) (A [ η b o f ] ) ≈ (_* um) (A [ η b o g ]) ]
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
139 lemma-cong1 a b f g eq = ( IsUniversalMapping.uniquness ( UniversalMapping.isUniversalMapping um ) ) ( lemma-cong2 a b f g eq )
46
5d1b0fd2ad21 Functor cong done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
140 lemma-cong : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → B [ myFMap f ≈ myFMap g ]
5d1b0fd2ad21 Functor cong done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
141 lemma-cong {a} {b} {f} {g} eq = lemma-cong1 a b f g eq
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
142 lemma-distr2 : (a b c : Obj A) (f : Hom A a b) (g : Hom A b c) →
47
0124e3c971e5 F is Functor proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 46
diff changeset
143 A [ A [ FMap U (B [(_* um) (A [ η c o g ]) o (_* um)( A [ η b o f ]) ]) o η a ] ≈ (A [ η c o A [ g o f ] ]) ]
0124e3c971e5 F is Functor proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 46
diff changeset
144 lemma-distr2 a b c f g = let open ≈-Reasoning (A) in
0124e3c971e5 F is Functor proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 46
diff changeset
145 begin
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
146 ( FMap U (B [(_* um) (A [ η c o g ]) o (_* um)( A [ η b o f ]) ] ) ) o η a
66
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
147 ≈⟨ car (distr U ) ⟩
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
148 (( FMap U ((_* um) (A [ η c o g ])) o ( FMap U ((_* um)( A [ η b o f ])))) ) o η a
47
0124e3c971e5 F is Functor proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 46
diff changeset
149 ≈⟨ sym assoc ⟩
0124e3c971e5 F is Functor proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 46
diff changeset
150 ( FMap U ((_* um) (A [ η c o g ])) o (( FMap U ((_* um)( A [ η b o f ])))) o η a )
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
151 ≈⟨ cdr ( IsUniversalMapping.universalMapping ( UniversalMapping.isUniversalMapping um )) ⟩
47
0124e3c971e5 F is Functor proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 46
diff changeset
152 ( FMap U ((_* um) (A [ η c o g ])) o ( η b o f) )
0124e3c971e5 F is Functor proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 46
diff changeset
153 ≈⟨ assoc ⟩
0124e3c971e5 F is Functor proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 46
diff changeset
154 ( FMap U ((_* um) (A [ η c o g ])) o η b) o f
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
155 ≈⟨ car ( IsUniversalMapping.universalMapping ( UniversalMapping.isUniversalMapping um )) ⟩
47
0124e3c971e5 F is Functor proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 46
diff changeset
156 ( η c o g ) o f
0124e3c971e5 F is Functor proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 46
diff changeset
157 ≈⟨ sym assoc ⟩
0124e3c971e5 F is Functor proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 46
diff changeset
158 η c o ( g o f )
0124e3c971e5 F is Functor proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 46
diff changeset
159 ∎
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
160 lemma-distr1 : (a b c : Obj A) (f : Hom A a b) (g : Hom A b c) →
47
0124e3c971e5 F is Functor proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 46
diff changeset
161 B [ (_* um) (A [ η c o A [ g o f ] ]) ≈ (B [(_* um) (A [ η c o g ]) o (_* um)( A [ η b o f ]) ] )]
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
162 lemma-distr1 a b c f g = ( IsUniversalMapping.uniquness ( UniversalMapping.isUniversalMapping um )) (lemma-distr2 a b c f g )
47
0124e3c971e5 F is Functor proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 46
diff changeset
163 lemma-distr : {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} → B [ myFMap (A [ g o f ]) ≈ (B [ myFMap g o myFMap f ] )]
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
164 lemma-distr {a} {b} {c} {f} {g} = lemma-distr1 a b c f g
42
9694f93977ca Functor Identity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
165 myIsFunctor : IsFunctor A B F myFMap
9694f93977ca Functor Identity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
166 myIsFunctor =
46
5d1b0fd2ad21 Functor cong done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
167 record { ≈-cong = lemma-cong
42
9694f93977ca Functor Identity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
168 ; identity = lemma-id
47
0124e3c971e5 F is Functor proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 46
diff changeset
169 ; distr = lemma-distr
42
9694f93977ca Functor Identity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
170 }
41
e9fa5c95eff7 isFunctor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
171
48
d5a8edad2a83 naturarity of η
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
172 --
d5a8edad2a83 naturarity of η
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
173 -- naturality of η
d5a8edad2a83 naturarity of η
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
174 --
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
175 nat-η : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
689
fb9fc9652c04 fix again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 688
diff changeset
176 { U : Functor B A }
690
3d41a8edbf63 fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 689
diff changeset
177 → (um : UniversalMapping A B U ) →
689
fb9fc9652c04 fix again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 688
diff changeset
178 NTrans A A identityFunctor ( U ○ FunctorF A B um )
690
3d41a8edbf63 fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 689
diff changeset
179 nat-η A B {U} um = record {
48
d5a8edad2a83 naturarity of η
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
180 TMap = η ; isNTrans = myIsNTrans
d5a8edad2a83 naturarity of η
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
181 } where
690
3d41a8edbf63 fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 689
diff changeset
182 F : Obj A → Obj B
3d41a8edbf63 fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 689
diff changeset
183 F = UniversalMapping.F um
3d41a8edbf63 fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 689
diff changeset
184 η : (a : Obj A) → Hom A a ( FObj U (F a) )
3d41a8edbf63 fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 689
diff changeset
185 η = UniversalMapping.η um
48
d5a8edad2a83 naturarity of η
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
186 F' : Functor A B
54
5d2a33bb1291 cleanup
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
187 F' = FunctorF A B um
690
3d41a8edbf63 fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 689
diff changeset
188 _* : (UniversalMapping A B U ) → { a : Obj A} { b : Obj B} → ( Hom A a (FObj U b) ) → Hom B (F a ) b
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
189 _* _ = UniversalMapping._* um
130
5f331dfc000b remove Kleisli record
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 66
diff changeset
190 commute : {a b : Obj A} {f : Hom A a b}
48
d5a8edad2a83 naturarity of η
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
191 → A [ A [ (FMap U (FMap F' f)) o ( η a ) ] ≈ A [ (η b ) o f ] ]
130
5f331dfc000b remove Kleisli record
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 66
diff changeset
192 commute {a} {b} {f} = let open ≈-Reasoning (A) in
49
d2b5be1143bf naturality of ε
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
193 begin
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
194 (FMap U (FMap F' f)) o ( η a )
49
d2b5be1143bf naturality of ε
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
195 ≈⟨⟩
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
196 (FMap U ((_* um) (A [ η b o f ]))) o ( η a )
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
197 ≈⟨ (IsUniversalMapping.universalMapping ( UniversalMapping.isUniversalMapping um )) ⟩
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
198 (η b ) o f
49
d2b5be1143bf naturality of ε
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
199 ∎
48
d5a8edad2a83 naturarity of η
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
200 myIsNTrans : IsNTrans A A identityFunctor ( U ○ F' ) η
130
5f331dfc000b remove Kleisli record
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 66
diff changeset
201 myIsNTrans = record { commute = commute }
49
d2b5be1143bf naturality of ε
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
202
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
203 nat-ε : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
689
fb9fc9652c04 fix again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 688
diff changeset
204 { U : Functor B A }
690
3d41a8edbf63 fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 689
diff changeset
205 → (um : UniversalMapping A B U ) →
689
fb9fc9652c04 fix again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 688
diff changeset
206 NTrans B B ( FunctorF A B um ○ U ) identityFunctor
690
3d41a8edbf63 fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 689
diff changeset
207 nat-ε A B {U} um = record {
49
d2b5be1143bf naturality of ε
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
208 TMap = ε ; isNTrans = myIsNTrans
d2b5be1143bf naturality of ε
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
209 } where
690
3d41a8edbf63 fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 689
diff changeset
210 F : Obj A → Obj B
3d41a8edbf63 fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 689
diff changeset
211 F = UniversalMapping.F um
3d41a8edbf63 fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 689
diff changeset
212 η : (a : Obj A) → Hom A a ( FObj U (F a) )
3d41a8edbf63 fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 689
diff changeset
213 η = UniversalMapping.η um
49
d2b5be1143bf naturality of ε
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
214 F' : Functor A B
54
5d2a33bb1291 cleanup
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
215 F' = FunctorF A B um
690
3d41a8edbf63 fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 689
diff changeset
216 _* : (UniversalMapping A B U ) → { a : Obj A} { b : Obj B} → ( Hom A a (FObj U b) ) → Hom B (F a ) b
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
217 _* _ = UniversalMapping._* um
56
83ff8d48fdca add unitility
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 55
diff changeset
218 ε : ( b : Obj B ) → Hom B ( FObj F' ( FObj U b) ) b
49
d2b5be1143bf naturality of ε
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
219 ε b = (_* um) ( id1 A (FObj U b))
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
220 lemma-nat1 : (a b : Obj B) (f : Hom B a b ) →
51
adc6bd3c9270 on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 50
diff changeset
221 A [ A [ FMap U ( B [ (um *) (id1 A (FObj U b)) o ((um *) (A [ η (FObj U b) o FMap U f ])) ] ) o η (FObj U a) ]
adc6bd3c9270 on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 50
diff changeset
222 ≈ A [ FMap U f o id1 A (FObj U a) ] ]
adc6bd3c9270 on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 50
diff changeset
223 lemma-nat1 a b f = let open ≈-Reasoning (A) in
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
224 begin
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
225 FMap U ( B [ (um *) (id1 A (FObj U b)) o ((um *) ( η (FObj U b) o FMap U f )) ] ) o η (FObj U a)
66
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
226 ≈⟨ car ( distr U ) ⟩
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
227 ( FMap U ((um *) (id1 A (FObj U b))) o FMap U ((um *) ( η (FObj U b) o FMap U f )) ) o η (FObj U a)
51
adc6bd3c9270 on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 50
diff changeset
228 ≈⟨ sym assoc ⟩
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
229 FMap U ((um *) (id1 A (FObj U b))) o ( FMap U ((um *) ( η (FObj U b) o FMap U f ))) o η (FObj U a)
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
230 ≈⟨ cdr ((IsUniversalMapping.universalMapping ( UniversalMapping.isUniversalMapping um )) ) ⟩
51
adc6bd3c9270 on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 50
diff changeset
231 FMap U ((um *) (id1 A (FObj U b))) o ( η (FObj U b) o FMap U f )
adc6bd3c9270 on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 50
diff changeset
232 ≈⟨ assoc ⟩
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
233 (FMap U ((um *) (id1 A (FObj U b))) o η (FObj U b)) o FMap U f
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
234 ≈⟨ car ((IsUniversalMapping.universalMapping ( UniversalMapping.isUniversalMapping um )) ) ⟩
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
235 id1 A (FObj U b) o FMap U f
51
adc6bd3c9270 on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 50
diff changeset
236 ≈⟨ idL ⟩
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
237 FMap U f
51
adc6bd3c9270 on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 50
diff changeset
238 ≈⟨ sym idR ⟩
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
239 FMap U f o id (FObj U a)
51
adc6bd3c9270 on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 50
diff changeset
240 ∎
56
83ff8d48fdca add unitility
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 55
diff changeset
241 lemma-nat2 : (a b : Obj B) (f : Hom B a b ) → A [ A [ FMap U ( B [ f o ((um *) (id1 A (FObj U a ))) ] ) o η (FObj U a) ]
52
0fc0dbda7b55 nat-ε proved
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 51
diff changeset
242 ≈ A [ FMap U f o id1 A (FObj U a) ] ]
0fc0dbda7b55 nat-ε proved
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 51
diff changeset
243 lemma-nat2 a b f = let open ≈-Reasoning (A) in
0fc0dbda7b55 nat-ε proved
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 51
diff changeset
244 begin
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
245 FMap U ( B [ f o ((um *) (id1 A (FObj U a ))) ]) o η (FObj U a)
66
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
246 ≈⟨ car ( distr U ) ⟩
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
247 (FMap U f o FMap U ((um *) (id1 A (FObj U a )))) o η (FObj U a)
52
0fc0dbda7b55 nat-ε proved
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 51
diff changeset
248 ≈⟨ sym assoc ⟩
0fc0dbda7b55 nat-ε proved
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 51
diff changeset
249 FMap U f o ( FMap U ((um *) (id1 A (FObj U a ))) o η (FObj U a) )
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
250 ≈⟨ cdr ( IsUniversalMapping.universalMapping ( UniversalMapping.isUniversalMapping um)) ⟩
52
0fc0dbda7b55 nat-ε proved
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 51
diff changeset
251 FMap U f o id (FObj U a )
0fc0dbda7b55 nat-ε proved
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 51
diff changeset
252 ∎
130
5f331dfc000b remove Kleisli record
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 66
diff changeset
253 commute : {a b : Obj B} {f : Hom B a b }
49
d2b5be1143bf naturality of ε
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
254 → B [ B [ f o (ε a) ] ≈ B [(ε b) o (FMap F' (FMap U f)) ] ]
130
5f331dfc000b remove Kleisli record
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 66
diff changeset
255 commute {a} {b} {f} = let open ≈-Reasoning (B) in
49
d2b5be1143bf naturality of ε
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
256 sym ( begin
d2b5be1143bf naturality of ε
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
257 ε b o (FMap F' (FMap U f))
d2b5be1143bf naturality of ε
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
258 ≈⟨⟩
50
b518af3a9b07 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
259 ε b o ((_* um) (A [ η (FObj U b) o (FMap U f) ]))
b518af3a9b07 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
260 ≈⟨⟩
b518af3a9b07 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
261 ((_* um) ( id1 A (FObj U b))) o ((_* um) (A [ η (FObj U b) o (FMap U f) ]))
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
262 ≈⟨ sym ( ( IsUniversalMapping.uniquness ( UniversalMapping.isUniversalMapping um ) (lemma-nat1 a b f))) ⟩
51
adc6bd3c9270 on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 50
diff changeset
263 (_* um) ( A [ FMap U f o id1 A (FObj U a) ] )
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
264 ≈⟨ (IsUniversalMapping.uniquness ( UniversalMapping.isUniversalMapping um ) (lemma-nat2 a b f)) ⟩
50
b518af3a9b07 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
265 f o ((_* um) ( id1 A (FObj U a)))
b518af3a9b07 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
266 ≈⟨⟩
49
d2b5be1143bf naturality of ε
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
267 f o (ε a)
d2b5be1143bf naturality of ε
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
268 ∎ )
d2b5be1143bf naturality of ε
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
269 myIsNTrans : IsNTrans B B ( F' ○ U ) identityFunctor　ε
130
5f331dfc000b remove Kleisli record
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 66
diff changeset
270 myIsNTrans = record { commute = commute }
53
b4530a807918 start adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 52
diff changeset
271
b4530a807918 start adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 52
diff changeset
272 ------
b4530a807918 start adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 52
diff changeset
273 --
b4530a807918 start adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 52
diff changeset
274 -- Adjunction Construction from Universal Mapping
b4530a807918 start adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 52
diff changeset
275 --
b4530a807918 start adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 52
diff changeset
276 -----
b4530a807918 start adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 52
diff changeset
277
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
278 UMAdjunction : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') →
690
3d41a8edbf63 fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 689
diff changeset
279 ( U : Functor B A ) →
3d41a8edbf63 fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 689
diff changeset
280 (um : UniversalMapping A B U ) →
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
281 Adjunction A B
690
3d41a8edbf63 fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 689
diff changeset
282 UMAdjunction A B U um = record {
689
fb9fc9652c04 fix again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 688
diff changeset
283 U = U ;
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
284 F = FunctorF A B um ;
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
285 η = nat-η A B um ;
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
286 ε = nat-ε A B um ;
53
b4530a807918 start adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 52
diff changeset
287 isAdjunction = record {
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
288 adjoint1 = adjoint1 ;
53
b4530a807918 start adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 52
diff changeset
289 adjoint2 = adjoint2
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
290 }
53
b4530a807918 start adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 52
diff changeset
291 } where
690
3d41a8edbf63 fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 689
diff changeset
292 F' : Obj A → Obj B
3d41a8edbf63 fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 689
diff changeset
293 F' = UniversalMapping.F um
3d41a8edbf63 fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 689
diff changeset
294 η' : (a : Obj A) → Hom A a ( FObj U (F' a) )
3d41a8edbf63 fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 689
diff changeset
295 η' = UniversalMapping.η um
53
b4530a807918 start adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 52
diff changeset
296 F : Functor A B
54
5d2a33bb1291 cleanup
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
297 F = FunctorF A B um
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
298 η : NTrans A A identityFunctor ( U ○ F )
54
5d2a33bb1291 cleanup
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
299 η = nat-η A B um
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
300 ε : NTrans B B ( F ○ U ) identityFunctor
54
5d2a33bb1291 cleanup
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
301 ε = nat-ε A B um
690
3d41a8edbf63 fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 689
diff changeset
302 _* : UniversalMapping A B U → { a : Obj A}{ b : Obj B} → ( Hom A a (FObj U b) ) → Hom B (FObj F a ) b
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
303 _* _ = UniversalMapping._* um
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
304 isUniversalMapping = UniversalMapping.isUniversalMapping
56
83ff8d48fdca add unitility
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 55
diff changeset
305 adjoint1 : { b : Obj B } →
53
b4530a807918 start adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 52
diff changeset
306 A [ A [ ( FMap U ( TMap ε b )) o ( TMap η ( FObj U b )) ] ≈ id1 A (FObj U b) ]
55
1716403c92c2 Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 54
diff changeset
307 adjoint1 {b} = let open ≈-Reasoning (A) in
1716403c92c2 Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 54
diff changeset
308 begin
1716403c92c2 Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 54
diff changeset
309 FMap U ( TMap ε b ) o TMap η ( FObj U b )
1716403c92c2 Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 54
diff changeset
310 ≈⟨⟩
1716403c92c2 Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 54
diff changeset
311 FMap U ((_* um) ( id1 A (FObj U b))) o η' ( FObj U b )
1716403c92c2 Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 54
diff changeset
312 ≈⟨ IsUniversalMapping.universalMapping ( isUniversalMapping um ) ⟩
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
313 id (FObj U b)
55
1716403c92c2 Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 54
diff changeset
314 ∎
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
315 lemma-adj1 : (a : Obj A) →
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
316 A [ A [ FMap U ((B [((_* um) ( id1 A (FObj U ( FObj F a )))) o (_* um) (A [ η' (FObj U ( FObj F a )) o ( η' a ) ]) ])) o η' a ]
55
1716403c92c2 Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 54
diff changeset
317 ≈ (η' a) ]
1716403c92c2 Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 54
diff changeset
318 lemma-adj1 a = let open ≈-Reasoning (A) in
1716403c92c2 Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 54
diff changeset
319 begin
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
320 FMap U ((B [((_* um) ( id1 A (FObj U ( FObj F a )))) o (_* um) (A [ η' (FObj U ( FObj F a )) o ( η' a ) ]) ])) o η' a
66
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
321 ≈⟨ car (distr U) ⟩
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
322 (FMap U ((_* um) ( id1 A (FObj U ( FObj F a)))) o FMap U ((_* um) (A [ η' (FObj U ( FObj F a )) o ( η' a ) ]))) o η' a
55
1716403c92c2 Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 54
diff changeset
323 ≈⟨ sym assoc ⟩
1716403c92c2 Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 54
diff changeset
324 FMap U ((_* um) ( id1 A (FObj U ( FObj F a)))) o ( FMap U ((_* um) (A [ η' (FObj U ( FObj F a )) o ( η' a ) ])) o η' a )
1716403c92c2 Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 54
diff changeset
325 ≈⟨ cdr (IsUniversalMapping.universalMapping ( isUniversalMapping um)) ⟩
1716403c92c2 Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 54
diff changeset
326 FMap U ((_* um) ( id1 A (FObj U ( FObj F a)))) o ( η' (FObj U ( FObj F a )) o ( η' a ) )
1716403c92c2 Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 54
diff changeset
327 ≈⟨ assoc ⟩
1716403c92c2 Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 54
diff changeset
328 (FMap U ((_* um) ( id1 A (FObj U ( FObj F a)))) o ( η' (FObj U ( FObj F a )))) o ( η' a )
1716403c92c2 Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 54
diff changeset
329 ≈⟨ car (IsUniversalMapping.universalMapping ( isUniversalMapping um)) ⟩
1716403c92c2 Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 54
diff changeset
330 id (FObj U ( FObj F a)) o ( η' a )
1716403c92c2 Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 54
diff changeset
331 ≈⟨ idL ⟩
1716403c92c2 Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 54
diff changeset
332 η' a
1716403c92c2 Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 54
diff changeset
333 ∎
56
83ff8d48fdca add unitility
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 55
diff changeset
334 lemma-adj2 : (a : Obj A) → A [ A [ FMap U (id1 B (FObj F a)) o η' a ] ≈ η' a ]
55
1716403c92c2 Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 54
diff changeset
335 lemma-adj2 a = let open ≈-Reasoning (A) in
1716403c92c2 Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 54
diff changeset
336 begin
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
337 FMap U (id1 B (FObj F a)) o η' a
55
1716403c92c2 Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 54
diff changeset
338 ≈⟨ car ( IsFunctor.identity ( isFunctor U)) ⟩
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
339 id (FObj U (FObj F a)) o η' a
55
1716403c92c2 Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 54
diff changeset
340 ≈⟨ idL ⟩
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
341 η' a
55
1716403c92c2 Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 54
diff changeset
342 ∎
56
83ff8d48fdca add unitility
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 55
diff changeset
343 adjoint2 : {a : Obj A} →
53
b4530a807918 start adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 52
diff changeset
344 B [ B [ ( TMap ε ( FObj F a )) o ( FMap F ( TMap η a )) ] ≈ id1 B (FObj F a) ]
55
1716403c92c2 Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 54
diff changeset
345 adjoint2 {a} = let open ≈-Reasoning (B) in
1716403c92c2 Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 54
diff changeset
346 begin
1716403c92c2 Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 54
diff changeset
347 TMap ε ( FObj F a ) o FMap F ( TMap η a )
1716403c92c2 Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 54
diff changeset
348 ≈⟨⟩
1716403c92c2 Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 54
diff changeset
349 ((_* um) ( id1 A (FObj U ( FObj F a )))) o (_* um) (A [ η' (FObj U ( FObj F a )) o ( η' a ) ])
1716403c92c2 Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 54
diff changeset
350 ≈⟨ sym ( ( IsUniversalMapping.uniquness ( isUniversalMapping um ) (lemma-adj1 a))) ⟩
1716403c92c2 Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 54
diff changeset
351 (_* um)( η' a )
1716403c92c2 Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 54
diff changeset
352 ≈⟨ IsUniversalMapping.uniquness ( isUniversalMapping um ) (lemma-adj2 a) ⟩
1716403c92c2 Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 54
diff changeset
353 id1 B (FObj F a)
1716403c92c2 Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 54
diff changeset
354 ∎
1716403c92c2 Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 54
diff changeset
355
1716403c92c2 Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 54
diff changeset
356
171
d25b0948e006 unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 159
diff changeset
357 ------
d25b0948e006 unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 159
diff changeset
358 --
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
359 -- Hom Set Adjunction
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
360 --
171
d25b0948e006 unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 159
diff changeset
361 -- Hom(F(-),-) = Hom(-,U(-))
d25b0948e006 unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 159
diff changeset
362 -- Unity of opposite
d25b0948e006 unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 159
diff changeset
363 -----
d25b0948e006 unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 159
diff changeset
364
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
365 -- Assuming
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
366 -- naturality of left (Φ)
177
63f6157a6a19 comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 176
diff changeset
367 -- k = Hom A b b' ; f' = k o f h Hom A a' a ; f' = f o h
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
368 -- left left
775
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
369 -- f : Hom A F(a) b ←------- f* : Hom B a U(b) f' : Hom A F(a')b ←------ f'* : Hom B a' U(b)
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
370 -- | -------→ | | |
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
371 -- |k right |U(k) |F(h) |h
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
372 -- ↓ ↓ ↓ ↓
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
373 -- f': Hom A F(a) b'←------ f'* : Hom B a U(b') f: Hom A F(a) b ←-------- f* : Hom B a U(b)
177
63f6157a6a19 comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 176
diff changeset
374 -- left left
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
375
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
376 record UnityOfOppsite {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
377 ( U : Functor B A )
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
378 ( F : Functor A B )
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
379 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
380 field
775
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
381 left : {a : Obj A} { b : Obj B } → Hom A a ( FObj U b ) → Hom B (FObj F a) b
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
382 right : {a : Obj A} { b : Obj B } → Hom B (FObj F a) b → Hom A a ( FObj U b )
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
383 left-injective : {a : Obj A} { b : Obj B } → {f : Hom A a (FObj U b) } → A [ right ( left f ) ≈ f ]
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
384 right-injective : {a : Obj A} { b : Obj B } → {f : Hom B (FObj F a) b } → B [ left ( right f ) ≈ f ]
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
385 --- naturality of Φ
775
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
386 right-commute1 : {a : Obj A} {b b' : Obj B } →
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 177
diff changeset
387 { f : Hom B (FObj F a) b } → { k : Hom B b b' } →
775
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
388 A [ right ( B [ k o f ] ) ≈ A [ FMap U k o right f ] ]
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
389 right-commute2 : {a a' : Obj A} {b : Obj B } →
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 177
diff changeset
390 { f : Hom B (FObj F a) b } → { h : Hom A a' a } →
775
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
391 A [ right ( B [ f o FMap F h ] ) ≈ A [ right f o h ] ]
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
392 r-cong : {a : Obj A} { b : Obj B } → { f g : Hom A a ( FObj U b ) } → A [ f ≈ g ] → B [ left f ≈ left g ]
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
393 l-cong : {a : Obj A} { b : Obj B } → { f g : Hom B (FObj F a) b } → B [ f ≈ g ] → A [ right f ≈ right g ]
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
394 -- naturality of left (Φ-1)
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
395 left-commute1 : {a : Obj A} {b b' : Obj B } →
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 177
diff changeset
396 { g : Hom A a (FObj U b)} → { k : Hom B b b' } →
775
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
397 B [ B [ k o left g ] ≈ left ( A [ FMap U k o g ] ) ]
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
398 left-commute1 {a} {b} {b'} {g} {k} = let open ≈-Reasoning (B) in
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
399 begin
775
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
400 k o left g
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
401 ≈⟨ sym right-injective ⟩
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
402 left ( right ( k o left g ) )
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
403 ≈⟨ r-cong right-commute1 ⟩
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
404 left ( A [ FMap U k o right ( left g ) ] )
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
405 ≈⟨ r-cong (lemma-1 g k) ⟩
775
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
406 left ( A [ FMap U k o g ] )
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
407 ∎ where
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 177
diff changeset
408 lemma-1 : {a : Obj A} {b b' : Obj B } →
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 177
diff changeset
409 ( g : Hom A a (FObj U b)) → ( k : Hom B b b' ) →
775
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
410 A [ A [ FMap U k o right ( left g ) ] ≈ A [ FMap U k o g ] ]
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
411 lemma-1 g k = let open ≈-Reasoning (A) in
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
412 begin
775
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
413 FMap U k o right ( left g )
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
414 ≈⟨ cdr ( left-injective) ⟩
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
415 FMap U k o g
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
416 ∎
775
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
417 left-commute2 : {a a' : Obj A} {b : Obj B } →
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 177
diff changeset
418 { g : Hom A a (FObj U b) } → { h : Hom A a' a } →
775
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
419 B [ B [ left g o FMap F h ] ≈ left ( A [ g o h ] ) ]
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
420 left-commute2 {a} {a'} {b} {g} {h} = let open ≈-Reasoning (B) in
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
421 begin
775
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
422 left g o FMap F h
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
423 ≈⟨ sym right-injective ⟩
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
424 left ( right ( left g o FMap F h ))
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
425 ≈⟨ r-cong right-commute2 ⟩
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
426 left ( A [ right ( left g ) o h ] )
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
427 ≈⟨ r-cong ( lemma-2 g h ) ⟩
775
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
428 left ( A [ g o h ] )
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
429 ∎ where
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 177
diff changeset
430 lemma-2 : {a a' : Obj A} {b : Obj B } →
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 177
diff changeset
431 ( g : Hom A a (FObj U b)) → ( h : Hom A a' a ) →
775
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
432 A [ A [ right ( left g ) o h ] ≈ A [ g o h ] ]
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
433 lemma-2 g h = let open ≈-Reasoning (A) in car ( left-injective )
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
434
171
d25b0948e006 unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 159
diff changeset
435 Adj2UO : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
436 ( adj : Adjunction A B ) → UnityOfOppsite A B (Adjunction.U adj) (Adjunction.F adj)
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
437 Adj2UO A B adj = record {
775
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
438 left = left ;
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
439 right = right ;
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
440 left-injective = left-injective ;
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
441 right-injective = right-injective ;
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
442 right-commute1 = right-commute1 ;
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
443 right-commute2 = right-commute2 ;
175
795be747d7a9 hom-set to universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 174
diff changeset
444 r-cong = r-cong ;
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
445 l-cong = l-cong
171
d25b0948e006 unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 159
diff changeset
446 } where
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
447 U : Functor B A
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
448 U = Adjunction.U adj
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
449 F : Functor A B
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
450 F = Adjunction.F adj
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
451 η : NTrans A A identityFunctor ( U ○ F )
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
452 η = Adjunction.η adj
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
453 ε : NTrans B B ( F ○ U ) identityFunctor
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
454 ε = Adjunction.ε adj
775
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
455 left : {a : Obj A} { b : Obj B } → Hom A a ( FObj U b ) → Hom B (FObj F a) b
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
456 left {a} {b} f = B [ TMap ε b o FMap F f ]
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
457 right : {a : Obj A} { b : Obj B } → Hom B (FObj F a) b → Hom A a ( FObj U b )
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
458 right {a} {b} f = A [ FMap U f o (TMap η a) ]
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
459 left-injective : {a : Obj A} { b : Obj B } → {f : Hom A a (FObj U b) } → A [ right ( left f ) ≈ f ]
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
460 left-injective {a} {b} {f} = let open ≈-Reasoning (A) in
171
d25b0948e006 unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 159
diff changeset
461 begin
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
462 FMap U (B [ TMap ε b o FMap F f ]) o (TMap η a)
171
d25b0948e006 unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 159
diff changeset
463 ≈⟨ car ( distr U ) ⟩
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
464 ( FMap U (TMap ε b) o FMap U (FMap F f )) o (TMap η a)
171
d25b0948e006 unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 159
diff changeset
465 ≈↑⟨ assoc ⟩
d25b0948e006 unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 159
diff changeset
466 FMap U (TMap ε b) o ( FMap U (FMap F f ) o (TMap η a) )
d25b0948e006 unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 159
diff changeset
467 ≈⟨ cdr ( nat η) ⟩
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
468 FMap U (TMap ε b) o ((TMap η (FObj U b)) o f )
171
d25b0948e006 unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 159
diff changeset
469 ≈⟨ assoc ⟩
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
470 (FMap U (TMap ε b) o (TMap η (FObj U b))) o f
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
471 ≈⟨ car ( IsAdjunction.adjoint1 ( Adjunction.isAdjunction adj )) ⟩
171
d25b0948e006 unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 159
diff changeset
472 id1 A (FObj U b) o f
d25b0948e006 unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 159
diff changeset
473 ≈⟨ idL ⟩
d25b0948e006 unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 159
diff changeset
474 f
d25b0948e006 unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 159
diff changeset
475 ∎
775
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
476 right-injective : {a : Obj A} { b : Obj B } → {f : Hom B (FObj F a) b } → B [ left ( right f ) ≈ f ]
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
477 right-injective {a} {b} {f} = let open ≈-Reasoning (B) in
171
d25b0948e006 unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 159
diff changeset
478 begin
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
479 TMap ε b o FMap F ( A [ FMap U f o (TMap η a) ])
171
d25b0948e006 unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 159
diff changeset
480 ≈⟨ cdr ( distr F ) ⟩
d25b0948e006 unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 159
diff changeset
481 TMap ε b o ( FMap F (FMap U f) o FMap F (TMap η a))
d25b0948e006 unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 159
diff changeset
482 ≈⟨ assoc ⟩
d25b0948e006 unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 159
diff changeset
483 ( TMap ε b o FMap F (FMap U f)) o FMap F (TMap η a)
d25b0948e006 unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 159
diff changeset
484 ≈↑⟨ car (nat ε) ⟩
d25b0948e006 unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 159
diff changeset
485 ( f o TMap ε ( FObj F a )) o ( FMap F ( TMap η a ))
d25b0948e006 unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 159
diff changeset
486 ≈↑⟨ assoc ⟩
d25b0948e006 unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 159
diff changeset
487 f o ( TMap ε ( FObj F a ) o ( FMap F ( TMap η a )))
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
488 ≈⟨ cdr ( IsAdjunction.adjoint2 ( Adjunction.isAdjunction adj )) ⟩
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
489 f o id1 B (FObj F a)
171
d25b0948e006 unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 159
diff changeset
490 ≈⟨ idR ⟩
d25b0948e006 unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 159
diff changeset
491 f
d25b0948e006 unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 159
diff changeset
492 ∎
775
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
493 right-commute1 : {a : Obj A} {b b' : Obj B } →
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 177
diff changeset
494 { f : Hom B (FObj F a) b } → { k : Hom B b b' } →
775
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
495 A [ right ( B [ k o f ] ) ≈ A [ FMap U k o right f ] ]
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
496 right-commute1 {a} {b} {b'} {f} {k} = let open ≈-Reasoning (A) in
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
497 begin
775
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
498 right ( B [ k o f ] )
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
499 ≈⟨⟩
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
500 FMap U ( B [ k o f ] ) o (TMap η a)
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
501 ≈⟨ car (distr U) ⟩
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
502 ( FMap U k o FMap U f ) o (TMap η a)
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
503 ≈↑⟨ assoc ⟩
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
504 FMap U k o ( FMap U f o (TMap η a) )
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
505 ≈⟨⟩
775
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
506 FMap U k o right f
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
507 ∎
775
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
508 right-commute2 : {a a' : Obj A} {b : Obj B } →
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 177
diff changeset
509 { f : Hom B (FObj F a) b } → { h : Hom A a' a} →
775
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
510 A [ right ( B [ f o FMap F h ] ) ≈ A [ right f o h ] ]
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
511 right-commute2 {a'} {a} {b} {f} {h} = let open ≈-Reasoning (A) in
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
512 begin
775
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
513 right ( B [ f o FMap F h ] )
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
514 ≈⟨⟩
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
515 FMap U ( B [ f o FMap F h ] ) o TMap η a
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
516 ≈⟨ car (distr U ) ⟩
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
517 (FMap U f o FMap U (FMap F h )) o TMap η a
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
518 ≈↑⟨ assoc ⟩
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
519 FMap U f o ( FMap U (FMap F h ) o TMap η a )
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
520 ≈⟨ cdr ( nat η) ⟩
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
521 FMap U f o (TMap η a' o h )
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
522 ≈⟨ assoc ⟩
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
523 ( FMap U f o TMap η a') o h
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
524 ≈⟨⟩
775
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
525 right f o h
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
526 ∎
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
527
775
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
528 r-cong : {a : Obj A} { b : Obj B } → { f g : Hom A a ( FObj U b ) } → A [ f ≈ g ] → B [ left f ≈ left g ]
175
795be747d7a9 hom-set to universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 174
diff changeset
529 r-cong eq = let open ≈-Reasoning (B) in ( cdr ( fcong F eq ) )
775
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
530 l-cong : {a : Obj A} { b : Obj B } → { f g : Hom B (FObj F a) b } → B [ f ≈ g ] → A [ right f ≈ right g ]
175
795be747d7a9 hom-set to universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 174
diff changeset
531 l-cong eq = let open ≈-Reasoning (A) in ( car ( fcong U eq ) )
795be747d7a9 hom-set to universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 174
diff changeset
532
171
d25b0948e006 unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 159
diff changeset
533
d25b0948e006 unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 159
diff changeset
534 open UnityOfOppsite
d25b0948e006 unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 159
diff changeset
535
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 177
diff changeset
536 -- f : a ----------→ U(b)
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 177
diff changeset
537 -- 1_F(a) :F(a) --------→ F(a)
775
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
538 -- ε(b) = left uo (1_F(a)) :UF(b)--------→ a
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
539 -- η(a) = right uo (1_U(a)) : a ----------→ FU(a)
172
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 171
diff changeset
540
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 171
diff changeset
541
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
542 uo-η-map : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
543 ( U : Functor B A )
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
544 ( F : Functor A B ) →
174
1c4788483d46 add more axiom on unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 173
diff changeset
545 ( uo : UnityOfOppsite A B U F) → (a : Obj A ) → Hom A a (FObj U ( FObj F a ))
775
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
546 uo-η-map A B U F uo a = right uo ( id1 B (FObj F a) )
174
1c4788483d46 add more axiom on unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 173
diff changeset
547
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
548 uo-ε-map : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
549 ( U : Functor B A )
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
550 ( F : Functor A B ) →
174
1c4788483d46 add more axiom on unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 173
diff changeset
551 ( uo : UnityOfOppsite A B U F) → (b : Obj B ) → Hom B (FObj F ( FObj U ( b ) )) b
775
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
552 uo-ε-map A B U F uo b = left uo ( id1 A (FObj U b) )
172
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 171
diff changeset
553
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 171
diff changeset
554 uo-solution : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 171
diff changeset
555 ( U : Functor B A )
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
556 ( F : Functor A B ) →
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 177
diff changeset
557 ( uo : UnityOfOppsite A B U F) → {a : Obj A} {b : Obj B } →
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 177
diff changeset
558 ( f : Hom A a (FObj U b )) → Hom B (FObj F a) b
775
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
559 uo-solution A B U F uo {a} {b} f = -- B [ left uo (id1 A (FObj U b)) o FMap F f ]
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
560 left uo f
172
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 171
diff changeset
561
173
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 172
diff changeset
562 -- F(ε(b)) o η(F(b))
775
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
563 -- F( left uo (id1 A (FObj U b)) ) o right uo (id1 B (FObj F a)) ] == 1
172
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 171
diff changeset
564
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 171
diff changeset
565 UO2UM : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 171
diff changeset
566 ( U : Functor B A )
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
567 ( F : Functor A B ) →
690
3d41a8edbf63 fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 689
diff changeset
568 ( uo : UnityOfOppsite A B U F) → UniversalMapping A B U
172
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 171
diff changeset
569 UO2UM A B U F uo = record {
690
3d41a8edbf63 fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 689
diff changeset
570 F = FObj F ;
3d41a8edbf63 fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 689
diff changeset
571 η = uo-η-map A B U F uo ;
172
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 171
diff changeset
572 _* = uo-solution A B U F uo ;
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 171
diff changeset
573 isUniversalMapping = record {
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 171
diff changeset
574 universalMapping = universalMapping;
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 171
diff changeset
575 uniquness = uniqueness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 171
diff changeset
576 }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 171
diff changeset
577 } where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 171
diff changeset
578 universalMapping : {a' : Obj A} { b' : Obj B } → { f : Hom A a' (FObj U b') } →
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
579 A [ A [ FMap U ( uo-solution A B U F uo f) o ( uo-η-map A B U F uo ) a' ] ≈ f ]
172
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 171
diff changeset
580 universalMapping {a} {b} {f} = let open ≈-Reasoning (A) in
171
d25b0948e006 unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 159
diff changeset
581 begin
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
582 FMap U ( uo-solution A B U F uo f) o ( uo-η-map A B U F uo ) a
174
1c4788483d46 add more axiom on unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 173
diff changeset
583 ≈⟨⟩
775
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
584 FMap U ( left uo f) o right uo ( id1 B (FObj F a) )
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
585 ≈↑⟨ right-commute1 uo ⟩
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
586 right uo ( B [ left uo f o id1 B (FObj F a) ] )
175
795be747d7a9 hom-set to universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 174
diff changeset
587 ≈⟨ l-cong uo lemma-1 ⟩
775
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
588 right uo ( left uo f )
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
589 ≈⟨ left-injective uo ⟩
172
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 171
diff changeset
590 f
175
795be747d7a9 hom-set to universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 174
diff changeset
591 ∎ where
775
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
592 lemma-1 : B [ B [ left uo f o id1 B (FObj F a) ] ≈ left uo f ]
175
795be747d7a9 hom-set to universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 174
diff changeset
593 lemma-1 = let open ≈-Reasoning (B) in idR
172
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 171
diff changeset
594 uniqueness : {a' : Obj A} { b' : Obj B } → { f : Hom A a' (FObj U b') } → { g : Hom B (FObj F a') b'} →
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
595 A [ A [ FMap U g o ( uo-η-map A B U F uo ) a' ] ≈ f ] → B [ uo-solution A B U F uo f ≈ g ]
172
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 171
diff changeset
596 uniqueness {a} {b} {f} {g} eq = let open ≈-Reasoning (B) in
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 171
diff changeset
597 begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 171
diff changeset
598 uo-solution A B U F uo f
175
795be747d7a9 hom-set to universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 174
diff changeset
599 ≈⟨⟩
775
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
600 left uo f
175
795be747d7a9 hom-set to universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 174
diff changeset
601 ≈↑⟨ r-cong uo eq ⟩
775
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
602 left uo ( A [ FMap U g o right uo ( id1 B (FObj F a) ) ] )
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
603 ≈↑⟨ r-cong uo ( right-commute1 uo ) ⟩
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
604 left uo ( right uo ( g o ( id1 B (FObj F a) ) ) )
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
605 ≈⟨ right-injective uo ⟩
175
795be747d7a9 hom-set to universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 174
diff changeset
606 g o ( id1 B (FObj F a) )
795be747d7a9 hom-set to universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 174
diff changeset
607 ≈⟨ idR ⟩
172
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 171
diff changeset
608 g
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
609 ∎
171
d25b0948e006 unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 159
diff changeset
610
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
611 uo-η : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
612 ( U : Functor B A )
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
613 ( F : Functor A B ) →
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
614 ( uo : UnityOfOppsite A B U F) → NTrans A A identityFunctor ( U ○ F )
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
615 uo-η A B U F uo = record {
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
616 TMap = uo-η-map A B U F uo ; isNTrans = myIsNTrans
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
617 } where
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
618 η = uo-η-map A B U F uo
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
619 commute : {a b : Obj A} {f : Hom A a b}
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
620 → A [ A [ (FMap U (FMap F f)) o ( η a ) ] ≈ A [ (η b ) o f ] ]
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
621 commute {a} {b} {f} = let open ≈-Reasoning (A) in
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
622 begin
775
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
623 (FMap U (FMap F f)) o (right uo ( id1 B (FObj F a) ) )
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
624 ≈↑⟨ right-commute1 uo ⟩
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
625 right uo ( B [ (FMap F f) o ( id1 B (FObj F a) ) ] )
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
626 ≈⟨ l-cong uo (IsCategory.identityR (Category.isCategory B)) ⟩
775
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
627 right uo ( FMap F f )
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
628 ≈↑⟨ l-cong uo (IsCategory.identityL (Category.isCategory B)) ⟩
775
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
629 right uo ( B [ ( id1 B (FObj F b )) o FMap F f ] )
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
630 ≈⟨ right-commute2 uo ⟩
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
631 (right uo ( id1 B (FObj F b) ) ) o f
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
632 ≈⟨⟩
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
633 (η b ) o f
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
634 ∎ where
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
635 lemma-1 : B [ B [ (FMap F f) o ( id1 B (FObj F a) ) ] ≈ FMap F f ]
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
636 lemma-1 = IsCategory.identityR (Category.isCategory B)
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
637 myIsNTrans : IsNTrans A A identityFunctor ( U ○ F ) η
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
638 myIsNTrans = record { commute = commute }
171
d25b0948e006 unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 159
diff changeset
639
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
640 uo-ε : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
641 ( U : Functor B A )
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
642 ( F : Functor A B )→
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
643 ( uo : UnityOfOppsite A B U F) → NTrans B B ( F ○ U ) identityFunctor
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
644 uo-ε A B U F uo = record {
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
645 TMap = ε ; isNTrans = myIsNTrans
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
646 } where
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
647 ε = uo-ε-map A B U F uo
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
648 commute : {a b : Obj B} {f : Hom B a b }
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
649 → B [ B [ f o (ε a) ] ≈ B [(ε b) o (FMap F (FMap U f)) ] ]
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
650 commute {a} {b} {f} = let open ≈-Reasoning (B) in
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
651 sym ( begin
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
652 ε b o (FMap F (FMap U f))
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
653 ≈⟨⟩
775
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
654 left uo ( id1 A (FObj U b) ) o (FMap F (FMap U f))
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
655 ≈⟨ left-commute2 uo ⟩
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
656 left uo ( A [ id1 A (FObj U b) o FMap U f ] )
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
657 ≈⟨ r-cong uo (IsCategory.identityL (Category.isCategory A)) ⟩
775
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
658 left uo ( FMap U f )
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
659 ≈↑⟨ r-cong uo (IsCategory.identityR (Category.isCategory A)) ⟩
775
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
660 left uo ( A [ FMap U f o id1 A (FObj U a) ] )
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
661 ≈↑⟨ left-commute1 uo ⟩
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
662 f o left uo ( id1 A (FObj U a) )
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
663 ≈⟨⟩
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
664 f o (ε a)
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
665 ∎ )
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
666 myIsNTrans : IsNTrans B B ( F ○ U ) identityFunctor　ε
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
667 myIsNTrans = record { commute = commute }
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
668
172
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 171
diff changeset
669
171
d25b0948e006 unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 159
diff changeset
670 UO2Adj : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
d25b0948e006 unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 159
diff changeset
671 { U : Functor B A }
d25b0948e006 unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 159
diff changeset
672 { F : Functor A B }
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
673 ( uo : UnityOfOppsite A B U F)
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
674 → Adjunction A B
171
d25b0948e006 unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 159
diff changeset
675 UO2Adj A B {U} {F} uo = record {
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
676 U = U ;
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
677 F = F ;
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
678 η = uo-η A B U F uo ;
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
679 ε = uo-ε A B U F uo ;
171
d25b0948e006 unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 159
diff changeset
680 isAdjunction = record {
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
681 adjoint1 = adjoint1 ;
171
d25b0948e006 unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 159
diff changeset
682 adjoint2 = adjoint2
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
683 }
171
d25b0948e006 unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 159
diff changeset
684 } where
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
685 um = UO2UM A B U F uo
171
d25b0948e006 unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 159
diff changeset
686 adjoint1 : { b : Obj B } →
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
687 A [ A [ ( FMap U ( TMap (uo-ε A B U F uo) b )) o ( TMap (uo-η A B U F uo) ( FObj U b )) ] ≈ id1 A (FObj U b) ]
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
688 adjoint1 {b} = let open ≈-Reasoning (A) in
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
689 begin
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
690 ( FMap U ( TMap (uo-ε A B U F uo) b )) o ( TMap (uo-η A B U F uo) ( FObj U b ))
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
691 ≈⟨⟩
775
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
692 FMap U (left uo (id1 A (FObj U b))) o (right uo (id1 B (FObj F (FObj U b))))
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
693 ≈↑⟨ right-commute1 uo ⟩
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
694 right uo ( B [ left uo (id1 A (FObj U b)) o id1 B (FObj F (FObj U b)) ] )
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
695 ≈⟨ l-cong uo ((IsCategory.identityR (Category.isCategory B))) ⟩
775
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
696 right uo ( left uo (id1 A (FObj U b)) )
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
697 ≈⟨ left-injective uo ⟩
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
698 id1 A (FObj U b)
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
699 ∎
171
d25b0948e006 unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 159
diff changeset
700 adjoint2 : {a : Obj A} →
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
701 B [ B [ ( TMap (uo-ε A B U F uo) ( FObj F a )) o ( FMap F ( TMap (uo-η A B U F uo) a )) ] ≈ id1 B (FObj F a) ]
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
702 adjoint2 {a} = let open ≈-Reasoning (B) in
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
703 begin
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
704 ( TMap (uo-ε A B U F uo) ( FObj F a )) o ( FMap F ( TMap (uo-η A B U F uo) a ))
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
705 ≈⟨⟩
775
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
706 left uo (Category.Category.Id A) o FMap F (right uo (id1 B (FObj F a)))
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
707 ≈⟨ left-commute2 uo ⟩
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
708 left uo ( A [ (Category.Category.Id A) o (right uo (id1 B (FObj F a))) ] )
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
709 ≈⟨ r-cong uo ((IsCategory.identityL (Category.isCategory A))) ⟩
775
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
710 left uo ( right uo (id1 B (FObj F a)))
06a7831cf6ce exchange left and right
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
711 ≈⟨ right-injective uo ⟩
176
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
712 id1 B (FObj F a)
ae1a4f7e5203 hom set adjunction done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 175
diff changeset
713 ∎
171
d25b0948e006 unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 159
diff changeset
714
d25b0948e006 unity of oppsite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 159
diff changeset
715
55
1716403c92c2 Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 54
diff changeset
716 -- done!
1716403c92c2 Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 54
diff changeset
717