Mercurial > hg > Members > kono > Proof > category

annotate universal-mapping.agda @ 689:fb9fc9652c04

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