--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ToposEx.agda	Tue Feb 23 14:11:12 2021 +0900
@@ -0,0 +1,49 @@
+module ToposEx where
+open import CCC
+open import Level
+open import Category
+open import cat-utility
+open import HomReasoning
+
+open Topos
+open Equalizer
+
+--             ○ b
+--       b -----------→ 1
+--       |              |
+--     m |              | ⊤
+--       ↓    char m    ↓
+--       a -----------→ Ω
+--             h
+
+
+topos-pullback : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)  ( １ : Obj A) (○ : (a : Obj A ) → Hom A a １)
+  → (e2  : {a : Obj A} → ∀ { f : Hom A a １ } →  A [ f ≈ ○ a ] )
+  → (t : Topos A １ ○ ) → {a : Obj A}  → (h : Hom A a (Ω t)) → Pullback A h (⊤ t)
+topos-pullback A １ ○ e2 t {a} h = record {
+     --   Ker t h : Equalizer A h (A [ ⊤ o (○ a) ])
+      ab = equalizer-c (Ker t h)         -- b
+    ; π1 = equalizer   (Ker t h)         -- m
+    ; π2 = ○ ( equalizer-c (Ker t h) )   -- ○ b
+    ; isPullback = record {
+              commute = comm
+         ;    pullback = λ {d} {p1} {p2} eq → IsEqualizer.k (isEqualizer (Ker t h)) p1 (lemma1 p1 p2 eq )
+         ;    π1p=π1 = {!!}
+         ;    π2p=π2 = {!!}
+         ;    uniqueness = {!!}
+      }
+  } where
+    open ≈-Reasoning A
+    comm :  A [ A [ h o equalizer (Ker t h) ] ≈ A [ ⊤ t o ○ (equalizer-c (Ker t h)) ] ]
+    comm = begin
+            h o equalizer (Ker t h)      ≈⟨ {!!}  ⟩
+            ⊤ t o ○ (equalizer-c (Ker t h))   ∎
+    lemma1 : {d : Obj A}  (p1 : Hom A d a) (p2 : Hom A d １) (eq : A [ A [ h o p1 ] ≈ A [ ⊤ t o p2 ] ] )
+        → A [ A [ h o p1 ] ≈ A [ A [ ⊤ t o ○ a ] o p1 ] ]
+    lemma1 {d} p1 p2 eq = begin
+            h o p1                      ≈⟨ eq ⟩
+            ⊤ t o p2                    ≈⟨ cdr e2 ⟩
+            ⊤ t o  (○ d)                ≈↑⟨ cdr e2 ⟩
+            ⊤ t o ( ○ a o p1 )          ≈⟨ assoc ⟩
+           (⊤ t o ○ a ) o p1            ∎ 
+