|
477
|
1 open import Level
|
|
|
2 open import Category
|
|
|
3 module Comma {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') ( F G : Functor A B ) where
|
|
|
4
|
|
|
5 open import HomReasoning
|
|
|
6 open import cat-utility
|
|
|
7
|
|
|
8
|
|
|
9 -- this a special case A = A, B = A, C = B
|
|
|
10
|
|
|
11 open Functor
|
|
|
12
|
|
|
13 record CommaObj : Set ( c₁ ⊔ c₂' ) where
|
|
|
14 field
|
|
|
15 obj : Obj A
|
|
|
16 hom : Hom B ( FObj F obj ) ( FObj G obj )
|
|
|
17
|
|
|
18 open CommaObj
|
|
|
19
|
|
|
20 record CommaHom ( a b : CommaObj ) : Set ( c₂ ⊔ ℓ' ) where
|
|
|
21 field
|
|
|
22 arrow : Hom A ( obj a ) ( obj b )
|
|
|
23 comm : B [ B [ FMap G arrow o hom a ] ≈ B [ hom b o FMap F arrow ] ]
|
|
|
24
|
|
|
25 open CommaHom
|
|
|
26
|
|
|
27 _⋍_ : { a b : CommaObj } ( f g : CommaHom a b ) → Set ℓ
|
|
|
28 _⋍_ f g = A [ arrow f ≈ arrow g ]
|
|
|
29
|
|
|
30 _∙_ : {a b c : CommaObj } → CommaHom b c → CommaHom a b → CommaHom a c
|
|
|
31 _∙_ {a} {b} {c} f g = record {
|
|
|
32 arrow = A [ arrow f o arrow g ] ;
|
|
|
33 comm = comm1
|
|
|
34 } where
|
|
|
35 comm1 : B [ B [ FMap G (A [ arrow f o arrow g ] ) o hom a ] ≈ B [ hom c o FMap F (A [ arrow f o arrow g ]) ] ]
|
|
|
36 comm1 = {!!}
|
|
|
37
|
|
|
38 CommaId : { a : CommaObj } → CommaHom a a
|
|
|
39 CommaId {a} = record { arrow = id1 A ( obj a ) ;
|
|
|
40 comm = comm2 } where
|
|
|
41 comm2 : B [ B [ FMap G (id1 A (obj a)) o hom a ] ≈ B [ hom a o FMap F (id1 A (obj a)) ] ]
|
|
|
42 comm2 = {!!}
|
|
|
43
|
|
|
44 open import Relation.Binary.Core
|
|
|
45
|
|
|
46 isCommaCategory : IsCategory CommaObj CommaHom _⋍_ _∙_ CommaId
|
|
|
47 isCommaCategory = record {
|
|
|
48 isEquivalence = let open ≈-Reasoning (A) in record {refl = refl-hom ;
|
|
|
49 sym = sym ;
|
|
|
50 trans = trans-hom }
|
|
|
51 ; identityL = {!!}
|
|
|
52 ; identityR = {!!}
|
|
|
53 ; o-resp-≈ = λ{a b c f g h i } → o-resp-≈1 {a} {b} {c} {f} {g} {h} {i}
|
|
|
54 ; associative = {!!}
|
|
|
55 } where
|
|
|
56 o-resp-≈1 : {!!}
|
|
|
57 o-resp-≈1 = {!!}
|
|
|
58
|
|
|
59
|
|
|
60 _↑_ : Category {!!} {!!} ℓ
|
|
|
61 _↑_ = {!!}
|
|
|
62
|
