# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1614565588 -32400
# Node ID 5731ffd6cf7a6f3e43fe54f2ff1a4351581a78a7
# Parent  5f76e5cf3d496321cc098e7121be78174bac7639
...

diff -r 5f76e5cf3d49 -r 5731ffd6cf7a src/CCC.agda
--- a/src/CCC.agda	Sun Feb 28 17:31:13 2021 +0900
+++ b/src/CCC.agda	Mon Mar 01 11:26:28 2021 +0900
@@ -169,8 +169,8 @@
         (Ker : {a : Obj A} → ( h : Hom A a Ω ) → Equalizer A h (A [ ⊤ o (○ a) ]))
         (char : {a b : Obj A} → (m :  Hom A b a) → Mono A m  → Hom A a Ω) :  Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
      field
-         char-ker  : {a b : Obj A }  (m : Hom A b a ) → ( mono : Mono A m ) → {h : Hom A a Ω}
-             → A [ char m mono  ≈ h ]
+         char-ker  : {a b : Obj A } {h : Hom A a Ω}
+             → A [ char (equalizer (Ker h)) record { isMono = λ f g → monic (Ker h) }  ≈ h ]
          ker-char : {a b : Obj A} →  (m :  Hom A b a) → (mono : Mono A m)  → Iso A b (  equalizer-c (Ker ( char m mono ))) 
 
 record Topos {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)  ( １ : Obj A) (○ : (a : Obj A ) → Hom A a １) :  Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
@@ -206,8 +206,3 @@
          gNat : (nat : NatD A １ ) → Hom A (Nat TNat) (Nat nat)
          isToposN : IsToposNat A １ TNat gNat
 
-
-
-
-
-
diff -r 5f76e5cf3d49 -r 5731ffd6cf7a src/ToposEx.agda
--- a/src/ToposEx.agda	Sun Feb 28 17:31:13 2021 +0900
+++ b/src/ToposEx.agda	Mon Mar 01 11:26:28 2021 +0900
@@ -1,12 +1,15 @@
-module ToposEx where
 open import CCC
 open import Level
 open import Category
 open import cat-utility
 open import HomReasoning
+module ToposEx   {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (c : CCC A) (t : Topos A (CCC.１ c) (CCC.○ c) ) where
 
-open Topos
-open Equalizer
+  open Topos
+  open Equalizer
+  open ≈-Reasoning A
+  open CCC.CCC c
+
 
 --             ○ b
 --       b -----------→ 1
@@ -18,10 +21,8 @@
 --
 --   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 {
+  topos-pullback :  {a : Obj A}  → (h : Hom A a (Ω t)) → Pullback A h (⊤ t)
+  topos-pullback {a} h = record {
       ab = equalizer-c (Ker t h)         -- b
     ; π1 = equalizer   (Ker t h)         -- m
     ; π2 = ○ ( equalizer-c (Ker t h) )   -- ○ b
@@ -32,13 +33,13 @@
          ;    π2p=π2 = λ {d} {p1'} {p2'} {eq} → lemma2 eq
          ;    uniqueness = uniq
       }
-  } where
-    open ≈-Reasoning A
+    } where
+    e2 = IsCCC.e2 isCCC
     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)      ≈⟨ 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 (○ 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 ] ]
@@ -61,30 +62,8 @@
              IsEqualizer.k (isEqualizer (Ker t h)) p1' (lemma1 p1' p2' eq)  ≈⟨ IsEqualizer.uniqueness  (isEqualizer (Ker t h)) pe1 ⟩
              p' ∎ 
 
-topos-m-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 b : Obj A}  → (m : Hom A b a) → (mono : Mono A m ) → Pullback A (char t m mono )  (⊤ t)
-topos-m-pullback A １ ○ e2 t {a} {b} m mono  = topos-pullback A １ ○ e2 t {a} (char t m mono)
-
----
----
----
-
--- SubObjectFunctor : {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 １ ○ ) →  Functor A A
--- SubObjectFunctor A １ ○  e2 t = record {
---       FObj = λ x → Ω t
---     ; FMap = {!!}
---     ; isFunctor = record {
---           identity = {!!}
---         ; distr = {!!}
---         ; ≈-cong  = {!!}
---       }
---    }
-
-module _  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (c : CCC A) (t : Topos A (CCC.１ c) (CCC.○ c) ) where
-  open ≈-Reasoning A
-  open CCC.CCC c
+  topos-m-pullback : {a b : Obj A}  → (m : Hom A b a) → (mono : Mono A m ) → Pullback A (char t m mono )  (⊤ t)
+  topos-m-pullback {a} {b} m mono  = topos-pullback {a} (char t m mono)
 
   δmono : {b : Obj A } → Mono A < id1 A b , id1 A b >
   δmono  = record {
@@ -101,8 +80,8 @@
             id1 A _ o g  ≈⟨ idL ⟩
             g ∎
 
-  open Equalizer
-  open import equalizer
+  ip : {b : Obj A } → Pullback A  (char t  < id1 A b , id1 A b > δmono )  (⊤ t)
+  ip {b} = topos-m-pullback  < id1 A b , id1 A b > δmono
 
   prop32→ :  {a b : Obj A}→ (f g : Hom A a b )
     → A [ f ≈ g ] → A [ A [ char t < id1 A b , id1 A b > δmono  o < f , g > ]  ≈ A [ ⊤ t o  ○  a  ] ]
@@ -111,24 +90,12 @@
             char t < id1 A b , id1 A b > δmono o < f , f >  ≈↑⟨ cdr ( IsCCC.π-cong isCCC idL idL ) ⟩
             char t < id1 A b , id1 A b > δmono o < id1 A _ o f , id1 A _ o f >    ≈↑⟨ cdr ( IsCCC.distr-π isCCC ) ⟩
             char t < id1 A b , id1 A b > δmono o (< id1 A _ , id1 A _ > o f)   ≈⟨ assoc ⟩
-            (char t < id1 A b , id1 A b > δmono o < id1 A _ , id1 A _ > ) o f ≈⟨ car lem1 ⟩
+           (char t < id1 A b , id1 A b > δmono o Pullback.π1 pb ) o f  ≈⟨ car (IsPullback.commute (Pullback.isPullback pb)) ⟩
             (⊤ t o  ○  b)  o f  ≈↑⟨ assoc ⟩
             ⊤ t o  (○  b  o f)  ≈⟨ cdr (IsCCC.e2 isCCC)  ⟩
             ⊤ t o  ○  a  ∎ where
-               i = char t < id1 A b , id1 A b > δmono o < id1 A _ , id1 A _ > 
-               e = Ker t ( ⊤ t o ○ b) 
-               ki =  IsEqualizer.k (isEqualizer e) (id1 A _) refl-hom
-               lem1 : (char t < id1 A b , id1 A b > δmono o < id1 A _ , id1 A _ > ) ≈ ( ⊤ t o  ○  b )
-               lem1 = begin
-                  i ≈↑⟨ idR ⟩
-                  i o id1 A _    ≈↑⟨ cdr (IsEqualizer.ek=h (isEqualizer e) ) ⟩
-                  i o (equalizer e o ki ) ≈⟨ assoc ⟩
-                  (i o equalizer e ) o ki ≈⟨ {!!} ⟩
-                  (((⊤ t) o (○ b)) o equalizer e ) o ki ≈⟨ car (IsEqualizer.fe=ge (isEqualizer e)) ⟩
-                  ((⊤ t o  ○  b) o equalizer e ) o  ki ≈↑⟨ assoc ⟩
-                  (⊤ t o  ○  b) o (equalizer e  o  ki )   ≈⟨ cdr (IsEqualizer.ek=h (isEqualizer e) )⟩
-                  (⊤ t o  ○  b) o id1 A _   ≈⟨ idR ⟩
-                  ⊤ t o  ○  b ∎ 
+               pb : Pullback A (char t < id1 A b , id1 A b > δmono) (⊤ t )
+               pb =  {!!}
                
 
   prop23→ :  {a b : Obj A}→ (f g : Hom A a b )