Mercurial > hg > Members > kono > Proof > category

changeset 807:91a2efb67462

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
termination on fmap failed
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 26 Apr 2019 18:24:07 +0900
parents dd0d0a201990
children e4cc2ccd0f06
files CCChom.agda
diffstat 1 files changed, 27 insertions(+), 19 deletions(-) [+]
line wrap: on
line diff
--- a/CCChom.agda	Fri Apr 26 16:54:18 2019 +0900
+++ b/CCChom.agda	Fri Apr 26 18:24:07 2019 +0900
@@ -631,16 +631,24 @@
    fobj {G} (a ∧ b) = (fobj {G} a ) /\ (fobj {G} b )
    fobj {G} (a <= b) = fobj {G} b → fobj {G} a
    fobj ⊤ = One'
-   {-# TERMINATING #-}
+   -- {-# TERMINATING #-}
    fmap : {G : SM} { a b : Obj (DX G) } → Hom (DX G) a b → fobj {G} a → fobj {G} b
    fmap {G} {a} {a} (id a) = λ z → z
-   fmap {G} {a} {(atom b)} (next (arrow x) f) = λ z → smap G x ( fmap f z )
+   fmap {G} {a} {(atom b)} (next {a} {c} (arrow x) f) = λ z → smap G x ( k z ) where
+       k : fobj a → fobj {G} c 
+       k z = fmap f z
    fmap {G} {a} {b} (next (id b) f) = fmap f
    fmap {G} {a} {⊤} (next (○ b) f) = λ _ → OneObj'
-   fmap {G} {a} {b} (next {a} {.b ∧ y} {b} π f) = λ z → proj₁ ( fmap f z )
-   fmap {G} {a} {b} (next π' f) =  λ z → proj₂ ( fmap f z )
-   fmap {G} {a} {b} (next ε f) =  λ z → (  proj₁ (fmap f z) )(  proj₂ (fmap f z) )
-   fmap {G} {a} {b} (next (f ・ g) h) =  λ z →  fmap (next f (next g h)) z
+   fmap {G} {a} {b} (next {a} {x ∧ y} {b} π f) = λ z → proj₁ ( k z ) where
+       k : fobj a → fobj x /\ fobj y  
+       k z = fmap f z
+   fmap {G} {a} {b} (next {.a} {x ∧ y} π' f) =  λ z → proj₂ ( k z ) where
+       k : fobj a → fobj x /\ fobj y  
+       k z = fmap f z
+   fmap {G} {a} {b} (next {.a} {(x <= y) ∧ y} {.b} ε f) =  λ z → (  proj₁ (k z))(  proj₂ (k z)) where
+       k :  fobj a →  (fobj y → fobj x) /\ fobj y
+       k z = fmap f z
+   fmap {G} {a} {b} (next {.a} {c} (_・_ {c} {d} {b} f g) h) =  λ z → fmap ( next f (id d)) ( fmap (next g (id c )) ( fmap h z ))
    fmap {G} {a} {(_ ∧ _)} (next < f , g > h) = λ z → ( fmap (next f h) z ,  fmap (next g h) z)
    fmap {G} {a} {(c <= b)} (next {_} {d} (f *) g ) = λ x y → fmap (next f (id (d ∧ b))) ( fmap g x , y )
 
@@ -650,32 +658,32 @@
    isFunctor (CS {G}) = isf where
        _++_ = Category._o_ (DX G)
        distrCS : {a b c : Obj (DX G)}  { f : Hom (DX G) a b } { g : Hom (DX G) b c } → Sets [ fmap ((DX G) [ g o f ]) ≈ Sets [ fmap g o fmap f ] ]
-       distrCS {a} {.a} {.a} {id a} {id .a} = refl
+       distrCS {a} {.a} {.a} {id a} {id .a} = {!!}
        distrCS {a} {.a} {c} {id a} {next x g} = begin
              fmap (DX G [ next x g o Chain.id a ])
           ≈⟨⟩
              fmap ( next x ( g ++ (Chain.id a)))
           ≈⟨ extensionality Sets ( λ y → cong ( λ k → fmap ( next x k ) y ) (idR1 (DX G)) ) ⟩
              fmap ( next x  g )
-          ≈↑⟨ idL ⟩
+          ≈↑⟨ {!!} ⟩
              Sets [ fmap (next x g) o fmap (Chain.id a) ]
           ∎  where open ≈-Reasoning Sets
-       distrCS {a} {b} {b} {f} {id b} = refl
-       distrCS {a} {b} {atom z} {f} {next (arrow x) g} = distrCS 
-       distrCS {a} {b} {c} {f} {next (id c) g} = distrCS 
+       distrCS {a} {b} {b} {f} {id b} =  {!!}
+       distrCS {a} {b} {atom z} {f} {next {.b} {atom y} {atom z} (arrow x) g} = {!!}
+       distrCS {a} {b} {c} {f} {next (id c) g} =  {!!}
        distrCS {a} {b} {.⊤} {f} {next (○ a₁) g} = begin
              fmap (DX G [ next (○ a₁) g o f ])
-          ≈⟨ extensionality Sets ( λ x → refl ) ⟩
+          ≈⟨ {!!} ⟩
              Sets [ fmap (next (○ a₁) g) o fmap f ]
           ∎  where open ≈-Reasoning Sets
-       distrCS {a} {b} {c} {f} {next {.b} {c ∧ x} {c} π g} = distrCS
-       distrCS {a} {b} {c} {f} {next π' g} = distrCS
-       distrCS {a} {b} {c} {f} {next ε g} = distrCS
-       distrCS {a} {b} {.(_ ∧ _)} {f} {next < x , x₁ > g} = distrCS
-       distrCS {a} {b} {c} {f} {next (x ・ y) g} = distrCS
-       distrCS {a} {b} {.(_ <= _)} {f} {next (x *) g} = distrCS
+       distrCS {a} {b} {c} {f} {next {.b} {c ∧ x} {c} π g} = {!!}
+       distrCS {a} {b} {c} {f} {next π' g} = {!!}
+       distrCS {a} {b} {c} {f} {next ε g} = {!!}
+       distrCS {a} {b} {.(_ ∧ _)} {f} {next < x , x₁ > g} = {!!}
+       distrCS {a} {b} {c} {f} {next (x ・ y) g} = {!!}
+       distrCS {a} {b} {.(_ <= _)} {f} {next (x *) g} = {!!}
        isf : IsFunctor (DX G) Sets fobj fmap 
-       IsFunctor.identity isf = extensionality Sets ( λ x → refl )
+       IsFunctor.identity isf = extensionality Sets ( λ x → {!!} )
        IsFunctor.≈-cong isf refl = refl
        IsFunctor.distr isf {a} {b} {c} {g} {f} = distrCS {a} {b} {c} {g} {f}