Mercurial > hg > Members > kono > Proof > category
changeset 970:72b6b4577911
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 26 Feb 2021 12:19:58 +0900 |
| parents | 6548572b7089 |
| children | 9746e93a8c31 |
| files | src/Polynominal.agda |
| diffstat | 1 files changed, 42 insertions(+), 6 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Polynominal.agda Fri Feb 26 02:08:22 2021 +0900 +++ b/src/Polynominal.agda Fri Feb 26 12:19:58 2021 +0900 @@ -88,6 +88,10 @@ SCat = record { Obj = Obj A ; Hom = SHom ; _o_ = _*_ ; _≈_ = _⋍_ ; Id = λ {a} → S-id a ; isCategory = isSCat } open CCC.CCC C + open coMonad + open Functor + open NTrans + open import Category.Cat SA : (a : Obj A) → Functor A A SA a = record { @@ -118,17 +122,49 @@ SM : (a : Obj A) → coMonad A (SA a) SM a = record { - δ = record { TMap = λ x → < π , id1 A _ > ; isNTrans = record { commute = {!!} } } - ; ε = record { TMap = λ x → π' ; isNTrans = record { commute = {!!} } } + δ = record { TMap = λ x → < π , id1 A _ > ; isNTrans = record { commute = δ-comm} } + ; ε = record { TMap = λ x → π' ; isNTrans = record { commute = ε-comm } } ; isCoMonad = record { unity1 = IsCCC.e3b isCCC - ; unity2 = {!!} -- IsCCC.e3b isCCC - ; assoc = {!!} + ; unity2 = unity2 + ; assoc = assoc2 } } where open ≈-Reasoning A + δ-comm : {a₁ : Obj A} {b : Obj A} {f : Hom A a₁ b} → + FMap (_○_ (SA a) (SA a)) f o < π , id1 A _ > ≈ < π , id1 A _ > o FMap (SA a) f + δ-comm {x} {b} {f} = begin + FMap (_○_ (SA a) (SA a)) f o < π , id1 A _ > ≈⟨ IsCCC.distr-π isCCC ⟩ + < π o < π , id1 A _ > , (FMap (SA a) f o π' ) o < π , id1 A _ > > ≈⟨ IsCCC.π-cong isCCC (IsCCC.e3a isCCC) (sym assoc) ⟩ + < π , FMap (SA a) f o ( π' o < π , id1 A _ >) > ≈⟨ IsCCC.π-cong isCCC refl-hom (cdr (IsCCC.e3b isCCC)) ⟩ + < π , FMap (SA a) f o id1 A _ > ≈⟨ IsCCC.π-cong isCCC refl-hom idR ⟩ + < π , FMap (SA a) f > ≈↑⟨ IsCCC.π-cong isCCC (IsCCC.e3a isCCC) idL ⟩ + < π o FMap (SA a) f , id1 A _ o FMap (SA a) f > ≈↑⟨ IsCCC.distr-π isCCC ⟩ + < π , id1 A _ > o FMap (SA a) f ∎ + ε-comm : {a₁ : Obj A} {b : Obj A} {f : Hom A a₁ b} → + FMap (identityFunctor {_} {_} {_} {A}) f o π' ≈ π' o FMap (SA a) f + ε-comm {_} {_} {f} = sym (IsCCC.e3b isCCC) + unity2 : {a₁ : Obj A} → FMap (SA a) π' o < π , id1 A _ > ≈ id1 A (a ∧ a₁) + unity2 {x} = begin + FMap (SA a) π' o < π , id1 A _ > ≈⟨ IsCCC.distr-π isCCC ⟩ + < π o < π , id1 A _ > , ( π' o π' ) o < π , id1 A _ > > ≈⟨ IsCCC.π-cong isCCC (IsCCC.e3a isCCC) (sym assoc) ⟩ + < π , π' o ( π' o < π , id1 A _ > ) > ≈⟨ IsCCC.π-cong isCCC refl-hom (cdr (IsCCC.e3b isCCC)) ⟩ + < π , π' o id1 A _ > ≈⟨ IsCCC.π-cong isCCC refl-hom idR ⟩ + < π , π' > ≈⟨ IsCCC.π-id isCCC ⟩ + id1 A (a ∧ x) ∎ + assoc2 : {a₁ : Obj A} → < π , id1 A _ > o < π , id1 A _ > ≈ FMap (SA a) < π , id1 A (a ∧ a₁) > o < π , id1 A _ > + assoc2 {x} = begin + < π , id1 A _ > o < π , id1 A _ > ≈⟨ IsCCC.distr-π isCCC ⟩ + < π o < π , id1 A _ > , id1 A _ o < π , id1 A _ > > ≈⟨ IsCCC.π-cong isCCC (IsCCC.e3a isCCC) idL ⟩ + < π , < π , id1 A _ > > ≈↑⟨ IsCCC.π-cong isCCC refl-hom idR ⟩ + < π , < π , id1 A _ > o id1 A _ > ≈↑⟨ IsCCC.π-cong isCCC refl-hom (cdr (IsCCC.e3b isCCC)) ⟩ + < π , < π , id1 A _ > o ( π' o < π , id1 A _ > ) > ≈↑⟨ IsCCC.π-cong isCCC (IsCCC.e3a isCCC) (sym assoc) ⟩ + < π o < π , id1 A _ > , (< π , id1 A _ > o π' ) o < π , id1 A _ > > ≈↑⟨ IsCCC.distr-π isCCC ⟩ + FMap (SA a) < π , id1 A (a ∧ x) > o < π , id1 A _ > ∎ - functional-completeness : (C : CCC A ) → {a : Obj A} → ( x : Hom A (CCC.１ C) a ) → {!!} - functional-completeness = {!!} + + + -- functional-completeness : (C : CCC A ) → {a : Obj A} → ( x : Hom A (CCC.１ C) a ) → {!!} + -- functional-completeness = {!!} -- end