Mercurial > hg > Members > kono > Proof > category
changeset 1056:9272cafd1675
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 19 Apr 2021 16:05:52 +0900 |
| parents | c61674a18a2e |
| children | 88f441d5bb18 |
| files | src/Polynominal.agda |
| diffstat | 1 files changed, 15 insertions(+), 18 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Polynominal.agda Mon Apr 19 09:21:59 2021 +0900 +++ b/src/Polynominal.agda Mon Apr 19 16:05:52 2021 +0900 @@ -152,26 +152,23 @@ -- -- f ∙ < x ∙ ○ b , id1 A b > ≈ f → f ≈ k x (phi p) -- + k-cong : {a b c : Obj A} → (x : Hom A １ a) → (f g : Hom A b c ) → A [ f ≈ g ] → (fp : φ x {b} {c} f ) (gp : φ x {b} {c} g ) + → A [ k x fp ≈ k x gp ] + k-cong = {!!} 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 ≈⟨⟩ - 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 ∙ π' > ≈⟨⟩ - 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 ∎ ) - ... | ii = {!!} - ... | iii t t₁ = {!!} - ... | iv t t₁ = {!!} - ... | v t = {!!} - ... | φ-cong x₁ t = {!!} + uniq {a} {b} {c} x f phi f' fx=p = sym (begin + -- k x phi ≈⟨ uniq x (f ∙ < x ∙ ○ b , id1 A b > ) i (k x phi) {!!} ⟩ + k x phi ≈⟨ k-cong x _ _ (sym fx=p) phi i ⟩ + 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 (trans-hom (IsCCC.e3a isCCC) k x {< x ∙ ○ b , id1 A b >} (iii i 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) ⟩ + f' ∙ id1 A _ ≈⟨ idR ⟩ + f' ∎ ) -- functional completeness ε form FC : {a b : Obj A} → (φ : Poly a b １ ) → Fc {a} {b} φ