Mercurial > hg > Members > kono > Proof > category

annotate 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
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
968
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 open import Category
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 open import CCC
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import Level
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 open import HomReasoning
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open import cat-utility
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 module Polynominal { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { S : Functor A A } (SM : coMonad A S) where
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 open coMonad
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 open Functor
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 open NTrans
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 --
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 -- Hom in Sleisli Category
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 --
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 record SHom (a : Obj A) (b : Obj A)
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 : Set c₂ where
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 field
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 SMap : Hom A ( FObj S a ) b
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 open SHom
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 S-id : (a : Obj A) → SHom a a
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 S-id a = record { SMap = TMap (ε SM) a }
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 open import Relation.Binary
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 _⋍_ : { a : Obj A } { b : Obj A } (f g : SHom a b ) → Set ℓ
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 _⋍_ {a} {b} f g = A [ SMap f ≈ SMap g ]
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 _*_ : { a b c : Obj A } → ( SHom b c) → ( SHom a b) → SHom a c
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 _*_ {a} {b} {c} g f = record { SMap = coJoin SM {a} {b} {c} (SMap g) (SMap f) }
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 isSCat : IsCategory ( Obj A ) SHom _⋍_ _*_ (λ {a} → S-id a)
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 isSCat = record { isEquivalence = isEquivalence
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 ; identityL = SidL
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 ; identityR = SidR
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 ; o-resp-≈ = So-resp
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 ; associative = Sassoc
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 }
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 where
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 open ≈-Reasoning A
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 isEquivalence : { a b : Obj A } → IsEquivalence {_} {_} {SHom a b} _⋍_
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 isEquivalence {C} {D} = record { refl = refl-hom ; sym = sym ; trans = trans-hom }
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47 SidL : {a b : Obj A} → {f : SHom a b} → (S-id _ * f) ⋍ f
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 SidL {a} {b} {f} = begin
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 SMap (S-id _ * f) ≈⟨⟩
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50 (TMap (ε SM) b o (FMap S (SMap f))) o TMap (δ SM) a ≈↑⟨ car (nat (ε SM)) ⟩
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51 (SMap f o TMap (ε SM) (FObj S a)) o TMap (δ SM) a ≈↑⟨ assoc ⟩
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52 SMap f o TMap (ε SM) (FObj S a) o TMap (δ SM) a ≈⟨ cdr (IsCoMonad.unity1 (isCoMonad SM)) ⟩
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53 SMap f o id1 A _ ≈⟨ idR ⟩
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 SMap f ∎
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
55 SidR : {C D : Obj A} → {f : SHom C D} → (f * S-id _ ) ⋍ f
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 SidR {a} {b} {f} = begin
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
57 SMap (f * S-id a) ≈⟨⟩
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58 (SMap f o FMap S (TMap (ε SM) a)) o TMap (δ SM) a ≈↑⟨ assoc ⟩
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59 SMap f o (FMap S (TMap (ε SM) a) o TMap (δ SM) a) ≈⟨ cdr (IsCoMonad.unity2 (isCoMonad SM)) ⟩
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60 SMap f o id1 A _ ≈⟨ idR ⟩
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
61 SMap f ∎
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62 So-resp : {a b c : Obj A} → {f g : SHom a b } → {h i : SHom b c } →
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63 f ⋍ g → h ⋍ i → (h * f) ⋍ (i * g)
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64 So-resp {a} {b} {c} {f} {g} {h} {i} eq-fg eq-hi = resp refl-hom (resp (fcong S eq-fg ) eq-hi )
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
65 Sassoc : {a b c d : Obj A} → {f : SHom c d } → {g : SHom b c } → {h : SHom a b } →
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
66 (f * (g * h)) ⋍ ((f * g) * h)
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
67 Sassoc {a} {b} {c} {d} {f} {g} {h} = begin
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
68 SMap (f * (g * h)) ≈⟨ car (cdr (distr S)) ⟩
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69 {!!} ≈⟨ {!!} ⟩
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
70 SMap ((f * g) * h) ∎
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
71
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
72 SCat : Category c₁ c₂ ℓ
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
73 SCat = record { Obj = Obj A ; Hom = SHom ; _o_ = _*_ ; _≈_ = _⋍_ ; Id = λ {a} → S-id a ; isCategory = isSCat }
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
74
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
75 -- end