|
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
|
|
|
33 *refl : { c₁ c₂ ℓ : Level} -> { A : Category c₁ c₂ ℓ } -> {a b : Obj A } -> {x : Maybe ( Hom A a b ) } → A [ x ≡≡ x ]
|
|
|
34 *refl {_} {_} {_} {A} {_} {_} {just x} = just refl-hom where open ≈-Reasoning (A)
|
|
|
35 *refl {_} {_} {_} {A} {_} {_} {nothing} = nothing
|
|
|
36
|
|
|
37 *sym : { c₁ c₂ ℓ : Level} -> { A : Category c₁ c₂ ℓ } -> {a b : Obj A } -> {x y : Maybe ( Hom A a b ) } → A [ x ≡≡ y ] → A [ y ≡≡ x ]
|
|
|
38 *sym {_} {_} {_} {A} (just x≈y) = just (sym x≈y) where open ≈-Reasoning (A)
|
|
|
39 *sym {_} {_} {_} {A} nothing = nothing
|
|
|
40
|
|
|
41 *trans : { c₁ c₂ ℓ : Level} -> { A : Category c₁ c₂ ℓ } -> {a b : Obj A } -> {x y z : Maybe ( Hom A a b ) } → A [ x ≡≡ y ] → A [ y ≡≡ z ] → A [ x ≡≡ z ]
|
|
|
42 *trans {_} {_} {_} {A} (just x≈y) (just y≈z) = just (trans-hom x≈y y≈z) where open ≈-Reasoning (A)
|
|
|
43 *trans {_} {_} {_} {A} nothing nothing = nothing
|
|
|
44
|
|
398
|
45
|
|
|
46
|
|
402
|
47 MaybeCat : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) -> Category c₁ (ℓ ⊔ c₂) (ℓ ⊔ c₂)
|
|
|
48 MaybeCat { c₁} {c₂} {ℓ} ( A ) = record {
|
|
398
|
49 Obj = Obj A ;
|
|
|
50 Hom = λ a b → MaybeHom A a b ;
|
|
403
|
51 _o_ = _+_ ;
|
|
|
52 _≈_ = λ a b → _[_≡≡_] { c₁} {c₂} {ℓ} A (hom a) (hom b) ;
|
|
398
|
53 Id = \{a} -> MaybeHomId a ;
|
|
|
54 isCategory = record {
|
|
403
|
55 isEquivalence = record {refl = *refl {_} {_} {_} {A}; trans = *trans {_} {_} {_} {A}; sym = *sym {_} {_} {_} {A}};
|
|
399
|
56 identityL = \{a b f} -> identityL {a} {b} {f} ;
|
|
|
57 identityR = \{a b f} -> identityR {a} {b} {f};
|
|
|
58 o-resp-≈ = \{a b c f g h i} -> o-resp-≈ {a} {b} {c} {f} {g} {h} {i} ;
|
|
|
59 associative = \{a b c d f g h } -> associative {a } { b } { c } { d } { f } { g } { h }
|
|
398
|
60 }
|
|
|
61 } where
|
|
|
62 open ≈-Reasoning (A)
|
|
403
|
63 identityL : { a b : Obj A } { f : MaybeHom A a b } -> A [ hom (MaybeHomId b + f) ≡≡ hom f ]
|
|
399
|
64 identityL {a} {b} {f} with hom f
|
|
|
65 identityL {a} {b} {_} | nothing = nothing
|
|
|
66 identityL {a} {b} {_} | just f = just ( IsCategory.identityL ( Category.isCategory A ) {a} {b} {f} )
|
|
|
67
|
|
403
|
68 identityR : { a b : Obj A } { f : MaybeHom A a b } -> A [ hom (f + MaybeHomId a ) ≡≡ hom f ]
|
|
399
|
69 identityR {a} {b} {f} with hom f
|
|
|
70 identityR {a} {b} {_} | nothing = nothing
|
|
|
71 identityR {a} {b} {_} | just f = just ( IsCategory.identityR ( Category.isCategory A ) {a} {b} {f} )
|
|
|
72
|
|
402
|
73 o-resp-≈ : {a b c : Obj A} → {f g : MaybeHom A a b } → {h i : MaybeHom A b c } →
|
|
403
|
74 A [ hom f ≡≡ hom g ] → A [ hom h ≡≡ hom i ] → A [ hom (h + f) ≡≡ hom (i + g) ]
|
|
399
|
75 o-resp-≈ {a} {b} {c} {f} {g} {h} {i} eq-fg eq-hi with hom f | hom g | hom h | hom i
|
|
|
76 o-resp-≈ {a} {b} {c} {_} {_} {_} {_} (just eq-fg) (just eq-hi) | just f | just g | just h | just i =
|
|
|
77 just ( IsCategory.o-resp-≈ ( Category.isCategory A ) {a} {b} {c} {f} {g} {h} {i} eq-fg eq-hi )
|
|
|
78 o-resp-≈ {a} {b} {c} {f} {g} {h} {i} (just _) nothing | just _ | just _ | nothing | nothing = nothing
|
|
|
79 o-resp-≈ {a} {b} {c} {f} {g} {h} {i} nothing (just _) | nothing | nothing | just _ | just _ = nothing
|
|
|
80 o-resp-≈ {a} {b} {c} {f} {g} {h} {i} nothing nothing | nothing | nothing | nothing | nothing = nothing
|
|
|
81
|
|
|
82
|
|
402
|
83 associative : {a b c d : Obj A} → {f : MaybeHom A c d } → {g : MaybeHom A b c } → {h : MaybeHom A a b } →
|
|
403
|
84 A [ hom (f + (g + h)) ≡≡ hom ((f + g) + h) ]
|
|
399
|
85 associative {_} {_} {_} {_} {f} {g} {h} with hom f | hom g | hom h
|
|
|
86 associative {_} {_} {_} {_} {f} {g} {h} | nothing | _ | _ = nothing
|
|
|
87 associative {_} {_} {_} {_} {f} {g} {h} | just _ | nothing | _ = nothing
|
|
|
88 associative {_} {_} {_} {_} {f} {g} {h} | just _ | just _ | nothing = nothing
|
|
|
89 associative {a} {b} {c} {d} {_} {_} {_} | just f | just g | just h =
|
|
|
90 just ( IsCategory.associative ( Category.isCategory A ) {a} {b} {c} {d} {f} {g} {h} )
|
