Some minor refactoring surrounding Dedekind reals

[fredrik-bakke]

Arising from a discussion on the Discord earlier today, here are some mild refactors.

• Touch up file about Dedekind reals
• Rename disj to disjunction (disambiguates from disjoint)
• Rename conj to conjunction (disambiguates from conjugation)
• Introduce _⇒_ notation for type-implication-Prop. This is consistent with the already-established _⇔_

[fredrik-bakke]

Turns out we have 3 different names for implication at the moment:

• function-Prop
• hom-Prop
• implication-Prop

This seems a little overkill to me.

[fredrik-bakke]

For fun, here's what is-dedekind-cut-Prop could look like with our currently defined notations:

  is-dedekind-cut-Prop : Prop (l1 ⊔ l2)
  is-dedekind-cut-Prop =
    ( exists-Prop ℚ L ∧ exists-Prop ℚ U) ∧
    ( Π-Prop ℚ
      ( λ q → iff-Prop (L q) (exists-Prop ℚ (λ r → le-ℚ-Prop q r ∧ L r)))) ∧
    ( Π-Prop ℚ
      ( λ r → iff-Prop (U r) (exists-Prop ℚ (λ q → le-ℚ-Prop q r ∧ U q)))) ∧
    ( ( Π-Prop ℚ (λ q → neg-Prop (L q ∧ U q))) ∧
      ( Π-Prop ℚ
        ( λ q → Π-Prop ℚ (λ r → implication-Prop (le-ℚ-Prop q r) (L q ∨ U r)))))

Notice that there are many competing conventions going on, which is not good.

[fredrik-bakke]

The competing conventions are as follows:

1. use special binary operators taking values in types: _⇔_ : Prop → Prop → UU
2. use special binary operators taking values in propositions: _∧_ : Prop → Prop → Prop
3. Use unicode symbol in name for operators with minimal assumptions of propositions. E.g. Π-Prop : (X : UU) → (X → Prop) → Prop and use textual name for the construction where more types are assumed to be props.
   E.g. ∃-Prop : (X : UU) → (X → UU) → Prop while exists-Prop : (X : UU) → (X → Prop) → Prop

[fredrik-bakke]

I eliminated convention 2 by making _∨_ and _∧_ take values in types, although I think it could still be useful. It is not currently clear to me how to implement convention 2 consistently, however.

[fredrik-bakke]

To be clear, there is quite a bit of refactoring left to do regarding the definition of Dedekind cuts, but I don't have time for that currently.

[VojtechStep]

LGTM