{α : Type v} →
  (Target : Type u) →
    (deflate : α → Target) →
      (inflate : Target → α) →
        (∀ {a : Target}, deflate (inflate a) = a) →
          (∀ {a : α}, inflate (deflate a) = a) → Std.Internal.ComputableSmall α