--- a/freyd2.agda	Thu Jul 06 12:22:54 2017 +0900
+++ b/freyd2.agda	Thu Jul 06 13:50:45 2017 +0900
@@ -502,9 +502,12 @@
              ≈⟨ car (distr U) ⟩
                  ( FMap U (FMap (identityFunctor {_} {_} {_} {A}) f) o FMap U (arrow (initial (In (FObj U a))
                     (record { obj = a ; hom = id1 B (FObj U a) })))) o (tmap-η (FObj U a))
-             ≈⟨ {!!} ⟩
-                FMap U f 
-             ≈↑⟨ idR ⟩
+             ≈↑⟨ assoc ⟩
+                 FMap U (FMap (identityFunctor {_} {_} {_} {A}) f) o (FMap U (arrow (initial (In (FObj U a))
+                    (record { obj = a ; hom = id1 B (FObj U a) }))) o tmap-η (FObj U a) )
+             ≈⟨ cdr ( univ (id1 B (FObj U a))) ⟩
+                 FMap U (FMap (identityFunctor {_} {_} {_} {A}) f) o id1 B (FObj U a)
+             ≈⟨⟩
                 FMap U f o id1 B (FObj U a) 
              ∎  
         lemma-nat2 : {a b : Obj A} {f : Hom A a b} →
@@ -514,7 +517,23 @@
         lemma-nat2 {a} {b} {f} = let open ≈-Reasoning B in begin
                  FMap U (A [ arrow (initial (In (FObj U b))
                   (record { obj = b ; hom = id1 B (FObj U b) })) o FMap (F ○ U) f ] ) o tmap-η (FObj U a) 
-             ≈⟨ {!!} ⟩
+             ≈⟨ car (distr U) ⟩
+                 ( FMap U (arrow (initial (In (FObj U b)) (record { obj = b ; hom = id1 B (FObj U b) })))
+                    o FMap U ( FMap (F ○ U) f ))  o tmap-η (FObj U a) 
+             ≈↑⟨ assoc ⟩
+                 FMap U (arrow (initial (In (FObj U b)) (record { obj = b ; hom = id1 B (FObj U b) })))
+                    o ( FMap U ( FMap (F ○ U) f )  o tmap-η (FObj U a)  )
+             ≈⟨ cdr ( univ ( tmap-η (FObj U b) o FMap U f ) ) ⟩
+                 FMap U (arrow (initial (In (FObj U b)) (record { obj = b ; hom = id1 B (FObj U b) })))
+                    o  ( tmap-η (FObj U b) o FMap U f )
+             ≈⟨ assoc ⟩
+                 ( FMap U (arrow (initial (In (FObj U b)) (record { obj = b ; hom = id1 B (FObj U b) })))
+                    o  tmap-η (FObj U b) ) o FMap U f 
+             ≈⟨ car (univ (id1 B (FObj U b))) ⟩
+                 id1 B (FObj U b) o FMap U f 
+             ≈⟨ idL ⟩
+                 FMap U f 
+             ≈↑⟨ idR ⟩
                  FMap U f o id1 B (FObj U a) 
              ∎  
         comm1 : {a b : Obj A} {f : Hom A a b} →
@@ -551,6 +570,41 @@
        ; 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 = {!!}
+       adjoint1 {b} = let open ≈-Reasoning B in begin
+              FMap U (TMap nat-ε b) o TMap nat-η (FObj U b) 
+             ≈⟨ univ (id1 B (FObj U b))  ⟩
+              id1 B (FObj U b) 
+             ∎
+       adj2comm1 : {a : Obj B} → B [ B [ FMap U (A [ TMap nat-ε (FObj F a) o FMap F (TMap nat-η a) ]) o
+                tmap-η (FObj (identityFunctor {_} {_} {_} {B}) a) ] ≈ tmap-η a ]
+       adj2comm1 {a} = let open ≈-Reasoning B in begin
+               FMap U (A [ TMap nat-ε (FObj F a) o FMap F (TMap nat-η a) ]) o tmap-η a 
+             ≈⟨ car (distr U) ⟩
+               (FMap U (TMap nat-ε (FObj F a)) o FMap U (FMap F (TMap nat-η a) )) o tmap-η a 
+             ≈↑⟨ assoc ⟩
+               FMap U (TMap nat-ε (FObj F a)) o (FMap U (FMap F (TMap nat-η a) ) o tmap-η a )
+             ≈⟨ cdr ( univ (tmap-η  (FObj U (obj (i a))) o tmap-η a )) ⟩
+               FMap U (TMap nat-ε (FObj F a)) o (tmap-η  (FObj U (obj (i a))) o tmap-η a )
+             ≈⟨ assoc ⟩
+               ( FMap U (TMap nat-ε (FObj F a)) o tmap-η (FObj U (obj (i a)))) o tmap-η a 
+             ≈⟨ car (univ (id1 B (FObj U (FObj F a)))) ⟩
+               id1 B (FObj U (FObj F a)) o tmap-η a 
+             ≈⟨ idL ⟩
+               tmap-η a 
+             ∎ 
+       adj2comm2 : {a : Obj B} → B [ B [ FMap U (id1 A (FObj F a)) o tmap-η a ] ≈ tmap-η a ]
+       adj2comm2 {a} = let open ≈-Reasoning B in begin
+               FMap U (id1 A (FObj F a)) o tmap-η a 
+             ≈⟨ car (IsFunctor.identity (isFunctor U)) ⟩
+               id1 B (FObj U (obj (i a))) o tmap-η a 
+             ≈⟨ idL ⟩
+               tmap-η a 
+             ∎ 
        adjoint2 : {a : Obj B} → A [ A [ TMap nat-ε (FObj F a) o FMap F (TMap nat-η a) ] ≈ id1 A (FObj F a) ]
-       adjoint2 = {!!}
+       adjoint2 {a} = let open ≈-Reasoning A in begin
+              TMap nat-ε (FObj F a) o FMap F (TMap nat-η a) 
+             ≈↑⟨ unique adj2comm1 ⟩
+               arrow (solution ( tmap-η a ) )
+             ≈⟨ unique adj2comm2 ⟩
+              id1 A (FObj F a) 
+             ∎