Mercurial > hg > Members > kono > Proof > category

changeset 381:1ae9a3fcb0ee

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 13 Mar 2016 02:11:50 +0900
parents c2ca1443bc1d
children 813cf2e2bd1a
files limit-to.agda
diffstat 1 files changed, 63 insertions(+), 93 deletions(-) [+]
line wrap: on
line diff
--- a/limit-to.agda	Sat Mar 12 13:15:53 2016 +0900
+++ b/limit-to.agda	Sun Mar 13 02:11:50 2016 +0900
@@ -67,23 +67,32 @@
 Two-id t0  = just ( record { Map = id-t0 ; Sel = t0 ; selection = refl } )
 Two-id t1  = just ( record { Map = id-t1 ; Sel = t0 ; selection = refl } )
 
+arrow2hom : {a b : TwoObject} -> Arrow  -> Maybe ( Two-Hom a b ) 
+arrow2hom {t0} {t0}  id-t0 = Two-id t0
+arrow2hom {t1} {t1}  id-t1 = Two-id t1
+arrow2hom {t0} {t1}  arrow-f = just ( record { Map = arrow-f ; Sel = t0 ; selection = refl } )
+arrow2hom {t0} {t1}  arrow-g = just ( record { Map = arrow-g ; Sel = t1 ; selection = refl } )
+arrow2hom {_} {_} _  = nothing
+
+lemma-iso  : {a b : TwoObject} -> { f :  Two-Hom a b  } -> just f ≡ arrow2hom ( arrowSel a b (Sel f) )  
+lemma-iso  = {!!}
+
 -- arrow composition
 
-
-two-hom-comp  :   {A B C : TwoObject } →  Two-Hom B C  →  Two-Hom A B  →  Maybe ( Two-Hom A C )
-two-hom-comp   {t0} {t0} {t0} a b  = just ( record { Map = id-t0 ; Sel = t0 ; selection = refl } )
-two-hom-comp   {t0} {t0} {t1} a b  = just ( record { Map = Map a ; Sel = Sel a ; selection = selection a } )
-two-hom-comp   {t0} {t1} {t0} a b  = nothing
-two-hom-comp   {t0} {t1} {t1} a b  = just ( record { Map = Map b ; Sel = Sel b ; selection = selection b } )
-two-hom-comp   {t1} {t0} {t0} a b  = nothing
-two-hom-comp   {t1} {t0} {t1} a b  = nothing
-two-hom-comp   {t1} {t1} {t0} a b  = nothing
-two-hom-comp   {t1} {t1} {t1} a b  = just ( record { Map = id-t1 ; Sel = t0 ; selection = refl } )
+twocomp :  {A B C : TwoObject } → Maybe Arrow -> Maybe Arrow -> Maybe ( Two-Hom A C )
+twocomp    {a} {b} {c} nothing  ga  = nothing
+twocomp    {a} {b} {c} fa  nothing  = nothing
+twocomp   {t0} {t0} {t0} ( just i ) ( just _ ) = arrow2hom i
+twocomp   {t0} {t0} {t1} ( just f ) ( just _ ) = arrow2hom f
+twocomp   {t0} {t1} {t0} ( just _ ) ( just _ ) = nothing
+twocomp   {t0} {t1} {t1} ( just _ ) ( just g ) = arrow2hom g
+twocomp   {t1} {t0} {t0} ( just _ ) ( just _ ) = nothing
+twocomp   {t1} {t0} {t1} ( just _ ) ( just _ ) = nothing
+twocomp   {t1} {t1} {t0} ( just _ ) ( just _ ) = nothing
+twocomp   {t1} {t1} {t1} ( just _ ) ( just i ) = arrow2hom i
 
 _×_ :  {A B C : TwoObject } → Maybe ( Two-Hom B C ) → Maybe ( Two-Hom A B ) → Maybe ( Two-Hom A C )
-_×_   {_} {_} {_} _ nothing  = nothing
-_×_   {_} {_} {_} nothing _  = nothing
-_×_   {a} {b} {c} (just f) (just g) = two-hom-comp {a} {b} {c}  f g 
+_×_   {a} {b} {c} f g  = twocomp {a} {b} {c} ( twomap {b} {c} f ) ( twomap {a} {b} g )
 
 twocat : {ℓ c₁ c₂ : Level  } ->  Category _ _ _ 
 twocat  = record {
@@ -97,100 +106,61 @@
             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}
+            associative  = \{a b c d f g h } -> associative  {a} {b} {c} {d} {f} {g} {h}
        } 
    } where
         open  import  Relation.Binary.PropositionalEquality
         ≡-cong = Relation.Binary.PropositionalEquality.cong 
-        identityL : {A B : TwoObject} {f : Two-Hom A B} →  twomap ( Two-id B × (just f) ) ≡ twomap (just f)
-        identityL {t0} {t0} {f} =  let open ≡-Reasoning in
-              begin
-                twomap ( Two-id t0 × (just f) )
-              ≡⟨⟩
-                just ( Map ( record { Map = id-t0 ; Sel = t0 ; selection = refl } ) )
-              ≡⟨ refl ⟩
-                just (arrowSel t0 t0 (Sel f ) )
-              ≡⟨ ≡-cong (\x -> just x) ( selection f )  ⟩
-                twomap (just f)
-              ∎
-        identityL {t0} {t1} {f} = refl
-        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}  =  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 ) 
+        identityL' {t0} {t0} {f = nothing}  = refl
+        identityL' {t0} {t1} {f = nothing}  = refl
+        identityL' {t1} {t0} {f = nothing}  = refl
+        identityL' {t1} {t1} {f = nothing}  = refl
+        identityL' {t0} {t0} {just f} = ≡-cong (\x -> just x) ( selection f ) 
+        identityL' {t1} {t1} {just f} = ?
+        identityL' {t1} {t0} {just f} = refl
+        identityL' {t0} {t1} {just f} with (Sel f)
+        identityL' {t0} {t1} {just f} | t0 =  {!!}
+        identityL' {t0} {t1} {just f} | t1 =  {!!}
         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
-        nothing-eq : {A B : TwoObject} {f : Maybe ( Two-Hom A B)} ->  twomap f ≡ nothing -> f ≡ nothing
-        nothing-eq {_} {_} {nothing } eq = refl
-        nothing-eq {t0} {t0} {just f} eq = ?
-        nothing-eq {t0} {t1} {just f} eq = ?
-        nothing-eq {t1} {t0} {just f} eq = ?
-        nothing-eq {t1} {t1} {just f} eq = ?
+        identityR' {t0} {t0} {just f} = {!!} 
+        identityR' {t1} {t1} {just f} = ≡-cong (\x -> just x) ( selection f ) 
+        identityR' {t1} {t0} {just f} = refl
+        identityR' {t0} {t1} {just f} =  {!!}
         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
+        o-resp-≈  {a} {b} {c} {f} {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)
+                twomap (twocomp {a} {b} {c}  ( twomap h ) ( twomap {a} {b} f )  )
+              ≡⟨ ≡-cong (\y -> twomap (twocomp {a} {b} {c}  y  ( twomap {a} {b} f )  )) h≡i  ⟩
+                twomap (twocomp {a} {b} {c}  ( twomap i ) ( twomap {a} {b} f )  )
+              ≡⟨ ≡-cong (\y -> twomap (twocomp {a} {b} {c}  (twomap i)   y  )) f≡g  ⟩
+                twomap (twocomp {a} {b} {c}  ( twomap i ) ( twomap {a} {b} 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
---         associative {t0} {t0} {t1} {t0} {f} {g} {h} = refl
---         associative {t0} {t0} {t1} {t1} {f} {g} {h} = refl
---         associative {t0} {t1} {t0} {t0} {f} {g} {h} = refl
---         ---      g = (f o f') o g !=  f o ( f' o g ) = f
---         associative {t0} {t1} {t0} {t1} {f} {g} {h} =  let open ≡-Reasoning in
---               begin
---                 Map ( f × (g × h) )
---               ≡⟨⟩
---                 Map f 
---               ≡⟨ {!!} ⟩
---                 Map h
---               ≡⟨⟩
---                 Map ( (f × g) × h )
---               ∎
---         associative {t0} {t1} {t1} {t0} {f} {g} {h} = refl
---         associative {t0} {t1} {t1} {t1} {f} {g} {h} = refl
---         associative {t1} {t0} {t0} {t0} {f} {g} {h} = refl
---         associative {t1} {t0} {t0} {t1} {f} {g} {h} = refl
---         associative {t1} {t0} {t1} {t0} {f} {g} {h} = refl
---         associative {t1} {t0} {t1} {t1} {f} {g} {h} = refl
---         associative {t1} {t1} {t0} {t0} {f} {g} {h} = refl
---         associative {t1} {t1} {t0} {t1} {f} {g} {h} = refl
---         associative {t1} {t1} {t1} {t0} {f} {g} {h} = refl
---         associative {t1} {t1} {t1} {t1} {f} {g} {h} = refl
+        associative : {A B C D : TwoObject} {f : Maybe (Two-Hom C D)} {g : Maybe (Two-Hom B C)} {h : Maybe (Two-Hom A B)} → twomap ( f × (g × h) ) ≡ twomap ( (f × g) × h )
+        associative {_} {_} {_} {_} {nothing} {g} {h} = refl
+        associative {_} {_} {_} {_} {_} {nothing} {h} = {!!}
+        associative {_} {_} {_} {_} {_} {g} {nothing} = {!!}
+        associative {t0} {t0} {t0} {t0} {just f} {just g} {just h} = {!!}
+        associative {t0} {t0} {t0} {t1} {just f} {just g} {just h} = {!!}
+        associative {t0} {t0} {t1} {t0} {just f} {just g} {just h} = {!!}
+        associative {t0} {t0} {t1} {t1} {just f} {just g} {just h} = {!!}
+        associative {t0} {t1} {t0} {t0} {just f} {just g} {just h} = {!!}
+        associative {t0} {t1} {t0} {t1} {just f} {just g} {just h} = {!!}
+        associative {t0} {t1} {t1} {t0} {just f} {just g} {just h} = {!!}
+        associative {t0} {t1} {t1} {t1} {just f} {just g} {just h} = {!!}
+        associative {t1} {t0} {t0} {t0} {just f} {just g} {just h} = {!!}
+        associative {t1} {t0} {t0} {t1} {just f} {just g} {just h} = {!!}
+        associative {t1} {t0} {t1} {t0} {just f} {just g} {just h} = {!!}
+        associative {t1} {t0} {t1} {t1} {just f} {just g} {just h} = {!!}
+        associative {t1} {t1} {t0} {t0} {just f} {just g} {just h} = {!!}
+        associative {t1} {t1} {t0} {t1} {just f} {just g} {just h} = {!!}
+        associative {t1} {t1} {t1} {t0} {just f} {just g} {just h} = {!!}
+        associative {t1} {t1} {t1} {t1} {just f} {just g} {just h} = {!!}