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

module Securability where

open import Basis

open import Spread.Baire
open import Dialogue as ๐““
open import SystemT.Syntax
open import SystemT.Semantics

infixl 4 _โ—‚_

-- A Brouwerian mental construction to verify that a node is securable.
data _โ—‚_ (U : Node) (ฯ† : Species) : Set where
  spit : ฯ† U โ†’ U โ—‚ ฯ†
  bite : (โˆ€ x โ†’ U โŒข x โ—‚ ฯ†) โ†’ U โ—‚ ฯ†

-- Proof that a dialogue computes the securability of a node.
_โŠฉ_โ—ƒ_
  : ๐”… โ„• โ„•
  โ†’ Node
  โ†’ Species
  โ†’ Set
d โŠฉ U โ—ƒ ฯ† =
  (ฮฑ : Point)
    โ†’ ฯ† (U <++ ฮฑ [ ๐”…[ d โ‹„ ฮฑ ] + โˆฃ U โˆฃ ])

_โŠฉ_โ—ƒแต€_
  : โŠขแต€ (nat โ‡’ nat) โ‡’ nat
  โ†’ Node
  โ†’ Species
  โ†’ Set
F โŠฉ U โ—ƒแต€ ฯ† =
  (ฮฑ : Point)
    โ†’ ฯ† (U <++ ฮฑ [ tmโŸฆ F โŸงโ‚€ ฮฑ + โˆฃ U โˆฃ ])