Mercurial > hg > Members > kono > Proof > category
annotate src/HomReasoning.agda @ 1124:f683d96fbc93 default tip
safe fix done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 07 Jul 2024 22:28:50 +0900 |
| parents | 45de2b31bf02 |
| children |
| rev | line source |
|---|---|
|
1110
45de2b31bf02
add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1106
diff
changeset
|
1 {-# OPTIONS --cubical-compatible --safe #-} |
| 56 | 2 module HomReasoning where |
| 31 | 3 |
| 4 -- Shinji KONO <kono@ie.u-ryukyu.ac.jp> | |
| 5 | |
| 6 open import Level | |
|
1110
45de2b31bf02
add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1106
diff
changeset
|
7 open import Category |
| 31 | 8 |
| 9 module ≈-Reasoning {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) where | |
|
949
ac53803b3b2a
reorganization for apkg
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
948
diff
changeset
|
10 open import Relation.Binary |
|
1110
45de2b31bf02
add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1106
diff
changeset
|
11 open Functor |
| 31 | 12 |
| 13 _o_ : {a b c : Obj A } ( x : Hom A a b ) ( y : Hom A c a ) → Hom A c b | |
| 14 x o y = A [ x o y ] | |
| 15 | |
| 16 _≈_ : {a b : Obj A } → Rel (Hom A a b) ℓ | |
| 17 x ≈ y = A [ x ≈ y ] | |
| 18 | |
| 19 infixr 9 _o_ | |
| 20 infix 4 _≈_ | |
| 21 | |
| 22 refl-hom : {a b : Obj A } { x : Hom A a b } → x ≈ x | |
| 23 refl-hom = IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory A )) | |
| 24 | |
| 25 trans-hom : {a b : Obj A } { x y z : Hom A a b } → | |
| 26 x ≈ y → y ≈ z → x ≈ z | |
| 27 trans-hom b c = ( IsEquivalence.trans (IsCategory.isEquivalence ( Category.isCategory A ))) b c | |
| 28 | |
| 29 -- some short cuts | |
| 30 | |
| 31 car : {a b c : Obj A } {x y : Hom A a b } { f : Hom A c a } → | |
| 32 x ≈ y → ( x o f ) ≈ ( y o f ) | |
| 787 | 33 car eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) ( refl-hom ) eq |
| 34 | |
| 35 car1 : { c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b c : Obj A } {x y : Hom A a b } { f : Hom A c a } → | |
| 36 A [ x ≈ y ] → A [ A [ x o f ] ≈ A [ y o f ] ] | |
| 37 car1 A eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) ( IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory A )) ) eq | |
| 31 | 38 |
| 39 cdr : {a b c : Obj A } {x y : Hom A a b } { f : Hom A b c } → | |
| 40 x ≈ y → f o x ≈ f o y | |
| 787 | 41 cdr eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) eq (refl-hom ) |
| 42 | |
| 43 cdr1 : { c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b c : Obj A } {x y : Hom A a b } { f : Hom A b c } → | |
| 44 A [ x ≈ y ] → A [ A [ f o x ] ≈ A [ f o y ] ] | |
| 45 cdr1 A eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) eq (IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory A )) ) | |
| 31 | 46 |
| 47 id : (a : Obj A ) → Hom A a a | |
| 48 id a = (Id {_} {_} {_} {A} a) | |
| 49 | |
|
479
a5034bdf6f38
Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
50 idL : {a b : Obj A } { f : Hom A a b } → id b o f ≈ f |
| 31 | 51 idL = IsCategory.identityL (Category.isCategory A) |
| 52 | |
| 53 idR : {a b : Obj A } { f : Hom A a b } → f o id a ≈ f | |
| 54 idR = IsCategory.identityR (Category.isCategory A) | |
| 55 | |
| 56 sym : {a b : Obj A } { f g : Hom A a b } → f ≈ g → g ≈ f | |
| 57 sym = IsEquivalence.sym (IsCategory.isEquivalence (Category.isCategory A)) | |
| 58 | |
| 455 | 59 sym-hom = sym |
| 60 | |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
61 -- working on another cateogry |
|
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
62 idL1 : { c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A } { f : Hom A b a } → A [ A [ Id {_} {_} {_} {A} a o f ] ≈ f ] |
|
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
63 idL1 A = IsCategory.identityL (Category.isCategory A) |
|
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
64 |
|
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
65 idR1 : { c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A } { f : Hom A a b } → A [ A [ f o Id {_} {_} {_} {A} a ] ≈ f ] |
|
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
66 idR1 A = IsCategory.identityR (Category.isCategory A) |
|
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
67 |
| 781 | 68 open import Relation.Binary.PropositionalEquality using ( _≡_ ) |
| 693 | 69 ≈←≡ : {a b : Obj A } { x y : Hom A a b } → (x≈y : x ≡ y ) → x ≈ y |
| 781 | 70 ≈←≡ _≡_.refl = refl-hom |
| 75 | 71 |
| 693 | 72 -- Ho← to prove this? |
| 73 -- ≡←≈ : {a b : Obj A } { x y : Hom A a b } → (x≈y : x ≈ y ) → x ≡ y | |
| 74 -- ≡←≈ x≈y = irr x≈y | |
| 75 | |
| 75 | 76 ≡-cong : { c₁′ c₂′ ℓ′ : Level} {B : Category c₁′ c₂′ ℓ′} {x y : Obj B } { a b : Hom B x y } {x' y' : Obj A } → |
|
420
3e44951b9bdb
refl in free-monoid trouble
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
299
diff
changeset
|
77 (f : Hom B x y → Hom A x' y' ) → a ≡ b → f a ≈ f b |
| 781 | 78 ≡-cong f _≡_.refl = ≈←≡ _≡_.refl |
| 75 | 79 |
| 67 | 80 -- cong-≈ : { c₁′ c₂′ ℓ′ : Level} {B : Category c₁′ c₂′ ℓ′} {x y : Obj B } { a b : Hom B x y } {x' y' : Obj A } → |
| 81 -- B [ a ≈ b ] → (f : Hom B x y → Hom A x' y' ) → f a ≈ f b | |
| 75 | 82 -- cong-≈ eq f = {!!} |
| 67 | 83 |
|
69
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
67
diff
changeset
|
84 assoc : {a b c d : Obj A } {f : Hom A c d} {g : Hom A b c} {h : Hom A a b} |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
85 → f o ( g o h ) ≈ ( f o g ) o h |
| 31 | 86 assoc = IsCategory.associative (Category.isCategory A) |
| 87 | |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
88 -- working on another cateogry |
|
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
89 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} |
|
69
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
67
diff
changeset
|
90 → A [ A [ f o ( A [ g o h ] ) ] ≈ A [ ( A [ f o g ] ) o h ] ] |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
91 assoc1 A = IsCategory.associative (Category.isCategory A) |
|
69
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
67
diff
changeset
|
92 |
|
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
67
diff
changeset
|
93 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
|
94 { 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
|
95 → A [ FMap T ( D [ g o f ] ) ≈ A [ FMap T g o FMap T f ] ] |
| 75 | 96 distr T = IsFunctor.distr ( isFunctor T ) |
| 97 | |
| 98 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) | |
| 99 resp = IsCategory.o-resp-≈ (Category.isCategory A) | |
| 100 | |
| 101 fcong : { c₁ c₂ ℓ : Level} {C : Category c₁ c₂ ℓ} | |
| 102 { 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 ] | |
| 103 fcong T = IsFunctor.≈-cong (isFunctor T) | |
| 31 | 104 |
| 606 | 105 infix 3 _∎ |
| 31 | 106 infixr 2 _≈⟨_⟩_ _≈⟨⟩_ |
| 168 | 107 infixr 2 _≈↑⟨_⟩_ |
| 31 | 108 infix 1 begin_ |
| 109 | |
| 110 ------ If we have this, for example, as an axiom of a category, we can use ≡-Reasoning directly | |
| 111 -- ≈-to-≡ : {a b : Obj A } { x y : Hom A a b } → A [ x ≈ y ] → x ≡ y | |
| 112 -- ≈-to-≡ refl-hom = refl | |
| 113 | |
| 114 data _IsRelatedTo_ { a b : Obj A } ( x y : Hom A a b ) : | |
| 115 Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where | |
| 116 relTo : (x≈y : x ≈ y ) → x IsRelatedTo y | |
| 117 | |
| 118 begin_ : { a b : Obj A } { x y : Hom A a b } → | |
| 119 x IsRelatedTo y → x ≈ y | |
| 120 begin relTo x≈y = x≈y | |
| 121 | |
| 122 _≈⟨_⟩_ : { a b : Obj A } ( x : Hom A a b ) → { y z : Hom A a b } → | |
| 123 x ≈ y → y IsRelatedTo z → x IsRelatedTo z | |
| 124 _ ≈⟨ x≈y ⟩ relTo y≈z = relTo (trans-hom x≈y y≈z) | |
| 125 | |
| 168 | 126 _≈↑⟨_⟩_ : { a b : Obj A } ( x : Hom A a b ) → { y z : Hom A a b } → |
| 127 y ≈ x → y IsRelatedTo z → x IsRelatedTo z | |
| 128 _ ≈↑⟨ y≈x ⟩ relTo y≈z = relTo (trans-hom ( sym y≈x ) y≈z) | |
| 129 | |
| 31 | 130 _≈⟨⟩_ : { a b : Obj A } ( x : Hom A a b ) → { y : Hom A a b } → x IsRelatedTo y → x IsRelatedTo y |
| 131 _ ≈⟨⟩ x∼y = x∼y | |
| 132 | |
| 133 _∎ : { a b : Obj A } ( x : Hom A a b ) → x IsRelatedTo x | |
| 134 _∎ _ = relTo refl-hom | |
| 135 | |
| 948 | 136 |
| 1106 | 137 -- examples |
| 56 | 138 |
| 139 Lemma61 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) → | |
| 140 { a : Obj A } ( b : Obj A ) → | |
| 141 ( f : Hom A a b ) | |
| 142 → A [ A [ (Id {_} {_} {_} {A} b) o f ] ≈ f ] | |
| 143 Lemma61 c b g = -- IsCategory.identityL (Category.isCategory c) | |
| 606 | 144 let open ≈-Reasoning (c) in begin |
| 145 c [ ( Id {_} {_} {_} {c} b ) o g ] | |
| 56 | 146 ≈⟨ IsCategory.identityL (Category.isCategory c) ⟩ |
| 147 g | |
| 148 ∎ | |
| 253 | 149 |
| 150 Lemma62 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) → | |
| 151 { a b : Obj A } → | |
| 152 ( f g : Hom A a b ) | |
| 153 → A [ A [ (Id {_} {_} {_} {A} b) o f ] ≈ A [ (Id {_} {_} {_} {A} b) o g ] ] | |
| 154 → A [ g ≈ f ] | |
| 155 Lemma62 A {a} {b} f g 1g=1f = let open ≈-Reasoning A in | |
| 156 begin | |
| 157 g | |
| 158 ≈↑⟨ idL ⟩ | |
| 159 id b o g | |
| 160 ≈↑⟨ 1g=1f ⟩ | |
| 161 id b o f | |
| 162 ≈⟨ idL ⟩ | |
| 163 f | |
| 164 ∎ |