Mercurial > hg > Members > kono > Proof > category

comparison maybeCat.agda @ 411:33958fdfc77e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add reasoning
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 23 Mar 2016 11:29:45 +0900
parents 07bea66e5ceb
children b5519e954b57
comparison
equal deleted inserted replaced
410:508c88223aab 411:33958fdfc77e
28 28
29 _[_≡≡_] : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b : Obj A } -> Rel (Maybe (Hom A a b)) (c₂ ⊔ ℓ) 29 _[_≡≡_] : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b : Obj A } -> Rel (Maybe (Hom A a b)) (c₂ ⊔ ℓ)
30 _[_≡≡_] A = Eq ( Category._≈_ A ) 30 _[_≡≡_] A = Eq ( Category._≈_ A )
31 31
32 32
33 ≡≡-refl : { c₁ c₂ ℓ : Level} -> { A : Category c₁ c₂ ℓ } -> {a b : Obj A } -> {x : Maybe ( Hom A a b ) } → A [ x ≡≡ x ] 33 module ≡≡-Reasoning { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) where
34 ≡≡-refl {_} {_} {_} {A} {_} {_} {just x} = just refl-hom where open ≈-Reasoning (A)
35 ≡≡-refl {_} {_} {_} {A} {_} {_} {nothing} = nothing
36 34
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 ] 35 infixr 2 _∎
38 ≡≡-sym {_} {_} {_} {A} (just x≈y) = just (sym x≈y) where open ≈-Reasoning (A) 36 infixr 2 _≡≡⟨_⟩_ _≡≡⟨⟩_
39 ≡≡-sym {_} {_} {_} {A} nothing = nothing 37 infix 1 begin_
40 38
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 ] 39 ≡≡-refl : {a b : Obj A } -> {x : Maybe ( Hom A a b ) } → A [ x ≡≡ x ]
42 ≡≡-trans {_} {_} {_} {A} (just x≈y) (just y≈z) = just (trans-hom x≈y y≈z) where open ≈-Reasoning (A) 40 ≡≡-refl {_} {_} {just x} = just refl-hom where open ≈-Reasoning (A)
43 ≡≡-trans {_} {_} {_} {A} nothing nothing = nothing 41 ≡≡-refl {_} {_} {nothing} = nothing
44 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
51
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
59
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)
63
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
45 70
46 71
47 MaybeCat : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) -> Category c₁ (ℓ ⊔ c₂) (ℓ ⊔ c₂) 72 MaybeCat : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) -> Category c₁ (ℓ ⊔ c₂) (ℓ ⊔ c₂)
48 MaybeCat { c₁} {c₂} {ℓ} ( A ) = record { 73 MaybeCat { c₁} {c₂} {ℓ} ( A ) = record {
49 Obj = Obj A ; 74 Obj = Obj A ;
50 Hom = λ a b → MaybeHom A a b ; 75 Hom = λ a b → MaybeHom A a b ;
51 _o_ = _+_ ; 76 _o_ = _+_ ;
52 _≈_ = λ a b → _[_≡≡_] { c₁} {c₂} {ℓ} A (hom a) (hom b) ; 77 _≈_ = λ a b → _[_≡≡_] { c₁} {c₂} {ℓ} A (hom a) (hom b) ;
53 Id = \{a} -> MaybeHomId a ; 78 Id = \{a} -> MaybeHomId a ;
54 isCategory = record { 79 isCategory = record {
55 isEquivalence = record {refl = ≡≡-refl {_} {_} {_} {A}; trans = ≡≡-trans {_} {_} {_} {A}; sym = ≡≡-sym {_} {_} {_} {A}}; 80 isEquivalence = let open ≡≡-Reasoning (A) in record {refl = ≡≡-refl ; trans = ≡≡-trans ; sym = ≡≡-sym } ;
56 identityL = \{a b f} -> identityL {a} {b} {f} ; 81 identityL = \{a b f} -> identityL {a} {b} {f} ;
57 identityR = \{a b f} -> identityR {a} {b} {f}; 82 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} ; 83 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 } 84 associative = \{a b c d f g h } -> associative {a } { b } { c } { d } { f } { g } { h }
60 } 85 }
61 } where 86 } where
62 open ≈-Reasoning (A)
63 identityL : { a b : Obj A } { f : MaybeHom A a b } -> A [ hom (MaybeHomId b + f) ≡≡ hom f ] 87 identityL : { a b : Obj A } { f : MaybeHom A a b } -> A [ hom (MaybeHomId b + f) ≡≡ hom f ]
64 identityL {a} {b} {f} with hom f 88 identityL {a} {b} {f} with hom f
65 identityL {a} {b} {_} | nothing = nothing 89 identityL {a} {b} {_} | nothing = nothing
66 identityL {a} {b} {_} | just f = just ( IsCategory.identityL ( Category.isCategory A ) {a} {b} {f} ) 90 identityL {a} {b} {_} | just f = just ( IsCategory.identityL ( Category.isCategory A ) {a} {b} {f} )
67 91