Mercurial > hg > Members > kono > Proof > category

changeset 420:3e44951b9bdb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
refl in free-monoid trouble
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 24 Mar 2016 11:31:14 +0900
parents 8919c162b894
children 06ffcad985ac
files HomReasoning.agda free-monoid.agda limit-to.agda
diffstat 3 files changed, 89 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- a/HomReasoning.agda	Thu Mar 24 02:53:25 2016 +0900
+++ b/HomReasoning.agda	Thu Mar 24 11:31:14 2016 +0900
@@ -87,8 +87,8 @@
 --  ≈-≡ : {a b : Obj A } { x y : Hom A a b } →  (x≈y : x ≈ y ) → x ≡ y
 --  ≈-≡  x≈y = irr x≈y
   ≡-cong : { c₁′ c₂′ ℓ′ : Level}  {B : Category c₁′ c₂′ ℓ′} {x y : Obj B } { a b : Hom B x y } {x' y' : Obj A }  →
-             a ≡ b  → (f : Hom B x y → Hom A x' y' ) →  f a  ≈  f b
-  ≡-cong refl f =  ≡-≈ refl
+             (f : Hom B x y → Hom A x' y' ) →  a ≡ b  → f a  ≈  f b
+  ≡-cong f refl =  ≡-≈ refl
 
 --  cong-≈ :  { c₁′ c₂′ ℓ′ : Level}  {B : Category c₁′ c₂′ ℓ′} {x y : Obj B } { a b : Hom B x y } {x' y' : Obj A }  → 
 --             B [ a ≈ b ] → (f : Hom B x y → Hom A x' y' ) →  f a ≈ f b
--- a/free-monoid.agda	Thu Mar 24 02:53:25 2016 +0900
+++ b/free-monoid.agda	Thu Mar 24 11:31:14 2016 +0900
@@ -118,15 +118,16 @@
                     ; o-resp-≈ =    λ {a} {b} {c} {f} {g} {h} {i} → o-resp-≈ {a} {b} {c} {f} {g} {h} {i}
                     }
      where
-        o-resp-≈ :  {a b c :  ≡-Monoid } {f g : Monomorph a b } → {h i : Monomorph b c } → 
-                          f ==  g → h ==  i → (h + f) ==  (i + g)
-        o-resp-≈  {A} refl refl = refl
         isEquivalence1 : { a b : ≡-Monoid } → IsEquivalence {_} {_} {Monomorph a b}  _==_ 
         isEquivalence1  =      -- this is the same function as A's equivalence but has different types
            record { refl  = refl
              ; sym   = sym
              ; trans = trans
              } 
+        o-resp-≈ :  {a b c :  ≡-Monoid } {f g : Monomorph a b } → {h i : Monomorph b c } → 
+                          f ==  g → h ==  i → (h + f) ==  (i + g)
+        o-resp-≈ refl refl = refl
+
 Monoids : Category _ _ _
 Monoids  =
   record { Obj =  ≡-Monoid 
--- a/limit-to.agda	Thu Mar 24 02:53:25 2016 +0900
+++ b/limit-to.agda	Thu Mar 24 11:31:14 2016 +0900
@@ -40,7 +40,7 @@
 
 open TwoHom
 
-hom :  ∀{ c₁ c₂ }  {  a b : TwoObject  {c₁} } -> 
+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
@@ -90,7 +90,7 @@
 ==refl {_} {_} {_} {_} {just x}  = just refl
 ==refl {_} {_} {_} {_} {nothing} = nothing
 
-==sym :  ∀{  c₁ c₂ a b }   -> ∀ {x y :  Maybe (Arrow  {c₁}  {c₂} t0 t1 a b )} → _==_ x  y → _==_ y  x
+==sym :  ∀{  c₁ c₂ a b }   -> ∀ {x y :  Maybe (Arrow  {c₁}  {c₂} t0 t1 a b )} →  x == y →  y == x
 ==sym (just x≈y) = just (≡-sym x≈y)
 ==sym nothing    = nothing
 
@@ -99,6 +99,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
+
 
 module ==-Reasoning {c₁ c₂ : Level} where
 
@@ -130,6 +134,8 @@
 
 --          f    g    h
 --       d <- c <- b <- a
+--
+--   It can be proved without Arrow constraints
 
 assoc-× :   {c₁  c₂ : Level } {a b c d : TwoObject  {c₁} }
        {f : (TwoHom {c₁}  {c₂ } c d )} →
@@ -270,7 +276,79 @@
         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-≈  {_} {_} {a} {b} {c} {f} {g} {h} {i}  f≡g h≡i  = {!!}
+        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
+--                   {!!}
+--                ==⟨ {!!} ⟩
+--                   {!!}
+--                ∎
+
 
 
 indexFunctor :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( a b : Obj (MaybeCat A )) ( f g : Hom A a b ) ->  Functor (TwoCat {c₁} {c₂} {c₂} ) (MaybeCat A )
@@ -299,7 +377,7 @@
           identity :  {x : Obj I} → MA [ fmap ( id1 I x ) ≈  id1 MA (fobj x) ]
           identity {t0}  =  refl-hom
           identity {t1}  =  refl-hom
-          distr1 : {a₁ : Obj I} {b₁ : Obj I} {c : Obj I} {f₁ : Hom I a₁ b₁} {g₁ : Hom I b₁ c} → 
+          distr1 : {a₁ : Obj I} {b₁ : Obj I} {c : Obj I} {f₁ : Hom I a₁ b₁} {g₁ : Hom I b₁ c} →
                MA [ fmap (I [ g₁ o f₁ ])  ≈  MA [ fmap g₁ o fmap f₁ ] ]
           distr1 {a1} {b1} {c1} {f1} {g1}   with hom g1 | hom f1
           distr1 {t0} {t0} {t0} {f1} {g1} | nothing | nothing   =  nothing
@@ -366,7 +444,7 @@
           ≈-cong   {t1} {t0} {f1} {g1} f≈g | just inv-f | just inv-f = refl-hom
           ≈-cong   {t0} {t1} {f1} {g1} f≈g | just arrow-f | just arrow-g = begin
                      {!!}
-                 ≈⟨ {!!} ⟩ 
+                 ≈⟨ {!!} ⟩
                      {!!}
                  ∎