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

[Andrew M. Pitts]

> On 24 Apr 2020, at 10:41, Nils Anders Danielsson <nad at cse.gu.se> wrote:
> 
> 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.

I and my co-authors can’t seem to do without sized inductive types in the recent paper <https://www.cl.cam.ac.uk/~amp12/papers/coniqi/coniqi.pdf>

But our enthusiasm for sized types in Agda was severely dampened when we learned later that in current versions they allow one to prove that true equals false :-( — see <https://github.com/agda/agda/issues/3026>. 

Andy Pitts