Mercurial > hg > Members > kono > Proof > category
changeset 968:3a096cb82dc4
Polynominal category and functional completeness begin
coMonad and coKleisli category
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 25 Feb 2021 18:50:06 +0900 |
| parents | 472bcadfd216 |
| children | 6548572b7089 |
| files | src/Polynominal.agda src/bi-ccc.agda src/cat-utility.agda |
| diffstat | 3 files changed, 98 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Polynominal.agda Thu Feb 25 18:50:06 2021 +0900 @@ -0,0 +1,75 @@ +open import Category +open import CCC +open import Level +open import HomReasoning +open import cat-utility + +module Polynominal { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { S : Functor A A } (SM : coMonad A S) where + + open coMonad + + open Functor + open NTrans + + -- + -- Hom in Sleisli Category + -- + + record SHom (a : Obj A) (b : Obj A) + : Set c₂ where + field + SMap : Hom A ( FObj S a ) b + + open SHom + + S-id : (a : Obj A) → SHom a a + S-id a = record { SMap = TMap (ε SM) a } + + open import Relation.Binary + + _⋍_ : { a : Obj A } { b : Obj A } (f g : SHom a b ) → Set ℓ + _⋍_ {a} {b} f g = A [ SMap f ≈ SMap g ] + + _*_ : { a b c : Obj A } → ( SHom b c) → ( SHom a b) → SHom a c + _*_ {a} {b} {c} g f = record { SMap = coJoin SM {a} {b} {c} (SMap g) (SMap f) } + + isSCat : IsCategory ( Obj A ) SHom _⋍_ _*_ (λ {a} → S-id a) + isSCat = record { isEquivalence = isEquivalence + ; identityL = SidL + ; identityR = SidR + ; o-resp-≈ = So-resp + ; associative = Sassoc + } + where + open ≈-Reasoning A + isEquivalence : { a b : Obj A } → IsEquivalence {_} {_} {SHom a b} _⋍_ + isEquivalence {C} {D} = record { refl = refl-hom ; sym = sym ; trans = trans-hom } + SidL : {a b : Obj A} → {f : SHom a b} → (S-id _ * f) ⋍ f + SidL {a} {b} {f} = begin + SMap (S-id _ * f) ≈⟨⟩ + (TMap (ε SM) b o (FMap S (SMap f))) o TMap (δ SM) a ≈↑⟨ car (nat (ε SM)) ⟩ + (SMap f o TMap (ε SM) (FObj S a)) o TMap (δ SM) a ≈↑⟨ assoc ⟩ + SMap f o TMap (ε SM) (FObj S a) o TMap (δ SM) a ≈⟨ cdr (IsCoMonad.unity1 (isCoMonad SM)) ⟩ + SMap f o id1 A _ ≈⟨ idR ⟩ + SMap f ∎ + SidR : {C D : Obj A} → {f : SHom C D} → (f * S-id _ ) ⋍ f + SidR {a} {b} {f} = begin + SMap (f * S-id a) ≈⟨⟩ + (SMap f o FMap S (TMap (ε SM) a)) o TMap (δ SM) a ≈↑⟨ assoc ⟩ + SMap f o (FMap S (TMap (ε SM) a) o TMap (δ SM) a) ≈⟨ cdr (IsCoMonad.unity2 (isCoMonad SM)) ⟩ + SMap f o id1 A _ ≈⟨ idR ⟩ + SMap f ∎ + So-resp : {a b c : Obj A} → {f g : SHom a b } → {h i : SHom b c } → + f ⋍ g → h ⋍ i → (h * f) ⋍ (i * g) + So-resp {a} {b} {c} {f} {g} {h} {i} eq-fg eq-hi = resp refl-hom (resp (fcong S eq-fg ) eq-hi ) + Sassoc : {a b c d : Obj A} → {f : SHom c d } → {g : SHom b c } → {h : SHom a b } → + (f * (g * h)) ⋍ ((f * g) * h) + Sassoc {a} {b} {c} {d} {f} {g} {h} = begin + SMap (f * (g * h)) ≈⟨ car (cdr (distr S)) ⟩ + {!!} ≈⟨ {!!} ⟩ + SMap ((f * g) * h) ∎ + + SCat : Category c₁ c₂ ℓ + SCat = record { Obj = Obj A ; Hom = SHom ; _o_ = _*_ ; _≈_ = _⋍_ ; Id = λ {a} → S-id a ; isCategory = isSCat } + +-- end
--- a/src/bi-ccc.agda Thu Feb 25 13:08:17 2021 +0900 +++ b/src/bi-ccc.agda Thu Feb 25 18:50:06 2021 +0900 @@ -107,3 +107,5 @@ id1 A ⊥ ∎ +-- define boolean category ( bi-cartesian closed category wth ⊤ and ⊥ object ) +-- Any bi-cartesian closed category is isomorpphic to the boolean category
--- a/src/cat-utility.agda Thu Feb 25 13:08:17 2021 +0900 +++ b/src/cat-utility.agda Thu Feb 25 18:50:06 2021 +0900 @@ -117,6 +117,27 @@ ( Hom A b ( FObj T c )) → ( Hom A a ( FObj T b)) → Hom A a ( FObj T c ) join {_} {_} {c} g f = A [ TMap μ c o A [ FMap T g o f ] ] + record IsCoMonad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) + ( S : Functor A A ) + ( ε : NTrans A A S identityFunctor ) + ( δ : NTrans A A S (S ○ S) ) + : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where + field + assoc : {a : Obj A} → A [ A [ TMap δ (FObj S a) o TMap δ a ] ≈ A [ FMap S (TMap δ a) o TMap δ a ] ] + unity1 : {a : Obj A} → A [ A [ TMap ε ( FObj S a ) o TMap δ a ] ≈ Id {_} {_} {_} {A} (FObj S a) ] + unity2 : {a : Obj A} → A [ A [ (FMap S (TMap ε a )) o TMap δ a ] ≈ Id {_} {_} {_} {A} (FObj S a) ] + + record coMonad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (S : Functor A A) + : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where + field + ε : NTrans A A S identityFunctor + δ : NTrans A A S (S ○ S) + isCoMonad : IsCoMonad A S ε δ + -- g ○ f = g S(f) δ(a) + coJoin : { a b : Obj A } → { c : Obj A } → + ( Hom A (FObj S b ) c ) → ( Hom A ( FObj S a) b ) → Hom A ( FObj S a ) c + coJoin {a} {_} {_} g f = A [ A [ g o FMap S f ] o TMap δ a ] + Functor*Nat : {c₁ c₂ ℓ c₁' c₂' ℓ' c₁'' c₂'' ℓ'' : Level} (A : Category c₁ c₂ ℓ) {B : Category c₁' c₂' ℓ'} (C : Category c₁'' c₂'' ℓ'') (F : Functor B C) → { G H : Functor A B } → ( n : NTrans A B G H ) → NTrans A C (F ○ G) (F ○ H)