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

module BarTheorem where

open import Basis
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

: {U : Node}
β (k : β)
β spit k β© U β π
β U β π
spit
(β‘.coe* π
(Point.β’.prepend-take-len _)
(f 0β―))

bite Ξ» x β
β‘.coe* π
(Point.β’.take-cong
(Point.β’.su-+-transpose _ _)
(Ξ» _ β refl))
(f (x <β· Ξ±))

: (U : Node)
β (m : π.π β β)
β m β© U β π
β U β π

readback U (spit 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
```