Mercurial > hg > Members > kono > Proof > category

changeset 649:4d742e13fb7c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
module introdued
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 04 Jul 2017 10:26:38 +0900
parents 10f2057c8bff
children 449025d1327f
files freyd2.agda
diffstat 1 files changed, 33 insertions(+), 91 deletions(-) [+]
line wrap: on
line diff
--- a/freyd2.agda	Tue Jul 04 10:16:07 2017 +0900
+++ b/freyd2.agda	Tue Jul 04 10:26:38 2017 +0900
@@ -380,128 +380,70 @@
      (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) 
+   tmap-η : (y : Obj B)  → Hom B y (FObj U (obj (i y)))
+   tmap-η  y = hom (i y) 
 
-tmap-η : {c₁ c₂ ℓ : Level} (A B : Category c₁ c₂ ℓ)  
-     (U : Functor A B )
-     (i : (b : Obj B) → Obj ( K B A b ↓ U) )
-     (y : Obj B)   → Hom B y (FObj U (obj (i y)))
-tmap-η A B U i y = hom (i y) 
-
-objB : {c₁ c₂ ℓ : Level} (A B : Category c₁ c₂ ℓ)  
-     (U : Functor A B )
-     (i : (b : Obj B) → Obj ( K B A b ↓ U) )
-     (a b  : Obj B)  → ( f : Hom B a b ) → Obj ( K B A a ↓ U)
-objB A B U i a b f  = record { obj = obj (i b) ; hom = B [ tmap-η A B U i b o f ] }
+   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 ] }
 
-solution : {c₁ c₂ ℓ : Level} (A B : Category c₁ c₂ ℓ)  
-     (U : Functor A B )
-     (i : (b : Obj B) → Obj ( K B A b ↓ U) )
-     (In : (b : Obj B) → HasInitialObject ( K B A b ↓ U) (i b) ) 
-     (a b  : Obj B)  → ( f : Hom B a b ) → CommaHom (K B A a) U (i a) (objB A B U i a b f )
-solution A B U i In a b f =  initial (In a) (objB A B U i a b 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 )
 
-FunctorF : {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) ) 
-     (LP :  LimitPreserve A I B U  )
-        → Functor B A
-FunctorF A B I comp U SFS PI i In LP = record {
+   F : Functor B A
+   F = record {
     FObj = λ b →  obj (i b) 
-  ; FMap = λ {x} {y} (f : Hom B x y ) → arrow ( initial (In x) (objB A B U i x y f)) 
-  ; isFunctor = record {
+    ; FMap = λ {x} {y} (f : Hom B x y ) → arrow ( initial (In x) (objB 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 ) 
         } 
-    }  where
-        identity1 : {a : Obj B} → A [ arrow (initial (In a) (objB A B U i a a (Id a))) ≈ Id (obj (i a)) ]
+      }  where
+        identity1 : {a : Obj B} → A [ arrow (initial (In a) (objB 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 B U i a c (B [ g o f ]))) ≈
-                A [ arrow (initial (In b) (objB A B U i b c g)) o arrow (initial (In a) (objB A B U i a b f)) ] ]
+                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)) ] ]
         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 U i a b f)) ≈
-           arrow (initial (In a) (objB A B U i a b g)) ]
+          B [ f ≈ g ] → A [ arrow (initial (In a) (objB a b f)) ≈
+           arrow (initial (In a) (objB a b g)) ]
         cong1  = {!!}
 
-nat-ε : {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) ) 
-     (LP :  LimitPreserve A I B U  )
-        → NTrans A A ( (FunctorF A B I comp U SFS PI i In LP)  ○ U ) identityFunctor
-nat-ε  A B I comp U SFS PI i In LP = 
-      record {
+   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
-        F : Functor B A
-        F = FunctorF A B I comp U SFS PI i In LP
         comm1 : {a b : Obj A} {f : Hom A a b} →
-                A [ A [ FMap identityFunctor f o
+                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 (FunctorF A B I comp U SFS PI i In LP ○ U) f ] ]
+                    o FMap (F ○ U) f ] ]
         comm1 = {!!}
 
-nat-η : {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) ) 
-     (LP :  LimitPreserve A I B U  )
-        → NTrans B B identityFunctor (U ○ (FunctorF A B I comp U SFS PI i In LP) )
-nat-η  A B I comp U SFS PI i In LP = 
-      record { TMap = λ y →  tmap-η A B U i y ; isNTrans = record { commute = comm1 } } where
-       F : Functor B A
-       F = FunctorF A B I comp U SFS PI i In LP
+   nat-η : NTrans B B identityFunctor (U ○ F)
+   nat-η = record { TMap = λ y →  tmap-η y ; isNTrans = record { commute = comm1 } } where
        comm1 : {a b : Obj B} {f : Hom B a b}
-          → B [ B [ FMap (U ○ FunctorF A B I comp U SFS PI i In LP) f o tmap-η A B U i a ]
-                ≈ B [ tmap-η A B U i b o f ] ]
+          → B [ B [ FMap (U ○ F) f o tmap-η a ]
+                ≈ B [ tmap-η b o f ] ]
        comm1 {a} {b} {f} = let open ≈-Reasoning B in begin
-               FMap (U ○ F) f o tmap-η A B U i a 
+               FMap (U ○ F) f o tmap-η a 
              ≈⟨⟩
-               FMap U ( arrow ( initial (In a) (objB A B U i a b f ))) o hom ( i a )
-             ≈⟨ comm ( initial (In a) (objB A B U i a b f)) ⟩
-               ( tmap-η A B U i b o f ) o FMap (K B A a) (arrow (initial (In a) (objB A B U i a b f)))    
+               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)))    
              ≈⟨ idR ⟩
                hom (i b ) o f 
              ≈⟨⟩
-               tmap-η A B U i b o f 
+               tmap-η b o f 
              ∎ 
 
-IsLeftAdjoint  : {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) ) 
-     (LP :  LimitPreserve A I B U  )
-        → Adjunction B A U (FunctorF A B I comp U SFS PI i In LP) 
-            (nat-η A B I comp U SFS PI i In LP) (nat-ε A B I comp U SFS PI i In LP)
-IsLeftAdjoint   A B I comp U SFS PI i In LP = record { isAdjunction = record {
+   FisLeftAdjoint  : Adjunction B A U F nat-η nat-ε 
+   FisLeftAdjoint  = record { isAdjunction = record {
          adjoint1 = {!!}
        ; adjoint2 = {!!}
     } } where
-       F : Functor B A
-       F = FunctorF A B I comp U SFS PI i In LP
-       η :  NTrans B B identityFunctor (U ○ F )
-       η = nat-η A B I comp U SFS PI i In LP
-       ε : NTrans A A ( F ○ U ) identityFunctor
-       ε = nat-ε A B I comp U SFS PI i In LP
-       adjoint1 : {b : Obj A} → B [ B [ FMap U (TMap (nat-ε A B I comp U SFS PI i In LP) b) o
-                TMap (nat-η A B I comp U SFS PI i In LP) (FObj U b) ] ≈ id1 B (FObj U b) ]
+       adjoint1 : {b : Obj A} → B [ B [ FMap U (TMap nat-ε b) o TMap nat-η (FObj U b) ] ≈ id1 B (FObj U b) ]
        adjoint1 = {!!}
-       adjoint2 : {a : Obj B} → A [ A [ TMap (nat-ε A B I comp U SFS PI i In LP)
-                (FObj (FunctorF A B I comp U SFS PI i In LP) a)
-                o FMap (FunctorF A B I comp U SFS PI i In LP) (TMap (nat-η A B I comp U SFS PI i In LP) a) ]
-                ≈ id1 A (FObj (FunctorF A B I comp U SFS PI i In LP) a) ]
+       adjoint2 : {a : Obj B} → A [ A [ TMap nat-ε (FObj F a) o FMap F (TMap nat-η a) ] ≈ id1 A (FObj F a) ]
        adjoint2 = {!!}