Project Page Index Table of Contents
  • Definitions
    • Dialogue continuity
    • Intensional dialogue continuity
      • Brouwer continuity, Baire space variant of dialogue continuity
    • Tree function continuity
      • Tree function continuity via interrogations
      • Tree function continuity via interaction trees
    • Modulus continuity
  • Brouwer trees
      • Dialogue continuity implies tree function continuity
      • Tree function continuity is equivalent to tree function continuity with interrogations
      • Tree function continuity is equivalent to interaction tree continuity
    • Modulus continuity
      • Tree function continuity implies computable modulus continuity
      • Special case: If Q = nat then moduli can be nat
      • Self-modulating continuity implies tree function continuity for Q = nat
    • Tree function continuity is equivalent to self-modulating continuity when Q = nat
    • Continuity for Cantor space
      • Neighborhood continuity is equivalent to interaction tree continuity
Generated by coqdoc and improved with CoqdocJS