Mercurial > hg > Members > kono > Proof > category
annotate cat-utility.agda @ 260:a87d3ea9efe4
pullback
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 20 Sep 2013 15:39:50 +0900 |
| parents | 24e83b8b81be |
| children | 78ce12f8e6b6 |
| rev | line source |
|---|---|
| 56 | 1 module cat-utility where |
| 2 | |
| 3 -- Shinji KONO <kono@ie.u-ryukyu.ac.jp> | |
| 4 | |
| 87 | 5 open import Category -- https://github.com/konn/category-agda |
| 6 open import Level | |
| 7 --open import Category.HomReasoning | |
| 8 open import HomReasoning | |
| 56 | 9 |
| 87 | 10 open Functor |
| 56 | 11 |
| 87 | 12 id1 : ∀{c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (a : Obj A ) → Hom A a a |
| 13 id1 A a = (Id {_} {_} {_} {A} a) | |
| 253 | 14 -- We cannot make A implicit |
| 56 | 15 |
| 87 | 16 record IsUniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') |
| 17 ( U : Functor B A ) | |
| 18 ( F : Obj A → Obj B ) | |
| 19 ( η : (a : Obj A) → Hom A a ( FObj U (F a) ) ) | |
| 20 ( _* : { a : Obj A}{ b : Obj B} → ( Hom A a (FObj U b) ) → Hom B (F a ) b ) | |
| 21 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where | |
| 22 field | |
| 101 | 23 universalMapping : {a : Obj A} { b : Obj B } → { f : Hom A a (FObj U b) } → |
| 24 A [ A [ FMap U ( f * ) o η a ] ≈ f ] | |
| 25 uniquness : {a : Obj A} { b : Obj B } → { f : Hom A a (FObj U b) } → { g : Hom B (F a) b } → | |
| 26 A [ A [ FMap U g o η a ] ≈ f ] → B [ f * ≈ g ] | |
| 56 | 27 |
| 87 | 28 record UniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') |
| 29 ( U : Functor B A ) | |
| 30 ( F : Obj A → Obj B ) | |
| 31 ( η : (a : Obj A) → Hom A a ( FObj U (F a) ) ) | |
| 32 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where | |
| 33 infixr 11 _* | |
| 34 field | |
| 35 _* : { a : Obj A}{ b : Obj B} → ( Hom A a (FObj U b) ) → Hom B (F a ) b | |
| 36 isUniversalMapping : IsUniversalMapping A B U F η _* | |
| 56 | 37 |
| 87 | 38 open NTrans |
| 39 open import Category.Cat | |
| 40 record IsAdjunction {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') | |
| 41 ( U : Functor B A ) | |
| 42 ( F : Functor A B ) | |
| 43 ( η : NTrans A A identityFunctor ( U ○ F ) ) | |
| 44 ( ε : NTrans B B ( F ○ U ) identityFunctor ) | |
| 45 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where | |
| 46 field | |
| 47 adjoint1 : { b : Obj B } → | |
| 48 A [ A [ ( FMap U ( TMap ε b )) o ( TMap η ( FObj U b )) ] ≈ id1 A (FObj U b) ] | |
| 49 adjoint2 : {a : Obj A} → | |
| 50 B [ B [ ( TMap ε ( FObj F a )) o ( FMap F ( TMap η a )) ] ≈ id1 B (FObj F a) ] | |
| 56 | 51 |
| 87 | 52 record Adjunction {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') |
| 53 ( U : Functor B A ) | |
| 54 ( F : Functor A B ) | |
| 55 ( η : NTrans A A identityFunctor ( U ○ F ) ) | |
| 56 ( ε : NTrans B B ( F ○ U ) identityFunctor ) | |
| 57 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where | |
| 58 field | |
| 59 isAdjunction : IsAdjunction A B U F η ε | |
|
202
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
176
diff
changeset
|
60 U-functor = U |
|
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
176
diff
changeset
|
61 F-functor = F |
|
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
176
diff
changeset
|
62 Eta = η |
|
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
176
diff
changeset
|
63 Epsiron = ε |
| 56 | 64 |
| 65 | |
| 87 | 66 record IsMonad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) |
| 67 ( T : Functor A A ) | |
| 68 ( η : NTrans A A identityFunctor T ) | |
| 69 ( μ : NTrans A A (T ○ T) T) | |
| 70 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where | |
| 71 field | |
| 72 assoc : {a : Obj A} → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈ A [ TMap μ a o FMap T (TMap μ a) ] ] | |
| 73 unity1 : {a : Obj A} → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] | |
| 74 unity2 : {a : Obj A} → A [ A [ TMap μ a o (FMap T (TMap η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ] | |
| 56 | 75 |
| 87 | 76 record Monad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (T : Functor A A) (η : NTrans A A identityFunctor T) (μ : NTrans A A (T ○ T) T) |
| 77 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where | |
| 78 field | |
| 79 isMonad : IsMonad A T η μ | |
| 130 | 80 -- g ○ f = μ(c) T(g) f |
| 81 join : { a b : Obj A } → { c : Obj A } → | |
| 82 ( Hom A b ( FObj T c )) → ( Hom A a ( FObj T b)) → Hom A a ( FObj T c ) | |
| 83 join {_} {_} {c} g f = A [ TMap μ c o A [ FMap T g o f ] ] | |
| 84 | |
| 56 | 85 |
| 87 | 86 Functor*Nat : {c₁ c₂ ℓ c₁' c₂' ℓ' c₁'' c₂'' ℓ'' : Level} (A : Category c₁ c₂ ℓ) {B : Category c₁' c₂' ℓ'} (C : Category c₁'' c₂'' ℓ'') |
| 87 (F : Functor B C) -> { G H : Functor A B } -> ( n : NTrans A B G H ) -> NTrans A C (F ○ G) (F ○ H) | |
| 88 Functor*Nat A {B} C F {G} {H} n = record { | |
| 89 TMap = \a -> FMap F (TMap n a) | |
| 90 ; isNTrans = record { | |
| 130 | 91 commute = commute |
| 87 | 92 } |
| 93 } where | |
| 130 | 94 commute : {a b : Obj A} {f : Hom A a b} |
| 87 | 95 → 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)) ] ] |
| 130 | 96 commute {a} {b} {f} = let open ≈-Reasoning (C) in |
| 87 | 97 begin |
| 98 (FMap F ( FMap H f )) o ( FMap F (TMap n a)) | |
| 99 ≈⟨ sym (distr F) ⟩ | |
| 100 FMap F ( B [ (FMap H f) o TMap n a ]) | |
| 101 ≈⟨ IsFunctor.≈-cong (isFunctor F) ( nat n ) ⟩ | |
| 102 FMap F ( B [ (TMap n b ) o FMap G f ] ) | |
| 103 ≈⟨ distr F ⟩ | |
| 104 (FMap F (TMap n b )) o (FMap F (FMap G f)) | |
| 105 ∎ | |
| 56 | 106 |
| 87 | 107 Nat*Functor : {c₁ c₂ ℓ c₁' c₂' ℓ' c₁'' c₂'' ℓ'' : Level} (A : Category c₁ c₂ ℓ) {B : Category c₁' c₂' ℓ'} (C : Category c₁'' c₂'' ℓ'') |
| 108 { G H : Functor B C } -> ( n : NTrans B C G H ) -> (F : Functor A B) -> NTrans A C (G ○ F) (H ○ F) | |
| 109 Nat*Functor A {B} C {G} {H} n F = record { | |
| 110 TMap = \a -> TMap n (FObj F a) | |
| 111 ; isNTrans = record { | |
| 130 | 112 commute = commute |
| 87 | 113 } |
| 114 } where | |
| 130 | 115 commute : {a b : Obj A} {f : Hom A a b} |
| 87 | 116 → 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)) ] ] |
| 130 | 117 commute {a} {b} {f} = IsNTrans.commute ( isNTrans n) |
| 56 | 118 |
| 87 | 119 -- T ≃ (U_R ○ F_R) |
| 120 -- μ = U_R ε F_R | |
| 121 -- nat-ε | |
| 122 -- nat-η -- same as η but has different types | |
| 84 | 123 |
| 87 | 124 record MResolution {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) ( B : Category c₁' c₂' ℓ' ) |
| 125 ( T : Functor A A ) | |
|
94
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
91
diff
changeset
|
126 -- { η : NTrans A A identityFunctor T } |
|
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
91
diff
changeset
|
127 -- { μ : NTrans A A (T ○ T) T } |
|
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
91
diff
changeset
|
128 -- { M : Monad A T η μ } |
| 87 | 129 ( UR : Functor B A ) ( FR : Functor A B ) |
| 130 { ηR : NTrans A A identityFunctor ( UR ○ FR ) } | |
| 131 { εR : NTrans B B ( FR ○ UR ) identityFunctor } | |
| 132 { μR : NTrans A A ( (UR ○ FR) ○ ( UR ○ FR )) ( UR ○ FR ) } | |
| 133 ( Adj : Adjunction A B UR FR ηR εR ) | |
| 134 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where | |
| 135 field | |
| 136 T=UF : T ≃ (UR ○ FR) | |
| 137 μ=UεF : {x : Obj A } -> A [ TMap μR x ≈ FMap UR ( TMap εR ( FObj FR x ) ) ] | |
|
94
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
91
diff
changeset
|
138 -- ηR=η : {x : Obj A } -> A [ TMap ηR x ≈ TMap η x ] -- We need T -> UR FR conversion |
| 87 | 139 -- μR=μ : {x : Obj A } -> A [ TMap μR x ≈ TMap μ x ] |
| 86 | 140 |
| 88 | 141 |
| 260 | 142 record Equalizer { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {c a b : Obj A} (e : Hom A c a) (f g : Hom A a b) : Set (ℓ ⊔ (c₁ ⊔ c₂)) where |
| 143 field | |
| 144 fe=ge : A [ A [ f o e ] ≈ A [ g o e ] ] | |
| 145 k : {d : Obj A} (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c | |
| 146 ek=h : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → A [ A [ e o k {d} h eq ] ≈ h ] | |
| 147 uniqueness : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → {k' : Hom A d c } → | |
| 148 A [ A [ e o k' ] ≈ h ] → A [ k {d} h eq ≈ k' ] | |
| 149 equalizer : Hom A c a | |
| 150 equalizer = e | |
| 151 | |
| 152 -- | |
| 153 -- Product | |
| 154 -- | |
| 155 -- | |
| 156 -- | |
| 157 -- | |
| 158 -- | |
| 159 -- | |
| 160 -- | |
| 161 | |
| 162 | |
| 163 record Product { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a b ab : Obj A) | |
| 164 ( π1 : Hom A ab a ) | |
| 165 ( π2 : Hom A ab b ) | |
| 166 : Set (ℓ ⊔ (c₁ ⊔ c₂)) where | |
| 167 field | |
| 168 _×_ : {c : Obj A} ( f : Hom A c a ) → ( g : Hom A c b ) → Hom A c ab | |
| 169 π1fxg=f : {c : Obj A} { f : Hom A c a } → { g : Hom A c b } → A [ A [ π1 o ( f × g ) ] ≈ f ] | |
| 170 π2fxg=g : {c : Obj A} { f : Hom A c a } → { g : Hom A c b } → A [ A [ π2 o ( f × g ) ] ≈ g ] | |
| 171 uniqueness : {c : Obj A} { h : Hom A c ab } → A [ ( A [ π1 o h ] ) × ( A [ π2 o h ] ) ≈ h ] | |
| 172 axb : Obj A | |
| 173 axb = ab | |
| 174 | |
| 175 -- | |
| 176 -- Pullback | |
| 177 -- f | |
| 178 -- a -------> c | |
| 179 -- ^ ^ | |
| 180 -- π1 | |g | |
| 181 -- | | | |
| 182 -- ab -------> b | |
| 183 -- ^ π2 | |
| 184 -- | | |
| 185 -- d | |
| 186 -- | |
| 187 record Pullback { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a b c ab : Obj A) | |
| 188 ( f : Hom A a c ) ( g : Hom A b c ) | |
| 189 ( π1 : Hom A ab a ) ( π2 : Hom A ab b ) | |
| 190 : Set (ℓ ⊔ (c₁ ⊔ c₂)) where | |
| 191 field | |
| 192 commute : A [ A [ f o π1 ] ≈ A [ g o π2 ] ] | |
| 193 p : { d : Obj A } → { π1' : Hom A d a } { π2' : Hom A d b } → A [ A [ f o π1' ] ≈ A [ g o π2' ] ] → Hom A d ab | |
| 194 π1p=π1 : { d : Obj A } → { π1' : Hom A d a } { π2' : Hom A d b } → { eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ] } | |
| 195 → A [ A [ π1 o p eq ] ≈ π1' ] | |
| 196 π2p=π2 : { d : Obj A } → { π1' : Hom A d a } { π2' : Hom A d b } → { eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ] } | |
| 197 → A [ A [ π2 o p eq ] ≈ π2' ] | |
| 198 uniqueness : { d : Obj A } → ( p' : Hom A d ab ) → { π1' : Hom A d a } { π2' : Hom A d b } → { eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ] } | |
| 199 → { π1p=π1' : A [ A [ π1 o p' ] ≈ π1' ] } | |
| 200 → { π2p=π2' : A [ A [ π2 o p' ] ≈ π2' ] } | |
| 201 → A [ p eq ≈ p' ] | |
| 202 axb : Obj A | |
| 203 axb = ab |