Mercurial > hg > Members > kono > Proof > category

changeset 378:3af53d4757e7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add maybe in twocat
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 12 Mar 2016 11:35:10 +0900
parents 2dfa2d59268c
children 44f045fcbd20
files limit-to.agda
diffstat 1 files changed, 92 insertions(+), 68 deletions(-) [+]
line wrap: on
line diff
--- a/limit-to.agda	Fri Mar 11 18:49:58 2016 +0900
+++ b/limit-to.agda	Sat Mar 12 11:35:10 2016 +0900
@@ -6,6 +6,7 @@
 open import cat-utility
 open import HomReasoning
 open import Relation.Binary.Core
+open import Data.Maybe.Core
 open Functor
 
 
@@ -53,100 +54,123 @@
        Sel    : TwoObject
        selection :  ( arrowSel a b Sel  ) ≡ Map
 
+open Two-Hom
 
-Two-id :  (a : TwoObject ) ->  Two-Hom a a
-Two-id t0  = record { Map = id-t0 ; Sel = t0 ; selection = refl }
-Two-id t1  = record { Map = id-t1 ; Sel = t0 ; selection = refl }
+twomap : {a b : TwoObject} -> Maybe ( Two-Hom a b ) -> Maybe ( Arrow )
+twomap {_} {_} nothing = nothing
+twomap {t0} {t0} (just f)  =   just ( Map f )
+twomap {t0} {t1} (just f)  =   just ( Map f )
+twomap {t1} {t0} (just f)  =   nothing
+twomap {t1} {t1} (just f)  =   just ( Map f )
+
+Two-id :  (a : TwoObject ) ->  Maybe ( Two-Hom a a )
+Two-id t0  = just ( record { Map = id-t0 ; Sel = t0 ; selection = refl } )
+Two-id t1  = just ( record { Map = id-t1 ; Sel = t0 ; selection = refl } )
 
 -- arrow composition
 
-open Two-Hom
 
-_×_ :  {A B C : TwoObject } → Two-Hom B C → Two-Hom A B → Two-Hom A C
-_×_   {t0} {t0} {t0} a b  = record { Map = id-t0 ; Sel = t0 ; selection = refl }
-_×_   {t0} {t0} {t1} a b  = record { Map = Map a ; Sel = Sel a ; selection = selection a }
-_×_   {t0} {t1} {t0} a b  = record { Map = id-t0 ; Sel = t0 ; selection = refl }
-_×_   {t0} {t1} {t1} a b  = record { Map = Map b ; Sel = Sel b ; selection = selection b }
-_×_   {t1} {t0} {t0} a b  = record { Map = arrow-f' ; Sel = t0 ; selection = refl }
-_×_   {t1} {t0} {t1} a b  = record { Map = id-t1 ; Sel = t0 ; selection = refl }
-_×_   {t1} {t1} {t0} a b  = record { Map = arrow-f' ; Sel = t0 ; selection = refl }
-_×_   {t1} {t1} {t1} a b  = record { Map = id-t1 ; Sel = t0 ; selection = refl }
+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 } )
 
-
-
+_×_ :  {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 
 
 twocat : {ℓ c₁ c₂ : Level  } ->  Category _ _ _ 
 twocat  = record {
     Obj  = TwoObject  ;
-    Hom = λ a b →  Two-Hom a b   ; 
+    Hom = λ a b →  Maybe ( Two-Hom a b )  ; 
     _o_ =  _×_ ;
-    _≈_ = λ a b →   Map a ≡ Map b  ;
+    _≈_ = λ a b →   twomap a ≡ twomap b  ;
     Id  =  \{a} -> Two-id a ;
     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} ;
-            associative  = \{a b c d f g h } -> associative  {a} {b} {c} {d} {f} {g} {h}
+            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  import  Relation.Binary.PropositionalEquality
         ≡-cong = Relation.Binary.PropositionalEquality.cong 
-        identityL : {A B : TwoObject} {f : Two-Hom A B} → Map ( Two-id B × f ) ≡ Map f
+        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
-                Map ( Two-id t0 × f )
+                twomap ( Two-id t0 × (just f) )
               ≡⟨⟩
-                Map ( record { Map = id-t0 ; Sel = t0 ; selection = refl } )
+                just ( Map ( record { Map = id-t0 ; Sel = t0 ; selection = refl } ) )
               ≡⟨ refl ⟩
-                 arrowSel t0 t0 (Sel f )
-              ≡⟨ selection f  ⟩
-                Map f
+                just (arrowSel t0 t0 (Sel f ) )
+              ≡⟨ Relation.Binary.PropositionalEquality.cong (\x -> just x) ( selection f )  ⟩
+                twomap (just f)
               ∎
         identityL {t0} {t1} {f} = refl
-        identityL {t1} {t0} {f} = selection f
-        identityL {t1} {t1} {f} = selection 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
-        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
-        associative {t0} {t1} {t0} {t1} {f} {g} {h} =  let open ≡-Reasoning in
+        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' : {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
-                Map ( f × (g × h) )
-              ≡⟨⟩
-                Map f 
-              ≡⟨ {!!} ⟩
-                Map h
-              ≡⟨⟩
-                Map ( (f × g) × h )
+                twomap {a} {b} ( Two-id b × nothing )
+              ≡⟨ Relation.Binary.PropositionalEquality.cong (\x -> twomap  {a} {b} x) refl ⟩
+                twomap {a} {b} nothing
               ∎
-        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
+        identityL' {a} {b} {just f}  =  identityL {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
+--         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