Mercurial > hg > Members > kono > Proof > category
changeset 1092:e1816090be31
could be. but give up now
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 17 May 2021 09:30:48 +0900 |
| parents | 9f967d9312f1 |
| children | |
| files | src/Polynominal.agda |
| diffstat | 1 files changed, 28 insertions(+), 22 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Polynominal.agda Mon May 17 01:19:00 2021 +0900 +++ b/src/Polynominal.agda Mon May 17 09:30:48 2021 +0900 @@ -68,20 +68,22 @@ -- it is better to define A[x] as an extension of A as described before open import Data.Unit - xnef : {a b c : Obj A } → ( x∈a : Hom A １ a ) → {z : Hom A b c } → ( y : φ {a} x∈a z ) → Set c₂ + xnef : {a b c : Obj A } → ( x∈a : Hom A １ a ) → {f : Hom A b c } → ( y : φ {a} x∈a f ) → Set c₂ xnef {a} {b} {c} x (i f) = ¬ (x ≅ f) xnef {a} {１} x ii = Lift _ ⊤ xnef {a} {b} x (iii phi phi₁) = xnef x phi × xnef x phi₁ xnef {a} {b} x (iv phi phi₁) = xnef x phi × xnef x phi₁ xnef {a} {b} x (v phi) = xnef x phi + nx : {a b c : Obj A } → ( x : Hom A １ a ) → {f : Hom A b c } → ( y : φ {a} x f ) → xnef x y → ¬ (x ≅ f) + nx = {!!} + record Poly (a c b : Obj A ) : Set (c₁ ⊔ c₂ ⊔ ℓ) where field x : Hom A １ a -- λ x f : Hom A b c phi : φ x {b} {c} f -- construction of f - nf : (fp : φ x {b} {c} f) → xnef x fp - + nf : xnef x {f} phi -- since we have A[x] now, we can proceed the proof on p.64 in some possible future @@ -125,33 +127,33 @@ -- all other cases, arguments are reduced to f ∙ π' . ki : {a b c : Obj A} → (x : Hom A １ a) → (f : Hom A b c ) → (fp : φ x {b} {c} f ) - → ((fp : φ x {b} {c} f ) → xnef x fp ) → A [ k x (i f) ≈ k x fp ] - ki x f (i _) _ = refl-hom - ki {a} x .x ii ne = ⊥-elim ( ne (i x) HE.refl ) - ki x _ (iii {_} {_} {_} {f₁}{ f₂} fp₁ fp₂ ) ne = begin + → xnef x fp → ¬ (x ≅ f) → A [ k x (i f) ≈ k x fp ] + ki x f (i _) _ _ = refl-hom + ki {a} x .x ii _ ne = ⊥-elim ( ne HE.refl ) + ki x _ (iii {_} {_} {_} {f₁}{ f₂} fp₁ fp₂ ) xf ne = begin < f₁ , f₂ > ∙ π' ≈⟨ IsCCC.distr-π isCCC ⟩ - < f₁ ∙ π' , f₂ ∙ π' > ≈⟨ π-cong (ki x f₁ fp₁ (λ fp → proj₁ (ne (iii fp fp₂ )))) (ki x f₂ fp₂ (λ fp → proj₂ (ne (iii fp₁ fp )))) ⟩ + < f₁ ∙ π' , f₂ ∙ π' > ≈⟨ π-cong (ki x f₁ fp₁ (proj₁ xf) {!!}) (ki x f₂ fp₂ (proj₂ xf) {!!}) ⟩ k x (iii fp₁ fp₂ ) ∎ - ki x _ (iv {_} {_} {_} {f₁} {f₂} fp fp₁) ne = begin + ki x _ (iv {_} {_} {_} {f₁} {f₂} fp fp₁) xf ne = begin (f₁ ∙ f₂ ) ∙ π' ≈↑⟨ assoc ⟩ f₁ ∙ ( f₂ ∙ π') ≈↑⟨ cdr (IsCCC.e3b isCCC) ⟩ f₁ ∙ ( π' ∙ < π , (f₂ ∙ π' ) >) ≈⟨ assoc ⟩ - (f₁ ∙ π' ) ∙ < π , (f₂ ∙ π' ) > ≈⟨ resp (π-cong refl-hom (ki x _ fp₁ (λ p → proj₂ (ne (iv fp p ) ) )) ) (ki x _ fp (λ p → proj₁ (ne (iv p fp₁ ) ))) ⟩ + (f₁ ∙ π' ) ∙ < π , (f₂ ∙ π' ) > ≈⟨ resp (π-cong refl-hom (ki x _ fp₁ (proj₂ xf) {!!}) ) (ki x _ fp (proj₁ xf) {!!}) ⟩ k x fp ∙ < π , k x fp₁ > ≈⟨⟩ k x (iv fp fp₁ ) ∎ - ki x _ (v {_} {_} {_} {f} fp) ne = begin + ki x _ (v {_} {_} {_} {f} fp) xf ne = begin (f *) ∙ π' ≈⟨ distr-* ⟩ ( f ∙ < π' ∙ π , π' > ) * ≈↑⟨ *-cong (cdr (IsCCC.e3b isCCC)) ⟩ ( f ∙ ( π' ∙ < π ∙ π , < π' ∙ π , π' > > ) ) * ≈⟨ *-cong assoc ⟩ - ( (f ∙ π') ∙ < π ∙ π , < π' ∙ π , π' > > ) * ≈⟨ *-cong ( car ( ki x _ fp (λ p → ne (v p )) )) ⟩ + ( (f ∙ π') ∙ < π ∙ π , < π' ∙ π , π' > > ) * ≈⟨ *-cong ( car ( ki x _ fp xf {!!} )) ⟩ ( k x fp ∙ < π ∙ π , < π' ∙ π , π' > > ) * ≈⟨⟩ k x (v fp ) ∎ k-cong : {a b c : Obj A} → (f g : Poly a c b ) → A [ Poly.f f ≈ Poly.f g ] → A [ k (Poly.x f) (Poly.phi f) ≈ k (Poly.x g) (Poly.phi g) ] k-cong {a} {b} {c} f g f=f = begin - k (Poly.x f) (Poly.phi f) ≈↑⟨ ki (Poly.x f) (Poly.f f) (Poly.phi f) (Poly.nf f ) ⟩ + k (Poly.x f) (Poly.phi f) ≈↑⟨ ki (Poly.x f) (Poly.f f) (Poly.phi f) (Poly.nf f ) {!!} ⟩ Poly.f f ∙ π' ≈⟨ car f=f ⟩ - Poly.f g ∙ π' ≈⟨ ki (Poly.x g) (Poly.f g) (Poly.phi g) (Poly.nf g ) ⟩ + Poly.f g ∙ π' ≈⟨ ki (Poly.x g) (Poly.f g) (Poly.phi g) (Poly.nf g ) {!!} ⟩ k (Poly.x g) (Poly.phi g) ∎ -- proof in p.59 Lambek @@ -164,7 +166,7 @@ functional-completeness {a} {b} {c} p = record { fun = k (Poly.x p) (Poly.phi p) ; fp = fc0 (Poly.x p) (Poly.f p) (Poly.phi p) - ; uniq = λ f eq → uniq (Poly.x p) (Poly.f p) (Poly.phi p) f (Poly.nf p ) eq + ; uniq = λ f eq → uniq (Poly.x p) (Poly.f p) (Poly.phi p) f (Poly.nf p ) {!!} eq } where fc0 : {a b c : Obj A} → (x : Hom A １ a) (f : Hom A b c) (phi : φ x {b} {c} f ) → A [ k x phi ∙ < x ∙ ○ b , id1 A b > ≈ f ] @@ -221,10 +223,11 @@ -- f ∙ < x ∙ ○ b , id1 A b > ≈ f → f ≈ k x (phi p) -- 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) - → ((phi : φ x {b} {c} f) → xnef x phi) + → xnef x phi + → ¬ x ≅ f → A [ f' ∙ < x ∙ ○ b , id1 A b > ≈ f ] → A [ f' ≈ k x phi ] - uniq {a} {b} {c} x f phi f' ne fx=p = sym (begin - k x phi ≈↑⟨ ki x f phi ne ⟩ + uniq {a} {b} {c} x f phi f' xf ne fx=p = sym (begin + k x phi ≈↑⟨ ki x f phi xf ne ⟩ k x {f} (i _) ≈↑⟨ car fx=p ⟩ k x {f' ∙ < x ∙ ○ b , id1 A b >} (i _) ≈⟨ trans-hom (sym assoc) (cdr (IsCCC.distr-π isCCC) ) ⟩ -- ( f' ∙ < x ∙ ○ b , id1 A b> ) ∙ π' f' ∙ k x {< x ∙ ○ b , id1 A b >} (iii (i _) (i _) ) ≈⟨⟩ -- ( f' ∙ < (x ∙ ○ b) ∙ π' , id1 A b ∙ π' > ) @@ -235,11 +238,14 @@ f' ∙ < π , π' > ≈⟨ cdr (IsCCC.π-id isCCC) ⟩ f' ∙ id1 A _ ≈⟨ idR ⟩ f' ∎ ) where - -- x ∙ ○ b is clearly Polynominal, but our xnef is too strong to prove it - postulate - xf : {a b : Obj A} → { x : Hom A １ a } → (fp : φ x (x ∙ ○ b)) → xnef x fp + xf1 : {a b : Obj A} → ( x : Hom A １ a ) → (f : Hom A b a) → (fp : φ x f) → φ x f ≅ φ x (x ∙ ○ b) → xnef x fp + xf1 x f (i .f) eq = {!!} + xf1 x f ii eq = lift tt + xf1 x f (iii fp fp₁) eq = {!!} + xf1 x f (iv fp fp₁) eq = {!!} -- φ x (f₂ ∙ g) ≅ φ x (x ∙ ○ b₂) → + xf1 x f (v fp) eq = {!!} u2 : k x {x ∙ ○ b} (i _) ≈ k x {x} ii ∙ < π , k x {○ b} (i _) > -- (x ∙ (○ b)) ∙ π' ≈ π ∙ < π , (○ b) ∙ π' > - u2 = ki x (x ∙ ○ b) (iv ii (i _)) xf + u2 = ki x (x ∙ ○ b) (iv ii (i _)) (xf1 x (x ∙ ○ b) (iv ii (i _)) HE.refl) {!!} -- functional completeness ε form --