Mercurial > hg > Members > kono > Proof > category
annotate discrete.agda @ 456:4d97955ea419
limit with nat
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 02 Mar 2017 17:41:20 +0900 |
| parents | 55a9b6177ed4 |
| children | 0ba86e29f492 |
| rev | line source |
|---|---|
|
448
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
1 open import Category -- https://github.com/konn/category-agda |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
2 open import Level |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
3 |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
4 module discrete where |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
5 |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
6 open import Relation.Binary.Core |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
7 open import Relation.Nullary |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
8 open import Data.Empty |
|
453
3c2ce4474d92
try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
451
diff
changeset
|
9 open import Data.Unit |
|
448
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
10 open import Data.Maybe |
|
453
3c2ce4474d92
try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
451
diff
changeset
|
11 open import cat-utility |
|
3c2ce4474d92
try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
451
diff
changeset
|
12 open import HomReasoning |
|
448
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
13 |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
14 open Functor |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
15 |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
16 data TwoObject {c₁ : Level} : Set c₁ where |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
17 t0 : TwoObject |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
18 t1 : TwoObject |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
19 |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
20 -- If we have limit then we have equalizer |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
21 --- two objects category |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
22 --- |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
23 --- f |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
24 --- -----→ |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
25 --- 0 1 |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
26 --- -----→ |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
27 --- g |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
28 |
| 455 | 29 data TwoHom {c₁ c₂ : Level } : TwoObject {c₁} → TwoObject {c₁} → Set c₂ where |
| 30 id-t0 : TwoHom t0 t0 | |
| 31 id-t1 : TwoHom t1 t1 | |
| 32 arrow-f : TwoHom t0 t1 | |
| 33 arrow-g : TwoHom t0 t1 | |
|
448
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
34 |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
35 |
| 455 | 36 comp : ∀ {c₁ c₂} → {a b c : TwoObject {c₁}} → TwoHom {c₁} {c₂} b c → TwoHom {c₁} {c₂} a b → TwoHom {c₁} {c₂} a c |
|
453
3c2ce4474d92
try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
451
diff
changeset
|
37 comp {_} {_} {t0} {t1} {t1} id-t1 arrow-f = arrow-f |
|
3c2ce4474d92
try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
451
diff
changeset
|
38 comp {_} {_} {t0} {t1} {t1} id-t1 arrow-g = arrow-g |
|
3c2ce4474d92
try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
451
diff
changeset
|
39 comp {_} {_} {t1} {t1} {t1} id-t1 id-t1 = id-t1 |
|
3c2ce4474d92
try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
451
diff
changeset
|
40 comp {_} {_} {t0} {t0} {t1} arrow-f id-t0 = arrow-f |
|
3c2ce4474d92
try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
451
diff
changeset
|
41 comp {_} {_} {t0} {t0} {t1} arrow-g id-t0 = arrow-g |
|
3c2ce4474d92
try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
451
diff
changeset
|
42 comp {_} {_} {t0} {t0} {t0} id-t0 id-t0 = id-t0 |
|
448
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
43 |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
44 open TwoHom |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
45 |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
46 _×_ : ∀ {c₁ c₂} → {a b c : TwoObject {c₁}} → ( TwoHom {c₁} {c₂} b c ) → ( TwoHom {c₁} {c₂} a b ) → ( TwoHom {c₁} {c₂} a c ) |
| 455 | 47 _×_ {c₁} {c₂} {a} {b} {c} f g = comp {c₁} {c₂} {a} {b} {c} f g |
|
448
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
48 |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
49 |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
50 -- f g h |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
51 -- d <- c <- b <- a |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
52 -- |
| 455 | 53 -- It can be proved without TwoHom constraints |
|
448
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
54 |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
55 assoc-× : {c₁ c₂ : Level } {a b c d : TwoObject {c₁} } |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
56 {f : (TwoHom {c₁} {c₂ } c d )} → |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
57 {g : (TwoHom {c₁} {c₂ } b c )} → |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
58 {h : (TwoHom {c₁} {c₂ } a b )} → |
| 455 | 59 ( f × (g × h)) ≡ ((f × g) × h ) |
| 60 assoc-× {c₁} {c₂} {a} {b} {c} {d} {f} {g} {h} with f | g | h | |
|
453
3c2ce4474d92
try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
451
diff
changeset
|
61 assoc-× {c₁} {c₂} {t0} {t0} {t0} {t0} | id-t0 | id-t0 | id-t0 = refl |
|
3c2ce4474d92
try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
451
diff
changeset
|
62 assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} | arrow-f | id-t0 | id-t0 = refl |
|
3c2ce4474d92
try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
451
diff
changeset
|
63 assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} | arrow-g | id-t0 | id-t0 = refl |
|
3c2ce4474d92
try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
451
diff
changeset
|
64 assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} | id-t1 | arrow-f | id-t0 = refl |
|
3c2ce4474d92
try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
451
diff
changeset
|
65 assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} | id-t1 | arrow-g | id-t0 = refl |
|
3c2ce4474d92
try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
451
diff
changeset
|
66 assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} | id-t1 | id-t1 | arrow-f = refl |
|
3c2ce4474d92
try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
451
diff
changeset
|
67 assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} | id-t1 | id-t1 | arrow-g = refl |
|
3c2ce4474d92
try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
451
diff
changeset
|
68 assoc-× {c₁} {c₂} {t1} {t1} {t1} {t1} | id-t1 | id-t1 | id-t1 = refl |
| 449 | 69 |
| 70 TwoId : {c₁ c₂ : Level } (a : TwoObject {c₁} ) → (TwoHom {c₁} {c₂ } a a ) | |
| 455 | 71 TwoId {_} {_} t0 = id-t0 |
| 72 TwoId {_} {_} t1 = id-t1 | |
| 449 | 73 |
| 74 open import Relation.Binary | |
|
453
3c2ce4474d92
try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
451
diff
changeset
|
75 open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong ) |
|
3c2ce4474d92
try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
451
diff
changeset
|
76 |
| 455 | 77 TwoCat : {c₁ c₂ : Level } → Category c₁ c₂ c₂ |
| 78 TwoCat {c₁} {c₂} = record { | |
| 449 | 79 Obj = TwoObject {c₁} ; |
| 80 Hom = λ a b → ( TwoHom {c₁} {c₂ } a b ) ; | |
| 81 _o_ = λ{a} {b} {c} x y → _×_ {c₁ } { c₂} {a} {b} {c} x y ; | |
| 455 | 82 _≈_ = λ x y → x ≡ y ; |
| 449 | 83 Id = λ{a} → TwoId {c₁ } { c₂} a ; |
| 84 isCategory = record { | |
|
453
3c2ce4474d92
try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
451
diff
changeset
|
85 isEquivalence = record {refl = refl ; trans = trans ; sym = sym } ; |
| 449 | 86 identityL = λ{a b f} → identityL {c₁} {c₂ } {a} {b} {f} ; |
| 87 identityR = λ{a b f} → identityR {c₁} {c₂ } {a} {b} {f} ; | |
| 88 o-resp-≈ = λ{a b c f g h i} → o-resp-≈ {c₁} {c₂ } {a} {b} {c} {f} {g} {h} {i} ; | |
| 89 associative = λ{a b c d f g h } → assoc-× {c₁} {c₂} {a} {b} {c} {d} {f} {g} {h} | |
| 90 } | |
| 91 } where | |
| 455 | 92 identityL : {c₁ c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁} {c₂ } A B) } → ((TwoId B) × f) ≡ f |
| 93 identityL {c₁} {c₂} {a} {b} {f} with f | |
|
453
3c2ce4474d92
try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
451
diff
changeset
|
94 identityL {c₁} {c₂} {t1} {t1} | id-t1 = refl |
|
3c2ce4474d92
try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
451
diff
changeset
|
95 identityL {c₁} {c₂} {t0} {t0} | id-t0 = refl |
|
3c2ce4474d92
try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
451
diff
changeset
|
96 identityL {c₁} {c₂} {t0} {t1} | arrow-f = refl |
|
3c2ce4474d92
try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
451
diff
changeset
|
97 identityL {c₁} {c₂} {t0} {t1} | arrow-g = refl |
| 455 | 98 identityR : {c₁ c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁} {c₂ } A B) } → ( f × TwoId A ) ≡ f |
| 99 identityR {c₁} {c₂} {_} {_} {f} with f | |
|
453
3c2ce4474d92
try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
451
diff
changeset
|
100 identityR {c₁} {c₂} {t1} {t1} | id-t1 = refl |
|
3c2ce4474d92
try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
451
diff
changeset
|
101 identityR {c₁} {c₂} {t0} {t0} | id-t0 = refl |
|
3c2ce4474d92
try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
451
diff
changeset
|
102 identityR {c₁} {c₂} {t0} {t1} | arrow-f = refl |
|
3c2ce4474d92
try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
451
diff
changeset
|
103 identityR {c₁} {c₂} {t0} {t1} | arrow-g = refl |
| 449 | 104 o-resp-≈ : {c₁ c₂ : Level } {A B C : TwoObject {c₁} } {f g : ( TwoHom {c₁} {c₂ } A B)} {h i : ( TwoHom B C)} → |
| 455 | 105 f ≡ g → h ≡ i → ( h × f ) ≡ ( i × g ) |
| 449 | 106 o-resp-≈ {c₁} {c₂} {a} {b} {c} {f} {g} {h} {i} f==g h==i = |
|
453
3c2ce4474d92
try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
451
diff
changeset
|
107 let open ≡-Reasoning in begin |
| 455 | 108 ( h × f ) |
|
453
3c2ce4474d92
try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
451
diff
changeset
|
109 ≡⟨ refl ⟩ |
| 455 | 110 comp (h) (f) |
| 111 ≡⟨ cong (λ x → comp ( h ) x ) f==g ⟩ | |
| 112 comp (h) (g) | |
| 113 ≡⟨ cong (λ x → comp x ( g ) ) h==i ⟩ | |
| 114 comp (i) (g) | |
|
453
3c2ce4474d92
try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
451
diff
changeset
|
115 ≡⟨ refl ⟩ |
| 455 | 116 ( i × g ) |
| 449 | 117 ∎ |
| 118 | |
| 455 | 119 indexFunctor : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( a b : Obj A) ( f g : Hom A a b ) → Functor (TwoCat {c₁} {c₂}) A |
| 120 indexFunctor {c₁} {c₂} {ℓ} A a b f g = record { | |
|
448
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
121 FObj = λ a → fobj a |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
122 ; FMap = λ {a} {b} f → fmap {a} {b} f |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
123 ; isFunctor = record { |
|
453
3c2ce4474d92
try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
451
diff
changeset
|
124 identity = λ{x} → identity x |
|
448
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
125 ; distr = λ {a} {b} {c} {f} {g} → distr1 {a} {b} {c} {f} {g} |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
126 ; ≈-cong = λ {a} {b} {c} {f} → ≈-cong {a} {b} {c} {f} |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
127 } |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
128 } where |
| 455 | 129 T = TwoCat {c₁} {c₂} |
| 130 fobj : Obj T → Obj A | |
| 131 fobj t0 = a | |
| 132 fobj t1 = b | |
| 133 fmap : {x y : Obj T } → (Hom T x y ) → Hom A (fobj x) (fobj y) | |
| 134 fmap {t0} {t0} id-t0 = id1 A a | |
| 135 fmap {t1} {t1} id-t1 = id1 A b | |
| 136 fmap {t0} {t1} arrow-f = f | |
| 137 fmap {t0} {t1} arrow-g = g | |
| 138 ≈-cong : {a : Obj T} {b : Obj T} {f g : Hom T a b} → T [ f ≈ g ] → A [ fmap f ≈ fmap g ] | |
| 139 ≈-cong {a} {b} {f} {.f} refl = let open ≈-Reasoning A in refl-hom | |
| 140 identity : (x : Obj T ) -> A [ fmap (id1 T x) ≈ id1 A (fobj x) ] | |
| 141 identity t0 = let open ≈-Reasoning A in refl-hom | |
| 142 identity t1 = let open ≈-Reasoning A in refl-hom | |
| 143 distr1 : {a : Obj T} {b : Obj T} {c : Obj T} {f : Hom T a b} {g : Hom T b c} → | |
| 144 A [ fmap (T [ g o f ]) ≈ A [ fmap g o fmap f ] ] | |
| 145 distr1 {a} {b} {c} {f} {g} with f | g | |
| 146 distr1 {t0} {t0} {t0} {f} {g} | id-t0 | id-t0 = let open ≈-Reasoning A in sym-hom idL | |
| 147 distr1 {t1} {t1} {t1} {f} {g} | id-t1 | id-t1 = let open ≈-Reasoning A in begin | |
| 148 id1 A b | |
| 149 ≈↑⟨ idL ⟩ | |
| 150 id1 A b o id1 A b | |
| 151 ∎ | |
| 152 distr1 {t0} {t0} {t1} {f} {g} | id-t0 | arrow-f = let open ≈-Reasoning A in begin | |
| 153 fmap (comp arrow-f id-t0) | |
| 154 ≈⟨⟩ | |
| 155 fmap arrow-f | |
| 156 ≈↑⟨ idR ⟩ | |
| 157 fmap arrow-f o id1 A a | |
| 158 ∎ | |
| 159 distr1 {t0} {t0} {t1} {f} {g} | id-t0 | arrow-g = let open ≈-Reasoning A in begin | |
| 160 fmap (comp arrow-g id-t0) | |
| 161 ≈⟨⟩ | |
| 162 fmap arrow-g | |
| 163 ≈↑⟨ idR ⟩ | |
| 164 fmap arrow-g o id1 A a | |
| 165 ∎ | |
| 166 distr1 {t0} {t1} {t1} {f} {g} | arrow-f | id-t1 = let open ≈-Reasoning A in begin | |
| 167 fmap (comp id-t1 arrow-f) | |
| 168 ≈⟨⟩ | |
| 169 fmap arrow-f | |
| 170 ≈↑⟨ idL ⟩ | |
| 171 id1 A b o fmap arrow-f | |
| 172 ∎ | |
| 173 distr1 {t0} {t1} {t1} {f} {g} | arrow-g | id-t1 = let open ≈-Reasoning A in begin | |
| 174 fmap (comp id-t1 arrow-g) | |
| 175 ≈⟨⟩ | |
| 176 fmap arrow-g | |
| 177 ≈↑⟨ idL ⟩ | |
| 178 id1 A b o fmap arrow-g | |
| 179 ∎ | |
|
448
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
180 |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
181 --- Equalizer |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
182 --- f |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
183 --- e -----→ |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
184 --- c -----→ a b |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
185 --- ^ / -----→ |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
186 --- |k h g |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
187 --- | / |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
188 --- | / ^ |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
189 --- | / | |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
190 --- |/ | Γ |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
191 --- d _ | |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
192 --- |\ | |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
193 --- \ K af |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
194 --- \ -----→ |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
195 --- \ t0 t1 |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
196 --- -----→ |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
197 --- ag |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
198 --- |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
199 --- |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
200 |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
201 open Complete |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
202 open Limit |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
203 open NTrans |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
204 |
| 455 | 205 equlimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A} -> (f g : Hom A a b) (comp : Complete A (TwoCat {c₁} {c₂} )) -> |
| 206 Hom A ( limit-c comp (indexFunctor {c₁} {c₂} {ℓ} A a b f g)) a | |
| 456 | 207 equlimit {c₁} {c₂} {ℓ} A {a} {b} f g comp = ? -- TMap (limit-u comp (indexFunctor {c₁} {c₂} {ℓ} A a b f g)) t0 |
|
448
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
208 |
| 455 | 209 lim-to-equ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) |
| 210 (comp : Complete A (TwoCat {c₁} {c₂} ) ) | |
|
448
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
211 → {a b : Obj A} (f g : Hom A a b ) |
| 455 | 212 → (fe=ge : A [ A [ f o (equlimit A f g comp ) ] ≈ A [ g o (equlimit A f g comp ) ] ] ) |
| 213 → IsEqualizer A (equlimit A f g comp ) f g | |
| 214 lim-to-equ {c₁} {c₂} {ℓ} A comp {a} {b} f g fe=ge = record { | |
| 215 fe=ge = fe=ge | |
|
448
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
216 ; k = λ {d} h fh=gh → k {d} h fh=gh |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
217 ; ek=h = λ {d} {h} {fh=gh} → ek=h d h fh=gh |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
218 ; uniqueness = λ {d} {h} {fh=gh} {k'} → uniquness d h fh=gh k' |
|
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
219 } where |
| 455 | 220 I = TwoCat {c₁} {c₂} |
|
448
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
221 Γ : Functor I A |
| 455 | 222 Γ = indexFunctor {c₁} {c₂} {ℓ} A a b f g |
| 223 c = limit-c comp Γ | |
| 224 k : {d : Obj A} (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c | |
| 456 | 225 nmap : (x : Obj I ) ( d : Obj (A) ) (h : Hom A d a ) → Hom A (FObj (K A I d) x) (FObj Γ x) |
| 226 nmap x d h with x | |
| 227 ... | t0 = h | |
| 228 ... | t1 = A [ f o h ] | |
| 229 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 ] ] | |
| 230 → A [ A [ FMap Γ f' o nmap x d h ] ≈ A [ nmap y d h o FMap (K A I d) f' ] ] | |
| 231 commute1 {x} {y} {f'} d h fh=gh with f' | |
| 232 commute1 {t0} {t1} {f'} d h fh=gh | arrow-f = let open ≈-Reasoning A in begin | |
| 233 f o h | |
| 234 ≈↑⟨ idR ⟩ | |
| 235 (f o h ) o id1 A d | |
| 236 ∎ | |
| 237 commute1 {t0} {t1} {f'} d h fh=gh | arrow-g = let open ≈-Reasoning A in begin | |
| 238 g o h | |
| 239 ≈↑⟨ fh=gh ⟩ | |
| 240 f o h | |
| 241 ≈↑⟨ idR ⟩ | |
| 242 (f o h ) o id1 A d | |
| 243 ∎ | |
| 244 commute1 {t0} {t0} {f'} d h fh=gh | id-t0 = let open ≈-Reasoning A in begin | |
| 245 id1 A a o h | |
| 246 ≈⟨ idL ⟩ | |
| 247 h | |
| 248 ≈↑⟨ idR ⟩ | |
| 249 h o id1 A d | |
| 250 ∎ | |
| 251 commute1 {t1} {t1} {f'} d h fh=gh | id-t1 = let open ≈-Reasoning A in begin | |
| 252 id1 A b o ( f o h ) | |
| 253 ≈⟨ idL ⟩ | |
| 254 f o h | |
| 255 ≈↑⟨ idR ⟩ | |
| 256 ( f o h ) o id1 A d | |
| 257 ∎ | |
| 258 nat1 : (d : Obj A) → (h : Hom A d a ) → A [ A [ f o h ] ≈ A [ g o h ] ] → NTrans I A (K A I d) Γ | |
| 259 nat1 d h fh=gh = record { | |
| 260 TMap = λ x → nmap x d h ; | |
| 261 isNTrans = record { | |
| 262 commute = λ {x} {y} {f'} → commute1 {x} {y} {f'} d h fh=gh | |
| 263 } | |
| 264 } | |
| 265 e = equlimit A f g comp | |
| 266 eqlim = isLimit comp Γ (nat1 c e fe=ge ) | |
| 267 k {d} h fh=gh = limit eqlim d (nat1 d h fh=gh ) | |
| 455 | 268 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 ] |
| 456 | 269 ek=h d h fh=gh = let open ≈-Reasoning A in begin |
| 270 e o k h fh=gh | |
| 271 ≈⟨ t0f=t eqlim {d} {nat1 d h fh=gh} {t0} ⟩ | |
| 272 h | |
| 273 ∎ | |
| 274 uniq-nat : {i : Obj I} → (d : Obj A ) (h : Hom A d a ) ( k' : Hom A d c ) | |
| 275 ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ]) → A [ A [ e o k' ] ≈ h ] → | |
| 276 A [ A [ TMap (nat1 c e fe=ge ) i o k' ] ≈ TMap (nat1 d h fh=gh) i ] | |
| 277 uniq-nat {t0} d h k' fh=gh ek'=h = let open ≈-Reasoning A in begin | |
| 278 (nmap t0 c e ) o k' | |
| 279 ≈⟨⟩ | |
| 280 e o k' | |
| 281 ≈⟨ ek'=h ⟩ | |
| 282 h | |
| 283 ≈⟨⟩ | |
| 284 nmap t0 d h | |
| 285 ∎ | |
| 286 uniq-nat {t1} d h k' fh=gh ek'=h = let open ≈-Reasoning A in begin | |
| 287 (nmap t1 c e ) o k' | |
| 288 ≈⟨⟩ | |
| 289 (f o e ) o k' | |
| 290 ≈↑⟨ assoc ⟩ | |
| 291 f o ( e o k' ) | |
| 292 ≈⟨ cdr ek'=h ⟩ | |
| 293 f o h | |
| 294 ≈⟨⟩ | |
| 295 TMap (nat1 d h fh=gh) t1 | |
| 296 ∎ | |
| 297 uniquness : (d : Obj A ) (h : Hom A d a ) → ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ] ) → | |
|
448
c2616de4d208
discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
298 ( k' : Hom A d c ) |
| 456 | 299 → A [ A [ e o k' ] ≈ h ] → A [ k h fh=gh ≈ k' ] |
| 300 uniquness d h fh=gh k' ek'=h = let open ≈-Reasoning A in begin | |
| 301 k h fh=gh | |
| 302 ≈⟨ limit-uniqueness eqlim k' ( λ{i} → uniq-nat {i} d h k' fh=gh ek'=h ) ⟩ | |
| 303 k' | |
| 304 ∎ | |
| 305 |