Mercurial > hg > Members > kono > Proof > category

changeset 652:236e916760e6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
rewritw solution
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 05 Jul 2017 09:39:58 +0900
parents 1503af5d7440
children 893ae9a95ee1
files freyd2.agda
diffstat 1 files changed, 12 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/freyd2.agda	Wed Jul 05 07:53:07 2017 +0900
+++ b/freyd2.agda	Wed Jul 05 09:39:58 2017 +0900
@@ -383,16 +383,22 @@
    tmap-η : (y : Obj B)  → Hom B y (FObj U (obj (i y)))
    tmap-η  y = hom (i y) 
 
-   ηf : (a b  : Obj B)  → ( f : Hom B a b ) → Obj ( K B A a ↓ U)
-   ηf a b f  = record { obj = obj (i b) ; hom = B [ tmap-η b o f ] }
+   sobj  : {a : Obj B} {b : Obj A}  → ( f : Hom B a (FObj U b) ) → CommaObj (K B A a) U 
+   sobj {a} {b} f = record {obj = b; hom =  f } 
+   solution : {a : Obj B} {b : Obj A}  → ( f : Hom B a (FObj U b) ) → CommaHom (K B A a) U (i a) (sobj f)
+   solution {a} {b} f = initial (In a) (sobj f)
 
-   solution : (a b  : Obj B)  → ( f : Hom B a b ) → CommaHom (K B A a) U (i a) (ηf a b f )
-   solution a b f =  initial (In a) (ηf a b f )
+   univ : (a : Obj B) (b : Obj A)  → (f : Hom B a (FObj U b))
+       → B [ B [ FMap U (arrow (solution f)) o tmap-η a ]  ≈ f ]
+   univ = {!!}
+
+   ηf : (a b  : Obj B)  → ( f : Hom B a b ) → Obj ( K B A a ↓ U)
+   ηf a b f  = sobj ( B [ tmap-η b o f ]  )
 
    F : Functor B A
    F = record {
     FObj = λ b →  obj (i b) 
-    ; FMap = λ {x} {y} (f : Hom B x y ) → arrow (solution x y f)
+    ; FMap = λ {x} {y} (f : Hom B x y ) → arrow (solution ( B [ tmap-η y o f ]  ))
     ; isFunctor = record {
              identity =  identity1
            ; distr = distr1 
@@ -432,8 +438,7 @@
 
    nat-ε : NTrans A A (F  ○ U) identityFunctor
    nat-ε  = record {
-         TMap = λ x → arrow (initial (In (FObj U x)) (record { obj = x ; hom = id1 B (FObj U x) }))
-         --     why we cannot write this using solution? should be *(id B) 
+         TMap = λ x → arrow ( solution (id1 B (FObj U x)))
          ; isNTrans = record { commute = comm1 } } where
         comm1 : {a b : Obj A} {f : Hom A a b} →
                 A [ A [ FMap (identityFunctor {_} {_} {_} {A}) f o