Mercurial > hg > Members > kono > Proof > category

annotate limit-to.agda @ 416:e4a2544d468c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good so A [ g o f ] should be nothing in codomain Category
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 23 Mar 2016 22:47:32 +0900
parents dd086f5fb29f
children 1e76e611d454
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
415
dd086f5fb29f same conflict again ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 414
diff changeset
1 open import Category -- https://github.com/konn/category-agda
350
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 open import Level
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3
403
375edfefbf6a maybe CAT
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 402
diff changeset
4 module limit-to where
350
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 open import cat-utility
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 open import HomReasoning
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
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
416
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
10 open import maybeCat
350
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 open Functor
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13
401
e4c10d6375f6 Maybe Category to-limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 400
diff changeset
14
e4c10d6375f6 Maybe Category to-limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 400
diff changeset
15
415
dd086f5fb29f same conflict again ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 414
diff changeset
16 -- If we have limit then we have equalizer
350
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 --- two objects category
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 ---
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 --- f
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 --- ------>
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 --- 0 1
366
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
22 --- ------>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
23 --- g
387
2f59c2db9d98 what is this ?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
24
350
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25
355
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 354
diff changeset
26
385
ff3803fc0c8a add level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 384
diff changeset
27 data TwoObject {c₁ : Level} : Set c₁ where
415
dd086f5fb29f same conflict again ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 414
diff changeset
28 t0 : TwoObject
dd086f5fb29f same conflict again ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 414
diff changeset
29 t1 : TwoObject
dd086f5fb29f same conflict again ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 414
diff changeset
30
dd086f5fb29f same conflict again ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 414
diff changeset
31
416
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
32 record TwoCat {ℓ c₁ c₂ : Level } (A : Category c₁ c₂ ℓ) ( a b : Obj A ) ( f g : Hom A a b ): Set (c₂ ⊔ c₁ ⊔ ℓ) where
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
33 field
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
34 obj→ : Obj A -> TwoObject { c₁}
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
35 hom→ : {a b : Obj A} -> Hom A a b -> TwoObject { c₁}
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
36 inv : {a b : Obj A} -> Hom A a b -> Hom A b a
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
37 iso→ : {a b : Obj A} -> ( h : Hom A a b ) -> A [ A [ inv h o h ] ≈ id1 A a ]
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
38 iso← : {a b : Obj A} -> ( h : Hom A a b ) -> A [ A [ h o inv h ] ≈ id1 A b ]
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
39 obj← : TwoObject {c₁} -> Obj A
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
40 obj← t0 = a
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
41 obj← t1 = b
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
42 hom← : TwoObject {c₁} -> Hom A a b
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
43 hom← t0 = f
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
44 hom← t1 = g
414
28249d32b700 Maybe does not help conflict ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 413
diff changeset
45
416
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
46 open TwoCat
410
508c88223aab add reasoning
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 409
diff changeset
47
406
2fbd92ddecb5 non recorded arrow does not work
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 405
diff changeset
48
416
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
49 open MaybeHom
404
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 403
diff changeset
50
409
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 408
diff changeset
51
416
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
52 indexFunctor : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( a b : Obj A) ( f g : Hom A a b ) ->
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
53 TwoCat A a b f g ->
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
54 Functor A (MaybeCat A )
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
55 indexFunctor {c₁} {c₂} {ℓ} A a b f g two = record {
385
ff3803fc0c8a add level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 384
diff changeset
56 FObj = λ a → fobj a
405
4c34c0e3c4bb no Maybe TwoCat in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 404
diff changeset
57 ; FMap = λ {a} {b} f → fmap {a} {b} f
366
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
58 ; isFunctor = record {
374
5641b923201e limit-to: indexFunctor distribution law cannot be proved
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 373
diff changeset
59 identity = \{x} -> identity {x}
415
dd086f5fb29f same conflict again ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 414
diff changeset
60 ; distr = \ {a} {b} {c} {f} {g} -> distr1 {a} {b} {c} {f} {g}
dd086f5fb29f same conflict again ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 414
diff changeset
61 ; ≈-cong = \ {a} {b} {c} {f} -> ≈-cong {a} {b} {c} {f}
366
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
62 }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
63 } where
402
9123f79c0642 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 401
diff changeset
64 MA = MaybeCat A
404
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 403
diff changeset
65 open ≈-Reasoning (MA)
416
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
66 fobj : Obj A -> Obj A
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
67 fobj x with obj→ two x
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
68 fobj _ | t0 = a
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
69 fobj _ | t1 = b
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
70 fmap : {x y : Obj A } -> (Hom A x y ) -> Hom MA (fobj x) (fobj y)
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
71 fmap {x} {y} h with obj→ two x | obj→ two y | hom→ two f
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
72 fmap {_} {_} h | t0 | t1 | t0 = record { hom = just f }
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
73 fmap {_} {_} h | t0 | t1 | t1 = record { hom = just g }
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
74 fmap {_} {_} h | t1 | t0 | t0 = record { hom = just (inv two f) }
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
75 fmap {_} {_} h | t1 | t0 | t1 = record { hom = just (inv two g) }
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
76 fmap {x} {_} h | t0 | t0 | _ = id1 MA ( obj← two t0 )
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
77 fmap {x} {_} h | t1 | t1 | _ = id1 MA ( obj← two t1 )
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
78 identity : {x : Obj A} → MA [ fmap ( id1 A x ) ≈ id1 MA ( fobj x ) ]
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
79 identity {x} with obj→ two x
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
80 identity | t0 = refl-hom
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
81 identity | t1 = refl-hom
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
82 distr1 : {a₁ : Obj A} {b₁ : Obj A} {c : Obj A} {f₁ : Hom A a₁ b₁} {g₁ : Hom A b₁ c} →
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
83 MA [ fmap (A [ g₁ o f₁ ]) ≈ MA [ fmap g₁ o fmap f₁ ] ]
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
84 distr1 {a1} {b1} {c} {f1} {g1} with obj→ two a1 | obj→ two b1 | obj→ two c | hom→ two f | hom→ two g
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
85 distr1 {a1} {b1} {c} {f1} {g1} | t0 | t0 | t0 | _ | _ = {!!}
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
86 distr1 {a1} {b1} {c} {f1} {g1} | t0 | t0 | t1 | _ | _ = {!!}
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
87 distr1 {a1} {b1} {c} {f1} {g1} | t0 | t1 | t1 | _ | _ = {!!}
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
88 distr1 {a1} {b1} {c} {f1} {g1} | t1 | t1 | t1 | _ | _ = {!!}
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
89 distr1 {a1} {b1} {c} {f1} {g1} | t1 | t0 | t0 | _ | _ = {!!}
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
90 distr1 {a1} {b1} {c} {f1} {g1} | t1 | t1 | t0 | _ | _ = {!!}
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
91 -- next two cases require the inverse of f and g
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
92 -- if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
93 -- so A [ g o f ] should be nothing in codomain Category
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
94 distr1 {a1} {b1} {c} {f1} {g1} | t1 | t0 | t1 | _ | _ = {!!}
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
95 distr1 {a1} {b1} {c} {f1} {g1} | t0 | t1 | t0 | _ | _ = {!!}
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
96 ≈-cong : {a : Obj A} {b : Obj A} {f g : Hom A a b} → _[_≈_] A f g → {!!}
402
9123f79c0642 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 401
diff changeset
97 ≈-cong {_} {_} {f1} {g1} f≈g = {!!}
388
a0ab2643eee7 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 387
diff changeset
98
365
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 364
diff changeset
99
387
2f59c2db9d98 what is this ?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
100 --- Equalizer
2f59c2db9d98 what is this ?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
101 --- f
2f59c2db9d98 what is this ?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
102 --- e ------>
2f59c2db9d98 what is this ?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
103 --- c ------> a b
2f59c2db9d98 what is this ?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
104 --- ^ / ------>
2f59c2db9d98 what is this ?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
105 --- |k h g
415
dd086f5fb29f same conflict again ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 414
diff changeset
106 --- | /
dd086f5fb29f same conflict again ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 414
diff changeset
107 --- | /
dd086f5fb29f same conflict again ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 414
diff changeset
108 --- | /
dd086f5fb29f same conflict again ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 414
diff changeset
109 --- |/
dd086f5fb29f same conflict again ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 414
diff changeset
110 --- d
387
2f59c2db9d98 what is this ?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
111
350
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
112 open Limit
352
f589e71875ea bad approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 351
diff changeset
113
403
375edfefbf6a maybe CAT
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 402
diff changeset
114 lim-to-equ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ->
412
f04b2fb91432 recover TwoHom
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 410
diff changeset
115 (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
415
dd086f5fb29f same conflict again ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 414
diff changeset
116 → {a b c : Obj A} (f g : Hom A a b )
365
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 364
diff changeset
117 → (e : Hom A c a ) → (fe=ge : A [ A [ f o e ] ≈ A [ g o e ] ] ) → Equalizer A e f g
403
375edfefbf6a maybe CAT
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 402
diff changeset
118 lim-to-equ {c₁} {c₂} {ℓ } A lim {a} {b} {c} f g e fe=ge = record {
350
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
119 fe=ge = fe=ge
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
120 ; k = λ {d} h fh=gh → k {d} h fh=gh
373
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 372
diff changeset
121 ; ek=h = λ {d} {h} {fh=gh} → ek=h d h fh=gh
416
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
122 ; uniqueness = λ {d} {h} {fh=gh} {k'} → uniquness d h fh=gh k' } where
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
123 I = A
e4a2544d468c if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 415
diff changeset
124 MA = MaybeCat A
402
9123f79c0642 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 401
diff changeset
125 Γ = {!!}
375
5a6db4bc4d9b still trying ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 374
diff changeset
126 nmap : (x : Obj I) ( d : Obj A ) (h : Hom A d a ) -> Hom A (FObj (K A I d) x) (FObj Γ x)
385
ff3803fc0c8a add level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 384
diff changeset
127 nmap x d h = {!!}
415
dd086f5fb29f same conflict again ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 414
diff changeset
128 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 ] ]
375
5a6db4bc4d9b still trying ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 374
diff changeset
129 → A [ A [ FMap Γ f' o nmap x d h ] ≈ A [ nmap y d h o FMap (K A I d) f' ] ]
385
ff3803fc0c8a add level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 384
diff changeset
130 commute1 {x} {y} {f'} d h fh=gh = {!!}
375
5a6db4bc4d9b still trying ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 374
diff changeset
131 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
132 nat d h fh=gh = record {
415
dd086f5fb29f same conflict again ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 414
diff changeset
133 TMap = λ x → nmap x d h ;
350
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
134 isNTrans = record {
415
dd086f5fb29f same conflict again ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 414
diff changeset
135 commute = λ {x} {y} {f'} -> commute1 {x} {y} {f'} d h fh=gh
350
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
136 }
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
137 }
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
138 k : {d : Obj A} (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c
385
ff3803fc0c8a add level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 384
diff changeset
139 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
140 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
141 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
142 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
143 ( k' : Hom A d c )
b4855a3ebd34 add more lemma in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 371
diff changeset
144 -> A [ A [ e o k' ] ≈ h ] → A [ k h fh=gh ≈ k' ]
415
dd086f5fb29f same conflict again ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 414
diff changeset
145 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
146
372
b4855a3ebd34 add more lemma in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 371
diff changeset
147