Mercurial > hg > Members > kono > Proof > category

changeset 532:d5d7163f2a1d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
equalizer does not fit
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 29 Mar 2017 09:30:22 +0900
parents 66cad3cb3a66
children c3dcea3a92a7
files SetsCompleteness.agda
diffstat 1 files changed, 16 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Tue Mar 28 22:25:07 2017 +0900
+++ b/SetsCompleteness.agda	Wed Mar 29 09:30:22 2017 +0900
@@ -99,21 +99,21 @@
 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
 
+equ  :  {  c₂ : Level}  {a b : Obj (Sets {c₂}) } { f g : Hom (Sets {c₂}) a b } → ( sequ a b  f g ) →  a
+equ  (elem x eq)  = x 
+
 open sequ
 
-SetsEqualizer :  {  c₂ : Level}  →  (a b : Obj (Sets {c₂}) )  (f g : Hom (Sets {c₂}) a b) → Equalizer Sets f g
-SetsEqualizer {c₂} a b f g = record { 
-           equalizer-c = sequ a b f g
-         ; equalizer = λ e → equ e
-         ; isEqualizer = record {
+--           equalizer-c = sequ a b f g
+--          ; equalizer = λ e → equ e
+
+SetsIsEqualizer :  {  c₂ : Level}  →  (a b : Obj (Sets {c₂}) )  (f g : Hom (Sets {c₂}) a b) → IsEqualizer Sets (λ e → equ e )f g
+SetsIsEqualizer {c₂} a b f g = record { 
                fe=ge  = fe=ge
              ; k = k
              ; ek=h = λ {d} {h} {eq} → ek=h {d} {h} {eq}
              ; uniqueness  = uniqueness
-           }
        } where
-           equ  : ( sequ a b  f g ) →  a
-           equ  (elem x eq)  = x 
            fe=ge0  :  (x : sequ a b f g) → (Sets [ f o (λ e → equ e) ]) x ≡ (Sets [ g o (λ e → equ e) ]) x
            fe=ge0 (elem x eq )  =  eq
            fe=ge  :  Sets [ Sets [ f o (λ e → equ e ) ] ≈ Sets [ g o (λ e → equ e ) ] ]
@@ -176,6 +176,7 @@
 open import HomReasoning
 
 open NTrans
+open IsEqualizer
 
 SetsNat : {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( s : Small C I )  ( Γ : Functor C (Sets  {c₁} ) ) 
     → NTrans C Sets (K Sets C (slim  (ΓObj s Γ) (ΓMap s Γ)) ) Γ
@@ -189,12 +190,15 @@
     iid {i} = FMap Γ ( small-iso s ) 
     proj :  (i : Obj C ) → ( prod : iproduct I (λ j → ΓObj s Γ j )) → FObj Γ i
     proj i prod = iid (  pi1 prod ( small→ s i )  )
+    equa : {b : Obj Sets } ( e : slim  (ΓObj s Γ) (ΓMap s Γ) → iproduct I (λ j → ΓObj s Γ j) ) → ( f g : Hom Sets (iproduct I (λ j → ΓObj s Γ j)) b ) → 
+           IsEqualizer Sets e f g
+    equa e f g = {!!}  -- SetsIsEqualizer ? ? ? ?
     comm2 :  {a b : Obj C} {f : Hom C a b} → ( x : slim  (ΓObj s Γ) (ΓMap s Γ) ) → (Sets [ FMap Γ f o Sets [ proj a o e ] ]) x ≡ (Sets [ proj b o e ]) x 
     comm2 {a} {b} {f} x =    begin
         (FMap Γ f ) ( ( proj a o e )  x )
       ≡⟨⟩
         (FMap Γ f ) (  iid ( slim-obj x  (small→ s a) ))
-      ≡⟨ {!!}  ⟩
+      ≡⟨ {!!} ⟩
         iid ( slim-obj x ( small→ s b )  ) 
       ∎   where
           open  import  Relation.Binary.PropositionalEquality
@@ -203,7 +207,9 @@
         Sets [ Sets [ proj b o e ] o FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ))) f ] ]
     comm1 {a} {b} {f} = begin
           Sets [ FMap Γ f o Sets [ proj a o e ]  ]
-        ≈⟨  extensionality Sets  ( λ x →  comm2 x )  ⟩
+        ≈⟨  assoc  ⟩
+          Sets [ Sets [ FMap Γ f o proj a ]  o e  ]
+        ≈⟨ fe=ge  (equa e ( Sets [ FMap Γ f o proj a ] ) (proj b ))  ⟩
           Sets [ proj b o e ] 
         ≈↑⟨ idR  ⟩
           Sets [ Sets [ proj b o e ] o id1 Sets (slim  (ΓObj s Γ) (ΓMap s Γ)) ]