Mercurial > hg > Members > kono > Proof > category
diff src/Polynominal.agda @ 1079:d07cfce03236
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 12 May 2021 00:42:14 +0900 |
| parents | 5aa36440e6fe |
| children | c61639f34e7b |
line wrap: on
line diff
--- a/src/Polynominal.agda Tue May 11 22:59:27 2021 +0900 +++ b/src/Polynominal.agda Wed May 12 00:42:14 2021 +0900 @@ -75,29 +75,6 @@ -- all other cases, arguments are reduced to f ∙ π' . --postulate -- x-singleon : {a b c : Obj A} → (f : Poly a c b ) → (x y : Hom A b a) → x ≡ y -- minimul equivalende assumption (variables are the same except its name) - k-cong : {a b c : Obj A} → (f g : Poly a c b ) - → Poly.x f ≡ Poly.x g - → 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 refl f=f with Poly.x f | (Poly.phi f) | (Poly.phi g) - ... | x | i {_} {_} {f'} | i = resp refl-hom f=f - ... | x | i {_} {_} {f'} | ii = {!!} - ... | x | i {_} {_} {h} | iii {_} {_} {_} {f₁} {g₁} t t₁ = begin - k x {h} i ≈⟨⟩ - h ∙ π' ≈⟨ car f=f ⟩ - < f₁ , g₁ > ∙ π' ≈⟨ IsCCC.distr-π isCCC ⟩ - < f₁ ∙ π' , g₁ ∙ π' > ≈⟨⟩ - < k x {f₁} i , k x {g₁} i > ≈⟨ IsCCC.π-cong isCCC (k-cong _ _ refl {!!} ) {!!} ⟩ - < k x t , k x t₁ > ≈⟨⟩ - k x (iii t t₁) ∎ - ... | x | i {_} {_} {f'} | iv t t₁ = {!!} - ... | x | i {_} {_} {f'} | v t = {!!} - ... | x | i {_} {_} {f'} | φ-cong x₁ t = {!!} - ... | _ | ii | t = {!!} - ... | x | iii s s₁ | t = {!!} - ... | x | iv s s₁ | t = {!!} - ... | x | v s | t = {!!} - ... | x | φ-cong x₁ s | t = {!!} - -- we may prove k-cong from x-singleon -- 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=g with Poly.phi f | Poly.phi g @@ -138,6 +115,10 @@ *-cong = IsCCC.*-cong isCCC distr-* = IsCCC.distr-* isCCC e2 = IsCCC.e2 isCCC + idx : {a : Obj A} → {x : Hom A １ a} → x ∙ ○ a ≈ id1 A a + idx {a} {x} = begin + x ∙ ○ a ≈⟨ {!!} ⟩ + id1 A a ∎ -- proof in p.59 Lambek functional-completeness : {a b c : Obj A} ( p : Poly a c b ) → Functional-completeness p @@ -201,13 +182,36 @@ -- -- f ∙ < x ∙ ○ b , id1 A b > ≈ f → f ≈ k x (phi p) -- + ki : {a b c : Obj A} → (x : Hom A １ a) → (f : Hom A b c ) → (fp : φ x {b} {c} f ) → A [ f ∙ π' ≈ k x fp ] + ki x f i = refl-hom + ki {a} x .x ii = begin + x ∙ π' ≈⟨ {!!} ⟩ + x ∙ ○ (a ∧ １) ≈⟨ {!!} ⟩ + x ∙ (○ a ∙ π ) ≈⟨ {!!} ⟩ + (x ∙ ○ a ) ∙ π ≈⟨ {!!} ⟩ + id1 A a ∙ π ≈⟨ {!!} ⟩ + k x ii ∎ + ki x .(< f₁ , f₂ > ) (iii {_} {_} {_} {f₁}{ f₂} fp₁ fp₂ ) = begin + < f₁ , f₂ > ∙ π' ≈⟨ IsCCC.distr-π isCCC ⟩ + < f₁ ∙ π' , f₂ ∙ π' > ≈⟨ π-cong (ki x f₁ fp₁) (ki x f₂ fp₂) ⟩ + k x (iii fp₁ fp₂ ) ∎ + ki x .((A Category.o _) _) (iv {_} {_} {_} {f₁} {f₂} fp fp₁) = begin + (f₁ ∙ f₂ ) ∙ π' ≈⟨ {!!} ⟩ + f₁ ∙ ( f₂ ∙ π') ≈⟨ {!!} ⟩ + f₁ ∙ ( π' ∙ < π , (f₂ ∙ π' ) >) ≈⟨ {!!} ⟩ + (f₁ ∙ π' ) ∙ < π , (f₂ ∙ π' ) > ≈⟨ {!!} ⟩ + k x fp ∙ < π , k x fp₁ > ≈⟨⟩ + k x (iv fp fp₁ ) ∎ + ki x .((C CCC.*) _) (v fp) = {!!} + ki x f (φ-cong x₁ fp) = {!!} 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 = sym (begin - k x phi ≈↑⟨ k-cong record {x = x ; f = _ ; phi = i } record {x = x ; f = _ ; phi = phi } refl fx=p ⟩ + k x phi ≈↑⟨ ki 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 (k-cong record {x = x ; f = _ ; phi = i } record {x = x ; f = _ ; phi = iv ii i } refl refl-hom ) refl-hom) ⟩ + ≈⟨ 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 ) ⟩ @@ -216,6 +220,35 @@ f' ∙ id1 A _ ≈⟨ idR ⟩ f' ∎ ) + ki : {a b c : Obj A} → (x : Hom A １ a) → (f : Hom A b c ) → (fp : φ x {b} {c} f ) → A [ f ∙ π' ≈ k x fp ] + ki = {!!} + k-cong : {a b c : Obj A} → (f g : Poly a c b ) + → Poly.x f ≡ Poly.x g + → 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 refl f=f = kcong (Poly.x f ) (Poly.f f) (Poly.f g) f=f ( Poly.phi f ) ( Poly.phi g) where + kcong : {a b c : Obj A} → (x : Hom A １ a) → (f g : Hom A b c ) → (f=g : f ≈ g ) → (fp : φ x {b} {c} f )( gp : φ x {b} {c} g ) → A [ k x fp ≈ k x gp ] + kcong {a} {b} {c} x f g f=g i i = resp refl-hom f=g + kcong {a} {.(CCC.１ C)} {.a} x f .x f=g i ii = begin + k x {f} i ≈⟨⟩ + f ∙ π' ≈⟨ car f=g ⟩ + x ∙ π' ≈⟨ ki x x ii ⟩ + k x ii ∎ + kcong {a} {b} {.((C CCC.∧ _) _)} x f .(< g₁ , g₂ >) f=g i (iii {_} {_} {_} {g₁} {g₂} gp₁ gp₂) = begin + k x i ≈⟨ car f=g ⟩ + < g₁ , g₂ > ∙ π' ≈⟨ IsCCC.distr-π isCCC ⟩ + < g₁ ∙ π' , g₂ ∙ π' > ≈⟨ IsCCC.π-cong isCCC (ki x _ gp₁ ) (ki x _ gp₂) ⟩ + < k x gp₁ , k x gp₂ > ≈⟨⟩ + k x (iii gp₁ gp₂) ∎ + kcong {a} {b} {c} x f .((A Category.o _) _) f=g i (iv gp gp₁) = {!!} + kcong {a} {b} {.((C CCC.<= _) _)} x f .((C CCC.*) _) f=g i (v gp) = {!!} + kcong {a} {b} {c} x f g f=g i (φ-cong x₁ gp) = {!!} + kcong {a} {.(CCC.１ C)} {.a} x .x g f=g ii gp = {!!} + kcong {a} {b} {.((C CCC.∧ _) _)} x .(CCC.< C , _ > _) g f=g (iii fp fp₁) gp = {!!} + kcong {a} {b} {c} x .((A Category.o _) _) g f=g (iv fp fp₁) gp = {!!} + kcong {a} {b} {.((C CCC.<= _) _)} x .((C CCC.*) _) g f=g (v fp) gp = {!!} + kcong {a} {b} {c} x f g f=g (φ-cong x₁ fp) gp = {!!} + + -- functional completeness ε form -- -- g : Hom A １ (b <= a) fun : Hom A (a ∧ １) c