# HG changeset patch # User Shinji KONO # Date 1621117951 -32400 # Node ID 372ea20015e8cb564fa53f7b435b4e3cdf72bc03 # Parent caba080b1dedb0d58ecc3a7cd9aa5ef4c1054ee6 ... diff -r caba080b1ded -r 372ea20015e8 src/Polynominal.agda --- a/src/Polynominal.agda Sat May 15 11:33:07 2021 +0900 +++ b/src/Polynominal.agda Sun May 16 07:32:31 2021 +0900 @@ -69,7 +69,7 @@ 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} {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₁ @@ -79,8 +79,8 @@ field x : Hom A １ a -- λ x f : Hom A b c - phi : φ x {b} {c} f -- construction of f - nf : xnef x phi + 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 @@ -95,8 +95,8 @@ field 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 ] + uniq : ( f : Hom A (a ∧ b) c) → A [ f ∙ < x ∙ ○ b , id1 A b > ≈ Poly.f p ] + → A [ f ≈ fun ] -- ε form -- f ≡ λ (x ∈ a) → φ x , ∃ (f : b <= a) → f ∙ x ≈ φ x @@ -109,7 +109,7 @@ field isSelect : A [ ε ∙ < g , Poly.x φ > ≈ Poly.f φ ] isUnique : (f : Hom A １ (b <= a) ) → A [ ε ∙ < f , Poly.x φ > ≈ Poly.f φ ] - → A [ g ≈ f ] + → A [ g ≈ f ] -- we should open IsCCC isCCC π-cong = IsCCC.π-cong isCCC @@ -123,33 +123,34 @@ -- 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 ∙ π' . - 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 + 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 < f₁ , f₂ > ∙ π' ≈⟨ IsCCC.distr-π isCCC ⟩ - < f₁ ∙ π' , f₂ ∙ π' > ≈⟨ π-cong (ki x f₁ fp₁ (proj₁ ne) {!!} ) (ki x f₂ fp₂ (proj₂ ne ) {!!} ) ⟩ - k x (iii fp₁ fp₂ ) ∎ - ki x _ (iv {_} {_} {_} {f₁} {f₂} fp fp₁) ne _ = begin + < f₁ ∙ π' , f₂ ∙ π' > ≈⟨ π-cong (ki x f₁ fp₁ (λ fp → proj₁ (ne (iii fp fp₂ )))) (ki x f₂ fp₂ (λ fp → proj₂ (ne (iii fp₁ fp )))) ⟩ + k x (iii fp₁ fp₂ ) ∎ + 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 x _ fp₁ (proj₂ ne) {!!} ) ) (ki x _ fp (proj₁ ne) {!!}) ⟩ + (f₁ ∙ π' ) ∙ < π , (f₂ ∙ π' ) > ≈⟨ resp (π-cong refl-hom (ki x _ fp₁ (λ p → proj₂ (ne (iv fp p ) ) )) ) (ki x _ fp (λ p → proj₁ (ne (iv p fp₁ ) ))) ⟩ k x fp ∙ < π , k x fp₁ > ≈⟨⟩ k x (iv fp fp₁ ) ∎ - ki x _ (v {_} {_} {_} {f} fp) ne fx = begin + ki x _ (v {_} {_} {_} {f} fp) ne = begin (f *) ∙ π' ≈⟨ distr-* ⟩ ( f ∙ < π' ∙ π , π' > ) * ≈↑⟨ *-cong (cdr (IsCCC.e3b isCCC)) ⟩ ( f ∙ ( π' ∙ < π ∙ π , < π' ∙ π , π' > > ) ) * ≈⟨ *-cong assoc ⟩ - ( (f ∙ π') ∙ < π ∙ π , < π' ∙ π , π' > > ) * ≈⟨ *-cong ( car ( ki x _ fp ne {!!} )) ⟩ + ( (f ∙ π') ∙ < π ∙ π , < π' ∙ π , π' > > ) * ≈⟨ *-cong ( car ( ki x _ fp (λ p → ne (v p )) )) ⟩ ( 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 @@ -162,7 +163,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 ] @@ -219,14 +220,19 @@ -- 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) - → xnef x phi + → ((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 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) ⟩ + ≈⟨ cdr (begin + k x (iii (i (x ∙ ○ b)) (i (id1 A _))) ≈⟨⟩ + < ( x ∙ (○ b)) ∙ π' , id1 A _ ∙ π' > ≈⟨ π-cong {!!} refl-hom ⟩ + < π , id1 A _ ∙ π' > ≈↑⟨ π-cong (IsCCC.e3a isCCC) refl-hom ⟩ + < π ∙ < π , (○ b) ∙ π' > , id1 A _ ∙ π' > ≈⟨⟩ + < k x (iv ii (i (○ b))) , k x (i (id1 A _)) > ∎ ) ⟩ 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 ) ⟩