Mercurial > hg > Members > kono > Proof > category

changeset 997:d9419216ae0c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 07 Mar 2021 15:51:45 +0900
parents 6cd40df80dec
children 98f412058488
files src/SetsCompleteness.agda src/yoneda.agda
diffstat 2 files changed, 40 insertions(+), 16 deletions(-) [+]
line wrap: on
line diff
--- a/src/SetsCompleteness.agda	Sun Mar 07 11:47:19 2021 +0900
+++ b/src/SetsCompleteness.agda	Sun Mar 07 15:51:45 2021 +0900
@@ -202,29 +202,43 @@
                   open  import  Relation.Binary.PropositionalEquality
                   open ≡-Reasoning
 
-data cequ {c : Level} {A B : Set c} ( f g : A → B )  :   Set c where
-    celem : (b : B)  → (a : A) → f a ≡  b → g a ≡ b →  cequ f g 
+equc  :  {  c₂ : Level}  {a b : Obj (Sets {c₂}) } ( f g : Hom (Sets {c₂}) a b ) → Hom Sets b ({y : a} → f y ≡ g y → sequ a b f g )
+equc {_} {a} {b} f g x {y} eq = elem y eq
 
-record  cequ' {c : Level} {A B : Set c} ( f g : A → B )  :   Set c where
-   field
-      cb : B
-      celem' : (a : A ) → f a ≡ cb → g a ≡ cb 
-
-c-equ  :  {  c₂ : Level}  {a b : Obj (Sets {c₂}) } ( f g : Hom (Sets {c₂}) a b ) → b → cequ f g
-c-equ {_} {a} {b} f g = {!!} 
-
-SetsIsCoEqualizer :  {  c₂ : Level}  →  (a b : Obj (Sets {c₂}) )  (f g : Hom (Sets {c₂}) a b) → IsCoEqualizer Sets (c-equ f g) f g
+SetsIsCoEqualizer :  {  c₂ : Level}  →  (a b : Obj (Sets {c₂}) )  (f g : Hom (Sets {c₂}) a b) → IsCoEqualizer Sets (equc f g) f g
 SetsIsCoEqualizer {c₂} a b f g = record {
-               ef=eg  = extensionality Sets {!!}
+               ef=eg  = extensionality Sets (λ x → refl )
              ; k = k 
              ; ke=h = λ {d} {h} {eq} → ke=h {d} {h} {eq}
              ; uniqueness  = {!!}
        } where
-          k : {d : Obj Sets} (h : Hom Sets b d) → Sets [ Sets [ h o f ] ≈ Sets [ h o g ] ] → Hom Sets {!!} d
-          k = {!!}
+          c : Set c₂
+          c =  {y : a} → f y ≡ g y → sequ a b f g
+          e : Hom Sets b c
+          e x {y} eq = elem y eq
+          ee : Hom Sets (sequ a b f g)  a
+          ee (elem y eq) = y
+          k : {d : Obj Sets} (h : Hom Sets b d) → Sets [ Sets [ h o f ] ≈ Sets [ h o g ] ] → Hom Sets c d
+          k {d} h hf=hg ec = {!!} where
+             cd : ( {y : a} → f y ≡ g y → sequ a b f g ) → d
+             cd ec = h ( f {!!} ) 
+             ff : sequ a b f g → sequ a d ( Sets [ h o f ]) (Sets [ h o g ])  
+             ff (elem x eq) = elem x (cong (λ k → k x ) hf=hg )
+             gg : {y : a} → f y ≡ g y → sequ a d ( Sets [ h o f ]) (Sets [ h o g ])  
+             gg {y} eq  = ff (ec eq)
+             hoge : ({y : a} → f y ≡ g y → sequ a d ( Sets [ h o f ]) (Sets [ h o g ]) ) → d
+             hoge ed = {!!}
           ke=h : {d : Obj Sets } {h : Hom Sets b d } → { eq : Sets [ Sets [ h o f ] ≈ Sets [ h o g ] ] }
-           →   Sets [ Sets [ k h eq o {!!} ] ≈ h ]
-          ke=h = {!!}
+           →   Sets [ Sets [ k h eq o equc f g ] ≈ h ]
+          ke=h {d} {h} {eq} =  extensionality Sets  ( λ  x → begin
+             k h eq ( equc f g x) ≡⟨ {!!} ⟩
+             h (f {!!})  ≡⟨ {!!}  ⟩
+             h (g {!!})  ≡⟨ {!!}  ⟩
+             h x
+             ∎ )  where
+                  open  import  Relation.Binary.PropositionalEquality
+                  open ≡-Reasoning
+
 
 open Functor
 
--- a/src/yoneda.agda	Sun Mar 07 11:47:19 2021 +0900
+++ b/src/yoneda.agda	Sun Mar 07 15:51:45 2021 +0900
@@ -334,6 +334,16 @@
 a1 : { c₁ : Level} {A B : Set c₁ } {a : A } { b : B } → a ≅ b → A ≡ B 
 a1 HE.refl = refl
 
+eqObj1' :  {a b : Obj A}  → Hom A a a ≡ Hom A a b → a ≡ b
+eqObj1' {a} {b} ha=hb = {!!} where
+        open Small small
+        ylem1 : I
+        ylem1  = hom→ (id1 A a)
+        ylem3 : I → Hom A a b
+        ylem3 i = hom← i
+        ylem2  : (i : I) → hom→ {a} {a} ( subst (λ k → k) (Relation.Binary.PropositionalEquality.sym ha=hb) (hom← {a} {b} i) ) ≡ i
+        ylem2 i = {!!} -- hom-rev
+
 open import Category.Cat