Mercurial > hg > Members > kono > Proof > category
annotate deductive.agda @ 798:6e6c7ad8ea1c
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 23 Apr 2019 06:39:24 +0900 |
| parents | f37f11e1b871 |
| children | 82a8c1ab4ef5 |
| rev | line source |
|---|---|
|
792
5bee48f7c126
deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
791
diff
changeset
|
1 open import Level |
|
5bee48f7c126
deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
791
diff
changeset
|
2 open import Category |
|
5bee48f7c126
deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
791
diff
changeset
|
3 module deductive {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) where |
| 791 | 4 |
| 5 -- Deduction Theorem | |
| 6 | |
|
792
5bee48f7c126
deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
791
diff
changeset
|
7 -- positive logic |
| 791 | 8 |
|
792
5bee48f7c126
deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
791
diff
changeset
|
9 record PositiveLogic {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where |
|
5bee48f7c126
deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
791
diff
changeset
|
10 field |
|
5bee48f7c126
deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
791
diff
changeset
|
11 ⊤ : Obj A |
|
5bee48f7c126
deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
791
diff
changeset
|
12 ○ : (a : Obj A ) → Hom A a ⊤ |
|
5bee48f7c126
deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
791
diff
changeset
|
13 _∧_ : Obj A → Obj A → Obj A |
|
5bee48f7c126
deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
791
diff
changeset
|
14 <_,_> : {a b c : Obj A } → Hom A c a → Hom A c b → Hom A c (a ∧ b) |
|
5bee48f7c126
deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
791
diff
changeset
|
15 π : {a b : Obj A } → Hom A (a ∧ b) a |
|
5bee48f7c126
deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
791
diff
changeset
|
16 π' : {a b : Obj A } → Hom A (a ∧ b) b |
|
5bee48f7c126
deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
791
diff
changeset
|
17 _<=_ : (a b : Obj A ) → Obj A |
|
5bee48f7c126
deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
791
diff
changeset
|
18 _* : {a b c : Obj A } → Hom A (a ∧ b) c → Hom A a (c <= b) |
|
5bee48f7c126
deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
791
diff
changeset
|
19 ε : {a b : Obj A } → Hom A ((a <= b ) ∧ b) a |
|
5bee48f7c126
deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
791
diff
changeset
|
20 |
| 798 | 21 module ccc-from-graph ( Atom : Set ) ( Hom : Atom → Atom → Set ) where |
| 22 | |
| 23 open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong ) | |
|
792
5bee48f7c126
deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
791
diff
changeset
|
24 |
| 798 | 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 ) | |
| 791 | 41 |
| 798 | 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 | |
| 791 | 49 |
| 798 | 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 } | |
| 791 | 78 |
| 798 | 79 module deduction-theorem ( L : PositiveLogic A ) where |
| 791 | 80 |
| 798 | 81 open PositiveLogic L |
| 82 _・_ = _[_o_] A | |
| 83 | |
| 84 -- every proof b → c with assumption a has following forms | |
| 85 | |
| 86 data φ {a : Obj A } ( x : Hom A ⊤ a ) : {b c : Obj A } → Hom A b c → Set ( c₁ ⊔ c₂ ) where | |
| 87 i : {b c : Obj A} {k : Hom A b c } → φ x k | |
| 88 ii : φ x {⊤} {a} x | |
| 89 iii : {b c' c'' : Obj A } { f : Hom A b c' } { g : Hom A b c'' } (ψ : φ x f ) (χ : φ x g ) → φ x {b} {c' ∧ c''} < f , g > | |
| 90 iv : {b c d : Obj A } { f : Hom A d c } { g : Hom A b d } (ψ : φ x f ) (χ : φ x g ) → φ x ( f ・ g ) | |
| 91 v : {b c' c'' : Obj A } { f : Hom A (b ∧ c') c'' } (ψ : φ x f ) → φ x {b} {c'' <= c'} ( f * ) | |
| 92 | |
| 93 α : {a b c : Obj A } → Hom A (( a ∧ b ) ∧ c ) ( a ∧ ( b ∧ c ) ) | |
| 94 α = < π ・ π , < π' ・ π , π' > > | |
| 95 | |
| 96 -- genetate (a ∧ b) → c proof from proof b → c with assumption a | |
| 97 | |
| 98 kx∈a : {a b c : Obj A } → ( x : Hom A ⊤ a ) → {z : Hom A b c } → ( y : φ {a} x z ) → Hom A (a ∧ b) c | |
| 99 kx∈a x {k} i = k ・ π' | |
| 100 kx∈a x ii = π | |
| 101 kx∈a x (iii ψ χ ) = < kx∈a x ψ , kx∈a x χ > | |
| 102 kx∈a x (iv ψ χ ) = kx∈a x ψ ・ < π , kx∈a x χ > | |
| 103 kx∈a x (v ψ ) = ( kx∈a x ψ ・ α ) * |