Mercurial > hg > Members > kono > Proof > category

annotate limit-to.agda @ 460:961c236807f1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
limit-to done discrete done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 03 Mar 2017 12:12:06 +0900
parents fd79b6d9f350
children 8436a018f88a
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
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
10 open import discrete
427
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
11
365
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 364
diff changeset
12
458
fd79b6d9f350 fix comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 457
diff changeset
13 --- Equalizer from Limit ( 2->A functor Γ and Nat : K ->　Γ)
fd79b6d9f350 fix comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 457
diff changeset
14 ---
fd79b6d9f350 fix comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 457
diff changeset
15 ---
387
2f59c2db9d98 what is this ?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
16 --- f
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
17 --- e -----→
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
18 --- c -----→ a b A
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
19 --- ^ / -----→
387
2f59c2db9d98 what is this ?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
20 --- |k h g
415
dd086f5fb29f same conflict again ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 414
diff changeset
21 --- | /
426
1290d6876129 Functor MA → A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 425
diff changeset
22 --- | / ^
1290d6876129 Functor MA → A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 425
diff changeset
23 --- | / |
1290d6876129 Functor MA → A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 425
diff changeset
24 --- |/ | Γ
1290d6876129 Functor MA → A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 425
diff changeset
25 --- d _ |
432
688066ac172e add another method as a comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 431
diff changeset
26 --- |\ |
688066ac172e add another method as a comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 431
diff changeset
27 --- \ K af
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
28 --- \ -----→
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
29 --- \ t0 t1 I
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
30 --- -----→
426
1290d6876129 Functor MA → A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 425
diff changeset
31 --- ag
1290d6876129 Functor MA → A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 425
diff changeset
32 ---
1290d6876129 Functor MA → A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 425
diff changeset
33 ---
387
2f59c2db9d98 what is this ?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
34
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
35 open Complete
350
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 open Limit
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
37 open NTrans
352
f589e71875ea bad approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 351
diff changeset
38
458
fd79b6d9f350 fix comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 457
diff changeset
39 -- Functor Γ : TwoCat -> A
424
4329525f5085 fix imit-to-edu for MaybeCat / TwoCat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 423
diff changeset
40
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
41 IndexFunctor : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( a b : Obj A) ( f g : Hom A a b ) → Functor (TwoCat {c₁} {c₂}) A
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
42 IndexFunctor {c₁} {c₂} {ℓ} A a b f g = record {
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
43 FObj = λ a → fobj a
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
44 ; FMap = λ {a} {b} f → fmap {a} {b} f
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
45 ; isFunctor = record {
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
46 identity = λ{x} → identity x
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
47 ; distr = λ {a} {b} {c} {f} {g} → distr1 {a} {b} {c} {f} {g}
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
48 ; ≈-cong = λ {a} {b} {c} {f} → ≈-cong {a} {b} {c} {f}
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
49 }
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
50 } where
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
51 T = TwoCat {c₁} {c₂}
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
52 fobj : Obj T → Obj A
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
53 fobj t0 = a
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
54 fobj t1 = b
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
55 fmap : {x y : Obj T } → (Hom T x y ) → Hom A (fobj x) (fobj y)
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
56 fmap {t0} {t0} id-t0 = id1 A a
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
57 fmap {t1} {t1} id-t1 = id1 A b
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
58 fmap {t0} {t1} arrow-f = f
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
59 fmap {t0} {t1} arrow-g = g
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
60 ≈-cong : {a : Obj T} {b : Obj T} {f g : Hom T a b} → T [ f ≈ g ] → A [ fmap f ≈ fmap g ]
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
61 ≈-cong {a} {b} {f} {.f} refl = let open ≈-Reasoning A in refl-hom
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
62 identity : (x : Obj T ) -> A [ fmap (id1 T x) ≈ id1 A (fobj x) ]
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
63 identity t0 = let open ≈-Reasoning A in refl-hom
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
64 identity t1 = let open ≈-Reasoning A in refl-hom
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
65 distr1 : {a : Obj T} {b : Obj T} {c : Obj T} {f : Hom T a b} {g : Hom T b c} →
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
66 A [ fmap (T [ g o f ]) ≈ A [ fmap g o fmap f ] ]
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
67 distr1 {t0} {t0} {t0} {id-t0 } { id-t0 } = let open ≈-Reasoning A in sym-hom idL
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
68 distr1 {t1} {t1} {t1} { id-t1 } { id-t1 } = let open ≈-Reasoning A in begin
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
69 id1 A b
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
70 ≈↑⟨ idL ⟩
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
71 id1 A b o id1 A b
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
72 ∎
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
73 distr1 {t0} {t0} {t1} { id-t0 } { arrow-f } = let open ≈-Reasoning A in begin
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
74 fmap (comp arrow-f id-t0)
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
75 ≈⟨⟩
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
76 fmap arrow-f
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
77 ≈↑⟨ idR ⟩
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
78 fmap arrow-f o id1 A a
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
79 ∎
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
80 distr1 {t0} {t0} {t1} { id-t0 } { arrow-g } = let open ≈-Reasoning A in begin
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
81 fmap (comp arrow-g id-t0)
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
82 ≈⟨⟩
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
83 fmap arrow-g
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
84 ≈↑⟨ idR ⟩
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
85 fmap arrow-g o id1 A a
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
86 ∎
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
87 distr1 {t0} {t1} {t1} { arrow-f } { id-t1 } = let open ≈-Reasoning A in begin
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
88 fmap (comp id-t1 arrow-f)
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
89 ≈⟨⟩
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
90 fmap arrow-f
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
91 ≈↑⟨ idL ⟩
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
92 id1 A b o fmap arrow-f
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
93 ∎
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
94 distr1 {t0} {t1} {t1} { arrow-g } { id-t1 } = let open ≈-Reasoning A in begin
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
95 fmap (comp id-t1 arrow-g)
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
96 ≈⟨⟩
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
97 fmap arrow-g
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
98 ≈↑⟨ idL ⟩
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
99 id1 A b o fmap arrow-g
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
100 ∎
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
101
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
102 --- Nat for Limit
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
103 --
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
104 -- Nat : K -> IndexFunctor
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
105 --
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
106
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
107 open Functor
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
108
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
109 IndexNat : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
110 → {a b : Obj A} (f g : Hom A a b )
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
111 (d : Obj A) → (h : Hom A d a ) → A [ A [ f o h ] ≈ A [ g o h ] ] →
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
112 NTrans (TwoCat {c₁} {c₂}) A (K A (TwoCat {c₁} {c₂}) d) (IndexFunctor {c₁} {c₂} {ℓ} A a b f g)
460
961c236807f1 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 458
diff changeset
113 IndexNat {c₁} {c₂} {ℓ} A {a} {b} f g d h fh=gh = record {
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
114 TMap = λ x → nmap x d h ;
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
115 isNTrans = record {
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
116 commute = λ {x} {y} {f'} → commute1 {x} {y} {f'} d h fh=gh
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
117 }
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
118 } where
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
119 I = TwoCat {c₁} {c₂}
429
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
120 Γ : Functor I A
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
121 Γ = IndexFunctor {c₁} {c₂} {ℓ} A a b f g
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
122 nmap : (x : Obj I ) ( d : Obj (A) ) (h : Hom A d a ) → Hom A (FObj (K A I d) x) (FObj Γ x)
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
123 nmap t0 d h = h
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
124 nmap t1 d h = A [ f o h ]
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
125 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 ] ]
427
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
126 → A [ A [ FMap Γ f' o nmap x d h ] ≈ A [ nmap y d h o FMap (K A I d) f' ] ]
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
127 commute1 {t0} {t1} {arrow-f} d h fh=gh = let open ≈-Reasoning A in begin
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
128 f o h
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
129 ≈↑⟨ idR ⟩
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
130 (f o h ) o id1 A d
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
131 ∎
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
132 commute1 {t0} {t1} {arrow-g} d h fh=gh = let open ≈-Reasoning A in begin
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
133 g o h
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
134 ≈↑⟨ fh=gh ⟩
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
135 f o h
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
136 ≈↑⟨ idR ⟩
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
137 (f o h ) o id1 A d
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
138 ∎
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
139 commute1 {t0} {t0} {id-t0} d h fh=gh = let open ≈-Reasoning A in begin
429
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
140 id1 A a o h
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
141 ≈⟨ idL ⟩
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
142 h
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
143 ≈↑⟨ idR ⟩
428
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 427
diff changeset
144 h o id1 A d
429
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
145 ∎
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
146 commute1 {t1} {t1} {id-t1} d h fh=gh = let open ≈-Reasoning A in begin
429
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
147 id1 A b o ( f o h )
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
148 ≈⟨ idL ⟩
428
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 427
diff changeset
149 f o h
429
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
150 ≈↑⟨ idR ⟩
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
151 ( f o h ) o id1 A d
428
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 427
diff changeset
152 ∎
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
153
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
154
460
961c236807f1 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 458
diff changeset
155 equlimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A} -> (f g : Hom A a b) (comp : Complete A (TwoCat {c₁} {c₂} )) ->
961c236807f1 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 458
diff changeset
156 Hom A ( limit-c comp (IndexFunctor {c₁} {c₂} {ℓ} A a b f g)) a
961c236807f1 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 458
diff changeset
157 equlimit {c₁} {c₂} {ℓ} A {a} {b} f g comp = TMap (limit-u comp (IndexFunctor {c₁} {c₂} {ℓ} A a b f g)) t0
961c236807f1 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 458
diff changeset
158
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
159 lim-to-equ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
160 (comp : Complete A (TwoCat {c₁} {c₂} ) )
460
961c236807f1 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 458
diff changeset
161 → {a b : Obj A} (f g : Hom A a b )
961c236807f1 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 458
diff changeset
162 → (fe=ge : A [ A [ f o (equlimit A f g comp) ] ≈ A [ g o (equlimit A f g comp) ] ] )
961c236807f1 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 458
diff changeset
163 → IsEqualizer A (equlimit A f g comp) f g
961c236807f1 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 458
diff changeset
164 lim-to-equ {c₁} {c₂} {ℓ} A comp {a} {b} f g fe=ge = record {
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
165 fe=ge = fe=ge
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
166 ; k = λ {d} h fh=gh → k {d} h fh=gh
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
167 ; ek=h = λ {d} {h} {fh=gh} → ek=h d h fh=gh
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
168 ; uniqueness = λ {d} {h} {fh=gh} {k'} → uniquness d h fh=gh k'
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
169 } where
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
170 I = TwoCat {c₁} {c₂}
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
171 Γ : Functor I A
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
172 Γ = IndexFunctor {c₁} {c₂} {ℓ} A a b f g
460
961c236807f1 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 458
diff changeset
173 e = equlimit A f g comp
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
174 c = limit-c comp Γ
460
961c236807f1 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 458
diff changeset
175 natL = limit-u comp Γ
961c236807f1 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 458
diff changeset
176 eqlim = isLimit comp Γ
961c236807f1 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 458
diff changeset
177 nat0 = IndexNat A f g
350
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
178 k : {d : Obj A} (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
179 k {d} h fh=gh = limit eqlim d (nat0 d h fh=gh )
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
180 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 ]
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
181 ek=h d h fh=gh = let open ≈-Reasoning A in begin
430
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
182 e o k h fh=gh
460
961c236807f1 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 458
diff changeset
183 ≈⟨⟩
961c236807f1 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 458
diff changeset
184 TMap (limit-u comp Γ) t0 o k h fh=gh
961c236807f1 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 458
diff changeset
185 ≈⟨ t0f=t eqlim {d} {nat0 d h fh=gh } {t0} ⟩
961c236807f1 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 458
diff changeset
186 TMap (nat0 d h fh=gh) t0
961c236807f1 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 458
diff changeset
187 ≈⟨⟩
430
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
188 h
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
189 ∎
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
190 uniq-nat : {i : Obj I} → (d : Obj A ) (h : Hom A d a ) ( k' : Hom A d c )
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
191 ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ]) → A [ A [ e o k' ] ≈ h ] →
460
961c236807f1 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 458
diff changeset
192 A [ A [ TMap (limit-u comp Γ) i o k' ] ≈ TMap (nat0 d h fh=gh) i ]
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
193 uniq-nat {t0} d h k' fh=gh ek'=h = let open ≈-Reasoning A in begin
460
961c236807f1 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 458
diff changeset
194 TMap (limit-u comp Γ) t0 o k'
430
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
195 ≈⟨⟩
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
196 e o k'
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
197 ≈⟨ ek'=h ⟩
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
198 h
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
199 ≈⟨⟩
460
961c236807f1 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 458
diff changeset
200 TMap (nat0 d h fh=gh) t0
430
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
201 ∎
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
202 uniq-nat {t1} d h k' fh=gh ek'=h = let open ≈-Reasoning A in begin
460
961c236807f1 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 458
diff changeset
203 TMap (limit-u comp Γ) t1 o k'
961c236807f1 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 458
diff changeset
204 ≈↑⟨ car (idR) ⟩
961c236807f1 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 458
diff changeset
205 ( TMap (limit-u comp Γ) t1 o id1 A c ) o k'
961c236807f1 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 458
diff changeset
206 ≈⟨⟩
961c236807f1 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 458
diff changeset
207 ( TMap (limit-u comp Γ) t1 o FMap (K A I c) arrow-f ) o k'
961c236807f1 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 458
diff changeset
208 ≈↑⟨ car ( nat1 (limit-u comp Γ) arrow-f ) ⟩
961c236807f1 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 458
diff changeset
209 ( FMap Γ arrow-f o TMap (limit-u comp Γ) t0 ) o k'
430
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
210 ≈⟨⟩
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
211 (f o e ) o k'
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
212 ≈↑⟨ assoc ⟩
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
213 f o ( e o k' )
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
214 ≈⟨ cdr ek'=h ⟩
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
215 f o h
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
216 ≈⟨⟩
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
217 TMap (nat0 d h fh=gh) t1
430
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
218 ∎
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
219 uniquness : (d : Obj A ) (h : Hom A d a ) → ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ] ) →
372
b4855a3ebd34 add more lemma in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 371
diff changeset
220 ( k' : Hom A d c )
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
221 → A [ A [ e o k' ] ≈ h ] → A [ k h fh=gh ≈ k' ]
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
222 uniquness d h fh=gh k' ek'=h = let open ≈-Reasoning A in begin
430
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
223 k h fh=gh
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 443
diff changeset
224 ≈⟨ limit-uniqueness eqlim k' ( λ{i} → uniq-nat {i} d h k' fh=gh ek'=h ) ⟩
430
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
225 k'
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
226 ∎
368
b18585089d2e add more parameter to nat in lim-to-equ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 367
diff changeset
227