Mercurial > hg > Members > kono > Proof > category

annotate discrete.agda @ 458:fd79b6d9f350

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix comment
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 02 Mar 2017 19:04:04 +0900
parents 0ba86e29f492
children 8436a018f88a
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
55a9b6177ed4 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 454
diff changeset
24 id-t0 : TwoHom t0 t0
55a9b6177ed4 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 454
diff changeset
25 id-t1 : TwoHom t1 t1
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
455
55a9b6177ed4 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 454
diff changeset
30 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
31 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
32 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
33 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
34 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
35 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
36 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
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 _×_ : ∀ {c₁ c₂} → {a b c : TwoObject {c₁}} → ( TwoHom {c₁} {c₂} b c ) → ( TwoHom {c₁} {c₂} a b ) → ( TwoHom {c₁} {c₂} a c )
455
55a9b6177ed4 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 454
diff changeset
41 _×_ {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
42
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 -- f g h
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 -- d <- c <- b <- a
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 --
455
55a9b6177ed4 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 454
diff changeset
47 -- It can be proved without TwoHom constraints
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 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
50 {f : (TwoHom {c₁} {c₂ } c d )} →
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51 {g : (TwoHom {c₁} {c₂ } b c )} →
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52 {h : (TwoHom {c₁} {c₂ } a b )} →
455
55a9b6177ed4 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 454
diff changeset
53 ( f × (g × h)) ≡ ((f × g) × h )
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 456
diff changeset
54 assoc-× {c₁} {c₂} {t0} {t0} {t0} {t0} { id-t0 }{ id-t0 }{ id-t0 } = refl
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 456
diff changeset
55 assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} { arrow-f }{ id-t0 }{ id-t0 } = refl
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 456
diff changeset
56 assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} { arrow-g }{ id-t0 }{ id-t0 } = refl
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 456
diff changeset
57 assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} { id-t1 }{ arrow-f }{ id-t0 } = refl
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 456
diff changeset
58 assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} { id-t1 }{ arrow-g }{ id-t0 } = refl
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 456
diff changeset
59 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
60 assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} { id-t1 }{ id-t1 }{ arrow-g } = refl
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 456
diff changeset
61 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
62
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
63 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
64 TwoId {_} {_} t0 = id-t0
55a9b6177ed4 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 454
diff changeset
65 TwoId {_} {_} t1 = id-t1
449
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
66
453
3c2ce4474d92 try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 451
diff changeset
67 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
68
455
55a9b6177ed4 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 454
diff changeset
69 TwoCat : {c₁ c₂ : Level } → Category c₁ c₂ c₂
55a9b6177ed4 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 454
diff changeset
70 TwoCat {c₁} {c₂} = record {
449
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
71 Obj = TwoObject {c₁} ;
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
72 Hom = λ a b → ( TwoHom {c₁} {c₂ } a b ) ;
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
73 _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
74 _≈_ = λ x y → x ≡ y ;
449
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
75 Id = λ{a} → TwoId {c₁ } { c₂} a ;
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
76 isCategory = record {
453
3c2ce4474d92 try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 451
diff changeset
77 isEquivalence = record {refl = refl ; trans = trans ; sym = sym } ;
449
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
78 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
79 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
80 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
81 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
82 }
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
83 } where
455
55a9b6177ed4 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 454
diff changeset
84 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
85 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
86 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
87 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
88 identityL {c₁} {c₂} {t0} {t1} { arrow-g } = refl
455
55a9b6177ed4 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 454
diff changeset
89 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
90 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
91 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
92 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
93 identityR {c₁} {c₂} {t0} {t1} { arrow-g } = refl
449
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
94 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
95 f ≡ g → h ≡ i → ( h × f ) ≡ ( i × g )
449
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
96 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
97 let open ≡-Reasoning in begin
455
55a9b6177ed4 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 454
diff changeset
98 ( h × f )
453
3c2ce4474d92 try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 451
diff changeset
99 ≡⟨ refl ⟩
455
55a9b6177ed4 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 454
diff changeset
100 comp (h) (f)
55a9b6177ed4 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 454
diff changeset
101 ≡⟨ cong (λ x → comp ( h ) x ) f==g ⟩
55a9b6177ed4 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 454
diff changeset
102 comp (h) (g)
55a9b6177ed4 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 454
diff changeset
103 ≡⟨ cong (λ x → comp x ( g ) ) h==i ⟩
55a9b6177ed4 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 454
diff changeset
104 comp (i) (g)
453
3c2ce4474d92 try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 451
diff changeset
105 ≡⟨ refl ⟩
455
55a9b6177ed4 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 454
diff changeset
106 ( i × g )
449
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
107 ∎
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
108