|
398
|
1 open import Category -- https://github.com/konn/category-agda
|
|
|
2 open import Level
|
|
|
3
|
|
402
|
4 module maybeCat where
|
|
398
|
5
|
|
|
6 open import cat-utility
|
|
|
7 open import HomReasoning
|
|
|
8 open import Relation.Binary
|
|
|
9 open import Data.Maybe
|
|
|
10
|
|
|
11 open Functor
|
|
|
12
|
|
|
13
|
|
|
14 record MaybeHom { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a : Obj A ) (b : Obj A ) : Set (ℓ ⊔ c₂) where
|
|
|
15 field
|
|
|
16 hom : Maybe ( Hom A a b )
|
|
|
17
|
|
|
18 open MaybeHom
|
|
|
19
|
|
403
|
20 _+_ : { c₁ c₂ ℓ : Level} -> { A : Category c₁ c₂ ℓ } -> {a b c : Obj A } → MaybeHom A b c → MaybeHom A a b → MaybeHom A a c
|
|
|
21 _+_ {x} {y} {z} {A} {a} {b} {c} f g with hom f | hom g
|
|
|
22 _+_ {_} {_} {_} {A} {a} {b} {c} f g | nothing | _ = record { hom = nothing }
|
|
|
23 _+_ {_} {_} {_} {A} {a} {b} {c} f g | _ | nothing = record { hom = nothing }
|
|
|
24 _+_ {_} {_} {_} {A} {a} {b} {c} _ _ | (just f) | (just g) = record { hom = just ( A [ f o g ] ) }
|
|
398
|
25
|
|
402
|
26 MaybeHomId : { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } (a : Obj A ) -> MaybeHom A a a
|
|
|
27 MaybeHomId {_} {_} {_} {A} a = record { hom = just ( id1 A a) }
|
|
398
|
28
|
|
403
|
29 _[_≡≡_] : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b : Obj A } -> Rel (Maybe (Hom A a b)) (c₂ ⊔ ℓ)
|
|
|
30 _[_≡≡_] A = Eq ( Category._≈_ A )
|
|
|
31
|
|
|
32
|
|
411
|
33 module ≡≡-Reasoning { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) where
|
|
|
34
|
|
|
35 infixr 2 _∎
|
|
|
36 infixr 2 _≡≡⟨_⟩_ _≡≡⟨⟩_
|
|
|
37 infix 1 begin_
|
|
|
38
|
|
|
39 ≡≡-refl : {a b : Obj A } -> {x : Maybe ( Hom A a b ) } → A [ x ≡≡ x ]
|
|
|
40 ≡≡-refl {_} {_} {just x} = just refl-hom where open ≈-Reasoning (A)
|
|
|
41 ≡≡-refl {_} {_} {nothing} = nothing
|
|
|
42
|
|
|
43 ≡≡-sym : {a b : Obj A } -> {x y : Maybe ( Hom A a b ) } → A [ x ≡≡ y ] → A [ y ≡≡ x ]
|
|
|
44 ≡≡-sym (just x≈y) = just (sym x≈y) where open ≈-Reasoning (A)
|
|
|
45 ≡≡-sym nothing = nothing
|
|
|
46
|
|
|
47 ≡≡-trans : {a b : Obj A } -> {x y z : Maybe ( Hom A a b ) } → A [ x ≡≡ y ] → A [ y ≡≡ z ] → A [ x ≡≡ z ]
|
|
|
48 ≡≡-trans (just x≈y) (just y≈z) = just (trans-hom x≈y y≈z) where open ≈-Reasoning (A)
|
|
|
49 ≡≡-trans nothing nothing = nothing
|
|
|
50
|
|
403
|
51
|
|
411
|
52 data _IsRelatedTo_ {a b : Obj A} (x y : (Maybe (Hom A a b ))) :
|
|
|
53 Set (ℓ ⊔ c₂) where
|
|
|
54 relTo : (x≈y : A [ x ≡≡ y ] ) → x IsRelatedTo y
|
|
|
55
|
|
|
56 begin_ : {a b : Obj A} {x : Maybe (Hom A a b ) } {y : Maybe (Hom A a b )} →
|
|
|
57 x IsRelatedTo y → A [ x ≡≡ y ]
|
|
|
58 begin relTo x≈y = x≈y
|
|
403
|
59
|
|
411
|
60 _≡≡⟨_⟩_ : {a b : Obj A} (x : Maybe (Hom A a b )) {y z : Maybe (Hom A a b ) } →
|
|
|
61 A [ x ≡≡ y ] → y IsRelatedTo z → x IsRelatedTo z
|
|
|
62 _ ≡≡⟨ x≈y ⟩ relTo y≈z = relTo (≡≡-trans x≈y y≈z)
|
|
403
|
63
|
|
411
|
64 _≡≡⟨⟩_ : {a b : Obj A} (x : Maybe (Hom A a b )) {y : Maybe (Hom A a b )}
|
|
|
65 → x IsRelatedTo y → x IsRelatedTo y
|
|
|
66 _ ≡≡⟨⟩ x≈y = x≈y
|
|
|
67
|
|
|
68 _∎ : {a b : Obj A} (x : Maybe (Hom A a b )) → x IsRelatedTo x
|
|
|
69 _∎ _ = relTo ≡≡-refl
|
|
398
|
70
|
|
|
71
|
|
402
|
72 MaybeCat : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) -> Category c₁ (ℓ ⊔ c₂) (ℓ ⊔ c₂)
|
|
|
73 MaybeCat { c₁} {c₂} {ℓ} ( A ) = record {
|
|
398
|
74 Obj = Obj A ;
|
|
|
75 Hom = λ a b → MaybeHom A a b ;
|
|
403
|
76 _o_ = _+_ ;
|
|
|
77 _≈_ = λ a b → _[_≡≡_] { c₁} {c₂} {ℓ} A (hom a) (hom b) ;
|
|
398
|
78 Id = \{a} -> MaybeHomId a ;
|
|
|
79 isCategory = record {
|
|
411
|
80 isEquivalence = let open ≡≡-Reasoning (A) in record {refl = ≡≡-refl ; trans = ≡≡-trans ; sym = ≡≡-sym } ;
|
|
399
|
81 identityL = \{a b f} -> identityL {a} {b} {f} ;
|
|
|
82 identityR = \{a b f} -> identityR {a} {b} {f};
|
|
|
83 o-resp-≈ = \{a b c f g h i} -> o-resp-≈ {a} {b} {c} {f} {g} {h} {i} ;
|
|
|
84 associative = \{a b c d f g h } -> associative {a } { b } { c } { d } { f } { g } { h }
|
|
398
|
85 }
|
|
|
86 } where
|
|
403
|
87 identityL : { a b : Obj A } { f : MaybeHom A a b } -> A [ hom (MaybeHomId b + f) ≡≡ hom f ]
|
|
399
|
88 identityL {a} {b} {f} with hom f
|
|
|
89 identityL {a} {b} {_} | nothing = nothing
|
|
|
90 identityL {a} {b} {_} | just f = just ( IsCategory.identityL ( Category.isCategory A ) {a} {b} {f} )
|
|
|
91
|
|
403
|
92 identityR : { a b : Obj A } { f : MaybeHom A a b } -> A [ hom (f + MaybeHomId a ) ≡≡ hom f ]
|
|
399
|
93 identityR {a} {b} {f} with hom f
|
|
|
94 identityR {a} {b} {_} | nothing = nothing
|
|
|
95 identityR {a} {b} {_} | just f = just ( IsCategory.identityR ( Category.isCategory A ) {a} {b} {f} )
|
|
|
96
|
|
402
|
97 o-resp-≈ : {a b c : Obj A} → {f g : MaybeHom A a b } → {h i : MaybeHom A b c } →
|
|
403
|
98 A [ hom f ≡≡ hom g ] → A [ hom h ≡≡ hom i ] → A [ hom (h + f) ≡≡ hom (i + g) ]
|
|
399
|
99 o-resp-≈ {a} {b} {c} {f} {g} {h} {i} eq-fg eq-hi with hom f | hom g | hom h | hom i
|
|
|
100 o-resp-≈ {a} {b} {c} {_} {_} {_} {_} (just eq-fg) (just eq-hi) | just f | just g | just h | just i =
|
|
|
101 just ( IsCategory.o-resp-≈ ( Category.isCategory A ) {a} {b} {c} {f} {g} {h} {i} eq-fg eq-hi )
|
|
|
102 o-resp-≈ {a} {b} {c} {f} {g} {h} {i} (just _) nothing | just _ | just _ | nothing | nothing = nothing
|
|
|
103 o-resp-≈ {a} {b} {c} {f} {g} {h} {i} nothing (just _) | nothing | nothing | just _ | just _ = nothing
|
|
|
104 o-resp-≈ {a} {b} {c} {f} {g} {h} {i} nothing nothing | nothing | nothing | nothing | nothing = nothing
|
|
|
105
|
|
|
106
|
|
402
|
107 associative : {a b c d : Obj A} → {f : MaybeHom A c d } → {g : MaybeHom A b c } → {h : MaybeHom A a b } →
|
|
403
|
108 A [ hom (f + (g + h)) ≡≡ hom ((f + g) + h) ]
|
|
399
|
109 associative {_} {_} {_} {_} {f} {g} {h} with hom f | hom g | hom h
|
|
|
110 associative {_} {_} {_} {_} {f} {g} {h} | nothing | _ | _ = nothing
|
|
|
111 associative {_} {_} {_} {_} {f} {g} {h} | just _ | nothing | _ = nothing
|
|
|
112 associative {_} {_} {_} {_} {f} {g} {h} | just _ | just _ | nothing = nothing
|
|
|
113 associative {a} {b} {c} {d} {_} {_} {_} | just f | just g | just h =
|
|
|
114 just ( IsCategory.associative ( Category.isCategory A ) {a} {b} {c} {d} {f} {g} {h} )
|
