Dedekind reals are arithmetically located

[lowasser]

The last, and hardest, lemma we need to add reals.

[lowasser]

Well, we pulled out some lemmas, but they're merged now, so we can come back to this.

[lowasser]

I could only find one place to use map-exists here, but maybe there are others.

[fredrik-bakke]

I could only find one place to use map-exists here, but maybe there are others.

I think you should be able to invoke a map-quaternary-exists, if that had been defined, in arithmetically-located-ℝ. Otherwise, you could replace the three innermost calls to elim-exists with map-ternary-exists

[lowasser]

I don't think we can do anything as neat as you're suggesting.

The main issue is with which existential statements depend on each other. The choice of ε', p, and q are all independent, but the object being shown to exist depends on an existential that depends on all three of those in turn; map-ternary-exists certainly can't handle cases where either a) the object being shown to exist is not a function of the three arguments, b) any of the existential arguments have dependencies on another.

So we can use a map-ternary-exists to combine those three into just a tuple type together, and then we can do some work with that existential, and I guess that reduces the nesting level somewhat, but I think that's the best we can do.

[lowasser]

I've done what I believe is the best possible.

[VojtechStep]

I think this situation with elim-exists is worth exploring, and I don't think adding map-exists-nary is the way. We could use Agda's do notation, which works similarly to Haskell's — it desugars do x <- a; k to a >>= \ x -> k, but it's a BYOB (bring your own bind) in the sense that it will just use whatever _>>=_ you have in scope. We haven't done anything with it, but you can try temporarily adding a

where
  _>>=_ : {l1 l2 : Level} {A : UU l1} {B : A -> UU l2} -> exists-structure A B -> (Sigma A B -> type-Prop claim) -> type-Prop claim
  x >>= f = elim-exists claim (ev-pair f) x

to your definition (replacing Sigma with the Greek symbol, I'm on my phone), and see if it helps with readability

[lowasser]

@VojtechStep , that was incredibly effective. Thanks!

[lowasser]

Should I fold this into a PR for addition of reals in general?

[lowasser]

I'm going to do that.