Show and Arbitrary for Function Types?

[ana-brendel]

Considering the type:
Definition total_map (A:Type) := nat -> A.

Assuming that as a default, we let A be nat. Is there any support for "showing" an instance of this type? I can imagine that to prove decidability you could define equality as f1 = f2 <-> forall n, f1 n = f2 n and the this would easy to prove decidability for because nat is decidable. Similar for a generator, we could just generate nats and populate the function. But, I am not sure if it is possible to show an instance of a total_map. Is it? Or is there some support for it?

[liyishuai]

#64 (comment)
@lemonidas @Lysxia Maybe worth adding an example for CoArbitrary?