annotate universal-mapping.agda @ 45:659b8a21caf7

uniq-univeralMapping from Adjunction
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 23 Jul 2013 01:45:56 +0900
parents a626fdd909c3
children 5d1b0fd2ad21
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
17b8bafebad7 add universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import Category -- https://github.com/konn/category-agda
17b8bafebad7 add universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 open import Level
17b8bafebad7 add universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open import Category.HomReasoning
17b8bafebad7 add universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6
17b8bafebad7 add universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 open Functor
37
2f5f5b4d62fa universalMapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 36
diff changeset
8
31
17b8bafebad7 add universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 record IsUniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
17b8bafebad7 add universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 ( U : Functor B A )
17b8bafebad7 add universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 ( F : Obj A -> Obj B )
17b8bafebad7 add universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 ( η : (a : Obj A) -> Hom A a ( FObj U (F a) ) )
17b8bafebad7 add universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 ( _* : { a : Obj A}{ b : Obj B} -> ( Hom A a (FObj U b) ) -> Hom B (F a ) b )
17b8bafebad7 add universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
17b8bafebad7 add universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 field
36
ad997bd9788b isUniversalMapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 35
diff changeset
16 universalMapping : (a' : Obj A) ( b' : Obj B ) -> { f : Hom A a' (FObj U b') } ->
37
2f5f5b4d62fa universalMapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 36
diff changeset
17 A [ A [ FMap U ( f * ) o η a' ] ≈ f ]
42
9694f93977ca Functor Identity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
18 unique-universalMapping : (a' : Obj A) ( b' : Obj B ) -> ( f : Hom A a' (FObj U b') ) -> ( g : Hom B (F a') b') ->
9694f93977ca Functor Identity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
19 A [ A [ FMap U g o η a' ] ≈ f ] -> B [ f * ≈ g ]
31
17b8bafebad7 add universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20
17b8bafebad7 add universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 record UniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
17b8bafebad7 add universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 ( U : Functor B A )
17b8bafebad7 add universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 ( F : Obj A -> Obj B )
17b8bafebad7 add universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 ( η : (a : Obj A) -> Hom A a ( FObj U (F a) ) )
17b8bafebad7 add universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
37
2f5f5b4d62fa universalMapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 36
diff changeset
26 infixr 11 _*
31
17b8bafebad7 add universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 field
37
2f5f5b4d62fa universalMapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 36
diff changeset
28 _* : { a : Obj A}{ b : Obj B} -> ( Hom A a (FObj U b) ) -> Hom B (F a ) b
31
17b8bafebad7 add universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 isUniversalMapping : IsUniversalMapping A B U F η _*
17b8bafebad7 add universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30
32
7862ad3b000f Adjoint
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 31
diff changeset
31 open NTrans
7862ad3b000f Adjoint
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 31
diff changeset
32 open import Category.Cat
7862ad3b000f Adjoint
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 31
diff changeset
33 record IsAdjunction {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
7862ad3b000f Adjoint
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 31
diff changeset
34 ( U : Functor B A )
7862ad3b000f Adjoint
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 31
diff changeset
35 ( F : Functor A B )
7862ad3b000f Adjoint
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 31
diff changeset
36 ( η : NTrans A A identityFunctor ( U ○ F ) )
7862ad3b000f Adjoint
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 31
diff changeset
37 ( ε : NTrans B B ( F ○ U ) identityFunctor )
7862ad3b000f Adjoint
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 31
diff changeset
38 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
7862ad3b000f Adjoint
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 31
diff changeset
39 field
40
c34b1cfe9fdc Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 39
diff changeset
40 adjoint1 : { b' : Obj B } ->
32
7862ad3b000f Adjoint
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 31
diff changeset
41 A [ A [ ( FMap U ( TMap ε b' )) o ( TMap η ( FObj U b' )) ] ≈ Id {_} {_} {_} {A} (FObj U b') ]
40
c34b1cfe9fdc Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 39
diff changeset
42 adjoint2 : {a' : Obj A} ->
32
7862ad3b000f Adjoint
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 31
diff changeset
43 B [ B [ ( TMap ε ( FObj F a' )) o ( FMap F ( TMap η a' )) ] ≈ Id {_} {_} {_} {B} (FObj F a') ]
31
17b8bafebad7 add universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44
32
7862ad3b000f Adjoint
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 31
diff changeset
45 record Adjunction {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
7862ad3b000f Adjoint
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 31
diff changeset
46 ( U : Functor B A )
7862ad3b000f Adjoint
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 31
diff changeset
47 ( F : Functor A B )
7862ad3b000f Adjoint
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 31
diff changeset
48 ( η : NTrans A A identityFunctor ( U ○ F ) )
7862ad3b000f Adjoint
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 31
diff changeset
49 ( ε : NTrans B B ( F ○ U ) identityFunctor )
7862ad3b000f Adjoint
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 31
diff changeset
50 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
7862ad3b000f Adjoint
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 31
diff changeset
51 field
40
c34b1cfe9fdc Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 39
diff changeset
52 isAdjunction : IsAdjunction A B U F η ε
32
7862ad3b000f Adjoint
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 31
diff changeset
53
43
5506abc832c7 uniqness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
54 --
5506abc832c7 uniqness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
55 -- Adjunction yields solution of universal mapping
5506abc832c7 uniqness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
56 --
5506abc832c7 uniqness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
57 --
5506abc832c7 uniqness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
58
34
306aa1873b2f trying...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 33
diff changeset
59 open Adjunction
306aa1873b2f trying...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 33
diff changeset
60 open UniversalMapping
35
4ac419251f86 f∗ = ε(b)F(f),
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
61
33
fefebc387eae add Adj to Universal Mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
62 Lemma1 : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
35
4ac419251f86 f∗ = ε(b)F(f),
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
63 ( U : Functor B A )
4ac419251f86 f∗ = ε(b)F(f),
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
64 ( F : Functor A B )
4ac419251f86 f∗ = ε(b)F(f),
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
65 ( η : NTrans A A identityFunctor ( U ○ F ) )
4ac419251f86 f∗ = ε(b)F(f),
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
66 ( ε : NTrans B B ( F ○ U ) identityFunctor ) ->
37
2f5f5b4d62fa universalMapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 36
diff changeset
67 Adjunction A B U F η ε -> UniversalMapping A B U (FObj F) (TMap η)
35
4ac419251f86 f∗ = ε(b)F(f),
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
68 Lemma1 A B U F η ε adj = record {
43
5506abc832c7 uniqness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
69 _* = solution ;
36
ad997bd9788b isUniversalMapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 35
diff changeset
70 isUniversalMapping = record {
43
5506abc832c7 uniqness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
71 universalMapping = universalMapping;
5506abc832c7 uniqness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
72 unique-universalMapping = uniqness
36
ad997bd9788b isUniversalMapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 35
diff changeset
73 }
ad997bd9788b isUniversalMapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 35
diff changeset
74 } where
43
5506abc832c7 uniqness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
75 solution : { a : Obj A} { b : Obj B} -> ( f : Hom A a (FObj U b) ) -> Hom B (FObj F a ) b
5506abc832c7 uniqness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
76 solution {_} {b} f = B [ TMap ε b o FMap F f ]
37
2f5f5b4d62fa universalMapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 36
diff changeset
77 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
78 A [ A [ FMap U ( solution f) o TMap η a' ] ≈ f ]
38
999e637d14c7 reasoning
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
79 universalMapping a b {f} =
999e637d14c7 reasoning
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
80 let open ≈-Reasoning (A) in
999e637d14c7 reasoning
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
81 begin
43
5506abc832c7 uniqness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
82 FMap U ( solution f) o TMap η a
39
77c3a5292a2f Reasoning
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
83 ≈⟨⟩
77c3a5292a2f Reasoning
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
84 FMap U ( B [ TMap ε b o FMap F f ] ) o TMap η a
77c3a5292a2f Reasoning
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
85 ≈⟨ car (IsFunctor.distr ( isFunctor U )) ⟩
77c3a5292a2f Reasoning
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
86 ( (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
87 ≈⟨ sym assoc ⟩
c34b1cfe9fdc Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 39
diff changeset
88 (FMap U (TMap ε b)) o ((FMap U ( FMap F f )) o TMap η a )
c34b1cfe9fdc Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 39
diff changeset
89 ≈⟨ cdr (nat A η) ⟩
c34b1cfe9fdc Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 39
diff changeset
90 (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
91 ≈⟨ assoc ⟩
c34b1cfe9fdc Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 39
diff changeset
92 ((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
93 ≈⟨ car ( IsAdjunction.adjoint1 ( isAdjunction adj)) ⟩
c34b1cfe9fdc Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 39
diff changeset
94 id (FObj U b) o f
c34b1cfe9fdc Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 39
diff changeset
95 ≈⟨ idL ⟩
38
999e637d14c7 reasoning
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
96 f
999e637d14c7 reasoning
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
97
44
a626fdd909c3 f replacement
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 43
diff changeset
98 lemma1 : (a : Obj A) ( b : Obj B ) ( f : Hom A a (FObj U b) ) -> ( g : Hom B (FObj F a) b) ->
a626fdd909c3 f replacement
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 43
diff changeset
99 A [ A [ FMap U g o TMap η a ] ≈ f ] ->
a626fdd909c3 f replacement
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 43
diff changeset
100 B [ (FMap F (A [ FMap U g o TMap η a ] )) ≈ FMap F f ]
a626fdd909c3 f replacement
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 43
diff changeset
101 lemma1 a b f g k = IsFunctor.≈-cong (isFunctor F) k
43
5506abc832c7 uniqness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
102 uniqness : (a' : Obj A) ( b' : Obj B ) -> ( f : Hom A a' (FObj U b') ) -> ( g : Hom B (FObj F a') b') ->
5506abc832c7 uniqness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
103 A [ A [ FMap U g o TMap η a' ] ≈ f ] -> B [ solution f ≈ g ]
44
a626fdd909c3 f replacement
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 43
diff changeset
104 uniqness a b f g k = let open ≈-Reasoning (B) in
a626fdd909c3 f replacement
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 43
diff changeset
105 begin
a626fdd909c3 f replacement
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 43
diff changeset
106 solution f
a626fdd909c3 f replacement
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 43
diff changeset
107 ≈⟨⟩
a626fdd909c3 f replacement
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 43
diff changeset
108 TMap ε b o FMap F f
45
659b8a21caf7 uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
109 ≈⟨ cdr (sym ( lemma1 a b f g k )) ⟩
44
a626fdd909c3 f replacement
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 43
diff changeset
110 TMap ε b o FMap F ( A [ FMap U g o TMap η a ] )
45
659b8a21caf7 uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
111 ≈⟨ cdr (IsFunctor.distr ( isFunctor F )) ⟩
659b8a21caf7 uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
112 TMap ε b o ( FMap F ( FMap U g) o FMap F ( TMap η a ) )
659b8a21caf7 uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
113 ≈⟨ assoc ⟩
659b8a21caf7 uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
114 ( TMap ε b o FMap F ( FMap U g) ) o FMap F ( TMap η a )
659b8a21caf7 uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
115 ≈⟨ sym ( car ( nat B ε )) ⟩
659b8a21caf7 uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
116 ( g o TMap ε ( FObj F a) ) o FMap F ( TMap η a )
659b8a21caf7 uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
117 ≈⟨ sym assoc ⟩
659b8a21caf7 uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
118 g o ( TMap ε ( FObj F a) o FMap F ( TMap η a ) )
659b8a21caf7 uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
119 ≈⟨ cdr ( IsAdjunction.adjoint2 ( isAdjunction adj )) ⟩
659b8a21caf7 uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
120 g o id (FObj F a)
659b8a21caf7 uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
121 ≈⟨ idR ⟩
44
a626fdd909c3 f replacement
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 43
diff changeset
122 g
a626fdd909c3 f replacement
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 43
diff changeset
123
a626fdd909c3 f replacement
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 43
diff changeset
124
43
5506abc832c7 uniqness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
125 --
5506abc832c7 uniqness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
126 --
5506abc832c7 uniqness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
127 -- Universal mapping yields Adjunction
5506abc832c7 uniqness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
128 --
5506abc832c7 uniqness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
129 --
5506abc832c7 uniqness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
130
5506abc832c7 uniqness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
131
5506abc832c7 uniqness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
132 --
5506abc832c7 uniqness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
133 -- F is an functor
5506abc832c7 uniqness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
134 --
5506abc832c7 uniqness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
135
41
e9fa5c95eff7 isFunctor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
136 FunctorF : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
e9fa5c95eff7 isFunctor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
137 ( U : Functor B A )
e9fa5c95eff7 isFunctor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
138 ( F : Obj A -> Obj B )
e9fa5c95eff7 isFunctor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
139 ( η : (a : Obj A) -> Hom A a ( FObj U (F a) ) ) ->
e9fa5c95eff7 isFunctor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
140 UniversalMapping A B U F η -> Functor A B
e9fa5c95eff7 isFunctor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
141 FunctorF A B U F η um = record {
e9fa5c95eff7 isFunctor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
142 FObj = F;
42
9694f93977ca Functor Identity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
143 FMap = myFMap ;
9694f93977ca Functor Identity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
144 isFunctor = myIsFunctor
41
e9fa5c95eff7 isFunctor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
145 } where
42
9694f93977ca Functor Identity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
146 myFMap : {a b : Obj A} -> Hom A a b -> Hom B (F a) (F b)
9694f93977ca Functor Identity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
147 myFMap f = (_* um) (A [ η (Category.cod A f ) o f ])
9694f93977ca Functor Identity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
148 lemma-id-1 : {a : Obj A} -> A [ A [ FMap U (Id {_} {_} {_} {B} (F a)) o η a ] ≈ (A [ (η a) o (Id {_} {_} {_} {A} a) ]) ]
9694f93977ca Functor Identity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
149 lemma-id-1 {a} = let open ≈-Reasoning (A) in
9694f93977ca Functor Identity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
150 begin
9694f93977ca Functor Identity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
151 A [ FMap U (Id {_} {_} {_} {B} (F a)) o η a ]
9694f93977ca Functor Identity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
152 ≈⟨ ( car ( IsFunctor.identity ( isFunctor U ))) ⟩
9694f93977ca Functor Identity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
153 A [ (Id {_} {_} {_} {A} (FObj U ( F a )) ) o η a ]
9694f93977ca Functor Identity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
154 ≈⟨ idL ⟩
9694f93977ca Functor Identity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
155 η a
9694f93977ca Functor Identity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
156 ≈⟨ sym idR ⟩
9694f93977ca Functor Identity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
157 (A [ (η a) o (Id {_} {_} {_} {A} a) ])
9694f93977ca Functor Identity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
158
9694f93977ca Functor Identity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
159 lemma-id : {a : Obj A} → B [ ( (_* um) (A [ (η a) o (Id {_} {_} {_} {A} a)] )) ≈ (Id {_} {_} {_} {B} (F a)) ]
9694f93977ca Functor Identity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
160 lemma-id {a} = ( IsUniversalMapping.unique-universalMapping ( isUniversalMapping um ) )
9694f93977ca Functor Identity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
161 a (F a) ((A [ (η a) o (Id {_} {_} {_} {A} a)] )) ((Id {_} {_} {_} {B} (F a))) lemma-id-1
9694f93977ca Functor Identity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
162 myIsFunctor : IsFunctor A B F myFMap
9694f93977ca Functor Identity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
163 myIsFunctor =
9694f93977ca Functor Identity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
164 record { ≈-cong = {!!}
9694f93977ca Functor Identity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
165 ; identity = lemma-id
9694f93977ca Functor Identity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
166 ; distr = {!!}
9694f93977ca Functor Identity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
167 }
41
e9fa5c95eff7 isFunctor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
168