
[Jul. 1st, 201308:47 pm]
Jason

Here's a thing I don't know what to make of:
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 naturalfeeling 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 naturalfeeling 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. 

