Mercurial > hg > Members > kono > Proof > category

annotate Comma.agda @ 479:a5034bdf6f38

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Comma Category with A B C
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 09 Mar 2017 14:16:03 +0900
parents dc24ac6ebdb3
children 08f9c8a59ff4
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
477
bcf941e20737 add Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 open import Level
bcf941e20737 add Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 open import Category
479
a5034bdf6f38 Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 478
diff changeset
3 module Comma {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} {A : Category c₁ c₂ ℓ} {B : Category c₁ c₂ ℓ} {C : Category c₁' c₂' ℓ'}
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
bcf941e20737 add Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5
bcf941e20737 add Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 open import HomReasoning
bcf941e20737 add Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 open import cat-utility
bcf941e20737 add Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8
478
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
9 --
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
10 -- F G
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
11 -- A -> C <- B
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
12 --
477
bcf941e20737 add Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13
bcf941e20737 add Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 open Functor
bcf941e20737 add Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15
bcf941e20737 add Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 record CommaObj : Set ( c₁ ⊔ c₂' ) where
bcf941e20737 add Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 field
bcf941e20737 add Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
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
bcf941e20737 add Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21
bcf941e20737 add Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 open CommaObj
bcf941e20737 add Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23
bcf941e20737 add Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 record CommaHom ( a b : CommaObj ) : Set ( c₂ ⊔ ℓ' ) where
bcf941e20737 add Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 field
bcf941e20737 add Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
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
bcf941e20737 add Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29
bcf941e20737 add Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 open CommaHom
bcf941e20737 add Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31
479
a5034bdf6f38 Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 478
diff changeset
32 record _⋍_ { a b : CommaObj } ( f g : CommaHom a b ) : Set ℓ where
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
bcf941e20737 add Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38
bcf941e20737 add Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 _∙_ : {a b c : CommaObj } → CommaHom b c → CommaHom a b → CommaHom a c
bcf941e20737 add Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 _∙_ {a} {b} {c} f g = record {
bcf941e20737 add Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 arrow = A [ arrow f o arrow g ] ;
bcf941e20737 add Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 comm = comm1
bcf941e20737 add Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 } where
479
a5034bdf6f38 Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 478
diff changeset
44 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
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
45 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
46 FMap G (B [ arrowg f o arrowg g ] ) o hom a
478
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
47 ≈⟨ car ( distr G ) ⟩
479
a5034bdf6f38 Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 478
diff changeset
48 ( FMap G (arrowg f) o FMap G (arrowg g )) o hom a
478
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
49 ≈↑⟨ assoc ⟩
479
a5034bdf6f38 Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 478
diff changeset
50 FMap G (arrowg f) o ( FMap G (arrowg g ) o hom a )
478
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
51 ≈⟨ cdr ( comm g ) ⟩
479
a5034bdf6f38 Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 478
diff changeset
52 FMap G (arrowg f) o ( hom b o FMap F (arrow g ) )
478
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
53 ≈⟨ assoc ⟩
479
a5034bdf6f38 Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 478
diff changeset
54 ( FMap G (arrowg f) o hom b) o FMap F (arrow g )
478
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
55 ≈⟨ car ( comm f ) ⟩
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
56 ( hom c o FMap F (arrow f) ) o FMap F (arrow g )
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
57 ≈↑⟨ assoc ⟩
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
58 hom c o ( FMap F (arrow f) o FMap F (arrow g ) )
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
59 ≈↑⟨ cdr ( distr F) ⟩
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
60 hom c o FMap F (A [ arrow f o arrow g ])
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
61 ∎
477
bcf941e20737 add Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62
bcf941e20737 add Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63 CommaId : { a : CommaObj } → CommaHom a a
bcf941e20737 add Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64 CommaId {a} = record { arrow = id1 A ( obj a ) ;
bcf941e20737 add Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
65 comm = comm2 } where
479
a5034bdf6f38 Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 478
diff changeset
66 comm2 : C [ C [ FMap G (id1 B (objb a)) o hom a ] ≈ C [ hom a o FMap F (id1 A (obj a)) ] ]
478
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
67 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
68 FMap G (id1 B (objb a)) o hom a
478
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
69 ≈⟨ 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
70 id1 C (FObj G (objb a)) o hom a
478
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
71 ≈⟨ idL ⟩
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
72 hom a
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
73 ≈↑⟨ idR ⟩
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
74 hom a o id1 C (FObj F (obj a))
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
75 ≈↑⟨ cdr ( IsFunctor.identity ( isFunctor F ) )⟩
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
76 hom a o FMap F (id1 A (obj a))
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
77 ∎
477
bcf941e20737 add Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
78
bcf941e20737 add Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
79 isCommaCategory : IsCategory CommaObj CommaHom _⋍_ _∙_ CommaId
bcf941e20737 add Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
80 isCommaCategory = record {
479
a5034bdf6f38 Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 478
diff changeset
81 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
82 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
83 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
84 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
85 ; 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
86 } }
a5034bdf6f38 Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 478
diff changeset
87 ; identityL = λ{a b f} → record {
a5034bdf6f38 Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 478
diff changeset
88 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
89 ; 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
90 }
a5034bdf6f38 Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 478
diff changeset
91 ; identityR = λ{a b f} → record {
a5034bdf6f38 Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 478
diff changeset
92 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
93 ; 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
94 }
a5034bdf6f38 Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 478
diff changeset
95 ; 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
96 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
97 ; 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
98 }
a5034bdf6f38 Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 478
diff changeset
99 ; 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
100 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
101 ; 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
102 }
a5034bdf6f38 Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 478
diff changeset
103 }
478
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
104
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
105 _↓_ : Category (c₂' ⊔ c₁) (ℓ' ⊔ c₂) ℓ
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
106 _↓_ = record { Obj = CommaObj
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
107 ; Hom = CommaHom
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
108 ; _o_ = _∙_
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
109 ; _≈_ = _⋍_
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
110 ; Id = CommaId
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
111 ; isCategory = isCommaCategory
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
112 }
477
bcf941e20737 add Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
113
bcf941e20737 add Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
114