<div dir="ltr"><div>I'm wondering if there are general guidelines as to when to use sized types vs. just using natural numbers as fuel/index.</div><div><br></div><div>** My Problem **</div><div>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.<br></div><div>↑ sz ≟ ↑ sz'</div><div>or ↑ sz ≟  sz'</div><div><br></div><div>** My Questions **</div><div><br></div><div>* 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? <br></div><div><br></div><div>* How does unification work with sizes? Why do the above unifications fail? Is ↑ not injective?<br></div><div><br></div><div>* How does the subtyping work with sizes? Is T i < T (i ⊔ˢ j)? <br></div><div>Or (T i) < (T j) when i : Size< j? Or do I need to write manual "size-lifting" functions?<br></div><div><br></div><div>* Does --without-K or --cubical interact with sized types in a weird way?</div><div><br></div><div>* Is there a general way to write a fixed-point combinator in with sized types? Something like:</div><div>  mu : (A : Size -> Set) -> ( (i : Size) -> A i -> A (↑ i) ) -> (j : Size) -> A j<br></div><div><br></div><div>* Likewise, is there any way to write a sized-version of a type-fixed point combinator (Mu : (Set -> Set) -> Set)<br></div><div><br></div><div>Thanks!<br></div></div>