### view maybeCat.agda @ 790:1e7319868d77

Sets is CCC
author Shinji KONO Fri, 19 Apr 2019 23:42:19 +0900 a15f52456c78
line wrap: on
line source
```
open import Category -- https://github.com/konn/category-agda
open import Level

module maybeCat where

open import cat-utility
open import HomReasoning
open import Relation.Binary
open import Relation.Binary.Core
open import Data.Maybe

open Functor

record MaybeHom { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  (a : Obj A ) (b : Obj A ) : Set  (ℓ ⊔ c₂)   where
field
hom : Maybe ( Hom A a b )

open MaybeHom

_+_ :  { c₁ c₂ ℓ : Level} → { A : Category c₁ c₂ ℓ } →  {a b c : Obj A } → MaybeHom A b c  →  MaybeHom A a b  →  MaybeHom A  a c
_+_  {x} {y} {z} {A} {a} {b} {c} f g with hom f | hom g
_+_  {_} {_} {_} {A} {a} {b} {c} f g | nothing  | _  = record { hom =  nothing }
_+_  {_} {_} {_} {A} {a} {b} {c} f g | _ | nothing   = record { hom =  nothing }
_+_  {_} {_} {_} {A} {a} {b} {c} _ _ | (just f) |  (just g)  = record { hom =  just ( A [ f o  g ]  ) }

MaybeHomId  : { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } (a  : Obj A ) → MaybeHom A a a
MaybeHomId   {_} {_} {_} {A} a  = record { hom = just ( id1 A a)  }

_[_≡≡_] : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {a b : Obj A } →  Rel (Maybe (Hom A a b)) (c₂ ⊔ ℓ)
_[_≡≡_]  A =  Eq ( Category._≈_ A )

module ≡≡-Reasoning { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  where

infixr  2 _∎
infixr 2 _≡≡⟨_⟩_ _≡≡⟨⟩_
infix  1 begin_

≡≡-refl :   {a b : Obj A } → {x : Maybe ( Hom A a b ) } → A [ x ≡≡ x ]
≡≡-refl  {_} {_} {just x}  = just refl-hom where  open ≈-Reasoning (A)
≡≡-refl  {_} {_} {nothing} = nothing

≡≡-sym :  {a b : Obj A } → {x y : Maybe ( Hom A a b ) }  → A [ x ≡≡ y ] → A [ y ≡≡ x ]
≡≡-sym (just x≈y) = just (sym x≈y)  where  open ≈-Reasoning (A)
≡≡-sym nothing    = nothing

≡≡-trans :  {a b : Obj A } → {x y z : Maybe ( Hom A a b ) }  → A [ x ≡≡ y ] → A [ y ≡≡ z ] → A [ x ≡≡ z ]
≡≡-trans (just x≈y) (just y≈z) = just (trans-hom x≈y y≈z)  where  open ≈-Reasoning (A)
≡≡-trans nothing    nothing    = nothing

≡≡-cong :  ∀{ a b c d }   → ∀ {x y :  Maybe (Hom A a b )} →
(f : Maybe (Hom A a b ) → Maybe (Hom A c d ) )  →  x  ≡  y  →  A [ f x ≡≡ f y ]
≡≡-cong  {a} {b } {c} {d} {nothing} {nothing} f refl  = ≡≡-refl
≡≡-cong  {a} {b } {c} {d} {just x} {just .x} f refl  = ≡≡-refl

data _IsRelatedTo_  {a b : Obj A}  (x y : (Maybe (Hom A a b ))) :
Set  (ℓ ⊔ c₂)  where
relTo : (x≈y : A [ x  ≡≡ y  ] ) → x IsRelatedTo y

begin_ :  {a b : Obj A}  {x : Maybe (Hom A a b ) } {y : Maybe (Hom A a b )} →
x IsRelatedTo y →  A [ x ≡≡  y ]
begin relTo x≈y = x≈y

_≡≡⟨_⟩_ :  {a b : Obj A}  (x :  Maybe  (Hom A a b )) {y z :  Maybe (Hom A a b ) } →
A [ x ≡≡ y ]  → y IsRelatedTo z → x IsRelatedTo z
_ ≡≡⟨ x≈y ⟩ relTo y≈z = relTo (≡≡-trans x≈y y≈z)

_≡≡⟨⟩_ :  {a b : Obj A}  (x : Maybe  (Hom A a b )) {y : Maybe (Hom A a b )}
→ x IsRelatedTo y → x IsRelatedTo y
_ ≡≡⟨⟩ x≈y = x≈y

_∎ :   {a b : Obj A}  (x :  Maybe (Hom A a b )) → x IsRelatedTo x
_∎ _ = relTo ≡≡-refl

MaybeCat : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Category   c₁ (ℓ ⊔ c₂)  (ℓ ⊔ c₂)
MaybeCat { c₁} {c₂} {ℓ} ( A ) =   record {
Obj  = Obj A  ;
Hom = λ a b →   MaybeHom A  a b   ;
_o_ =  _+_   ;
_≈_ = λ a b →    _[_≡≡_] { c₁} {c₂} {ℓ} A  (hom a) (hom b)  ;
Id  =  λ {a} → MaybeHomId a ;
isCategory  = record {
isEquivalence = let open ≡≡-Reasoning (A) in record {refl = ≡≡-refl ; trans = ≡≡-trans ; sym = ≡≡-sym  } ;
identityL  = λ {a b f} → identityL {a} {b} {f} ;
identityR  = λ {a b f} → identityR {a} {b} {f};
o-resp-≈  = λ {a b c f g h i} →  o-resp-≈ {a} {b} {c} {f} {g} {h} {i} ;
associative  = λ {a b c d f g h } → associative {a } { b } { c } { d } { f } { g } { h }
}
} where
identityL : { a b : Obj A } { f : MaybeHom A a b } →  A [ hom (MaybeHomId b + f) ≡≡ hom f ]
identityL {a} {b} {f}  with hom f
identityL {a} {b} {_} | nothing  = nothing
identityL {a} {b} {_} | just f = just ( IsCategory.identityL ( Category.isCategory A )  {a} {b} {f}  )

identityR : { a b : Obj A } { f : MaybeHom A a b } →  A [ hom (f + MaybeHomId a  ) ≡≡ hom f ]
identityR {a} {b} {f}  with hom f
identityR {a} {b} {_} | nothing  = nothing
identityR {a} {b} {_} | just f = just ( IsCategory.identityR ( Category.isCategory A )  {a} {b} {f}  )

o-resp-≈  :  {a b c : Obj A} → {f g : MaybeHom A a b } → {h i : MaybeHom A  b c } →
A [ hom f ≡≡ hom g ] → A [ hom h ≡≡ hom i ] → A [ hom (h + f) ≡≡ hom (i + g) ]
o-resp-≈  {a} {b} {c} {f} {g} {h} {i} eq-fg eq-hi with hom f | hom g  | hom h | hom i
o-resp-≈  {a} {b} {c} {_} {_} {_} {_}  (just eq-fg)  (just eq-hi) | just f | just g | just h | just i =
just ( IsCategory.o-resp-≈ ( Category.isCategory A )  {a} {b} {c} {f} {g} {h} {i} eq-fg eq-hi )
o-resp-≈  {a} {b} {c} {f} {g} {h} {i} (just _)  nothing | just _ | just _ | nothing | nothing = nothing
o-resp-≈  {a} {b} {c} {f} {g} {h} {i} nothing  (just _) | nothing | nothing | just _ | just _ = nothing
o-resp-≈  {a} {b} {c} {f} {g} {h} {i} nothing nothing | nothing | nothing | nothing | nothing = nothing

associative  :  {a b c d : Obj A} → {f : MaybeHom A c d } → {g : MaybeHom A b c } → {h : MaybeHom A a b } →
A [ hom (f + (g + h)) ≡≡ hom ((f + g) + h) ]
associative  {_} {_} {_} {_} {f} {g} {h}  with hom f | hom g | hom h
associative  {_} {_} {_} {_} {f} {g} {h}  | nothing | _ | _ = nothing
associative  {_} {_} {_} {_} {f} {g} {h}  | just _ | nothing | _ = nothing
associative  {_} {_} {_} {_} {f} {g} {h}  | just _ | just _ | nothing = nothing
associative  {a} {b} {c} {d} {_} {_} {_}  | just f | just g | just h =
just ( IsCategory.associative ( Category.isCategory A )  {a} {b} {c} {d} {f} {g} {h}  )

≈-to-== : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) →  { a b :  Obj A }
{ f g : Hom A a b } →
A [ f ≈ g ] → (MaybeCat A) [  record { hom = just f } ≈  record { hom = just g } ]
≈-to-==  A {a} {b} {f} {g} f≈g =  just f≈g
```