Mercurial > hg > Members > kono > Proof > category

comparison src/Polynominal.agda @ 968:3a096cb82dc4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
children 6548572b7089
comparison
equal deleted inserted replaced
967:472bcadfd216 968:3a096cb82dc4
1 open import Category
2 open import CCC
3 open import Level
4 open import HomReasoning
5 open import cat-utility
6
7 module Polynominal { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { S : Functor A A } (SM : coMonad A S) where
8
9 open coMonad
10
11 open Functor
12 open NTrans
13
14 --
15 -- Hom in Sleisli Category
16 --
17
18 record SHom (a : Obj A) (b : Obj A)
19 : Set c₂ where
20 field
21 SMap : Hom A ( FObj S a ) b
22
23 open SHom
24
25 S-id : (a : Obj A) → SHom a a
26 S-id a = record { SMap = TMap (ε SM) a }
27
28 open import Relation.Binary
29
30 _⋍_ : { a : Obj A } { b : Obj A } (f g : SHom a b ) → Set ℓ
31 _⋍_ {a} {b} f g = A [ SMap f ≈ SMap g ]
32
33 _*_ : { a b c : Obj A } → ( SHom b c) → ( SHom a b) → SHom a c
34 _*_ {a} {b} {c} g f = record { SMap = coJoin SM {a} {b} {c} (SMap g) (SMap f) }
35
36 isSCat : IsCategory ( Obj A ) SHom _⋍_ _*_ (λ {a} → S-id a)
37 isSCat = record { isEquivalence = isEquivalence
38 ; identityL = SidL
39 ; identityR = SidR
40 ; o-resp-≈ = So-resp
41 ; associative = Sassoc
42 }
43 where
44 open ≈-Reasoning A
45 isEquivalence : { a b : Obj A } → IsEquivalence {_} {_} {SHom a b} _⋍_
46 isEquivalence {C} {D} = record { refl = refl-hom ; sym = sym ; trans = trans-hom }
47 SidL : {a b : Obj A} → {f : SHom a b} → (S-id _ * f) ⋍ f
48 SidL {a} {b} {f} = begin
49 SMap (S-id _ * f) ≈⟨⟩
50 (TMap (ε SM) b o (FMap S (SMap f))) o TMap (δ SM) a ≈↑⟨ car (nat (ε SM)) ⟩
51 (SMap f o TMap (ε SM) (FObj S a)) o TMap (δ SM) a ≈↑⟨ assoc ⟩
52 SMap f o TMap (ε SM) (FObj S a) o TMap (δ SM) a ≈⟨ cdr (IsCoMonad.unity1 (isCoMonad SM)) ⟩
53 SMap f o id1 A _ ≈⟨ idR ⟩
54 SMap f ∎
55 SidR : {C D : Obj A} → {f : SHom C D} → (f * S-id _ ) ⋍ f
56 SidR {a} {b} {f} = begin
57 SMap (f * S-id a) ≈⟨⟩
58 (SMap f o FMap S (TMap (ε SM) a)) o TMap (δ SM) a ≈↑⟨ assoc ⟩
59 SMap f o (FMap S (TMap (ε SM) a) o TMap (δ SM) a) ≈⟨ cdr (IsCoMonad.unity2 (isCoMonad SM)) ⟩
60 SMap f o id1 A _ ≈⟨ idR ⟩
61 SMap f ∎
62 So-resp : {a b c : Obj A} → {f g : SHom a b } → {h i : SHom b c } →
63 f ⋍ g → h ⋍ i → (h * f) ⋍ (i * g)
64 So-resp {a} {b} {c} {f} {g} {h} {i} eq-fg eq-hi = resp refl-hom (resp (fcong S eq-fg ) eq-hi )
65 Sassoc : {a b c d : Obj A} → {f : SHom c d } → {g : SHom b c } → {h : SHom a b } →
66 (f * (g * h)) ⋍ ((f * g) * h)
67 Sassoc {a} {b} {c} {d} {f} {g} {h} = begin
68 SMap (f * (g * h)) ≈⟨ car (cdr (distr S)) ⟩
69 {!!} ≈⟨ {!!} ⟩
70 SMap ((f * g) * h) ∎
71
72 SCat : Category c₁ c₂ ℓ
73 SCat = record { Obj = Obj A ; Hom = SHom ; _o_ = _*_ ; _≈_ = _⋍_ ; Id = λ {a} → S-id a ; isCategory = isSCat }
74
75 -- end