Mercurial > hg > Members > kono > Proof > category
annotate cat-utility.agda @ 495:633df882db86
fryed1 done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 14 Mar 2017 13:08:03 +0900 |
| parents | c7b8017bcd4d |
| children | 3ce21b2a671a |
| rev | line source |
|---|---|
| 56 | 1 module cat-utility where |
| 2 | |
| 3 -- Shinji KONO <kono@ie.u-ryukyu.ac.jp> | |
| 4 | |
| 87 | 5 open import Category -- https://github.com/konn/category-agda |
| 6 open import Level | |
| 7 --open import Category.HomReasoning | |
| 8 open import HomReasoning | |
| 56 | 9 |
| 87 | 10 open Functor |
| 56 | 11 |
| 87 | 12 id1 : ∀{c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (a : Obj A ) → Hom A a a |
| 13 id1 A a = (Id {_} {_} {_} {A} a) | |
| 253 | 14 -- We cannot make A implicit |
| 56 | 15 |
|
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
16 record IsUniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') |
| 87 | 17 ( U : Functor B A ) |
| 18 ( F : Obj A → Obj B ) | |
| 19 ( η : (a : Obj A) → Hom A a ( FObj U (F a) ) ) | |
| 20 ( _* : { a : Obj A}{ b : Obj B} → ( Hom A a (FObj U b) ) → Hom B (F a ) b ) | |
| 21 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where | |
| 22 field | |
|
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
23 universalMapping : {a : Obj A} { b : Obj B } → { f : Hom A a (FObj U b) } → |
| 101 | 24 A [ A [ FMap U ( f * ) o η a ] ≈ f ] |
|
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
25 uniquness : {a : Obj A} { b : Obj B } → { f : Hom A a (FObj U b) } → { g : Hom B (F a) b } → |
| 101 | 26 A [ A [ FMap U g o η a ] ≈ f ] → B [ f * ≈ g ] |
| 56 | 27 |
|
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
28 record UniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') |
| 87 | 29 ( U : Functor B A ) |
| 30 ( F : Obj A → Obj B ) | |
| 31 ( η : (a : Obj A) → Hom A a ( FObj U (F a) ) ) | |
| 32 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where | |
| 33 infixr 11 _* | |
| 34 field | |
|
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
35 _* : { a : Obj A}{ b : Obj B} → ( Hom A a (FObj U b) ) → Hom B (F a ) b |
| 87 | 36 isUniversalMapping : IsUniversalMapping A B U F η _* |
| 56 | 37 |
|
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
38 record coIsUniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') |
| 268 | 39 ( F : Functor A B ) |
| 40 ( U : Obj B → Obj A ) | |
| 41 ( ε : (b : Obj B) → Hom B ( FObj F (U b) ) b ) | |
| 42 ( _*' : { b : Obj B}{ a : Obj A} → ( Hom B (FObj F a) b ) → Hom A a (U b ) ) | |
| 43 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where | |
| 44 field | |
|
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
45 couniversalMapping : {b : Obj B} { a : Obj A } → { f : Hom B (FObj F a) b } → |
| 268 | 46 B [ B [ ε b o FMap F ( f *' ) ] ≈ f ] |
|
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
47 couniquness : {b : Obj B} { a : Obj A } → { f : Hom B (FObj F a) b } → { g : Hom A a (U b) } → |
| 268 | 48 B [ B [ ε b o FMap F g ] ≈ f ] → A [ f *' ≈ g ] |
| 49 | |
|
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
50 record coUniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') |
| 268 | 51 ( F : Functor A B ) |
| 52 ( U : Obj B → Obj A ) | |
| 53 ( ε : (b : Obj B) → Hom B ( FObj F (U b) ) b ) | |
| 54 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where | |
| 55 infixr 11 _*' | |
| 56 field | |
|
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
57 _*' : { b : Obj B}{ a : Obj A} → ( Hom B (FObj F a) b ) → Hom A a (U b ) |
| 268 | 58 iscoUniversalMapping : coIsUniversalMapping A B F U ε _*' |
| 59 | |
| 87 | 60 open NTrans |
| 61 open import Category.Cat | |
|
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
62 record IsAdjunction {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') |
| 87 | 63 ( U : Functor B A ) |
| 64 ( F : Functor A B ) | |
| 65 ( η : NTrans A A identityFunctor ( U ○ F ) ) | |
| 66 ( ε : NTrans B B ( F ○ U ) identityFunctor ) | |
| 67 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where | |
| 68 field | |
| 69 adjoint1 : { b : Obj B } → | |
| 70 A [ A [ ( FMap U ( TMap ε b )) o ( TMap η ( FObj U b )) ] ≈ id1 A (FObj U b) ] | |
| 71 adjoint2 : {a : Obj A} → | |
| 72 B [ B [ ( TMap ε ( FObj F a )) o ( FMap F ( TMap η a )) ] ≈ id1 B (FObj F a) ] | |
| 56 | 73 |
|
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
74 record Adjunction {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') |
| 87 | 75 ( U : Functor B A ) |
| 76 ( F : Functor A B ) | |
| 77 ( η : NTrans A A identityFunctor ( U ○ F ) ) | |
| 78 ( ε : NTrans B B ( F ○ U ) identityFunctor ) | |
| 79 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where | |
| 80 field | |
| 81 isAdjunction : IsAdjunction A B U F η ε | |
|
202
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
176
diff
changeset
|
82 U-functor = U |
|
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
176
diff
changeset
|
83 F-functor = F |
|
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
176
diff
changeset
|
84 Eta = η |
|
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
176
diff
changeset
|
85 Epsiron = ε |
| 56 | 86 |
| 87 | |
|
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
88 record IsMonad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) |
| 87 | 89 ( T : Functor A A ) |
| 90 ( η : NTrans A A identityFunctor T ) | |
| 91 ( μ : NTrans A A (T ○ T) T) | |
| 92 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where | |
| 93 field | |
| 94 assoc : {a : Obj A} → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈ A [ TMap μ a o FMap T (TMap μ a) ] ] | |
| 95 unity1 : {a : Obj A} → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] | |
| 96 unity2 : {a : Obj A} → A [ A [ TMap μ a o (FMap T (TMap η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ] | |
| 56 | 97 |
| 87 | 98 record Monad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (T : Functor A A) (η : NTrans A A identityFunctor T) (μ : NTrans A A (T ○ T) T) |
| 99 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where | |
| 100 field | |
| 101 isMonad : IsMonad A T η μ | |
| 130 | 102 -- g ○ f = μ(c) T(g) f |
| 103 join : { a b : Obj A } → { c : Obj A } → | |
| 104 ( Hom A b ( FObj T c )) → ( Hom A a ( FObj T b)) → Hom A a ( FObj T c ) | |
| 105 join {_} {_} {c} g f = A [ TMap μ c o A [ FMap T g o f ] ] | |
| 106 | |
| 56 | 107 |
| 87 | 108 Functor*Nat : {c₁ c₂ ℓ c₁' c₂' ℓ' c₁'' c₂'' ℓ'' : Level} (A : Category c₁ c₂ ℓ) {B : Category c₁' c₂' ℓ'} (C : Category c₁'' c₂'' ℓ'') |
| 300 | 109 (F : Functor B C) → { G H : Functor A B } → ( n : NTrans A B G H ) → NTrans A C (F ○ G) (F ○ H) |
| 87 | 110 Functor*Nat A {B} C F {G} {H} n = record { |
| 300 | 111 TMap = λ a → FMap F (TMap n a) |
| 87 | 112 ; isNTrans = record { |
| 130 | 113 commute = commute |
| 87 | 114 } |
| 115 } where | |
|
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
116 commute : {a b : Obj A} {f : Hom A a b} |
| 87 | 117 → C [ C [ (FMap F ( FMap H f )) o ( FMap F (TMap n a)) ] ≈ C [ (FMap F (TMap n b )) o (FMap F (FMap G f)) ] ] |
| 130 | 118 commute {a} {b} {f} = let open ≈-Reasoning (C) in |
|
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
119 begin |
| 87 | 120 (FMap F ( FMap H f )) o ( FMap F (TMap n a)) |
| 121 ≈⟨ sym (distr F) ⟩ | |
| 122 FMap F ( B [ (FMap H f) o TMap n a ]) | |
| 123 ≈⟨ IsFunctor.≈-cong (isFunctor F) ( nat n ) ⟩ | |
| 124 FMap F ( B [ (TMap n b ) o FMap G f ] ) | |
| 125 ≈⟨ distr F ⟩ | |
| 126 (FMap F (TMap n b )) o (FMap F (FMap G f)) | |
| 127 ∎ | |
| 56 | 128 |
| 87 | 129 Nat*Functor : {c₁ c₂ ℓ c₁' c₂' ℓ' c₁'' c₂'' ℓ'' : Level} (A : Category c₁ c₂ ℓ) {B : Category c₁' c₂' ℓ'} (C : Category c₁'' c₂'' ℓ'') |
| 300 | 130 { G H : Functor B C } → ( n : NTrans B C G H ) → (F : Functor A B) → NTrans A C (G ○ F) (H ○ F) |
| 87 | 131 Nat*Functor A {B} C {G} {H} n F = record { |
| 300 | 132 TMap = λ a → TMap n (FObj F a) |
| 87 | 133 ; isNTrans = record { |
| 130 | 134 commute = commute |
| 87 | 135 } |
| 136 } where | |
|
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
137 commute : {a b : Obj A} {f : Hom A a b} |
| 87 | 138 → C [ C [ ( FMap H (FMap F f )) o ( TMap n (FObj F a)) ] ≈ C [ (TMap n (FObj F b )) o (FMap G (FMap F f)) ] ] |
|
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
139 commute {a} {b} {f} = IsNTrans.commute ( isNTrans n) |
| 56 | 140 |
| 87 | 141 -- T ≃ (U_R ○ F_R) |
| 142 -- μ = U_R ε F_R | |
| 143 -- nat-ε | |
| 144 -- nat-η -- same as η but has different types | |
| 84 | 145 |
|
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
146 record MResolution {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) ( B : Category c₁' c₂' ℓ' ) |
|
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
147 ( T : Functor A A ) |
|
94
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
91
diff
changeset
|
148 -- { η : NTrans A A identityFunctor T } |
|
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
91
diff
changeset
|
149 -- { μ : NTrans A A (T ○ T) T } |
|
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
91
diff
changeset
|
150 -- { M : Monad A T η μ } |
| 87 | 151 ( UR : Functor B A ) ( FR : Functor A B ) |
|
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
152 { ηR : NTrans A A identityFunctor ( UR ○ FR ) } |
|
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
153 { εR : NTrans B B ( FR ○ UR ) identityFunctor } |
| 87 | 154 { μR : NTrans A A ( (UR ○ FR) ○ ( UR ○ FR )) ( UR ○ FR ) } |
| 155 ( Adj : Adjunction A B UR FR ηR εR ) | |
| 156 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where | |
| 157 field | |
|
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
158 T=UF : T ≃ (UR ○ FR) |
| 300 | 159 μ=UεF : {x : Obj A } → A [ TMap μR x ≈ FMap UR ( TMap εR ( FObj FR x ) ) ] |
| 160 -- ηR=η : {x : Obj A } → A [ TMap ηR x ≈ TMap η x ] -- We need T → UR FR conversion | |
| 161 -- μR=μ : {x : Obj A } → A [ TMap μR x ≈ TMap μ x ] | |
| 86 | 162 |
| 88 | 163 |
|
350
c483374f542b
try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
312
diff
changeset
|
164 -- |
|
c483374f542b
try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
312
diff
changeset
|
165 -- e f |
|
c483374f542b
try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
312
diff
changeset
|
166 -- c -------→ a ---------→ b |
|
c483374f542b
try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
312
diff
changeset
|
167 -- ^ . ---------→ |
|
c483374f542b
try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
312
diff
changeset
|
168 -- | . g |
|
c483374f542b
try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
312
diff
changeset
|
169 -- |k . |
|
c483374f542b
try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
312
diff
changeset
|
170 -- | . h |
|
c483374f542b
try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
312
diff
changeset
|
171 -- d |
|
c483374f542b
try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
312
diff
changeset
|
172 |
| 443 | 173 record IsEqualizer { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {c a b : Obj A} (e : Hom A c a) (f g : Hom A a b) : Set (ℓ ⊔ (c₁ ⊔ c₂)) where |
| 260 | 174 field |
| 175 fe=ge : A [ A [ f o e ] ≈ A [ g o e ] ] | |
| 176 k : {d : Obj A} (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c | |
| 177 ek=h : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → A [ A [ e o k {d} h eq ] ≈ h ] | |
| 178 uniqueness : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → {k' : Hom A d c } → | |
| 179 A [ A [ e o k' ] ≈ h ] → A [ k {d} h eq ≈ k' ] | |
| 443 | 180 equalizer1 : Hom A c a |
| 181 equalizer1 = e | |
| 260 | 182 |
| 443 | 183 record Equalizer { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b : Obj A} (f g : Hom A a b) : Set (ℓ ⊔ (c₁ ⊔ c₂)) where |
| 440 | 184 field |
| 443 | 185 equalizer-c : Obj A |
| 186 equalizer : Hom A equalizer-c a | |
|
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
187 isEqualizer : IsEqualizer A equalizer f g |
| 440 | 188 |
|
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
189 -- |
| 260 | 190 -- Product |
| 191 -- | |
| 264 | 192 -- c |
| 193 -- f | g | |
| 194 -- |f×g | |
| 195 -- v | |
| 300 | 196 -- a <-------- ab ---------→ b |
| 264 | 197 -- π1 π2 |
| 260 | 198 |
| 199 | |
|
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
200 record Product { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a b ab : Obj A) |
| 260 | 201 ( π1 : Hom A ab a ) |
| 202 ( π2 : Hom A ab b ) | |
| 203 : Set (ℓ ⊔ (c₁ ⊔ c₂)) where | |
| 204 field | |
| 205 _×_ : {c : Obj A} ( f : Hom A c a ) → ( g : Hom A c b ) → Hom A c ab | |
| 206 π1fxg=f : {c : Obj A} { f : Hom A c a } → { g : Hom A c b } → A [ A [ π1 o ( f × g ) ] ≈ f ] | |
| 207 π2fxg=g : {c : Obj A} { f : Hom A c a } → { g : Hom A c b } → A [ A [ π2 o ( f × g ) ] ≈ g ] | |
| 208 uniqueness : {c : Obj A} { h : Hom A c ab } → A [ ( A [ π1 o h ] ) × ( A [ π2 o h ] ) ≈ h ] | |
|
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
209 ×-cong : {c : Obj A} { f f' : Hom A c a } → { g g' : Hom A c b } → A [ f ≈ f' ] → A [ g ≈ g' ] → A [ f × g ≈ f' × g' ] |
| 440 | 210 |
|
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
211 record CreateProduct { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) |
| 440 | 212 : Set (ℓ ⊔ (c₁ ⊔ c₂)) where |
| 213 field | |
| 214 product : (a b : Obj A) -> Obj A | |
|
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
215 π1 : (a b : Obj A) -> Hom A (product a b ) a |
|
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
216 π2 : (a b : Obj A) -> Hom A (product a b ) b |
| 440 | 217 isProduct : (a b : Obj A) -> Product A a b (product a b) (π1 a b ) (π2 a b) |
| 260 | 218 |
|
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
219 ----- |
|
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
220 -- |
|
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
221 -- product on arbitrary index |
|
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
222 -- |
|
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
223 |
|
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
224 record IProduct { c c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Set c) |
|
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
225 ( p : Obj A ) -- product |
|
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
226 ( ai : I → Obj A ) -- families |
|
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
227 ( pi : (i : I ) → Hom A p ( ai i ) ) -- projections |
|
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
228 : Set (c ⊔ ℓ ⊔ (c₁ ⊔ c₂)) where |
|
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
229 field |
|
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
230 iproduct : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → Hom A q p |
|
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
231 pif=q : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → ∀ { i : I } → A [ A [ ( pi i ) o ( iproduct qi ) ] ≈ (qi i) ] |
|
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
232 ip-uniqueness : {q : Obj A} { h : Hom A q p } → A [ iproduct ( λ (i : I) → A [ (pi i) o h ] ) ≈ h ] |
|
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
233 ip-cong : {q : Obj A} → { qi : (i : I) → Hom A q (ai i) } → { qi' : (i : I) → Hom A q (ai i) } |
|
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
234 → ( ∀ (i : I ) → A [ qi i ≈ qi' i ] ) → A [ iproduct qi ≈ iproduct qi' ] |
|
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
235 -- another form of uniquness |
|
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
236 ip-uniqueness1 : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → ( product' : Hom A q p ) |
|
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
237 → ( ∀ { i : I } → A [ A [ ( pi i ) o product' ] ≈ (qi i) ] ) |
|
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
238 → A [ product' ≈ iproduct qi ] |
|
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
239 ip-uniqueness1 {a} qi product' eq = let open ≈-Reasoning (A) in begin |
|
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
240 product' |
|
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
241 ≈↑⟨ ip-uniqueness ⟩ |
|
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
242 iproduct (λ i₁ → A [ pi i₁ o product' ]) |
|
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
243 ≈⟨ ip-cong ( λ i → begin |
|
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
244 pi i o product' |
|
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
245 ≈⟨ eq {i} ⟩ |
|
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
246 qi i |
|
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
247 ∎ ) ⟩ |
|
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
248 iproduct qi |
|
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
249 ∎ |
|
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
250 |
|
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
251 |
| 260 | 252 -- Pullback |
| 253 -- f | |
| 300 | 254 -- a ------→ c |
|
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
255 -- ^ ^ |
| 260 | 256 -- π1 | |g |
| 257 -- | | | |
| 300 | 258 -- ab ------→ b |
| 260 | 259 -- ^ π2 |
| 260 -- | | |
|
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
261 -- d |
| 260 | 262 -- |
|
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
263 record Pullback { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a b c ab : Obj A) |
| 260 | 264 ( f : Hom A a c ) ( g : Hom A b c ) |
| 265 ( π1 : Hom A ab a ) ( π2 : Hom A ab b ) | |
| 266 : Set (ℓ ⊔ (c₁ ⊔ c₂)) where | |
| 267 field | |
| 268 commute : A [ A [ f o π1 ] ≈ A [ g o π2 ] ] | |
| 269 p : { d : Obj A } → { π1' : Hom A d a } { π2' : Hom A d b } → A [ A [ f o π1' ] ≈ A [ g o π2' ] ] → Hom A d ab | |
|
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
270 π1p=π1 : { d : Obj A } → { π1' : Hom A d a } { π2' : Hom A d b } → { eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ] } |
|
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
271 → A [ A [ π1 o p eq ] ≈ π1' ] |
|
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
272 π2p=π2 : { d : Obj A } → { π1' : Hom A d a } { π2' : Hom A d b } → { eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ] } |
|
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
273 → A [ A [ π2 o p eq ] ≈ π2' ] |
|
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
274 uniqueness : { d : Obj A } → ( p' : Hom A d ab ) → { π1' : Hom A d a } { π2' : Hom A d b } → { eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ] } |
| 260 | 275 → { π1p=π1' : A [ A [ π1 o p' ] ≈ π1' ] } |
| 276 → { π2p=π2' : A [ A [ π2 o p' ] ≈ π2' ] } | |
| 277 → A [ p eq ≈ p' ] | |
| 278 axb : Obj A | |
| 279 axb = ab | |
|
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
280 pi1 : Hom A ab a |
|
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
281 pi1 = π1 |
|
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
282 pi2 : Hom A ab b |
|
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
283 pi2 = π2 |
|
312
702adc45704f
is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
300
diff
changeset
|
284 |
|
702adc45704f
is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
300
diff
changeset
|
285 -- |
|
702adc45704f
is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
300
diff
changeset
|
286 -- Limit |
|
702adc45704f
is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
300
diff
changeset
|
287 -- |
|
702adc45704f
is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
300
diff
changeset
|
288 ----- |
|
702adc45704f
is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
300
diff
changeset
|
289 |
|
702adc45704f
is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
300
diff
changeset
|
290 -- Constancy Functor |
|
702adc45704f
is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
300
diff
changeset
|
291 |
|
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
292 K : { c₁' c₂' ℓ' : Level} (A : Category c₁' c₂' ℓ') { c₁'' c₂'' ℓ'' : Level} ( I : Category c₁'' c₂'' ℓ'' ) |
|
312
702adc45704f
is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
300
diff
changeset
|
293 → ( a : Obj A ) → Functor I A |
|
702adc45704f
is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
300
diff
changeset
|
294 K A I a = record { |
|
702adc45704f
is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
300
diff
changeset
|
295 FObj = λ i → a ; |
|
702adc45704f
is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
300
diff
changeset
|
296 FMap = λ f → id1 A a ; |
|
702adc45704f
is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
300
diff
changeset
|
297 isFunctor = let open ≈-Reasoning (A) in record { |
|
702adc45704f
is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
300
diff
changeset
|
298 ≈-cong = λ f=g → refl-hom |
|
702adc45704f
is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
300
diff
changeset
|
299 ; identity = refl-hom |
|
702adc45704f
is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
300
diff
changeset
|
300 ; distr = sym idL |
|
702adc45704f
is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
300
diff
changeset
|
301 } |
|
702adc45704f
is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
300
diff
changeset
|
302 } |
|
702adc45704f
is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
300
diff
changeset
|
303 |
|
702adc45704f
is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
300
diff
changeset
|
304 |
| 487 | 305 record IsLimit { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) |
| 306 (a0 : Obj A ) (t0 : NTrans I A ( K A I a0 ) Γ ) : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where | |
|
312
702adc45704f
is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
300
diff
changeset
|
307 field |
|
702adc45704f
is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
300
diff
changeset
|
308 limit : ( a : Obj A ) → ( t : NTrans I A ( K A I a ) Γ ) → Hom A a a0 |
|
702adc45704f
is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
300
diff
changeset
|
309 t0f=t : { a : Obj A } → { t : NTrans I A ( K A I a ) Γ } → ∀ { i : Obj I } → |
|
702adc45704f
is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
300
diff
changeset
|
310 A [ A [ TMap t0 i o limit a t ] ≈ TMap t i ] |
| 495 | 311 limit-uniqueness : { a : Obj A } → { t : NTrans I A ( K A I a ) Γ } → { f : Hom A a a0 } → ( ∀ { i : Obj I } → |
|
312
702adc45704f
is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
300
diff
changeset
|
312 A [ A [ TMap t0 i o f ] ≈ TMap t i ] ) → A [ limit a t ≈ f ] |
|
702adc45704f
is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
300
diff
changeset
|
313 |
| 487 | 314 record Limit { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) |
| 315 : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where | |
| 316 field | |
| 317 a0 : Obj A | |
| 318 t0 : NTrans I A ( K A I a0 ) Γ | |
| 319 isLimit : IsLimit A I Γ a0 t0 | |
| 320 | |
| 321 LimitNat : { c₁' c₂' ℓ' : Level} (B : Category c₁' c₂' ℓ') { c₁ c₂ ℓ : Level} ( I : Category c₁ c₂ ℓ ) { c₁'' c₂'' ℓ'' : Level} | |
| 322 ( C : Category c₁'' c₂'' ℓ'' ) | |
| 323 ( Γ : Functor I B ) | |
| 324 ( lim : Obj B ) ( tb : NTrans I B ( K B I lim ) Γ ) → | |
| 325 ( U : Functor B C) → NTrans I C ( K C I (FObj U lim) ) (U ○ Γ) | |
| 326 LimitNat B I C Γ lim tb U = record { | |
| 327 TMap = TMap (Functor*Nat I C U tb) ; | |
| 328 isNTrans = record { commute = λ {a} {b} {f} → let open ≈-Reasoning (C) in begin | |
| 329 FMap (U ○ Γ) f o TMap (Functor*Nat I C U tb) a | |
| 330 ≈⟨ nat ( Functor*Nat I C U tb ) ⟩ | |
| 331 TMap (Functor*Nat I C U tb) b o FMap (U ○ K B I lim) f | |
| 332 ≈⟨ cdr (IsFunctor.identity (isFunctor U) ) ⟩ | |
| 333 TMap (Functor*Nat I C U tb) b o FMap (K C I (FObj U lim)) f | |
| 334 ∎ | |
| 335 } } | |
| 336 | |
| 337 open Limit | |
| 338 record LimitPreserve { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Category c₁' c₂' ℓ' ) | |
| 339 { c₁'' c₂'' ℓ'' : Level} ( C : Category c₁'' c₂'' ℓ'' ) | |
| 340 (G : Functor A C) : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁'' ⊔ c₂'' ⊔ ℓ'' )) where | |
| 341 field | |
| 342 preserve : ( Γ : Functor I A ) → ( limita : Limit A I Γ ) → | |
| 343 IsLimit C I (G ○ Γ) (FObj G (a0 limita ) ) (LimitNat A I C Γ (a0 limita ) (t0 limita) G ) | |
| 492 | 344 plimit : { Γ : Functor I A } → ( limita : Limit A I Γ ) → Limit C I (G ○ Γ ) |
| 345 plimit {Γ} limita = record { a0 = (FObj G (a0 limita )) | |
| 487 | 346 ; t0 = LimitNat A I C Γ (a0 limita ) (t0 limita) G |
| 347 ; isLimit = preserve Γ limita } | |
| 348 | |
|
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
349 record CreateLimit { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Category c₁' c₂' ℓ' ) |
| 440 | 350 : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where |
| 351 field | |
| 487 | 352 climit : ( Γ : Functor I A ) -> Limit A I Γ |
| 440 | 353 |
|
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
354 record Complete { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Category c₁' c₂' ℓ' ) |
| 440 | 355 : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where |
| 356 field | |
| 487 | 357 climit : ( Γ : Functor I A ) -> Limit A I Γ |
| 358 alimit : ( Γ : Functor I A ) (a0 : Obj A ) ( t0 : NTrans I A ( K A I a0 ) Γ ) -> IsLimit A I Γ a0 t0 | |
| 440 | 359 |
| 360 product : (a b : Obj A) -> Obj A | |
|
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
361 π1 : (a b : Obj A) -> Hom A (product a b ) a |
|
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
362 π2 : (a b : Obj A) -> Hom A (product a b ) b |
| 440 | 363 isProduct : (a b : Obj A) -> Product A a b (product a b) (π1 a b ) (π2 a b) |
| 364 | |
| 365 equalizer-p : {a b : Obj A} (f g : Hom A a b) -> Obj A | |
| 366 equalizer-e : {a b : Obj A} (f g : Hom A a b) -> Hom A (equalizer-p f g) a | |
|
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
367 isEqualizer : {a b : Obj A} (f g : Hom A a b) -> IsEqualizer A (equalizer-e f g) f g |
|
484
fcae3025d900
fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
468
diff
changeset
|
368 open Limit |
|
fcae3025d900
fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
468
diff
changeset
|
369 limit-c : ( Γ : Functor I A ) -> Obj A |
| 487 | 370 limit-c Γ = a0 ( climit Γ) |
|
484
fcae3025d900
fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
468
diff
changeset
|
371 limit-u : ( Γ : Functor I A ) -> NTrans I A ( K A I (limit-c Γ )) Γ |
| 487 | 372 limit-u Γ = t0 ( climit Γ) |