Mercurial > hg > Members > kono > Proof > category

annotate src/cokleisli.agda @ 1015:e01a1d29492b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Functional Completeness
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 21 Mar 2021 10:16:57 +0900
parents src/Polynominal.agda@4f1db956d3b4
children 45de2b31bf02
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 Level
1015
e01a1d29492b Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1014
diff changeset
3 open import HomReasoning
968
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 open import cat-utility
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6
1015
e01a1d29492b Functional Completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1014
diff changeset
7 module coKleisli { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { S : Functor A A } (SM : coMonad A S) where
969
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
8
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
9 open coMonad
968
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10
969
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
11 open Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
12 open NTrans
968
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13
969
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
14 --
971
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 970
diff changeset
15 -- Hom in Kleisli Category
969
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
16 --
968
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17
969
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
18 record SHom (a : Obj A) (b : Obj A)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
19 : Set c₂ where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
20 field
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
21 SMap : Hom A ( FObj S a ) b
968
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22
969
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
23 open SHom
968
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24
969
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
25 S-id : (a : Obj A) → SHom a a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
26 S-id a = record { SMap = TMap (ε SM) a }
968
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27
969
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
28 open import Relation.Binary
968
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29
969
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
30 _⋍_ : { a : Obj A } { b : Obj A } (f g : SHom a b ) → Set ℓ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
31 _⋍_ {a} {b} f g = A [ SMap f ≈ SMap g ]
968
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32
969
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
33 _*_ : { a b c : Obj A } → ( SHom b c) → ( SHom a b) → SHom a c
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
34 _*_ {a} {b} {c} g f = record { SMap = coJoin SM {a} {b} {c} (SMap g) (SMap f) }
968
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35
969
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
36 isSCat : IsCategory ( Obj A ) SHom _⋍_ _*_ (λ {a} → S-id a)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
37 isSCat = record { isEquivalence = isEquivalence
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
38 ; identityL = SidL
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
39 ; identityR = SidR
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
40 ; o-resp-≈ = So-resp
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
41 ; associative = Sassoc
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
42 }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
43 where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
44 open ≈-Reasoning A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
45 isEquivalence : { a b : Obj A } → IsEquivalence {_} {_} {SHom a b} _⋍_
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
46 isEquivalence {C} {D} = record { refl = refl-hom ; sym = sym ; trans = trans-hom }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
47 SidL : {a b : Obj A} → {f : SHom a b} → (S-id _ * f) ⋍ f
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
48 SidL {a} {b} {f} = begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
49 SMap (S-id _ * f) ≈⟨⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
50 (TMap (ε SM) b o (FMap S (SMap f))) o TMap (δ SM) a ≈↑⟨ car (nat (ε SM)) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
51 (SMap f o TMap (ε SM) (FObj S a)) o TMap (δ SM) a ≈↑⟨ assoc ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
52 SMap f o TMap (ε SM) (FObj S a) o TMap (δ SM) a ≈⟨ cdr (IsCoMonad.unity1 (isCoMonad SM)) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
53 SMap f o id1 A _ ≈⟨ idR ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
54 SMap f ∎
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
55 SidR : {C D : Obj A} → {f : SHom C D} → (f * S-id _ ) ⋍ f
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
56 SidR {a} {b} {f} = begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
57 SMap (f * S-id a) ≈⟨⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
58 (SMap f o FMap S (TMap (ε SM) a)) o TMap (δ SM) a ≈↑⟨ assoc ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
59 SMap f o (FMap S (TMap (ε SM) a) o TMap (δ SM) a) ≈⟨ cdr (IsCoMonad.unity2 (isCoMonad SM)) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
60 SMap f o id1 A _ ≈⟨ idR ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
61 SMap f ∎
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
62 So-resp : {a b c : Obj A} → {f g : SHom a b } → {h i : SHom b c } →
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
63 f ⋍ g → h ⋍ i → (h * f) ⋍ (i * g)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
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 )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
65 Sassoc : {a b c d : Obj A} → {f : SHom c d } → {g : SHom b c } → {h : SHom a b } →
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
66 (f * (g * h)) ⋍ ((f * g) * h)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
67 Sassoc {a} {b} {c} {d} {f} {g} {h} = begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
68 SMap (f * (g * h)) ≈⟨ car (cdr (distr S)) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
69 (SMap f o ( FMap S (SMap g o FMap S (SMap h)) o FMap S (TMap (δ SM) a) )) o TMap (δ SM) a ≈⟨ car assoc ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
70 ((SMap f o FMap S (SMap g o FMap S (SMap h))) o FMap S (TMap (δ SM) a) ) o TMap (δ SM) a ≈↑⟨ assoc ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
71 (SMap f o FMap S (SMap g o FMap S (SMap h))) o (FMap S (TMap (δ SM) a) o TMap (δ SM) a ) ≈↑⟨ cdr (IsCoMonad.assoc (isCoMonad SM)) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
72 (SMap f o (FMap S (SMap g o FMap S (SMap h)))) o ( TMap (δ SM) (FObj S a) o TMap (δ SM) a ) ≈⟨ assoc ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
73 ((SMap f o (FMap S (SMap g o FMap S (SMap h)))) o TMap (δ SM) (FObj S a) ) o TMap (δ SM) a ≈⟨ car (car (cdr (distr S))) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
74 ((SMap f o (FMap S (SMap g) o FMap S (FMap S (SMap h)))) o TMap (δ SM) (FObj S a) ) o TMap (δ SM) a ≈↑⟨ car assoc ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
75 (SMap f o ((FMap S (SMap g) o FMap S (FMap S (SMap h))) o TMap (δ SM) (FObj S a) )) o TMap (δ SM) a ≈↑⟨ assoc ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
76 SMap f o (((FMap S (SMap g) o FMap S (FMap S (SMap h))) o TMap (δ SM) (FObj S a) ) o TMap (δ SM) a) ≈↑⟨ cdr (car assoc ) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
77 SMap f o ((FMap S (SMap g) o (FMap S (FMap S (SMap h)) o TMap (δ SM) (FObj S a) )) o TMap (δ SM) a) ≈⟨ cdr (car (cdr (nat (δ SM)))) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
78 SMap f o ((FMap S (SMap g) o ( TMap (δ SM) b o FMap S (SMap h))) o TMap (δ SM) a) ≈⟨ assoc ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
79 (SMap f o (FMap S (SMap g) o ( TMap (δ SM) b o FMap S (SMap h)))) o TMap (δ SM) a ≈⟨ car (cdr assoc) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
80 (SMap f o ((FMap S (SMap g) o TMap (δ SM) b ) o FMap S (SMap h))) o TMap (δ SM) a ≈⟨ car assoc ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
81 ((SMap f o (FMap S (SMap g) o TMap (δ SM) b )) o FMap S (SMap h)) o TMap (δ SM) a ≈⟨ car (car assoc) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
82 (((SMap f o FMap S (SMap g)) o TMap (δ SM) b ) o FMap S (SMap h)) o TMap (δ SM) a ≈⟨⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
83 SMap ((f * g) * h) ∎
968
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
84
969
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
85 SCat : Category c₁ c₂ ℓ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
86 SCat = record { Obj = Obj A ; Hom = SHom ; _o_ = _*_ ; _≈_ = _⋍_ ; Id = λ {a} → S-id a ; isCategory = isSCat }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 968
diff changeset
87