Mercurial > hg > Members > kono > Proof > category
annotate HomReasoning.agda @ 130:5f331dfc000b
remove Kleisli record
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 08 Aug 2013 22:05:41 +0900 |
| parents | 8e665152c306 |
| children | a9f5cfbbc0fa |
| rev | line source |
|---|---|
| 56 | 1 module HomReasoning where |
| 31 | 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 Functor | |
| 8 | |
| 9 | |
| 10 -- F(f) | |
| 11 -- F(a) ---→ F(b) | |
| 12 -- | | | |
| 13 -- |t(a) |t(b) G(f)t(a) = t(b)F(f) | |
| 14 -- | | | |
| 15 -- v v | |
| 16 -- G(a) ---→ G(b) | |
| 17 -- G(f) | |
| 18 | |
| 19 record IsNTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (D : Category c₁ c₂ ℓ) (C : Category c₁′ c₂′ ℓ′) | |
| 20 ( F G : Functor D C ) | |
| 21 (TMap : (A : Obj D) → Hom C (FObj F A) (FObj G A)) | |
| 22 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where | |
| 23 field | |
| 130 | 24 commute : {a b : Obj D} {f : Hom D a b} |
| 31 | 25 → C [ C [ ( FMap G f ) o ( TMap a ) ] ≈ C [ (TMap b ) o (FMap F f) ] ] |
| 26 | |
| 130 | 27 record NTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (domain : Category c₁ c₂ ℓ) (codomain : Category c₁′ c₂′ ℓ′) |
| 28 (F G : Functor domain codomain ) | |
| 31 | 29 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where |
| 30 field | |
| 31 TMap : (A : Obj domain) → Hom codomain (FObj F A) (FObj G A) | |
| 32 isNTrans : IsNTrans domain codomain F G TMap | |
| 33 | |
| 34 | |
| 35 module ≈-Reasoning {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) where | |
| 36 open import Relation.Binary.Core | |
| 37 | |
| 38 _o_ : {a b c : Obj A } ( x : Hom A a b ) ( y : Hom A c a ) → Hom A c b | |
| 39 x o y = A [ x o y ] | |
| 40 | |
| 41 _≈_ : {a b : Obj A } → Rel (Hom A a b) ℓ | |
| 42 x ≈ y = A [ x ≈ y ] | |
| 43 | |
| 44 infixr 9 _o_ | |
| 45 infix 4 _≈_ | |
| 46 | |
| 47 refl-hom : {a b : Obj A } { x : Hom A a b } → x ≈ x | |
| 48 refl-hom = IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory A )) | |
| 49 | |
| 50 trans-hom : {a b : Obj A } { x y z : Hom A a b } → | |
| 51 x ≈ y → y ≈ z → x ≈ z | |
| 52 trans-hom b c = ( IsEquivalence.trans (IsCategory.isEquivalence ( Category.isCategory A ))) b c | |
| 53 | |
| 54 -- some short cuts | |
| 55 | |
| 56 car : {a b c : Obj A } {x y : Hom A a b } { f : Hom A c a } → | |
| 57 x ≈ y → ( x o f ) ≈ ( y o f ) | |
| 58 car {f} eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) ( refl-hom ) eq | |
| 59 | |
| 60 cdr : {a b c : Obj A } {x y : Hom A a b } { f : Hom A b c } → | |
| 61 x ≈ y → f o x ≈ f o y | |
| 62 cdr {f} eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) eq (refl-hom ) | |
| 63 | |
| 64 id : (a : Obj A ) → Hom A a a | |
| 65 id a = (Id {_} {_} {_} {A} a) | |
| 66 | |
| 67 idL : {a b : Obj A } { f : Hom A b a } → id a o f ≈ f | |
| 68 idL = IsCategory.identityL (Category.isCategory A) | |
| 69 | |
| 70 idR : {a b : Obj A } { f : Hom A a b } → f o id a ≈ f | |
| 71 idR = IsCategory.identityR (Category.isCategory A) | |
| 72 | |
| 73 sym : {a b : Obj A } { f g : Hom A a b } → f ≈ g → g ≈ f | |
| 74 sym = IsEquivalence.sym (IsCategory.isEquivalence (Category.isCategory A)) | |
| 75 | |
| 67 | 76 -- How to prove this? |
| 75 | 77 ≡-≈ : {a b : Obj A } { x y : Hom A a b } → (x≈y : x ≡ y ) → x ≈ y |
| 78 ≡-≈ refl = refl-hom | |
| 79 | |
| 80 -- ≈-≡ : {a b : Obj A } { x y : Hom A a b } → (x≈y : x ≈ y ) → x ≡ y | |
| 81 -- ≈-≡ x≈y = irr x≈y | |
| 82 ≡-cong : { c₁′ c₂′ ℓ′ : Level} {B : Category c₁′ c₂′ ℓ′} {x y : Obj B } { a b : Hom B x y } {x' y' : Obj A } → | |
| 83 a ≡ b → (f : Hom B x y → Hom A x' y' ) → f a ≈ f b | |
| 84 ≡-cong refl f = ≡-≈ refl | |
| 85 | |
| 67 | 86 -- cong-≈ : { c₁′ c₂′ ℓ′ : Level} {B : Category c₁′ c₂′ ℓ′} {x y : Obj B } { a b : Hom B x y } {x' y' : Obj A } → |
| 87 -- B [ a ≈ b ] → (f : Hom B x y → Hom A x' y' ) → f a ≈ f b | |
| 75 | 88 -- cong-≈ eq f = {!!} |
| 67 | 89 |
|
69
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
67
diff
changeset
|
90 assoc : {a b c d : Obj A } {f : Hom A c d} {g : Hom A b c} {h : Hom A a b} |
|
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
67
diff
changeset
|
91 → A [ A [ f o ( A [ g o h ] ) ] ≈ A [ ( A [ f o g ] ) o h ] ] |
| 31 | 92 assoc = IsCategory.associative (Category.isCategory A) |
| 93 | |
|
69
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
67
diff
changeset
|
94 -- slow but working on another cateogry |
|
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
67
diff
changeset
|
95 assoc1 : { c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} {a b c d : Obj A } {f : Hom A c d} {g : Hom A b c} {h : Hom A a b} |
|
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
67
diff
changeset
|
96 → A [ A [ f o ( A [ g o h ] ) ] ≈ A [ ( A [ f o g ] ) o h ] ] |
|
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
67
diff
changeset
|
97 assoc1 {_} {_} {_} {A} = IsCategory.associative (Category.isCategory A) |
|
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
67
diff
changeset
|
98 |
|
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
67
diff
changeset
|
99 distr : { c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} |
|
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
67
diff
changeset
|
100 { c₁′ c₂′ ℓ′ : Level} {D : Category c₁′ c₂′ ℓ′} (T : Functor D A) → {a b c : Obj D} {g : Hom D b c} { f : Hom D a b } |
|
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
67
diff
changeset
|
101 → A [ FMap T ( D [ g o f ] ) ≈ A [ FMap T g o FMap T f ] ] |
| 75 | 102 distr T = IsFunctor.distr ( isFunctor T ) |
| 103 | |
| 104 resp : {a b c : Obj A} {f g : Hom A a b} {h i : Hom A b c} → f ≈ g → h ≈ i → (h o f) ≈ (i o g) | |
| 105 resp = IsCategory.o-resp-≈ (Category.isCategory A) | |
| 106 | |
| 107 fcong : { c₁ c₂ ℓ : Level} {C : Category c₁ c₂ ℓ} | |
| 108 { c₁′ c₂′ ℓ′ : Level} {D : Category c₁′ c₂′ ℓ′} {a b : Obj C} {f g : Hom C a b} → (T : Functor C D) → C [ f ≈ g ] → D [ FMap T f ≈ FMap T g ] | |
| 109 fcong T = IsFunctor.≈-cong (isFunctor T) | |
| 31 | 110 |
| 111 open NTrans | |
|
69
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
67
diff
changeset
|
112 nat : { c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} { c₁′ c₂′ ℓ′ : Level} {D : Category c₁′ c₂′ ℓ′} |
|
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
67
diff
changeset
|
113 {a b : Obj D} {f : Hom D a b} {F G : Functor D A } |
| 31 | 114 → (η : NTrans D A F G ) |
|
69
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
67
diff
changeset
|
115 → A [ A [ FMap G f o TMap η a ] ≈ A [ TMap η b o FMap F f ] ] |
| 130 | 116 nat η = IsNTrans.commute ( isNTrans η ) |
| 31 | 117 |
| 118 infixr 2 _∎ | |
| 119 infixr 2 _≈⟨_⟩_ _≈⟨⟩_ | |
| 120 infix 1 begin_ | |
| 121 | |
| 122 ------ If we have this, for example, as an axiom of a category, we can use ≡-Reasoning directly | |
| 123 -- ≈-to-≡ : {a b : Obj A } { x y : Hom A a b } → A [ x ≈ y ] → x ≡ y | |
| 124 -- ≈-to-≡ refl-hom = refl | |
| 125 | |
| 126 data _IsRelatedTo_ { a b : Obj A } ( x y : Hom A a b ) : | |
| 127 Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where | |
| 128 relTo : (x≈y : x ≈ y ) → x IsRelatedTo y | |
| 129 | |
| 130 begin_ : { a b : Obj A } { x y : Hom A a b } → | |
| 131 x IsRelatedTo y → x ≈ y | |
| 132 begin relTo x≈y = x≈y | |
| 133 | |
| 134 _≈⟨_⟩_ : { a b : Obj A } ( x : Hom A a b ) → { y z : Hom A a b } → | |
| 135 x ≈ y → y IsRelatedTo z → x IsRelatedTo z | |
| 136 _ ≈⟨ x≈y ⟩ relTo y≈z = relTo (trans-hom x≈y y≈z) | |
| 137 | |
| 138 _≈⟨⟩_ : { a b : Obj A } ( x : Hom A a b ) → { y : Hom A a b } → x IsRelatedTo y → x IsRelatedTo y | |
| 139 _ ≈⟨⟩ x∼y = x∼y | |
| 140 | |
| 141 _∎ : { a b : Obj A } ( x : Hom A a b ) → x IsRelatedTo x | |
| 142 _∎ _ = relTo refl-hom | |
| 143 | |
| 56 | 144 -- an example |
| 145 | |
| 146 Lemma61 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) → | |
| 147 { a : Obj A } ( b : Obj A ) → | |
| 148 ( f : Hom A a b ) | |
| 149 → A [ A [ (Id {_} {_} {_} {A} b) o f ] ≈ f ] | |
| 150 Lemma61 c b g = -- IsCategory.identityL (Category.isCategory c) | |
| 151 let open ≈-Reasoning (c) in | |
| 152 begin | |
| 153 c [ Id {_} {_} {_} {c} b o g ] | |
| 154 ≈⟨ IsCategory.identityL (Category.isCategory c) ⟩ | |
| 155 g | |
| 156 ∎ |