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
404
+ − 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
403
+ − 36
404
+ − 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
403
+ − 40
404
+ − 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
403
+ − 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 {
404
+ − 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} )