# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1614685753 -32400
# Node ID db288effad97ec1365bd629b0748a37775a05f11
# Parent  8ffdc897f29b1f754b7af18fb9ef1b16c4f4da6b
...

diff -r 8ffdc897f29b -r db288effad97 src/ToposEx.agda
--- a/src/ToposEx.agda	Tue Mar 02 17:56:31 2021 +0900
+++ b/src/ToposEx.agda	Tue Mar 02 20:49:13 2021 +0900
@@ -70,14 +70,14 @@
     ; π2 = ○ b   
     ; isPullback = record {
               commute = char-m=⊤ t m mono
-         ;    pullback = λ {d} {p1} {p2} eq →  
-             Iso.≅← (IsoL.iso-L (IsTopos.ker-char (isTopos t) m mono ))  o IsEqualizer.k (isEqualizer (Ker t (char t m mono))) p1 (mh=⊤ (char t m mono) p1 p2 eq )
+         ;    pullback = λ {d} {p1} {p2} eq →  f← o k  p1 p2 eq
          ;    π1p=π1 = λ {d} {p1'} {p2'} {eq} → lemma3 p1' p2' eq
          ;    π2p=π2 = λ {d} {p1'} {p2'} {eq} → trans-hom (IsCCC.e2 isCCC) (sym (IsCCC.e2 isCCC))
          ;    uniqueness = {!!}
       }
     } where
         f← = Iso.≅← (IsoL.iso-L (IsTopos.ker-char (isTopos t) m mono ))
+        f→ = Iso.≅→ (IsoL.iso-L (IsTopos.ker-char (isTopos t) m mono ))
         k : {d : Obj A} (p1 : Hom A d a) → (p2 : Hom A d １) →  A [ A [ char t m mono o p1 ] ≈ A [ ⊤ t o p2 ] ] → Hom A d (equalizer-c (Ker t (char t m mono)))
         k p1 p2 eq = IsEqualizer.k (isEqualizer (Ker t (char t m mono))) p1 (mh=⊤ (char t m mono) p1 p2 eq )
         lemma3 : {d : Obj A} (p1 : Hom A d a) → (p2 : Hom A d １)
@@ -87,6 +87,14 @@
            (m o f← ) o k p1 p2 eq ≈⟨ car (IsoL.iso≈L (IsTopos.ker-char (isTopos t) m mono )) ⟩
            equalizer (Ker t (char t m mono)) o k p1 p2 eq ≈⟨ IsEqualizer.ek=h (isEqualizer (Ker t (char t m mono))) ⟩
            p1 ∎
+        uniq : {d : Obj A} (p' : Hom A d b) (π1' : Hom A d a) (π2' : Hom A d １)
+            (eq : A [ A [ char t m mono o π1' ] ≈ A [ ⊤ t o π2' ] ]) →
+            A [ A [ m o p' ] ≈ π1' ] → A [ A [ ○ b o p' ] ≈ π2' ] → f← o k π1' π2' eq ≈ p' 
+        uniq {d} p p1 p2 eq pe1 pe2 = begin
+             f← o k p1 p2 eq ≈⟨ cdr ( IsEqualizer.uniqueness  (isEqualizer (Ker t  (char t m mono))) {!!} ) ⟩
+             f← o (f→ o p ) ≈⟨ {!!} ⟩
+             p ∎
+
 
   δmono : {b : Obj A } → Mono A < id1 A b , id1 A b >
   δmono  = record {