Mercurial > hg > Members > kono > Proof > category
changeset 1089:77e40cea8264
i : {b c : Obj A} (f : Hom A b c ) → ¬ ( f ≅ x ) → φ x f is bad
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 17 May 2021 00:42:08 +0900 |
| parents | ed657b63315d |
| children | a72b95a4b7b5 |
| files | src/Polynominal.agda |
| diffstat | 1 files changed, 33 insertions(+), 32 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Polynominal.agda Sun May 16 23:38:00 2021 +0900 +++ b/src/Polynominal.agda Mon May 17 00:42:08 2021 +0900 @@ -37,7 +37,7 @@ open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) data φ {a ⊤ : Obj A } ( x : Hom A ⊤ a ) : {b c : Obj A } → Hom A b c → Set ( c₁ ⊔ c₂ ⊔ ℓ) where - i : {b c : Obj A} (k : Hom A b c ) → φ x k + i : {b c : Obj A} (f : Hom A b c ) → ¬ ( f ≅ x ) → φ x f ii : φ x {⊤} {a} x 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 > iv : {b c d : Obj A } { f : Hom A d c } { g : Hom A b d } (ψ : φ x f ) (χ : φ x g ) → φ x ( f ∙ g ) @@ -50,15 +50,12 @@ -- from page. 51 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 - k x∈a {k} (i _) = k ∙ π' + k x∈a {k} (i _ _ ) = k ∙ π' k x∈a ii = π k x∈a (iii ψ χ ) = < k x∈a ψ , k x∈a χ > k x∈a (iv ψ χ ) = k x∈a ψ ∙ < π , k x∈a χ > k x∈a (v ψ ) = ( k x∈a ψ ∙ α ) * - toφ : {a ⊤ b c : Obj A } → ( x∈a : Hom A ⊤ a ) → (z : Hom A b c ) → φ {a} x∈a z - toφ {a} {⊤} {b} {c} x∈a z = i z - -- The Polynominal arrow -- λ term in A -- -- arrow in A[x], equality in A[x] should be a modulo x, that is k x phi ≈ k x phi' @@ -69,18 +66,27 @@ 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} 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 + xnef x (i f ne) = ¬ (f ≅ x) + xnef x ii = Lift _ ⊤ + xnef x (iii phi phi₁) = xnef x phi × xnef x phi₁ + xnef x (iv phi phi₁) = xnef x phi × xnef x phi₁ + xnef x (v phi) = xnef x phi + + is-xnef : {a b c : Obj A } → ( x∈a : Hom A １ a ) → {z : Hom A b c } → ( y : φ {a} x∈a z ) → xnef x∈a {z} y + is-xnef {a} {b} {c} x {z} (i z ne ) = ne + is-xnef x ii = lift tt + is-xnef x (iii t t₁) = ( is-xnef x t , is-xnef x t₁ ) + is-xnef x (iv t t₁) = ( is-xnef x t , is-xnef x t₁ ) + is-xnef x (v t) = is-xnef x t + + toφ : {a ⊤ b c : Obj A } → ( x∈a : Hom A ⊤ a ) → (z : Hom A b c ) → ¬ ( z ≅ x∈a ) → φ {a} x∈a z + toφ {a} {⊤} {b} {c} x∈a z ne = i z ne 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 -- since we have A[x] now, we can proceed the proof on p.64 in some possible future @@ -124,9 +130,9 @@ -- 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 ) + → ((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 = {!!} ki x _ (iii {_} {_} {_} {f₁}{ f₂} fp₁ fp₂ ) 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 )))) ⟩ @@ -148,9 +154,9 @@ 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) (is-xnef (Poly.x 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) (is-xnef (Poly.x g)) ⟩ k (Poly.x g) (Poly.phi g) ∎ -- proof in p.59 Lambek @@ -163,12 +169,12 @@ 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 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 ] fc0 {a} {b} {c} x f' phi with phi - ... | i {_} {_} s = begin + ... | i {_} {_} s ne = begin (s ∙ π') ∙ < ( x ∙ ○ b ) , id1 A b > ≈↑⟨ assoc ⟩ s ∙ (π' ∙ < ( x ∙ ○ b ) , id1 A b >) ≈⟨ cdr (IsCCC.e3b isCCC ) ⟩ s ∙ id1 A b ≈⟨ idR ⟩ @@ -220,27 +226,22 @@ -- 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) → 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 ⟩ - 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 ∙ π' > ) - f' ∙ < k x (i (x ∙ ○ b)) , k x {id1 A b} (i _) > ≈⟨ cdr (π-cong u2 refl-hom) ⟩ -- ( f' ∙ < (x ∙ ○ b) ∙ π' , id1 A b ∙ π' > ) - f' ∙ < k x {x} ii ∙ < π , k x {○ b} (i _) > , k x {id1 A b} (i _) > -- ( f' ∙ < π ∙ < π , (x ∙ ○ b) ∙ π' > , id1 A b ∙ π' > ) + uniq {a} {b} {c} x f phi f' fx=p = sym (begin + k x phi ≈↑⟨ ki x f phi (is-xnef x) ⟩ + 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 ∙ π' > ) + f' ∙ < k x (i (x ∙ ○ b) _) , k x {id1 A b} (i _ _) > ≈⟨ cdr (π-cong u2 refl-hom) ⟩ -- ( f' ∙ < (x ∙ ○ b) ∙ π' , id1 A b ∙ π' > ) + f' ∙ < k x {x} ii ∙ < π , k x {○ b} (i _ _) > , k x {id1 A b} (i _ _) > -- ( f' ∙ < π ∙ < π , (x ∙ ○ b) ∙ π' > , id1 A b ∙ π' > ) ≈⟨ cdr (π-cong (cdr (π-cong refl-hom (car e2))) idL ) ⟩ f' ∙ < π ∙ < π , (○ b ∙ π' ) > , π' > ≈⟨ cdr (π-cong (IsCCC.e3a isCCC) refl-hom) ⟩ f' ∙ < π , π' > ≈⟨ cdr (IsCCC.π-id isCCC) ⟩ f' ∙ id1 A _ ≈⟨ idR ⟩ f' ∎ ) where -- (phi : φ x f) → xnef x phi - xff : ((fp : φ x f) → xnef x fp) → (g : Hom A b a) → (gp : φ x g) → xnef x gp - xff = {!!} - xf : (fp : φ x (x ∙ ○ b)) → xnef x fp - xf = {!!} - u2 : k x {x ∙ ○ b} (i _) ≈ k x {x} ii ∙ < π , k x {○ b} (i _) > - u2 = ki x (x ∙ ○ b) (iv ii (i _)) xf + u2 : k x {x ∙ ○ b} (i _ _) ≈ k x {x} ii ∙ < π , k x {○ b} (i _ _ ) > + u2 = ki x (x ∙ ○ b) (iv ii (i _ _ )) (is-xnef x) -- functional completeness ε form --