Mercurial > hg > Members > kono > Proof > category

comparison discrete.agda @ 778:06388660995b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix applicative for Agda version 2.5.4.1
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 26 Sep 2018 20:17:09 +0900
parents 4c0a955b651d
children 340708e8d54f
comparison
equal deleted inserted replaced
777:5160b431f1de 778:06388660995b
90 o-resp-≈ {c₁} {c₂} {a} {b} {c} {f} {.f} {h} {.h} refl refl = refl 90 o-resp-≈ {c₁} {c₂} {a} {b} {c} {f} {.f} {h} {.h} refl refl = refl
91 91
92 92
93 -- Category with no arrow but identity 93 -- Category with no arrow but identity
94 94
95 record DiscreteObj {c₁ : Level } (S : Set c₁) : Set c₁ where 95 record DiscreteHom { c₁ : Level} { S : Set c₁} (a : S) (b : S)
96 field
97 obj : S -- this is necessary to avoid single object
98
99 open DiscreteObj
100
101 record DiscreteHom { c₁ : Level} { S : Set c₁} (a : DiscreteObj {c₁} S) (b : DiscreteObj {c₁} S)
102 : Set c₁ where 96 : Set c₁ where
103 field 97 field
104 discrete : a ≡ b -- if f : a → b then a ≡ b 98 discrete : a ≡ b -- if f : a → b then a ≡ b
105 dom : DiscreteObj S 99 dom : S
106 dom = a 100 dom = a
107 101
108 open DiscreteHom 102 open DiscreteHom
109 103
110 _*_ : ∀ {c₁} → {S : Set c₁} {a b c : DiscreteObj {c₁} S} → DiscreteHom {c₁} b c → DiscreteHom {c₁} a b → DiscreteHom {c₁} a c 104 _*_ : ∀ {c₁} → {S : Set c₁} {a b c : S} → DiscreteHom {c₁} b c → DiscreteHom {c₁} a b → DiscreteHom {c₁} a c
111 _*_ {_} {a} {b} {c} x y = record {discrete = trans ( discrete y) (discrete x) } 105 _*_ {_} {a} {b} {c} x y = record {discrete = trans ( discrete y) (discrete x) }
112 106
113 DiscreteId : { c₁ : Level} { S : Set c₁} ( a : DiscreteObj {c₁} S ) → DiscreteHom {c₁} a a 107 DiscreteId : { c₁ : Level} { S : Set c₁} ( a : S ) → DiscreteHom {c₁} a a
114 DiscreteId a = record { discrete = refl } 108 DiscreteId a = record { discrete = refl }
115 109
116 open import Relation.Binary.PropositionalEquality 110 open import Relation.Binary.PropositionalEquality
117 111
118 assoc-* : {c₁ : Level } { S : Set c₁} {a b c d : DiscreteObj {c₁} S} 112 assoc-* : {c₁ : Level } { S : Set c₁} {a b c d : S}
119 {f : (DiscreteHom c d )} → {g : (DiscreteHom b c )} → {h : (DiscreteHom a b )} → 113 {f : (DiscreteHom c d )} → {g : (DiscreteHom b c )} → {h : (DiscreteHom a b )} →
120 dom ( f * (g * h)) ≡ dom ((f * g) * h ) 114 dom ( f * (g * h)) ≡ dom ((f * g) * h )
121 assoc-* {c₁} {S} {a} {b} {c} {d} {f} {g} {h } = refl 115 assoc-* {c₁} {S} {a} {b} {c} {d} {f} {g} {h } = refl
122 116
123 DiscreteCat : {c₁ : Level } → (S : Set c₁) → Category c₁ c₁ c₁ 117 DiscreteCat : {c₁ : Level } → (S : Set c₁) → Category c₁ c₁ c₁
124 DiscreteCat {c₁} S = record { 118 DiscreteCat {c₁} S = record {
125 Obj = DiscreteObj {c₁} S ; 119 Obj = S ;
126 Hom = λ a b → DiscreteHom {c₁} {S} a b ; 120 Hom = λ a b → DiscreteHom {c₁} {S} a b ;
127 _o_ = λ{a} {b} {c} x y → _*_ {c₁ } {S} {a} {b} {c} x y ; 121 _o_ = λ{a} {b} {c} x y → _*_ {c₁ } {S} {a} {b} {c} x y ;
128 _≈_ = λ x y → dom x ≡ dom y ; -- x ≡ y does not work because refl ≡ discrete f is failed as it should be 122 _≈_ = λ x y → dom x ≡ dom y ; -- x ≡ y does not work because refl ≡ discrete f is failed as it should be
129 Id = λ{a} → DiscreteId a ; 123 Id = λ{a} → DiscreteId a ;
130 isCategory = record { 124 isCategory = record {
133 identityR = λ{a b f} → identityR {a} {b} {f} ; 127 identityR = λ{a b f} → identityR {a} {b} {f} ;
134 o-resp-≈ = λ{a b c f g h i} → o-resp-≈ {a} {b} {c} {f} {g} {h} {i} ; 128 o-resp-≈ = λ{a b c f g h i} → o-resp-≈ {a} {b} {c} {f} {g} {h} {i} ;
135 associative = λ{a b c d f g h } → assoc-* { c₁} {S} {a} {b} {c} {d} {f} {g} {h} 129 associative = λ{a b c d f g h } → assoc-* { c₁} {S} {a} {b} {c} {d} {f} {g} {h}
136 } 130 }
137 } where 131 } where
138 identityL : {a b : DiscreteObj {c₁} S} {f : ( DiscreteHom {c₁} a b) } → dom ((DiscreteId b) * f) ≡ dom f 132 identityL : {a b : S} {f : ( DiscreteHom {c₁} a b) } → dom ((DiscreteId b) * f) ≡ dom f
139 identityL {a} {b} {f} = refl 133 identityL {a} {b} {f} = refl
140 identityR : {A B : DiscreteObj S} {f : ( DiscreteHom {c₁} A B) } → dom ( f * DiscreteId A ) ≡ dom f 134 identityR : {A B : S} {f : ( DiscreteHom {c₁} A B) } → dom ( f * DiscreteId A ) ≡ dom f
141 identityR {a} {b} {f} = refl 135 identityR {a} {b} {f} = refl
142 o-resp-≈ : {A B C : DiscreteObj S } {f g : ( DiscreteHom {c₁} A B)} {h i : ( DiscreteHom B C)} → 136 o-resp-≈ : {A B C : S } {f g : ( DiscreteHom {c₁} A B)} {h i : ( DiscreteHom B C)} →
143 dom f ≡ dom g → dom h ≡ dom i → dom ( h * f ) ≡ dom ( i * g ) 137 dom f ≡ dom g → dom h ≡ dom i → dom ( h * f ) ≡ dom ( i * g )
144 o-resp-≈ {a} {b} {c} {f} {g} {h} {i} refl refl = refl 138 o-resp-≈ {a} {b} {c} {f} {g} {h} {i} refl refl = refl
145 139
146 140
147 141