Mercurial > hg > Members > kono > Proof > category
annotate src/Polynominal.agda @ 975:f8fba4f1dcfa
char-m=⊤
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 01 Mar 2021 17:01:00 +0900 |
| parents | 9746e93a8c31 |
| children | 5dcbf2b9194e |
| 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 |
| 969 | 7 module Polynominal { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( C : CCC A ) where |
|
968
3a096cb82dc4
Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
8 |
| 969 | 9 module coKleisli { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { S : Functor A A } (SM : coMonad A S) where |
| 10 | |
| 11 open coMonad | |
|
968
3a096cb82dc4
Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
12 |
| 969 | 13 open Functor |
| 14 open NTrans | |
|
968
3a096cb82dc4
Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
15 |
| 969 | 16 -- |
| 971 | 17 -- Hom in Kleisli Category |
| 969 | 18 -- |
|
968
3a096cb82dc4
Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
19 |
| 969 | 20 record SHom (a : Obj A) (b : Obj A) |
| 21 : Set c₂ where | |
| 22 field | |
| 23 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
|
24 |
| 969 | 25 open SHom |
|
968
3a096cb82dc4
Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
26 |
| 969 | 27 S-id : (a : Obj A) → SHom a a |
| 28 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
|
29 |
| 969 | 30 open import Relation.Binary |
|
968
3a096cb82dc4
Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
31 |
| 969 | 32 _⋍_ : { a : Obj A } { b : Obj A } (f g : SHom a b ) → Set ℓ |
| 33 _⋍_ {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
|
34 |
| 969 | 35 _*_ : { a b c : Obj A } → ( SHom b c) → ( SHom a b) → SHom a c |
| 36 _*_ {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
|
37 |
| 969 | 38 isSCat : IsCategory ( Obj A ) SHom _⋍_ _*_ (λ {a} → S-id a) |
| 39 isSCat = record { isEquivalence = isEquivalence | |
| 40 ; identityL = SidL | |
| 41 ; identityR = SidR | |
| 42 ; o-resp-≈ = So-resp | |
| 43 ; associative = Sassoc | |
| 44 } | |
| 45 where | |
| 46 open ≈-Reasoning A | |
| 47 isEquivalence : { a b : Obj A } → IsEquivalence {_} {_} {SHom a b} _⋍_ | |
| 48 isEquivalence {C} {D} = record { refl = refl-hom ; sym = sym ; trans = trans-hom } | |
| 49 SidL : {a b : Obj A} → {f : SHom a b} → (S-id _ * f) ⋍ f | |
| 50 SidL {a} {b} {f} = begin | |
| 51 SMap (S-id _ * f) ≈⟨⟩ | |
| 52 (TMap (ε SM) b o (FMap S (SMap f))) o TMap (δ SM) a ≈↑⟨ car (nat (ε SM)) ⟩ | |
| 53 (SMap f o TMap (ε SM) (FObj S a)) o TMap (δ SM) a ≈↑⟨ assoc ⟩ | |
| 54 SMap f o TMap (ε SM) (FObj S a) o TMap (δ SM) a ≈⟨ cdr (IsCoMonad.unity1 (isCoMonad SM)) ⟩ | |
| 55 SMap f o id1 A _ ≈⟨ idR ⟩ | |
| 56 SMap f ∎ | |
| 57 SidR : {C D : Obj A} → {f : SHom C D} → (f * S-id _ ) ⋍ f | |
| 58 SidR {a} {b} {f} = begin | |
| 59 SMap (f * S-id a) ≈⟨⟩ | |
| 60 (SMap f o FMap S (TMap (ε SM) a)) o TMap (δ SM) a ≈↑⟨ assoc ⟩ | |
| 61 SMap f o (FMap S (TMap (ε SM) a) o TMap (δ SM) a) ≈⟨ cdr (IsCoMonad.unity2 (isCoMonad SM)) ⟩ | |
| 62 SMap f o id1 A _ ≈⟨ idR ⟩ | |
| 63 SMap f ∎ | |
| 64 So-resp : {a b c : Obj A} → {f g : SHom a b } → {h i : SHom b c } → | |
| 65 f ⋍ g → h ⋍ i → (h * f) ⋍ (i * g) | |
| 66 So-resp {a} {b} {c} {f} {g} {h} {i} eq-fg eq-hi = resp refl-hom (resp (fcong S eq-fg ) eq-hi ) | |
| 67 Sassoc : {a b c d : Obj A} → {f : SHom c d } → {g : SHom b c } → {h : SHom a b } → | |
| 68 (f * (g * h)) ⋍ ((f * g) * h) | |
| 69 Sassoc {a} {b} {c} {d} {f} {g} {h} = begin | |
| 70 SMap (f * (g * h)) ≈⟨ car (cdr (distr S)) ⟩ | |
| 71 (SMap f o ( FMap S (SMap g o FMap S (SMap h)) o FMap S (TMap (δ SM) a) )) o TMap (δ SM) a ≈⟨ car assoc ⟩ | |
| 72 ((SMap f o FMap S (SMap g o FMap S (SMap h))) o FMap S (TMap (δ SM) a) ) o TMap (δ SM) a ≈↑⟨ assoc ⟩ | |
| 73 (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)) ⟩ | |
| 74 (SMap f o (FMap S (SMap g o FMap S (SMap h)))) o ( TMap (δ SM) (FObj S a) o TMap (δ SM) a ) ≈⟨ assoc ⟩ | |
| 75 ((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))) ⟩ | |
| 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 ≈↑⟨ car assoc ⟩ | |
| 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 ≈↑⟨ assoc ⟩ | |
| 78 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 ) ⟩ | |
| 79 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)))) ⟩ | |
| 80 SMap f o ((FMap S (SMap g) o ( TMap (δ SM) b o FMap S (SMap h))) o TMap (δ SM) a) ≈⟨ assoc ⟩ | |
| 81 (SMap f o (FMap S (SMap g) o ( TMap (δ SM) b o FMap S (SMap h)))) o TMap (δ SM) a ≈⟨ car (cdr assoc) ⟩ | |
| 82 (SMap f o ((FMap S (SMap g) o TMap (δ SM) b ) o FMap S (SMap h))) o TMap (δ SM) a ≈⟨ car assoc ⟩ | |
| 83 ((SMap f o (FMap S (SMap g) o TMap (δ SM) b )) o FMap S (SMap h)) o TMap (δ SM) a ≈⟨ car (car assoc) ⟩ | |
| 84 (((SMap f o FMap S (SMap g)) o TMap (δ SM) b ) o FMap S (SMap h)) o TMap (δ SM) a ≈⟨⟩ | |
| 85 SMap ((f * g) * h) ∎ | |
|
968
3a096cb82dc4
Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
86 |
| 969 | 87 SCat : Category c₁ c₂ ℓ |
| 88 SCat = record { Obj = Obj A ; Hom = SHom ; _o_ = _*_ ; _≈_ = _⋍_ ; Id = λ {a} → S-id a ; isCategory = isSCat } | |
| 89 | |
| 90 open CCC.CCC C | |
| 970 | 91 open coMonad |
| 92 open Functor | |
| 93 open NTrans | |
| 94 open import Category.Cat | |
| 969 | 95 |
| 96 SA : (a : Obj A) → Functor A A | |
| 97 SA a = record { | |
| 98 FObj = λ x → a ∧ x | |
| 99 ; FMap = λ f → < π , A [ f o π' ] > | |
| 100 ; isFunctor = record { | |
| 101 identity = sa-id | |
| 102 ; ≈-cong = λ eq → IsCCC.π-cong isCCC refl-hom (resp refl-hom eq ) | |
| 103 ; distr = sa-distr | |
| 104 } | |
| 105 } where | |
| 106 open ≈-Reasoning A | |
| 107 sa-id : {b : Obj A} → < π , ( id1 A b o π' ) > ≈ id1 A (a ∧ b ) | |
| 108 sa-id {b} = begin | |
| 109 < π , ( id1 A b o π' ) > ≈⟨ IsCCC.π-cong isCCC (sym idR) (trans-hom idL (sym idR) ) ⟩ | |
| 110 < ( π o id1 A _ ) , ( π' o id1 A _ ) > ≈⟨ IsCCC.e3c isCCC ⟩ | |
| 111 id1 A (a ∧ b ) ∎ | |
| 112 sa-distr : {x b c : Obj A} {f : Hom A x b} {g : Hom A b c} → | |
| 113 < π , (( g o f ) o π') > ≈ < π , ( g o π' ) > o < π , (f o π') > | |
| 114 sa-distr {x} {b} {c} {f} {g} = begin | |
| 115 < π , (( g o f ) o π') > ≈↑⟨ IsCCC.π-cong isCCC (IsCCC.e3a isCCC) ( begin | |
| 116 ( g o π' ) o < π , (f o π') > ≈↑⟨ assoc ⟩ | |
| 117 g o ( π' o < π , (f o π') > ) ≈⟨ cdr (IsCCC.e3b isCCC) ⟩ | |
| 118 g o ( f o π') ≈⟨ assoc ⟩ | |
| 119 ( g o f ) o π' ∎ ) ⟩ | |
| 120 < (π o < π , (f o π') >) , ( ( g o π' ) o < π , (f o π') >) > ≈↑⟨ IsCCC.distr-π isCCC ⟩ | |
| 121 < π , ( g o π' ) > o < π , (f o π') > ∎ | |
| 122 | |
| 123 SM : (a : Obj A) → coMonad A (SA a) | |
| 124 SM a = record { | |
| 970 | 125 δ = record { TMap = λ x → < π , id1 A _ > ; isNTrans = record { commute = δ-comm} } |
| 126 ; ε = record { TMap = λ x → π' ; isNTrans = record { commute = ε-comm } } | |
| 969 | 127 ; isCoMonad = record { |
| 128 unity1 = IsCCC.e3b isCCC | |
| 970 | 129 ; unity2 = unity2 |
| 130 ; assoc = assoc2 | |
| 969 | 131 } |
| 132 } where | |
| 133 open ≈-Reasoning A | |
| 970 | 134 δ-comm : {a₁ : Obj A} {b : Obj A} {f : Hom A a₁ b} → |
| 135 FMap (_○_ (SA a) (SA a)) f o < π , id1 A _ > ≈ < π , id1 A _ > o FMap (SA a) f | |
| 136 δ-comm {x} {b} {f} = begin | |
| 137 FMap (_○_ (SA a) (SA a)) f o < π , id1 A _ > ≈⟨ IsCCC.distr-π isCCC ⟩ | |
| 138 < π o < π , id1 A _ > , (FMap (SA a) f o π' ) o < π , id1 A _ > > ≈⟨ IsCCC.π-cong isCCC (IsCCC.e3a isCCC) (sym assoc) ⟩ | |
| 139 < π , FMap (SA a) f o ( π' o < π , id1 A _ >) > ≈⟨ IsCCC.π-cong isCCC refl-hom (cdr (IsCCC.e3b isCCC)) ⟩ | |
| 140 < π , FMap (SA a) f o id1 A _ > ≈⟨ IsCCC.π-cong isCCC refl-hom idR ⟩ | |
| 141 < π , FMap (SA a) f > ≈↑⟨ IsCCC.π-cong isCCC (IsCCC.e3a isCCC) idL ⟩ | |
| 142 < π o FMap (SA a) f , id1 A _ o FMap (SA a) f > ≈↑⟨ IsCCC.distr-π isCCC ⟩ | |
| 143 < π , id1 A _ > o FMap (SA a) f ∎ | |
| 144 ε-comm : {a₁ : Obj A} {b : Obj A} {f : Hom A a₁ b} → | |
| 145 FMap (identityFunctor {_} {_} {_} {A}) f o π' ≈ π' o FMap (SA a) f | |
| 146 ε-comm {_} {_} {f} = sym (IsCCC.e3b isCCC) | |
| 147 unity2 : {a₁ : Obj A} → FMap (SA a) π' o < π , id1 A _ > ≈ id1 A (a ∧ a₁) | |
| 148 unity2 {x} = begin | |
| 149 FMap (SA a) π' o < π , id1 A _ > ≈⟨ IsCCC.distr-π isCCC ⟩ | |
| 150 < π o < π , id1 A _ > , ( π' o π' ) o < π , id1 A _ > > ≈⟨ IsCCC.π-cong isCCC (IsCCC.e3a isCCC) (sym assoc) ⟩ | |
| 151 < π , π' o ( π' o < π , id1 A _ > ) > ≈⟨ IsCCC.π-cong isCCC refl-hom (cdr (IsCCC.e3b isCCC)) ⟩ | |
| 152 < π , π' o id1 A _ > ≈⟨ IsCCC.π-cong isCCC refl-hom idR ⟩ | |
| 153 < π , π' > ≈⟨ IsCCC.π-id isCCC ⟩ | |
| 154 id1 A (a ∧ x) ∎ | |
| 155 assoc2 : {a₁ : Obj A} → < π , id1 A _ > o < π , id1 A _ > ≈ FMap (SA a) < π , id1 A (a ∧ a₁) > o < π , id1 A _ > | |
| 156 assoc2 {x} = begin | |
| 157 < π , id1 A _ > o < π , id1 A _ > ≈⟨ IsCCC.distr-π isCCC ⟩ | |
| 158 < π o < π , id1 A _ > , id1 A _ o < π , id1 A _ > > ≈⟨ IsCCC.π-cong isCCC (IsCCC.e3a isCCC) idL ⟩ | |
| 159 < π , < π , id1 A _ > > ≈↑⟨ IsCCC.π-cong isCCC refl-hom idR ⟩ | |
| 160 < π , < π , id1 A _ > o id1 A _ > ≈↑⟨ IsCCC.π-cong isCCC refl-hom (cdr (IsCCC.e3b isCCC)) ⟩ | |
| 161 < π , < π , id1 A _ > o ( π' o < π , id1 A _ > ) > ≈↑⟨ IsCCC.π-cong isCCC (IsCCC.e3a isCCC) (sym assoc) ⟩ | |
| 162 < π o < π , id1 A _ > , (< π , id1 A _ > o π' ) o < π , id1 A _ > > ≈↑⟨ IsCCC.distr-π isCCC ⟩ | |
| 163 FMap (SA a) < π , id1 A (a ∧ x) > o < π , id1 A _ > ∎ | |
| 969 | 164 |
| 970 | 165 |
| 166 | |
| 167 -- functional-completeness : (C : CCC A ) → {a : Obj A} → ( x : Hom A (CCC.１ C) a ) → {!!} | |
| 168 -- functional-completeness = {!!} | |
|
968
3a096cb82dc4
Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
169 |
|
3a096cb82dc4
Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
170 -- end |