Mercurial > hg > Members > kono > Proof > category

comparison maybeCat.agda @ 404:07bea66e5ceb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 20 Mar 2016 12:32:13 +0900
parents 375edfefbf6a
children 33958fdfc77e
comparison
equal deleted inserted replaced
403:375edfefbf6a 404:07bea66e5ceb
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 ≡≡-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) 34 ≡≡-refl {_} {_} {_} {A} {_} {_} {just x} = just refl-hom where open ≈-Reasoning (A)
35 *refl {_} {_} {_} {A} {_} {_} {nothing} = nothing 35 ≡≡-refl {_} {_} {_} {A} {_} {_} {nothing} = nothing
36 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 ] 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) 38 ≡≡-sym {_} {_} {_} {A} (just x≈y) = just (sym x≈y) where open ≈-Reasoning (A)
39 *sym {_} {_} {_} {A} nothing = nothing 39 ≡≡-sym {_} {_} {_} {A} nothing = nothing
40 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 ] 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) 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 43 ≡≡-trans {_} {_} {_} {A} nothing nothing = nothing
44 44
45 45
46 46
47 MaybeCat : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) -> Category c₁ (ℓ ⊔ c₂) (ℓ ⊔ c₂) 47 MaybeCat : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) -> Category c₁ (ℓ ⊔ c₂) (ℓ ⊔ c₂)
48 MaybeCat { c₁} {c₂} {ℓ} ( A ) = record { 48 MaybeCat { c₁} {c₂} {ℓ} ( A ) = record {
50 Hom = λ a b → MaybeHom A a b ; 50 Hom = λ a b → MaybeHom A a b ;
51 _o_ = _+_ ; 51 _o_ = _+_ ;
52 _≈_ = λ a b → _[_≡≡_] { c₁} {c₂} {ℓ} A (hom a) (hom b) ; 52 _≈_ = λ a b → _[_≡≡_] { c₁} {c₂} {ℓ} A (hom a) (hom b) ;
53 Id = \{a} -> MaybeHomId a ; 53 Id = \{a} -> MaybeHomId a ;
54 isCategory = record { 54 isCategory = record {
55 isEquivalence = record {refl = *refl {_} {_} {_} {A}; trans = *trans {_} {_} {_} {A}; sym = *sym {_} {_} {_} {A}}; 55 isEquivalence = record {refl = ≡≡-refl {_} {_} {_} {A}; trans = ≡≡-trans {_} {_} {_} {A}; sym = ≡≡-sym {_} {_} {_} {A}};
56 identityL = \{a b f} -> identityL {a} {b} {f} ; 56 identityL = \{a b f} -> identityL {a} {b} {f} ;
57 identityR = \{a b f} -> identityR {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} ; 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 } 59 associative = \{a b c d f g h } -> associative {a } { b } { c } { d } { f } { g } { h }
60 } 60 }