Mercurial > hg > Members > kono > Proof > category

changeset 1037:f757156ac9fe

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, 02 Apr 2021 19:55:43 +0900
parents b836c3dc7a29
children db3e89065178
files src/ToposEx.agda
diffstat 1 files changed, 109 insertions(+), 44 deletions(-) [+]
line wrap: on
line diff
--- a/src/ToposEx.agda	Fri Apr 02 11:26:44 2021 +0900
+++ b/src/ToposEx.agda	Fri Apr 02 19:55:43 2021 +0900
@@ -321,60 +321,125 @@
                      nsuc (prop33.xnat (p f (g o π))) o initialNat (prop33.xnat (p f' (g' o π))) ∎
  
   open Functor
-  open import Category.Sets
+  open import Category.Sets hiding (_o_)
   open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym)
 
+  record Singleton (a : Obj A) : Set (c₁ ⊔ c₂ ⊔ ℓ) where
+     field
+        singleton : Hom A (a ∧ a) ( CCC._<=_ c (Ω t) (a ∧ a) )
+        scommute  : A [ A [ CCC.ε c o < singleton , id1 A _ > ] ≈  char t < id1 A _ , id1 A _ > δmono ]  
+
+  tequalizer : {a b : Obj A} → (f g : Hom A a b ) → Equalizer A f g
+  tequalizer {a} {b} f g = record {
+      equalizer-c = equalizer-c  ker
+    ; equalizer = equalizer ker
+    ; isEqualizer = record {
+          fe=ge = {!!}
+        ; k = {!!}
+        ; ek=h = {!!}
+        ; uniqueness = {!!}
+      }
+    } where
+        ker : Equalizer A ( A [  char t < id1 A _ , id1 A b > δmono o < f , g > ] ) (A [ ⊤ t o (CCC.○ c a) ])
+        ker = Ker t ( A [  char t < id1 A _ , id1 A b > δmono o < f , g > ] )
+
+  singleton→mono : {a : Obj A} (s : Singleton a ) → Mono A (Singleton.singleton s)
+  singleton→mono {a} s = record { isMono = λ {b} f g eq → {!!} }
+
+  record Partialmap  (a b : Obj A) :  Set (c₁ ⊔ c₂ ⊔ ℓ) where
+      field
+         p : Obj A
+         d : Hom A p a
+         f : Hom A p b
+         dm  : Mono A d
+
+  record PartialmapClassifier  (b : Obj A) :  Set (c₁ ⊔ c₂ ⊔ ℓ) where
+      field
+         b1 : Obj A
+         η : Hom A b b1
+         pm : Partialmap b1 b
+         pmc : {a : Obj A} ( d f : Hom A a b) → Mono A d → Hom A a b1
+         pb : {a : Obj A} ( d f : Hom A a b) → (dm : Mono A d ) → Pullback A (pmc d f dm) η 
+         uniq : {a : Obj A} ( d f : Hom A a b) → (dm : Mono A d ) → (p : Hom A a b1) → Pullback A p η → A [ pmc d f dm ≈ p ]
+
+  partialmapClassifier : (b : Obj A) → PartialmapClassifier b
+  partialmapClassifier = {!!}
+
   record SubObject (a : Obj A) : Set (c₁ ⊔ c₂ ⊔ ℓ)  where
      field
         sb : Obj A
         sm : Hom A sb a 
         smono : Mono A sm
 
+  postulate
+    I : Set c₁
+    small : Small A I 
 
-  module SubObjectFunctor
-     (S : (a : Set (c₁ ⊔ c₂ ⊔ ℓ))  → Set c₂)
-     (solv← : {x : Obj A} → S (SubObject x) → SubObject x)
-     (solv→ : {x : Obj A} → SubObject x → S (SubObject x))
-     (soiso← : {a : Obj A} → (x : SubObject a) → solv← (solv→ x) ≡ x)
-     (soiso→ : {a : Obj A} → (x : S (SubObject a) ) → solv→ (solv← x) ≡ x)
-     (≡←≈ :   {a b : Obj A } { x y : Hom A a b } →  (x≈y : A [ x ≈ y  ]) → x ≡ y) where
+  open import yoneda A I small
 
-    open SubObject 
-
-    smap : {x y : Obj A} → Hom A y x → SubObject x → SubObject y
-    smap h s = record { sb = sb s ; sm = A [ {!!} o sm s ] ; smono = record { isMono = λ f g eq → Mono.isMono (smono s) f g {!!} } } 
-     -- A [ A [ A [ h o  (sm s) ] o f ] ≈ A [ A [ h o (sm s) ] o g ]  → A [ A [ sm s o f ] ≈ A [ sm s o g ] ]
-
-    Smap : {x y : Obj A} → Hom A y x → Hom Sets (S (SubObject x)) (S (SubObject y))
-    Smap {x} {y} h s = solv→ (smap h (solv← s))
+  cs : CCC SetsAop
+  cs = {!!}
+  
+  toposS : Topos SetsAop cs
+  toposS = {!!}
 
-    SubObjectFuntor  : Functor  (Category.op A)  (Sets {c₂})
-    SubObjectFuntor  = record {
-         FObj = λ x → S (SubObject x)
-       ; FMap = Smap
-       ; isFunctor  = {!!}
-       } 
-
-    sub→topos : (Ω : Obj A) → Representable A ≡←≈ SubObjectFuntor Ω → Topos A c
-    sub→topos Ω R = record {
-          Ω =  Ω
-       ;  ⊤ = {!!}
-       ;  Ker = {!!}
-       ;  char = λ m mono → {!!} 
-       ;  isTopos = record {
-          char-uniqueness  = {!!}
-       ;  ker-m = {!!}
-          } }
- 
-    topos→rep : (t : Topos A c ) → Representable A ≡←≈ SubObjectFuntor (Topos.Ω t)
-    topos→rep t = record {
-        repr→ = record { TMap = λ a Sa → Topos.char t (sm (solv← Sa)) (smono (solv← Sa)) ; isNTrans = record { commute = {!!} } } -- Hom A a Ω
-      ; repr← = record { TMap = λ a h →  solv→ record {sb = equalizer-c (Ker t h) ; sm = equalizer (Ker t h) ; smono =
-         {!!} } ; isNTrans = {!!} }  -- FObj (Sub S) a
-      ; reprId→  = {!!}
-      ; reprId←  = {!!}
-     }
- 
- 
+-- 
+--   module SubObjectFunctor
+--      (S : (a : Set (c₁ ⊔ c₂ ⊔ ℓ))  → Set c₂)
+--      (solv← : {x : Obj A} → S (SubObject x) → SubObject x)
+--      (solv→ : {x : Obj A} → SubObject x → S (SubObject x))
+--      (soiso← : {a : Obj A} → (x : SubObject a) → solv← (solv→ x) ≡ x)
+--      (soiso→ : {a : Obj A} → (x : S (SubObject a) ) → solv→ (solv← x) ≡ x)
+--      (≡←≈ :   {a b : Obj A } { x y : Hom A a b } →  (x≈y : A [ x ≈ y  ]) → x ≡ y) where
+-- 
+--     open SubObject 
+-- 
+--     Smap : {x y : Obj A} → Hom A y x → Hom Sets (S (SubObject x)) (S (SubObject y))
+--     Smap {x} {y} h s = solv→ record { sb = y ; sm = id1 A y ; smono = record { isMono = λ f g eq → sm1 f g eq } } where
+--          sm1 : {a : Obj A } → ( f g : Hom A a y ) → A [ A [ id1 A y o f ]  ≈ A [ id1 A y o g ] ] → A [ f  ≈ g ]
+--          sm1 f g eq = begin
+--               f ≈↑⟨ idL ⟩ 
+--               id1 A y o f ≈⟨ eq ⟩ 
+--               id1 A y o g ≈⟨ idL  ⟩ 
+--               g ∎  
+-- 
+--     SubObjectFuntor  : Functor  (Category.op A)  (Sets {c₂})
+--     SubObjectFuntor  = record {
+--          FObj = λ x → S (SubObject x)
+--        ; FMap = Smap
+--        ; isFunctor  = record {
+--               identity = {!!}
+--             ; distr  = {!!}
+--             ; ≈-cong  = {!!}
+--           }
+--        } 
+-- 
+--     open NTrans 
+--     sub→topos : (Ω : Obj A) → Representable A ≡←≈ SubObjectFuntor Ω → Topos A c
+--     sub→topos Ω R = record {
+--           Ω =  Ω
+--        ;  ⊤ = TMap (Representable.repr→ R) １ (solv→ record { sb = {!!} ; sm = {!!} ; smono = {!!} })
+--        ;  Ker = λ {a} h → record { equalizer-c = sb {!!}
+--           ; equalizer = sm {!!}
+--           ; isEqualizer = {!!}
+--           }
+--        ;  char = λ m mono → {!!} 
+--        ;  isTopos = record {
+--           char-uniqueness  = {!!}
+--        ;  ker-m = {!!}
+--           } }
+--  
+--     topos→rep : (t : Topos A c ) → Representable A ≡←≈ SubObjectFuntor (Topos.Ω t)
+--     topos→rep t = record {
+--         repr→ = record { TMap = λ a Sa → Topos.char t (sm (solv← Sa)) (smono (solv← Sa)) ; isNTrans = record { commute = {!!} } } -- Hom A a Ω
+--       ; repr← = record { TMap = λ a h →  solv→ record {sb = equalizer-c (Ker t h) ; sm = equalizer (Ker t h) ; smono =
+--          {!!} } ; isNTrans = {!!} }  -- FObj (Sub S) a
+--       ; reprId→  = {!!}
+--       ; reprId←  = {!!}
+--      }
+--  
+--  
+-- 
+--