Mercurial > hg > Members > kono > Proof > category

changeset 646:4e0f0105a85d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add adjunction
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 03 Jul 2017 20:53:14 +0900
parents 5f26af3f1c00
children 4d261d04b176
files freyd2.agda
diffstat 1 files changed, 39 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/freyd2.agda	Mon Jul 03 16:40:34 2017 +0900
+++ b/freyd2.agda	Mon Jul 03 20:53:14 2017 +0900
@@ -380,31 +380,62 @@
      (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 = {!!}  
+FunctorF A B I comp U SFS PI i In LP = record {
+    FObj = {!!}
+  ; FMap = {!!}
+  ; 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
 
 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 LP)  ○ U ) identityFunctor
-nat-ε = {!!}
+        → 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 { TMap = λ i → {!!} ; isNTrans = record { commute = {!!} } } where
+       F : Functor B A
+       F = FunctorF A B I comp U SFS PI i In LP
 
 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 LP) )
-nat-η = {!!}
+        → 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 = λ i → {!!} ; isNTrans = record { commute = {!!} } } where
+       F : Functor B A
+       F = FunctorF A B I comp U SFS PI i In LP
 
 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 LP) 
-            (nat-η A B I comp U SFS PI LP) (nat-ε A B I comp U SFS PI LP)
-IsLeftAdjoint  = {!!}
+        → 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 {
+         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