Recall like I was saying here that if you have a relation ≤ on some type A, and you know to be reflexive and transitive, and a predicate p on A, then you can build a variant of p, call it q, by saying
q(x) = Πy:A. y ≥ x → p(y)
and you find that q restricts p, and is monotone:
1) if q(x), then p(x)
2) if x ≤ y, and q(x), then q(y)
If you want q to be antitone instead of monotone, that's easy, too, you could say:
q(x) = Πy:A. y ≤ x → p(y)
and get
1) if q(x), then p(x)
2) if x ≤ y, and q(y), then q(x)
Ok, let's say that instead of a single-place predicate p on A, you have a relation R : A → A → type, and you want to build a relation out of that, and have it be antitone in the first argument, and monotone in the second. No big deal! We just define S : A → A → type like so:
S(x, y) = Πw:A. w ≤ x → Πz:A. z ≥ y → R(w, z)
and we find
1) if S(x, y), then R(x, y)
2a) if x ≤ y, and S(y, z), then S(x, z)
2b) if S(x, y), and y ≤ z, then S(x, z)
Note how I wrote 2a and 2b to look like ways of saying that S is kind of transitive, at least in the sense of ≤ acting on it on either end.
Okay, let's say we'd like S to be reflexive also. What we can do is make a choice of R to force this to be true. Consider what S(x, x) is. It's this:
S(x, x) = Πw:A. w ≤ x → Πz:A. z ≥ x → R(w, z)
The obligation is to build up something of type R(w, z) when all we know is that w is less than x, and z is greater. So let's just make that the set of data needed to make R:
R(w, z) = Σa:A. w ≤ a ∧ a ≤ z
So now all we've accomplished is we made up a type family S, defined by
S(x, y) = Πw:A. w ≤ x → Πz:A. z ≥ y → Σa:A. w ≤ a ∧ a ≤ z
and we can observe that it has the properties
1) S(x, x)
2a) if x ≤ y, and S(y, z), then S(x, z)
2b) if S(x, y), and y ≤ z, then S(x, z)
And this is all assuming that ≤ is transitive in the first place.
But now, to tie the knot, we erase the whole whiteboard, and start over by making the following recursive type definition of ≤:
x ≤ y := Πw:A. w ≤ x → Πz:A. z ≥ y → Σa:A. w ≤ a ∧ a ≤ z
It surprised me that you can then actually prove that this relation is reflexive and transitive.
Reflexivity is trivial because we shoved in that sigma-type there. A term of type Πx. x ≤ x is:
λxy.λw.λD:(w ≤ x).λz.λE:(z ≥ x).〈x,〈D, E〉〉
There's at least two evident ways to prove transitivity, because you have to make an arbitrary choice of ordering between two operations. What x ≤ y is really saying is that the "gap" between x and y can be shrunk to a point, for the purposes of a larger path starting somewhere before x and ending after y. There's two gaps I need to shrink during the transitivity proof, and I have a choice of which one I shrink first.
So if I know that w ≤ x and x ≤ y, and I want to show that w ≤ y, then I start out by abstracting over a "prefix" v ≤ w and a "suffix" y ≤ z. Here's the whole picture:
v ≤ w ≤ x ≤ y ≤ z
I can now either
1) expand the definition of w ≤ x to find an m such that v ≤ m ≤ y, and then expand the definition of m ≤ y (knowing that v ≤ m and y ≤ z) to find an n such that v ≤ n ≤ z, finishing the proof, or
2) expand the definition of x ≤ y to find an m such that w ≤ m ≤ z, and then expand the definition of w ≤ m (knowing that v ≤ w and m ≤ z) to find an n such that v ≤ n ≤ z, finishing the proof.
