{-# OPTIONS --without-K #-}

module BarTheorem where

open import Basis
open import Spread.Baire
open import Securability
open import SystemT.Syntax
open import SystemT.Semantics
open import Dialogue as 𝓓 hiding (module ⊒)

module BarTheorem (𝔅 : Species) (𝔅-mono : monotone 𝔅) where

  -- The content of Brouwer's Bar Theorem is that if we have a functional that
  -- will compute for any point Ξ± the length of the first approximation U β‰Ί Ξ±
  -- that is in the species Ο†, then we can well-order this insight into a
  -- mental construction that Ο† is a bar.
  bar-theorem
    : (F : βŠ’α΅€ (nat β‡’ nat) β‡’ nat)
    β†’ F ⊩ [] β—ƒα΅€ 𝔅
    β†’ [] β—‚ 𝔅
  bar-theorem F =
    readback [] (𝓓.norm (tmβŸͺ F βŸ«β‚€ 𝓓.generic))
      ∘ eval F

    where
      eval
        : (F : βŠ’α΅€ (nat β‡’ nat) β‡’ nat)
        β†’ F ⊩ [] β—ƒα΅€ 𝔅
        β†’ norm (tmβŸͺ F βŸ«β‚€ generic) ⊩ [] β—ƒ 𝔅
      eval F p Ξ± =
        ≑.coe*
         (Ξ» β–  β†’ 𝔅 (Ξ± [ β–  + 0 ]))
         (≑.seq
          (Coh.hauptsatzβ‚€ _ F _ generic Ξ» ⟦n⟧ βŸͺn⟫ ⟦n⟧∼βŸͺn⟫ β†’
           ≑.seq
            (≑.cong Ξ± ⟦n⟧∼βŸͺn⟫)
            (𝓓.⊒.generic-diagram Ξ± βŸͺn⟫))
          (𝓓.⊒.coh (tmβŸͺ F βŸ«β‚€ generic) Ξ±))
         (p Ξ±)

      0β‹― : Point
      0β‹― _ = 0


      readback/Ξ·
        : {U : Node}
        β†’ (k : β„•)
        β†’ spit k ⊩ U β—ƒ 𝔅
        β†’ U β—‚ 𝔅
      readback/Ξ· zero f =
        spit
         (≑.coe* 𝔅
          (Point.⊒.prepend-take-len _)
          (f 0β‹―))

      readback/Ξ· (suc n) f =
        bite Ξ» x β†’
        readback/Ξ· n Ξ» Ξ± β†’
        ≑.coe* 𝔅
         (Point.⊒.take-cong
          (Point.⊒.su-+-transpose _ _)
          (Ξ» _ β†’ refl))
         (f (x <∷ α))


      readback
        : (U : Node)
        β†’ (m : 𝓓.𝔅 β„• β„•)
        β†’ m ⊩ U β—ƒ 𝔅
        β†’ U β—‚ 𝔅

      readback U (spit n) f =
        readback/Ξ· n f

      readback U (bite ΞΊ) f =
        bite Ξ» x β†’
        readback _ (ΞΊ x) Ξ» Ξ± β†’
        ≑.coe*
          (𝔅 ∘ U <++ x <∷ Ξ± [_])
          (Point.⊒.su-+-transpose _ 𝔅[ ΞΊ x β‹„ Ξ± ])
          (𝔅-mono (f (x <∷ Ξ±)))


  -- The Bar Induction Principle is a corollary to the Bar Theorem.
  module Induction
    (𝔄 : Species)
    (π”…βŠ‘π”„ : 𝔅 βŠ‘ 𝔄)
    (𝔄-hered : hereditary 𝔄)
    where

      relabel
        : (U : Node)
        β†’ (U β—‚ 𝔅)
        β†’ 𝔄 U

      relabel U (spit x) =
        π”…βŠ‘π”„ U x

      relabel U (bite m) =
        𝔄-hered Ξ» x β†’
        relabel (U ⌒ x) (m x)


      induction
        : (F : βŠ’α΅€ (nat β‡’ nat) β‡’ nat)
        β†’ F ⊩ [] β—ƒα΅€ 𝔅
        β†’ 𝔄 []
      induction F =
        relabel []
        ∘ bar-theorem F