Mercurial > hg > Members > kono > Proof > category

changeset 422:3a4a99a8edbe

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
o-resp passed
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 24 Mar 2016 13:11:50 +0900
parents 06ffcad985ac
children b5519e954b57
files limit-to.agda
diffstat 1 files changed, 46 insertions(+), 108 deletions(-) [+]
line wrap: on
line diff
--- a/limit-to.agda	Thu Mar 24 12:07:32 2016 +0900
+++ b/limit-to.agda	Thu Mar 24 13:11:50 2016 +0900
@@ -36,56 +36,48 @@
 
 record TwoHom {c₁ c₂ : Level} (a b : TwoObject {c₁}  ) : Set   c₂ where
    field
-       RawHom   :   Maybe ( Arrow {c₁} {c₂} t0 t1 a b )
-
-open TwoHom
-
-hom :  ∀{ c₁ c₂ }  {  a b : TwoObject  {c₁} } ->
-       ∀ (f :  TwoHom {c₁}  {c₂ } a b ) → Maybe ( Arrow {c₁} {c₂} t0 t1 a b )
-hom {_} {_} {a} {b} f with RawHom  f
-hom {_} {_} {t0} {t0} _ | just id-t0 = just id-t0
-hom {_} {_} {t1} {t1} _ | just id-t1 = just id-t1
-hom {_} {_} {t0} {t1} _ | just arrow-f = just arrow-f
-hom {_} {_} {t0} {t1} _ | just arrow-g = just arrow-g
-hom {_} {_} {t1} {t0} _ | just inv-f = just inv-f
-hom {_} {_} {_ } {_ } _ | _ = nothing
-
+       hom   :   Maybe ( Arrow {c₁} {c₂} t0 t1 a b )
 
 open TwoHom
 
 -- arrow composition
 
 
+comp :  ∀ {c₁  c₂}  -> {a b c : TwoObject {c₁}} →  Maybe ( Arrow {c₁} {c₂} t0 t1 b c ) →  Maybe ( Arrow {c₁} {c₂} t0 t1 a b )  →  Maybe ( Arrow {c₁} {c₂} t0 t1 a c )
+comp {_}  {_}  {_} {_} {_}  nothing     _                =   nothing 
+comp {_}  {_}  {_} {_} {_}  (just _     ) nothing          =   nothing 
+comp {_}  {_}  {t0} {t1} {t1}  (just id-t1 ) ( just arrow-f )  =   just arrow-f 
+comp {_}  {_}  {t0} {t1} {t1}  (just id-t1 ) ( just arrow-g ) =   just arrow-g 
+comp {_}  {_}  {t1} {t1} {t1}  (just id-t1 ) ( just id-t1   ) =   just id-t1 
+comp {_}  {_}  {t1} {t1} {t0}  (just inv-f ) ( just id-t1   ) =   just inv-f 
+comp {_}  {_}  {t0} {t0} {t1}  (just arrow-f ) ( just id-t0 )   =   just arrow-f 
+comp {_}  {_}  {t0} {t0} {t1}  (just arrow-g ) ( just id-t0 )   =   just arrow-g 
+comp {_}  {_}  {t0} {t0} {t0}  (just id-t0 ) ( just id-t0  )  =   just id-t0 
+comp {_}  {_}  {t1} {t0} {t0}  (just id-t0 ) ( just inv-f )   =   just inv-f 
+comp {_}  {_}  {_} {_} {_}  (just _ ) ( just _ )  =   nothing 
+
+
 _×_ :  ∀ {c₁  c₂}  -> {a b c : TwoObject {c₁}} →  ( TwoHom {c₁}  {c₂} b c ) →  ( TwoHom {c₁} {c₂} a b )  →  ( TwoHom {c₁}  {c₂} a c )
-_×_  {c₁}  {c₂}  {a} {b} {c} f g with hom f | hom g
-_×_  {_}  {_}  {_} {_} {_} f g | nothing    | _                = record { RawHom =  nothing }
-_×_  {_}  {_}  {_} {_} {_} f g | just _     | nothing          = record { RawHom =  nothing }
-_×_  {_}  {_}  {t0} {t1} {t1} f g | just id-t1 | just arrow-f  = record { RawHom =  just arrow-f }
-_×_  {_}  {_}  {t0} {t1} {t1} f g | just id-t1 | just arrow-g  = record { RawHom =  just arrow-g }
-_×_  {_}  {_}  {t1} {t1} {t1} f g | just id-t1 | just id-t1    = record { RawHom =  just id-t1 }
-_×_  {_}  {_}  {t1} {t1} {t0} f g | just inv-f | just id-t1    = record { RawHom =  just inv-f }
-_×_  {_}  {_}  {t0} {t0} {t1} f g | just arrow-f | just id-t0    = record { RawHom =  just arrow-f }
-_×_  {_}  {_}  {t0} {t0} {t1} f g | just arrow-g | just id-t0    = record { RawHom =  just arrow-g }
-_×_  {_}  {_}  {t0} {t0} {t0} f g | just id-t0 | just id-t0    = record { RawHom =  just id-t0 }
-_×_  {_}  {_}  {t1} {t0} {t0} f g | just id-t0 | just inv-f    = record { RawHom =  just inv-f }
-_×_  {_}  {_}  {_} {_} {_} f g | just _ | just _   = record { RawHom =  nothing }
+_×_  {c₁}  {c₂}  {a} {b} {c} f g  = record { hom = comp  {c₁}  {c₂}  {a} {b} {c} (hom f) (hom g ) }
 
 
 _==_ :  ∀{ c₁ c₂ a b }   ->  Rel (Maybe (Arrow {c₁} {c₂} t0 t1 a b )) (c₂)
 _==_   =  Eq   _≡_
 
 map2hom :  ∀{ c₁ c₂ } ->  {a b  : TwoObject {c₁}} →  Maybe ( Arrow  {c₁} {c₂} t0 t1 a b ) ->  TwoHom {c₁}  {c₂ } a b
-map2hom {_} {_} {t1} {t1} (just id-t1)  = record { RawHom =  just id-t1 }
-map2hom {_} {_} {t0} {t1} (just arrow-f) = record { RawHom =  just arrow-f }
-map2hom {_} {_} {t0} {t1} (just arrow-g) = record { RawHom =  just arrow-g }
-map2hom {_} {_} {t0} {t0} (just id-t0)   = record { RawHom =  just id-t0 }
-map2hom {_} {_} {_} {_} _       = record { RawHom =  nothing }
+map2hom {_} {_} {t1} {t1} (just id-t1)  = record { hom =  just id-t1 }
+map2hom {_} {_} {t0} {t1} (just arrow-f) = record { hom =  just arrow-f }
+map2hom {_} {_} {t0} {t1} (just arrow-g) = record { hom =  just arrow-g }
+map2hom {_} {_} {t0} {t0} (just id-t0)   = record { hom =  just id-t0 }
+map2hom {_} {_} {_} {_} _       = record { hom =  nothing }
 
 record TwoHom1 {c₁ c₂ : Level}  (a : TwoObject {c₁}  ) (b : TwoObject {c₁}  ) : Set   c₂ where
    field
        Map       :   TwoHom {c₁}  {c₂ } a b
        iso-Map   :   Map ≡  map2hom ( hom Map )
 
+open TwoHom1
+
 ==refl :  ∀{  c₁ c₂ a b }  ->  ∀ {x : Maybe (Arrow  {c₁} {c₂} t0 t1 a b )} → x == x
 ==refl {_} {_} {_} {_} {just x}  = just refl
 ==refl {_} {_} {_} {_} {nothing} = nothing
@@ -99,9 +91,10 @@
 ==trans (just x≈y) (just y≈z) = just (≡-trans x≈y y≈z)
 ==trans nothing    nothing    = nothing
 
-==cong :  ∀{  c₁ c₂ a b }   -> ∀ {x y :  Maybe (Arrow  {c₁}  {c₂} t0 t1 a b )} →  
-        (f : Maybe (Arrow  {c₁}  {c₂} t0 t1 a b ) -> Maybe (Arrow  {c₁}  {c₂} t0 t1 a b ) ) -> x  ≡  y →  f x == f y
-==cong f refl = ==refl
+==cong :  ∀{  c₁ c₂ a b c d }   -> ∀ {x y :  Maybe (Arrow  {c₁}  {c₂} t0 t1 a b )} →  
+        (f : Maybe (Arrow  {c₁}  {c₂} t0 t1 a b ) -> Maybe (Arrow  {c₁}  {c₂} t0 t1 c d ) ) -> x  ==  y →  f x == f y
+==cong   {  c₁} {c₂} {a} {b } {c} {d} {nothing} {nothing} f nothing = ==refl
+==cong   {  c₁} {c₂} {a} {b } {c} {d} {just x} {just .x} f (just refl)  = ==refl
 
 
 module ==-Reasoning {c₁ c₂ : Level} where
@@ -123,6 +116,7 @@
                     x == y  → y IsRelatedTo z → x IsRelatedTo z
         _ ==⟨ x≈y ⟩ relTo y≈z = relTo (==trans x≈y y≈z)
 
+        
         _==⟨⟩_ :   { a b : TwoObject  {c₁} }(x : Maybe (Arrow  {c₁}  {c₂} t0 t1 a b )) {y : Maybe (Arrow  {c₁}  {c₂} t0 t1 a b  )}
                     → x IsRelatedTo y → x IsRelatedTo y
         _ ==⟨⟩ x≈y = x≈y
@@ -131,6 +125,10 @@
         _∎ _ = relTo ==refl
 
 
+-- TwoHom1Eq :  {c₁  c₂ : Level } {a b : TwoObject  {c₁} } {f g :  ( TwoHom1 {c₁}  {c₂ } a b)}  →
+--             hom (Map f) == hom (Map g) → f == g
+-- TwoHom1Eq  = ?
+
 
 --          f    g    h
 --       d <- c <- b <- a
@@ -224,8 +222,8 @@
 
 
 TwoId :  {c₁  c₂ : Level } (a : TwoObject  {c₁} ) ->  (TwoHom {c₁}  {c₂ } a a )
-TwoId {_} {_} t0 = record { RawHom =  just id-t0 }
-TwoId {_} {_} t1 = record { RawHom =  just id-t1 }
+TwoId {_} {_} t0 = record { hom =  just id-t0 }
+TwoId {_} {_} t1 = record { hom =  just id-t1 }
 
 open import maybeCat
 
@@ -276,78 +274,18 @@
         identityR  {c₁}  {c₂}  {t0} {t1} {_} | just arrow-g = ==refl
         o-resp-≈ :  {c₁  c₂ : Level } {A B C : TwoObject  {c₁} } {f g :  ( TwoHom {c₁}  {c₂ } A B)} {h i : ( TwoHom B C)} →
             hom f == hom g → hom h == hom i → hom ( h × f ) == hom ( i × g )
-        o-resp-≈  {c₁}  {c₂} {a} {b} {c} {f} {g} {h} {i}  f≡g h≡i  with hom f | hom g | hom h | hom i
-        o-resp-≈  {c₁}  {c₂} {t0} {t0} {t0} {f} {g} {h} {i}  nothing nothing | nothing | nothing | nothing | nothing  = nothing
-        o-resp-≈  {c₁}  {c₂} {t0} {t0} {t1} {f} {g} {h} {i}  nothing nothing | nothing | nothing | nothing | nothing  = nothing
-        o-resp-≈  {c₁}  {c₂} {t0} {t1} {t0} {f} {g} {h} {i}  nothing nothing | nothing | nothing | nothing | nothing  = nothing
-        o-resp-≈  {c₁}  {c₂} {t0} {t1} {t1} {f} {g} {h} {i}  nothing nothing | nothing | nothing | nothing | nothing  = nothing
-        o-resp-≈  {c₁}  {c₂} {t1} {t0} {t0} {f} {g} {h} {i}  nothing nothing | nothing | nothing | nothing | nothing  = nothing
-        o-resp-≈  {c₁}  {c₂} {t1} {t0} {t1} {f} {g} {h} {i}  nothing nothing | nothing | nothing | nothing | nothing  = nothing
-        o-resp-≈  {c₁}  {c₂} {t1} {t1} {t0} {f} {g} {h} {i}  nothing nothing | nothing | nothing | nothing | nothing  = nothing
-        o-resp-≈  {c₁}  {c₂} {t1} {t1} {t1} {f} {g} {h} {i}  nothing nothing | nothing | nothing | nothing | nothing  = nothing
-        o-resp-≈  {c₁}  {c₂} {t0} {t0} {t0} {f} {g} {h} {i}  f≡g nothing | just _ | just _ | nothing | nothing  = nothing
-        o-resp-≈  {c₁}  {c₂} {t0} {t0} {t1} {f} {g} {h} {i}  f≡g nothing | just _ | just _ | nothing | nothing  = nothing
-        o-resp-≈  {c₁}  {c₂} {t0} {t1} {t0} {f} {g} {h} {i}  f≡g nothing | just _ | just _ | nothing | nothing  = nothing
-        o-resp-≈  {c₁}  {c₂} {t0} {t1} {t1} {f} {g} {h} {i}  f≡g nothing | just _ | just _ | nothing | nothing  = nothing
-        o-resp-≈  {c₁}  {c₂} {t1} {t0} {t0} {f} {g} {h} {i}  f≡g nothing | just _ | just _ | nothing | nothing  = nothing
-        o-resp-≈  {c₁}  {c₂} {t1} {t0} {t1} {f} {g} {h} {i}  f≡g nothing | just _ | just _ | nothing | nothing  = nothing
-        o-resp-≈  {c₁}  {c₂} {t1} {t1} {t0} {f} {g} {h} {i}  f≡g nothing | just _ | just _ | nothing | nothing  = nothing
-        o-resp-≈  {c₁}  {c₂} {t1} {t1} {t1} {f} {g} {h} {i}  f≡g nothing | just _ | just _ | nothing | nothing  = nothing
-        o-resp-≈  {c₁}  {c₂} {t0} {t0} {t0} {f} {g} {h} {i}  nothing h≡i | nothing | nothing | just _ | just _ = nothing
-        o-resp-≈  {c₁}  {c₂} {t0} {t0} {t1} {f} {g} {h} {i}  nothing h≡i | nothing | nothing | just _ | just _ = nothing
-        o-resp-≈  {c₁}  {c₂} {t0} {t1} {t0} {f} {g} {h} {i}  nothing h≡i | nothing | nothing | just _ | just _ = nothing
-        o-resp-≈  {c₁}  {c₂} {t0} {t1} {t1} {f} {g} {h} {i}  nothing h≡i | nothing | nothing | just _ | just _ = nothing
-        o-resp-≈  {c₁}  {c₂} {t1} {t0} {t0} {f} {g} {h} {i}  nothing h≡i | nothing | nothing | just _ | just _ = nothing
-        o-resp-≈  {c₁}  {c₂} {t1} {t0} {t1} {f} {g} {h} {i}  nothing h≡i | nothing | nothing | just _ | just _ = nothing
-        o-resp-≈  {c₁}  {c₂} {t1} {t1} {t0} {f} {g} {h} {i}  nothing h≡i | nothing | nothing | just _ | just _ = nothing
-        o-resp-≈  {c₁}  {c₂} {t1} {t1} {t1} {f} {g} {h} {i}  nothing h≡i | nothing | nothing | just _ | just _ = nothing
-        o-resp-≈  {c₁}  {c₂} {_} {_} {_} {f} {g} {h} {i}  f≡g (just refl) | nothing | just _ | just jh | just .jh = {!!}
-        o-resp-≈  {c₁}  {c₂} {_} {_} {_} {f} {g} {h} {i}  f≡g (just refl) | just _ | nothing | just jh | just .jh = {!!}
-        o-resp-≈  {c₁}  {c₂} {_} {_} {_} {f} {g} {h} {i}  (just refl) h≡i | just jf | just .jf | nothing | just _ = {!!}
-        o-resp-≈  {c₁}  {c₂} {_} {_} {_} {f} {g} {h} {i}  (just refl) h≡i | just jf | just .jf | just _ | nothing = {!!}
-        o-resp-≈  {c₁}  {c₂} {t0} {t0} {t0} {f} {g} {h} {i}  f≡g h≡i | just id-t0 | nothing | just id-t0 | nothing = ?
-        o-resp-≈  {c₁}  {c₂} {_} {_} {_} {f} {g} {h} {i}  f≡g h≡i | just _ | nothing | just _ | nothing = {!!}
-        o-resp-≈  {c₁}  {c₂} {_} {_} {_} {f} {g} {h} {i}  f≡g h≡i | nothing | just _ | just _ | nothing = {!!}
-        o-resp-≈  {c₁}  {c₂} {_} {_} {_} {f} {g} {h} {i}  f≡g h≡i | nothing | just _ | nothing | just _ = {!!}
-        o-resp-≈  {c₁}  {c₂} {_} {_} {_} {f} {g} {h} {i}  f≡g h≡i | just _ | nothing | nothing | just _ = {!!}
-        o-resp-≈  {c₁}  {c₂} {t0} {t0} {t0} {f} {g} {h} {i}  nothing h≡i | nothing | nothing | nothing | just _ = nothing
-        o-resp-≈  {c₁}  {c₂} {t0} {t0} {t1} {f} {g} {h} {i}  nothing h≡i | nothing | nothing | nothing | just _ = nothing
-        o-resp-≈  {c₁}  {c₂} {t0} {t1} {t0} {f} {g} {h} {i}  nothing h≡i | nothing | nothing | nothing | just _ = nothing
-        o-resp-≈  {c₁}  {c₂} {t0} {t1} {t1} {f} {g} {h} {i}  nothing h≡i | nothing | nothing | nothing | just _ = nothing
-        o-resp-≈  {c₁}  {c₂} {t1} {t0} {t0} {f} {g} {h} {i}  nothing h≡i | nothing | nothing | nothing | just _ = nothing
-        o-resp-≈  {c₁}  {c₂} {t1} {t0} {t1} {f} {g} {h} {i}  nothing h≡i | nothing | nothing | nothing | just _ = nothing
-        o-resp-≈  {c₁}  {c₂} {t1} {t1} {t0} {f} {g} {h} {i}  nothing h≡i | nothing | nothing | nothing | just _ = nothing
-        o-resp-≈  {c₁}  {c₂} {t1} {t1} {t1} {f} {g} {h} {i}  nothing h≡i | nothing | nothing | nothing | just _ = nothing
-        o-resp-≈  {c₁}  {c₂} {t0} {t0} {t0} {f} {g} {h} {i}  nothing h≡i | nothing | nothing | just _ | nothing = nothing
-        o-resp-≈  {c₁}  {c₂} {t0} {t0} {t1} {f} {g} {h} {i}  nothing h≡i | nothing | nothing | just _ | nothing = nothing
-        o-resp-≈  {c₁}  {c₂} {t0} {t1} {t0} {f} {g} {h} {i}  nothing h≡i | nothing | nothing | just _ | nothing = nothing
-        o-resp-≈  {c₁}  {c₂} {t0} {t1} {t1} {f} {g} {h} {i}  nothing h≡i | nothing | nothing | just _ | nothing = nothing
-        o-resp-≈  {c₁}  {c₂} {t1} {t0} {t0} {f} {g} {h} {i}  nothing h≡i | nothing | nothing | just _ | nothing = nothing
-        o-resp-≈  {c₁}  {c₂} {t1} {t0} {t1} {f} {g} {h} {i}  nothing h≡i | nothing | nothing | just _ | nothing = nothing
-        o-resp-≈  {c₁}  {c₂} {t1} {t1} {t0} {f} {g} {h} {i}  nothing h≡i | nothing | nothing | just _ | nothing = nothing
-        o-resp-≈  {c₁}  {c₂} {t1} {t1} {t1} {f} {g} {h} {i}  nothing h≡i | nothing | nothing | just _ | nothing = nothing
-        o-resp-≈  {c₁}  {c₂} {t0} {t0} {t0} {f} {g} {h} {i}  f≡g nothing | nothing | just _ | nothing | nothing = nothing
-        o-resp-≈  {c₁}  {c₂} {_} {_} {_} {f} {g} {h} {i}  f≡g h≡i | nothing | just _ | nothing | nothing = {!!}
-        o-resp-≈  {c₁}  {c₂} {t0} {t0} {t0} {f} {g} {h} {i}  f≡g nothing | just _ | nothing | nothing | nothing = nothing
-        o-resp-≈  {c₁}  {c₂} {_} {_} {_} {f} {g} {h} {i}  f≡g h≡i | just _ | nothing | nothing | nothing = {!!}
-        o-resp-≈  {c₁}  {c₂} {t0} {t0} {t0} {f} {g} {h} {i}  (just refl) (just refl) | just id-t0 | just id-t0 | just id-t0  | just id-t0   =  ==refl
-        o-resp-≈  {c₁}  {c₂} {t1} {t1} {t1} {f} {g} {h} {i}  (just refl) (just refl) | just id-t1 | just id-t1 | just id-t1  | just id-t1   =  ==refl
-        o-resp-≈  {c₁}  {c₂} {t0} {t1} {t1} {f} {g} {h} {i}  (just refl) (just refl) | just arrow-f | just arrow-f | just id-t1  | just id-t1   =  ==refl
-        o-resp-≈  {c₁}  {c₂} {t0} {t1} {t1} {f} {g} {h} {i}  (just refl) (just refl) | just arrow-g | just arrow-g | just id-t1  | just id-t1   =  ==refl
-        o-resp-≈  {c₁}  {c₂} {t0} {t0} {t1} {f} {g} {h} {i}  (just refl) (just refl) | just id-t0 | just id-t0 | just arrow-f | just arrow-f  =  ==refl
-        o-resp-≈  {c₁}  {c₂} {t0} {t0} {t1} {f} {g} {h} {i}  (just refl) (just refl) | just id-t0 | just id-t0 | just arrow-g | just arrow-g  =  ==refl
-        o-resp-≈  {c₁}  {c₂} {t1} {t1} {t0} {f} {g} {h} {i}  (just refl) (just refl) | just id-t1 | just id-t1 | just inv-f | just inv-f  =  ==refl
-        o-resp-≈  {c₁}  {c₂} {t1} {t0} {t0} {f} {g} {h} {i}  (just refl) (just refl) | just inv-f | just inv-f | just id-t0  | just id-t0   =  ==refl
-        o-resp-≈  {c₁}  {c₂} {t1} {t0} {t1} {f} {g} {h} {i}  (just refl) (just refl) | just inv-f | just inv-f | just arrow-f  | just arrow-f   =  ==refl
-        o-resp-≈  {c₁}  {c₂} {t1} {t0} {t1} {f} {g} {h} {i}  (just refl) (just refl) | just inv-f | just inv-f | just arrow-g  | just arrow-g   =  ==refl
-        o-resp-≈  {c₁}  {c₂} {t0} {t1} {t0} {f} {g} {h} {i}  (just refl) (just refl) | just arrow-f | just arrow-f | just inv-f  | just inv-f   =  ==refl
-        o-resp-≈  {c₁}  {c₂} {t0} {t1} {t0} {f} {g} {h} {i}  (just refl) (just refl) | just arrow-g | just arrow-g | just inv-f  | just inv-f   =  ==refl
---        o-resp-≈  {c₁}  {c₂} {a} {b} {c} {f} {g} {h} {i}  (just refl) (just refl) | just jf | just .jf | just jh  | just .jh   =  
---          let open  ==-Reasoning {c₁} {c₂ } in begin
---                   {!!}
---                ==⟨ {!!} ⟩
---                   {!!}
---                ∎
+        o-resp-≈  {c₁}  {c₂} {a} {b} {c} {f} {g} {h} {i}  f==g h==i  = 
+          let open  ==-Reasoning {c₁} {c₂ } in begin
+                    hom ( h × f )
+                ==⟨⟩
+                    comp (hom h) (hom f)
+                ==⟨ ==cong (\ x  -> comp ( hom h ) x )  f==g ⟩
+                    comp (hom h) (hom g)
+                ==⟨ ==cong (\ x  -> comp x ( hom g ) )  h==i ⟩
+                    comp (hom i) (hom g)
+                ==⟨⟩
+                    hom ( i × g )
+                ∎