module Countable (X : Set) where

open import Data.List
open import Data.List.Membership.Propositional
open import Data.List.Properties
open import Data.List.Relation.Unary.Any
open import Data.List.Relation.Unary.Any.Properties
open import Data.Nat hiding (_≤_)
open import Relation.Binary.PropositionalEquality
open import Data.Product
open import Data.Sum
open import Data.Maybe
open import Data.Fin hiding (_≥_; _>_)

-- Good P σ heißt: egal, wie sich die endliche Approximation σ an eine
-- Surjektion ℕ ↠ X zu einer besseren solchen Approximation entwickeln 
-- wird, schlussendlich wird sie P erfüllen.
data Good (P : List X → Set) : List X → Set where
  Here     : {σ : List X} → (p : P σ) → Good P σ
  Total    : {σ : List X} → (f : (x : X) → Good P (x ∷ σ)) → Good P σ
  Preimage : {a : X} {σ : List X} → (g : (τ : List X) → a ∈ τ ++ σ → Good P (τ ++ σ)) → Good P σ

-- Folgendes ist die Kripke-Joyal-Übersetzung von: "Jedes a wird getroffen."
-- Gibt es unten noch mal als ex₂, dort wird die KJ-Übersetzung anders
-- als hier nicht von Hand vorgenommen.
ex₀ : {a : X} → Good (λ σ → a ∈ σ) []
ex₀ = Preimage (λ τ → Here)

-- Folgendes ist die Kripke-Joyal-Übersetzung von: "f(0), f(1) und f(2) sind alle definiert"
ex₁ : Good (λ σ → length σ ≥ ) []
ex₁ = Total λ _ → Total (λ _ → Here (s≤s (s≤s z≤n)))

module _ (x₀ : X) (Q : Set) where
  lemma-conservative : {σ : List X} → Good (λ _ → Q) σ → Q
  lemma-conservative (Here p)             = p
  lemma-conservative (Total f)            = lemma-conservative (f x₀)
  lemma-conservative {σ} (Preimage {a} g) = lemma-conservative (g (a ∷ σ) (Data.List.Relation.Unary.Any.Any.here refl))

Monotonic : (P : List X → Set) → Set
Monotonic P = (σ : List X) → P σ → ((x : X) → P (x ∷ σ))

++-and-∷ʳ : (τ : List X) (x : X) (σ : List X) → τ ∷ʳ x ++ σ ≡ τ ++ x ∷ σ
++-and-∷ʳ []      x σ = refl
++-and-∷ʳ (a ∷ τ) x σ = cong (_∷_ a) (++-and-∷ʳ τ x σ)

module _ (P : List X → Set) (m : Monotonic P) where
  lemma-monotonic : Monotonic (Good P)
  lemma-monotonic σ (Here     p)     x = Here (m σ p x)
  lemma-monotonic σ (Total    f)     x = f x
  lemma-monotonic σ (Preimage {a} g) x = Preimage {a = a} go
    where
    go : (τ : List X) → a ∈ τ ++ x ∷ σ → Good P (τ ++ x ∷ σ)
    go τ p with g (τ ∷ʳ x)
    go τ p | q rewrite ++-and-∷ʳ τ x σ = q p

module _ {P Q : List X → Set} (h : {σ : List X} → P σ → Q σ) where
  lemma-map : {σ : List X} → Good P σ → Good Q σ
  lemma-map (Here     p) = Here     (h p)
  lemma-map (Total    f) = Total    (λ x → lemma-map (f x))
  lemma-map (Preimage g) = Preimage (λ τ z → lemma-map (g τ z))

module _ {P Q : List X → Set} (h : {σ : List X} → P σ → Good Q σ) where
  lemma-map' : {σ : List X} → Good P σ → Good Q σ
  lemma-map' (Here     p) = h p
  lemma-map' (Total    f) = Total (λ x → lemma-map' (f x))
  lemma-map' (Preimage g) = Preimage (λ τ z → lemma-map' (g τ z))

-- KRIPKE-JOYAL-SEMANTIK

Ty : Set₁
Ty = Set

Cxt : Set₁
Cxt = List Ty

data Term (Δ : Cxt) : Ty → Set₁ where
  var : {A : Ty} → A ∈ Δ → Term Δ A
  con : {A : Ty} → A → Term Δ A

data Form (Δ : Cxt) : Set₁ where
  _≣_ : {A : Ty} → Term Δ A → Term Δ A → Form Δ
  RR  : Term Δ ℕ → Term Δ X → Form Δ   -- RR(n,x) meint: f(n) = x, wobei f die generische Surjektion ist
  ⊤   : Form Δ
  ⊥   : Form Δ
  _∧_ : Form Δ → Form Δ → Form Δ
  _∨_ : Form Δ → Form Δ → Form Δ
  _⇒_ : Form Δ → Form Δ → Form Δ
  ⋀   : (A : Ty) → Form (A ∷ Δ) → Form Δ
  ⋁   : (A : Ty) → Form (A ∷ Δ) → Form Δ

data Env : Cxt → Set₁ where
  []  : Env []
  _∷_ : {A : Ty} {Δ : Cxt} → A → Env Δ → Env (A ∷ Δ)

record Unit : Set where

data Bottom : Set where

eval' : {Δ : Cxt} {A : Ty} → Env Δ → Term Δ A → A
eval' env (con x) = x
eval' [] (var ())
eval' (x ∷ env) (var (here refl)) = x
eval' (_ ∷ env) (var (there x)) = eval' env (var x)

_!!_ : List X → ℕ → Maybe X
[]       !! n = nothing
(x ∷ xs) !! zero  = just x
(x ∷ xs) !! suc n = xs !! n

R : ℕ → X → List X → Set
R n x σ = reverse σ !! n ≡ just x

eval : {Δ : Cxt} → Env Δ → Form Δ → List X → Set
eval {Δ} env (s ≣ t)  = Good (λ _ → eval' env s ≡ eval' env t)
eval {Δ} env (RR n x) = Good (R (eval' env n) (eval' env x))
eval {Δ} env ⊤        = λ _ → Unit
eval {Δ} env ⊥        = Good (λ _ → Bottom)
eval {Δ} env (φ ∧ ψ)  = λ σ → eval env φ σ × eval env ψ σ
eval {Δ} env (φ ∨ ψ)  = Good (λ τ → eval env φ τ ⊎ eval env ψ τ)
eval {Δ} env (φ ⇒ ψ)  = λ σ → (τ : List X) → eval env φ (τ ++ σ) → eval env ψ (τ ++ σ)
eval {Δ} env (⋀ A φ)  = λ σ → (a : A) → eval (a ∷ env) φ σ
eval {Δ} env (⋁ A φ)  = Good (λ τ → Σ[ a ∈ A ] eval (a ∷ env) φ τ)

univ-surj-is-surj : Form []
univ-surj-is-surj = ⋀ X (⋁ ℕ (RR (var (here refl)) (var (there (here refl)))))

ex₂ : eval [] univ-surj-is-surj []
ex₂ = λ a → Preimage {a = a} λ σ p → Here (Data.Product.map₂ Here (lemma₃ p))
  where
  lemma₁ : {σ : List X} {a : X} → (p : a ∈ σ) → σ !! toℕ (index p) ≡ just a
  lemma₁ {.(a ∷ _)} {a} (here refl) = refl
  lemma₁ {.(_ ∷ _)} {a} (there p) = lemma₁ p
  
  lemma₂ : {σ : List X} {a : X} → a ∈ reverse σ → Σ[ n ∈ ℕ ] (R n a σ)
  lemma₂ {σ} {a} p = toℕ (index p) , lemma₁ p
  
  lemma₃ : {σ : List X} {a : X} → a ∈ σ → Σ[ n ∈ ℕ ] (R n a σ)
  lemma₃ {σ} {a} p = lemma₂ {σ} {a} (reverse⁺ p)

univ-surj-is-total : Form []
univ-surj-is-total = ⋀ ℕ (⋁ X (RR (var (there (here refl))) (var (here refl))))

{-
ex₃ : eval [] univ-surj-is-total []
ex₃ n = Total^ n λ σ p → Here ((reverse σ !!' (subst (λ m → m > n) (sym (length-reverse σ)) p)) , Here (go n σ p))
  where
  Total^ : (n : ℕ) {P : List X → Set} → ((σ : List X) → length σ > n → Good P σ) → Good P []
  Total^ zero    f = Total (λ x → f (x ∷ []) (s≤s z≤n))
  Total^ (suc n) f = Total^ n (λ σ z → Total (λ x → f (x ∷ σ) (s≤s z)))

  _!!'_ : (σ : List X) {n : ℕ} → length σ > n → X
  _!!'_ (x ∷ σ) {zero} p = x
  _!!'_ (x ∷ σ) {suc n} (s≤s p) = σ !!' p

  go : (n : ℕ) (σ : List X) (p : length σ > n) → R n (reverse σ !!' subst (λ m → m > n) (sym (length-reverse σ)) p) σ
  go = {!!}

inv : {P Q : List X → Set} {x : X} {σ : List X} → ({τ : List X} → P (τ ++ σ) → Q (τ ++ σ)) → ({τ : List X} → P (τ ++ x ∷ σ) → Q (τ ++ x ∷ σ))
inv h p = subst {!!} (++-and-∷ʳ {!!} {!!} {!!}) {!!}

module _ {P Q : List X → Set} where
  lemma-map'' : {σ : List X} → (h : {τ : List X} → P (τ ++ σ) → Good Q (τ ++ σ)) → Good P σ → Good Q σ
  lemma-map'' h (Here p) = h p
  lemma-map'' {σ} h (Total f) = Total λ x → lemma-map'' {x ∷ σ} (inv {P = P} {Q = Good Q} {x = x} {σ = σ} h) (f x) -- lemma-map'' (λ {τ} p → subst {!λ v → P v!} (sym (++-and-∷ʳ τ x σ)) {!!}) (f x)
  lemma-map'' h (Preimage {a} g) = Preimage {a = a} λ τ q → lemma-map'' {!!} (g τ q)


univ-surj-is-single-valued : Form []
univ-surj-is-single-valued = ⋀ ℕ (⋀ X (⋀ X ((RR (var (there (there (here refl)))) (var (here refl)) ∧ RR (var (there (there (here refl)))) (var (there (here refl)))) ⇒ (var (here refl) ≣ var (there (here refl))))))

ex₄ : eval [] univ-surj-is-single-valued []
ex₄ = λ n x x' σ (p , p') → lemma-map'' (λ q → lemma-map'' {!!} {!!}) p

_↓_ : (ℕ → X) → ℕ → List X
α ↓ 0       = []
α ↓ (suc n) = α n ∷ (α ↓ n)

Surjective : {A B : Set} → (A → B) → Set
Surjective {A} {B} f = (y : B) → Σ[ x ∈ A ] f x ≡ y

module _ (P : List X → Set) where
  lemma : {σ : List X} → Good P σ → (α : ℕ → X) → Surjective α → α ↓ length σ ≡ σ → Σ[ n ∈ ℕ ] (P (α ↓ n))
  lemma {σ} (Here p) α surj q = length σ , subst P (sym q) p
  lemma {σ} (Total f) α surj q = lemma (f (α (length σ))) α surj (cong (λ τ → α (length σ) ∷ τ) q)
  lemma {σ} (Preimage g) α surj q = {!!}



{-

record Presheaf : Set₁ where
  field
    Γ    : List X → Set
    _//_ : {σ : List X} → Γ σ → (x : X) → Γ (x ∷ σ)

  _//*_ : {σ : List X} → Γ σ → (τ : List X) → Γ (τ ++ σ)
  s //* [] = s
  s //* (x ∷ τ) = (s //* τ) // x

{-
record GluingData (E : Presheaf) {I : Set} (u : I → List X) : Set where
  open Presheaf E
  field
    sections   : (i : I) → Γ (u i)
    compatible :
-}

record Sheaf : Set₁ where
  field
    presheaf : Presheaf
  open Presheaf presheaf public

  field
    glue-total : {σ : List X} → (s : (x : X) → Γ (x ∷ σ)) → Γ σ
    glue-total₀
      : {σ : List X} (s : (x : X) → Γ (x ∷ σ))
      → (x : X) → glue-total s // x ≡ s x
    glue-total₁
      : {σ : List X} (s t : Γ σ)
      → ((x : X) → s // x ≡ t // x)
      → s ≡ t

    glue-preimage
      : {σ : List X} {a : X}
      → (s : (τ : List X) → a ∈ τ ++ σ → Γ (τ ++ σ))
      → ((x : X) (τ : List X) → (p : a ∈ τ ++ σ) → s τ p // x ≡ s (x ∷ τ) (there p))
      → Γ σ
    glue-preimage₀
      : {σ : List X} {a : X}
      → (s : (τ : List X) → a ∈ τ ++ σ → Γ (τ ++ σ))
      → (f : (x : X) (τ : List X) → (p : a ∈ τ ++ σ) → s τ p // x ≡ s (x ∷ τ) (there p))
      → (τ : List X) (p : a ∈ τ ++ σ) → glue-preimage s f //* τ ≡ s τ p
    glue-preimage₁
      : {σ : List X} {a : X}
      → (s t : Γ σ)
      → ((τ : List X) → a ∈ τ ++ σ → s //* τ ≡ t //* τ)
      → s ≡ t

{-
Constant : Set → Sheaf
Constant A = record
  { presheaf = record
    { Γ = λ σ → Good (λ _ → A) σ
    ; _//_ = λ p x → lemma-monotonic (λ _ → A) (λ σ z x → z) _ p x
    }
  ; glue-total = Total
  ; glue-total₀ = λ s x → refl
  ; glue-total₁ = {!!}
  ; glue-preimage = λ s _ → Preimage s
  ; glue-preimage₀ = {!!}
  ; glue-preimage₁ = {!!}
  }
-}

_///_ : Presheaf → List X → Presheaf
E /// σ = record
  { Γ    = λ τ → Γ E (τ ++ σ)
  ; _//_ = λ s x → _//_ E s x
  }
  where
  open Presheaf

record PresheafMorphism (E E' : Presheaf) : Set where
  open Presheaf E
  open Presheaf E' renaming (Γ to Γ'; _//_ to _//'_)

  field
    omap : {σ : List X} → Γ σ → Γ' σ
    fmap : {σ : List X} {x : X} {s : Γ σ} → omap (s // x) ≡ omap s //' x

{-
_⇒_ : Presheaf → Presheaf → Presheaf
E ⇒ F = record
  { Γ    = λ σ → PresheafMorphism (E /// σ) (F /// σ) 
  ; _//_ = λ {σ} mor x → record { omap = λ {τ} s →  {!!} ; fmap = {!!} }
  }
  where
  open PresheafMorphism
-}


{-
[x,y,z] meint: das Offene, wo f(0) = x, f(1) = y, f(2) = z

zum Beispiel werden wir haben: Good (λ xs → in xs kommt irgendwo a vor) []
zum Beispiel werden wir haben: Good (λ xs → die Länge von xs ist ≥ 5)   []
-}

{-
data _≤_ : List X → List X → Set where
  base : {σ : List X} → σ ≤ []
  step : {σ τ : List X} {x : X} → σ ≤ τ → (x ∷ σ) ≤ τ

tr : {α β γ : List X} → α ≤ β → β ≤ γ → α ≤ γ
tr base base = base
tr (step p) q = step (tr p q)

lemma : {τ σ σ' : List X} → τ ≤ σ → τ ≤ σ' → σ ≤ σ' ⊎ σ' ≤ σ
lemma base p' = inj₂ base
lemma (step p) base = inj₁ base
lemma (step p) (step p') = lemma p p'
-}

-}

-}