# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1490149635 -32400
# Node ID 5b4a794f378467f8666137332010ea9ca099c893
# Parent  844328b49d5d76e1a839e30976198d192d5e0974
k-cong done

diff -r 844328b49d5d -r 5b4a794f3784 SetsCompleteness.agda
--- a/SetsCompleteness.agda	Tue Mar 21 16:28:34 2017 +0900
+++ b/SetsCompleteness.agda	Wed Mar 22 11:27:15 2017 +0900
@@ -14,7 +14,7 @@
 -- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g → ( λ x → f x ≡ λ x → g x )
 postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
 
-≡-cong = Relation.Binary.PropositionalEquality.cong 
+≡cong = Relation.Binary.PropositionalEquality.cong 
 
 
 
@@ -75,7 +75,7 @@
        ipcx {q} {qi} {qi'} qi=qi x  = 
               begin
                 record { pi1 = λ i → (qi i) x  }
-             ≡⟨ ≡-cong ( λ QIX → record { pi1 = QIX } ) ( extensionality Sets (λ i → ≡-cong ( λ f → f x )  (qi=qi i)  )) ⟩
+             ≡⟨ ≡cong ( λ QIX → record { pi1 = QIX } ) ( extensionality Sets (λ i → ≡cong ( λ f → f x )  (qi=qi i)  )) ⟩
                 record { pi1 = λ i → (qi' i) x  }
              ∎  where
                   open  import  Relation.Binary.PropositionalEquality 
@@ -117,24 +117,26 @@
            fe=ge  :  Sets [ Sets [ f o (λ e → equ e ) ] ≈ Sets [ g o (λ e → equ e ) ] ]
            fe=ge  =  extensionality Sets (fe=ge0 ) 
            k :  {d : Obj Sets} (h : Hom Sets d a) → Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ] → Hom Sets d (sequ a b f g)
-           k {d} h eq = λ x → elem  (h x) ( cong ( λ y → y x ) eq )
+           k {d} h eq = λ x → elem  (h x) ( ≡cong ( λ y → y x ) eq )
            ek=h : {d : Obj Sets} {h : Hom Sets d a} {eq : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} → Sets [ Sets [ (λ e → equ e )  o k h eq ] ≈ h ]
            ek=h {d} {h} {eq} = refl 
-           fhy=ghy : (d : Obj Sets ) ( h : Hom Sets d a ) (y : d ) →  (fh=gh : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ])  → f (h y) ≡ g (h y)
-           fhy=ghy d h y fh=gh = cong ( λ f → f y ) fh=gh
+           fhy=ghy : {d : Obj Sets } { h : Hom Sets d a } {y : d } →  (fh=gh : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ])  → f (h y) ≡ g (h y)
+           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' = {!!}
+           irr : {d : Set c₂ }  { x y : d } ( eq eq' :  x  ≡ y ) → eq ≡ eq'
+           irr refl refl = refl
+           elm-cong :   {x y : sequ a b f g} → equ x ≡ equ y →  x  ≡ y
+           elm-cong { elem x eq  } {elem .x eq' } refl   =  ≡cong ( λ ee → elem x ee ) ( irr 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' )
+                 elem (h  y) ( fhy=ghy fh=gh )
+              ≡⟨  elm-cong  ( ≡cong ( λ h  → h y ) h=h') ⟩
+                 elem (h' y) ( fhy=ghy fh'=gh' )
               ≡⟨⟩
                  k h' fh'=gh' y
               ∎ ) where   
@@ -144,11 +146,7 @@
                  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  ⟩
+                ≈⟨   extensionality Sets  ( λ y → fe=ge0 (k' y )  )  ⟩
                     Sets [ g o Sets [ (λ e → equ e) o k' ] ]
                 ∎ where
                   open ≈-Reasoning Sets
@@ -161,10 +159,10 @@
            uniqueness  {d} {h} {fh=gh} {k'} ek'=h =  begin
                  k h fh=gh
               ≈↑⟨ k-cong ek'=h ⟩
-                 k ( Sets [  (λ e → equ e)  o k' ]  ) ( lemma3 {d} {k'} )
+                 k ( Sets [  (λ e → equ e)  o k' ]  ) {!!}
               ≈⟨⟩
                  Sets [ ( λ e → elem  (equ e) (fe=ge0 e ))  o  k'  ]
-              ≈⟨ car ( lemma2 {{!!}} ) ⟩
+              ≈⟨ car  lemma2  ⟩
                  Sets [ ( λ e → e ) o k'  ]
               ≈⟨⟩
                  k'