--- a/src/ToposIL.agda	Tue Apr 27 08:52:39 2021 +0900
+++ b/src/ToposIL.agda	Tue Apr 27 10:24:04 2021 +0900
@@ -103,16 +103,29 @@
      _⊢_  : {a : Obj A}  (p : Poly a  (Topos.Ω t) １ ) (q : Poly a  (Topos.Ω t) １ ) → Set  ( c₁  ⊔  c₂ ⊔ ℓ ) 
      _⊢_  {a}  p q = {c : Obj A} (h : Hom A c １ ) → A [ Poly.f p ∙  h  ≈  (Topos.⊤ t) ∙  ○  c  ]
          → A [   Poly.f q ∙ h  ≈  (Topos.⊤ t) ∙  ○  c  ] 
+--
+--     iso          ○ b
+--  e ⇐====⇒  b -----------→ 1     
+--  |         |              |
+--  |       h |              | ⊤
+--  |         ↓    char h    ↓    
+--  + ------→ 1 -----------→ Ω    
+--     ker h       fp / fq
+--
      tl01 : {a : Obj A}  (p : Poly a  (Topos.Ω t) １ ) (q : Poly a  (Topos.Ω t) １ )
         → p ⊢ q → q ⊢ p →  A [ Poly.f p ≈ Poly.f q ]
      tl01 {a} p q p<q q<p = begin
-          Poly.f p ≈↑⟨ tt p ⟩
-          char t (equalizer (Ker t (Poly.f p))) (mm p) ≈⟨   {!!} ⟩
-          (char t (equalizer (Ker t (Poly.f p))) (mm p) ∙ {!!} ) ∙ {!!} ≈⟨ car (IsTopos.char-m=⊤ (Topos.isTopos t) (equalizer (Ker t (Poly.f p))) (mm p) ) ⟩
-          (Topos.⊤ t  ∙ {!!} ) ∙ {!!}  ≈⟨   {!!} ⟩
+          Poly.f p ≈⟨ {!!} ⟩
+          char t (id1 A _) {!!} ≈⟨   {!!} ⟩
           Topos.⊤ t ≈⟨  {!!} ⟩
           {!!}  ≈⟨ tt q ⟩
           Poly.f q ∎  where
+        pm : {c : Obj A} (h : Hom A c １ ) → A [   Poly.f p ∙ h  ≈  (Topos.⊤ t) ∙  ○  c  ] → A [   Poly.f q ∙ h  ≈  (Topos.⊤ t) ∙  ○  c  ] 
+        pm h = p<q h
+        qm : {c : Obj A} (h : Hom A c １ ) → A [   Poly.f q ∙ h  ≈  (Topos.⊤ t) ∙  ○  c  ] → A [   Poly.f p ∙ h  ≈  (Topos.⊤ t) ∙  ○  c  ] 
+        qm h = q<p h
+        hm : (h : Hom A {!!}  １ ) → Mono A h
+        hm h = record { isMono = {!!} }
         pp : Hom A １ (Topos.Ω t)
         pp =  Poly.f q
         open import equalizer using ( monic )