# HG changeset patch # User Shinji KONO # Date 1621045987 -32400 # Node ID caba080b1dedb0d58ecc3a7cd9aa5ef4c1054ee6 # Parent a59d7f0edeae6417242df5de2563efd24f6907e6 ... diff -r a59d7f0edeae -r caba080b1ded src/Polynominal.agda --- a/src/Polynominal.agda Wed May 12 21:14:24 2021 +0900 +++ b/src/Polynominal.agda Sat May 15 11:33:07 2021 +0900 @@ -5,6 +5,9 @@ open import Level open import HomReasoning open import cat-utility +open import Relation.Nullary +open import Data.Empty +open import Data.Product renaming ( <_,_> to ⟪_,_⟫ ) module Polynominal { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( C : CCC A ) where @@ -25,12 +28,16 @@ -- that is, a subscategory of A[x]. -- -- i : {b c : Obj A} {k : Hom A b c } → sub k → φ x k + -- sub k is ¬ ( k ≈ x ), we cannot write this because b≡⊤ c≡a is forced -- -- this makes a few changes, but we don't care. -- from page. 51 -- + + 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} (k : Hom A b c ) → φ x k 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 ) @@ -43,14 +50,14 @@ -- 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 + toφ {a} {⊤} {b} {c} x∈a z = i z -- The Polynominal arrow -- λ term in A -- @@ -60,12 +67,20 @@ -- if we use equality on f as in A, Poly is ovioously Hom c b of a Category. -- 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} 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 + 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 - idx : {a : Obj A} → {x : Hom A １ a} → x ∙ ○ a ≈ id1 A a -- minimum equivalence + nf : xnef x phi -- since we have A[x] now, we can proceed the proof on p.64 in some possible future @@ -108,48 +123,33 @@ -- we have (x y : Hom A １ a) → x ≈ y (minimul equivalende assumption) in record Poly. this makes all k x ii case valid -- all other cases, arguments are reduced to f ∙ π' . - mineq : {a b c : Obj A } → Poly a b c → (x y : Hom A １ a) → x ≈ y - mineq {a} p x y = begin - x ≈↑⟨ idR ⟩ - x ∙ id1 A １ ≈⟨ cdr e2 ⟩ - x ∙ ○ _ ≈↑⟨ cdr e2 ⟩ - x ∙ (○ a ∙ y ) ≈⟨ assoc ⟩ - (x ∙ ○ a ) ∙ y ≈⟨ car (Poly.idx p) ⟩ - id1 A _ ∙ y ≈⟨ idL ⟩ - y ∎ - ki : {a b b' c c' : Obj A} → Poly a c' b' → (x : Hom A １ a) → (f : Hom A b c ) → (fp : φ x {b} {c} f ) → A [ f ∙ π' ≈ k x fp ] - ki p x f i = refl-hom - ki {a} p x .x ii = begin - x ∙ π' ≈⟨ cdr e2 ⟩ - x ∙ ○ (a ∧ １) ≈↑⟨ cdr e2 ⟩ - x ∙ (○ a ∙ π ) ≈⟨ assoc ⟩ - (x ∙ ○ a ) ∙ π ≈⟨ car (Poly.idx p) ⟩ -- smallest equivalence - id1 A a ∙ π ≈⟨ idL ⟩ - k x ii ∎ - ki p x _ (iii {_} {_} {_} {f₁}{ f₂} fp₁ fp₂ ) = begin + 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 ] + ki x f (i _) _ _ = refl-hom + ki {a} x .x ii ne fx = ⊥-elim ( fx HE.refl ) + ki x _ (iii {_} {_} {_} {f₁}{ f₂} fp₁ fp₂ ) ne fx = begin < f₁ , f₂ > ∙ π' ≈⟨ IsCCC.distr-π isCCC ⟩ - < f₁ ∙ π' , f₂ ∙ π' > ≈⟨ π-cong (ki p x f₁ fp₁) (ki p x f₂ fp₂) ⟩ + < f₁ ∙ π' , f₂ ∙ π' > ≈⟨ π-cong (ki x f₁ fp₁ (proj₁ ne) {!!} ) (ki x f₂ fp₂ (proj₂ ne ) {!!} ) ⟩ k x (iii fp₁ fp₂ ) ∎ - ki p x _ (iv {_} {_} {_} {f₁} {f₂} fp fp₁) = begin + ki x _ (iv {_} {_} {_} {f₁} {f₂} fp fp₁) ne _ = begin (f₁ ∙ f₂ ) ∙ π' ≈↑⟨ assoc ⟩ f₁ ∙ ( f₂ ∙ π') ≈↑⟨ cdr (IsCCC.e3b isCCC) ⟩ f₁ ∙ ( π' ∙ < π , (f₂ ∙ π' ) >) ≈⟨ assoc ⟩ - (f₁ ∙ π' ) ∙ < π , (f₂ ∙ π' ) > ≈⟨ resp (π-cong refl-hom (ki p x _ fp₁) ) (ki p x _ fp) ⟩ + (f₁ ∙ π' ) ∙ < π , (f₂ ∙ π' ) > ≈⟨ resp (π-cong refl-hom (ki x _ fp₁ (proj₂ ne) {!!} ) ) (ki x _ fp (proj₁ ne) {!!}) ⟩ k x fp ∙ < π , k x fp₁ > ≈⟨⟩ k x (iv fp fp₁ ) ∎ - ki p x _ (v {_} {_} {_} {f} fp) = begin + ki x _ (v {_} {_} {_} {f} fp) ne fx = begin (f *) ∙ π' ≈⟨ distr-* ⟩ ( f ∙ < π' ∙ π , π' > ) * ≈↑⟨ *-cong (cdr (IsCCC.e3b isCCC)) ⟩ ( f ∙ ( π' ∙ < π ∙ π , < π' ∙ π , π' > > ) ) * ≈⟨ *-cong assoc ⟩ - ( (f ∙ π') ∙ < π ∙ π , < π' ∙ π , π' > > ) * ≈⟨ *-cong ( car ( ki p x _ fp)) ⟩ + ( (f ∙ π') ∙ < π ∙ π , < π' ∙ π , π' > > ) * ≈⟨ *-cong ( car ( ki x _ fp ne {!!} )) ⟩ ( 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 f (Poly.x f) _ (Poly.phi 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 f (Poly.x g) _ (Poly.phi 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 @@ -162,12 +162,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 p (Poly.x p) (Poly.f p) (Poly.phi p) f 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 ] fc0 {a} {b} {c} x f' phi with phi - ... | i {_} {_} {s} = begin + ... | i {_} {_} s = begin (s ∙ π') ∙ < ( x ∙ ○ b ) , id1 A b > ≈↑⟨ assoc ⟩ s ∙ (π' ∙ < ( x ∙ ○ b ) , id1 A b >) ≈⟨ cdr (IsCCC.e3b isCCC ) ⟩ s ∙ id1 A b ≈⟨ idR ⟩ @@ -218,16 +218,17 @@ -- -- f ∙ < x ∙ ○ b , id1 A b > ≈ f → f ≈ k x (phi p) -- - uniq : {a b c : Obj A} → (p : Poly a c b) → (x : Hom A １ a) (f : Hom A b c) (phi : φ x {b} {c} f ) (f' : Hom A (a ∧ b) c) → - A [ f' ∙ < x ∙ ○ b , id1 A b > ≈ f ] → A [ f' ≈ k x phi ] - uniq {a} {b} {c} p x f phi f' fx=p = sym (begin - k x phi ≈↑⟨ ki p x f phi ⟩ - 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 ∙ π' > ) - ≈⟨ cdr (π-cong (ki p x ( x ∙ ○ b) (iv ii i) ) refl-hom) ⟩ - f' ∙ < k x {x ∙ ○ b} (iv ii i ) , k x {id1 A b} i > ≈⟨ refl-hom ⟩ - 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 : Obj A} → (x : Hom A １ a) (f : Hom A b c) (phi : φ x {b} {c} f ) (f' : Hom A (a ∧ b) c) + → 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 ∙ π' > ) + ≈⟨ cdr (π-cong (ki x ( x ∙ ○ b) (iv ii (i _) ) {!!} {!!} ) refl-hom) ⟩ + f' ∙ < k x {x ∙ ○ b} (iv ii (i _) ) , k x {id1 A b} (i _) > ≈⟨ refl-hom ⟩ + 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) ⟩