Mercurial > hg > Members > kono > Proof > category

comparison 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
comparison
equal deleted inserted replaced
478:dc24ac6ebdb3 479:a5034bdf6f38
1 open import Level 1 open import Level
2 open import Category 2 open import Category
3 module Comma {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} {A : Category c₁ c₂ ℓ} {B : Category c₁ c₂ ℓ} {C : Category c₁' c₂' ℓ'} ( F G : Functor A C ) where 3 module Comma {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} {A : Category c₁ c₂ ℓ} {B : Category c₁ c₂ ℓ} {C : Category c₁' c₂' ℓ'}
4 ( F : Functor A C ) ( G : Functor B C ) where
4 5
5 open import HomReasoning 6 open import HomReasoning
6 open import cat-utility 7 open import cat-utility
7 8
8 -- 9 --
9 -- F G 10 -- F G
10 -- A -> C <- B 11 -- A -> C <- B
11 -- 12 --
12 -- this a special case A = B
13 13
14 open Functor 14 open Functor
15 15
16 record CommaObj : Set ( c₁ ⊔ c₂' ) where 16 record CommaObj : Set ( c₁ ⊔ c₂' ) where
17 field 17 field
18 obj : Obj A 18 obj : Obj A
19 hom : Hom C ( FObj F obj ) ( FObj G obj ) 19 objb : Obj B
20 hom : Hom C ( FObj F obj ) ( FObj G objb )
20 21
21 open CommaObj 22 open CommaObj
22 23
23 record CommaHom ( a b : CommaObj ) : Set ( c₂ ⊔ ℓ' ) where 24 record CommaHom ( a b : CommaObj ) : Set ( c₂ ⊔ ℓ' ) where
24 field 25 field
25 arrow : Hom A ( obj a ) ( obj b ) 26 arrow : Hom A ( obj a ) ( obj b )
26 comm : C [ C [ FMap G arrow o hom a ] ≈ C [ hom b o FMap F arrow ] ] 27 arrowg : Hom B ( objb a ) ( objb b )
28 comm : C [ C [ FMap G arrowg o hom a ] ≈ C [ hom b o FMap F arrow ] ]
27 29
28 open CommaHom 30 open CommaHom
29 31
30 _⋍_ : { a b : CommaObj } ( f g : CommaHom a b ) → Set ℓ 32 record _⋍_ { a b : CommaObj } ( f g : CommaHom a b ) : Set ℓ where
31 _⋍_ f g = A [ arrow f ≈ arrow g ] 33 field
34 eqa : A [ arrow f ≈ arrow g ]
35 eqb : B [ arrowg f ≈ arrowg g ]
36
37 open _⋍_
32 38
33 _∙_ : {a b c : CommaObj } → CommaHom b c → CommaHom a b → CommaHom a c 39 _∙_ : {a b c : CommaObj } → CommaHom b c → CommaHom a b → CommaHom a c
34 _∙_ {a} {b} {c} f g = record { 40 _∙_ {a} {b} {c} f g = record {
35 arrow = A [ arrow f o arrow g ] ; 41 arrow = A [ arrow f o arrow g ] ;
36 comm = comm1 42 comm = comm1
37 } where 43 } where
38 comm1 : C [ C [ FMap G (A [ arrow f o arrow g ] ) o hom a ] ≈ C [ hom c o FMap F (A [ arrow f o arrow g ]) ] ] 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 ]) ] ]
39 comm1 = let open ≈-Reasoning C in begin 45 comm1 = let open ≈-Reasoning C in begin
40 FMap G (A [ arrow f o arrow g ] ) o hom a 46 FMap G (B [ arrowg f o arrowg g ] ) o hom a
41 ≈⟨ car ( distr G ) ⟩ 47 ≈⟨ car ( distr G ) ⟩
42 ( FMap G (arrow f) o FMap G (arrow g )) o hom a 48 ( FMap G (arrowg f) o FMap G (arrowg g )) o hom a
43 ≈↑⟨ assoc ⟩ 49 ≈↑⟨ assoc ⟩
44 FMap G (arrow f) o ( FMap G (arrow g ) o hom a ) 50 FMap G (arrowg f) o ( FMap G (arrowg g ) o hom a )
45 ≈⟨ cdr ( comm g ) ⟩ 51 ≈⟨ cdr ( comm g ) ⟩
46 FMap G (arrow f) o ( hom b o FMap F (arrow g ) ) 52 FMap G (arrowg f) o ( hom b o FMap F (arrow g ) )
47 ≈⟨ assoc ⟩ 53 ≈⟨ assoc ⟩
48 ( FMap G (arrow f) o hom b) o FMap F (arrow g ) 54 ( FMap G (arrowg f) o hom b) o FMap F (arrow g )
49 ≈⟨ car ( comm f ) ⟩ 55 ≈⟨ car ( comm f ) ⟩
50 ( hom c o FMap F (arrow f) ) o FMap F (arrow g ) 56 ( hom c o FMap F (arrow f) ) o FMap F (arrow g )
51 ≈↑⟨ assoc ⟩ 57 ≈↑⟨ assoc ⟩
52 hom c o ( FMap F (arrow f) o FMap F (arrow g ) ) 58 hom c o ( FMap F (arrow f) o FMap F (arrow g ) )
53 ≈↑⟨ cdr ( distr F) ⟩ 59 ≈↑⟨ cdr ( distr F) ⟩
55 ∎ 61 ∎
56 62
57 CommaId : { a : CommaObj } → CommaHom a a 63 CommaId : { a : CommaObj } → CommaHom a a
58 CommaId {a} = record { arrow = id1 A ( obj a ) ; 64 CommaId {a} = record { arrow = id1 A ( obj a ) ;
59 comm = comm2 } where 65 comm = comm2 } where
60 comm2 : C [ C [ FMap G (id1 A (obj a)) o hom a ] ≈ C [ hom a o FMap F (id1 A (obj a)) ] ] 66 comm2 : C [ C [ FMap G (id1 B (objb a)) o hom a ] ≈ C [ hom a o FMap F (id1 A (obj a)) ] ]
61 comm2 = let open ≈-Reasoning C in begin 67 comm2 = let open ≈-Reasoning C in begin
62 FMap G (id1 A (obj a)) o hom a 68 FMap G (id1 B (objb a)) o hom a
63 ≈⟨ car ( IsFunctor.identity ( isFunctor G ) ) ⟩ 69 ≈⟨ car ( IsFunctor.identity ( isFunctor G ) ) ⟩
64 id1 C (FObj G (obj a)) o hom a 70 id1 C (FObj G (objb a)) o hom a
65 ≈⟨ idL ⟩ 71 ≈⟨ idL ⟩
66 hom a 72 hom a
67 ≈↑⟨ idR ⟩ 73 ≈↑⟨ idR ⟩
68 hom a o id1 C (FObj F (obj a)) 74 hom a o id1 C (FObj F (obj a))
69 ≈↑⟨ cdr ( IsFunctor.identity ( isFunctor F ) )⟩ 75 ≈↑⟨ cdr ( IsFunctor.identity ( isFunctor F ) )⟩
70 hom a o FMap F (id1 A (obj a)) 76 hom a o FMap F (id1 A (obj a))
71 ∎ 77 ∎
72 78
73 isCommaCategory : IsCategory CommaObj CommaHom _⋍_ _∙_ CommaId 79 isCommaCategory : IsCategory CommaObj CommaHom _⋍_ _∙_ CommaId
74 isCommaCategory = record { 80 isCommaCategory = record {
75 isEquivalence = let open ≈-Reasoning (A) in record {refl = refl-hom ; 81 isEquivalence = record { refl = record { eqa = let open ≈-Reasoning (A) in refl-hom ; eqb = let open ≈-Reasoning (B) in refl-hom } ;
76 sym = sym ; 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 ) } ;
77 trans = trans-hom } 83 trans = λ {f} {g} {h} f=g g=h → record {
78 ; identityL = λ{a b f} → identityL {a} {b} {f} 84 eqa = let open ≈-Reasoning (A) in trans-hom (eqa f=g) (eqa g=h)
79 ; identityR = λ{a b f} → let open ≈-Reasoning A in idR 85 ; eqb = let open ≈-Reasoning (B) in trans-hom (eqb f=g) (eqb g=h)
80 ; o-resp-≈ = IsCategory.o-resp-≈ ( Category.isCategory A ) 86 } }
81 ; associative = IsCategory.associative (Category.isCategory A) 87 ; identityL = λ{a b f} → record {
82 } where 88 eqa = let open ≈-Reasoning (A) in idL {obj a} {obj b} {arrow f}
83 identityL : {a : CommaObj} {b : CommaObj} {f : CommaHom a b} → (CommaId ∙ f) ⋍ f 89 ; eqb = let open ≈-Reasoning (B) in idL {objb a} {objb b} {arrowg f}
84 identityL {a} {b} {f} = let open ≈-Reasoning A in begin 90 }
85 arrow (CommaId ∙ f) 91 ; identityR = λ{a b f} → record {
86 ≈⟨⟩ 92 eqa = let open ≈-Reasoning (A) in idR {obj a} {obj b} {arrow f}
87 arrow (CommaId {b} ) o arrow f 93 ; eqb = let open ≈-Reasoning (B) in idR {objb a} {objb b} {arrowg f}
88 ≈⟨⟩ 94 }
89 id1 A (obj b) o arrow f 95 ; o-resp-≈ = λ {a b c } {f g } {h i } f=g h=i → record {
90 ≈⟨ idL ⟩ 96 eqa = IsCategory.o-resp-≈ (Category.isCategory A) (eqa f=g) (eqa h=i )
91 arrow f 97 ; eqb = IsCategory.o-resp-≈ (Category.isCategory B) (eqb f=g) (eqb h=i )
92 ∎ 98 }
99 ; associative = λ {a b c d} {f} {g} {h} → record {
100 eqa = IsCategory.associative (Category.isCategory A)
101 ; eqb = IsCategory.associative (Category.isCategory B)
102 }
103 }
93 104
94 _↓_ : Category (c₂' ⊔ c₁) (ℓ' ⊔ c₂) ℓ 105 _↓_ : Category (c₂' ⊔ c₁) (ℓ' ⊔ c₂) ℓ
95 _↓_ = record { Obj = CommaObj 106 _↓_ = record { Obj = CommaObj
96 ; Hom = CommaHom 107 ; Hom = CommaHom
97 ; _o_ = _∙_ 108 ; _o_ = _∙_