Mercurial > hg > Members > kono > Proof > category
annotate src/Polynominal.agda @ 1083:caba080b1ded
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 15 May 2021 11:33:07 +0900 |
| parents | a59d7f0edeae |
| children | 372ea20015e8 |
| rev | line source |
|---|---|
| 1048 | 1 {-# OPTIONS --allow-unsolved-metas #-} |
| 2 | |
|
968
3a096cb82dc4
Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
3 open import Category |
|
3a096cb82dc4
Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
4 open import CCC |
|
3a096cb82dc4
Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
5 open import Level |
|
1015
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
6 open import HomReasoning |
|
968
3a096cb82dc4
Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
7 open import cat-utility |
| 1083 | 8 open import Relation.Nullary |
| 9 open import Data.Empty | |
| 10 open import Data.Product renaming ( <_,_> to ⟪_,_⟫ ) | |
|
968
3a096cb82dc4
Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
11 |
| 969 | 12 module Polynominal { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( C : CCC A ) where |
|
968
3a096cb82dc4
Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
13 |
| 969 | 14 open CCC.CCC C |
|
1015
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
15 open ≈-Reasoning A hiding (_∙_) |
| 969 | 16 |
|
1015
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
17 _∙_ = _[_o_] A |
| 970 | 18 |
|
1015
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
19 -- |
|
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
20 -- Polynominal (p.57) in Introduction to Higher order categorical logic |
|
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
21 -- |
|
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
22 -- Given object a₀ and a of a caterisian closed category A, how does one adjoin an interminate arraow x : a₀ → a to A? |
|
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
23 -- A[x] based on the `assumption' x, as was done in Section 2 (data φ). The formulas of A[x] are the objects of A and the |
|
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
24 -- proofs of A[x] are formed from the arrows of A and the new arrow x : a₀ → a by the appropriate ules of inference. |
| 1014 | 25 -- |
| 26 -- Here, A is actualy A[x]. It contains x and all the arrow generated from x. | |
|
1015
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
27 -- If we can put constraints on rule i (sub : Hom A b c → Set), then A is strictly smaller than A[x], |
|
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
28 -- that is, a subscategory of A[x]. |
|
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
29 -- |
|
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
30 -- i : {b c : Obj A} {k : Hom A b c } → sub k → φ x k |
| 1083 | 31 -- sub k is ¬ ( k ≈ x ), we cannot write this because b≡⊤ c≡a is forced |
|
1015
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
32 -- |
|
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
33 -- this makes a few changes, but we don't care. |
|
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
34 -- from page. 51 |
| 1014 | 35 -- |
| 1083 | 36 |
| 37 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) | |
| 38 | |
| 1012 | 39 data φ {a ⊤ : Obj A } ( x : Hom A ⊤ a ) : {b c : Obj A } → Hom A b c → Set ( c₁ ⊔ c₂ ⊔ ℓ) where |
| 1083 | 40 i : {b c : Obj A} (k : Hom A b c ) → φ x k |
| 1012 | 41 ii : φ x {⊤} {a} x |
| 42 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 > | |
|
1015
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
43 iv : {b c d : Obj A } { f : Hom A d c } { g : Hom A b d } (ψ : φ x f ) (χ : φ x g ) → φ x ( f ∙ g ) |
| 1012 | 44 v : {b c' c'' : Obj A } { f : Hom A (b ∧ c') c'' } (ψ : φ x f ) → φ x {b} {c'' <= c'} ( f * ) |
| 45 | |
| 46 α : {a b c : Obj A } → Hom A (( a ∧ b ) ∧ c ) ( a ∧ ( b ∧ c ) ) | |
|
1015
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
47 α = < π ∙ π , < π' ∙ π , π' > > |
| 1012 | 48 |
| 49 -- genetate (a ∧ b) → c proof from proof b → c with assumption a | |
|
1015
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
50 -- from page. 51 |
| 1012 | 51 |
| 52 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 | |
| 1083 | 53 k x∈a {k} (i _) = k ∙ π' |
| 1012 | 54 k x∈a ii = π |
| 55 k x∈a (iii ψ χ ) = < k x∈a ψ , k x∈a χ > | |
|
1015
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
56 k x∈a (iv ψ χ ) = k x∈a ψ ∙ < π , k x∈a χ > |
|
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
57 k x∈a (v ψ ) = ( k x∈a ψ ∙ α ) * |
| 1012 | 58 |
| 59 toφ : {a ⊤ b c : Obj A } → ( x∈a : Hom A ⊤ a ) → (z : Hom A b c ) → φ {a} x∈a z | |
| 1083 | 60 toφ {a} {⊤} {b} {c} x∈a z = i z |
| 1012 | 61 |
|
1081
3f85f57599e0
Polynominal done with minimum equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1080
diff
changeset
|
62 -- The Polynominal arrow -- λ term in A |
|
3f85f57599e0
Polynominal done with minimum equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1080
diff
changeset
|
63 -- |
| 1059 | 64 -- arrow in A[x], equality in A[x] should be a modulo x, that is k x phi ≈ k x phi' |
| 65 -- the smallest equivalence relation | |
| 66 -- | |
| 67 -- if we use equality on f as in A, Poly is ovioously Hom c b of a Category. | |
| 68 -- it is better to define A[x] as an extension of A as described before | |
| 69 | |
| 1083 | 70 open import Data.Unit |
| 71 xnef : {a b c : Obj A } → ( x∈a : Hom A １ a ) → {z : Hom A b c } → ( y : φ {a} x∈a z ) → Set c₂ | |
| 72 xnef {a} {b} {c} x (i f) = ¬ ( x ≅ f) | |
| 73 xnef {a} {１} x ii = Lift _ ⊤ | |
| 74 xnef {a} {b} x (iii phi phi₁) = xnef x phi × xnef x phi₁ | |
| 75 xnef {a} {b} x (iv phi phi₁) = xnef x phi × xnef x phi₁ | |
| 76 xnef {a} {b} x (v phi) = xnef x phi | |
| 77 | |
| 1054 | 78 record Poly (a c b : Obj A ) : Set (c₁ ⊔ c₂ ⊔ ℓ) where |
| 1048 | 79 field |
|
1081
3f85f57599e0
Polynominal done with minimum equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1080
diff
changeset
|
80 x : Hom A １ a -- λ x |
| 1054 | 81 f : Hom A b c |
|
1081
3f85f57599e0
Polynominal done with minimum equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1080
diff
changeset
|
82 phi : φ x {b} {c} f -- construction of f |
| 1083 | 83 nf : xnef x phi |
|
1061
805a4113ad74
functional completeness ε form done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1060
diff
changeset
|
84 |
| 1062 | 85 -- since we have A[x] now, we can proceed the proof on p.64 in some possible future |
| 86 | |
|
1015
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
87 -- |
|
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
88 -- Proposition 6.1 |
|
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
89 -- |
|
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
90 -- For every polynominal ψ(x) : b → c in an indeterminate x : 1 → a over a cartesian or cartesian closed |
|
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
91 -- category A there is a unique arrow f : a ∧ b → c in A such that f ∙ < x ∙ ○ b , id1 A b > ≈ ψ(x). |
|
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
92 |
| 1054 | 93 record Functional-completeness {a b c : Obj A} ( p : Poly a c b ) : Set (c₁ ⊔ c₂ ⊔ ℓ) where |
| 94 x = Poly.x p | |
| 1012 | 95 field |
| 1054 | 96 fun : Hom A (a ∧ b) c |
| 97 fp : A [ fun ∙ < x ∙ ○ b , id1 A b > ≈ Poly.f p ] | |
| 98 uniq : ( f : Hom A (a ∧ b) c) → A [ f ∙ < x ∙ ○ b , id1 A b > ≈ Poly.f p ] | |
| 99 → A [ f ≈ fun ] | |
| 1012 | 100 |
| 1062 | 101 -- ε form |
| 1047 | 102 -- f ≡ λ (x ∈ a) → φ x , ∃ (f : b <= a) → f ∙ x ≈ φ x |
|
1051
1948ce61e2f0
... Polynominal arg type
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1050
diff
changeset
|
103 record Fc {a b : Obj A } ( φ : Poly a b １ ) |
| 1048 | 104 : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where |
| 105 field | |
| 106 sl : Hom A a b | |
| 1050 | 107 g : Hom A １ (b <= a) |
| 1082 | 108 g = ( sl ∙ π' ) * |
| 1048 | 109 field |
| 1082 | 110 isSelect : A [ ε ∙ < g , Poly.x φ > ≈ Poly.f φ ] |
| 111 isUnique : (f : Hom A １ (b <= a) ) → A [ ε ∙ < f , Poly.x φ > ≈ Poly.f φ ] | |
| 1050 | 112 → A [ g ≈ f ] |
| 1047 | 113 |
| 1062 | 114 -- we should open IsCCC isCCC |
| 1052 | 115 π-cong = IsCCC.π-cong isCCC |
| 116 *-cong = IsCCC.*-cong isCCC | |
| 1059 | 117 distr-* = IsCCC.distr-* isCCC |
| 1052 | 118 e2 = IsCCC.e2 isCCC |
|
1080
c61639f34e7b
fix Poly minimum equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1079
diff
changeset
|
119 |
|
c61639f34e7b
fix Poly minimum equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1079
diff
changeset
|
120 -- f ≈ g → k x {f} _ ≡ k x {g} _ Lambek p.60 |
|
c61639f34e7b
fix Poly minimum equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1079
diff
changeset
|
121 -- if A is locally small, it is ≡-cong. |
|
c61639f34e7b
fix Poly minimum equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1079
diff
changeset
|
122 -- case i i is π ∙ f ≈ π ∙ g |
|
c61639f34e7b
fix Poly minimum equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1079
diff
changeset
|
123 -- we have (x y : Hom A １ a) → x ≈ y (minimul equivalende assumption) in record Poly. this makes all k x ii case valid |
|
c61639f34e7b
fix Poly minimum equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1079
diff
changeset
|
124 -- all other cases, arguments are reduced to f ∙ π' . |
|
c61639f34e7b
fix Poly minimum equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1079
diff
changeset
|
125 |
| 1083 | 126 ki : {a b c : Obj A} → (x : Hom A １ a) → (f : Hom A b c ) → (fp : φ x {b} {c} f ) → xnef x fp → ¬ (f ≅ x) → A [ k x (i f) ≈ k x fp ] |
| 127 ki x f (i _) _ _ = refl-hom | |
| 128 ki {a} x .x ii ne fx = ⊥-elim ( fx HE.refl ) | |
| 129 ki x _ (iii {_} {_} {_} {f₁}{ f₂} fp₁ fp₂ ) ne fx = begin | |
|
1080
c61639f34e7b
fix Poly minimum equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1079
diff
changeset
|
130 < f₁ , f₂ > ∙ π' ≈⟨ IsCCC.distr-π isCCC ⟩ |
| 1083 | 131 < f₁ ∙ π' , f₂ ∙ π' > ≈⟨ π-cong (ki x f₁ fp₁ (proj₁ ne) {!!} ) (ki x f₂ fp₂ (proj₂ ne ) {!!} ) ⟩ |
|
1080
c61639f34e7b
fix Poly minimum equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1079
diff
changeset
|
132 k x (iii fp₁ fp₂ ) ∎ |
| 1083 | 133 ki x _ (iv {_} {_} {_} {f₁} {f₂} fp fp₁) ne _ = begin |
|
1080
c61639f34e7b
fix Poly minimum equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1079
diff
changeset
|
134 (f₁ ∙ f₂ ) ∙ π' ≈↑⟨ assoc ⟩ |
|
c61639f34e7b
fix Poly minimum equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1079
diff
changeset
|
135 f₁ ∙ ( f₂ ∙ π') ≈↑⟨ cdr (IsCCC.e3b isCCC) ⟩ |
|
c61639f34e7b
fix Poly minimum equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1079
diff
changeset
|
136 f₁ ∙ ( π' ∙ < π , (f₂ ∙ π' ) >) ≈⟨ assoc ⟩ |
| 1083 | 137 (f₁ ∙ π' ) ∙ < π , (f₂ ∙ π' ) > ≈⟨ resp (π-cong refl-hom (ki x _ fp₁ (proj₂ ne) {!!} ) ) (ki x _ fp (proj₁ ne) {!!}) ⟩ |
|
1080
c61639f34e7b
fix Poly minimum equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1079
diff
changeset
|
138 k x fp ∙ < π , k x fp₁ > ≈⟨⟩ |
|
c61639f34e7b
fix Poly minimum equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1079
diff
changeset
|
139 k x (iv fp fp₁ ) ∎ |
| 1083 | 140 ki x _ (v {_} {_} {_} {f} fp) ne fx = begin |
|
1081
3f85f57599e0
Polynominal done with minimum equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1080
diff
changeset
|
141 (f *) ∙ π' ≈⟨ distr-* ⟩ |
|
3f85f57599e0
Polynominal done with minimum equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1080
diff
changeset
|
142 ( f ∙ < π' ∙ π , π' > ) * ≈↑⟨ *-cong (cdr (IsCCC.e3b isCCC)) ⟩ |
|
3f85f57599e0
Polynominal done with minimum equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1080
diff
changeset
|
143 ( f ∙ ( π' ∙ < π ∙ π , < π' ∙ π , π' > > ) ) * ≈⟨ *-cong assoc ⟩ |
| 1083 | 144 ( (f ∙ π') ∙ < π ∙ π , < π' ∙ π , π' > > ) * ≈⟨ *-cong ( car ( ki x _ fp ne {!!} )) ⟩ |
|
1081
3f85f57599e0
Polynominal done with minimum equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1080
diff
changeset
|
145 ( k x fp ∙ < π ∙ π , < π' ∙ π , π' > > ) * ≈⟨⟩ |
|
3f85f57599e0
Polynominal done with minimum equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1080
diff
changeset
|
146 k x (v fp ) ∎ |
|
1080
c61639f34e7b
fix Poly minimum equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1079
diff
changeset
|
147 k-cong : {a b c : Obj A} → (f g : Poly a c b ) |
|
c61639f34e7b
fix Poly minimum equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1079
diff
changeset
|
148 → A [ Poly.f f ≈ Poly.f g ] → A [ k (Poly.x f) (Poly.phi f) ≈ k (Poly.x g) (Poly.phi g) ] |
| 1082 | 149 k-cong {a} {b} {c} f g f=f = begin |
| 1083 | 150 k (Poly.x f) (Poly.phi f) ≈↑⟨ ki (Poly.x f) (Poly.f f) (Poly.phi f) (Poly.nf f) {!!} ⟩ |
|
1081
3f85f57599e0
Polynominal done with minimum equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1080
diff
changeset
|
151 Poly.f f ∙ π' ≈⟨ car f=f ⟩ |
| 1083 | 152 Poly.f g ∙ π' ≈⟨ ki (Poly.x g) (Poly.f g) (Poly.phi g) (Poly.nf g) {!!} ⟩ |
|
1081
3f85f57599e0
Polynominal done with minimum equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1080
diff
changeset
|
153 k (Poly.x g) (Poly.phi g) ∎ |
| 1052 | 154 |
| 1059 | 155 -- proof in p.59 Lambek |
| 1082 | 156 -- |
| 157 -- (ψ : Poly a c b) is basically λ x.ψ(x). To use x from outside as a ψ(x), apply x ψ will work. | |
| 158 -- Instead of replacing x in Poly.phi ψ, we can use simple application with this fuctional completeness | |
| 159 -- in the internal language of Topos. | |
| 160 -- | |
| 1054 | 161 functional-completeness : {a b c : Obj A} ( p : Poly a c b ) → Functional-completeness p |
| 162 functional-completeness {a} {b} {c} p = record { | |
| 163 fun = k (Poly.x p) (Poly.phi p) | |
| 1055 | 164 ; fp = fc0 (Poly.x p) (Poly.f p) (Poly.phi p) |
| 1083 | 165 ; uniq = λ f eq → uniq (Poly.x p) (Poly.f p) (Poly.phi p) f (Poly.nf p) eq |
|
1015
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
166 } where |
| 1055 | 167 fc0 : {a b c : Obj A} → (x : Hom A １ a) (f : Hom A b c) (phi : φ x {b} {c} f ) |
| 168 → A [ k x phi ∙ < x ∙ ○ b , id1 A b > ≈ f ] | |
| 169 fc0 {a} {b} {c} x f' phi with phi | |
| 1083 | 170 ... | i {_} {_} s = begin |
|
1015
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
171 (s ∙ π') ∙ < ( x ∙ ○ b ) , id1 A b > ≈↑⟨ assoc ⟩ |
|
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
172 s ∙ (π' ∙ < ( x ∙ ○ b ) , id1 A b >) ≈⟨ cdr (IsCCC.e3b isCCC ) ⟩ |
|
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
173 s ∙ id1 A b ≈⟨ idR ⟩ |
| 1055 | 174 s ∎ |
| 1012 | 175 ... | ii = begin |
|
1015
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
176 π ∙ < ( x ∙ ○ b ) , id1 A b > ≈⟨ IsCCC.e3a isCCC ⟩ |
|
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
177 x ∙ ○ b ≈↑⟨ cdr (e2 ) ⟩ |
|
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
178 x ∙ id1 A b ≈⟨ idR ⟩ |
| 1055 | 179 x ∎ |
| 1012 | 180 ... | iii {_} {_} {_} {f} {g} y z = begin |
|
1015
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
181 < k x y , k x z > ∙ < (x ∙ ○ b ) , id1 A b > ≈⟨ IsCCC.distr-π isCCC ⟩ |
|
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
182 < k x y ∙ < (x ∙ ○ b ) , id1 A b > , k x z ∙ < (x ∙ ○ b ) , id1 A b > > |
| 1055 | 183 ≈⟨ π-cong (fc0 x f y ) (fc0 x g z ) ⟩ |
| 1012 | 184 < f , g > ≈⟨⟩ |
| 1055 | 185 f' ∎ |
| 1012 | 186 ... | iv {_} {_} {d} {f} {g} y z = begin |
|
1015
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
187 (k x y ∙ < π , k x z >) ∙ < ( x ∙ ○ b ) , id1 A b > ≈↑⟨ assoc ⟩ |
|
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
188 k x y ∙ ( < π , k x z > ∙ < ( x ∙ ○ b ) , id1 A b > ) ≈⟨ cdr (IsCCC.distr-π isCCC) ⟩ |
|
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
189 k x y ∙ ( < π ∙ < ( x ∙ ○ b ) , id1 A b > , k x z ∙ < ( x ∙ ○ b ) , id1 A b > > ) |
| 1055 | 190 ≈⟨ cdr (π-cong (IsCCC.e3a isCCC) (fc0 x g z ) ) ⟩ |
|
1015
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
191 k x y ∙ ( < x ∙ ○ b , g > ) ≈↑⟨ cdr (π-cong (cdr (e2)) refl-hom ) ⟩ |
|
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
192 k x y ∙ ( < x ∙ ( ○ d ∙ g ) , g > ) ≈⟨ cdr (π-cong assoc (sym idL)) ⟩ |
|
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
193 k x y ∙ ( < (x ∙ ○ d) ∙ g , id1 A d ∙ g > ) ≈↑⟨ cdr (IsCCC.distr-π isCCC) ⟩ |
|
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
194 k x y ∙ ( < x ∙ ○ d , id1 A d > ∙ g ) ≈⟨ assoc ⟩ |
| 1055 | 195 (k x y ∙ < x ∙ ○ d , id1 A d > ) ∙ g ≈⟨ car (fc0 x f y ) ⟩ |
| 1078 | 196 f ∙ g ∎ |
| 1012 | 197 ... | v {_} {_} {_} {f} y = begin |
|
1015
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
198 ( (k x y ∙ < π ∙ π , < π' ∙ π , π' > >) *) ∙ < x ∙ (○ b) , id1 A b > ≈⟨ IsCCC.distr-* isCCC ⟩ |
|
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
199 ( (k x y ∙ < π ∙ π , < π' ∙ π , π' > >) ∙ < < x ∙ ○ b , id1 A _ > ∙ π , π' > ) * ≈⟨ IsCCC.*-cong isCCC ( begin |
|
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
200 ( k x y ∙ < π ∙ π , < π' ∙ π , π' > >) ∙ < < x ∙ ○ b , id1 A _ > ∙ π , π' > ≈↑⟨ assoc ⟩ |
|
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
201 k x y ∙ ( < π ∙ π , < π' ∙ π , π' > > ∙ < < x ∙ ○ b , id1 A _ > ∙ π , π' > ) ≈⟨ cdr (IsCCC.distr-π isCCC) ⟩ |
|
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
202 k x y ∙ < (π ∙ π) ∙ < < x ∙ ○ b , id1 A _ > ∙ π , π' > , < π' ∙ π , π' > ∙ < < x ∙ ○ b , id1 A _ > ∙ π , π' > > |
|
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
203 ≈⟨ cdr (π-cong (sym assoc) (IsCCC.distr-π isCCC )) ⟩ |
|
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
204 k x y ∙ < π ∙ (π ∙ < < x ∙ ○ b , id1 A _ > ∙ π , π' > ) , |
|
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
205 < (π' ∙ π) ∙ < < x ∙ ○ b , id1 A _ > ∙ π , π' > , π' ∙ < < x ∙ ○ b , id1 A _ > ∙ π , π' > > > |
|
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
206 ≈⟨ cdr ( π-cong (cdr (IsCCC.e3a isCCC))( π-cong (sym assoc) (IsCCC.e3b isCCC) )) ⟩ |
|
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
207 k x y ∙ < π ∙ ( < x ∙ ○ b , id1 A _ > ∙ π ) , < π' ∙ (π ∙ < < x ∙ ○ b , id1 A _ > ∙ π , π' >) , π' > > |
|
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
208 ≈⟨ cdr ( π-cong refl-hom ( π-cong (cdr (IsCCC.e3a isCCC)) refl-hom )) ⟩ |
|
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
209 k x y ∙ < (π ∙ ( < x ∙ ○ b , id1 A _ > ∙ π ) ) , < π' ∙ (< x ∙ ○ b , id1 A _ > ∙ π ) , π' > > |
|
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
210 ≈⟨ cdr ( π-cong assoc (π-cong assoc refl-hom )) ⟩ |
|
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
211 k x y ∙ < (π ∙ < x ∙ ○ b , id1 A _ > ) ∙ π , < (π' ∙ < x ∙ ○ b , id1 A _ > ) ∙ π , π' > > |
|
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
212 ≈⟨ cdr (π-cong (car (IsCCC.e3a isCCC)) (π-cong (car (IsCCC.e3b isCCC)) refl-hom )) ⟩ |
|
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
213 k x y ∙ < ( (x ∙ ○ b ) ∙ π ) , < id1 A _ ∙ π , π' > > ≈⟨ cdr (π-cong (sym assoc) (π-cong idL refl-hom )) ⟩ |
|
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
214 k x y ∙ < x ∙ (○ b ∙ π ) , < π , π' > > ≈⟨ cdr (π-cong (cdr (e2)) (IsCCC.π-id isCCC) ) ⟩ |
| 1055 | 215 k x y ∙ < x ∙ ○ _ , id1 A _ > ≈⟨ fc0 x f y ⟩ |
| 1013 | 216 f ∎ ) ⟩ |
| 1055 | 217 f * ∎ |
|
1015
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
218 -- |
| 1054 | 219 -- f ∙ < x ∙ ○ b , id1 A b > ≈ f → f ≈ k x (phi p) |
|
1015
e01a1d29492b
Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1014
diff
changeset
|
220 -- |
| 1083 | 221 uniq : {a b c : Obj A} → (x : Hom A １ a) (f : Hom A b c) (phi : φ x {b} {c} f ) (f' : Hom A (a ∧ b) c) |
| 222 → xnef x phi | |
| 223 → A [ f' ∙ < x ∙ ○ b , id1 A b > ≈ f ] → A [ f' ≈ k x phi ] | |
| 224 uniq {a} {b} {c} x f phi f' ne fx=p = sym (begin | |
| 225 k x phi ≈↑⟨ ki x f phi ne {!!} ⟩ | |
| 226 k x {f} (i _) ≈↑⟨ car fx=p ⟩ | |
| 227 k x {f' ∙ < x ∙ ○ b , id1 A b >} (i _) ≈⟨ trans-hom (sym assoc) (cdr (IsCCC.distr-π isCCC) ) ⟩ -- ( f' ∙ < x ∙ ○ b , id1 A b> ) ∙ π' | |
| 228 f' ∙ k x {< x ∙ ○ b , id1 A b >} (iii (i _) (i _) ) -- ( f' ∙ < (x ∙ ○ b) ∙ π' , id1 A b ∙ π' > ) | |
| 229 ≈⟨ cdr (π-cong (ki x ( x ∙ ○ b) (iv ii (i _) ) {!!} {!!} ) refl-hom) ⟩ | |
| 230 f' ∙ < k x {x ∙ ○ b} (iv ii (i _) ) , k x {id1 A b} (i _) > ≈⟨ refl-hom ⟩ | |
| 231 f' ∙ < k x {x} ii ∙ < π , k x {○ b} (i _) > , k x {id1 A b} (i _) > -- ( f' ∙ < π ∙ < π , (x ∙ ○ b) ∙ π' > , id1 A b ∙ π' > ) | |
| 1056 | 232 ≈⟨ cdr (π-cong (cdr (π-cong refl-hom (car e2))) idL ) ⟩ |
| 233 f' ∙ < π ∙ < π , (○ b ∙ π' ) > , π' > ≈⟨ cdr (π-cong (IsCCC.e3a isCCC) refl-hom) ⟩ | |
| 234 f' ∙ < π , π' > ≈⟨ cdr (IsCCC.π-id isCCC) ⟩ | |
| 235 f' ∙ id1 A _ ≈⟨ idR ⟩ | |
| 1078 | 236 f' ∎ ) |
| 1054 | 237 |
| 1079 | 238 |
| 1055 | 239 -- functional completeness ε form |
|
1060
2458af98786a
FC isSelect done, kcong assumption
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1059
diff
changeset
|
240 -- |
|
2458af98786a
FC isSelect done, kcong assumption
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1059
diff
changeset
|
241 -- g : Hom A １ (b <= a) fun : Hom A (a ∧ １) c |
|
2458af98786a
FC isSelect done, kcong assumption
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1059
diff
changeset
|
242 -- fun * ε ∙ < g ∙ π , π' > |
|
2458af98786a
FC isSelect done, kcong assumption
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1059
diff
changeset
|
243 -- a -> d <= b <-> (a ∧ b ) -> d |
|
2458af98786a
FC isSelect done, kcong assumption
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1059
diff
changeset
|
244 -- |
|
2458af98786a
FC isSelect done, kcong assumption
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1059
diff
changeset
|
245 -- fun ∙ < x ∙ ○ b , id1 A b > ≈ Poly.f p |
|
2458af98786a
FC isSelect done, kcong assumption
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1059
diff
changeset
|
246 -- (ε ∙ < g ∙ π , π' >) ∙ < x ∙ ○ b , id1 A b > ≈ Poly.f p |
| 1062 | 247 -- could be simpler |
| 1055 | 248 FC : {a b : Obj A} → (φ : Poly a b １ ) → Fc {a} {b} φ |
| 249 FC {a} {b} φ = record { | |
| 1082 | 250 sl = k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a > |
| 1065 | 251 ; isSelect = isSelect |
|
1061
805a4113ad74
functional completeness ε form done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1060
diff
changeset
|
252 ; isUnique = uniq |
| 1055 | 253 } where |
| 1065 | 254 π-exchg = IsCCC.π-exchg isCCC |
| 1055 | 255 fc0 : {b c : Obj A} (p : Poly b c １) → A [ k (Poly.x p ) (Poly.phi p) ∙ < Poly.x p ∙ ○ １ , id1 A １ > ≈ Poly.f p ] |
| 256 fc0 p = Functional-completeness.fp (functional-completeness p) | |
|
1060
2458af98786a
FC isSelect done, kcong assumption
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1059
diff
changeset
|
257 gg : A [ ( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a > ) ∙ Poly.x φ ≈ Poly.f φ ] |
|
2458af98786a
FC isSelect done, kcong assumption
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1059
diff
changeset
|
258 gg = begin |
|
2458af98786a
FC isSelect done, kcong assumption
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1059
diff
changeset
|
259 ( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a > ) ∙ Poly.x φ ≈⟨ trans-hom (sym assoc) (cdr (IsCCC.distr-π isCCC ) ) ⟩ |
|
2458af98786a
FC isSelect done, kcong assumption
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1059
diff
changeset
|
260 k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ ∙ Poly.x φ , ○ a ∙ Poly.x φ > ≈⟨ cdr (π-cong idL e2 ) ⟩ |
|
2458af98786a
FC isSelect done, kcong assumption
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1059
diff
changeset
|
261 k (Poly.x φ ) (Poly.phi φ) ∙ < Poly.x φ , ○ １ > ≈⟨ cdr (π-cong (trans-hom (sym idR) (cdr e2) ) (sym e2) ) ⟩ |
|
2458af98786a
FC isSelect done, kcong assumption
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1059
diff
changeset
|
262 k (Poly.x φ ) (Poly.phi φ) ∙ < Poly.x φ ∙ ○ １ , id1 A １ > ≈⟨ fc0 φ ⟩ |
|
2458af98786a
FC isSelect done, kcong assumption
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1059
diff
changeset
|
263 Poly.f φ ∎ |
| 1065 | 264 isSelect : A [ ε ∙ < ( ( k (Poly.x φ ) ( Poly.phi φ) ∙ < id1 A _ , ○ a > ) ∙ π' ) * , Poly.x φ > ≈ Poly.f φ ] |
| 265 isSelect = begin | |
| 266 ε ∙ < ((k (Poly.x φ) (Poly.phi φ)∙ < id1 A _ , ○ a > ) ∙ π') * , Poly.x φ > ≈↑⟨ cdr (π-cong idR refl-hom ) ⟩ | |
| 267 ε ∙ (< ((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ id1 A _ , Poly.x φ > ) ≈⟨ cdr (π-cong (cdr e2) refl-hom ) ⟩ | |
| 268 ε ∙ (< ((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ ○ １ , Poly.x φ > ) ≈↑⟨ cdr (π-cong (cdr e2) refl-hom ) ⟩ | |
| 269 ε ∙ (< ((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ (○ a ∙ Poly.x φ) , Poly.x φ > ) ≈↑⟨ cdr (π-cong (sym assoc) idL ) ⟩ | |
| 270 ε ∙ (< (((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ ○ a ) ∙ Poly.x φ , id1 A _ ∙ Poly.x φ > ) | |
| 271 ≈↑⟨ cdr (IsCCC.distr-π isCCC) ⟩ | |
| 272 ε ∙ ((< (((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ ○ a ) , id1 A _ > ) ∙ Poly.x φ ) | |
| 273 ≈↑⟨ cdr (car (π-cong (cdr (IsCCC.e3a isCCC) ) refl-hom)) ⟩ | |
| 274 ε ∙ ((< (((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ (π ∙ < ○ a , id1 A _ > )) , id1 A _ > ) ∙ Poly.x φ ) | |
| 275 ≈⟨ cdr (car (π-cong assoc (sym (IsCCC.e3b isCCC)) )) ⟩ | |
| 276 ε ∙ ((< ((((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ π ) ∙ < ○ a , id1 A _ > ) , (π' ∙ < ○ a , id1 A _ > ) > ) ∙ Poly.x φ ) | |
| 277 ≈↑⟨ cdr (car (IsCCC.distr-π isCCC)) ⟩ | |
| 278 ε ∙ ((< ((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ π , π' > ∙ < ○ a , id1 A _ > ) ∙ Poly.x φ ) ≈⟨ assoc ⟩ | |
| 279 (ε ∙ (< ((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ π , π' > ∙ < ○ a , id1 A _ > ) ) ∙ Poly.x φ ≈⟨ car assoc ⟩ | |
| 280 ((ε ∙ < ((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) * ) ∙ π , π' > ) ∙ < ○ a , id1 A _ > ) ∙ Poly.x φ | |
| 281 ≈⟨ car (car (IsCCC.e4a isCCC)) ⟩ | |
| 282 ((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ) ∙ < ○ a , id1 A _ > ) ∙ Poly.x φ ≈↑⟨ car assoc ⟩ | |
| 283 (( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a > ) ∙ (π' ∙ < ○ a , id1 A _ > ) ) ∙ Poly.x φ ≈⟨ car (cdr (IsCCC.e3b isCCC)) ⟩ | |
| 284 (( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a > ) ∙ id1 A _ ) ∙ Poly.x φ ≈⟨ car idR ⟩ | |
| 285 ( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a > ) ∙ Poly.x φ ≈⟨ gg ⟩ | |
| 286 Poly.f φ ∎ | |
| 1082 | 287 uniq : (f : Hom A １ (b <= a)) → A [ ε ∙ < f , Poly.x φ > ≈ Poly.f φ ] → |
|
1061
805a4113ad74
functional completeness ε form done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1060
diff
changeset
|
288 A [ (( k (Poly.x φ) (Poly.phi φ) ∙ < id1 A _ , ○ a > )∙ π' ) * ≈ f ] |
|
805a4113ad74
functional completeness ε form done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1060
diff
changeset
|
289 uniq f eq = begin |
|
805a4113ad74
functional completeness ε form done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1060
diff
changeset
|
290 (( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ , ○ a > ) ∙ π' ) * ≈⟨ IsCCC.*-cong isCCC ( begin |
|
805a4113ad74
functional completeness ε form done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1060
diff
changeset
|
291 (k (Poly.x φ) (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ≈↑⟨ assoc ⟩ |
|
805a4113ad74
functional completeness ε form done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1060
diff
changeset
|
292 k (Poly.x φ) (Poly.phi φ) ∙ (< id1 A _ , ○ a > ∙ π') ≈⟨ car ( sym (Functional-completeness.uniq (functional-completeness φ) _ ( begin |
|
805a4113ad74
functional completeness ε form done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1060
diff
changeset
|
293 ((ε ∙ < f ∙ π , π' >) ∙ < π' , π >) ∙ < Poly.x φ ∙ ○ １ , id1 A １ > ≈↑⟨ assoc ⟩ |
|
805a4113ad74
functional completeness ε form done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1060
diff
changeset
|
294 (ε ∙ < f ∙ π , π' >) ∙ ( < π' , π > ∙ < Poly.x φ ∙ ○ １ , id1 A １ > ) ≈⟨ cdr (IsCCC.distr-π isCCC) ⟩ |
|
805a4113ad74
functional completeness ε form done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1060
diff
changeset
|
295 (ε ∙ < f ∙ π , π' >) ∙ < π' ∙ < Poly.x φ ∙ ○ １ , id1 A １ > , π ∙ < Poly.x φ ∙ ○ １ , id1 A １ > > |
|
805a4113ad74
functional completeness ε form done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1060
diff
changeset
|
296 ≈⟨ cdr (π-cong (IsCCC.e3b isCCC) (IsCCC.e3a isCCC)) ⟩ |
|
805a4113ad74
functional completeness ε form done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1060
diff
changeset
|
297 (ε ∙ < f ∙ π , π' >) ∙ < id1 A １ , Poly.x φ ∙ ○ １ > ≈↑⟨ assoc ⟩ |
|
805a4113ad74
functional completeness ε form done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1060
diff
changeset
|
298 ε ∙ ( < f ∙ π , π' > ∙ < id1 A １ , Poly.x φ ∙ ○ １ > ) ≈⟨ cdr (IsCCC.distr-π isCCC) ⟩ |
|
805a4113ad74
functional completeness ε form done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1060
diff
changeset
|
299 ε ∙ ( < (f ∙ π ) ∙ < id1 A １ , Poly.x φ ∙ ○ １ > , π' ∙ < id1 A １ , Poly.x φ ∙ ○ １ > > ) ≈⟨ cdr (π-cong (sym assoc) (IsCCC.e3b isCCC)) ⟩ |
|
805a4113ad74
functional completeness ε form done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1060
diff
changeset
|
300 ε ∙ ( < f ∙ (π ∙ < id1 A １ , Poly.x φ ∙ ○ １ > ) , Poly.x φ ∙ ○ １ > ) ≈⟨ cdr (π-cong (cdr (IsCCC.e3a isCCC)) (cdr (trans-hom e2 (sym e2)))) ⟩ |
|
805a4113ad74
functional completeness ε form done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1060
diff
changeset
|
301 ε ∙ ( < f ∙ id1 A １ , Poly.x φ ∙ id1 A １ > ) ≈⟨ cdr (π-cong idR idR ) ⟩ |
|
805a4113ad74
functional completeness ε form done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1060
diff
changeset
|
302 ε ∙ < f , Poly.x φ > ≈⟨ eq ⟩ |
|
805a4113ad74
functional completeness ε form done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1060
diff
changeset
|
303 Poly.f φ ∎ ))) ⟩ |
|
805a4113ad74
functional completeness ε form done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1060
diff
changeset
|
304 ((ε ∙ < f ∙ π , π' > ) ∙ < π' , π > ) ∙ ( < id1 A _ , ○ a > ∙ π' ) ≈↑⟨ assoc ⟩ |
|
805a4113ad74
functional completeness ε form done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1060
diff
changeset
|
305 (ε ∙ < f ∙ π , π' > ) ∙ (< π' , π > ∙ ( < id1 A _ , ○ a > ∙ π' ) ) ≈⟨ cdr (IsCCC.distr-π isCCC) ⟩ |
|
805a4113ad74
functional completeness ε form done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1060
diff
changeset
|
306 (ε ∙ < f ∙ π , π' > ) ∙ (< π' ∙ ( < id1 A _ , ○ a > ∙ π' ) , π ∙ ( < id1 A _ , ○ a > ∙ π' ) > ) ≈⟨ cdr (π-cong assoc assoc ) ⟩ |
|
805a4113ad74
functional completeness ε form done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1060
diff
changeset
|
307 (ε ∙ < f ∙ π , π' > ) ∙ (< (π' ∙ < id1 A _ , ○ a > ) ∙ π' , (π ∙ < id1 A _ , ○ a > ) ∙ π' > ) |
|
805a4113ad74
functional completeness ε form done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1060
diff
changeset
|
308 ≈⟨ cdr (π-cong (car (IsCCC.e3b isCCC)) (car (IsCCC.e3a isCCC) )) ⟩ |
|
805a4113ad74
functional completeness ε form done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1060
diff
changeset
|
309 (ε ∙ < f ∙ π , π' > ) ∙ < ○ a ∙ π' , id1 A _ ∙ π' > ≈⟨ cdr (π-cong (trans-hom e2 (sym e2) ) idL ) ⟩ |
|
805a4113ad74
functional completeness ε form done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1060
diff
changeset
|
310 (ε ∙ < f ∙ π , π' > ) ∙ < π , π' > ≈⟨ cdr (IsCCC.π-id isCCC) ⟩ |
|
805a4113ad74
functional completeness ε form done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1060
diff
changeset
|
311 (ε ∙ < f ∙ π , π' > ) ∙ id1 A (１ ∧ a) ≈⟨ idR ⟩ |
|
805a4113ad74
functional completeness ε form done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1060
diff
changeset
|
312 ε ∙ < f ∙ π , π' > ∎ ) ⟩ |
| 1082 | 313 ( ε ∙ < A [ f o π ] , π' > ) * ≈⟨ IsCCC.e4b isCCC ⟩ |
|
1061
805a4113ad74
functional completeness ε form done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1060
diff
changeset
|
314 f ∎ |
|
805a4113ad74
functional completeness ε form done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1060
diff
changeset
|
315 |
| 1055 | 316 |
|
968
3a096cb82dc4
Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
317 |
|
3a096cb82dc4
Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
318 -- end |