Mercurial > hg > Members > kono > Proof > category

changeset 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 508c88223aab
children f04b2fb91432
files maybeCat.agda
diffstat 1 files changed, 35 insertions(+), 11 deletions(-) [+]
line wrap: on
line diff
--- a/maybeCat.agda	Wed Mar 23 11:16:16 2016 +0900
+++ b/maybeCat.agda	Wed Mar 23 11:29:45 2016 +0900
@@ -30,18 +30,43 @@
 _[_≡≡_]  A =  Eq ( Category._≈_ A ) 
 
 
-≡≡-refl :   { c₁ c₂ ℓ : Level} -> { A : Category c₁ c₂ ℓ } ->  {a b : Obj A } -> {x : Maybe ( Hom A a b ) } → A [ x ≡≡ x ]
-≡≡-refl  {_} {_} {_} {A} {_} {_} {just x}  = just refl-hom where  open ≈-Reasoning (A)
-≡≡-refl  {_} {_} {_} {A} {_} {_} {nothing} = nothing
+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
+
 
-≡≡-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 ]
-≡≡-sym {_} {_} {_} {A} (just x≈y) = just (sym x≈y)  where  open ≈-Reasoning (A)
-≡≡-sym {_} {_} {_} {A} nothing    = nothing
+        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
 
-≡≡-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 ]
-≡≡-trans {_} {_} {_} {A} (just x≈y) (just y≈z) = just (trans-hom x≈y y≈z)  where  open ≈-Reasoning (A)
-≡≡-trans {_} {_} {_} {A} nothing    nothing    = nothing
+        _≡≡⟨_⟩_ :  {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₂)
@@ -52,14 +77,13 @@
     _≈_ = λ a b →    _[_≡≡_] { c₁} {c₂} {ℓ} A  (hom a) (hom b)  ;
     Id  =  \{a} -> MaybeHomId a ;
     isCategory  = record {
-            isEquivalence = record {refl = ≡≡-refl  {_} {_} {_} {A}; trans = ≡≡-trans  {_} {_} {_} {A}; sym = ≡≡-sym  {_} {_} {_} {A}};
+            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
-        open ≈-Reasoning (A) 
         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