10
$\begingroup$

This may have been asked before, but I haven't been able to find it if so.

The induction and recursion principles for various types in (for me, at least, homotopy) type theory allow one to define a function despite having what appears to be only partial information.

For example one can prove results about (or define functions from) product types by proving those results (defining the function) only for pairs, one can prove results for $x: \textbf1$ by proving them only for $\star:\textbf{1}$, one can prove results concerning equality by only considering reflexivity.

How am I best to interpret the fact that we can do this? I've flip-flopped between three different views so far, given below, for a fair bit.

  1. Am I supposed to decide that these functions are only partially defined (whence what if I were to find elements of $\textbf{1}$ which weren't definitionally equal to $\star$?)?

  2. Am I supposed to decide that the rules simply express that there exists functions out of, say, $A\times B$ which have such results on pairs (and we just don't know what these functions will do for possible non-pairs, except that they will send them to the target).

  3. Am I supposed to see this as an assertion that the only elements of these types we will ever meet are those equal to whatever we are inducting over? (But this can't be right because the univalence axiom gives more proofs of equality that refl).

  4. Anything else?

The fact that we can prove the relevant propositional equalities using these principles doesn't really solve the problem for me, because without a proper interpretation this still very much seems as though I'm only proving this for the special objects we care about.

Which is the better, or more correct, interpretation, here? I personally prefer the second one, it seems to me as though that makes all the relevant propositions-as-types identifications more agreeable.

$\endgroup$
  • $\begingroup$ (2) is probably the best interpretation. (3) is also true, but you have to be careful. $\endgroup$ – Zhen Lin Feb 22 '16 at 20:19
  • 3
    $\begingroup$ I would say that (3) is the best interpretation, and could could even make it stronger and say "the only elements of these types that exist" -- it's not as if there are some others hanging around that you'll never meet. (Of course, this "only" is propositional/typal equality, not definitional equality.) The apparent conflict with univalence is explained in Remark 1.12.1 of the HoTT Book. $\endgroup$ – Mike Shulman Feb 23 '16 at 6:14
4
$\begingroup$

As Mike Shulman says, 3 is the best interpretation. 2, by itself, is true but is arguably not really induction (without 3). I want to go into more detail about this, but first I want to elaborate on Mike's comment with regards to identity types.

To use your wording what the elimination rule for identity types says is that for $M : A$, $\langle M,\mathbf{refl}_M \rangle$ is the only value of $\Sigma x:A.(M =_A x)$ that we'll ever see or, to use Mike's wording, that exists. The rule says no such thing about $(M =_A N)$ for given or fixed $M, N : A$. Of course, there may be inhabitants of $\Sigma x:A.(M =_A x)$ that are only propositionally but not definitionally equal to $\langle M,\mathbf{refl}_M \rangle$. But ultimately they would be like different representatives from the same equivalence class, e.g. $\frac{2}{3} = \frac{4}{6}$ even though they look different. (Though generally I think it is better to think in terms of widening what we consider equal rather than forming equivalence classes, something much easier done in type theories than in [classical] set theories with a global notion of equality.) Notice that equality varies with type and this makes a crucial difference in this case. For example, you may retort "$\langle \mathbf{base}, \mathbf{loop} \rangle$ does not equal $\langle \mathbf{base}, \mathbf{refl_{base}} \rangle$ for the circle $\mathbb{S}^1$". To which I would reply, "at what type?" At the type $\mathbb{S}^1\times(\mathbf{base} =_{\mathbb{S}^1} \mathbf{base})$, i.e. $\Sigma x:\mathbb{S}^1.(\mathbf{base} =_{\mathbb{S}^1} \mathbf{base})$, you would be right. But at the type $\Sigma x:\mathbb{S}^1.(\mathbf{base} =_{\mathbb{S}^1} x)$, you would be wrong. (If we looked at the groupoid model, what's happening is that in this case these types as groupoids (may) have the same objects but have different arrows. In particular, the latter type has more isomorphisms.)

That was a bit longer than I was expecting. Moving to induction, it may be useful to look at an example where a nominal induction rule failed to achieve this property. The main example of this is the failure of the first-order induction schema in Peano arithmetic to rule out non-standard models. (Note, Peano's original formulation used a second-order induction rule, so didn't have this problem.) The first-order induction schema says $$\frac{P(0) \qquad \forall n.(P(n) \implies P(S(n)))}{\forall n.P(n)}$$ for each $P$ that you can write down. You could view it as a macro that looks at the syntax of the property $P$ you want to check, and then expands out into a tailor-made axiom for that property. The problem, of course, is not every property in the model need be syntactically expressible. On the other hand, the second-order characterization, i.e. where we quantify over $P$, essentially says that all properties in the model obey this rule. You can think of this as saying the induction rule is "uniform" or "continuous".

The "standard" set-theoretic model for Peano arithmetic is the minimal one. The second-order rule is interpreted as saying that we are looking for the set that is the intersection of all sets $X$ for which $0 \in X$ and $n \in X \implies S(n) \in X$. Categorically, this is stated by defining the natural numbers as the initial algebra of a functor. It's unique up to unique isomorphism. In type theory, if we have a universe, we can directly state what we want to achieve, namely any other type that "behaves" like the natural numbers (i.e. provides the same constructors and induction rule) is isomorphic to the natural numbers. Below is the Agda code. It's easy to change it to have the assumed induction rule on N target a type of propositions which better fits the preceding scenarios. Making that change means the recursor, rec, must now be assumed rather than defined from ind, and we also then need to assume that N is a (h-)set, i.e. that the identity type Id n m is a proposition for any two values n and m of N. Once that is done, Nat-is-unique barely changes and we don't necessarily need to be working in a type theory with a universe. This illustrates what's going on though. Among the properties being quantified over there is, for each potential model of the naturals, the property for which the conclusion of the induction rule is that the naturals embed in this alternate model and the premises of that instance of induction are satisfiable.

For inductive families like $=_A$, but also $\leq_{\mathbb{N}}$ and the rules defining type systems and operational semantics and many other things, we are inductively defining a subset of a (product) type. For $=_A$ we are saying the subset $\{ x:A\ |\ M =_A x \}$ is inductively defined. Or equivalently, the subset $\{ \langle x,y \rangle:A\times A\ |\ x =_A y \}$ is inductively defined. In extensional type theories, this is basically exactly what is happening. In intensional type theories like HoTT, our types are not necessarily "sets" (h-sets), and so "subset" becomes a much richer notion.

(I want to point out that there is still a lot of nuance here. In particular, it's critical to keep the distinction between internal and external views of a logic/type theory. Andrej Bauer has a good article showing that (externally) inductive types can look quite different from what we expect. But also see Peter Lumsdaine's comment therein.)

data Nat : Set where
    Zero : Nat
    Succ : Nat → Nat

data Id {A : Set} (x : A) : A → Set where
    Refl : Id x x

_trans_ : {A : Set}{x y z : A} → Id x y → Id y z → Id x z
Refl trans q = q

cong : {A B : Set}{x y : A}(f : A → B) → Id x y → Id (f x) (f y)
cong f Refl = Refl

record Iso (X Y : Set) : Set where
    field
        to : X → Y
        from : Y → X
        lInv : (x : X) → Id x (from (to x))
        rInv : (y : Y) → Id y (to (from y))

module _ (N : Set)
         (zero : N)
         (succ : N → N)
         (ind : (P : N → Set) → P zero → ({n : N} → P n → P (succ n)) → (n : N) → P n) where
    rec : (A : Set) → A → (A → A) → N → A
    rec A z s = ind (λ _ → A) z (λ {_} → s)

    module _ (recZ : (A : Set) → (z : A) → (s : A → A) 
                     → Id z (rec A z s zero))
             (recS : (A : Set) → (z : A) → (s : A → A) → (n : N) 
                     → Id (s (rec A z s n)) (rec A z s (succ n))) where

        Nat-is-unique : Iso N Nat
        Nat-is-unique = record { to = toNat; from = fromNat; lInv = invN; rInv = invNat }
            where toNat : N → Nat
                  toNat = rec Nat Zero Succ
                  fromNat : Nat → N
                  fromNat Zero = zero
                  fromNat (Succ n) = succ (fromNat n)
                  invN : (n : N) → Id n (fromNat (toNat n))
                  invN = ind (λ n → Id n (fromNat (toNat n))) (cong fromNat (recZ Nat Zero Succ)) 
                        (λ {n} p → cong succ p trans cong fromNat (recS Nat Zero Succ n))
                  invNat : (n : Nat) → Id n (toNat (fromNat n))
                  invNat Zero = recZ Nat Zero Succ
                  invNat (Succ n) = cong Succ (invNat n) trans recS Nat Zero Succ (fromNat n)
| cite | improve this answer | |
$\endgroup$

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.