open import CCC
open import Level
open import Category
open import cat-utility
open import HomReasoning
open import Data.List hiding ( [_] )
module ToposIL   {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (c : CCC A)   where

  open Topos
  open Equalizer
  -- open ≈-Reasoning A hiding (_∙_)
  open CCC.CCC c

  open Functor
  open import Category.Sets hiding (_o_)
  open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym)
  open import Polynominal A c

  record IsLogic (Ω : Obj A) (⊤ : Hom A １ Ω) (P  : Obj A → Obj A)
         (_==_ : {a : Obj A} (x y : Hom A １ a ) → Hom A １ Ω)
         (_∈_ : {a : Obj A} (x :  Hom A １ a ) (α : Hom A １ (P a) ) → Hom A １ Ω)
         (select : {a : Obj A} → ( φ :  Poly a Ω １ ) → Hom A １ (P a))
         (apply : {a  : Obj A}  (p : Poly a  Ω １ )  → ( x : Hom A １ a ) →  Poly a  Ω １ )
             :   Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
     field
         isSelect : {a : Obj A} → ( φ :  Poly a Ω １ ) → {c : Obj A} (h : Hom A c １ )
            → A [ ( ( Poly.x φ ∈ select φ ) == Poly.f φ )  ∙ h  ≈  ⊤ ∙  ○  c ]
         uniqueSelect : {a : Obj A} → ( φ :  Poly a Ω １ ) → (α : Hom A １ (P a) )
            → {c : Obj A} (h : Hom A c １ )
            → A [ ( Poly.f φ == ( Poly.x φ ∈ α ) )  ∙ h  ≈  ⊤ ∙  ○  c ]
            → A [ ( select φ == α )  ∙ h  ≈  ⊤ ∙  ○  c ]
         isApply : {a : Obj A}  (x y : Hom A １ a ) → (q p : Poly a  Ω １ ) 
            → {c : Obj A} (h : Hom A c １ )  → A [ ( x == y )  ∙ h  ≈  ⊤ ∙  ○  c ] 
            → A [ Poly.f q ∙ h  ≈  ⊤ ∙  ○  c ]
            → A [ Poly.f (apply p x ) ∙ h  ≈  ⊤ ∙  ○  c ] 
            → A [ Poly.f (apply p y ) ∙ h  ≈  ⊤ ∙  ○  c ]  
         applyCong : {a : Obj A}  (x : Hom A １ a ) → (q p : Poly a  Ω １ ) 
            → {c : Obj A} (h : Hom A c １ )  
            → ( A [ Poly.f q ∙ h  ≈  ⊤ ∙  ○  c ] → A [ Poly.f p ∙ h  ≈  ⊤ ∙  ○  c ] )
            → ( A [ Poly.f (apply q x ) ∙ h  ≈  ⊤ ∙  ○  c ] → A [ Poly.f (apply p x ) ∙ h  ≈  ⊤ ∙  ○  c ] )

  record InternalLanguage (Ω : Obj A) (⊤ : Hom A １ Ω) (P  : Obj A → Obj A)
          :   Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
     field
         _==_ : {a : Obj A} (x y : Hom A １ a ) → Hom A １ Ω
         _∈_ : {a : Obj A} (x :  Hom A １ a ) (α : Hom A １ (P a) ) → Hom A １ Ω
         -- { x ∈ a | φ x } : P a
         select : {a : Obj A} → ( φ :  Poly a Ω １ ) → Hom A １ (P a)
         apply : {a  : Obj A}  (p : Poly a  Ω １ )  → ( x : Hom A １ a ) →  Poly a  Ω １ 
         isIL : IsLogic Ω ⊤ P _==_ _∈_  select apply
     _⊢_  : {a : Obj A}  (p : Poly a  Ω １ ) (q : Poly a  Ω １ ) → Set  ( c₁  ⊔  c₂ ⊔ ℓ ) 
     _⊢_  {a}  p q = {c : Obj A} (h : Hom A c １ ) → A [ Poly.f p ∙  h  ≈  ⊤ ∙  ○  c  ]
         → A [   Poly.f q ∙ h  ≈  ⊤ ∙  ○  c  ] 
     _,_⊢_  : {a : Obj A}  (p : Poly a  Ω １ ) (p1 : Poly a  Ω １ ) (q : Poly a  Ω １ ) → Set  ( c₁  ⊔  c₂ ⊔ ℓ ) 
     _,_⊢_  {a}  p p1 q = {c : Obj A} (h : Hom A c １ ) → A [ Poly.f p ∙  h  ≈  ⊤ ∙  ○  c  ]
         → A [   Poly.f p1 ∙ h  ≈  ⊤ ∙  ○  c  ] 
         → A [   Poly.f q  ∙ h  ≈  ⊤ ∙  ○  c  ] 
     expr : {a b c  : Obj A}  (p : Hom A １ Ω  )  → ( x : Hom A １ a ) →  Poly a  Ω １ 
     expr p x = record { x = x ;  f = p ; phi = i }
     ⊨_ :   (p : Hom A １ Ω  ) →  Set  ( c₁  ⊔  c₂ ⊔ ℓ )
     ⊨  p = {c : Obj A} (h : Hom A c １ )  → A [ p  ∙ h  ≈  ⊤ ∙  ○  c ] 

--             ○ b
--       b -----------→ 1
--       |              |
--     m |              | ⊤
--       ↓    char m    ↓
--       a -----------→ Ω

  -- (n : ToposNat A １)
  -- open NatD
  -- open ToposNat n

  -- N : Obj A
  -- N = Nat iNat 

  open import ToposEx A c using ( δmono  )

  -- f ≡ λ (x ∈ a) → φ x , ∃ (f : b <= a) →  f ∙ x ≈  φ x  

  -- functional completeness
  FC0 : Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ )
  FC0 = {a : Obj A}  (t : Topos A c) ( φ : Poly a (Ω t)１) → Functional-completeness φ

  FC1 : Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ )
  FC1 = {a : Obj A}  (t : Topos A c) ( φ : Poly a (Ω t)１) → Fc φ

  topos→logic : (t : Topos A c ) → ToposNat A １ → FC0 →  FC1  → InternalLanguage (Topos.Ω t) (Topos.⊤ t) (λ a → (Topos.Ω t) <= a)
  topos→logic t n fc0 fc = record {
         _==_ = λ {b} f g →   A [ char t < id1 A b , id1 A b > (δmono t n ) o < f , g > ]
      ;  _∈_ = λ {a} x α →  A [ ε o < α , x > ]
      -- { x ∈ a | φ x } : P a
      ;  select = λ {a} φ →  Fc.g ( fc t φ )
      ;  apply = λ {a}  φ x → record { x = x ; f = Functional-completeness.fun (fc0 t φ ) ∙ < x ∙  ○ _ , id1 A _ >  ; phi = i }
      ;  isIL = record {
           isSelect = {!!}
         ; uniqueSelect = {!!}
         ; isApply = {!!}
         ; applyCong = {!!}
        }
    } 

  module IL1 (Ω : Obj A) (⊤ : Hom A １ Ω) (P  : Obj A → Obj A) (il : InternalLanguage  Ω ⊤ P) where
     open InternalLanguage il
     il00 : {a : Obj A}  (p : Poly a  Ω １ )  → p  ⊢ p
     il00 {a}  p h eq = eq

     il01 : {a : Obj A}  (p : Poly a  Ω １ ) (q : Poly a  Ω １ )
        → p ⊢ q → q ⊢ p →  A [ Poly.f p ≈ Poly.f q ]
     il01 {a} p q p<q q<p = {!!}

     il011 : {a : Obj A}  (p q q1 : Poly a  Ω １ ) 
        → q ⊢ p → q , q1 ⊢ p 
     il011 {a} p q q1 p<q h tq tq1 = p<q h tq

     il012 : {a : Obj A}  (p q r : Poly a  Ω １ ) 
        → q ⊢ p → q , p  ⊢ r → q ⊢ r 
     il012 {a} p q r p<q pq<r h  qt = pq<r h qt (p<q h qt) 
     

     il02 : {a : Obj A} (x : Hom A １ a ) → ⊨ (x == x) 
     il02 = {!!}

     --- (b : Hom A １ a) → φ y  ⊢ φ' y  → φ b  ⊢ φ' b
     il03 : {a : Obj A}  (b : Hom A １ a ) → (q p : Poly a  Ω １ ) 
        → q ⊢ p → apply q b  ⊢ apply p b
     il03 {a} b q p q<p h = IsLogic.applyCong (InternalLanguage.isIL il ) b q p h (q<p h)

     --- a == b → φ a  ⊢ φ b
     il04 : {a : Obj A}  (x y : Hom A １ a ) → (q p : Poly a  Ω １ ) 
        → ⊨ (x == y) 
        → q ⊢ apply p x → q ⊢ apply p y
     il04 {a} x y q p eq q<px h qt = IsLogic.isApply (InternalLanguage.isIL il ) x y q p h (eq h) qt (q<px h qt )
  
     --- ⊨ x ∈ select φ == φ x
     il05 : {a : Obj A}  → (q : Poly a  Ω １ ) 
        → ⊨ ( ( Poly.x q ∈ select q ) == Poly.f q  )
     il05 {a} = IsLogic.isSelect (InternalLanguage.isIL il )
  
     ---    q ⊢  φ x == x ∈ α 
     ---   ----------------------- 
     ---    q ⊢ select φ == α
     ---
     il06 : {a : Obj A}  → (q : Poly a  Ω １ )  → (α : Hom A １ (P a) )
        → ⊨ ( Poly.f q  == ( Poly.x q ∈ α ) ) 
        → ⊨ ( select q == α )
     il06 {a} q p eq h = IsLogic.uniqueSelect (InternalLanguage.isIL il ) q p h (eq h)