Mercurial > hg > Members > kono > Proof > category
annotate Comma.agda @ 920:c10ee19a1ea3
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 04 May 2020 14:34:42 +0900 |
| parents | bed3be9a4168 |
| children |
| rev | line source |
|---|---|
| 477 | 1 open import Level |
| 2 open import Category | |
| 623 | 3 module Comma {c₁ c₂ ℓ c₁' c₂' ℓ' c₁'' c₂'' ℓ'' : Level} {A : Category c₁ c₂ ℓ} {B : Category c₁'' c₂'' ℓ''} {C : Category c₁' c₂' ℓ'} |
|
479
a5034bdf6f38
Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
478
diff
changeset
|
4 ( F : Functor A C ) ( G : Functor B C ) where |
| 477 | 5 |
| 6 open import HomReasoning | |
| 7 open import cat-utility | |
| 8 | |
| 478 | 9 -- |
| 10 -- F G | |
| 11 -- A -> C <- B | |
| 12 -- | |
| 477 | 13 |
| 14 open Functor | |
| 15 | |
| 623 | 16 record CommaObj : Set ( c₁ ⊔ c₁'' ⊔ c₂' ) where |
| 477 | 17 field |
| 18 obj : Obj A | |
|
479
a5034bdf6f38
Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
478
diff
changeset
|
19 objb : Obj B |
|
a5034bdf6f38
Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
478
diff
changeset
|
20 hom : Hom C ( FObj F obj ) ( FObj G objb ) |
| 477 | 21 |
| 22 open CommaObj | |
| 23 | |
| 623 | 24 record CommaHom ( a b : CommaObj ) : Set ( c₂ ⊔ c₂'' ⊔ ℓ' ) where |
| 477 | 25 field |
| 26 arrow : Hom A ( obj a ) ( obj b ) | |
|
479
a5034bdf6f38
Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
478
diff
changeset
|
27 arrowg : Hom B ( objb a ) ( objb b ) |
|
a5034bdf6f38
Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
478
diff
changeset
|
28 comm : C [ C [ FMap G arrowg o hom a ] ≈ C [ hom b o FMap F arrow ] ] |
| 477 | 29 |
| 30 open CommaHom | |
| 31 | |
| 623 | 32 record _⋍_ { a b : CommaObj } ( f g : CommaHom a b ) : Set (ℓ ⊔ ℓ'' ) where |
|
479
a5034bdf6f38
Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
478
diff
changeset
|
33 field |
|
a5034bdf6f38
Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
478
diff
changeset
|
34 eqa : A [ arrow f ≈ arrow g ] |
|
a5034bdf6f38
Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
478
diff
changeset
|
35 eqb : B [ arrowg f ≈ arrowg g ] |
|
a5034bdf6f38
Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
478
diff
changeset
|
36 |
|
a5034bdf6f38
Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
478
diff
changeset
|
37 open _⋍_ |
| 477 | 38 |
| 39 _∙_ : {a b c : CommaObj } → CommaHom b c → CommaHom a b → CommaHom a c | |
| 40 _∙_ {a} {b} {c} f g = record { | |
| 41 arrow = A [ arrow f o arrow g ] ; | |
| 492 | 42 arrowg = B [ arrowg f o arrowg g ] ; |
| 477 | 43 comm = comm1 |
| 44 } where | |
|
479
a5034bdf6f38
Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
478
diff
changeset
|
45 comm1 : C [ C [ FMap G (B [ arrowg f o arrowg g ] ) o hom a ] ≈ C [ hom c o FMap F (A [ arrow f o arrow g ]) ] ] |
| 478 | 46 comm1 = let open ≈-Reasoning C in begin |
|
479
a5034bdf6f38
Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
478
diff
changeset
|
47 FMap G (B [ arrowg f o arrowg g ] ) o hom a |
| 478 | 48 ≈⟨ car ( distr G ) ⟩ |
|
479
a5034bdf6f38
Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
478
diff
changeset
|
49 ( FMap G (arrowg f) o FMap G (arrowg g )) o hom a |
| 478 | 50 ≈↑⟨ assoc ⟩ |
|
479
a5034bdf6f38
Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
478
diff
changeset
|
51 FMap G (arrowg f) o ( FMap G (arrowg g ) o hom a ) |
| 478 | 52 ≈⟨ cdr ( comm g ) ⟩ |
|
479
a5034bdf6f38
Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
478
diff
changeset
|
53 FMap G (arrowg f) o ( hom b o FMap F (arrow g ) ) |
| 478 | 54 ≈⟨ assoc ⟩ |
|
479
a5034bdf6f38
Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
478
diff
changeset
|
55 ( FMap G (arrowg f) o hom b) o FMap F (arrow g ) |
| 478 | 56 ≈⟨ car ( comm f ) ⟩ |
| 57 ( hom c o FMap F (arrow f) ) o FMap F (arrow g ) | |
| 58 ≈↑⟨ assoc ⟩ | |
| 59 hom c o ( FMap F (arrow f) o FMap F (arrow g ) ) | |
| 60 ≈↑⟨ cdr ( distr F) ⟩ | |
| 61 hom c o FMap F (A [ arrow f o arrow g ]) | |
| 62 ∎ | |
| 477 | 63 |
| 64 CommaId : { a : CommaObj } → CommaHom a a | |
| 492 | 65 CommaId {a} = record { arrow = id1 A ( obj a ) ; arrowg = id1 B ( objb a ) ; |
| 477 | 66 comm = comm2 } where |
|
479
a5034bdf6f38
Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
478
diff
changeset
|
67 comm2 : C [ C [ FMap G (id1 B (objb a)) o hom a ] ≈ C [ hom a o FMap F (id1 A (obj a)) ] ] |
| 478 | 68 comm2 = let open ≈-Reasoning C in begin |
|
479
a5034bdf6f38
Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
478
diff
changeset
|
69 FMap G (id1 B (objb a)) o hom a |
| 478 | 70 ≈⟨ car ( IsFunctor.identity ( isFunctor G ) ) ⟩ |
|
479
a5034bdf6f38
Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
478
diff
changeset
|
71 id1 C (FObj G (objb a)) o hom a |
| 478 | 72 ≈⟨ idL ⟩ |
| 73 hom a | |
| 74 ≈↑⟨ idR ⟩ | |
| 75 hom a o id1 C (FObj F (obj a)) | |
| 76 ≈↑⟨ cdr ( IsFunctor.identity ( isFunctor F ) )⟩ | |
| 77 hom a o FMap F (id1 A (obj a)) | |
| 78 ∎ | |
| 477 | 79 |
| 80 isCommaCategory : IsCategory CommaObj CommaHom _⋍_ _∙_ CommaId | |
| 81 isCommaCategory = record { | |
|
479
a5034bdf6f38
Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
478
diff
changeset
|
82 isEquivalence = record { refl = record { eqa = let open ≈-Reasoning (A) in refl-hom ; eqb = let open ≈-Reasoning (B) in refl-hom } ; |
|
a5034bdf6f38
Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
478
diff
changeset
|
83 sym = λ {f} {g} f=g → record { eqa = let open ≈-Reasoning (A) in sym ( eqa f=g) ; eqb = let open ≈-Reasoning (B) in sym ( eqb f=g ) } ; |
|
a5034bdf6f38
Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
478
diff
changeset
|
84 trans = λ {f} {g} {h} f=g g=h → record { |
|
a5034bdf6f38
Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
478
diff
changeset
|
85 eqa = let open ≈-Reasoning (A) in trans-hom (eqa f=g) (eqa g=h) |
|
a5034bdf6f38
Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
478
diff
changeset
|
86 ; eqb = let open ≈-Reasoning (B) in trans-hom (eqb f=g) (eqb g=h) |
|
a5034bdf6f38
Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
478
diff
changeset
|
87 } } |
|
a5034bdf6f38
Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
478
diff
changeset
|
88 ; identityL = λ{a b f} → record { |
|
a5034bdf6f38
Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
478
diff
changeset
|
89 eqa = let open ≈-Reasoning (A) in idL {obj a} {obj b} {arrow f} |
|
a5034bdf6f38
Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
478
diff
changeset
|
90 ; eqb = let open ≈-Reasoning (B) in idL {objb a} {objb b} {arrowg f} |
|
a5034bdf6f38
Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
478
diff
changeset
|
91 } |
|
a5034bdf6f38
Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
478
diff
changeset
|
92 ; identityR = λ{a b f} → record { |
|
a5034bdf6f38
Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
478
diff
changeset
|
93 eqa = let open ≈-Reasoning (A) in idR {obj a} {obj b} {arrow f} |
|
a5034bdf6f38
Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
478
diff
changeset
|
94 ; eqb = let open ≈-Reasoning (B) in idR {objb a} {objb b} {arrowg f} |
|
a5034bdf6f38
Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
478
diff
changeset
|
95 } |
|
a5034bdf6f38
Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
478
diff
changeset
|
96 ; o-resp-≈ = λ {a b c } {f g } {h i } f=g h=i → record { |
|
a5034bdf6f38
Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
478
diff
changeset
|
97 eqa = IsCategory.o-resp-≈ (Category.isCategory A) (eqa f=g) (eqa h=i ) |
|
a5034bdf6f38
Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
478
diff
changeset
|
98 ; eqb = IsCategory.o-resp-≈ (Category.isCategory B) (eqb f=g) (eqb h=i ) |
|
a5034bdf6f38
Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
478
diff
changeset
|
99 } |
|
a5034bdf6f38
Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
478
diff
changeset
|
100 ; associative = λ {a b c d} {f} {g} {h} → record { |
|
a5034bdf6f38
Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
478
diff
changeset
|
101 eqa = IsCategory.associative (Category.isCategory A) |
|
a5034bdf6f38
Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
478
diff
changeset
|
102 ; eqb = IsCategory.associative (Category.isCategory B) |
|
a5034bdf6f38
Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
478
diff
changeset
|
103 } |
|
a5034bdf6f38
Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
478
diff
changeset
|
104 } |
| 478 | 105 |
| 623 | 106 CommaCategory : Category (c₂' ⊔ c₁ ⊔ c₁'') (ℓ' ⊔ c₂ ⊔ c₂'') (ℓ ⊔ ℓ'' ) |
| 480 | 107 CommaCategory = record { Obj = CommaObj |
| 478 | 108 ; Hom = CommaHom |
| 109 ; _o_ = _∙_ | |
| 110 ; _≈_ = _⋍_ | |
| 111 ; Id = CommaId | |
| 112 ; isCategory = isCommaCategory | |
| 113 } | |
| 477 | 114 |