--- a/src/CCCSets.agda	Tue Apr 27 10:24:04 2021 +0900
+++ b/src/CCCSets.agda	Thu Apr 29 11:16:18 2021 +0900
@@ -241,6 +241,31 @@
                ... | false | record { eq = eq1 } with tchar¬Img m mono (m x) eq1
                ... | t = ⊥-elim (t (isImage x)) 
 
+          open import Polynominal (Sets {c} )  (sets {c})
+          A = Sets {c}
+          Ω = Bool
+          １ = One
+          ⊤ = λ _ → true
+          ○ = λ _ → λ _ → !
+          _⊢_  : {a b : Obj A}  (p : Poly a  Ω b ) (q : Poly a  Ω b ) → Set (suc c )
+          _⊢_  {a} {b} p q = {c : Obj A} (h : Hom A c b ) → A [ Poly.f p o  h  ≈   ⊤ o ○  c  ]
+               → A [   Poly.f q ∙ h  ≈  ⊤ o  ○  c  ] 
+          tl01 : {a b : Obj A}  (p : Poly a  Ω b ) (q : Poly a  Ω b )
+             → p ⊢ q → q ⊢ p →  A [ Poly.f p ≈ Poly.f q ]
+          tl01 {a} {b} p q p<q q<p = extensionality Sets t1011 where
+            open ≡-Reasoning
+            t1011 : (s : b ) → Poly.f p s ≡ Poly.f q s 
+            t1011 x with Poly.f p x | inspect ( Poly.f p) x
+            ... | true | record { eq = eq1 } = sym tt1 where
+                 tt1 : Poly.f q _ ≡ true 
+                 tt1 = cong (λ k → k !) (p<q _ ( extensionality Sets (λ x → eq1) ))
+            ... | false |  record { eq = eq1 } with Poly.f q x | inspect (Poly.f q) x
+            ... | true | record { eq = eq2 } = ⊥-elim ( ¬x≡t∧x≡f record { fst  = eq1 ; snd = tt1 } ) where
+                 tt1 : Poly.f p _ ≡ true 
+                 tt1 = cong (λ k → k !) (q<p _ ( extensionality Sets (λ x → eq2) ))
+            ... | false | eq2 = refl
+
+
 open import graph
 module ccc-from-graph {c₁ c₂ : Level }  (G : Graph {c₁} {c₂})  where