Mercurial > hg > Members > kono > Proof > category

annotate deductive.agda @ 793:f37f11e1b871

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Hom a,b = Hom 1 b^a
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 22 Apr 2019 02:41:53 +0900
parents 5bee48f7c126
children 6e6c7ad8ea1c
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
376c07159acf deduction theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4
376c07159acf deduction theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 -- Deduction Theorem
376c07159acf deduction theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6
792
5bee48f7c126 deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 791
diff changeset
7 -- positive logic
791
376c07159acf deduction theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
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
5bee48f7c126 deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 791
diff changeset
21 postulate L : PositiveLogic A
5bee48f7c126 deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 791
diff changeset
22
5bee48f7c126 deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 791
diff changeset
23 ⊤ = PositiveLogic.⊤ L
5bee48f7c126 deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 791
diff changeset
24 ○ = PositiveLogic.○ L
5bee48f7c126 deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 791
diff changeset
25 _∧_ = PositiveLogic._∧_ L
5bee48f7c126 deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 791
diff changeset
26 <_,_> = PositiveLogic.<_,_> L
5bee48f7c126 deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 791
diff changeset
27 π = PositiveLogic.π L
5bee48f7c126 deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 791
diff changeset
28 π' = PositiveLogic.π' L
5bee48f7c126 deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 791
diff changeset
29 _<=_ = PositiveLogic._<=_ L
5bee48f7c126 deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 791
diff changeset
30 _* = PositiveLogic._* L
5bee48f7c126 deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 791
diff changeset
31 ε = PositiveLogic.ε L
5bee48f7c126 deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 791
diff changeset
32 _・_ = _[_o_] A
791
376c07159acf deduction theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33
376c07159acf deduction theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 -- every proof b → c with assumption a has following forms
376c07159acf deduction theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35
792
5bee48f7c126 deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 791
diff changeset
36 data φ {a : Obj A } ( x : Hom A ⊤ a ) : {b c : Obj A } → Hom A b c → Set ( c₁ ⊔ c₂ ) where
5bee48f7c126 deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 791
diff changeset
37 i : {b c : Obj A} {k : Hom A b c } → φ x k
791
376c07159acf deduction theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 ii : φ x {⊤} {a} x
793
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 792
diff changeset
39 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 >
792
5bee48f7c126 deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 791
diff changeset
40 iv : {b c d : Obj A } { f : Hom A d c } { g : Hom A b d } (ψ : φ x f ) (χ : φ x g ) → φ x ( f ・ g )
793
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 792
diff changeset
41 v : {b c' c'' : Obj A } { f : Hom A (b ∧ c') c'' } (ψ : φ x f ) → φ x {b} {c'' <= c'} ( f * )
791
376c07159acf deduction theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42
792
5bee48f7c126 deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 791
diff changeset
43 α : {a b c : Obj A } → Hom A (( a ∧ b ) ∧ c ) ( a ∧ ( b ∧ c ) )
791
376c07159acf deduction theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 α = < π ・ π , < π' ・ π , π' > >
376c07159acf deduction theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45
376c07159acf deduction theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 -- genetate (a ∧ b) → c proof from proof b → c with assumption a
376c07159acf deduction theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47
792
5bee48f7c126 deduction theorem using category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 791
diff changeset
48 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
791
376c07159acf deduction theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 kx∈a x {k} i = k ・ π'
376c07159acf deduction theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50 kx∈a x ii = π
376c07159acf deduction theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51 kx∈a x (iii ψ χ ) = < kx∈a x ψ , kx∈a x χ >
376c07159acf deduction theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52 kx∈a x (iv ψ χ ) = kx∈a x ψ ・ < π , kx∈a x χ >
376c07159acf deduction theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53 kx∈a x (v ψ ) = ( kx∈a x ψ ・ α ) *