# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1490692718 -32400
# Node ID 531547cf3b924fef051537dcd78c6815ec9c00f9
# Parent  beac7b0786cbad0eee8ab0653ba0027205fd5c38
fix

diff -r beac7b0786cb -r 531547cf3b92 SetsCompleteness.agda
--- a/SetsCompleteness.agda	Tue Mar 28 18:10:15 2017 +0900
+++ b/SetsCompleteness.agda	Tue Mar 28 18:18:38 2017 +0900
@@ -6,7 +6,6 @@
 module SetsCompleteness where
 
 
-open import HomReasoning
 open import cat-utility
 open import Relation.Binary.Core
 open import Function
@@ -144,7 +143,6 @@
 
 
 open Functor
-open NTrans
 
 record Small  {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ )
                 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
@@ -198,12 +196,18 @@
           proj i prod = iid (  pi1 prod ( small→ s i )  )
           comm1 :  {a b : Obj C} {f : Hom C a b} → Sets [ Sets [ FMap Γ f o Sets [ proj a o e ] ] ≈
                 Sets [ Sets [ proj b o e ] o FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ))) f ] ]
-          comm1 {a} {b} {f} = extensionality Sets  ( λ  x → begin
-                 ? 
-             ≡⟨ {!!}  ⟩
-                {!!}
-             ∎ )  where
-                  open  import  Relation.Binary.PropositionalEquality
-                  open ≡-Reasoning
+          comm1 {a} {b} {f} = begin
+                  Sets [ FMap Γ f o Sets [ proj a o e ]  ]
+              ≈⟨ assoc ⟩
+                  Sets [ Sets [ FMap Γ f o  proj a ] o e   ]
+              ≈⟨ {!!}  ⟩
+                  Sets [ proj b o e ] 
+              ≈↑⟨ idR  ⟩
+                  Sets [ Sets [ proj b o e ] o id1 Sets a0 ]
+              ≈⟨⟩
+                  Sets [ Sets [ proj b o e ] o FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ))) f ] 
+             ∎   where
+                  open import HomReasoning
+                  open  ≈-Reasoning Sets