Suppose I'm living in LF and I have some type

i : type.

of individuals, and let's say I have a relation

<= : i -> i -> type.

on i, and I want a predicate

c : i -> type.

to be

**monotone**in i, in the sense that

{x : i}{y : i} x <= y -> c(x) -> c(y).

Well, I could just throw in an axiom that says exactly that, but let's say I don't want to do that. I want to instead define c to be some type family expression that in some natural-feeling way has that property fall out of its definition.

**If**I knew that <= was transitive, say if I had

trans : X <= Y -> Y <= Z -> X <= Z.

then there's a nice way of doing this. I make up a new predicate d, and define c like so:

d : i -> type.

c = [x : i] {y : i} x <= y -> d(y).

In this case, I can prove {x : i}{y : i} x <= y -> c(x) -> c(y) by just writing a program

M : {x1 : i}{x2 : i} x1 <= x2 -> c(x1) -> c(x2) =

[x1][x2][p1 : x1 <= x2][t : {y : i} x1 <= y -> d(y)]

[y : i][p2 : x2 <= y] t y (trans p1 p2)

Okay, done! Except I still feel unsatisfied for some reason that I had to axiomatize <= to be transitive.

Let's say I don't want to do that. I want to instead define <= to be some type family expression that in some natural-feeling way has transitivity fall out of its definition.

How 'bout I make up a predicate

r : i -> type.

and define

<= : i -> i -> type = [x1][x2] r(x1) -> r(x2).

Then transitivity is just function composition.

Combining this definition with that of c, I get

c(x) = {y : i} (r(x) -> r(y)) -> d(y)

which looks suspiciously similar to (but not quite isomorphic to) the encoding

(↑P)* = ∀x. (P* ⇒ #(x)) ⇒ #(x)

that I've been dealing with so much lately, and that's the thing I'm not sure what to make of.