Mercurial > hg > Members > kono > Proof > category

changeset 1019:501e016bf877

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 Thu, 25 Mar 2021 14:23:51 +0900
parents 4b517d46e987
children d7e89e26700e
files src/CCCSets.agda
diffstat 1 files changed, 15 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/src/CCCSets.agda	Wed Mar 24 23:15:22 2021 +0900
+++ b/src/CCCSets.agda	Thu Mar 25 14:23:51 2021 +0900
@@ -116,6 +116,9 @@
 -- irr : { c₂ : Level}  {d : Set c₂ }  { x y : d } ( eq eq' :  x  ≡ y ) → eq ≡ eq'
 -- irr refl refl = refl
 
+open import Relation.Nullary
+open import Data.Empty
+
 topos : {c : Level } → Topos (Sets {c}) sets
 topos {c}  = record {
          Ω = Bool
@@ -144,19 +147,18 @@
            ; uniqueness = {!!} 
           } 
         uniq : {a : Obj (Sets {c})} {b : Obj Sets} (h : Hom Sets a Bool) (m : Hom Sets b a) (mono : Mono Sets m) (x : a) → true ≡ h x
-        uniq {a} {b} h m mono x = begin
-            true ≡⟨⟩
-            (λ × → true ) x ≡⟨ cong (λ k → {!!} ) (sym (IsEqualizer.fe=ge (Equalizer.isEqualizer (tker h)) ) ) ⟩
-            {!!} ≡⟨  {!!} ⟩
-            h x  ∎  where
-              open ≡-Reasoning 
-              yy : Sets [ (λ e → {!!} ) ≈ (λ e → true) ] 
-              yy = IsEqualizer.fe=ge (Equalizer.isEqualizer (tker h))
-              yyy : {c : Obj Sets } → (f g : c → b ) → Sets [ Sets [ m o f ] ≈ Sets [ m o g ] ] → f ≡ g
-              yyy f g eq = Mono.isMono mono f g eq
-              yyy1 : {c : Obj Sets } → (f g : c → b ) → Sets [ Sets [ m o f ] ≈ Sets [ m o g ] ] → f ≡ g
-              yyy1 f g eq = Mono.isMono mono f g eq
-
+        uniq {a} {b} h m mono x with IsEqualizer.fe=ge (Equalizer.isEqualizer (tker h)) | h x | inspect h x
+        ... | t | true | _ = refl
+        ... | t | false | record { eq = eq1 } = ⊥-elim ( uniq1 t ) where
+             neq : _≡_ {c} {Bool} true false → ⊥
+             neq ()
+             se : sequ a Bool h (λ _ → true)
+             se = elem x ? -- Mono.isMono mono ? ? ?  -- Equalizer.equalizer-c (tker h)
+             uniq1 : (λ x₁ → h (equ x₁)) ≡ (λ x₁ → true) → ⊥
+             uniq1 eq = neq ( begin
+                true ≡⟨ cong (λ k → k se) (sym eq)  ⟩
+                h x ≡⟨ eq1 ⟩
+                false ∎ ) where  open ≡-Reasoning 
            
 
 open import graph