Mercurial > hg > Members > kono > Proof > category

annotate discrete.agda @ 817:177162990879

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 28 Apr 2019 12:37:34 +0900
parents 4ff300e1e98c
children fbbc9c03bfed
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
781
340708e8d54f fix for 2.5.4.2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 778
diff changeset
7 open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym )
340708e8d54f fix for 2.5.4.2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 778
diff changeset
8
817
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 812
diff changeset
9 record Graph { v : Level } : Set (suc v) where
803
984d20c10c87 simpler graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 799
diff changeset
10 field
817
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 812
diff changeset
11 vertex : Set v
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 812
diff changeset
12 edge : vertex → vertex → Set v
799
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
13
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
14 module graphtocat where
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
15
803
984d20c10c87 simpler graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 799
diff changeset
16 open import Relation.Binary.PropositionalEquality
799
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
17
817
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 812
diff changeset
18 data Chain { v : Level } ( g : Graph {v} ) : ( a b : Graph.vertex g ) → Set v where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 812
diff changeset
19 id : ( a : Graph.vertex g ) → Chain g a a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 812
diff changeset
20 next : { a b c : Graph.vertex g } → (Graph.edge g b c ) → Chain g a b → Chain g a c
799
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
21
817
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 812
diff changeset
22 _・_ : {v : Level} { G : Graph {v} } {a b c : Graph.vertex G } (f : Chain G b c ) → (g : Chain G a b) → Chain G a c
809
0976d576f5f6 <_,_> as function on Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 806
diff changeset
23 id _ ・ f = f
0976d576f5f6 <_,_> as function on Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 806
diff changeset
24 (next x f) ・ g = next x ( f ・ g )
806
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 804
diff changeset
25
817
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 812
diff changeset
26 GraphtoCat : {v : Level} (G : Graph {v} ) → Category v v v
803
984d20c10c87 simpler graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 799
diff changeset
27 GraphtoCat G = record {
804
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 803
diff changeset
28 Obj = Graph.vertex G ;
817
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 812
diff changeset
29 Hom = λ a b → Chain G a b ;
809
0976d576f5f6 <_,_> as function on Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 806
diff changeset
30 _o_ = λ{a} {b} {c} x y → x ・ y ;
799
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
31 _≈_ = λ x y → x ≡ y ;
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
32 Id = λ{a} → id a ;
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
33 isCategory = record {
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
34 isEquivalence = record {refl = refl ; trans = trans ; sym = sym } ;
803
984d20c10c87 simpler graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 799
diff changeset
35 identityL = identityL;
984d20c10c87 simpler graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 799
diff changeset
36 identityR = identityR ;
984d20c10c87 simpler graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 799
diff changeset
37 o-resp-≈ = o-resp-≈ ;
984d20c10c87 simpler graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 799
diff changeset
38 associative = λ{a b c d f g h } → associative f g h
799
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
39 }
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
40 } where
803
984d20c10c87 simpler graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 799
diff changeset
41 open Chain
804
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 803
diff changeset
42 obj = Graph.vertex G
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 803
diff changeset
43 hom = Graph.edge G
803
984d20c10c87 simpler graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 799
diff changeset
44
817
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 812
diff changeset
45 identityL : {A B : Graph.vertex G} {f : Chain G A B} → (id B ・ f) ≡ f
803
984d20c10c87 simpler graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 799
diff changeset
46 identityL = refl
817
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 812
diff changeset
47 identityR : {A B : Graph.vertex G} {f : Chain G A B} → (f ・ id A) ≡ f
803
984d20c10c87 simpler graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 799
diff changeset
48 identityR {a} {_} {id a} = refl
984d20c10c87 simpler graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 799
diff changeset
49 identityR {a} {b} {next x f} = cong ( λ k → next x k ) ( identityR {_} {_} {f} )
817
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 812
diff changeset
50 o-resp-≈ : {A B C : Graph.vertex G} {f g : Chain G A B} {h i : Chain G B C} →
809
0976d576f5f6 <_,_> as function on Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 806
diff changeset
51 f ≡ g → h ≡ i → (h ・ f) ≡ (i ・ g)
803
984d20c10c87 simpler graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 799
diff changeset
52 o-resp-≈ refl refl = refl
817
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 812
diff changeset
53 associative : {a b c d : Graph.vertex G} (f : Chain G c d) (g : Chain G b c) (h : Chain G a b) →
809
0976d576f5f6 <_,_> as function on Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 806
diff changeset
54 (f ・ (g ・ h)) ≡ ((f ・ g) ・ h)
803
984d20c10c87 simpler graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 799
diff changeset
55 associative (id a) g h = refl
984d20c10c87 simpler graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 799
diff changeset
56 associative (next x f) g h = cong ( λ k → next x k ) ( associative f g h )
984d20c10c87 simpler graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 799
diff changeset
57
799
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
58
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
59
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
60 data TwoObject : Set where
448
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
61 t0 : TwoObject
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62 t1 : TwoObject
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63
458
fd79b6d9f350 fix comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 457
diff changeset
64 ---
fd79b6d9f350 fix comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 457
diff changeset
65 --- 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
66 ---
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
67 --- f
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
68 --- -----→
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69 --- 0 1
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
70 --- -----→
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
71 --- g
457
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 456
diff changeset
72 --
0ba86e29f492 limit-to and discrete clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 456
diff changeset
73 -- missing arrows are constrainted by TwoHom data
448
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
74
799
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
75 data TwoHom : TwoObject → TwoObject → Set where
466
44bd77c80555 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 461
diff changeset
76 id-t0 : TwoHom t0 t0
44bd77c80555 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 461
diff changeset
77 id-t1 : TwoHom t1 t1
455
55a9b6177ed4 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 454
diff changeset
78 arrow-f : TwoHom t0 t1
55a9b6177ed4 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 454
diff changeset
79 arrow-g : TwoHom t0 t1
448
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
80
799
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
81 TwoCat' : Category Level.zero Level.zero Level.zero
804
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 803
diff changeset
82 TwoCat' = GraphtoCat ( record { vertex = TwoObject ; edge = TwoHom } )
799
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
83 where open graphtocat
448
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
84
799
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
85 _×_ : {a b c : TwoObject } → TwoHom b c → TwoHom a b → TwoHom a c
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
86 _×_ {t0} {t1} {t1} id-t1 arrow-f = arrow-f
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
87 _×_ {t0} {t1} {t1} id-t1 arrow-g = arrow-g
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
88 _×_ {t1} {t1} {t1} id-t1 id-t1 = id-t1
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
89 _×_ {t0} {t0} {t1} arrow-f id-t0 = arrow-f
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
90 _×_ {t0} {t0} {t1} arrow-g id-t0 = arrow-g
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
91 _×_ {t0} {t0} {t0} id-t0 id-t0 = id-t0
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
92
448
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
93
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
94 open TwoHom
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
95
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
96 -- f g h
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
97 -- d <- c <- b <- a
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
98 --
455
55a9b6177ed4 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 454
diff changeset
99 -- It can be proved without TwoHom constraints
448
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
100
799
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
101 assoc-× : {a b c d : TwoObject }
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
102 {f : (TwoHom 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
103 ( f × (g × h)) ≡ ((f × g) × h )
799
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
104 assoc-× {t0} {t0} {t0} {t0} { id-t0 }{ id-t0 }{ id-t0 } = refl
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
105 assoc-× {t0} {t0} {t0} {t1} { arrow-f }{ id-t0 }{ id-t0 } = refl
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
106 assoc-× {t0} {t0} {t0} {t1} { arrow-g }{ id-t0 }{ id-t0 } = refl
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
107 assoc-× {t0} {t0} {t1} {t1} { id-t1 }{ arrow-f }{ id-t0 } = refl
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
108 assoc-× {t0} {t0} {t1} {t1} { id-t1 }{ arrow-g }{ id-t0 } = refl
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
109 assoc-× {t0} {t1} {t1} {t1} { id-t1 }{ id-t1 }{ arrow-f } = refl
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
110 assoc-× {t0} {t1} {t1} {t1} { id-t1 }{ id-t1 }{ arrow-g } = refl
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
111 assoc-× {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
112
799
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
113 TwoId : (a : TwoObject ) → (TwoHom a a )
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
114 TwoId t0 = id-t0
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
115 TwoId t1 = id-t1
449
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
116
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 466
diff changeset
117 open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong )
453
3c2ce4474d92 try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 451
diff changeset
118
799
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
119 TwoCat : Category Level.zero Level.zero Level.zero
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
120 TwoCat = record {
461
8436a018f88a clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 458
diff changeset
121 Obj = TwoObject ;
8436a018f88a clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 458
diff changeset
122 Hom = λ a b → TwoHom a b ;
455
55a9b6177ed4 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 454
diff changeset
123 _≈_ = λ x y → x ≡ y ;
461
8436a018f88a clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 458
diff changeset
124 Id = λ{a} → TwoId a ;
449
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
125 isCategory = record {
453
3c2ce4474d92 try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 451
diff changeset
126 isEquivalence = record {refl = refl ; trans = trans ; sym = sym } ;
799
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
127 identityL = λ{a b f} → identityL {a} {b} {f} ;
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
128 identityR = λ{a b f} → identityR {a} {b} {f} ;
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
129 o-resp-≈ = λ{a b c f g h i} → o-resp-≈ {a} {b} {c} {f} {g} {h} {i} ;
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
130 associative = λ{a b c d f g h } → assoc-× {a} {b} {c} {d} {f} {g} {h}
449
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
131 }
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
132 } where
799
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
133 identityL : {A B : TwoObject } {f : ( TwoHom A B) } → ((TwoId B) × f) ≡ f
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
134 identityL {t1} {t1} { id-t1 } = refl
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
135 identityL {t0} {t0} { id-t0 } = refl
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
136 identityL {t0} {t1} { arrow-f } = refl
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
137 identityL {t0} {t1} { arrow-g } = refl
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
138 identityR : {A B : TwoObject } {f : ( TwoHom A B) } → ( f × TwoId A ) ≡ f
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
139 identityR {t1} {t1} { id-t1 } = refl
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
140 identityR {t0} {t0} { id-t0 } = refl
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
141 identityR {t0} {t1} { arrow-f } = refl
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
142 identityR {t0} {t1} { arrow-g } = refl
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
143 o-resp-≈ : {A B C : TwoObject } {f g : ( TwoHom A B)} {h i : ( TwoHom B C)} →
455
55a9b6177ed4 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 454
diff changeset
144 f ≡ g → h ≡ i → ( h × f ) ≡ ( i × g )
799
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
145 o-resp-≈ {a} {b} {c} {f} {.f} {h} {.h} refl refl = refl
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 466
diff changeset
146
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 466
diff changeset
147
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 466
diff changeset
148 -- Category with no arrow but identity
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 466
diff changeset
149
799
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
150
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
151 open import Data.Empty
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
152
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
153 DiscreteCat' : (S : Set) → Category Level.zero Level.zero Level.zero
804
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 803
diff changeset
154 DiscreteCat' S = GraphtoCat ( record { vertex = S ; edge = ( λ _ _ → ⊥ ) } )
799
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
155 where open graphtocat
82a8c1ab4ef5 graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
156
778
06388660995b fix applicative for Agda version 2.5.4.1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 475
diff changeset
157 record DiscreteHom { c₁ : Level} { S : Set c₁} (a : S) (b : S)
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 466
diff changeset
158 : Set c₁ where
469
65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 468
diff changeset
159 field
474
2d32ded94aaf clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 472
diff changeset
160 discrete : a ≡ b -- if f : a → b then a ≡ b
778
06388660995b fix applicative for Agda version 2.5.4.1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 475
diff changeset
161 dom : S
472
f3d6d0275a0a discrete equality as a dom equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 469
diff changeset
162 dom = a
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 466
diff changeset
163
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 466
diff changeset
164 open DiscreteHom
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 466
diff changeset
165
778
06388660995b fix applicative for Agda version 2.5.4.1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 475
diff changeset
166 _*_ : ∀ {c₁} → {S : Set c₁} {a b c : S} → DiscreteHom {c₁} b c → DiscreteHom {c₁} a b → DiscreteHom {c₁} a c
469
65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 468
diff changeset
167 _*_ {_} {a} {b} {c} x y = record {discrete = trans ( discrete y) (discrete x) }
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 466
diff changeset
168
778
06388660995b fix applicative for Agda version 2.5.4.1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 475
diff changeset
169 DiscreteId : { c₁ : Level} { S : Set c₁} ( a : S ) → DiscreteHom {c₁} a a
469
65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 468
diff changeset
170 DiscreteId a = record { discrete = refl }
65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 468
diff changeset
171
65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 468
diff changeset
172 open import Relation.Binary.PropositionalEquality
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 466
diff changeset
173
778
06388660995b fix applicative for Agda version 2.5.4.1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 475
diff changeset
174 assoc-* : {c₁ : Level } { S : Set c₁} {a b c d : S}
469
65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 468
diff changeset
175 {f : (DiscreteHom c d )} → {g : (DiscreteHom b c )} → {h : (DiscreteHom a b )} →
472
f3d6d0275a0a discrete equality as a dom equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 469
diff changeset
176 dom ( f * (g * h)) ≡ dom ((f * g) * h )
f3d6d0275a0a discrete equality as a dom equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 469
diff changeset
177 assoc-* {c₁} {S} {a} {b} {c} {d} {f} {g} {h } = refl
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 466
diff changeset
178
469
65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 468
diff changeset
179 DiscreteCat : {c₁ : Level } → (S : Set c₁) → Category c₁ c₁ c₁
65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 468
diff changeset
180 DiscreteCat {c₁} S = record {
778
06388660995b fix applicative for Agda version 2.5.4.1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 475
diff changeset
181 Obj = S ;
469
65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 468
diff changeset
182 Hom = λ a b → DiscreteHom {c₁} {S} a b ;
65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 468
diff changeset
183 _o_ = λ{a} {b} {c} x y → _*_ {c₁ } {S} {a} {b} {c} x y ;
474
2d32ded94aaf clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 472
diff changeset
184 _≈_ = λ x y → dom x ≡ dom y ; -- x ≡ y does not work because refl ≡ discrete f is failed as it should be
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 466
diff changeset
185 Id = λ{a} → DiscreteId a ;
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 466
diff changeset
186 isCategory = record {
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 466
diff changeset
187 isEquivalence = record {refl = refl ; trans = trans ; sym = sym } ;
469
65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 468
diff changeset
188 identityL = λ{a b f} → identityL {a} {b} {f} ;
65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 468
diff changeset
189 identityR = λ{a b f} → identityR {a} {b} {f} ;
65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 468
diff changeset
190 o-resp-≈ = λ{a b c f g h i} → o-resp-≈ {a} {b} {c} {f} {g} {h} {i} ;
65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 468
diff changeset
191 associative = λ{a b c d f g h } → assoc-* { c₁} {S} {a} {b} {c} {d} {f} {g} {h}
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 466
diff changeset
192 }
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 466
diff changeset
193 } where
778
06388660995b fix applicative for Agda version 2.5.4.1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 475
diff changeset
194 identityL : {a b : S} {f : ( DiscreteHom {c₁} a b) } → dom ((DiscreteId b) * f) ≡ dom f
472
f3d6d0275a0a discrete equality as a dom equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 469
diff changeset
195 identityL {a} {b} {f} = refl
778
06388660995b fix applicative for Agda version 2.5.4.1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 475
diff changeset
196 identityR : {A B : S} {f : ( DiscreteHom {c₁} A B) } → dom ( f * DiscreteId A ) ≡ dom f
472
f3d6d0275a0a discrete equality as a dom equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 469
diff changeset
197 identityR {a} {b} {f} = refl
778
06388660995b fix applicative for Agda version 2.5.4.1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 475
diff changeset
198 o-resp-≈ : {A B C : S } {f g : ( DiscreteHom {c₁} A B)} {h i : ( DiscreteHom B C)} →
472
f3d6d0275a0a discrete equality as a dom equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 469
diff changeset
199 dom f ≡ dom g → dom h ≡ dom i → dom ( h * f ) ≡ dom ( i * g )
f3d6d0275a0a discrete equality as a dom equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 469
diff changeset
200 o-resp-≈ {a} {b} {c} {f} {g} {h} {i} refl refl = refl
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 466
diff changeset
201
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 466
diff changeset
202
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 466
diff changeset
203
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 466
diff changeset
204
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 466
diff changeset
205
472
f3d6d0275a0a discrete equality as a dom equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 469
diff changeset
206