Mercurial > hg > Members > kono > Proof > category

comparison deductive.agda @ 914:8c2da34e8dc1

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, 02 May 2020 05:32:42 +0900
parents 82a8c1ab4ef5
children
comparison
equal deleted inserted replaced
913:c5446790ddb1 914:8c2da34e8dc1
25 _・_ = _[_o_] A 25 _・_ = _[_o_] A
26 26
27 -- every proof b → c with assumption a has following forms 27 -- every proof b → c with assumption a has following forms
28 28
29 data φ {a : Obj A } ( x : Hom A ⊤ a ) : {b c : Obj A } → Hom A b c → Set ( c₁ ⊔ c₂ ) where 29 data φ {a : Obj A } ( x : Hom A ⊤ a ) : {b c : Obj A } → Hom A b c → Set ( c₁ ⊔ c₂ ) where
30 i : {b c : Obj A} {k : Hom A b c } → φ x k 30 i : {b c : Obj A} {k : Hom A b c } → φ x k
31 ii : φ x {⊤} {a} x 31 ii : φ x {⊤} {a} x
32 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 > 32 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 >
33 iv : {b c d : Obj A } { f : Hom A d c } { g : Hom A b d } (ψ : φ x f ) (χ : φ x g ) → φ x ( f ・ g ) 33 iv : {b c d : Obj A } { f : Hom A d c } { g : Hom A b d } (ψ : φ x f ) (χ : φ x g ) → φ x ( f ・ g )
34 v : {b c' c'' : Obj A } { f : Hom A (b ∧ c') c'' } (ψ : φ x f ) → φ x {b} {c'' <= c'} ( f * ) 34 v : {b c' c'' : Obj A } { f : Hom A (b ∧ c') c'' } (ψ : φ x f ) → φ x {b} {c'' <= c'} ( f * )
35 35
36 α : {a b c : Obj A } → Hom A (( a ∧ b ) ∧ c ) ( a ∧ ( b ∧ c ) ) 36 α : {a b c : Obj A } → Hom A (( a ∧ b ) ∧ c ) ( a ∧ ( b ∧ c ) )
37 α = < π ・ π , < π' ・ π , π' > > 37 α = < π ・ π , < π' ・ π , π' > >
38 38
39 -- genetate (a ∧ b) → c proof from proof b → c with assumption a 39 -- genetate (a ∧ b) → c proof from proof b → c with assumption a
40 40
41 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 41 k : {a b c : Obj A } → ( x∈a : Hom A ⊤ a ) → {z : Hom A b c } → ( y : φ {a} x∈a z ) → Hom A (a ∧ b) c
42 kx∈a x {k} i = k ・ π' 42 k x∈a {k} i = k ・ π'
43 kx∈a x ii = π 43 k x∈a ii = π
44 kx∈a x (iii ψ χ ) = < kx∈a x ψ , kx∈a x χ > 44 k x∈a (iii ψ χ ) = < k x∈a ψ , k x∈a χ >
45 kx∈a x (iv ψ χ ) = kx∈a x ψ ・ < π , kx∈a x χ > 45 k x∈a (iv ψ χ ) = k x∈a ψ ・ < π , k x∈a χ >
46 kx∈a x (v ψ ) = ( kx∈a x ψ ・ α ) * 46 k x∈a (v ψ ) = ( k x∈a ψ ・ α ) *
47
48 -- toφ : {a b c : Obj A } → ( x∈a : Hom A ⊤ a ) → (z : Hom A b c ) → φ {a} x∈a z
49 -- toφ {a} {b} {c} x∈a z = {!!}