[Agda] Nat Fuel vs Sized Types (and other Sized Type questions)

[Nils Anders Danielsson]

On 2020-04-22 05:56, Joey Eremondi wrote:
> I'm wondering if there are general guidelines as to when to use sized
> types vs. just using natural numbers as fuel/index.

Two data points:

* I have found it practical to use sized coinductive types, together
   with explicit definitions of (strong or weak) bisimilarity.

* I have found it less practical to use sized inductive types with
   /relevant/ size arguments together with propositional equality.

-- 
/NAD