Mercurial > hg > Members > kono > Proof > category
annotate maybeCat.agda @ 790:1e7319868d77
Sets is CCC
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 19 Apr 2019 23:42:19 +0900 |
| parents | a15f52456c78 |
| children |
| rev | line source |
|---|---|
| 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 | |
|
423
b5519e954b57
TwoCat / indexFunctor all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
411
diff
changeset
|
9 open import Relation.Binary.Core |
| 398 | 10 open import Data.Maybe |
| 11 | |
| 12 open Functor | |
| 13 | |
| 14 | |
| 15 record MaybeHom { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a : Obj A ) (b : Obj A ) : Set (ℓ ⊔ c₂) where | |
| 16 field | |
| 17 hom : Maybe ( Hom A a b ) | |
| 18 | |
| 19 open MaybeHom | |
| 20 | |
| 431 | 21 _+_ : { c₁ c₂ ℓ : Level} → { A : Category c₁ c₂ ℓ } → {a b c : Obj A } → MaybeHom A b c → MaybeHom A a b → MaybeHom A a c |
| 403 | 22 _+_ {x} {y} {z} {A} {a} {b} {c} f g with hom f | hom g |
| 23 _+_ {_} {_} {_} {A} {a} {b} {c} f g | nothing | _ = record { hom = nothing } | |
| 24 _+_ {_} {_} {_} {A} {a} {b} {c} f g | _ | nothing = record { hom = nothing } | |
| 25 _+_ {_} {_} {_} {A} {a} {b} {c} _ _ | (just f) | (just g) = record { hom = just ( A [ f o g ] ) } | |
| 398 | 26 |
| 431 | 27 MaybeHomId : { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } (a : Obj A ) → MaybeHom A a a |
| 402 | 28 MaybeHomId {_} {_} {_} {A} a = record { hom = just ( id1 A a) } |
| 398 | 29 |
| 431 | 30 _[_≡≡_] : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b : Obj A } → Rel (Maybe (Hom A a b)) (c₂ ⊔ ℓ) |
| 403 | 31 _[_≡≡_] A = Eq ( Category._≈_ A ) |
| 32 | |
| 33 | |
| 411 | 34 module ≡≡-Reasoning { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) where |
| 35 | |
| 36 infixr 2 _∎ | |
| 37 infixr 2 _≡≡⟨_⟩_ _≡≡⟨⟩_ | |
| 38 infix 1 begin_ | |
| 39 | |
| 431 | 40 ≡≡-refl : {a b : Obj A } → {x : Maybe ( Hom A a b ) } → A [ x ≡≡ x ] |
| 411 | 41 ≡≡-refl {_} {_} {just x} = just refl-hom where open ≈-Reasoning (A) |
| 42 ≡≡-refl {_} {_} {nothing} = nothing | |
| 43 | |
| 431 | 44 ≡≡-sym : {a b : Obj A } → {x y : Maybe ( Hom A a b ) } → A [ x ≡≡ y ] → A [ y ≡≡ x ] |
| 411 | 45 ≡≡-sym (just x≈y) = just (sym x≈y) where open ≈-Reasoning (A) |
| 46 ≡≡-sym nothing = nothing | |
| 47 | |
| 431 | 48 ≡≡-trans : {a b : Obj A } → {x y z : Maybe ( Hom A a b ) } → A [ x ≡≡ y ] → A [ y ≡≡ z ] → A [ x ≡≡ z ] |
| 411 | 49 ≡≡-trans (just x≈y) (just y≈z) = just (trans-hom x≈y y≈z) where open ≈-Reasoning (A) |
| 50 ≡≡-trans nothing nothing = nothing | |
| 51 | |
| 431 | 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 ] | |
|
423
b5519e954b57
TwoCat / indexFunctor all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
411
diff
changeset
|
54 ≡≡-cong {a} {b } {c} {d} {nothing} {nothing} f refl = ≡≡-refl |
|
b5519e954b57
TwoCat / indexFunctor all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
411
diff
changeset
|
55 ≡≡-cong {a} {b } {c} {d} {just x} {just .x} f refl = ≡≡-refl |
| 403 | 56 |
| 411 | 57 data _IsRelatedTo_ {a b : Obj A} (x y : (Maybe (Hom A a b ))) : |
| 58 Set (ℓ ⊔ c₂) where | |
| 59 relTo : (x≈y : A [ x ≡≡ y ] ) → x IsRelatedTo y | |
| 60 | |
| 61 begin_ : {a b : Obj A} {x : Maybe (Hom A a b ) } {y : Maybe (Hom A a b )} → | |
| 62 x IsRelatedTo y → A [ x ≡≡ y ] | |
| 63 begin relTo x≈y = x≈y | |
| 403 | 64 |
| 411 | 65 _≡≡⟨_⟩_ : {a b : Obj A} (x : Maybe (Hom A a b )) {y z : Maybe (Hom A a b ) } → |
| 66 A [ x ≡≡ y ] → y IsRelatedTo z → x IsRelatedTo z | |
| 67 _ ≡≡⟨ x≈y ⟩ relTo y≈z = relTo (≡≡-trans x≈y y≈z) | |
| 403 | 68 |
| 411 | 69 _≡≡⟨⟩_ : {a b : Obj A} (x : Maybe (Hom A a b )) {y : Maybe (Hom A a b )} |
| 70 → x IsRelatedTo y → x IsRelatedTo y | |
| 71 _ ≡≡⟨⟩ x≈y = x≈y | |
| 72 | |
| 73 _∎ : {a b : Obj A} (x : Maybe (Hom A a b )) → x IsRelatedTo x | |
| 74 _∎ _ = relTo ≡≡-refl | |
| 398 | 75 |
| 76 | |
| 426 | 77 |
| 78 | |
| 431 | 79 MaybeCat : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Category c₁ (ℓ ⊔ c₂) (ℓ ⊔ c₂) |
| 402 | 80 MaybeCat { c₁} {c₂} {ℓ} ( A ) = record { |
| 398 | 81 Obj = Obj A ; |
| 82 Hom = λ a b → MaybeHom A a b ; | |
| 403 | 83 _o_ = _+_ ; |
| 84 _≈_ = λ a b → _[_≡≡_] { c₁} {c₂} {ℓ} A (hom a) (hom b) ; | |
| 431 | 85 Id = λ {a} → MaybeHomId a ; |
| 398 | 86 isCategory = record { |
| 411 | 87 isEquivalence = let open ≡≡-Reasoning (A) in record {refl = ≡≡-refl ; trans = ≡≡-trans ; sym = ≡≡-sym } ; |
| 431 | 88 identityL = λ {a b f} → identityL {a} {b} {f} ; |
| 89 identityR = λ {a b f} → identityR {a} {b} {f}; | |
| 90 o-resp-≈ = λ {a b c f g h i} → o-resp-≈ {a} {b} {c} {f} {g} {h} {i} ; | |
| 91 associative = λ {a b c d f g h } → associative {a } { b } { c } { d } { f } { g } { h } | |
| 398 | 92 } |
| 93 } where | |
| 431 | 94 identityL : { a b : Obj A } { f : MaybeHom A a b } → A [ hom (MaybeHomId b + f) ≡≡ hom f ] |
| 399 | 95 identityL {a} {b} {f} with hom f |
| 96 identityL {a} {b} {_} | nothing = nothing | |
| 97 identityL {a} {b} {_} | just f = just ( IsCategory.identityL ( Category.isCategory A ) {a} {b} {f} ) | |
| 98 | |
| 431 | 99 identityR : { a b : Obj A } { f : MaybeHom A a b } → A [ hom (f + MaybeHomId a ) ≡≡ hom f ] |
| 399 | 100 identityR {a} {b} {f} with hom f |
| 101 identityR {a} {b} {_} | nothing = nothing | |
| 102 identityR {a} {b} {_} | just f = just ( IsCategory.identityR ( Category.isCategory A ) {a} {b} {f} ) | |
| 103 | |
| 402 | 104 o-resp-≈ : {a b c : Obj A} → {f g : MaybeHom A a b } → {h i : MaybeHom A b c } → |
| 403 | 105 A [ hom f ≡≡ hom g ] → A [ hom h ≡≡ hom i ] → A [ hom (h + f) ≡≡ hom (i + g) ] |
| 399 | 106 o-resp-≈ {a} {b} {c} {f} {g} {h} {i} eq-fg eq-hi with hom f | hom g | hom h | hom i |
| 107 o-resp-≈ {a} {b} {c} {_} {_} {_} {_} (just eq-fg) (just eq-hi) | just f | just g | just h | just i = | |
| 108 just ( IsCategory.o-resp-≈ ( Category.isCategory A ) {a} {b} {c} {f} {g} {h} {i} eq-fg eq-hi ) | |
| 109 o-resp-≈ {a} {b} {c} {f} {g} {h} {i} (just _) nothing | just _ | just _ | nothing | nothing = nothing | |
| 110 o-resp-≈ {a} {b} {c} {f} {g} {h} {i} nothing (just _) | nothing | nothing | just _ | just _ = nothing | |
| 111 o-resp-≈ {a} {b} {c} {f} {g} {h} {i} nothing nothing | nothing | nothing | nothing | nothing = nothing | |
| 112 | |
| 113 | |
| 402 | 114 associative : {a b c d : Obj A} → {f : MaybeHom A c d } → {g : MaybeHom A b c } → {h : MaybeHom A a b } → |
| 403 | 115 A [ hom (f + (g + h)) ≡≡ hom ((f + g) + h) ] |
| 399 | 116 associative {_} {_} {_} {_} {f} {g} {h} with hom f | hom g | hom h |
| 117 associative {_} {_} {_} {_} {f} {g} {h} | nothing | _ | _ = nothing | |
| 118 associative {_} {_} {_} {_} {f} {g} {h} | just _ | nothing | _ = nothing | |
| 119 associative {_} {_} {_} {_} {f} {g} {h} | just _ | just _ | nothing = nothing | |
| 120 associative {a} {b} {c} {d} {_} {_} {_} | just f | just g | just h = | |
| 121 just ( IsCategory.associative ( Category.isCategory A ) {a} {b} {c} {d} {f} {g} {h} ) | |
| 426 | 122 |
| 431 | 123 ≈-to-== : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → { a b : Obj A } |
| 124 { f g : Hom A a b } → | |
| 125 A [ f ≈ g ] → (MaybeCat A) [ record { hom = just f } ≈ record { hom = just g } ] | |
| 426 | 126 ≈-to-== A {a} {b} {f} {g} f≈g = just f≈g |