I asked a pretty vague question. I wasn't able to make it precise, but I can now. It seems to be out of the scope of the previous question, so I open another one.

In dependently-typed languages such as Agda or Idris, it's possible to define a universe inductive-recursively. However, W-types are known to have bad computational characteristics in traditional intensional type theories. Therefore, you need to be able to add new definitions of inductive data types anytime.

My question is, will HoTT improve this situation? That is, to have a closed universe. I know the general formulation of HIT is yet to be discovered, and that people seem not to be able to figure out induction-recursion, so I kind of suspect an definitive answer in the status quo. Still going to give it a chance though.

  • $\begingroup$ I don't think that the universe of (all) types can exist. By closed, do you mean closed under $\Pi$ and $\Sigma$? Or that $U:U$? Or that all the possible inductive types are in it even if you don't define them? $\endgroup$
    – xavierm02
    Jan 20 '17 at 14:51
  • $\begingroup$ I mean all inductive types. I'm asking if there could be some "universal inductive type" and all other inductive types are encoded with it. $\endgroup$
    – 盛安安
    Jan 20 '17 at 14:55
  • $\begingroup$ Well, maybe all inductive types except itself obviously. $\endgroup$
    – 盛安安
    Jan 20 '17 at 15:01
  • $\begingroup$ I realized if you can define a universe with induction-recursion, your universal inductive type must be able to encode it, and it's not consistent ... $\endgroup$
    – 盛安安
    Jan 20 '17 at 15:07

I'm uncertain what you're referring to exactly, but I can remark on a few things.

The first is that the usual problem with W-types is that encoding inductive types with them does not necessarily give you the right induction principles. For instance, we can try to define the natural numbers like so:

F : 2 → Type
F 0 = ⊥
F 1 = ⊤

ℕ : Type
ℕ = W 2 F

zero : ℕ
zero = sup 0 absurd

suc : ℕ → ℕ
suc n = sup 1 (const n)

induction : (P : ℕ → Type) → P zero → (∀ n. P n → P (suc n)) → ∀ n. P n
induction pz ps n = ???

The problem we'll run into is that induction on $W$ and $2$ allows us to observe the case $n = {\tt sup}\ 0\ f$, but we only have a proof of $P\ ({\tt sup}\ 0\ {\tt absurd})$. So we'll need a way to prove that $f = {\tt absurd}$, but there is no such principle in normal intensional type theory.

The answer to your question in this regard is that homotopy type theory does help in this regard, because e.g. univalence implies extensional equality of functions (and cubical type theory also includes this, for instance). So we should not have as many problems recovering the 'right' induction principles for $W$ based encodings.

However, another answer is that we didn't actually need this to begin with. This problem is somewhat particular to the specifics of $W$. Instead, we could use a more complex type of 'descriptions' of inductive definitions together with a decoding to a more 'first-order' representation of the container functor used in the $W$ definition. This approach is used in The Gentle Art of Levitation, which says it does not require extensional equality of functions (I believe).

This technique is also detailed in Ambrus Kaposi's thesis, which shows what sort of codes you need for inductive-recursive and inductive-inductive definitions.

The (I think) counter-intuitive bit about these systems is that they seem to actually be capable of describing themselves, and that this is not (it seems) contradictory.

So, it seems like we are relatively close to knowing how to to include most (commonly desired) definitions in type theory as a universe of descriptions with a 'decoding' function, instead of taking some universes to be open with respect to special definition forms. And this fact is somewhat independent of any features that homotopy type theory would have. I don't know of any system like Agda or Idris has this methodology on their roadmap, though.

I should say, there are potential traps, still. For instance, each universe Set i in Agda is called "Mahlo," because it admits inductive-recursive definitions. There are stronger universes known than Mahlo universes, too, which will in turn have (many) Mahlo universes within them. But the sort of 'universe' you define with induction-recursion cannot be Mahlo, because it is inconsistent for a Mahlo universe to have an induction principle. So any theory incorporating strong-than-Mahlo universes would at least need a different sort of 'description' system for those.

  • 1
    $\begingroup$ In your example, did you forget to provide P or at least its type? $\endgroup$ Sep 20 '18 at 5:55
  • $\begingroup$ It seems I did. Fixed. $\endgroup$
    – Dan Doel
    Sep 20 '18 at 11:45
  • $\begingroup$ You dont' actually need all of function extensionality, just an appropriate equation governing absurd. But I agree that's a hack. $\endgroup$ Sep 20 '18 at 13:33

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.