reflection

[ivoysey]

from the old todo file:

• reflection: generate mapreduces, so that makes tcomplete and ecomplete
  effectively just

    (mapreduce τ̇) (\ <||> = ⊥ | _ = ⊤) (_×_)
    (mapreduce ė) (\ <||> = ⊥ | <| _ |> = ⊥ | _ = ⊤) tcomplete (_×_)

  generate e^ and t^ from e and t, both erasure erasure functions, matched
  for both. what else? probably the movement rules.

  need newer version of agda to do reflection, which will probably break
  other proofs we've done so far because of backwards compatiblity issues.

[ivoysey]

migrating this to the issue tracker repo.