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