Mercurial > hg > Members > kono > Proof > category

changeset 379:44f045fcbd20

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
step by step ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 12 Mar 2016 12:33:31 +0900
parents 3af53d4757e7
children c2ca1443bc1d
files limit-to.agda
diffstat 1 files changed, 40 insertions(+), 26 deletions(-) [+]
line wrap: on
line diff
--- a/limit-to.agda	Sat Mar 12 11:35:10 2016 +0900
+++ b/limit-to.agda	Sat Mar 12 12:33:31 2016 +0900
@@ -95,8 +95,8 @@
     isCategory  = record {
             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} ;
+            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
@@ -110,40 +110,54 @@
                 just ( Map ( record { Map = id-t0 ; Sel = t0 ; selection = refl } ) )
               ≡⟨ refl ⟩
                 just (arrowSel t0 t0 (Sel f ) )
-              ≡⟨ Relation.Binary.PropositionalEquality.cong (\x -> just x) ( selection f )  ⟩
+              ≡⟨ ≡-cong (\x -> just x) ( selection f )  ⟩
                 twomap (just f)
               ∎
         identityL {t0} {t1} {f} = refl
-        identityL {t1} {t0} {f} =   let open ≡-Reasoning in
-              begin
-                twomap (Two-id t0 × just f)
-              ≡⟨ refl ⟩
-                twomap (just f)
-              ∎
-        identityL {t1} {t1} {f} = Relation.Binary.PropositionalEquality.cong (\x -> just x) ( selection f ) 
+        identityL {t1} {t0} {f} = refl
+        identityL {t1} {t1} {f} = ≡-cong (\x -> just x) ( selection f ) 
         identityL' : {A B : TwoObject} {f : Maybe ( Two-Hom A B)} →  twomap ( Two-id B × f ) ≡ twomap f
-        identityL' {a} {b} {f = nothing}  =   let open ≡-Reasoning in
-              begin
-                twomap {a} {b} ( Two-id b × nothing )
-              ≡⟨ Relation.Binary.PropositionalEquality.cong (\x -> twomap  {a} {b} x) refl ⟩
-                twomap {a} {b} nothing
-              ∎
+        identityL' {a} {b} {f = nothing}  =  refl
         identityL' {a} {b} {just f}  =  identityL {a} {b} {f}  
+        identityR : {A B : TwoObject} {f : Two-Hom A B} →  twomap ( (just f) × Two-id A ) ≡ twomap (just f)
+        identityR {t0} {t0} {f} = ≡-cong (\x -> just x) ( selection f ) 
+        identityR {t0} {t1} {f} = refl
+        identityR {t1} {t0} {f} = refl
+        identityR {t1} {t1} {f} = ≡-cong (\x -> just x) ( selection f ) 
+        identityR' : {A B : TwoObject} {f : Maybe ( Two-Hom A B)} →  twomap ( f × Two-id A  ) ≡ twomap f
+        identityR' {t0} {t0} {f = nothing}  = refl
+        identityR' {t0} {t1} {f = nothing}  = refl
+        identityR' {t1} {t0} {f = nothing}  = refl
+        identityR' {t1} {t1} {f = nothing}  = refl
+        identityR' {a} {b} {just f}  =  identityR {a} {b} {f}  
 --         identityR : {A B : TwoObject} {f : Two-Hom A B} → Map ( f × Two-id A ) ≡ Map f
 --         identityR {t0} {t0} {f} = selection f
 --         identityR {t0} {t1} {f} = refl
 --         identityR {t1} {t0} {f} = selection f
 --         identityR {t1} {t1} {f} = selection f
---         o-resp-≈  : {A B C : TwoObject} {f g : Two-Hom A B} {h i : Two-Hom B C} →
---            Map f ≡ Map g → Map h ≡ Map i → Map ( h × f ) ≡ Map ( i × g )
---         o-resp-≈  {t0} {t0} {t0} {f} {g} {h} {i} f≡g h≡i = refl
---         o-resp-≈  {t0} {t0} {t1} {f} {g} {h} {i} f≡g h≡i = h≡i
---         o-resp-≈  {t0} {t1} {t0} {f} {g} {h} {i} f≡g h≡i = refl
---         o-resp-≈  {t0} {t1} {t1} {f} {g} {h} {i} f≡g h≡i = f≡g
---         o-resp-≈  {t1} {t0} {t0} {f} {g} {h} {i} f≡g h≡i = refl
---         o-resp-≈  {t1} {t0} {t1} {f} {g} {h} {i} f≡g h≡i = refl
---         o-resp-≈  {t1} {t1} {t0} {f} {g} {h} {i} f≡g h≡i = refl
---         o-resp-≈  {t1} {t1} {t1} {f} {g} {h} {i} f≡g h≡i = refl
+        o-resp-≈ : {A B C : TwoObject} {f g : Maybe ( Two-Hom A B)} {h i : Maybe (Two-Hom B C)} →
+            twomap f ≡ twomap g → twomap h ≡ twomap i → twomap ( h × f ) ≡ twomap ( i × g )
+        o-resp-≈  {a} {b} {c} {nothing} {g} {h} {i}  f≡g  h≡i   =  let open ≡-Reasoning in
+              begin
+                twomap {a} {c} (h × nothing)
+              ≡⟨⟩
+                nothing
+              ≡⟨⟩
+                twomap {a} {c} (i × nothing)
+              ≡⟨ f≡g ⟩
+                twomap (i × g)
+              ∎
+        o-resp-≈  {_} {_} {_} {_} {nothing} {_} {_} _ _ = {!!}
+        o-resp-≈  {_} {_} {_} {_} {_} {nothing} {_} _ _ = {!!}
+        o-resp-≈  {_} {_} {_} {_} {_} {_} {nothing} _ _ = {!!}
+        o-resp-≈  {t0} {t0} {t0} {just f} {just g} {just h} {just i} _ _ = refl
+        o-resp-≈  {t0} {t0} {t1} {just f} {just g} {just h} {just i} _ h≡i = h≡i
+        o-resp-≈  {t0} {t1} {t0} {just f} {just g} {just h} {just i} _ _ = refl
+        o-resp-≈  {t0} {t1} {t1} {just f} {just g} {just h} {just i} f≡g _ = f≡g
+        o-resp-≈  {t1} {t0} {t0} {just f} {just g} {just h} {just i} _ _ = refl
+        o-resp-≈  {t1} {t0} {t1} {just f} {just g} {just h} {just i} _ _ = refl
+        o-resp-≈  {t1} {t1} {t0} {just f} {just g} {just h} {just i} _ _ = refl
+        o-resp-≈  {t1} {t1} {t1} {just f} {just g} {just h} {just i} _ _ = refl
 --         associative : {A B C D : TwoObject} {f : Two-Hom C D} {g : Two-Hom B C} {h : Two-Hom A B} → Map ( f × (g × h) ) ≡ Map ( (f × g) × h )
 --         associative {t0} {t0} {t0} {t0} {f} {g} {h} = refl
 --         associative {t0} {t0} {t0} {t1} {f} {g} {h} = refl