{-# OPTIONS --cubical --guardedness -WnoUnsupportedIndexedMatch --allow-unsolved-metas #-}

open import Data.Unit
open import Data.Empty
open import Data.List
open import Data.List.Membership.Propositional
open import Data.List.Membership.Propositional.Properties
open import Data.List.Relation.Unary.All
open import Data.List.Relation.Unary.All.Properties
open import Data.List.Relation.Unary.Any
open import Function.Base hiding (id)
open import Relation.Binary.PropositionalEquality
open import Data.Sum
open import Data.Product
open import Level

open import Cubical.HITs.SetQuotients

postulate
  sorry : {ℓ : Level} {A : Set ℓ} → A

1ℓ : Level
1ℓ = suc zero

record ⊤p {p : Level} : Set p where
  eta-equality
  constructor tt

data ⊥p {p : Level} : Set p where

record Signature : Set₁ where
  field
    Sort : Set
    Fun  : Set
    Rel  : Set

    dom : Fun → List Sort
    cod : Fun → Sort

    fld : Rel → List Sort

module Logic (S : Signature) where
  open Signature S

  Cxt : Set
  Cxt = List Sort

  data Term (Γ : Cxt) : Sort → Set where
    var  : {ty : Sort} → ty ∈ Γ → Term Γ ty
    _$ᵒ_ : (f : Fun) → All (Term Γ) (dom f) → Term Γ (cod f)

  data Fragment : Set where
    coherent  : Fragment
    geometric : Fragment
    full      : Fragment

  HasNegative : Fragment → Set
  HasNegative coherent  = ⊥
  HasNegative geometric = ⊥
  HasNegative full      = ⊤

  HasInfinitary : Fragment → Set
  HasInfinitary coherent  = ⊥
  HasInfinitary geometric = ⊤
  HasInfinitary full      = ⊤

  data Form (f : Fragment) : Cxt → Set₁ where
    _≡ᵒ_ : {ty : Sort} {Γ : Cxt} → Term Γ ty → Term Γ ty → Form f Γ
    atᵒ  : {Γ : Cxt} → (r : Rel) → All (Term Γ) (fld r) → Form f Γ
    ⊤ᵒ   : {Γ : Cxt} → Form f Γ
    ⊥ᵒ   : {Γ : Cxt} → Form f Γ
    _∧ᵒ_ : {Γ : Cxt} → Form f Γ → Form f Γ → Form f Γ
    _∨ᵒ_ : {Γ : Cxt} → Form f Γ → Form f Γ → Form f Γ
    ⋁ᵒ   : {Γ : Cxt} → {{HasInfinitary f}} → {I : Set} → (I → Form f Γ) → Form f Γ
    _⇒ᵒ_ : {Γ : Cxt} → {{HasNegative f}} → Form f Γ → Form f Γ → Form f Γ
    ∀ᵒ   : {ty : Sort} {Γ : Cxt} → {{HasNegative f}} → Form f (ty ∷ Γ) → Form f Γ
    ∃ᵒ   : {ty : Sort} {Γ : Cxt} → Form f (ty ∷ Γ) → Form f Γ

  data RedForm : Cxt → Set where
    _≡ᵒ_ : {ty : Sort} {Γ : Cxt} → Term Γ ty → Term Γ ty → RedForm Γ
    atᵒ  : {Γ : Cxt} → (r : Rel) → All (Term Γ) (fld r) → RedForm Γ
    ⊤ᵒ   : {Γ : Cxt} → RedForm Γ
    _∧ᵒ_ : {Γ : Cxt} → RedForm Γ → RedForm Γ → RedForm Γ
    ∃ᵒ   : {ty : Sort} {Γ : Cxt} → RedForm (ty ∷ Γ) → RedForm Γ

  red-relax : {f : Fragment} {Γ : Cxt} → RedForm Γ → Form f Γ
  red-relax (x ≡ᵒ y)   = x ≡ᵒ y
  red-relax (atᵒ r xs) = atᵒ r xs
  red-relax ⊤ᵒ         = ⊤ᵒ
  red-relax (φ ∧ᵒ ψ)   = red-relax φ ∧ᵒ red-relax ψ
  red-relax (∃ᵒ φ)     = ∃ᵒ (red-relax φ)

  record Theory (f : Fragment) : Set₁ where
    field
      Ax  : Set
      cxt : Ax → Cxt
      lhs : (a : Ax) → Form f (cxt a)
      rhs : (a : Ax) → Form f (cxt a)

  data Doctrine : Set where
    coherent       : Doctrine
    geometric      : Doctrine
    intuitionistic : Doctrine
    classical      : Doctrine
    minimal        : Doctrine

  SupportsExplosion : Doctrine → Set
  SupportsExplosion minimal = ⊥
  SupportsExplosion _       = ⊤

  SupportsLEM : Doctrine → Set
  SupportsLEM classical = ⊤
  SupportsLEM _         = ⊥

  SupportsNegative : Doctrine → Set
  SupportsNegative coherent       = ⊥
  SupportsNegative geometric      = ⊥
  SupportsNegative minimal        = ⊤
  SupportsNegative intuitionistic = ⊤
  SupportsNegative classical      = ⊤

  SupportsInfinitary : Doctrine → Set
  SupportsInfinitary coherent = ⊥
  SupportsInfinitary _        = ⊤

  {-# TERMINATING #-}
  raise : {Γ : Cxt} {σ τ : Sort} → Term Γ τ → Term (σ ∷ Γ) τ
  raise (var i)   = var (there i)
  raise (f $ᵒ xs) = f $ᵒ Data.List.Relation.Unary.All.map raise xs

  shift : {τ : Sort} {Γ Δ : Cxt} → ({σ : Sort} → σ ∈ Γ → Term Δ σ) → ({σ : Sort} → σ ∈ (τ ∷ Γ) → Term (τ ∷ Δ) σ)
  shift π (here i)  = var (here i)
  shift π (there i) = raise (π i)

  {-# TERMINATING #-}
  subs₀ : {Γ Δ : Cxt} {τ : Sort} → ({σ : Sort} → σ ∈ Γ → Term Δ σ) → Term Γ τ → Term Δ τ
  subs₀ π (var i)   = π i
  subs₀ π (f $ᵒ xs) = f $ᵒ Data.List.Relation.Unary.All.map (subs₀ π) xs

  subs : {frag : Fragment} {Γ Δ : Cxt} → ({σ : Sort} → σ ∈ Γ → Term Δ σ) → Form frag Γ → Form frag Δ
  subs π ⊤ᵒ         = ⊤ᵒ
  subs π ⊥ᵒ         = ⊥ᵒ
  subs π (φ ∧ᵒ ψ)   = subs π φ ∧ᵒ subs π ψ
  subs π (φ ∨ᵒ ψ)   = subs π φ ∨ᵒ subs π ψ
  subs π (⋁ᵒ φ)     = ⋁ᵒ (subs π ∘ φ)
  subs π (φ ⇒ᵒ ψ)   = subs π φ ⇒ᵒ subs π ψ
  subs π (∀ᵒ φ)     = ∀ᵒ (subs (shift π) φ)
  subs π (∃ᵒ φ)     = ∃ᵒ (subs (shift π) φ)
  subs π (s ≡ᵒ t)   = subs₀ π s ≡ᵒ subs₀ π t
  subs π (atᵒ r xs) = atᵒ r (Data.List.Relation.Unary.All.map (subs₀ π) xs)

  inj : {Γ : Cxt} {τ : Sort} → ({σ : Sort} → σ ∈ Γ → Term (τ ∷ Γ) σ)
  inj i = var (there i)

  weaken : {ty : Sort} {Γ : Cxt} {frag : Fragment} → Form frag Γ → Form frag (ty ∷ Γ)
  weaken = subs inj

  -- substitute a single term for the top-most variable, leaving the rest alone
  inst : {Γ : Cxt} {ty : Sort} → Term Γ ty → ({σ : Sort} → σ ∈ (ty ∷ Γ) → Term Γ σ)
  inst x (here refl) = x
  inst x (there i)   = var i

  inj-++ : {Γ Δ : Cxt} → ({σ : Sort} → σ ∈ Γ → Term (Γ ++ Δ) σ)
  inj-++ i = var (∈-++⁺ˡ i)

  weaken-++ : {Γ Δ : Cxt} {frag : Fragment} → Form frag Γ → Form frag (Γ ++ Δ)
  weaken-++ {Γ} {Δ} = subs (inj-++ {Γ} {Δ})

  inj-++ʳ : {Γ Δ : Cxt} → ({σ : Sort} → σ ∈ Δ → Term (Γ ++ Δ) σ)
  inj-++ʳ {Γ} i = var (∈-++⁺ʳ Γ i)
  
  weaken-++ʳ : {Γ Δ : Cxt} {frag : Fragment} → Form frag Δ → Form frag (Γ ++ Δ)
  weaken-++ʳ {Γ} {Δ} = subs (inj-++ʳ {Γ} {Δ})
   
  ∃ᵒ* : {frag : Fragment} {Γ : Cxt} (Δ : Cxt) → Form frag (Δ ++ Γ) → Form frag Γ
  ∃ᵒ* []      φ = φ
  ∃ᵒ* (τ ∷ Δ) φ = ∃ᵒ* Δ (∃ᵒ φ)

  eqᵒ* : {frag : Fragment} {Γ : Cxt} (Δ : Cxt)
       → ({σ : Sort} → σ ∈ Δ → Term Γ σ)
       → ({σ : Sort} → σ ∈ Δ → Term Γ σ)
       → Form frag Γ
  eqᵒ* []      lhs rhs = ⊤ᵒ
  eqᵒ* (τ ∷ Δ) lhs rhs = (lhs (here refl) ≡ᵒ rhs (here refl)) ∧ᵒ eqᵒ* Δ (lhs ∘ there) (rhs ∘ there)

  copy₁ : {Γ Δ : Cxt} {σ : Sort} → σ ∈ (Δ ++ Γ) → Term (Δ ++ (Δ ++ Γ)) σ
  copy₁ {Γ} {Δ} i with ∈-++⁻ Δ i
  ... | inj₁ j = var (∈-++⁺ˡ j)
  ... | inj₂ j = var (∈-++⁺ʳ Δ (∈-++⁺ʳ Δ j))
  
  copy₂ : {Γ Δ : Cxt} {σ : Sort} → σ ∈ (Δ ++ Γ) → Term (Δ ++ (Δ ++ Γ)) σ
  copy₂ {Γ} {Δ} i with ∈-++⁻ Δ i
  ... | inj₁ j = var (∈-++⁺ʳ Δ (∈-++⁺ˡ j))
  ... | inj₂ j = var (∈-++⁺ʳ Δ (∈-++⁺ʳ Δ j))

  swap-ctx : {Γ Δ : Cxt} {σ : Sort} → σ ∈ (Γ ++ Δ) → Term (Δ ++ Γ) σ
  swap-ctx {Γ} {Δ} i with ∈-++⁻ Γ i
  ... | inj₁ j = var (∈-++⁺ʳ Δ j)
  ... | inj₂ j = var (∈-++⁺ˡ j)

  relax : {f : Fragment} {Γ : Cxt} → Form f Γ → Form full Γ
  relax (s ≡ᵒ t)   = s ≡ᵒ t
  relax (atᵒ r xs) = atᵒ r xs
  relax ⊤ᵒ         = ⊤ᵒ
  relax ⊥ᵒ         = ⊥ᵒ
  relax (φ ∧ᵒ ψ)   = relax φ ∧ᵒ relax ψ
  relax (φ ∨ᵒ ψ)   = relax φ ∨ᵒ relax ψ
  relax (⋁ᵒ φ)     = ⋁ᵒ (relax ∘ φ)
  relax (φ ⇒ᵒ ψ)   = relax φ ⇒ᵒ relax ψ
  relax (∃ᵒ φ)     = ∃ᵒ (relax φ)
  relax (∀ᵒ φ)     = ∀ᵒ (relax φ)

  join-variables : {Γ : Cxt} {τ : Sort} → {σ : Sort} → σ ∈ (τ ∷ τ ∷ Γ) → Term (τ ∷ τ ∷ Γ) σ
  join-variables (here i)          = var (there (here i))
  join-variables (there (here i))  = var (there (here i))
  join-variables (there (there i)) = var (there (there i))

  module Proof {f : Fragment} (𝕋 : Theory f) (d : Doctrine) where
    open Theory 𝕋

    data _⊢_ : {Γ : Cxt} → Form f Γ → Form f Γ → Set₁ where
      axiom        : (a : Ax) → lhs a ⊢ rhs a
      identity     : {Γ : Cxt} {φ : Form f Γ} → φ ⊢ φ
      substitution : {Γ Δ : Cxt} {α β : Form f Γ} (π : {σ : Sort} → σ ∈ Γ → Term Δ σ) → α ⊢ β → subs π α ⊢ subs π β
      cut          : {Γ : Cxt} {α β γ : Form f Γ} → α ⊢ β → β ⊢ γ → α ⊢ γ
      eq-refl      : {τ : Sort} → (Form f (τ ∷ []) ∋ ⊤ᵒ) ⊢ (var (here refl) ≡ᵒ var (here refl))
      --eq-subst     : {Γ : Cxt} {τ : Sort} {α : Form f (τ ∷ τ ∷ Γ)} → ? -- ((var here ≡ᵒ var (there here)) ∧ᵒ α) ⊢ subs join-variables α  -- enough?
      top-intr     : {Γ : Cxt} {α : Form f Γ} → α ⊢ ⊤ᵒ
      conj-elimₗ   : {Γ : Cxt} {α β : Form f Γ} → (α ∧ᵒ β) ⊢ α
      conj-elimᵣ   : {Γ : Cxt} {α β : Form f Γ} → (α ∧ᵒ β) ⊢ β
      conj-intr    : {Γ : Cxt} {α β χ : Form f Γ} → χ ⊢ α → χ ⊢ β → χ ⊢ (α ∧ᵒ β)
      bot-elim     : {{SupportsExplosion d}} → {Γ : Cxt} {α : Form f Γ} → ⊥ᵒ ⊢ α
      disj-intrₗ   : {Γ : Cxt} {α β : Form f Γ} → α ⊢ (α ∨ᵒ β)
      disj-intrᵣ   : {Γ : Cxt} {α β : Form f Γ} → β ⊢ (α ∨ᵒ β)
      disj-elim    : {Γ : Cxt} {α β χ : Form f Γ} → α ⊢ χ → β ⊢ χ → (α ∨ᵒ β) ⊢ χ
      infdisj-intr : {{SupportsInfinitary d}} → {{_ : HasInfinitary f}} → {Γ : Cxt} {I : Set} {φ : I → Form f Γ} {i : I} → φ i ⊢ ⋁ᵒ φ
      infdisj-elim : {{SupportsInfinitary d}} → {{_ : HasInfinitary f}} → {Γ : Cxt} {I : Set} {φ : I → Form f Γ} {χ : Form f Γ} → ((i : I) → φ i ⊢ χ) → ⋁ᵒ φ ⊢ χ
      impl₁        : {{SupportsNegative d}} → {{_ : HasNegative f}} → {Γ : Cxt} {α β χ : Form f Γ} → (α ∧ᵒ β) ⊢ χ → α ⊢ (β ⇒ᵒ χ)
      impl₂        : {{SupportsNegative d}} → {{_ : HasNegative f}} → {Γ : Cxt} {α β χ : Form f Γ} → α ⊢ (β ⇒ᵒ χ) → (α ∧ᵒ β) ⊢ χ
      forall-intr  : {{SupportsNegative d}} → {{_ : HasNegative f}} → {Γ : Cxt} {ty : Sort} {α : Form f Γ} {β : Form f (ty ∷ Γ)} → weaken α ⊢ β → α ⊢ ∀ᵒ β
      forall-elim  : {{SupportsNegative d}} → {{_ : HasNegative f}} → {Γ : Cxt} {ty : Sort} {α : Form f Γ} {β : Form f (ty ∷ Γ)} {x : Term Γ ty} → α ⊢ ∀ᵒ β → α ⊢ subs (inst x) β
      exists-intr  : {Γ : Cxt} {ty : Sort} {α : Form f Γ} {β : Form f (ty ∷ Γ)} {x : Term Γ ty} → α ⊢ subs (inst x) β → α ⊢ ∃ᵒ β
      exists-elim  : {Γ : Cxt} {ty : Sort} {α : Form f (ty ∷ Γ)} {β : Form f Γ} → α ⊢ weaken β → ∃ᵒ α ⊢ β
      lem          : {{SupportsLEM d}} → {{_ : HasNegative f}} → {Γ : Cxt} {α : Form f Γ} → ⊤ᵒ ⊢ (α ∨ᵒ (α ⇒ᵒ ⊥ᵒ))

    _⊣⊢_ : {Γ : Cxt} → Form f Γ → Form f Γ → Set₁
    α ⊣⊢ β = (α ⊢ β) × (β ⊢ α)
    
  _⊢[_]_mod_ : {f : Fragment} {Γ : Cxt} → Form f Γ → Doctrine → Form f Γ → Theory f → Set₁
  α ⊢[ d ] β mod 𝕋 = α ⊢ β
    where open Proof 𝕋 d

record Cat (o m : Level) : Set (suc (o ⊔ m)) where
  infixr  _·_
  field
    Ob   : Set o
    Hom  : Ob → Ob → Set m

    id   : {A : Ob} → Hom A A
    _·_  : {A B C : Ob} → Hom B C → Hom A B → Hom A C

    assoc : {A B C D : Ob} (f : Hom A B) (g : Hom B C) (h : Hom C D) → (h · g) · f ≡ h · (g · f)
    left-id  : {A B : Ob} (f : Hom A B) → id · f ≡ f
    right-id : {A B : Ob} (f : Hom A B) → f · id ≡ f

  -- object of the slice over A
  record _↓ (A : Ob) : Set (o ⊔ m) where
    constructor ⟨_⟩
    field {stage} : Ob
          arr     : Hom stage A
  open _↓ public

  □ : {q : Level} {A : Ob} → (A ↓ → Set q) → Set (o ⊔ m ⊔ q)
  □ {A = A} P = {f : A ↓} → P f

record Presheaf {o m : Level} (cat : Cat o m) (p : Level) : Set (o ⊔ m ⊔ suc p) where
  open Cat cat

  field
    F₀ : Ob → Set p
    fmap : {A B : Ob} → Hom A B → F₀ B → F₀ A

    fmap-id : {A : Ob} → fmap {A} {A} id ≗ (λ x → x)
    fmap-·  : {A B C : Ob} (f : Hom A B) (g : Hom B C) → fmap f ∘ fmap g ≗ fmap (g · f)

-- Yoneda
module _ {o m : Level} (cat : Cat o m) where
  open Cat cat

  よ : Ob → Presheaf cat m
  よ A = record
    { F₀      = λ B → Hom B A
    ; fmap    = λ f g → g · f
    ; fmap-id = λ g → right-id g
    ; fmap-·  = λ f g h → assoc f g h
    }

record SubPresheaf {o m p : Level} {cat : Cat o m} (F : Presheaf cat p) (q : Level) : Set (o ⊔ m ⊔ p ⊔ suc q) where
  open Cat cat
  open Presheaf F

  field
    belongs   : {A : Ob} → F₀ A → Set q
    monotonic : {A B : Ob} (f : Hom A B) → (x : F₀ B) → belongs x → belongs (fmap f x)

module _ {o m : Level} {cat : Cat o m} (p : Level) where
  𝟙P : Presheaf cat p
  𝟙P = record
    { F₀      = λ _ → ⊤p
    ; fmap    = λ _ _ → tt
    ; fmap-id = λ _ → refl
    ; fmap-·  = λ _ _ _ → refl
    }

module _ {o m p p' : Level} {cat : Cat o m} where
  _×P_ : (F : Presheaf cat p) (F' : Presheaf cat p') → Presheaf cat (p ⊔ p')
  F ×P F' = record
    { F₀      = λ A → F₀ A × F₀' A
    ; fmap    = λ f (x , x') → fmap f x , fmap' f x'
    ; fmap-id = sorry
    ; fmap-·  = sorry
    }
    where
    open Presheaf F
    open Presheaf F' renaming (F₀ to F₀'; fmap to fmap')

module _ {o m p : Level} {cat : Cat o m} where
  open Cat cat
  open Presheaf

  productP : List (Presheaf cat p) → Presheaf cat p
  productP []       = 𝟙P p
  productP (F ∷ Fs) = F ×P productP Fs
  -- Would be nice to use `All` here, but then the output universe level would be more than `p`

  packP : {A : Ob} {Fs : List (Presheaf cat p)} → All (λ F → F₀ F A) Fs → F₀ (productP Fs) A
  packP []       = tt
  packP (x ∷ xs) = x , packP xs

record NaturalTransformation {o m p p' : Level} {cat : Cat o m} (F : Presheaf cat p) (F' : Presheaf cat p') : Set (o ⊔ m ⊔ p ⊔ p') where
  open Cat cat
  open Presheaf F
  open Presheaf F' renaming (F₀ to F₀'; fmap to fmap')

  field
    η : {A : Ob} → F₀ A → F₀' A
    natural : {A B : Ob} (f : Hom A B) → fmap' f ∘ η  ≗ η ∘ fmap f

record Coverage {o m : Level} (C : Cat o m) (c l : Level) : Set (o ⊔ m ⊔ suc c ⊔ suc l) where
  open Cat C
  field
    Cov    : Ob → Set c
    Leg    : ∀ {U} → Cov U → Set l
    src    : ∀ {U} {c : Cov U} → Leg c → Ob
    mor    : ∀ {U} {c : Cov U} (m : Leg c) → Hom (src m) U
    stable : ∀ {U V} (c : Cov U) (g : Hom V U)
           → Σ (Cov V) λ d
           → (m : Leg d)
           → Σ (Leg c) λ m'
           → Σ (Hom (src m) (src m')) λ h
           → mor m' · h ≡ g · mor m

record Site (o m c l : Level) : Set (suc (o ⊔ m ⊔ c ⊔ l)) where
  field
    cat : Cat o m
    cov : Coverage cat c l
  open Cat cat public
  open Coverage cov public

  data Ev {p : Level} (A : Ob) (P : A ↓ → Set p) : Set (o ⊔ m ⊔ l ⊔ c ⊔ p) where
    now   : P ⟨ id ⟩ → Ev A P
    later : (c : Cov A) → ((leg : Leg c) → Ev (src leg) (λ f → P ⟨ mor leg · arr f ⟩)) → Ev A P

  ∇ : {p : Level} {A : Ob} → (A ↓ → Set p) → Set (o ⊔ m ⊔ l ⊔ c ⊔ p)
  ∇ {A = A} P = Ev A P

  ∇-map : {p : Level} {A : Ob} {P Q : A ↓ → Set p} → ({f : A ↓} → P f → Q f) → Ev A P → Ev A Q
  ∇-map h (now x)     = now (h x)
  ∇-map h (later c k) = later c λ f → ∇-map h (k f)

record PresheafStructure {o m : Level} (cat : Cat o m) (S : Signature) (p : Level) : Set (o ⊔ m ⊔ suc p) where
  open Cat cat
  open Signature S
  open NaturalTransformation
  open Logic S
  open Presheaf

  field
    ⟦_⟧s : Sort → Presheaf cat p
    ⟦_⟧f : (f : Fun) → NaturalTransformation (productP (Data.List.map ⟦_⟧s (dom f))) ⟦ cod f ⟧s
    ⟦_⟧r : (r : Rel) → SubPresheaf (productP (Data.List.map ⟦_⟧s (fld r))) p

  Env : (Γ : Cxt) → (A : Ob) → Set p
  Env Γ A = All (λ ty → F₀ (⟦ ty ⟧s) A) Γ

  _↾_ : {Γ : Cxt} {A : Ob} → Env Γ A → (f : A ↓) → Env Γ (stage f)
  env ↾ f = Data.List.Relation.Unary.All.map (λ {ty} x → fmap (⟦ ty ⟧s) (arr f) x) env

  eval : {A : Ob} {ty : Sort} {Γ : Cxt} → Env Γ A → Term Γ ty → F₀ (⟦ ty ⟧s) A
  eval* : {A : Ob} {Γ : Cxt} {τs : List Sort} → Env Γ A → All (Term Γ) τs → All (λ ty → F₀ (⟦ ty ⟧s) A) τs

  eval env (var i)  = Data.List.Relation.Unary.All.lookup env i
  eval env (f $ᵒ xs) = η ⟦ f ⟧f (packP (Data.List.Relation.Unary.All.Properties.map⁺ (eval* env xs)))

  eval* env []       = []
  eval* env (x ∷ xs) = eval env x ∷ eval* env xs

module PresheafSemantics {o m p : Level} (cat : Cat o m) (S : Signature) (str : PresheafStructure cat S p) where
  open Cat cat
  open Signature S
  open Logic S
  open Presheaf
  open SubPresheaf
  open NaturalTransformation
  open PresheafStructure str

  execP : {A : Ob} {frag : Fragment} {Γ : Cxt} → Env Γ A → Form frag Γ → Set (o ⊔ m ⊔ p)
  execP env (x ≡ᵒ y)    = Lift (o ⊔ m) (eval env x ≡ eval env y)
  execP env (atᵒ r xs)  = Lift (o ⊔ m) (belongs ⟦ r ⟧r (packP (Data.List.Relation.Unary.All.Properties.map⁺ (Data.List.Relation.Unary.All.map (eval env) xs))))
  execP env ⊤ᵒ          = ⊤p
  execP env ⊥ᵒ          = ⊥p
  execP env (φ ∧ᵒ ψ)    = execP env φ × execP env ψ
  execP env (φ ∨ᵒ ψ)    = execP env φ ⊎ execP env ψ
  execP env (⋁ᵒ φ)      = ∃[ i ] execP env (φ i)
  execP env (φ ⇒ᵒ ψ)    = □ λ f → execP (env ↾ f) φ → execP (env ↾ f) ψ
  execP env (∀ᵒ {ty} φ) = □ λ f → (x : F₀ (⟦ ty ⟧s) _) → execP (x ∷ env ↾ f) φ
  execP env (∃ᵒ φ)      = ∃[ x ] execP (x ∷ env) φ

module SheafSemantics {o m c l p : Level} (site : Site o m c l) (S : Signature) (str : PresheafStructure (Site.cat site) S p) where
  open Site site
  open Signature S
  open Logic S
  open Presheaf
  open SubPresheaf
  open NaturalTransformation
  open PresheafStructure str

  exec∇ : {A : Ob} {frag : Fragment} {Γ : Cxt} → Env Γ A → Form frag Γ → Set (o ⊔ m ⊔ p ⊔ c ⊔ l)
  exec∇ env (x ≡ᵒ y)    = ∇ (λ f → eval (env ↾ f) x ≡ eval (env ↾ f) y)
  exec∇ env (atᵒ r xs)  = ∇ (λ f → (belongs ⟦ r ⟧r (packP (Data.List.Relation.Unary.All.Properties.map⁺ (Data.List.Relation.Unary.All.map (eval (env ↾ f)) xs)))))
  exec∇ env ⊤ᵒ          = ⊤p
  exec∇ {A} env ⊥ᵒ      = ∇ {A = A} λ _ → ⊥p {p}
  exec∇ env (φ ∧ᵒ ψ)    = exec∇ env φ × exec∇ env ψ
  exec∇ env (φ ∨ᵒ ψ)    = ∇ λ f → exec∇ (env ↾ f) φ ⊎ exec∇ (env ↾ f) ψ
  exec∇ env (⋁ᵒ φ)      = ∇ λ f → ∃[ i ] exec∇ (env ↾ f) (φ i)
  exec∇ env (φ ⇒ᵒ ψ)    = □ λ f → exec∇ (env ↾ f) φ → exec∇ (env ↾ f) ψ
  exec∇ env (∀ᵒ {ty} φ) = □ λ f → (x : F₀ (⟦ ty ⟧s) _) → exec∇ (x ∷ env ↾ f) φ
  exec∇ env (∃ᵒ φ)      = ∇ λ f → ∃[ x ] exec∇ (x ∷ env ↾ f) φ

module SyntacticSite (S : Signature) (open Logic S) (𝕋 : Theory geometric) (d : Doctrine) where
  open Signature S
  open Proof 𝕋 d

  Ob : Set₁
  Ob = Σ Cxt (Form geometric)

  record Hom' (A B : Ob) : Set₁ where
    private
      Γ = proj₁ A
      α = proj₂ A
      Δ = proj₁ B
      β = proj₂ B
    field
      χ             : Form geometric (Δ ++ Γ)
      bounded       : χ ⊢ (weaken-++ʳ α ∧ᵒ weaken-++ β)
      total         : α ⊢ ∃ᵒ* Δ χ
      single-valued : (subs (copy₁ {Γ} {Δ}) χ ∧ᵒ subs (copy₂ {Γ} {Δ}) χ) ⊢ eqᵒ* Δ (var ∘ ∈-++⁺ˡ) (var ∘ ∈-++⁺ʳ Δ ∘ ∈-++⁺ˡ)
  open Hom'

  _≈_ : {A B : Ob} → Hom' A B → Hom' A B → Set₁
  f ≈ g = χ f ⊣⊢ χ g

  Hom : Ob → Ob → Set₁
  Hom A B = Hom' A B / _≈_

  cat : Cat 1ℓ 1ℓ
  cat = record
    { Ob       = Ob
    ; Hom      = Hom
    ; id       = sorry
    ; _·_      = sorry
    ; assoc    = sorry
    ; left-id  = sorry
    ; right-id = sorry
    }

  record Cov (A : Ob) : Set₁ where
    private
      Γ = proj₁ A
      α = proj₂ A
  
    field
      I   : Set
      src : I → Ob
      mor : (i : I) → Hom' (src i) A

      jointly-surjective : α ⊢ ⋁ᵒ λ i → ∃ᵒ* (proj₁ (src i)) (subs (swap-ctx {Γ}) (χ (mor i)))

  cov : Coverage cat 1ℓ 0ℓ
  cov = record
    { Cov    = Cov
    ; Leg    = Cov.I
    ; src    = λ {c = c} → Cov.src c
    ; mor    = λ {c = c} → _/_.[_] ∘ Cov.mor c
    ; stable = sorry
    }

  site : Site 1ℓ 1ℓ 1ℓ 0ℓ
  site = record { cat = cat ; cov = cov }

  tauto' : Sort → Ob
  tauto' τ = τ ∷ [] , ⊤ᵒ

  tauto : Sort → Presheaf cat 1ℓ
  tauto τ = よ cat (tauto' τ)

  -- unfold a product element into the list of its component morphisms
  unpackP' : {A : Ob} (τs : Cxt)
           → Presheaf.F₀ (productP (Data.List.map tauto τs)) A
           → All (Hom A ∘ tauto') τs
  unpackP' []       _        = []
  unpackP' (τ ∷ τs) (x , xs) = x ∷ unpackP' τs xs

  composeMK : (f : Fun) (A : Ob) → All (Hom' A ∘ tauto') (dom f) → Hom' A (tauto' (cod f))
  composeMK f A reps = record
    { χ             = ∃ᵒ* (dom f) (bigConj (dom f) reps (λ i → i) ∧ᵒ (yterm ≡ᵒ (f $ᵒ argVars)))
    ; bounded       = sorry
    ; total         = sorry
    ; single-valued = sorry
    }
    where
      Γ : Cxt
      Γ = proj₁ A

      -- the (cod f)-output variable: it sits just past the dom-f prefix block
      yterm : Term (dom f ++ (cod f ∷ Γ)) (cod f)
      yterm = var (∈-++⁺ʳ (dom f) (here refl))

      -- the dom-f argument variables: the prefix block of the context
      argVars : All (Term (dom f ++ (cod f ∷ Γ))) (dom f)
      argVars = Data.List.Relation.Unary.All.tabulate (λ {σ} i → var (∈-++⁺ˡ i))

      place : {σ : Sort} → σ ∈ dom f → {ρ : Sort} → ρ ∈ (σ ∷ Γ) → Term (dom f ++ (cod f ∷ Γ)) ρ
      place i (here refl) = var (∈-++⁺ˡ i)
      place i (there j)   = var (∈-++⁺ʳ (dom f) (there j))

      bigConj : (Δ' : Cxt) → All (Hom' A ∘ tauto') Δ'
              → ({σ : Sort} → σ ∈ Δ' → σ ∈ dom f)
              → Form geometric (dom f ++ (cod f ∷ Γ))
      bigConj []       []       inj' = ⊤ᵒ
      bigConj (σ ∷ Δ') (r ∷ rs) inj' =
        subs (place (inj' (here refl))) (χ r) ∧ᵒ bigConj Δ' rs (λ j → inj' (there j))

  str : PresheafStructure cat S _
  str = record
    { ⟦_⟧s = tauto
    ; ⟦_⟧f = λ f → record
      { η       = ?
      ; natural = {!!}
      }
    ; ⟦_⟧r = λ r → record
      { belongs   = λ xs → {!!}
      ; monotonic = {!!}
      }
    }

  open PresheafStructure str

  -- the projection of the generic object (Γ , α) onto the i-th variable
  genπ : {Γ : Cxt} (α : Form geometric Γ) {σ : Sort} (i : σ ∈ Γ) → Hom' (Γ , α) (tauto' σ)
  genπ {Γ} α {σ} i = record
    { χ             = weaken α ∧ᵒ (var (here refl) ≡ᵒ var (there i))
    ; bounded       = conj-intr conj-elimₗ top-intr
    ; total         = {!!}
    ; single-valued = {!!}
    }

  -- the generic environment of (Γ , α): each variable is sent to its own projection
  gen* : (Γ : Cxt) (α : Form geometric Γ) → Env Γ (Γ , α)
  gen* Γ α = Data.List.Relation.Unary.All.tabulate (λ {σ} i → _/_.[ genπ α i ])

module Main (S : Signature) (open Logic S) (𝕋 : Theory geometric) where
  open SyntacticSite S 𝕋 geometric
  open SheafSemantics site S str
  open Signature S
  open Proof 𝕋 geometric
  open Site site

  complete : {Γ : Cxt} (α β : Form geometric Γ) → exec∇ {A = Γ , α} (gen* Γ α) β → α ⊢ β
  complete α (x ≡ᵒ y)  p = {!!}
  complete α (atᵒ r x) p = {!!}
  complete α ⊤ᵒ        p = top-intr
  complete α ⊥ᵒ        p = {!!}
  complete α (β ∧ᵒ β') p = conj-intr (complete α β (proj₁ p)) (complete α β' (proj₂ p))
  complete α (β ∨ᵒ β') p = {!!}
  complete α (⋁ᵒ x)    p = {!!}
  complete α (∃ᵒ β)    p = {!!}

  -- The following formula holds in the classifying topos of 𝕋: ∀x. (∀y. φ ⇒ ψ) ⇒ ⋁ α,
  -- where α ranges over all those geometric formulas for which α ∧ φ ⊢ ψ.
  nullstellensatz : {σ τ : Sort} → Form geometric (τ ∷ σ ∷ []) → Form geometric (τ ∷ σ ∷ []) → Form full []
  nullstellensatz φ ψ = ∀ᵒ (∀ᵒ (relax φ ⇒ᵒ relax ψ) ⇒ᵒ ⋁ᵒ {I = I} {!!})
    where
    I : Set
    I = ∃[ α ] {!? ⊢ ?!}

  nullstellensatz-holds : {σ τ : Sort} (φ ψ : Form geometric (τ ∷ σ ∷ [])) → exec∇ {A = [] , ⊤ᵒ} [] (nullstellensatz φ ψ)
  nullstellensatz-holds = {!!}