Mercurial > hg > Members > kono > Proof > category
changeset 1054:31c98ae4a772
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 19 Apr 2021 07:50:21 +0900 |
| parents | 9986af5bbd6f |
| children | c61674a18a2e |
| files | src/Polynominal.agda |
| diffstat | 1 files changed, 51 insertions(+), 48 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Polynominal.agda Mon Apr 19 05:21:41 2021 +0900 +++ b/src/Polynominal.agda Mon Apr 19 07:50:21 2021 +0900 @@ -54,18 +54,11 @@ 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 - record Poly (a b ⊤ : Obj A ) : Set (c₁ ⊔ c₂ ⊔ ℓ) where + record Poly (a c b : Obj A ) : Set (c₁ ⊔ c₂ ⊔ ℓ) where field - x : Hom A ⊤ a - f : Hom A ⊤ b - phi : φ x {⊤} {b} f - - record PHom {a ⊤ : Obj A } { x : Hom A ⊤ a } (b c : Obj A) : Set (c₁ ⊔ c₂ ⊔ ℓ) where - field - hom : Hom A b c - phi : φ x {b} {c} hom - - open PHom + x : Hom A １ a + f : Hom A b c + phi : φ x {b} {c} f -- -- Proposition 6.1 @@ -74,12 +67,13 @@ -- category A there is a unique arrow f : a ∧ b → c in A such that f ∙ < x ∙ ○ b , id1 A b > ≈ ψ(x). -- - record Functional-completeness {a : Obj A} ( x : Hom A １ a ) : Set (c₁ ⊔ c₂ ⊔ ℓ) where + record Functional-completeness {a b c : Obj A} ( p : Poly a c b ) : Set (c₁ ⊔ c₂ ⊔ ℓ) where + x = Poly.x p field - fun : {b c : Obj A} → PHom {a} {１} {x} b c → Hom A (a ∧ b) c - fp : {b c : Obj A} → (p : PHom b c) → A [ fun p ∙ < x ∙ ○ b , id1 A b > ≈ hom p ] - uniq : {b c : Obj A} → (p : PHom b c) → (f : Hom A (a ∧ b) c) → A [ f ∙ < x ∙ ○ b , id1 A b > ≈ hom p ] - → A [ f ≈ fun p ] + fun : Hom A (a ∧ b) c + fp : A [ fun ∙ < x ∙ ○ b , id1 A b > ≈ Poly.f p ] + uniq : ( f : Hom A (a ∧ b) c) → A [ f ∙ < x ∙ ○ b , id1 A b > ≈ Poly.f p ] + → A [ f ≈ fun ] -- f ≡ λ (x ∈ a) → φ x , ∃ (f : b <= a) → f ∙ x ≈ φ x record Fc {a b : Obj A } ( φ : Poly a b １ ) @@ -114,43 +108,46 @@ 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 ] fc0 = {!!} - -- {-# TERMINATING #-} - functional-completeness : {a : Obj A} ( x : Hom A １ a ) → Functional-completeness x - functional-completeness {a} x = record { - fun = λ y → k x (phi y) - ; fp = fc0 - ; uniq = uniq + functional-completeness : {a b c : Obj A} ( p : Poly a c b ) → Functional-completeness p + functional-completeness {a} {b} {c} p = record { + fun = k (Poly.x p) (Poly.phi p) + ; fp = fc0 p + ; uniq = uniq p } where - open φ - fc0 : {b c : Obj A} (p : PHom b c) → A [ k x (phi p) ∙ < x ∙ ○ b , id1 A b > ≈ hom p ] - fc0 {b} {c} p with phi p + fc0 : {a b c : Obj A} ( p : Poly a c b ) → A [ k (Poly.x p) (Poly.phi p) ∙ < (Poly.x p) ∙ ○ b , id1 A b > ≈ Poly.f p ] + fc0 {a} {b} {c} p with Poly.phi p ... | 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 ⟩ - s ∎ + s ∎ where + open Poly p ... | ii = begin π ∙ < ( x ∙ ○ b ) , id1 A b > ≈⟨ IsCCC.e3a isCCC ⟩ x ∙ ○ b ≈↑⟨ cdr (e2 ) ⟩ x ∙ id1 A b ≈⟨ idR ⟩ - x ∎ + x ∎ where + open φ + open Poly p ... | iii {_} {_} {_} {f} {g} y z = begin < k x y , k x z > ∙ < (x ∙ ○ b ) , id1 A b > ≈⟨ IsCCC.distr-π isCCC ⟩ < k x y ∙ < (x ∙ ○ b ) , id1 A b > , k x z ∙ < (x ∙ ○ b ) , id1 A b > > - ≈⟨ π-cong (fc0 record { hom = f ; phi = y } ) (fc0 record { hom = g ; phi = z } ) ⟩ + ≈⟨ π-cong (fc0 record { f = f ; phi = y } ) (fc0 record { f = g ; phi = z } ) ⟩ < f , g > ≈⟨⟩ - hom p ∎ + {!!} ∎ where + x = Poly.x p ... | iv {_} {_} {d} {f} {g} y z = begin (k x y ∙ < π , k x z >) ∙ < ( x ∙ ○ b ) , id1 A b > ≈↑⟨ assoc ⟩ k x y ∙ ( < π , k x z > ∙ < ( x ∙ ○ b ) , id1 A b > ) ≈⟨ cdr (IsCCC.distr-π isCCC) ⟩ k x y ∙ ( < π ∙ < ( x ∙ ○ b ) , id1 A b > , k x z ∙ < ( x ∙ ○ b ) , id1 A b > > ) - ≈⟨ cdr (π-cong (IsCCC.e3a isCCC) (fc0 record { hom = g ; phi = z} ) ) ⟩ + ≈⟨ cdr (π-cong (IsCCC.e3a isCCC) (fc0 record { f = g ; phi = z ; x = x } ) ) ⟩ k x y ∙ ( < x ∙ ○ b , g > ) ≈↑⟨ cdr (π-cong (cdr (e2)) refl-hom ) ⟩ k x y ∙ ( < x ∙ ( ○ d ∙ g ) , g > ) ≈⟨ cdr (π-cong assoc (sym idL)) ⟩ k x y ∙ ( < (x ∙ ○ d) ∙ g , id1 A d ∙ g > ) ≈↑⟨ cdr (IsCCC.distr-π isCCC) ⟩ k x y ∙ ( < x ∙ ○ d , id1 A d > ∙ g ) ≈⟨ assoc ⟩ - (k x y ∙ < x ∙ ○ d , id1 A d > ) ∙ g ≈⟨ car (fc0 record { hom = f ; phi = y }) ⟩ - f ∙ g ∎ + (k x y ∙ < x ∙ ○ d , id1 A d > ) ∙ g ≈⟨ car (fc0 record { f = f ; phi = y }) ⟩ + f ∙ g ∎ where + x = Poly.x p ... | v {_} {_} {_} {f} y = begin ( (k x y ∙ < π ∙ π , < π' ∙ π , π' > >) *) ∙ < x ∙ (○ b) , id1 A b > ≈⟨ IsCCC.distr-* isCCC ⟩ ( (k x y ∙ < π ∙ π , < π' ∙ π , π' > >) ∙ < < x ∙ ○ b , id1 A _ > ∙ π , π' > ) * ≈⟨ IsCCC.*-cong isCCC ( begin @@ -169,30 +166,36 @@ ≈⟨ cdr (π-cong (car (IsCCC.e3a isCCC)) (π-cong (car (IsCCC.e3b isCCC)) refl-hom )) ⟩ k x y ∙ < ( (x ∙ ○ b ) ∙ π ) , < id1 A _ ∙ π , π' > > ≈⟨ cdr (π-cong (sym assoc) (π-cong idL refl-hom )) ⟩ k x y ∙ < x ∙ (○ b ∙ π ) , < π , π' > > ≈⟨ cdr (π-cong (cdr (e2)) (IsCCC.π-id isCCC) ) ⟩ - k x y ∙ < x ∙ ○ _ , id1 A _ > ≈⟨ fc0 record { hom = f ; phi = y} ⟩ + k x y ∙ < x ∙ ○ _ , id1 A _ > ≈⟨ fc0 record { f = f ; phi = y} ⟩ f ∎ ) ⟩ - f * ∎ - ... | φ-cong {_} {_} {f} {f'} f=f' y = trans-hom (fc0 record { hom = f ; phi = y}) f=f' + f * ∎ where + open φ + x = Poly.x p + ... | φ-cong {_} {_} {f} {f'} f=f' y = trans-hom (fc0 record { f = f ; phi = y}) f=f' -- - -- f ∙ < x ∙ ○ b , id1 A b > ≈ hom p → f ≈ k x (phi p) + -- f ∙ < x ∙ ○ b , id1 A b > ≈ f → f ≈ k x (phi p) -- - uniq : {b c : Obj A} (p : PHom b c) (f : Hom A (a ∧ b) c) → - A [ f ∙ < x ∙ ○ b , id1 A b > ≈ hom p ] → A [ f ≈ k x (phi p) ] - uniq {b} {c} p f fx=p = sym (begin - k x (phi p) ≈⟨ fc1 p ⟩ - k x {hom p} i ≈⟨⟩ - hom p ∙ π' ≈↑⟨ car fx=p ⟩ + uniq : {a b c : Obj A} (p : Poly a c b) (f' : Hom A (a ∧ b) c) → + A [ f' ∙ < (Poly.x p) ∙ ○ b , id1 A b > ≈ Poly.f p ] → A [ f' ≈ k (Poly.x p) (Poly.phi p) ] + uniq {a} {b} {c} p f fx=p with Poly.phi p + ... | i = sym (begin + k x i ≈⟨⟩ + Poly.f p ∙ π' ≈↑⟨ car fx=p ⟩ (f ∙ < x ∙ ○ b , id1 A b > ) ∙ π' ≈↑⟨ assoc ⟩ f ∙ (< x ∙ ○ b , id1 A b > ∙ π') ≈⟨ cdr (IsCCC.distr-π isCCC) ⟩ f ∙ < (x ∙ ○ b) ∙ π' , id1 A b ∙ π' > ≈⟨⟩ - f ∙ < k x {x ∙ ○ b} i , id1 A b ∙ π' > ≈⟨ cdr (π-cong (sym (fc1 record { hom = x ∙ ○ b ; phi = iv ii i } )) refl-hom) ⟩ - f ∙ < k x (phi record { hom = x ∙ ○ b ; phi = iv ii i }) , id1 A b ∙ π' > ≈⟨ cdr (π-cong refl-hom idL) ⟩ + f ∙ < k x {x ∙ ○ b} i , id1 A b ∙ π' > ≈⟨ cdr (π-cong (sym {!!}) refl-hom) ⟩ + f ∙ < k x (Poly.phi record { f = x ∙ ○ b ; phi = iv ii i }) , id1 A b ∙ π' > ≈⟨ cdr (π-cong refl-hom idL) ⟩ f ∙ < π ∙ < π , (○ b ∙ π' ) > , π' > ≈⟨ cdr (π-cong (IsCCC.e3a isCCC) refl-hom) ⟩ f ∙ < π , π' > ≈⟨ cdr (IsCCC.π-id isCCC) ⟩ f ∙ id1 A _ ≈⟨ idR ⟩ - f ∎ ) where - fc1 : {b c : Obj A} (p : PHom b c) → A [ k x (phi p) ≈ k x {hom p} i ] -- it looks like (*) in page 60 - fc1 {b} {c} p = {!!} - + f ∎ ) where + x = Poly.x p + ... | ii = {!!} + ... | iii t t₁ = {!!} + ... | iv t t₁ = {!!} + ... | v t = {!!} + ... | φ-cong x₁ t = {!!} + -- end