[Agda] Restrictions on 'with' introductions?

[Nils Anders Danielsson]

On 2014-10-07 02:31, Dan Krejsa wrote:
> (The 'ordered' bit goes through pretty easy, but the 'permutation' bit
> is proving something of a pain to me.  In particular, I'm developing all the
> permutation infrastructure myself...)

Proofs of this kind are hopefully easy (but perhaps boring) if you use
the technique that I describe in "Bag Equivalence via a Proof-Relevant
Membership Relation":

   http://www.cse.chalmers.se/~nad/publications/danielsson-bag-equivalence.html

For instance, here's how one can implement tree sort, and prove that the
output is a permutation of the input:

   http://www.cse.chalmers.se/~nad/publications/danielsson-bag-equivalence/Tree-sort.Partial.html

The following code by Bob Atkey uses a different approach, embedding
linear logic inside Agda to give you the permutation property "for
free":

   https://github.com/bobatkey/sorting-types/blob/master/agda/Linear.agda

-- 
/NAD