SmithParadoxSmith’s paradox [1] is a proof that there exist non-admissible types, that is, types that cannot be used with fixpoint induction.
inadmissible_type : exists (a : U 0) . not (admiss a)
One such type is the type of partial functions from nat to unit:
{ h : nat -> partial unit | not (forall x . halts (h x)) }
Let T be this type, and let f be the function:
fn g x . if x =? 0 then () else g (x - 1)
Since f defers to its argument g, it preserves partiality. Thus
one can show that f : partial T -> partial T. If T were
admissible, we could conclude by fixpoint induction that
fix f : partial T. However fix f clearly halts, so it would
follow that fix f : T. That would mean fix f is a partial
function, but it is easy to show that fix f is actually total.
[1] Scott Fraser Smith. Partial Objects in Type Theory. Ph.D. dissertation, Cornell University. 1989.