[Agda] 'finitely supported' constructively and without decidable equality

[Jacques Carette]

On 2017-01-10 10:20 AM, Nils Anders Danielsson wrote:

> On 2016-12-30 16:02, Jacques Carette wrote:
>> I have used
>>     B : Pred A o
>>     finite : Σ ℕ (λ n → (Σ A B ↣ Fin n))
>>
>> to define a "finitely supported subset of A" which 'works', but is
>> extremely awkward to work with.
>
> Is A an h-set, and is B h-propositional?

I am doing this in MLTT rather than HoTT, so I don't have an explicit 
h-level for A.  One question is whether I need to restrict A somehow -- 
such as being an h-set.  B is just my way of trying to encode 'finitely 
supported' and is not essential to my actual situation.

The context is that I am to build, in Agda, various free objects. For 
example, one can show (using the categories package) that List, as a 
Functor, is left adjoint to the forgetful functor from Monoid to Sets.  
No additional assumptions are needed.  On the other hand, the left 
adjoint to the forgetful functor from *Commutative* Monoid to Sets is 
*finitely supported* Multisets (rather than just Multisets).

My real aim is to find a good representation to this left adjoint 
functor.  As far as I can tell, unlike for Monoid, this does not work 
for an arbitrary type A.  Basically because one can induce an 
equivalence relation on A from the Multiset structure.  Also, the 
required 'singleton' constructor (part of the adjunction data) is 
challenging (impossible?) to build without some additional structure on A.

Jacques