Competing conventions for operations on propositions

[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

Originally posted by @fredrik-bakke in #983 (comment)

[fredrik-bakke]

We could reconcile 1 and 2 by introducing some modifier symbol like ᴾ for operators that take values in propositions. Although this does not feel very agda-unimathy to me, we do do something similar for decidable embeddings already with ↪ᵈ

[VojtechStep]

I don't have experience with that part of the codebase, but I think I'd expect logical connectives to be composable. It's kinda surprising to not be able to do A ∧ B ∧ C (what's the point of specifying fixity then?), so I'd be in favor of having infix operators valued in Prop

[fredrik-bakke]

I want to note that there is still a conflict that arises when considering the current usage of ∃. There is also a conflict with the hypothetical _∈_. This leads me to believe that perhaps precisely what we need is adding a disambiguative symbol like ᴾ.

[fredrik-bakke]

We also do this for pointed types I just realized.

[fredrik-bakke]

Here's an example usage for size:

  is-dedekind-cut-Prop : Prop (l1 ⊔ l2)
  is-dedekind-cut-Prop =
    ( ∃ᴾ ℚ L ∧ᴾ ∃ᴾ ℚ U) ∧ᴾ
    ( ∀ᴾ ℚ (λ q → L q ⇔ᴾ (∃ᴾ ℚ (λ r → (q <ᴾ-ℚ r) ∧ᴾ L r)))) ∧ᴾ
    ( ∀ᴾ ℚ (λ r → U r ⇔ᴾ (∃ᴾ ℚ (λ q → (q <ᴾ-ℚ r) ∧ᴾ U q)))) ∧ᴾ
    ( ∀ᴾ ℚ (λ q → ¬ᴾ (L q ∧ᴾ U q))) ∧ᴾ
    ( ∀ᴾ ℚ (λ q → ∀ᴾ ℚ (λ r → (q <ᴾ-ℚ r) ⇒ᴾ (L q ∨ᴾ U r))))

It goes without saying that I would still much rather have this definition be in terms of conjunctions of more general predicates like is-lower-set-Subposet and so on (perhaps with intermediate definitions for is-lower-rounded and so on)