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 c ) where

  open Topos
  open Equalizer
  open ≈-Reasoning A
  open CCC.CCC c


--             ○ b
--       b -----------→ 1
--       |              |
--     m |              | ⊤
--       ↓    char m    ↓
--       a -----------→ Ω
--             h
--
--   Ker t h : Equalizer A h (A [ ⊤ o (○ a) ])

  mh=⊤ : {a d : Obj A} (h : Hom A a (Ω t))  (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 ] ]
  mh=⊤ {a} {d} h p1 p2 eq = begin
            h o p1                      ≈⟨ eq ⟩
            ⊤ t o p2                    ≈⟨ cdr (IsCCC.e2 isCCC) ⟩
            ⊤ t o  (○ d)                ≈↑⟨ cdr (IsCCC.e2 isCCC) ⟩
            ⊤ t o ( ○ a o p1 )          ≈⟨ assoc ⟩
           (⊤ t o ○ a ) o p1            ∎ 

  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
    ; isPullback = record {
              commute = comm
         ;    pullback = λ {d} {p1} {p2} eq → IsEqualizer.k (isEqualizer (Ker t h)) p1 (mh=⊤ h  p1 p2 eq )
         ;    π1p=π1 = IsEqualizer.ek=h (isEqualizer (Ker t h))
         ;    π2p=π2 = λ {d} {p1'} {p2'} {eq} → lemma2 eq
         ;    uniqueness = uniq
      }
    } 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 ○ (equalizer-c (Ker t h))   ∎
    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'(mh=⊤ h p1' p2' eq) ] ≈ p2' ]
    lemma2 {d} {p1'} {p2'} eq = begin
             ○ (equalizer-c (Ker t h)) o IsEqualizer.k (isEqualizer (Ker t h)) p1'(mh=⊤ h 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' (mh=⊤ h π1' π2' eq) ≈ p' ]
    uniq {d} (p') p1' p2' eq pe1 pe2 = begin
             IsEqualizer.k (isEqualizer (Ker t h)) p1' (mh=⊤ h p1' p2' eq)  ≈⟨ IsEqualizer.uniqueness  (isEqualizer (Ker t h)) pe1 ⟩
             p' ∎ 

  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  = record {
      ab = b     
    ; π1 = m    
    ; π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 )
         ;    π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 ))
        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 １)
            →  (eq : A [ A [ char t m mono o p1 ] ≈ A [ ⊤ t o p2 ] ] ) → m o (f← o k p1 p2 eq ) ≈ p1 
        lemma3 {d} p1 p2 eq = begin
           m o (f← o k p1 p2 eq ) ≈⟨ assoc ⟩
           (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 ∎

  δ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 eq = begin
            f  ≈↑⟨ idL ⟩
            id1 A _ o f ≈↑⟨ car (IsCCC.e3a isCCC) ⟩
            (π o < id1 A b , id1 A b >)  o f  ≈↑⟨ assoc ⟩
            π o (< id1 A b , id1 A b >  o f)  ≈⟨ cdr eq ⟩
            π o (< id1 A b , id1 A b >  o g)  ≈⟨ assoc ⟩
            (π o < id1 A b , id1 A b >)  o g  ≈⟨  car (IsCCC.e3a isCCC) ⟩
            id1 A _ o g  ≈⟨ idL ⟩
            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→ {a} {b} f g f=g = begin
            char t < id1 A b , id1 A b > δmono o < f , g >  ≈⟨  cdr ( IsCCC.π-cong isCCC refl-hom (sym f=g))  ⟩
            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 b , id1 A b > ) o f  ≈⟨ car (char-m=⊤ t < id1 A b , id1 A b > δmono  ) ⟩
            (⊤ t o  ○  b)  o f  ≈↑⟨ assoc ⟩
            ⊤ t o  (○  b  o f)  ≈⟨ cdr (IsCCC.e2 isCCC)  ⟩
            ⊤ t o  ○  a  ∎ 

  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→ {a} {b} f g eq = {!!} where
       δb : Hom A ( b ∧ b ) (Ω t)
       δb = char t  < id1 A b , id1 A b > δmono
       ip : Pullback A  δb  (⊤ t)
       ip = topos-m-pullback < id1 A b , id1 A b >  δmono
       k : Hom A a b
       k = IsPullback.pullback (Pullback.isPullback ip ) eq 
       p0 : δb o ( Pullback.π1 ip o  k )  ≈  ⊤ t o ○ a 
       p0 = begin
            δb o ( Pullback.π1 ip o k ) ≈⟨⟩
            char t < id1 A b , id1 A b > δmono o ( Pullback.π1 ip o k ) ≈⟨  {!!}  ⟩
            char t < id1 A b , id1 A b > δmono o < f , g >  ≈⟨   eq ⟩
            ⊤ t o ○ a  ∎
       pf :  f ≈ id1 A b o k
       pf =  {!!} -- IsPullback.uniqueness (Pullback.isPullback ip ) k  (Pullback.π1 ip o k )  (○  a) p0 refl-hom (IsCCC.e2 isCCC)
       p2 :  < f , g > ≈ ( < id1 A b , id1 A b > o k )
       p2 = begin
            < f , g >   ≈⟨  IsCCC.π-cong isCCC  pf {!!} ⟩
            < id1 A b o k  , id1 A b o k >   ≈↑⟨  IsCCC.distr-π isCCC  ⟩
            < id1 A b , id1 A b > o k  ∎

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

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

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

       }
    } where
        k2 : {a : Obj A} {f  : Hom A １ a} {g : Hom A (NatD.Nat (ToposNat.TNat n)) a }
           → A [ A [ prop33.g p f ((A Category.o g) π) o NatD.nsuc (ToposNat.TNat n) ] ≈ g ]
        k2 {a} {f} {g} = begin
            (prop33.g p f ((A Category.o g) π) o NatD.nsuc (ToposNat.TNat n))  ≈⟨ prop33.gs=h p f (g o π )   ⟩
            ( g o π ) o  < id1 A (N n) , prop33.g p f (g o π) >   ≈⟨ sym assoc ⟩
            g o ( π  o   < id1 A (N n) , prop33.g p f (g o π) >)  ≈⟨ cdr (IsCCC.e3a isCCC ) ⟩
            g o id1 A (N n)  ≈⟨ idR ⟩
            g  ∎