Mercurial > hg > Members > kono > Proof > category

annotate discrete.agda @ 466:44bd77c80555

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clean up
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 04 Mar 2017 16:57:58 +0900
parents 8436a018f88a
children c375d8f93a2c
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 data TwoObject {c₁ : Level} : Set c₁ where
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 t0 : TwoObject
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 t1 : TwoObject
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11
458
fd79b6d9f350 fix comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 457
diff changeset
12 ---
fd79b6d9f350 fix comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 457
diff changeset
13 --- two objects category ( for limit to equalizer proof )
448
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 ---
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 --- f
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 --- -----→
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 --- 0 1
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 --- -----→
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 --- g
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 456
diff changeset
20 --
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 456
diff changeset
21 -- missing arrows are constrainted by TwoHom data
448
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22
455
55a9b6177ed4 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 454
diff changeset
23 data TwoHom {c₁ c₂ : Level } : TwoObject {c₁} → TwoObject {c₁} → Set c₂ where
466
44bd77c80555 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 461
diff changeset
24 id-t0 : TwoHom t0 t0
44bd77c80555 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 461
diff changeset
25 id-t1 : TwoHom t1 t1
455
55a9b6177ed4 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 454
diff changeset
26 arrow-f : TwoHom t0 t1
55a9b6177ed4 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 454
diff changeset
27 arrow-g : TwoHom t0 t1
448
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29
461
8436a018f88a clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 458
diff changeset
30 _×_ : ∀ {c₁ c₂} → {a b c : TwoObject {c₁}} → TwoHom {c₁} {c₂} b c → TwoHom {c₁} {c₂} a b → TwoHom {c₁} {c₂} a c
466
44bd77c80555 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 461
diff changeset
31 _×_ {_} {_} {t0} {t1} {t1} id-t1 arrow-f = arrow-f
44bd77c80555 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 461
diff changeset
32 _×_ {_} {_} {t0} {t1} {t1} id-t1 arrow-g = arrow-g
44bd77c80555 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 461
diff changeset
33 _×_ {_} {_} {t1} {t1} {t1} id-t1 id-t1 = id-t1
44bd77c80555 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 461
diff changeset
34 _×_ {_} {_} {t0} {t0} {t1} arrow-f id-t0 = arrow-f
44bd77c80555 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 461
diff changeset
35 _×_ {_} {_} {t0} {t0} {t1} arrow-g id-t0 = arrow-g
44bd77c80555 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 461
diff changeset
36 _×_ {_} {_} {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
37
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 open TwoHom
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 -- f g h
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 -- d <- c <- b <- a
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 --
455
55a9b6177ed4 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 454
diff changeset
43 -- It can be proved without TwoHom constraints
448
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 assoc-× : {c₁ c₂ : Level } {a b c d : TwoObject {c₁} }
466
44bd77c80555 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 461
diff changeset
46 {f : (TwoHom {c₁} {c₂ } c d )} → {g : (TwoHom b c )} → {h : (TwoHom a b )} →
455
55a9b6177ed4 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 454
diff changeset
47 ( f × (g × h)) ≡ ((f × g) × h )
466
44bd77c80555 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 461
diff changeset
48 assoc-× {c₁} {c₂} {t0} {t0} {t0} {t0} { id-t0 }{ id-t0 }{ id-t0 } = refl
44bd77c80555 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 461
diff changeset
49 assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} { arrow-f }{ id-t0 }{ id-t0 } = refl
44bd77c80555 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 461
diff changeset
50 assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} { arrow-g }{ id-t0 }{ id-t0 } = refl
44bd77c80555 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 461
diff changeset
51 assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} { id-t1 }{ arrow-f }{ id-t0 } = refl
44bd77c80555 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 461
diff changeset
52 assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} { id-t1 }{ arrow-g }{ id-t0 } = refl
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 456
diff changeset
53 assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} { id-t1 }{ id-t1 }{ arrow-f } = refl
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 456
diff changeset
54 assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} { id-t1 }{ id-t1 }{ arrow-g } = refl
466
44bd77c80555 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 461
diff changeset
55 assoc-× {c₁} {c₂} {t1} {t1} {t1} {t1} { id-t1 }{ id-t1 }{ id-t1 } = refl
449
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
56
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
57 TwoId : {c₁ c₂ : Level } (a : TwoObject {c₁} ) → (TwoHom {c₁} {c₂ } a a )
455
55a9b6177ed4 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 454
diff changeset
58 TwoId {_} {_} t0 = id-t0
55a9b6177ed4 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 454
diff changeset
59 TwoId {_} {_} t1 = id-t1
449
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
60
466
44bd77c80555 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 461
diff changeset
61 open import Relation.Binary.PropositionalEquality
453
3c2ce4474d92 try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 451
diff changeset
62
455
55a9b6177ed4 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 454
diff changeset
63 TwoCat : {c₁ c₂ : Level } → Category c₁ c₂ c₂
55a9b6177ed4 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 454
diff changeset
64 TwoCat {c₁} {c₂} = record {
461
8436a018f88a clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 458
diff changeset
65 Obj = TwoObject ;
8436a018f88a clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 458
diff changeset
66 Hom = λ a b → TwoHom a b ;
449
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
67 _o_ = λ{a} {b} {c} x y → _×_ {c₁ } { c₂} {a} {b} {c} x y ;
455
55a9b6177ed4 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 454
diff changeset
68 _≈_ = λ x y → x ≡ y ;
461
8436a018f88a clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 458
diff changeset
69 Id = λ{a} → TwoId a ;
449
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
70 isCategory = record {
453
3c2ce4474d92 try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 451
diff changeset
71 isEquivalence = record {refl = refl ; trans = trans ; sym = sym } ;
449
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
72 identityL = λ{a b f} → identityL {c₁} {c₂ } {a} {b} {f} ;
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
73 identityR = λ{a b f} → identityR {c₁} {c₂ } {a} {b} {f} ;
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
74 o-resp-≈ = λ{a b c f g h i} → o-resp-≈ {c₁} {c₂ } {a} {b} {c} {f} {g} {h} {i} ;
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
75 associative = λ{a b c d f g h } → assoc-× {c₁} {c₂} {a} {b} {c} {d} {f} {g} {h}
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
76 }
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
77 } where
455
55a9b6177ed4 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 454
diff changeset
78 identityL : {c₁ c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁} {c₂ } A B) } → ((TwoId B) × f) ≡ f
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 456
diff changeset
79 identityL {c₁} {c₂} {t1} {t1} { id-t1 } = refl
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 456
diff changeset
80 identityL {c₁} {c₂} {t0} {t0} { id-t0 } = refl
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 456
diff changeset
81 identityL {c₁} {c₂} {t0} {t1} { arrow-f } = refl
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 456
diff changeset
82 identityL {c₁} {c₂} {t0} {t1} { arrow-g } = refl
455
55a9b6177ed4 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 454
diff changeset
83 identityR : {c₁ c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁} {c₂ } A B) } → ( f × TwoId A ) ≡ f
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 456
diff changeset
84 identityR {c₁} {c₂} {t1} {t1} { id-t1 } = refl
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 456
diff changeset
85 identityR {c₁} {c₂} {t0} {t0} { id-t0 } = refl
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 456
diff changeset
86 identityR {c₁} {c₂} {t0} {t1} { arrow-f } = refl
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 456
diff changeset
87 identityR {c₁} {c₂} {t0} {t1} { arrow-g } = refl
449
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
88 o-resp-≈ : {c₁ c₂ : Level } {A B C : TwoObject {c₁} } {f g : ( TwoHom {c₁} {c₂ } A B)} {h i : ( TwoHom B C)} →
455
55a9b6177ed4 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 454
diff changeset
89 f ≡ g → h ≡ i → ( h × f ) ≡ ( i × g )
461
8436a018f88a clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 458
diff changeset
90 o-resp-≈ {c₁} {c₂} {a} {b} {c} {f} {.f} {h} {.h} refl refl = refl