Mercurial > hg > Members > kono > Proof > category
annotate limit-to.agda @ 403:375edfefbf6a
maybe CAT
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 20 Mar 2016 11:36:44 +0900 |
| parents | 9123f79c0642 |
| children | 07bea66e5ceb |
| rev | line source |
|---|---|
| 350 | 1 open import Category -- https://github.com/konn/category-agda |
| 2 open import Level | |
| 3 | |
| 403 | 4 module limit-to where |
| 350 | 5 |
| 6 open import cat-utility | |
| 7 open import HomReasoning | |
| 8 open import Relation.Binary.Core | |
|
401
e4c10d6375f6
Maybe Category to-limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
400
diff
changeset
|
9 open import Data.Maybe |
| 350 | 10 open Functor |
| 11 | |
| 12 | |
|
401
e4c10d6375f6
Maybe Category to-limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
400
diff
changeset
|
13 |
|
e4c10d6375f6
Maybe Category to-limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
400
diff
changeset
|
14 |
| 350 | 15 -- If we have limit then we have equalizer |
| 16 --- two objects category | |
| 17 --- | |
| 18 --- f | |
| 19 --- ------> | |
| 20 --- 0 1 | |
| 366 | 21 --- ------> |
| 22 --- g | |
| 387 | 23 |
| 350 | 24 |
|
355
8fd085379380
add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
354
diff
changeset
|
25 |
| 385 | 26 data TwoObject {c₁ : Level} : Set c₁ where |
| 363 | 27 t0 : TwoObject |
| 28 t1 : TwoObject | |
| 359 | 29 |
| 385 | 30 data Arrow {ℓ : Level } : Set ℓ where |
|
377
2dfa2d59268c
associative in twocat dead end?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
376
diff
changeset
|
31 id-t0 : Arrow |
|
2dfa2d59268c
associative in twocat dead end?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
376
diff
changeset
|
32 arrow-f : Arrow |
|
2dfa2d59268c
associative in twocat dead end?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
376
diff
changeset
|
33 arrow-g : Arrow |
|
397
dd3fa0680897
inconsistent distribution law on nil x arrow-g
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
396
diff
changeset
|
34 nil : Arrow |
|
377
2dfa2d59268c
associative in twocat dead end?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
376
diff
changeset
|
35 |
| 403 | 36 record RawHom { c₁ c₂ : Level} (a : TwoObject {c₁} ) (b : TwoObject {c₁} ) : Set c₂ where |
| 384 | 37 field |
| 403 | 38 RawMap : Arrow { c₂ } |
| 384 | 39 |
| 40 open RawHom | |
| 382 | 41 |
| 403 | 42 record Two-Hom { c₁ c₂ : Level } (a : TwoObject { c₁} ) (b : TwoObject { c₁} ) : Set c₂ where |
|
377
2dfa2d59268c
associative in twocat dead end?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
376
diff
changeset
|
43 field |
| 403 | 44 hom : Maybe ( RawHom {c₁} { c₂ } a b ) |
| 400 | 45 |
| 46 open Two-Hom | |
| 47 | |
| 403 | 48 Two-id : { c₁ c₂ : Level } -> (a : TwoObject {c₁} ) -> Two-Hom {c₁} { c₂} a a |
|
401
e4c10d6375f6
Maybe Category to-limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
400
diff
changeset
|
49 Two-id _ = record { hom = just ( record { RawMap = id-t0 } ) } |
|
377
2dfa2d59268c
associative in twocat dead end?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
376
diff
changeset
|
50 |
|
2dfa2d59268c
associative in twocat dead end?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
376
diff
changeset
|
51 -- arrow composition |
|
2dfa2d59268c
associative in twocat dead end?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
376
diff
changeset
|
52 |
| 403 | 53 twocomp : {c₁ c₂ : Level } -> { a b : TwoObject {c₁} } -> Arrow { c₂ } -> Arrow { c₂ } -> Maybe ( RawHom a b ) |
|
401
e4c10d6375f6
Maybe Category to-limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
400
diff
changeset
|
54 twocomp id-t0 f = just ( record { RawMap = f } ) |
|
e4c10d6375f6
Maybe Category to-limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
400
diff
changeset
|
55 twocomp f id-t0 = just ( record { RawMap = f } ) |
| 400 | 56 twocomp _ _ = nothing |
|
377
2dfa2d59268c
associative in twocat dead end?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
376
diff
changeset
|
57 |
| 403 | 58 _×_ : { c₁ c₂ : Level } -> {A B C : TwoObject { c₁} } → Two-Hom { c₁} {c₂} B C → Two-Hom { c₁} {c₂} A B → Two-Hom { c₁} {c₂} A C |
|
401
e4c10d6375f6
Maybe Category to-limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
400
diff
changeset
|
59 _×_ { c₁} {ℓ} {a} {b} {c} f g with hom f | hom g |
|
e4c10d6375f6
Maybe Category to-limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
400
diff
changeset
|
60 _×_ { c₁} {ℓ} {a} {b} {c} f g | nothing | _ = record { hom = nothing } |
|
e4c10d6375f6
Maybe Category to-limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
400
diff
changeset
|
61 _×_ { c₁} {ℓ} {a} {b} {c} f g | _ | nothing = record { hom = nothing } |
|
e4c10d6375f6
Maybe Category to-limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
400
diff
changeset
|
62 _×_ { c₁} {ℓ} {a} {b} {c} _ _ | just f | just g = record { hom = twocomp { c₁} {ℓ} {a} {c} (RawMap f) (RawMap g ) } |
|
e4c10d6375f6
Maybe Category to-limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
400
diff
changeset
|
63 |
| 403 | 64 _==_ : {c₁ c₂ : Level } -> {a b : TwoObject {c₁} } -> Rel (Maybe (RawHom {c₁} {c₂} a b )) c₂ |
|
401
e4c10d6375f6
Maybe Category to-limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
400
diff
changeset
|
65 _==_ = Eq ( _≡_ ) |
| 393 | 66 |
| 403 | 67 open import maybeCat |
| 68 | |
| 393 | 69 |
| 403 | 70 TwoCat : { c₁ c₂ ℓ : Level } -> Category c₁ c₂ c₂ |
| 385 | 71 TwoCat {c₁} {c₂} {ℓ} = record { |
| 72 Obj = TwoObject {c₁} ; | |
| 403 | 73 Hom = λ a b → Two-Hom {c₁ } { c₂} a b ; |
| 74 _o_ = _×_ { c₁} {c₂} ; | |
|
401
e4c10d6375f6
Maybe Category to-limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
400
diff
changeset
|
75 _≈_ = λ a b → hom a == hom b ; |
|
377
2dfa2d59268c
associative in twocat dead end?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
376
diff
changeset
|
76 Id = \{a} -> Two-id a ; |
|
2dfa2d59268c
associative in twocat dead end?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
376
diff
changeset
|
77 isCategory = record { |
| 403 | 78 isEquivalence = record {refl = *refl {_} {_} {_} {{!!}}; trans = *trans {_} {_} {_} {{!!}}; sym = *sym {_} {_} {_} {{!!}}}; |
| 384 | 79 identityL = \{a b f} -> identityL {a} {b} {f} ; |
| 80 identityR = \{a b f} -> identityR {a} {b} {f} ; | |
| 379 | 81 o-resp-≈ = \{a b c f g h i} -> o-resp-≈ {a} {b} {c} {f} {g} {h} {i} ; |
| 381 | 82 associative = \{a b c d f g h } -> associative {a} {b} {c} {d} {f} {g} {h} |
|
377
2dfa2d59268c
associative in twocat dead end?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
376
diff
changeset
|
83 } |
|
2dfa2d59268c
associative in twocat dead end?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
376
diff
changeset
|
84 } where |
|
2dfa2d59268c
associative in twocat dead end?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
376
diff
changeset
|
85 open import Relation.Binary.PropositionalEquality |
|
2dfa2d59268c
associative in twocat dead end?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
376
diff
changeset
|
86 ≡-cong = Relation.Binary.PropositionalEquality.cong |
|
401
e4c10d6375f6
Maybe Category to-limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
400
diff
changeset
|
87 identityL : {A B : TwoObject} {f : Two-Hom A B} → hom ( Two-id B × f ) == hom f |
| 402 | 88 identityL {a} {b} {f} = {!!} |
|
401
e4c10d6375f6
Maybe Category to-limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
400
diff
changeset
|
89 identityR : {A B : TwoObject} {f : Two-Hom A B} → hom ( f × Two-id A ) == hom f |
| 402 | 90 identityR {a} {b} {f} = {!!} |
| 383 | 91 o-resp-≈ : {A B C : TwoObject} {f g : Two-Hom A B} {h i : Two-Hom B C} → |
|
401
e4c10d6375f6
Maybe Category to-limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
400
diff
changeset
|
92 hom f == hom g → hom h == hom i → hom ( h × f ) == hom ( i × g ) |
| 402 | 93 o-resp-≈ {a} {b} {c} {f} {g} {h} {i} f≡g h≡i = {!!} |
|
401
e4c10d6375f6
Maybe Category to-limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
400
diff
changeset
|
94 associative : {A B C D : TwoObject} {f : Two-Hom C D} {g : Two-Hom B C} {h : Two-Hom A B} → hom ( f × (g × h) ) == hom ( (f × g) × h ) |
| 402 | 95 associative {_} {_} {_} {_} {f} {g} {h} = {!!} |
| 393 | 96 |
| 403 | 97 indexFunctor : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( a b : Obj (MaybeCat A )) ( f g : Hom A a b ) -> Functor (TwoCat {c₁} {c₂} {c₂} ) (MaybeCat A ) |
| 98 indexFunctor {c₁} {c₂} {ℓ} A a b f g = record { | |
| 385 | 99 FObj = λ a → fobj a |
| 366 | 100 ; FMap = λ f → fmap f |
| 101 ; isFunctor = record { | |
|
374
5641b923201e
limit-to: indexFunctor distribution law cannot be proved
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
373
diff
changeset
|
102 identity = \{x} -> identity {x} |
| 388 | 103 ; distr = \ {a} {b} {c} {f} {g} -> distr1 {a} {b} {c} {f} {g} |
| 396 | 104 ; ≈-cong = \ {a} {b} {c} {f} -> ≈-cong {a} {b} {c} {f} |
| 366 | 105 } |
| 106 } where | |
| 388 | 107 I = TwoCat {c₁} {c₂} {ℓ} |
| 402 | 108 MA = MaybeCat A |
| 388 | 109 fobj : Obj I -> Obj A |
| 385 | 110 fobj t0 = a |
| 111 fobj t1 = b | |
| 403 | 112 fmap1 : {x y : Obj I } -> (Arrow {c₂} ) -> Hom MA (fobj x) (fobj y) |
|
401
e4c10d6375f6
Maybe Category to-limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
400
diff
changeset
|
113 fmap1 {t0} {t1} arrow-f = record { hom = just f } |
|
e4c10d6375f6
Maybe Category to-limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
400
diff
changeset
|
114 fmap1 {t0} {t1} arrow-g = record { hom = just g } |
|
e4c10d6375f6
Maybe Category to-limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
400
diff
changeset
|
115 fmap1 {t0} {t0} id-t0 = record { hom = just ( id1 A a )} |
|
e4c10d6375f6
Maybe Category to-limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
400
diff
changeset
|
116 fmap1 {t1} {t1} id-t0 = record { hom = just ( id1 A b )} |
|
e4c10d6375f6
Maybe Category to-limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
400
diff
changeset
|
117 fmap1 {_} {_} _ = record { hom = nothing } |
| 402 | 118 fmap : {x y : Obj I } -> Hom I x y -> Hom MA (fobj x) (fobj y) |
|
401
e4c10d6375f6
Maybe Category to-limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
400
diff
changeset
|
119 fmap {x} {y} f with ( hom f ) |
|
e4c10d6375f6
Maybe Category to-limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
400
diff
changeset
|
120 fmap {x} {y} f | nothing = record { hom = nothing } |
|
e4c10d6375f6
Maybe Category to-limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
400
diff
changeset
|
121 fmap {x} {y} _ | just f = fmap1 {x} {y} ( RawMap f ) |
| 388 | 122 open ≈-Reasoning (A) |
| 402 | 123 identity : {x : Obj I} → MA [ fmap (id1 I x) ≈ id1 MA (fobj x) ] |
| 124 identity {t0} = {!!} | |
| 125 identity {t1} = {!!} | |
|
401
e4c10d6375f6
Maybe Category to-limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
400
diff
changeset
|
126 distr1 : {a₁ : Obj I} {b₁ : Obj I} {c : Obj I} {f₁ : Hom I a₁ b₁} {g₁ : Hom I b₁ c} → |
| 402 | 127 MA [ fmap (I [ g₁ o f₁ ]) ≈ MA [ fmap g₁ o fmap f₁ ] ] |
| 128 distr1 {a1} {b1} {c} {f1} {g1} = {!!} | |
| 129 ≈-cong : {a : Obj I} {b : Obj I} {f g : Hom I a b} → I [ f ≈ g ] → MA [ fmap f ≈ fmap g ] | |
| 130 ≈-cong {_} {_} {f1} {g1} f≈g = {!!} | |
| 388 | 131 |
| 365 | 132 |
| 387 | 133 --- Equalizer |
| 134 --- f | |
| 135 --- e ------> | |
| 136 --- c ------> a b | |
| 137 --- ^ / ------> | |
| 138 --- |k h g | |
| 139 --- | / | |
| 140 --- | / | |
| 141 --- | / | |
| 142 --- |/ | |
| 143 --- d | |
| 144 | |
| 350 | 145 open Limit |
| 352 | 146 |
| 403 | 147 lim-to-equ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) -> |
| 364 | 148 (lim : (I : Category c₁ c₂ ℓ) ( Γ : Functor I A ) → { a0 : Obj A } { u : NTrans I A ( K A I a0 ) Γ } → Limit A I Γ a0 u ) -- completeness |
|
401
e4c10d6375f6
Maybe Category to-limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
400
diff
changeset
|
149 → {a b c : Obj A} (f g : Hom A a b ) |
| 365 | 150 → (e : Hom A c a ) → (fe=ge : A [ A [ f o e ] ≈ A [ g o e ] ] ) → Equalizer A e f g |
| 403 | 151 lim-to-equ {c₁} {c₂} {ℓ } A lim {a} {b} {c} f g e fe=ge = record { |
| 350 | 152 fe=ge = fe=ge |
| 153 ; k = λ {d} h fh=gh → k {d} h fh=gh | |
| 373 | 154 ; ek=h = λ {d} {h} {fh=gh} → ek=h d h fh=gh |
| 155 ; uniqueness = λ {d} {h} {fh=gh} {k'} → uniquness d h fh=gh k' | |
| 350 | 156 } where |
| 388 | 157 I = TwoCat {c₁} {c₂} {ℓ } |
| 402 | 158 Γ = {!!} |
| 375 | 159 nmap : (x : Obj I) ( d : Obj A ) (h : Hom A d a ) -> Hom A (FObj (K A I d) x) (FObj Γ x) |
| 385 | 160 nmap x d h = {!!} |
| 375 | 161 commute1 : {x y : Obj I} {f' : Hom I x y} (d : Obj A) (h : Hom A d a ) -> A [ A [ f o h ] ≈ A [ g o h ] ] |
| 162 → A [ A [ FMap Γ f' o nmap x d h ] ≈ A [ nmap y d h o FMap (K A I d) f' ] ] | |
| 385 | 163 commute1 {x} {y} {f'} d h fh=gh = {!!} |
| 375 | 164 nat : (d : Obj A) → (h : Hom A d a ) → A [ A [ f o h ] ≈ A [ g o h ] ] → NTrans I A (K A I d) Γ |
|
368
b18585089d2e
add more parameter to nat in lim-to-equ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
367
diff
changeset
|
165 nat d h fh=gh = record { |
| 367 | 166 TMap = λ x → nmap x d h ; |
| 350 | 167 isNTrans = record { |
|
371
3a125d05ae0f
limit-to nat will be done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
370
diff
changeset
|
168 commute = λ {x} {y} {f'} -> commute1 {x} {y} {f'} d h fh=gh |
| 350 | 169 } |
| 170 } | |
| 171 k : {d : Obj A} (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c | |
| 385 | 172 k {d} h fh=gh = {!!} -- limit (lim I Γ {c} {nat c e fe=ge }) d (nat d h fh=gh ) |
|
372
b4855a3ebd34
add more lemma in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
371
diff
changeset
|
173 ek=h : (d : Obj A ) (h : Hom A d a ) -> ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ] ) -> A [ A [ e o k h fh=gh ] ≈ h ] |
|
374
5641b923201e
limit-to: indexFunctor distribution law cannot be proved
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
373
diff
changeset
|
174 ek=h d h fh=gh = {!!} |
|
372
b4855a3ebd34
add more lemma in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
371
diff
changeset
|
175 uniquness : (d : Obj A ) (h : Hom A d a ) -> ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ] ) -> |
|
b4855a3ebd34
add more lemma in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
371
diff
changeset
|
176 ( k' : Hom A d c ) |
|
b4855a3ebd34
add more lemma in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
371
diff
changeset
|
177 -> A [ A [ e o k' ] ≈ h ] → A [ k h fh=gh ≈ k' ] |
|
b4855a3ebd34
add more lemma in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
371
diff
changeset
|
178 uniquness d h fh=gh = {!!} |
|
368
b18585089d2e
add more parameter to nat in lim-to-equ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
367
diff
changeset
|
179 |
|
372
b4855a3ebd34
add more lemma in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
371
diff
changeset
|
180 |