Mercurial > hg > Members > kono > Proof > category

comparison discrete.agda @ 474:2d32ded94aaf

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 Tue, 07 Mar 2017 08:27:33 +0900
parents f3d6d0275a0a
children 4c0a955b651d
comparison
equal deleted inserted replaced
472:f3d6d0275a0a 474:2d32ded94aaf
99 open DiscreteObj 99 open DiscreteObj
100 100
101 record DiscreteHom { c₁ : Level} { S : Set c₁} (a : DiscreteObj {c₁} S) (b : DiscreteObj {c₁} S) 101 record DiscreteHom { c₁ : Level} { S : Set c₁} (a : DiscreteObj {c₁} S) (b : DiscreteObj {c₁} S)
102 : Set c₁ where 102 : Set c₁ where
103 field 103 field
104 discrete : a ≡ b 104 discrete : a ≡ b -- if f : a → b then a ≡ b
105 dom : DiscreteObj S 105 dom : DiscreteObj S
106 dom = a 106 dom = a
107 107
108 open DiscreteHom 108 open DiscreteHom
109 109
123 DiscreteCat : {c₁ : Level } → (S : Set c₁) → Category c₁ c₁ c₁ 123 DiscreteCat : {c₁ : Level } → (S : Set c₁) → Category c₁ c₁ c₁
124 DiscreteCat {c₁} S = record { 124 DiscreteCat {c₁} S = record {
125 Obj = DiscreteObj {c₁} S ; 125 Obj = DiscreteObj {c₁} S ;
126 Hom = λ a b → DiscreteHom {c₁} {S} a b ; 126 Hom = λ a b → DiscreteHom {c₁} {S} a b ;
127 _o_ = λ{a} {b} {c} x y → _*_ {c₁ } {S} {a} {b} {c} x y ; 127 _o_ = λ{a} {b} {c} x y → _*_ {c₁ } {S} {a} {b} {c} x y ;
128 _≈_ = λ x y → dom x ≡ dom y ; 128 _≈_ = λ 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 ; 129 Id = λ{a} → DiscreteId a ;
130 isCategory = record { 130 isCategory = record {
131 isEquivalence = record {refl = refl ; trans = trans ; sym = sym } ; 131 isEquivalence = record {refl = refl ; trans = trans ; sym = sym } ;
132 identityL = λ{a b f} → identityL {a} {b} {f} ; 132 identityL = λ{a b f} → identityL {a} {b} {f} ;
133 identityR = λ{a b f} → identityR {a} {b} {f} ; 133 identityR = λ{a b f} → identityR {a} {b} {f} ;