Mercurial > hg > Members > kono > Proof > category

comparison deductive.agda @ 799:82a8c1ab4ef5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
graph to category
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 23 Apr 2019 11:30:34 +0900
parents 6e6c7ad8ea1c
children 6c5cfb9b333e 8c2da34e8dc1
comparison
equal deleted inserted replaced
798:6e6c7ad8ea1c 799:82a8c1ab4ef5
16 π' : {a b : Obj A } → Hom A (a ∧ b) b 16 π' : {a b : Obj A } → Hom A (a ∧ b) b
17 _<=_ : (a b : Obj A ) → Obj A 17 _<=_ : (a b : Obj A ) → Obj A
18 _* : {a b c : Obj A } → Hom A (a ∧ b) c → Hom A a (c <= b) 18 _* : {a b c : Obj A } → Hom A (a ∧ b) c → Hom A a (c <= b)
19 ε : {a b : Obj A } → Hom A ((a <= b ) ∧ b) a 19 ε : {a b : Obj A } → Hom A ((a <= b ) ∧ b) a
20 20
21 module ccc-from-graph ( Atom : Set ) ( Hom : Atom → Atom → Set ) where
22
23 open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong )
24
25 data Objs : Set where
26 ⊤ : Objs
27 atom : Atom → Objs
28 _∧_ : Objs → Objs → Objs
29 _<=_ : Objs → Objs → Objs
30
31 data Arrow : Objs → Objs → Set where
32 hom : (a b : Atom) → Hom a b → Arrow (atom a) (atom b)
33 id : (a : Objs ) → Arrow a a
34 _・_ : {a b c : Objs } → Arrow b c → Arrow a b → Arrow a c
35 ○ : (a : Objs ) → Arrow a ⊤
36 π : {a b : Objs } → Arrow ( a ∧ b ) a
37 π' : {a b : Objs } → Arrow ( a ∧ b ) b
38 <_,_> : {a b c : Objs } → Arrow c a → Arrow c b → Arrow c (a ∧ b)
39 ε : {a b : Objs } → Arrow ((a <= b) ∧ b ) a
40 _* : {a b c : Objs } → Arrow (c ∧ b ) a → Arrow c ( a <= b )
41
42 record GraphCat : Set where
43 field
44 identityL : {a b : Objs} {f : Arrow a b } → (id b ・ f) ≡ f
45 identityR : {a b : Objs} {f : Arrow a b } → (f ・ id a) ≡ f
46 resp : {a b c : Objs} {f g : Arrow a b } {h i : Arrow b c } → f ≡ g → h ≡ i → (h ・ f) ≡ (i ・ g)
47 associative : {a b c d : Objs} {f : Arrow c d }{g : Arrow b c }{h : Arrow a b } → (f ・ (g ・ h)) ≡ ((f ・ g) ・ h)
48
49
50 GLCat : GraphCat → Category Level.zero Level.zero Level.zero
51 GLCat gc = record {
52 Obj = Objs ;
53 Hom = λ a b → Arrow a b ;
54 _o_ = _・_ ; -- λ{a} {b} {c} x y → ; -- _×_ {c₁ } { c₂} {a} {b} {c} x y ;
55 _≈_ = λ x y → x ≡ y ;
56 Id = λ{a} → id a ;
57 isCategory = record {
58 isEquivalence = record {refl = refl ; trans = trans ; sym = sym }
59 ; identityL = λ{a b f} → GraphCat.identityL gc
60 ; identityR = λ{a b f} → GraphCat.identityR gc
61 ; o-resp-≈ = λ {a b c f g h i} f=g h=i → GraphCat.resp gc f=g h=i
62 ; associative = λ{a b c d f g h } → GraphCat.associative gc
63 }
64 }
65
66 GL : (gc : GraphCat ) → PositiveLogic (GLCat gc )
67 GL _ = record {
68 ⊤ = ⊤
69 ; ○ = ○
70 ; _∧_ = _∧_
71 ; <_,_> = <_,_>
72 ; π = π
73 ; π' = π'
74 ; _<=_ = _<=_
75 ; _* = _*
76 ; ε = ε
77 }
78 21
79 module deduction-theorem ( L : PositiveLogic A ) where 22 module deduction-theorem ( L : PositiveLogic A ) where
80 23
81 open PositiveLogic L 24 open PositiveLogic L
82 _・_ = _[_o_] A 25 _・_ = _[_o_] A