--- a/src/ToposEx.agda	Tue Feb 23 14:11:12 2021 +0900
+++ b/src/ToposEx.agda	Tue Feb 23 16:32:06 2021 +0900
@@ -15,28 +15,30 @@
 --       ↓    char m    ↓
 --       a -----------→ Ω
 --             h
-
+--
+--   Ker t h : Equalizer A h (A [ ⊤ o (○ a) ])
 
 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 = {!!}
+         ;    π1p=π1 = IsEqualizer.ek=h (isEqualizer (Ker t h))
+         ;    π2p=π2 = λ {d} {p1'} {p2'} {eq} → lemma2 eq
+         ;    uniqueness = uniq
       }
   } 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)      ≈⟨ {!!}  ⟩
+            h o equalizer (Ker t h)      ≈⟨ IsEqualizer.fe=ge (isEqualizer (Ker t h)) ⟩
+            (⊤ t o ○ a ) o equalizer (Ker t h) ≈↑⟨ assoc ⟩
+            ⊤ t o (○ a  o equalizer (Ker t h)) ≈⟨ cdr e2 ⟩
             ⊤ 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 ] ]
@@ -46,4 +48,17 @@
             ⊤ t o  (○ d)                ≈↑⟨ cdr e2 ⟩
             ⊤ t o ( ○ a o p1 )          ≈⟨ assoc ⟩
            (⊤ t o ○ a ) o p1            ∎ 
+    lemma2 : {d : Obj A}  {p1' : Hom A d a} {p2' : Hom A d １} (eq : A [ A [ h o p1' ] ≈ A [ ⊤ t o p2' ] ] )
+        →   A [ A [  ○ (equalizer-c (Ker t h)) o IsEqualizer.k (isEqualizer (Ker t h)) p1'(lemma1 p1' p2' eq) ] ≈ p2' ]
+    lemma2 {d} {p1'} {p2'} eq = begin
+             ○ (equalizer-c (Ker t h)) o IsEqualizer.k (isEqualizer (Ker t h)) p1'(lemma1 p1' p2' eq)          ≈⟨ e2 ⟩
+             ○ d ≈↑⟨ e2 ⟩
+             p2' ∎ 
+    uniq :  {d : Obj A} (p' : Hom A d (equalizer-c (Ker t h))) {π1' : Hom A d a} {π2' : Hom A d １} {eq : A [ A [ h o π1' ] ≈ A [ ⊤ t o π2' ] ]}
+            {π1p=π1' : A [ A [ equalizer (Ker t h) o p' ] ≈ π1' ]} {π2p=π2' : A [ A [ ○ (equalizer-c (Ker t h)) o p' ] ≈ π2' ]}
+             → A [ IsEqualizer.k (isEqualizer (Ker t h)) π1' (lemma1 π1' π2' eq) ≈ p' ]
+    uniq {d} (p') {p1'} {p2'} {eq} {pe1} {pe2} = begin
+             IsEqualizer.k (isEqualizer (Ker t h)) p1' (lemma1 p1' p2' eq)  ≈⟨ IsEqualizer.uniqueness  (isEqualizer (Ker t h)) pe1 ⟩
+             p' ∎ 
 
+