Mercurial > hg > Members > kono > Proof > category

annotate universal-mapping.agda @ 177:63f6157a6a19

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