annotate Comma.agda @ 790:1e7319868d77

Sets is CCC
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 19 Apr 2019 23:42:19 +0900
parents bed3be9a4168
children
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
623
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 492
diff changeset
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
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
623
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 492
diff changeset
16 record CommaObj : Set ( c₁ ⊔ c₁'' ⊔ c₂' ) where
477
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
623
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 492
diff changeset
24 record CommaHom ( a b : CommaObj ) : Set ( c₂ ⊔ c₂'' ⊔ ℓ' ) where
477
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
623
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 492
diff changeset
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
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 ] ;
492
c7b8017bcd4d on going..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 480
diff changeset
42 arrowg = B [ arrowg f o arrowg g ] ;
477
bcf941e20737 add Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 comm = comm1
bcf941e20737 add Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
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
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
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
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
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
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
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
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
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
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
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
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
56 ≈⟨ car ( comm f ) ⟩
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
57 ( 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
58 ≈↑⟨ assoc ⟩
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
59 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
60 ≈↑⟨ cdr ( distr F) ⟩
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
61 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
62
477
bcf941e20737 add Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63
bcf941e20737 add Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64 CommaId : { a : CommaObj } → CommaHom a a
492
c7b8017bcd4d on going..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 480
diff changeset
65 CommaId {a} = record { arrow = id1 A ( obj a ) ; arrowg = id1 B ( objb a ) ;
477
bcf941e20737 add Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
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
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
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
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
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
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
72 ≈⟨ idL ⟩
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
73 hom a
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
74 ≈↑⟨ idR ⟩
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
75 hom a o id1 C (FObj F (obj a))
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
76 ≈↑⟨ cdr ( IsFunctor.identity ( isFunctor F ) )⟩
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
77 hom a o FMap F (id1 A (obj a))
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
78
477
bcf941e20737 add Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
79
bcf941e20737 add Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
80 isCommaCategory : IsCategory CommaObj CommaHom _⋍_ _∙_ CommaId
bcf941e20737 add Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
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
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
105
623
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 492
diff changeset
106 CommaCategory : Category (c₂' ⊔ c₁ ⊔ c₁'') (ℓ' ⊔ c₂ ⊔ c₂'') (ℓ ⊔ ℓ'' )
480
08f9c8a59ff4 add Comma1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 479
diff changeset
107 CommaCategory = record { Obj = CommaObj
478
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
108 ; Hom = CommaHom
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
109 ; _o_ = _∙_
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
110 ; _≈_ = _⋍_
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
111 ; Id = CommaId
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
112 ; isCategory = isCommaCategory
dc24ac6ebdb3 Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 477
diff changeset
113 }
477
bcf941e20737 add Comma category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
114