Mercurial > hg > Members > kono > Proof > category

changeset 412:f04b2fb91432

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
recover TwoHom
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 23 Mar 2016 15:45:05 +0900
parents 33958fdfc77e
children e08af559efb9
files limit-to.agda
diffstat 1 files changed, 44 insertions(+), 74 deletions(-) [+]
line wrap: on
line diff
--- a/limit-to.agda	Wed Mar 23 11:29:45 2016 +0900
+++ b/limit-to.agda	Wed Mar 23 15:45:05 2016 +0900
@@ -27,59 +27,64 @@
    t0 : TwoObject 
    t1 : TwoObject 
 
+record TwoHom {c₁ c₂ : Level}  (a : TwoObject {c₁}  ) (b : TwoObject {c₁}  ) : Set   c₂ where
+   field
+       Map    : TwoObject  {c₂ }
+
 
 -- arrow composition
 
 
-_×_ :  ∀ { c₁  c₂ }  -> {A B C : TwoObject { c₁} } →  Maybe ( TwoObject   { c₂ }) →  Maybe ( TwoObject    { c₂ })  →  Maybe ( TwoObject  { c₂ })  
+_×_ :  ∀ {c₁  c₂}  -> {a b c : TwoObject {c₁}} →  Maybe ( TwoHom {c₁}  {c₂} b c ) →  Maybe ( TwoHom {c₁} {c₂} a b )  →  Maybe ( TwoHom {c₁}  {c₂} a c )
 _×_   nothing _  = nothing
 _×_   (just _) nothing  = nothing
-_×_   { c₁} { c₂} {t1} {t1} {t1} _ 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₂} {a} {b} {c} (just f)  (just g)   =  nothing
+_×_   {c₁} {c₂} {t1} {t1} {t1} _ 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₂} {a} {b} {c} (just f)  (just g)   =  nothing
 
 
-_==_ :  ∀{ c₂ }  ->  Rel (Maybe (TwoObject  { c₂ })) (c₂) 
+_==_ :  ∀{c₁ c₂ }  { a b : TwoObject  {c₁} } ->  Rel (Maybe (TwoHom {c₁}  {c₂ } a b )) (c₂) 
 _==_   =  Eq   _≡_ 
 
-==refl :  ∀{ c₂ } ->  ∀ {x : Maybe (TwoObject  { c₂ })} → _==_ x x
-==refl {_} {just x}  = just refl
-==refl {_} {nothing} = nothing
+==refl :  ∀{ c₁ c₂ } { a b : TwoObject  {c₁} } ->  ∀ {x : Maybe (TwoHom {c₁}  {c₂ } a b )} → x == x 
+==refl {_} {_} {_} {_} {just x}  = just refl
+==refl {_} {_} {_} {_} {nothing} = nothing
 
-==sym :  ∀{ c₂ } -> ∀ {x y :  Maybe (TwoObject  { c₂ })} → _==_ x  y → _==_ y  x
+==sym :  ∀{ c₁ c₂ }  { a b : TwoObject  {c₁} } -> ∀ {x y :  Maybe (TwoHom {c₁}  {c₂ } a b  )} → _==_ x  y → _==_ y  x
 ==sym (just x≈y) = just (≡-sym x≈y)
 ==sym nothing    = nothing
 
-==trans :  ∀{ c₂ } -> ∀ {x y z :   Maybe (TwoObject  { c₂ }) } → _==_ x  y → _==_ y  z → _==_ x  z
+==trans :  ∀{ c₁ c₂ }  { a b : TwoObject  {c₁} } -> ∀ {x y z :   Maybe (TwoHom {c₁}  {c₂ } a b  ) } → 
+         x == y → y == z  → x == z
 ==trans (just x≈y) (just y≈z) = just (≡-trans x≈y y≈z)
 ==trans nothing    nothing    = nothing
 
-module ==-Reasoning { c₁ c₂ : Level} where
+module ==-Reasoning {c₁ c₂ : Level} where
 
         infixr  2 _∎
         infixr 2 _==⟨_⟩_ _==⟨⟩_
         infix  1 begin_
 
 
-        data _IsRelatedTo_   (x y : (Maybe (TwoObject  { c₂ }))) :
+        data _IsRelatedTo_  { a b : TwoObject  {c₁} }   (x y : (Maybe (TwoHom {c₁}  {c₂ } a b ))) :
                              Set  c₂ where
             relTo : (x≈y : x  == y  ) → x IsRelatedTo y
 
-        begin_ :  {x : Maybe (TwoObject  { c₂ }) } {y : Maybe (TwoObject  { c₂ })} →
+        begin_ :  { a b : TwoObject  {c₁} } {x : Maybe (TwoHom {c₁}  {c₂ } a b ) } {y : Maybe (TwoHom {c₁}  {c₂ } a b )} →
                    x IsRelatedTo y →  x ==  y 
         begin relTo x≈y = x≈y
 
-        _==⟨_⟩_ :  (x :  Maybe (TwoObject  { c₂ })) {y z :  Maybe (TwoObject  { c₂ }) } →
+        _==⟨_⟩_ :  { a b : TwoObject  {c₁} } (x :  Maybe (TwoHom {c₁}  {c₂ } a b )) {y z :  Maybe (TwoHom {c₁}  {c₂ } a b ) } →
                     x == y  → y IsRelatedTo z → x IsRelatedTo z
         _ ==⟨ x≈y ⟩ relTo y≈z = relTo (==trans x≈y y≈z)
 
-        _==⟨⟩_ :  (x : Maybe (TwoObject  { c₂ })) {y : Maybe (TwoObject  { c₂ })} 
+        _==⟨⟩_ :   { a b : TwoObject  {c₁} }(x : Maybe (TwoHom {c₁}  {c₂ } a b )) {y : Maybe (TwoHom {c₁}  {c₂ } a b )} 
                     → x IsRelatedTo y → x IsRelatedTo y
         _ ==⟨⟩ x≈y = x≈y
 
-        _∎ :  (x :  Maybe (TwoObject  { c₂ })) → x IsRelatedTo x
+        _∎ :   { a b : TwoObject  {c₁} }(x :  Maybe (TwoHom {c₁}  {c₂ } a b )) → x IsRelatedTo x
         _∎ _ = relTo ==refl
 
 
@@ -87,70 +92,39 @@
 --          f    g    h
 --       d <- c <- b <- a
 
-assoc-× :   { c₁  c₂ : Level } {a b c d : TwoObject  { c₁} } {f g h : Maybe (TwoObject  { c₂ })} → 
-      (  _×_ { c₁} { c₂} {a} {b} {d} f ( _×_ { c₁} { c₂} {a} {b} {c} g h )  ) ==
-                (  _×_ { c₁} { c₂} {a} {c} {d}  ( _×_ { c₁} { c₂} {b} {c} {d} f g )   h )
---    ( f × (g × h)) == ((f × g) × h )
+assoc-× :   {c₁  c₂ : Level } {a b c d : TwoObject  {c₁} } 
+       {f : Maybe (TwoHom {c₁}  {c₂ } c d )} → 
+       {g : Maybe (TwoHom {c₁}  {c₂ } b c )} → 
+       {h : Maybe (TwoHom {c₁}  {c₂ } a b )} → 
+       ( f × (g × h)) == ((f × g) × h )
 assoc-× {_} {_} {_} {_} {_} {_} {nothing} {_} {_} = nothing
 assoc-× {_} {_} {_} {_} {_} {_} {just _} {nothing} {_} = nothing
-assoc-× {_} {_} {t0} {t0} {t0} {t0} {just _} {just _} {nothing} = nothing
-assoc-× {_} {_} {t0} {t0} {t0} {t1} {just _} {just _} {nothing} = nothing
-assoc-× {_} {_} {t0} {t0} {t1} {t0} {just _} {just _} {nothing} = nothing
-assoc-× {_} {_} {t0} {t0} {t1} {t1} {just _} {just _} {nothing} = nothing
-assoc-× {_} {_} {t0} {t1} {t0} {t0} {just _} {just _} {nothing} = nothing
-assoc-× {_} {_} {t0} {t1} {t0} {t1} {just _} {just _} {nothing} = nothing
-assoc-× {_} {_} {t0} {t1} {t1} {t0} {just _} {just _} {nothing} = nothing
-assoc-× {_} {_} {t0} {t1} {t1} {t1} {just _} {just _} {nothing} = nothing
-assoc-× {_} {_} {t1} {t0} {t0} {t0} {just _} {just _} {nothing} = nothing
-assoc-× {_} {_} {t1} {t0} {t0} {t1} {just _} {just _} {nothing} = nothing
-assoc-× {_} {_} {t1} {t0} {t1} {t0} {just _} {just _} {nothing} = nothing
-assoc-× {_} {_} {t1} {t0} {t1} {t1} {just _} {just _} {nothing} = nothing
-assoc-× {_} {_} {t1} {t1} {t0} {t0} {just _} {just _} {nothing} = nothing
-assoc-× {_} {_} {t1} {t1} {t0} {t1} {just _} {just _} {nothing} = nothing
-assoc-× {_} {_} {t1} {t1} {t1} {t0} {just _} {just _} {nothing} = nothing
-assoc-× {_} {_} {t1} {t1} {t1} {t1} {just _} {just _} {nothing} = nothing
-assoc-× {_} {_} {t0} {t0} {t0} {t0} {just _} {just _} {just _} = just refl
-assoc-× {_} {_} {t0} {t0} {t0} {t1} {just _} {just _} {just _} = just refl
-assoc-× {_} {_} {t0} {t1} {t1} {t1} {just _} {just _} {just _} = just refl
-assoc-× {_} {_} {t1} {t1} {t1} {t1} {just _} {just _} {just _} = just refl
-assoc-× {_} {_} {t0} {t0} {t1} {t0} {just _} {just _} {just _} =  {!!}
-assoc-× {_} {_} {t0} {t0} {t1} {t1} {just t0} {just t0} {just t0} = just refl
-assoc-× {_} {_} {t0} {t0} {t1} {t1} {just t0} {just t1} {just t0} = just refl
-assoc-× {_} {_} {t0} {t0} {t1} {t1} {just t1} {just t0} {just t1} = just refl
-assoc-× {_} {_} {t0} {t0} {t1} {t1} {just t1} {just t1} {just t1} = just refl
-assoc-× {_} {_} {t0} {t0} {t1} {t1} {just t1} {just t1} {just t0} = {!!}
-assoc-× {_} {_} {t0} {t0} {t1} {t1} {just t1} {just t0} {just t0} = {!!}
-assoc-× {_} {_} {t0} {t0} {t1} {t1} {just t0} {just t1} {just t1} = {!!}
-assoc-× {_} {_} {t0} {t0} {t1} {t1} {just t0} {just t0} {just t1} = {!!}
-assoc-× {_} {_} {t0} {t1} {t0} {t0} {just _} {just _} {just _} = nothing
-assoc-× {_} {_} {t0} {t1} {t0} {t1} {just _} {just _} {just _} = nothing
-assoc-× {_} {_} {t0} {t1} {t1} {t0} {just _} {just _} {just _} = nothing
-assoc-× {_} {_} {t1} {t0} {t0} {t0} {just _} {just _} {just _} = nothing
-assoc-× {_} {_} {t1} {t0} {t0} {t1} {just _} {just _} {just _} = nothing
-assoc-× {_} {_} {t1} {t0} {t1} {t0} {just _} {just _} {just _} = nothing
-assoc-× {_} {_} {t1} {t0} {t1} {t1} {just _} {just _} {just _} = {!!}
-assoc-× {_} {_} {t1} {t1} {t0} {t0} {just _} {just _} {just _} = nothing
-assoc-× {_} {_} {t1} {t1} {t0} {t1} {just _} {just _} {just _} = nothing
-assoc-× {_} {_} {t1} {t1} {t1} {t0} {just _} {just _} {just _} = nothing
+assoc-× {c₁} {c₂} {a} {b} {c} {d} {just f} {just g} {nothing} =  let open ==-Reasoning {c₁} {c₂} in 
+    begin
+        ?
+    ==⟨ ? ⟩ 
+         ?
+    ∎
+assoc-× {_} {_} {_} {_} {_} {_} {just _} {just _} {just _} = ?
 
 
 
 
-TwoId :  { c₁  c₂ : Level } {a : TwoObject  { c₁} } ->  Maybe (TwoObject  { c₂ })
-TwoId {_} {_} {_} = just t0
+TwoId :  {c₁  c₂ : Level } {a : TwoObject  {c₁} } ->  Maybe (TwoHom {c₁}  {c₂ } a a )
+TwoId {_} {_} {_} = just ?
 
 
 open import maybeCat  
 
 
 open import Relation.Binary 
-TwoCat : { c₁ c₂ ℓ : Level  } ->  Category   c₁  c₂  c₂
+TwoCat : {c₁ c₂ ℓ : Level  } ->  Category   c₁  c₂  c₂
 TwoCat   {c₁}  {c₂} {ℓ} = record {
     Obj  = TwoObject  {c₁} ;
-    Hom = λ a b →    Maybe ( TwoObject  { c₂ } ) ;
-    _o_ =  \{a} {b} {c} x y -> _×_ { c₁ } {  c₂} {a} {b} {c} x y ;
+    Hom = λ a b →    Maybe ( TwoHom {c₁}  {c₂ } a b ) ;
+    _o_ =  \{a} {b} {c} x y -> _×_ {c₁ } { c₂} {a} {b} {c} x y ;
     _≈_ =    Eq  _≡_   ;
-    Id  =  \{a} -> TwoId { c₁ } {  c₂} {a} ;
+    Id  =  \{a} -> TwoId {c₁ } { c₂} {a} ;
     isCategory  = record {
             isEquivalence =  record {refl = ==refl ; trans = ==trans ; sym = ==sym } ;
             identityL  = {!!} ;
@@ -176,12 +150,8 @@
           fobj :  Obj I -> Obj A
           fobj t0 = a
           fobj t1 = b
-          fmap :  {x y : Obj I } ->  Maybe (TwoObject  {c₂} ) -> Hom MA (fobj x) (fobj y)
-          fmap {t0} {t1} (just t0) = record { hom = just f }
-          fmap {t0} {t1} (just t1) = record { hom = just g }
-          fmap {t0} {t0} (just t0)  = record { hom = just ( id1 A a )}
-          fmap {t1} {t1} (just t0)  = record { hom = just ( id1 A b )}
-          fmap {_} {_}   _ = record { hom = nothing }
+          fmap :  {x y : Obj I } ->  Maybe (TwoHom {c₁}  {c₂} x y  ) -> Hom MA (fobj x) (fobj y)
+          fmap  = ?
           open ≈-Reasoning (A) 
           identity :  {x : Obj I} → {!!}
           identity {t0}  =  {!!}
@@ -207,7 +177,7 @@
 open Limit
 
 lim-to-equ :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)  ->
-      (lim : (I : Category c₁ c₂ ℓ) ( Γ : Functor I A ) → { a0 : Obj A } { u : NTrans I A ( K A I a0 ) Γ } → Limit A I Γ a0 u ) -- completeness
+      (lim : (I : Category c₁ c₂ ℓ) ( Γ : Functor I A ) → {a0 : Obj A } {u : NTrans I A ( K A I a0 ) Γ } → Limit A I Γ a0 u ) -- completeness
         →  {a b c : Obj A}      (f g : Hom A  a b ) 
         → (e : Hom A c a ) → (fe=ge : A [ A [ f o e ] ≈ A [ g o e ] ] ) → Equalizer A e f g
 lim-to-equ  {c₁} {c₂} {ℓ } A  lim {a} {b} {c}  f g e fe=ge = record {