Dan Doel dan.doel at gmail.com
Thu Dec 23 20:22:20 CET 2010

```On Thursday 23 December 2010 12:52:07 pm Daniel Peebles wrote:
> Fair enough :) that'll teach me to hypothesize something without thinking
> about it! I guess I could amend my coinductive proof:
>
> http://hpaste.org/paste/42516/mirrormirror_with_bottom#p42517
>
> does that cover bottom-ness adequately? I can't say I've thought through it
> terribly carefully.

That isn't the usual way to model partially defined values. For instance, you
can write functions with that datatype that would not be monotone:

pdefined :: {A : Set} -> Tree A -> Bool
pdefined ⊥ = false
pdefined _ = true

It's somewhat more accurate to take the partiality monad:

data D (A : Set) : Set where
now   : A -> D A
later : ∞ (D A) -> D A

⊥ : {A : Set} -> D A
⊥ = later (♯ ⊥)

Then we're interested in an equivalence relation on D As where two values are
equal if they either both diverge, or both converge to equal inhabitants of A
(not worrying about how many steps each takes to do so).

Then, the partially defined trees are given by:

mutual {A}
Tree = D Tree'

data Tree' : Set where
node : Tree -> A -> Tree -> Tree'
tip  : Tree'

And equivalence of these trees makes use of the above equivalence for D-
wrapped things. (It's actually a little weird that this works, I think, if you
expect Tree' to be a least fixed point; but Agda does not work that way).

If you're just interested in proving mirror (mirror x) = x, though, this is
probably overkill. Your original type should be isomorphic to the Haskell type
in a set theoretic way of thinking, and the definition of mirror does what the
Haskell function would do at all the values. So the fact that you can write
functions on that Agda type that would have no corresponding implementation in