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

[Joey Eremondi]

I'm wondering if there are general guidelines as to when to use sized types
vs. just using natural numbers as fuel/index.

** My Problem **
I've tried adding sized types to a proof I'm working on to establish an
explicit termination argument. However, in case splits I'm getting stuck on
unification problems like this.
↑ sz ≟ ↑ sz'
or ↑ sz ≟  sz'

** My Questions **

* Is there a general guideline for when to use sizes vs nats? Do sized
types give us anything Nats don't, other than having a solver, ∞ and some
implicit niceness? Or do they make the type theory strictly more powerful?

* How does unification work with sizes? Why do the above unifications fail?
Is ↑ not injective?

* How does the subtyping work with sizes? Is T i < T (i ⊔ˢ j)?
Or (T i) < (T j) when i : Size< j? Or do I need to write manual
"size-lifting" functions?

* Does --without-K or --cubical interact with sized types in a weird way?

* Is there a general way to write a fixed-point combinator in with sized
types? Something like:
  mu : (A : Size -> Set) -> ( (i : Size) -> A i -> A (↑ i) ) -> (j : Size)
-> A j

* Likewise, is there any way to write a sized-version of a type-fixed point
combinator (Mu : (Set -> Set) -> Set)

Thanks!
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200421/a261063b/attachment.html>