# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1490524904 -32400
# Node ID 8fd030f9f57247b7c179b4e1323d7c8f913fa77b
# Parent  00bf9eca0db71e3ae6b709f4c979dcb886ebcc44
Equalizer in Sets done

diff -r 00bf9eca0db7 -r 8fd030f9f572 SetsCompleteness.agda
--- a/SetsCompleteness.agda	Wed Mar 22 17:48:22 2017 +0900
+++ b/SetsCompleteness.agda	Sun Mar 26 19:41:44 2017 +0900
@@ -93,6 +93,7 @@
         --    |  . h
         --y : d
 
+        -- cf. https://github.com/danr/Agda-projects/blob/master/Category-Theory/Equalizer.agda
 
 data sequ {c : Level} (A B : Set c) ( f g : A → B ) :  Set c where
     elem : (x : A ) → (eq : f x ≡ g x) → sequ A B f g
@@ -124,62 +125,22 @@
            fhy=ghy {d} {h} {y} fh=gh = ≡cong ( λ f → f y ) fh=gh
            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} → {h' : Hom Sets d a} →　Sets [ h  ≈ h' ] 
-             → (fh=gh : Sets [ Sets [ f o h ] ≈ Sets [ g o 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} {h'} h=h' fh=gh fh'=gh' =  extensionality Sets ( λ y →   begin
-                 k h fh=gh y
-              ≡⟨⟩
-                 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   
-                  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' ] ]
-                ≈⟨   extensionality Sets  ( λ y → fe=ge0 (k' y )  )  ⟩
-                    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 )
-           lemma4 :  {d : Obj Sets } {k' : Hom Sets d (sequ a b f g)} → Sets [ Sets [ f o Sets [ equ o k' ] ] ≈ Sets [ g o Sets [ equ o k' ] ] ]
-           lemma4  {d} {k'} = extensionality Sets ( λ y →  begin
-                 f ( equ ( k' y ) )
-              ≡⟨ ≡cong ( λ e → e ( k' y)  ) fe=ge  ⟩
-                 g ( equ ( k' y ) )
-              ∎ ) where
-                  open  import  Relation.Binary.PropositionalEquality
-                  open ≡-Reasoning
+           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' )
+           lemma1 :  { c₂ : Level  } {a b  : Obj (Sets { c₂})} {f g : Hom Sets a b} →
+                Sets [ f ≈ g ] → (x : a ) → f x  ≡ g x
+           lemma1 refl  x  = refl
+           lemma5 :   {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 ] → (x : d ) → equ (k h fh=gh x) ≡ equ (k' x)
+           lemma5 refl  x  = refl   -- somehow this is not equal to lemma1
            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 =  begin
-                 k h fh=gh
-              ≈↑⟨ k-cong  ek'=h (lemma4 {d}  ) (lemma3 {d} ) ⟩
-                 Sets [ ( λ e → elem  (equ e) (fe=ge0 e ))  o  k'  ]
-              ≈⟨ car  (lemma2  )  ⟩
-                 Sets [ ( λ e → e ) o k'  ]
-              ≈⟨⟩
-                 k' 
-              ∎ where
-                  open ≈-Reasoning Sets
-
-
+           uniqueness  {d} {h} {fh=gh} {k'} ek'=h =  extensionality Sets  ( λ ( x : d ) → 
+                 elm-cong ( k h fh=gh x) (  k' x ) (lemma5 {d} {h} {fh=gh} {k'} ek'=h x ) )
 
 open Functor
 open NTrans
 
-
-
 record ΓObj   { c₂ }  ( I   : Set  c₂ )    : Set  c₂ where
    field
      obj :  I