Mercurial > hg > Members > kono > Proof > category
changeset 1055:c61674a18a2e
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 19 Apr 2021 09:21:59 +0900 |
| parents | 31c98ae4a772 |
| children | 9272cafd1675 |
| files | src/Polynominal.agda |
| diffstat | 1 files changed, 37 insertions(+), 44 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Polynominal.agda Mon Apr 19 07:50:21 2021 +0900 +++ b/src/Polynominal.agda Mon Apr 19 09:21:59 2021 +0900 @@ -91,63 +91,42 @@ *-cong = IsCCC.*-cong isCCC e2 = IsCCC.e2 isCCC - -- functional completeness - FC : {a b : Obj A} → (φ : Poly a b １ ) → Fc {a} {b} φ - FC {a} {b} φ = record { - sl = A [ k (Poly.x φ ) (Poly.phi φ) o < id1 A _ , ○ a > ] - ; isSelect = begin - ε ∙ < (( ((k (Poly.x φ) (Poly.phi φ)∙ < id1 A _ , ○ a > ) ∙ π ) ∙ < id1 A a , ○ a > ) ∙ π') * , Poly.x φ > ≈↑⟨ cdr (π-cong (*-cong (car assoc)) refl-hom) ⟩ - ε ∙ < (((k (Poly.x φ) (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ (π ∙ (< id1 A _ , ○ a >))) ∙ π' ) * , Poly.x φ > ≈⟨ {!!} ⟩ - ε ∙ < ( (k (Poly.x φ) (Poly.phi φ)∙ < id1 A _ , ○ a > ) ∙ (id1 A _ ∙ π' ) ) * , Poly.x φ > ≈⟨ {!!} ⟩ - ε ∙ ( < ((k (Poly.x φ ) (Poly.phi φ) * ) ∙ π ) , π' > ∙ < Poly.x φ ∙ ○ １ , id1 A １ > ) ≈⟨ assoc ⟩ - (ε ∙ < ((k (Poly.x φ ) (Poly.phi φ) * ) ∙ π ) , π' > ) ∙ < Poly.x φ ∙ ○ １ , id1 A １ > ≈⟨ car ( IsCCC.e4a isCCC ) ⟩ - k (Poly.x φ ) (Poly.phi φ) ∙ < Poly.x φ ∙ ○ １ , id1 A １ > ≈⟨ fc0 φ ⟩ - Poly.f φ ∎ - ; isUnique = {!!} - } where - 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 = {!!} - 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 + ; 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 eq } where - 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 + 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 (s ∙ π') ∙ < ( x ∙ ○ b ) , id1 A b > ≈↑⟨ assoc ⟩ s ∙ (π' ∙ < ( x ∙ ○ b ) , id1 A b >) ≈⟨ cdr (IsCCC.e3b isCCC ) ⟩ s ∙ id1 A b ≈⟨ idR ⟩ - s ∎ where - open Poly p + s ∎ ... | ii = begin π ∙ < ( x ∙ ○ b ) , id1 A b > ≈⟨ IsCCC.e3a isCCC ⟩ x ∙ ○ b ≈↑⟨ cdr (e2 ) ⟩ x ∙ id1 A b ≈⟨ idR ⟩ - x ∎ where - open φ - open Poly p + x ∎ ... | 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 { f = f ; phi = y } ) (fc0 record { f = g ; phi = z } ) ⟩ + ≈⟨ π-cong (fc0 x f y ) (fc0 x g z ) ⟩ < f , g > ≈⟨⟩ - {!!} ∎ where - x = Poly.x p + f' ∎ ... | 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 { f = g ; phi = z ; x = x } ) ) ⟩ + ≈⟨ cdr (π-cong (IsCCC.e3a isCCC) (fc0 x g z ) ) ⟩ 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 { f = f ; phi = y }) ⟩ - f ∙ g ∎ where - x = Poly.x p + (k x y ∙ < x ∙ ○ d , id1 A d > ) ∙ g ≈⟨ car (fc0 x f y ) ⟩ + f ∙ g ∎ ... | 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 @@ -166,21 +145,19 @@ ≈⟨ 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 { f = f ; phi = y} ⟩ + k x y ∙ < x ∙ ○ _ , id1 A _ > ≈⟨ fc0 x f y ⟩ 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 * ∎ + ... | φ-cong {_} {_} {f} {f'} f=f' y = trans-hom (fc0 x f y ) f=f' -- -- f ∙ < x ∙ ○ b , id1 A b > ≈ f → f ≈ k x (phi 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 + 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) → + A [ f' ∙ < x ∙ ○ b , id1 A b > ≈ f ] → A [ f' ≈ k x phi ] + uniq {a} {b} {c} x f' phi f fx=p with phi ... | i = sym (begin k x i ≈⟨⟩ - Poly.f p ∙ π' ≈↑⟨ car fx=p ⟩ + f' ∙ π' ≈↑⟨ 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 ∙ π' > ≈⟨⟩ @@ -189,13 +166,29 @@ f ∙ < π ∙ < π , (○ b ∙ π' ) > , π' > ≈⟨ cdr (π-cong (IsCCC.e3a isCCC) refl-hom) ⟩ f ∙ < π , π' > ≈⟨ cdr (IsCCC.π-id isCCC) ⟩ f ∙ id1 A _ ≈⟨ idR ⟩ - f ∎ ) where - x = Poly.x p + f ∎ ) ... | ii = {!!} ... | iii t t₁ = {!!} ... | iv t t₁ = {!!} ... | v t = {!!} ... | φ-cong x₁ t = {!!} + -- functional completeness ε form + FC : {a b : Obj A} → (φ : Poly a b １ ) → Fc {a} {b} φ + FC {a} {b} φ = record { + sl = A [ k (Poly.x φ ) (Poly.phi φ) o < id1 A _ , ○ a > ] + ; isSelect = begin + ε ∙ < (( ((k (Poly.x φ) (Poly.phi φ)∙ < id1 A _ , ○ a > ) ∙ π ) ∙ < id1 A a , ○ a > ) ∙ π') * , Poly.x φ > ≈↑⟨ cdr (π-cong (*-cong (car assoc)) refl-hom) ⟩ + ε ∙ < (((k (Poly.x φ) (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ (π ∙ (< id1 A _ , ○ a >))) ∙ π' ) * , Poly.x φ > ≈⟨ {!!} ⟩ + ε ∙ < ( (k (Poly.x φ) (Poly.phi φ)∙ < id1 A _ , ○ a > ) ∙ (id1 A _ ∙ π' ) ) * , Poly.x φ > ≈⟨ {!!} ⟩ + ε ∙ ( < ((k (Poly.x φ ) (Poly.phi φ) * ) ∙ π ) , π' > ∙ < Poly.x φ ∙ ○ １ , id1 A １ > ) ≈⟨ assoc ⟩ + (ε ∙ < ((k (Poly.x φ ) (Poly.phi φ) * ) ∙ π ) , π' > ) ∙ < Poly.x φ ∙ ○ １ , id1 A １ > ≈⟨ car ( IsCCC.e4a isCCC ) ⟩ + k (Poly.x φ ) (Poly.phi φ) ∙ < Poly.x φ ∙ ○ １ , id1 A １ > ≈⟨ fc0 φ ⟩ + Poly.f φ ∎ + ; isUnique = {!!} + } where + 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 p = Functional-completeness.fp (functional-completeness p) + -- end