module ToposEx where
open import CCC
open import Level
open import Category
open import cat-utility
open import HomReasoning

open Topos
open Equalizer

--             ○ b
--       b -----------→ 1
--       |              |
--     m |              | ⊤
--       ↓    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 {
      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 = 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)      ≈⟨ 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 ] ]
    lemma1 {d} p1 p2 eq = begin
            h o p1                      ≈⟨ eq ⟩
            ⊤ t o p2                    ≈⟨ cdr e2 ⟩
            ⊤ 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' ∎ 

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

  δmono : {b : Obj A } → Mono A < id1 A b , id1 A b >
  δmono  = record {
     isMono = m1
   } where
    m1 :   {d b : Obj A} (f g : Hom A d b) → A [ A [  < id1 A b , id1 A b > o f ] ≈ A [  < id1 A b , id1 A b > o g ] ] → A [ f ≈ g ]
    m1 {d} {b} f g = {!!}

  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  ] ]
  prop32→ = {!!}

  prop23→ :  {a b : Obj A}→ (f g : Hom A a b )
    → A [ A [ char t  < id1 A b , id1 A b > δmono  o < f , g > ]  ≈ A [ ⊤ t o  ○  a  ] ] → A [ f ≈ g ]
  prop23→ = {!!}

  N : (n : ToposNat A １ ) → Obj A
  N n = NatD.Nat (ToposNat.TNat n)

  record prop33  (n : ToposNat A １ ) {a : Obj A} (f : Hom A １ a ) ( h : Hom A (N n ∧ a) a ) : Set  ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
     field 
       g :  Hom A (N n) a
       g0=f : A [ A [ g o NatD.nzero (ToposNat.TNat n) ]  ≈ f ]
       gs=h : A [ A [ g o NatD.nsuc  (ToposNat.TNat n) ]  ≈ A [ h o < id1 A _ , g > ] ]

  cor33  : (n : ToposNat A １ )
     → ( {a : Obj A} (f : Hom A １ a ) ( h : Hom A (N n ∧ a) a ) → prop33 n f h )
     → coProduct A １ ( NatD.Nat (ToposNat.TNat n)  ) --  N ≅ N + 1
  cor33 n p = record {
        coproduct = N n
      ; κ1 = NatD.nzero (ToposNat.TNat n)
      ; κ2 = id1 A (N n)
      ; isProduct = record {
              _+_ = λ {a} f g → prop33.g ( p {a} f π' )
           ;  κ1fxg=f = λ {a} {f} {g} → prop33.g0=f (p f π' )
           ;  κ2fxg=g = λ {a} {f} {g} → ?
           ;  uniqueness = {!!}
           ;  +-cong = {!!}

       }
    }