Mercurial > hg > Members > kono > Proof > category

changeset 650:449025d1327f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 04 Jul 2017 11:03:37 +0900
parents 4d742e13fb7c
children 1503af5d7440
files freyd2.agda
diffstat 1 files changed, 25 insertions(+), 26 deletions(-) [+]
line wrap: on
line diff
--- a/freyd2.agda	Tue Jul 04 10:26:38 2017 +0900
+++ b/freyd2.agda	Tue Jul 04 11:03:37 2017 +0900
@@ -375,50 +375,49 @@
 module Adjoint-Functor {c₁ c₂ ℓ : Level} (A B : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) ( comp : Complete A I )
      (U : Functor A B )
      (SFS : (b : Obj B) → SmallFullSubcategory ((K B A b) ↓ U) )  
-     (PI : (b : Obj B) → PreInitial (K B A b ↓ U)  (SFSF (SFS b))) 
-     ( i : (b : Obj B) → Obj ( K B A b ↓ U) )
-     (In : (b : Obj B) → HasInitialObject ( K B A b ↓ U) (i b) ) 
+     (PI :  (b : Obj B) → PreInitial (K B A b ↓ U)  (SFSF (SFS b))) 
+     ( i :  (b : Obj B) → Obj ( K B A b ↓ U) )
+     (In :  (b : Obj B) → HasInitialObject ( K B A b ↓ U) (i b) ) 
      (LP :  LimitPreserve A I B U  ) where
 
    tmap-η : (y : Obj B)  → Hom B y (FObj U (obj (i y)))
    tmap-η  y = hom (i y) 
 
-   objB : (a b  : Obj B)  → ( f : Hom B a b ) → Obj ( K B A a ↓ U)
-   objB a b f  = record { obj = obj (i b) ; hom = B [ tmap-η b o f ] }
+   η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 ] }
 
-   solution : (a b  : Obj B)  → ( f : Hom B a b ) → CommaHom (K B A a) U (i a) (objB a b f )
-   solution a b f =  initial (In a) (objB a b 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 )
 
    F : Functor B A
    F = record {
     FObj = λ b →  obj (i b) 
-    ; FMap = λ {x} {y} (f : Hom B x y ) → arrow ( initial (In x) (objB x y f)) 
+    ; FMap = λ {x} {y} (f : Hom B x y ) → arrow (solution x y f)
     ; isFunctor = record {
-             identity =  {!!}
-           ; distr = {!!} -- λ {a} {b} {c} {f} {g} → extensionality A ( λ x → lemma-y-obj2 a b c f g x ) ;
-           ; ≈-cong = {!!} -- λ eq → extensionality A ( λ x →  lemma-y-obj3 x eq ) 
+             identity =  identity1
+           ; distr = distr1 
+           ; ≈-cong = cong1
         } 
       }  where
-        identity1 : {a : Obj B} → A [ arrow (initial (In a) (objB a a (id1 B a))) ≈ id1 A (obj (i a)) ]
+        identity1 : {a : Obj B} → A [ arrow (initial (In a) (ηf a a (id1 B a))) ≈ id1 A (obj (i a)) ]
         identity1 = {!!}
         distr1 : {a b c : Obj B} {f : Hom B a b} {g : Hom B b c} →
-                A [ arrow (initial (In a) (objB a c (B [ g o f ]))) ≈
-                A [ arrow (initial (In b) (objB b c g)) o arrow (initial (In a) (objB a b f)) ] ]
+                A [ arrow (initial (In a) (ηf a c (B [ g o f ]))) ≈
+                A [ arrow (initial (In b) (ηf b c g)) o arrow (initial (In a) (ηf a b f)) ] ]
         distr1 = {!!}
         cong1  : {a : Obj B} {b : Obj B} {f g : Hom B a b} →
-          B [ f ≈ g ] → A [ arrow (initial (In a) (objB a b f)) ≈
-           arrow (initial (In a) (objB a b g)) ]
+          B [ f ≈ g ] → A [ arrow (initial (In a) (ηf a b f)) ≈ arrow (initial (In a) (ηf a b g)) ]
         cong1  = {!!}
 
-   nat-ε : NTrans A A ( F  ○ U ) identityFunctor
+   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) }))
-         ; isNTrans = record { commute = {!!} } } where
+         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) 
+         ; isNTrans = record { commute = comm1 } } where
         comm1 : {a b : Obj A} {f : Hom A a b} →
                 A [ A [ FMap (identityFunctor {_} {_} {_} {A}) f o
                     arrow (initial (In (FObj U a)) (record { obj = a ; hom = id1 B (FObj U a) })) ]
-                ≈ A [ arrow (initial (In (FObj U b)) (record { obj = b ; hom = id1 B (FObj U b) }))
-                    o FMap (F ○ U) f ] ]
+              ≈ A [ arrow (initial (In (FObj U b)) (record { obj = b ; hom = id1 B (FObj U b) })) o FMap (F ○ U) f ] ]
         comm1 = {!!}
 
    nat-η : NTrans B B identityFunctor (U ○ F)
@@ -429,9 +428,9 @@
        comm1 {a} {b} {f} = let open ≈-Reasoning B in begin
                FMap (U ○ F) f o tmap-η a 
              ≈⟨⟩
-               FMap U ( arrow ( initial (In a) (objB a b f ))) o hom ( i a )
-             ≈⟨ comm ( initial (In a) (objB a b f)) ⟩
-               ( tmap-η b o f ) o FMap (K B A a) (arrow (initial (In a) (objB a b f)))    
+               FMap U ( arrow ( initial (In a) (ηf a b f ))) o hom ( i a )
+             ≈⟨ comm ( initial (In a) (ηf a b f)) ⟩
+               ( tmap-η b o f ) o FMap (K B A a) (arrow (initial (In a) (ηf a b f)))    
              ≈⟨ idR ⟩
                hom (i b ) o f 
              ≈⟨⟩
@@ -440,8 +439,8 @@
 
    FisLeftAdjoint  : Adjunction B A U F nat-η nat-ε 
    FisLeftAdjoint  = record { isAdjunction = record {
-         adjoint1 = {!!}
-       ; adjoint2 = {!!}
+         adjoint1 = adjoint1
+       ; adjoint2 = adjoint2
     } } where
        adjoint1 : {b : Obj A} → B [ B [ FMap U (TMap nat-ε b) o TMap nat-η (FObj U b) ] ≈ id1 B (FObj U b) ]
        adjoint1 = {!!}