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.
