Mercurial > hg > Members > kono > Proof > category
annotate cat-utility.agda @ 84:ee25f96ee8cc
record Resolution
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 27 Jul 2013 17:32:32 +0900 |
| parents | e945c201364a |
| children | be4e3b073e0d |
| rev | line source |
|---|---|
| 56 | 1 module cat-utility where |
| 2 | |
| 3 -- Shinji KONO <kono@ie.u-ryukyu.ac.jp> | |
| 4 | |
| 5 open import Category -- https://github.com/konn/category-agda | |
| 6 open import Level | |
| 7 --open import Category.HomReasoning | |
| 8 open import HomReasoning | |
| 9 | |
| 10 open Functor | |
| 11 | |
| 12 id1 : ∀{c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (a : Obj A ) → Hom A a a | |
| 13 id1 A a = (Id {_} {_} {_} {A} a) | |
| 14 | |
| 15 record IsUniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') | |
| 16 ( U : Functor B A ) | |
| 17 ( F : Obj A → Obj B ) | |
| 18 ( η : (a : Obj A) → Hom A a ( FObj U (F a) ) ) | |
| 19 ( _* : { a : Obj A}{ b : Obj B} → ( Hom A a (FObj U b) ) → Hom B (F a ) b ) | |
| 20 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where | |
| 21 field | |
| 22 universalMapping : {a' : Obj A} { b' : Obj B } → { f : Hom A a' (FObj U b') } → | |
| 23 A [ A [ FMap U ( f * ) o η a' ] ≈ f ] | |
| 24 uniquness : {a' : Obj A} { b' : Obj B } → { f : Hom A a' (FObj U b') } → { g : Hom B (F a') b' } → | |
| 25 A [ A [ FMap U g o η a' ] ≈ f ] → B [ f * ≈ g ] | |
| 26 | |
| 27 record UniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') | |
| 28 ( U : Functor B A ) | |
| 29 ( F : Obj A → Obj B ) | |
| 30 ( η : (a : Obj A) → Hom A a ( FObj U (F a) ) ) | |
| 31 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where | |
| 32 infixr 11 _* | |
| 33 field | |
| 34 _* : { a : Obj A}{ b : Obj B} → ( Hom A a (FObj U b) ) → Hom B (F a ) b | |
| 35 isUniversalMapping : IsUniversalMapping A B U F η _* | |
| 36 | |
| 37 open NTrans | |
| 38 open import Category.Cat | |
| 39 record IsAdjunction {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') | |
| 40 ( U : Functor B A ) | |
| 41 ( F : Functor A B ) | |
| 42 ( η : NTrans A A identityFunctor ( U ○ F ) ) | |
| 43 ( ε : NTrans B B ( F ○ U ) identityFunctor ) | |
| 44 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where | |
| 45 field | |
| 80 | 46 adjoint1 : { b : Obj B } → |
| 47 A [ A [ ( FMap U ( TMap ε b )) o ( TMap η ( FObj U b )) ] ≈ id1 A (FObj U b) ] | |
| 48 adjoint2 : {a : Obj A} → | |
| 49 B [ B [ ( TMap ε ( FObj F a )) o ( FMap F ( TMap η a )) ] ≈ id1 B (FObj F a) ] | |
| 56 | 50 |
| 51 record Adjunction {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') | |
| 52 ( U : Functor B A ) | |
| 53 ( F : Functor A B ) | |
| 54 ( η : NTrans A A identityFunctor ( U ○ F ) ) | |
| 55 ( ε : NTrans B B ( F ○ U ) identityFunctor ) | |
| 56 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where | |
| 57 field | |
| 58 isAdjunction : IsAdjunction A B U F η ε | |
| 59 | |
| 60 | |
| 61 record IsMonad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) | |
| 62 ( T : Functor A A ) | |
| 63 ( η : NTrans A A identityFunctor T ) | |
| 64 ( μ : NTrans A A (T ○ T) T) | |
| 65 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where | |
| 66 field | |
| 67 assoc : {a : Obj A} → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈ A [ TMap μ a o FMap T (TMap μ a) ] ] | |
| 68 unity1 : {a : Obj A} → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] | |
| 69 unity2 : {a : Obj A} → A [ A [ TMap μ a o (FMap T (TMap η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ] | |
| 70 | |
| 71 record Monad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (T : Functor A A) (η : NTrans A A identityFunctor T) (μ : NTrans A A (T ○ T) T) | |
| 72 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where | |
| 73 eta : NTrans A A identityFunctor T | |
| 74 eta = η | |
| 75 mu : NTrans A A (T ○ T) T | |
| 76 mu = μ | |
| 77 field | |
| 78 isMonad : IsMonad A T η μ | |
| 79 | |
| 80 Functor*Nat : {c₁ c₂ ℓ c₁' c₂' ℓ' c₁'' c₂'' ℓ'' : Level} (A : Category c₁ c₂ ℓ) {B : Category c₁' c₂' ℓ'} (C : Category c₁'' c₂'' ℓ'') | |
| 81 (F : Functor B C) -> { G H : Functor A B } -> ( n : NTrans A B G H ) -> NTrans A C (F ○ G) (F ○ H) | |
| 82 Functor*Nat A {B} C F {G} {H} n = record { | |
| 83 TMap = \a -> FMap F (TMap n a) | |
| 84 ; isNTrans = record { | |
| 85 naturality = naturality | |
| 86 } | |
| 87 } where | |
| 88 naturality : {a b : Obj A} {f : Hom A a b} | |
| 89 → C [ C [ (FMap F ( FMap H f )) o ( FMap F (TMap n a)) ] ≈ C [ (FMap F (TMap n b )) o (FMap F (FMap G f)) ] ] | |
| 90 naturality {a} {b} {f} = let open ≈-Reasoning (C) in | |
| 91 begin | |
| 92 (FMap F ( FMap H f )) o ( FMap F (TMap n a)) | |
| 66 | 93 ≈⟨ sym (distr F) ⟩ |
| 56 | 94 FMap F ( B [ (FMap H f) o TMap n a ]) |
|
69
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
68
diff
changeset
|
95 ≈⟨ IsFunctor.≈-cong (isFunctor F) ( nat n ) ⟩ |
| 56 | 96 FMap F ( B [ (TMap n b ) o FMap G f ] ) |
| 66 | 97 ≈⟨ distr F ⟩ |
| 56 | 98 (FMap F (TMap n b )) o (FMap F (FMap G f)) |
| 99 ∎ | |
| 100 | |
| 57 | 101 Nat*Functor : {c₁ c₂ ℓ c₁' c₂' ℓ' c₁'' c₂'' ℓ'' : Level} (A : Category c₁ c₂ ℓ) {B : Category c₁' c₂' ℓ'} (C : Category c₁'' c₂'' ℓ'') |
| 102 { G H : Functor B C } -> ( n : NTrans B C G H ) -> (F : Functor A B) -> NTrans A C (G ○ F) (H ○ F) | |
| 103 Nat*Functor A {B} C {G} {H} n F = record { | |
| 56 | 104 TMap = \a -> TMap n (FObj F a) |
| 105 ; isNTrans = record { | |
| 106 naturality = naturality | |
| 107 } | |
| 108 } where | |
| 109 naturality : {a b : Obj A} {f : Hom A a b} | |
| 110 → C [ C [ ( FMap H (FMap F f )) o ( TMap n (FObj F a)) ] ≈ C [ (TMap n (FObj F b )) o (FMap G (FMap F f)) ] ] | |
| 57 | 111 naturality {a} {b} {f} = IsNTrans.naturality ( isNTrans n) |
| 56 | 112 |
| 113 record Kleisli { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) | |
| 114 ( T : Functor A A ) | |
| 115 ( η : NTrans A A identityFunctor T ) | |
| 116 ( μ : NTrans A A (T ○ T) T ) | |
| 117 ( M : Monad A T η μ ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where | |
| 118 monad : Monad A T η μ | |
| 119 monad = M | |
| 120 -- g ○ f = μ(c) T(g) f | |
|
68
829e0698f87f
join implicit parameter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
66
diff
changeset
|
121 join : { a b : Obj A } → { c : Obj A } → |
| 56 | 122 ( Hom A b ( FObj T c )) → ( Hom A a ( FObj T b)) → Hom A a ( FObj T c ) |
|
68
829e0698f87f
join implicit parameter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
66
diff
changeset
|
123 join {_} {_} {c} g f = A [ TMap μ c o A [ FMap T g o f ] ] |
| 56 | 124 |
| 84 | 125 -- T ≃ (U_R ○ F_R) |
| 126 -- μ = U_R ε F_R | |
| 127 -- nat-ε | |
| 128 -- nat-η -- same as η but has different types | |
| 129 | |
| 130 record Resolution {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) ( B : Category c₁ c₂ ℓ ) | |
| 131 { U_R : Functor B A } { F_R : Functor A B } | |
| 132 { η : NTrans A A identityFunctor ( U_R ○ F_R ) } | |
| 133 { μ : NTrans A A ( ( U_R ○ F_R ) ○ ( U_R ○ F_R ) ) ( U_R ○ F_R ) } | |
| 134 ( M : Monad A ( U_R ○ F_R ) η μ ) | |
| 135 { ε_R : NTrans B B ( F_R ○ U_R ) identityFunctor } | |
| 136 ( Adj : Adjunction A B U_R F_R η ε_R ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where | |
| 137 field | |
| 138 μ=UεF : {x : Obj A } -> A [ TMap μ x ≈ FMap U_R ( TMap ε_R ( FObj F_R x ) ) ] |