# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1499130967 -32400
# Node ID 10f2057c8bff8d574806cb67c1c88349610be586
# Parent  4d261d04b176731e92724cb948327f8d63317c53
use module

diff -r 4d261d04b176 -r 10f2057c8bff freyd2.agda
--- a/freyd2.agda	Tue Jul 04 03:39:29 2017 +0900
+++ b/freyd2.agda	Tue Jul 04 10:16:07 2017 +0900
@@ -372,6 +372,17 @@
 -- Adjoint Functor Theorem
 --
 
+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) ) 
+     (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-η : {c₁ c₂ ℓ : Level} (A B : Category c₁ c₂ ℓ)  
      (U : Functor A B )
      (i : (b : Obj B) → Obj ( K B A b ↓ U) )
@@ -408,6 +419,16 @@
            ; ≈-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)) ]
+        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)) ] ]
+        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)) ]
+        cong1  = {!!}
 
 nat-ε : {c₁ c₂ ℓ : Level} (A B : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) ( comp : Complete A I )
      (U : Functor A B )
@@ -418,9 +439,17 @@
      (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 { TMap = λ i → {!!} ; isNTrans = record { commute = {!!} } } where
-       F : Functor B A
-       F = FunctorF A B I comp U SFS PI i In LP
+      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
+                    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 ] ]
+        comm1 = {!!}
 
 nat-η : {c₁ c₂ ℓ : Level} (A B : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) ( comp : Complete A I )
      (U : Functor A B )
@@ -468,3 +497,11 @@
        η = 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 = {!!}
+       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 = {!!}