Mercurial > hg > Members > kono > Proof > category

changeset 399:8304007dc2f8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
maybe category done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 17 Mar 2016 08:07:38 +0900
parents 64aa49a18469
children 89785764bccb
files maybeCat.agda
diffstat 1 files changed, 33 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/maybeCat.agda	Wed Mar 16 17:43:31 2016 +0900
+++ b/maybeCat.agda	Thu Mar 17 08:07:38 2016 +0900
@@ -38,11 +38,11 @@
     _≈_ = λ a b →    _==_ (hom a) (hom b)  ;
     Id  =  \{a} -> MaybeHomId a ;
     isCategory  = record {
-            isEquivalence = record {refl = *refl ; trans = ? ; sym = ? };
-            identityL  = \{a b f} -> {!!} {a} {b} {f} ;
-            identityR  = \{a b f} -> {!!} {a} {b} {f} ;
-            o-resp-≈  = \{a b c f g h i} -> {!!}  {a} {b} {c} {f} {g} {h} {i} ;
-            associative  = \{a b c d f g h } -> {!!}  {a} {b} {c} {d} {f} {g} {h}
+            isEquivalence = 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) 
@@ -51,11 +51,37 @@
         *refl  {_} {_} {just x}  = just refl-hom
         *refl  {_} {_} {nothing} = nothing
 
-        *sym : ∀ {x y} → x == y → y == x
+        *sym : {a b : Obj A } -> {x y : Maybe ( Hom A a b ) }  → x == y → y == x
         *sym (just x≈y) = just (sym x≈y)
         *sym nothing    = nothing
 
-        *trans : ∀ {x y z} → x == y → y == z → x == z
+        *trans : {a b : Obj A } -> {x y z : Maybe ( Hom A a b ) }  → x == y → y == z → x == z
         *trans (just x≈y) (just y≈z) = just (trans-hom x≈y y≈z)
         *trans nothing    nothing    = nothing
 
+        identityL : { a b : Obj A } { f : MaybeHom A a b } ->  hom (MaybeHomId b × f) == hom f
+        identityL {a} {b} {f}  with hom f
+        identityL {a} {b} {_} | nothing  = nothing
+        identityL {a} {b} {_} | just f = just ( IsCategory.identityL ( Category.isCategory A )  {a} {b} {f}  )
+
+        identityR : { a b : Obj A } { f : MaybeHom A a b } ->  hom (f × MaybeHomId a  ) == hom f
+        identityR {a} {b} {f}  with hom f
+        identityR {a} {b} {_} | nothing  = nothing
+        identityR {a} {b} {_} | just f = just ( IsCategory.identityR ( Category.isCategory A )  {a} {b} {f}  )
+
+        o-resp-≈  :  {a b c : Obj A} → {f g : MaybeHom A a b } → {h i : MaybeHom A  b c } → hom f == hom g → hom h == hom i → hom (h × f) == hom (i × g)
+        o-resp-≈  {a} {b} {c} {f} {g} {h} {i} eq-fg eq-hi with hom f | hom g  | hom h | hom i
+        o-resp-≈  {a} {b} {c} {_} {_} {_} {_}  (just eq-fg)  (just eq-hi) | just f | just g | just h | just i =  
+             just ( IsCategory.o-resp-≈ ( Category.isCategory A )  {a} {b} {c} {f} {g} {h} {i} eq-fg eq-hi )
+        o-resp-≈  {a} {b} {c} {f} {g} {h} {i} (just _)  nothing | just _ | just _ | nothing | nothing = nothing
+        o-resp-≈  {a} {b} {c} {f} {g} {h} {i} nothing  (just _) | nothing | nothing | just _ | just _ = nothing
+        o-resp-≈  {a} {b} {c} {f} {g} {h} {i} nothing nothing | nothing | nothing | nothing | nothing = nothing
+
+
+        associative  :  {a b c d : Obj A} → {f : MaybeHom A c d } → {g : MaybeHom A b c } → {h : MaybeHom A a b } → hom (f × (g × h)) == hom ((f × g) × h)
+        associative  {_} {_} {_} {_} {f} {g} {h}  with hom f | hom g | hom h 
+        associative  {_} {_} {_} {_} {f} {g} {h}  | nothing | _ | _ = nothing
+        associative  {_} {_} {_} {_} {f} {g} {h}  | just _ | nothing | _ = nothing
+        associative  {_} {_} {_} {_} {f} {g} {h}  | just _ | just _ | nothing = nothing
+        associative  {a} {b} {c} {d} {_} {_} {_}  | just f | just g | just h = 
+             just ( IsCategory.associative ( Category.isCategory A )  {a} {b} {c} {d} {f} {g} {h}  )