Mercurial > hg > Members > kono > Proof > category

changeset 645:5f26af3f1c00

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
start adjoint
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 03 Jul 2017 16:40:34 +0900
parents 8e35703ef116
children 4e0f0105a85d
files freyd2.agda
diffstat 1 files changed, 34 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/freyd2.agda	Mon Jul 03 15:35:28 2017 +0900
+++ b/freyd2.agda	Mon Jul 03 16:40:34 2017 +0900
@@ -374,3 +374,37 @@
              ∎  ) ) where
                   open  import  Relation.Binary.PropositionalEquality
                   open ≡-Reasoning
+
+
+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))) 
+     (LP :  LimitPreserve A I B U  )
+        → Functor B A
+FunctorF = {!!}  
+
+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))) 
+     (LP :  LimitPreserve A I B U  )
+        → NTrans A A ( (FunctorF A B I comp U SFS PI LP)  ○ U ) identityFunctor
+nat-ε = {!!}
+
+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))) 
+     (LP :  LimitPreserve A I B U  )
+        → NTrans B B identityFunctor (U ○ (FunctorF A B I comp U SFS PI LP) )
+nat-η = {!!}
+
+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))) 
+     (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  = {!!}