Mercurial > hg > Members > kono > Proof > category

comparison maybeCat.agda @ 423:b5519e954b57

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
TwoCat / indexFunctor all done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 24 Mar 2016 13:44:27 +0900
parents 33958fdfc77e
children 1290d6876129
comparison
equal deleted inserted replaced
422:3a4a99a8edbe 423:b5519e954b57
4 module maybeCat where 4 module maybeCat where
5 5
6 open import cat-utility 6 open import cat-utility
7 open import HomReasoning 7 open import HomReasoning
8 open import Relation.Binary 8 open import Relation.Binary
9 open import Relation.Binary.Core
9 open import Data.Maybe 10 open import Data.Maybe
10 11
11 open Functor 12 open Functor
12 13
13 14
46 47
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 : {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 (just x≈y) (just y≈z) = just (trans-hom x≈y y≈z) where open ≈-Reasoning (A)
49 ≡≡-trans nothing nothing = nothing 50 ≡≡-trans nothing nothing = nothing
50 51
52 ≡≡-cong : ∀{ a b c d } -> ∀ {x y : Maybe (Hom A a b )} →
53 (f : Maybe (Hom A a b ) -> Maybe (Hom A c d ) ) -> x ≡ y → A [ f x ≡≡ f y ]
54 ≡≡-cong {a} {b } {c} {d} {nothing} {nothing} f refl = ≡≡-refl
55 ≡≡-cong {a} {b } {c} {d} {just x} {just .x} f refl = ≡≡-refl
51 56
52 data _IsRelatedTo_ {a b : Obj A} (x y : (Maybe (Hom A a b ))) : 57 data _IsRelatedTo_ {a b : Obj A} (x y : (Maybe (Hom A a b ))) :
53 Set (ℓ ⊔ c₂) where 58 Set (ℓ ⊔ c₂) where
54 relTo : (x≈y : A [ x ≡≡ y ] ) → x IsRelatedTo y 59 relTo : (x≈y : A [ x ≡≡ y ] ) → x IsRelatedTo y
55 60