Mercurial > hg > Members > kono > Proof > category

changeset 374:5641b923201e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
limit-to: indexFunctor distribution law cannot be proved
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 06 Mar 2016 12:17:14 +0900
parents 4164586ffdb8
children 5a6db4bc4d9b
files limit-to.agda
diffstat 1 files changed, 25 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/limit-to.agda	Sun Mar 06 02:23:36 2016 +0900
+++ b/limit-to.agda	Sun Mar 06 12:17:14 2016 +0900
@@ -37,7 +37,7 @@
     field
          obj→ : Obj A  -> TwoObject 
          hom→ : {a b : Obj A} -> Hom A a b -> TwoObject
-         f-rev : Hom A b a
+         f-rev : Hom A b a   -- existence of this can be shown using completeness
          feq : A [ A [ f-rev o  f ] ≈  id1 A a ]
          geq : A [ A [ f-rev o  g ] ≈  id1 A a ]
     fobj : Obj A -> Obj A
@@ -57,8 +57,8 @@
          FObj = λ a → fobj two a
        ; FMap = λ f → fmap f
        ; isFunctor = record {
-             identity = {!!} 
-             ; distr = {!!}
+             identity = \{x} -> identity {x}
+             ; distr = \ {a} {b} {c} {f} {g}   -> distr {a} {b} {c} {f} {g} 
              ; ≈-cong = {!!}
        }
       } where
@@ -68,6 +68,27 @@
           ... | t1 | t0 = f-rev two
           ... | t1 | t1 = id1 A b
           ... | t0 | t1  = fmap' two (hom→ two f')
+          identity :  {x : Obj A} → A [ fmap (id1 A  x) ≈ id1 A  (fobj two x) ]
+          identity {x} with obj→ two x
+          ... | t0 = let open ≈-Reasoning (A) in refl-hom
+          ... | t1 = let open ≈-Reasoning (A) in refl-hom
+          distr : {a₁ : Obj A} {b₁ : Obj A} {c : Obj A} {f₁ : Hom A a₁ b₁} {g₁ : Hom A b₁ c} → A [ fmap (A [ g₁ o f₁ ]) ≈ A [ fmap g₁ o fmap f₁ ] ]
+          distr {a₁} {b₁} {c} {f₁} {g₁}  with obj→  two  a₁  | obj→  two  b₁  | obj→  two  c
+          ... | t0 | t0 | t0 = let open ≈-Reasoning (A) in
+              begin
+                 id1 A a
+              ≈↑⟨ idL ⟩
+                 id1 A a  o id1 A a
+              ∎
+          ... | t0 | t0 | t1 = {!!}
+          ... | t0 | t1 | t0 = {!!} 
+          ... | t0 | t1 | t1 = {!!} 
+          ... | t1 | t0 | t0 = {!!}
+          ... | t1 | t0 | t1 = {!!}
+          ... | t1 | t1 | t0 = {!!}
+          ... | t1 | t1 | t1 = {!!}
+          ≈-cong :   {a : Obj A} {b : Obj A} {f : Hom A a b} {g : Hom A a b} → A [ f ≈ g ] → A [ fmap f ≈ fmap g ]
+          ≈-cong {a} {b} {f} {g}  f≈g = let open ≈-Reasoning (A) in ?
 
 open Limit
 
@@ -134,7 +155,7 @@
          k : {d : Obj A}  (h : Hom A d a) → A [ A [ f  o  h ] ≈ A [ g  o h ] ] → Hom A d c
          k {d} h fh=gh  = limit (lim A Γ  {c} {nat c e fe=ge }) d (nat d h fh=gh )
          ek=h :  (d : Obj A ) (h : Hom A d a ) ->  ( fh=gh : A [ A [ f  o  h ] ≈ A [ g  o h ] ] )  -> A [ A [ e o k h fh=gh ] ≈ h ]
-         ek=h d h fh=gh = ?
+         ek=h d h fh=gh = {!!}
          uniquness :  (d : Obj A ) (h : Hom A d a ) ->  ( fh=gh : A [ A [ f  o  h ] ≈ A [ g  o h ] ] )  ->
                  ( k' : Hom A d c )
                 -> A [ A [ e o k' ] ≈ h ] → A [ k h fh=gh ≈ k' ]