Mercurial > hg > Members > kono > Proof > category

changeset 510:5eb4b69bf541

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
equalizer in Sets , uniquness remains
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 19 Mar 2017 11:14:49 +0900
parents 3e82fb1ce170
children b9c086bda3cc
files SetsCompleteness.agda
diffstat 1 files changed, 47 insertions(+), 18 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Sat Mar 18 17:35:57 2017 +0900
+++ b/SetsCompleteness.agda	Sun Mar 19 11:14:49 2017 +0900
@@ -10,6 +10,13 @@
 open import cat-utility
 open import Relation.Binary.Core
 open import Function
+import Relation.Binary.PropositionalEquality
+-- 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 
+
+
 
 record Σ {a} (A : Set a) (B : Set a) : Set a where
   constructor _,_
@@ -45,13 +52,6 @@
 
 open iproduct
 
-import Relation.Binary.PropositionalEquality
--- 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 
-
-
 SetsIProduct :  {  c₂ : Level} → (I : Obj Sets) (ai : I → Obj Sets ) 
      → IProduct ( Sets  {  c₂} ) I
 SetsIProduct I fi = record {
@@ -59,7 +59,7 @@
        ; iprod = iproduct I fi
        ; pi  = λ i prod  → pi1 prod i
        ; isIProduct = record {
-              iproduct = λ {q} qi x → record { pi1 = λ i → (qi i) x  }
+              iproduct = iproduct1
             ; pif=q = pif=q
             ; ip-uniqueness = ip-uniqueness
             ; ip-cong  = ip-cong
@@ -84,23 +84,52 @@
        ip-cong {q} {qi} {qi'} qi=qi  = extensionality Sets ( ipcx qi=qi )
 
 
+        --
+        --         e             f
+        --    c  -------→ a ---------→ b        f ( f' 
+        --    ^        .     ---------→
+        --    |      .            g
+        --    |k   .
+        --    |  . h
+        --    d
 
 
-SetsEqualizer :  {  c₂ : Level}  →  {a b : Obj (Sets {c₂}) }  (f g : Hom (Sets {c₂}) a b) → Equalizer Sets f g
-SetsEqualizer f g = record { 
-           equalizer-c = {!!} 
-         ; equalizer = {!!}
+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
+
+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 {
-               fe=ge  = {!!}
-             ; k = {!!}
-             ; ek=h = {!!}
-             ; uniqueness  = {!!}
+               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 ) ] ]
+           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 )
+           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 
+           uniqueness :   {d : Obj Sets} {h : Hom Sets d a} {eq : 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 eq  ≈ k' ]
+           uniqueness  {d} refl =  extensionality Sets ( λ x → {!!} )
+
 
 open Functor
 open NTrans
 
+
+
 record ΓObj   { c₂ }  ( I   : Set  c₂ )    : Set  c₂ where
    field
      obj :  I
@@ -138,7 +167,7 @@
 SetsLimit { c₂}  = record { 
            a0 =  Slimit (Obj Sets) {!!} ΓMap
          ; t0 = record { 
-               TMap = λ i → λ lim → s-t0 lim {!!}
+               TMap = λ i → λ lim → s-t0 lim {!!} 
              ; isNTrans = record { commute = {!!} } 
            }
          ; isLimit = record {