Mercurial > hg > Members > kono > Proof > category

comparison src/CCCGraph.agda @ 995:1d365952dde4

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 Sat, 06 Mar 2021 23:02:33 +0900
parents 485bc7560a75
children d89f2c8cf0f4
comparison
equal deleted inserted replaced
994:485bc7560a75 995:1d365952dde4
93 e4b = refl 93 e4b = refl
94 *-cong : {a b c : Obj Sets} {f f' : Hom Sets (a ∧ b) c} → 94 *-cong : {a b c : Obj Sets} {f f' : Hom Sets (a ∧ b) c} →
95 Sets [ f ≈ f' ] → Sets [ f * ≈ f' * ] 95 Sets [ f ≈ f' ] → Sets [ f * ≈ f' * ]
96 *-cong refl = refl 96 *-cong refl = refl
97 97
98 -- ○ b
99 -- b -----------→ 1
100 -- | |
101 -- m | | ⊤
102 -- ↓ char m ↓
103 -- a -----------→ Ω
104 -- h
105
98 data II {c : Level } : Set c where 106 data II {c : Level } : Set c where
99 true : II 107 true : II
100 false : II 108 false : II
101 109
102 data Tker {c : Level} {a : Set c} ( f : a → II {c} ) : Set c where 110 data Tker {c : Level} {a : Set c} ( f : a → II {c} ) : Set c where