--- a/src/ToposEx.agda	Fri Apr 02 02:48:12 2021 +0900
+++ b/src/ToposEx.agda	Fri Apr 02 11:26:44 2021 +0900
@@ -320,59 +320,61 @@
                      < (nsuc iNat) o π ,  g  o π > o initialNat (prop33.xnat (p f' (g' o π))) ≈⟨⟩
                      nsuc (prop33.xnat (p f (g o π))) o initialNat (prop33.xnat (p f' (g' o π))) ∎
  
---   open Functor
---   open import Category.Sets
---   open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym)
--- 
---   record SubObject (a : Obj A) : Set (c₁ ⊔ c₂ ⊔ ℓ)  where
---      field
---         sb : Obj A
---         sm : Hom A sb a 
---         smono : Mono A sm
--- 
---   postulate
---      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← : (x :  Set (c₁ ⊔ c₂ ⊔ ℓ)) → solv← (solv→ x) ≡ x
---      -- soiso→ : (x : Set c₂ ) → solv→ (solv← x) ≡ x
---      ≡←≈ :   {a b : Obj A } { x y : Hom A a b } →  (x≈y : A [ x ≈ y  ]) → x ≡ y
---   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→ y (smap h (solv← x s))
--- 
---   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← a Sa)) (smono (solv← a Sa)) ; isNTrans = record { commute = {!!} } } -- Hom A a Ω
---       ; repr← = record { TMap = λ a h →  solv→ a record {sb = equalizer-c (Ker t h) ; sm = equalizer (Ker t h) ; smono =
---          {!!} } ; isNTrans = {!!} }  -- FObj (Sub S) a
---       ; reprId→  = {!!}
---       ; reprId←  = {!!}
---     }
---  
---  
--- 
--- 
+  open Functor
+  open import Category.Sets
+  open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym)
+
+  record SubObject (a : Obj A) : Set (c₁ ⊔ c₂ ⊔ ℓ)  where
+     field
+        sb : Obj A
+        sm : Hom A sb a 
+        smono : Mono A sm
+
+
+  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 → 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))
+
+    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←  = {!!}
+     }
+ 
+ 
+
+