Mercurial > hg > Members > kono > Proof > category

changeset 414:28249d32b700

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Maybe does not help conflict ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 23 Mar 2016 17:16:29 +0900
parents e08af559efb9
children dd086f5fb29f
files limit-to.agda
diffstat 1 files changed, 30 insertions(+), 11 deletions(-) [+]
line wrap: on
line diff
--- a/limit-to.agda	Wed Mar 23 16:25:23 2016 +0900
+++ b/limit-to.agda	Wed Mar 23 17:16:29 2016 +0900
@@ -40,9 +40,11 @@
 _×_   nothing _  = nothing
 _×_   (just _) nothing  = nothing
 _×_   {c₁} {c₂} {t1} {t1} {t1} _ f   =  f
+_×_   {c₁} {c₂} {t0} {t0} {t0} f _   =  f
 _×_   {c₁} {c₂} {t0} {t1} {t1} _ f   =  f
-_×_   {c₁} {c₂} {t0} {t0} {t0} _ f   =  f
 _×_   {c₁} {c₂} {t0} {t0} {t1} f _   =  f
+-- _×_   {c₁} {c₂} {t1} {t0} {t0} _ f   =  f
+-- _×_   {c₁} {c₂} {t1} {t1} {t0} f _   =  f
 _×_   {c₁} {c₂} {a} {b} {c} (just f)  (just g)   =  nothing
 
 
@@ -62,6 +64,7 @@
 ==trans (just x≈y) (just y≈z) = just (≡-trans x≈y y≈z)
 ==trans nothing    nothing    = nothing
 
+
 module ==-Reasoning {c₁ c₂ : Level} where
 
         infixr  2 _∎
@@ -128,6 +131,12 @@
 
 open import maybeCat  
 
+--        identityL  {c₁}  {c₂}  {_} {b} {nothing}  =   let open ==-Reasoning  {c₁}  {c₂} in
+--                begin
+--                   (TwoId b × nothing)
+--                ==⟨ {!!}  ⟩
+--                  nothing
+--                ∎
 
 open import Relation.Binary 
 TwoCat : {c₁ c₂ ℓ : Level  } ->  Category   c₁  c₂  c₂
@@ -146,20 +155,30 @@
        } 
    }  where
         identityL :  {c₁  c₂ : Level } {A B : TwoObject {c₁}} {f : Maybe ( TwoHom {c₁}  {c₂ } A B) } →  ((TwoId B)  × f)  == f
-        identityL {_} {_}  {_} {_} {nothing}  = {!!}
-        identityL {_} {_}  {t0} {t0} {just f}  = ==refl
+        identityL  {c₁}  {c₂}  {t0} {t0} {nothing}  =   ==refl
+        identityL  {c₁}  {c₂}  {t0} {t1} {nothing}  =   ==refl
+        identityL  {c₁}  {c₂}  {t1} {t0} {nothing}  =   ==refl
+        identityL  {c₁}  {c₂}  {t1} {t1} {nothing}  =   ==refl
         identityL {_} {_}  {t0} {t1} {just f}  = ==refl
         identityL {_} {_}  {t1} {t1} {just f}  = ==refl
-        identityL   {c₁}  {c₂}  {t1} {t0} {just f}  =  let open ==-Reasoning  {c₁}  {c₂} in
-                begin 
-                  (TwoId t0 × just f)
+        identityL {_} {_}  {t0} {t0} {just f}  = {!!}
+        identityL {_} {_}  {t1} {t0} {just f}  = {!!}
+        identityR :  {c₁  c₂ : Level } {A B : TwoObject {c₁}} {f : Maybe ( TwoHom {c₁}  {c₂ } A B) } →   ( f × TwoId A )  == f
+        identityR  {c₁}  {c₂}  {t0} {t0} {nothing}  =   ==refl
+        identityR  {c₁}  {c₂}  {t0} {t1} {nothing}  =   ==refl
+        identityR  {c₁}  {c₂}  {t1} {t0} {nothing}  =   ==refl
+        identityR  {c₁}  {c₂}  {t1} {t1} {nothing}  =   ==refl
+        identityR {_} {_}  {t0} {t0} {just f}  = ==refl
+        identityR {_} {_}  {t0} {t1} {just f}  = ==refl
+        identityR {c₁}  {c₂}  {t1} {t0} {just f}  =   let open ==-Reasoning  {c₁}  {c₂} in                                                                
+                begin
+                  (just f × TwoId t1) 
                 ==⟨⟩
-                   nothing
+                  nothing
                 ==⟨ {!!} ⟩
-                   just f
-                ∎ 
-        identityR :  {c₁  c₂ : Level } {A B : TwoObject {c₁}} {f : Maybe ( TwoHom {c₁}  {c₂ } A B) } →   ( f × TwoId A )  == f
-        identityR {_} {_} {a} {b} {f}  = {!!}
+                  just f
+                ∎  
+        identityR {_} {_}  {t1} {t1} {just f}  = {!!}
         o-resp-≈ :  {c₁  c₂ : Level } {A B C : TwoObject  {c₁} } {f g :  Maybe ( TwoHom {c₁}  {c₂ } A B)} {h i : Maybe ( TwoHom B C)} →
             f == g → h == i → ( h × f ) == ( i × g )
         o-resp-≈  {_} {_} {a} {b} {c} {f} {g} {h} {i}  f≡g h≡i  = {!!}