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.