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.
Tags:

• #### (no subject)

A paper on describing circuits in an agda DSL: http://www.staff.science.uu.nl/~swier004/publications/2015-types-draft.pdf

• #### (no subject)

Going more carefully now through this little tutorial on fpga programming with the iCEstick. It's in spanish, which makes it slightly more…

• Post a new comment

#### Error

Anonymous comments are disabled in this journal

default userpic