?
Notes from a Medium-Sized Island [entries|archive|friends|userinfo]
Jason

[ website | My Website ]
[ userinfo | livejournal userinfo ]
[ archive | journal archive ]

[Jul. 1st, 2013|08:47 pm]
Jason
[Tags|]

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 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.
LinkReply