How can I change the work of forall in agda?

Question

I work with a pair of Streams of Rationalities, Say, (L, R), where L and R are the stream of rationals. There are three conditions that L and R must satisfy in order to say that they are valid. I wrote the code as ..

isCut_ : cut → Set
isCut x = (p q : pair ) → 
              if((((p mem (getLC x)) ∨ (p mem (getRC x)))) ∧ 
                ((not (p mem getLC x)) ∨ (not (p mem getRC x))) ∧ 
                (not (p <pair q) ∨ ((p mem getLC x) ∨ (q mem getRC x))))then ⊤
              else ⊥

I really wanted to change the return type of this function to Bool. Here, the truncated means (L, R) and mem are members.

The problem coming from forall p q which expect return type to be Set. How do I contact to get the desired result.

Answer 1

You can write something like the following:

isCut : cut → (p q : pair) → Bool
isCut x p q = (((p mem (getLC x)) ∨ (p mem (getRC x))))
            ∧ ((not (p mem getLC x)) ∨ (not (p mem getRC x)))
            ∧ (not (p <pair q) ∨ ((p mem getLC x) ∨ (q mem getRC x))))