Mercurial > hg > Members > kono > Proof > category

changeset 1009:a611f59932ef

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 Fri, 12 Mar 2021 19:36:18 +0900
parents e7b0db851a70
children bfd9c55ac628
files src/SetsCompleteness.agda
diffstat 1 files changed, 49 insertions(+), 45 deletions(-) [+]
line wrap: on
line diff
--- a/src/SetsCompleteness.agda	Thu Mar 11 12:47:19 2021 +0900
+++ b/src/SetsCompleteness.agda	Fri Mar 12 19:36:18 2021 +0900
@@ -202,54 +202,58 @@
                   open  import  Relation.Binary.PropositionalEquality
                   open ≡-Reasoning
 
-record cequ {c : Level} (A B : Set c)  :  Set c where
-  field
-    rev : (A → B) → B → A
-    surjective : (x : B ) → (g : A → B)  → g (rev g x) ≡ x
 
--- λ f₁ x y → (λ x₁ → x (f₁ x₁)) ≡ (λ x₁ → y (f₁ x₁)) → x ≡ y
--- λ x y → (λ x₁ → x x₁ ≡ y x₁) → x ≡ y
--- Y / R
+-- -- we have to make this Level c, that is {B : Set c} → (A → B) is iso to I : Set c
+-- record cequ {c : Level} (A B : Set c)  :  Set (suc c) where
+--   field
+--     rev : {B : Set c} → (A → B) → B → A
+--     surjective : {B : Set c } (x : B ) → (g : A → B)  → g (rev g x) ≡ x
 
--- equc  :  {  c₂ : Level}  {a b : Obj (Sets {c₂}) } ( f g : Hom (Sets {c₂}) a b )
---      → (x : b ) → ((y : a) →  f y ≡ x ) → ( (y : a) → g y ≡ x ) → cequ a b f g 
--- equc {_} {a} {b} f g x fyx gyx = record { sel = x ; modh = fyx ; modg = gyx }
+-- -- λ f₁ x y → (λ x₁ → x (f₁ x₁)) ≡ (λ x₁ → y (f₁ x₁)) → x ≡ y
+-- -- λ x y → (λ x₁ → x x₁ ≡ y x₁) → x ≡ y
+-- -- Y / R
+
+-- open import HomReasoning
 
-etsIsCoEqualizer :  {  c₂ : Level}  →  (a b : Obj (Sets {c₂}) )  (f g : Hom (Sets {c₂}) a b)
-  → IsCoEqualizer Sets (λ x → Sets [ cequ.rev x g o ? ]  ) f g
-etsIsCoEqualizer {c₂} a b f g = record {
-              ef=eg  = extensionality Sets (λ x → {!!} )
-            ; k = {!!} 
-            ; ke=h = λ {d} {h} {eq} → ke=h {d} {h} {eq}
-            ; uniqueness  = {!!}
-      } where
-         c : Set  c₂
-         c = cequ a b   
-         d : cequ a b   
-         d = {!!}
-         ef=eg : (x : a ) → (Sets [ cequ.rev d f o f ]) x ≡ (Sets [ cequ.rev d g o g ]) x
-         ef=eg x = begin
-             cequ.rev d f (f x) ≡⟨ ≡-sym (cequ.surjective d x (id1 Sets a)) ⟩
-             x ≡⟨ cequ.surjective d x (id1 Sets b) ⟩
-             cequ.rev d g (g x) ∎   where open ≡-Reasoning
-         epi :  { c₂ : Level  } {a b c : Obj (Sets { c₂})} (e : Hom Sets b c ) → (f g : Hom Sets a b) → Set c₂
-         epi e f g = Sets [ Sets [ e o f ] ≈ Sets [ e o g ] ] → Sets [ f ≈ g ]
-         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 = {!!} where
-            ca : Sets [ Sets [ h o f ] ≈ Sets [ h o g ] ] → a  -- (λ x → h (f x)) ≡ (λ x → h (g x))
-            ca eq = {!!}
-            cd : ( {y : a} → f y ≡ g y → sequ a b f g ) → d
-            cd = {!!}
-         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 {d} {h} {eq} =  extensionality Sets  ( λ  x → begin
-            k h eq ( {!!}) ≡⟨ {!!} ⟩
-            h (f {!!})  ≡⟨ {!!}  ⟩
-            h (g {!!})  ≡⟨ {!!}  ⟩
-            h x
-            ∎ )  where
-                 open  import  Relation.Binary.PropositionalEquality
-                 open ≡-Reasoning
+-- etsIsCoEqualizer :  {  c₂ : Level}  →  (a b : Obj (Sets {c₂}) )  (f g : Hom (Sets {c₂}) a b)
+--   → IsCoEqualizer Sets (λ x → {!!}    ) f g
+-- etsIsCoEqualizer {c₂} a b f g = record {
+--               ef=eg  = extensionality Sets (λ x → {!!} )
+--             ; k = {!!} 
+--             ; ke=h = λ {d} {h} {eq} → ke=h {d} {h} {eq}
+--             ; uniqueness  = {!!}
+--       } where
+--          c : Set  c₂
+--          c = {!!} --cequ a b   
+--          d : cequ a b   
+--          d = {!!}
+--          ef=eg :  Sets [ Sets [ cequ.rev d f o f ] ≈ Sets [ cequ.rev d g o g ] ]
+--          ef=eg = begin
+--              Sets [ cequ.rev d f o f ]  ≈↑⟨ idL ⟩
+--              Sets [ id1 Sets _ o Sets [ cequ.rev d f o f ]  ] ≈↑⟨ assoc ⟩
+--              Sets [ Sets [ id1 Sets _ o  cequ.rev d f ] o f ] ≈⟨ {!!}  ⟩
+--              Sets [ Sets [ id1 Sets _ o  cequ.rev d (id1 Sets _) ] o {!!} ] ≈⟨ car ( extensionality Sets (λ x →  cequ.surjective d {!!} {!!} ))  ⟩
+--              Sets [ {!!} o f ] ≈⟨ {!!}  ⟩
+--              Sets [ id1 Sets _ o Sets [ cequ.rev d g o g ]  ] ≈⟨ idL ⟩
+--              Sets [ cequ.rev d g o g ]  ∎  where open ≈-Reasoning Sets
+--          epi :  { c₂ : Level  } {a b c : Obj (Sets { c₂})} (e : Hom Sets b c ) → (f g : Hom Sets a b) → Set c₂
+--          epi e f g = Sets [ Sets [ e o f ] ≈ Sets [ e o g ] ] → Sets [ f ≈ g ]
+--          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 = {!!} where
+--             ca : Sets [ Sets [ h o f ] ≈ Sets [ h o g ] ] → a  -- (λ x → h (f x)) ≡ (λ x → h (g x))
+--             ca eq = {!!}
+--             cd : ( {y : a} → f y ≡ g y → sequ a b f g ) → d
+--             cd = {!!}
+--          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 {d} {h} {eq} =  extensionality Sets  ( λ  x → begin
+--             k h eq ( {!!}) ≡⟨ {!!} ⟩
+--             h (f {!!})  ≡⟨ {!!}  ⟩
+--             h (g {!!})  ≡⟨ {!!}  ⟩
+--             h x
+--             ∎ )  where
+--                  open  import  Relation.Binary.PropositionalEquality
+--                  open ≡-Reasoning
 
 
 open Functor