jonsterling / agda-effectful-forcing Goto Github PK

something miniature that contains only what I need.

One option would be to use the existing oracle and prune the trees like Escardó did; but we could also just add another oracle for the Cantor space, and generalize the proof of the bar theorem so that it can be instantiated at any spread for which we have an oracle. This could be a bit more elegant possibly...

Interpreting test at 0,1,2,... result in 0, but it equals 1. Clearly I've screwed this up 😉

  add : 𝓛.TΩ ▹ Ctx.⋄ ⊢ᵀ ` nat ⇒ ` nat ⇒ ` nat
  add = rec[ ` nat ] · ƛ succ

  test : 𝓓.𝓑 Nat
  test = ⟦ add · (Ω · zero) · (Ω · zero) ⟧₀

Vincent Rahli has informed me that the oracle only needs to exist in the semantics, not the syntax as far continuity is concerned. I think the same can work for the bar principle. So we ought to be able to remove the oracle from the language, and work entirely with vanilla System T, and establish a logical relation between the standard & dialogical interpretations.

For instance, succ and rec are "functions" rather than operators. It would be a bit clearer to do this in the modern style, where they are operators that take subterms.

We don't need them, but they're part of System T proper, so we might as well demonstrate them.

This is as simple as relabelling the mental construction into the motive, see https://github.com/jonsterling/agda-bar-induction/blob/master/src/BarTheorem.agda#L74

This is necessary to fill in the last hole of the Bar Theorem

Proving coherence is a bit tricky with the current style; not sure if the definition is just wrong, or if it is merely difficult.

It might be worthwhile to take another look at proving the bar theorem using Escardó's representation. In this case, instead of lists as approximations, we'd have lists with a bunch of holes in them.