# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1490081314 -32400
# Node ID 844328b49d5d76e1a839e30976198d192d5e0974
# Parent  52d30ad7f65295f712bf7f54c176dc94d56eae4d
try hom equality in uniquness

diff -r 52d30ad7f652 -r 844328b49d5d SetsCompleteness.agda
--- a/SetsCompleteness.agda	Tue Mar 21 15:15:46 2017 +0900
+++ b/SetsCompleteness.agda	Tue Mar 21 16:28:34 2017 +0900
@@ -124,47 +124,47 @@
            fhy=ghy d h y fh=gh = cong ( λ f → f y ) fh=gh
            xequ :  (x : a  ) → { fx=gx :  f x ≡ g x  } →  sequ a b  f g 
            xequ  x { fx=gx } = elem  x fx=gx
+           elem-cong : {x x' : a } → ( x ≡ x' ) →  ( eq eq' :  f x ≡ g x ) → ( elem x eq )  ≡ ( elem x' eq' )
+           elem-cong refl eq eq' = {!!}
+           k-cong :  {d : Obj Sets} {h : Hom Sets d a} → {fh=gh : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ] } → 
+                {h' : Hom Sets d a} →　Sets [ h  ≈ h' ] → {fh'=gh' : Sets [ Sets [ f o h' ] ≈ Sets [ g o h' ] ] } →   
+                Sets [ k h fh=gh ≈ k h' fh'=gh' ]
+           k-cong {d} {h} {fh=gh} {h'} h=h' {fh'=gh'} =  extensionality Sets ( λ y →   begin
+                 k h fh=gh y
+              ≡⟨⟩
+                 elem (h y) ( fhy=ghy d h y  fh=gh )
+              ≡⟨ {!!}  ⟩
+                 elem (h' y) ( fhy=ghy d h' y  fh'=gh' )
+              ≡⟨⟩
+                 k h' fh'=gh' y
+              ∎ ) where   
+                  open  import  Relation.Binary.PropositionalEquality 
+                  open ≡-Reasoning 
+           lemma3 :  {d : Obj Sets}  {k' : Hom Sets d (sequ a b f g)} →  Sets [ Sets [ f o Sets [ (λ e → equ e) o k' ] ] ≈
+                 Sets [ g o Sets [ (λ e → equ e) o k' ] ] ]
+           lemma3 {d} {k'}  =  begin
+                    Sets [ f o Sets [ (λ e → equ e) o k' ] ]
+                ≈⟨ assoc  ⟩
+                    Sets [ Sets [ f o (λ e → equ e) ] o k'  ]
+                ≈⟨ car {!!} ⟩
+                    Sets [ Sets [ g o (λ e → equ e) ] o k'  ]
+                ≈↑⟨ assoc  ⟩
+                    Sets [ g o Sets [ (λ e → equ e) o k' ] ]
+                ∎ where
+                  open ≈-Reasoning Sets
            lemma1 :  ( e : sequ a b f g ) →  ( z : sequ a b f g ) →  elem (equ z) (fe=ge0 z) ≡ z
            lemma1 ( elem x eq ) (elem x' eq' ) =  refl
            lemma2 :  { e : sequ a b f g } →   ( λ e → elem  (equ e) (fe=ge0 e ) ) ≡ ( λ e → e )
            lemma2 {e} =  extensionality Sets  ( λ z → lemma1 e z )
-           lemma3 :  {d : Obj Sets} (  e : sequ a b f g → a  ) → ( y : d ) → (k' : Hom Sets d (sequ a b f g))   → f ( e (k' y) ) ≡ g ( e (k' y))
-           lemma3 {d} e y k' = {!!}
-           uniquness1 :   {d : Obj Sets} {h : Hom Sets d a} {fh=gh : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} {k' : Hom Sets d (sequ a b f g)} → ( y : d ) →
-                Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → k h fh=gh y ≡ k' y
-           uniquness1 {d} {h} {fh=gh} {k'} y ek'=h = 
-              begin
-                 k h fh=gh y
-              ≡⟨⟩
-                 elem  (h y) (fhy=ghy d h y fh=gh )
-              ≡⟨⟩
-                 xequ  (h y ) {fhy=ghy d h y fh=gh }
-              ≡⟨ sym ( Category.cong (λ ek' → xequ (ek' y ) {{!!}} ) ek'=h )  ⟩
-                 xequ ( ( λ e → equ e ) ( k' y ) ) {fe=ge0 (k' y)}
-              ≡⟨⟩
-                 ( λ e → xequ ( equ e )  {fe=ge0 e } ) ( k' y ) 
-              ≡⟨⟩
-                 ( λ e → elem  (equ e) (fe=ge0 e )) ( k' y ) 
-              ≡⟨ Category.cong ( λ f → f ( k' y ) )  lemma2  ⟩
-                 ( λ e → e ) ( k' y ) 
-              ≡⟨⟩
-                 k' y
-              ∎  
-              where
-                  open  import  Relation.Binary.PropositionalEquality 
-                  open ≡-Reasoning 
            uniqueness :   {d : Obj Sets} {h : Hom Sets d a} {fh=gh : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} {k' : Hom Sets d (sequ a b f g)} →
                 Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → Sets [ k h fh=gh  ≈ k' ]
-           uniqueness  {d} {h} {fh=gh} {k'} ek'=h =  extensionality Sets ( λ y →  uniquness1 {d} {h} {fh=gh}{k'}  y ek'=h   ) 
-           uniqueness0 :   {d : Obj Sets} {h : Hom Sets d a} {fh=gh : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} {k' : Hom Sets d (sequ a b f g)} →
-                Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → Sets [ k h fh=gh  ≈ k' ]
-           uniqueness0  {d} {h} {fh=gh} {k'} ek'=h =  begin
+           uniqueness  {d} {h} {fh=gh} {k'} ek'=h =  begin
                  k h fh=gh
-              ≈⟨ {!!} ⟩
-                 k ( Sets [  (λ e → equ e)  o k' ]  ) {!!}
+              ≈↑⟨ k-cong ek'=h ⟩
+                 k ( Sets [  (λ e → equ e)  o k' ]  ) ( lemma3 {d} {k'} )
               ≈⟨⟩
                  Sets [ ( λ e → elem  (equ e) (fe=ge0 e ))  o  k'  ]
-              ≈⟨ {!!} ⟩
+              ≈⟨ car ( lemma2 {{!!}} ) ⟩
                  Sets [ ( λ e → e ) o k'  ]
               ≈⟨⟩
                  k' 
@@ -191,8 +191,7 @@
 open ΓMap
 
 fmap : { c₂ : Level}   {a b :  Set  c₂ } → (f : a → b  ) → ΓMap f
-fmap {a} {b} f =  record { map = λ aobj →  record { obj = f ( obj aobj ) } }
-
+fmap {a} {b} f =  record { map = λ aobj →  record { obj = f ( obj aobj ) } } 
 Γ :  { c₂ : Level } → Functor  (Sets { c₂}) (Sets { c₂}) 
 Γ { c₂} =   record { FObj =  ΓObj ; FMap = ( λ f →  map (fmap f )) ; isFunctor = record {
          identity =  λ {b} → refl ;