Replace use of impossible idiom with proof by reflection

[wenkokke]

The purpose of this WIP pull request is to slowly remove all usage of the impossible idiom by proof-by-reflection. A new development in Agda has made it possible to do this without using instance search.

• define product and unit types as records in Connectives;
• explain difference between data and records w.r.t. definitional equality in Connectives;
• define True in Decidable;
• add exercise for defining False in Decidable;
• replace S constructor in Lambda with a version which checks the inequality implicitly;

[wadler]

Nice!
I like the use of monus as an example.
"it is very painful to use" --> "it is painful to use"
"know the two numbers statically" --> "at the point minus is called"
"The trick is ..." Recall the definition of T (as a sentence, not code) and give a backwards reference to the place it is defined.
"For instance, _n≤m_254 : ⊥." --> "For instance, if we call 3 - 5 we get "
"We obtain ..." Same for toWitness. Possibly restructure, to do this for T and toWitness together.
"as long as we statically know the two numbers" --> "as long as we provide known numbers"
Explain how you can write x - y where x and y are known variables. I presume we can write something like
minus : (m n : ℕ) (n≤m : n ≤ m) → ℕ
minus m n n≤m = - m n {f n≤m}
for a suitable choice of f?
The exercise refers to True, but the text refers to T.

[wenkokke]

Explain how you can write x - y where x and y are known variables. I presume we can write something like
minus : (m n : ℕ) (n≤m : n ≤ m) → ℕ
minus m n n≤m = - m n {f n≤m}
for a suitable choice of f?

This technique is really only useful when both arguments to _-_ are literals. I'd prefer not to pretend that it has any value if you have any evidence that n ≤ m for two variables n and m, as the whole point is the fact that Agda can compute the answer for you, which goes out the window if you have to provide explicit evidence.

Furthermore, _-_ is defined in terms of minus, so your code here ties a strange loop?

The exercise refers to True, but the text refers to T.

True is defined just before the exercise and is distinct from T.

[wenkokke]

@wadler This is now done. Could you review the changes?