Alexander Kuklev (akuklev) wrote,
Alexander Kuklev

[Draft] Inductive-recursive construction of Very Dependent Types

One of the most intriguing open problems in the field of Homotopy Type Theory (HoTT) is the internal definition of presheaves on concrete shape categories (simplicial, cubical, dendroidal, opetopic, Segal’s Γ) as well as their variants with extra conditions, leading to internal definition of (weak) ∞-groupoids and (∞, 1)-categories. This is the enabling condition for doing higher category theory internally to HoTT.
In the draft of his Ph.D. Thesis Nicolai Kraus argues that type-valued presheaves on direct categories (including the most basic example of semisimplicial types) can be defined in Homotopy Type Theory augmented by so called Very Dependent Types [Hic96], a powerful generalization of dependent tuples for the case of potentially infinite number of tuple components, that constitute precisely the right structure to contain infinite towers of coherency conditions.

I'm going to explore definability of very dependent types in presence of indexed inductive-recursive types and discuss the right form of elimination rules for them which turns out to be the open induction, necessary for building an internal syntactic model of HoTT, which is an another open problem of tremendous interest.

Term-level Very-Dependent Functions
In Martin-Löf dependent type theories inductive type families come with eliminators that witness the type families being initial objects of their signature. Dependent eliminators are derivable from the non-dependent ones in presence of η-rules.

Analogously, even employing only the non-dependent eliminators for inductive type families, the terms corresponding to very dependent functions can be constructed, but their type render them virtually unusable, until we find a way to fix their type. Let me start with the simplest inductive type Nat = {zero: Nat | succ: Nat -> Nat}. Their non-dependent eliminator nat-rec takes
  T: Type
  succVal: (n: Nat, prevVal: T) -> T

and produces a function Nat -> T, i.e. a sequence of the objects of the type T [n0, n1, n2,..]

That's not the most general type of the sequence, a sequence might also have items of different types:
  [n0 : T(0), n1 : T(1), n2 : T(2),..].

Furthermore, type of each next component could be dependent on the value of the previous one:
  [n0 : ZeroT, n1 : SuccT(0, n0), n2 : SuccT(1, n1),..].

Such sequence can be easily defined by mutual recursion on the type and term level, i.e. we'll eliminate Nat into the type (T: Type, value: T):
the recursion base is constituted by pair (ZeroT, zeroVal: ZeroT),
the recursion step is constituted by two functions:
  SuccT: (n: Nat)(T: Type, value: T) -> Type
  succVal: (n: Nat)(T: Type, value: T) -> SuccT(n)(T, value)

This construction can be easily used to produce terms for dependent functions on inductive types and dependent pairs: just use Fin(2) as source type and obtain terms for dependent pairs and their special cases: pairs and disjoint unions. Using more involved inductive type families than Nat allows for sequences (or rather trees of potentially infinite depth) with arbitrary manifestly-wellfounded dependency structures. All that appears really nice until we take a look on the types:
    (T: Type, T)
    (ZeroT, zeroVal)
    (SuccT; succVal)

has the type Nat -> (T: Type, T). It produces mere pointed sets. There are not many things you can do with objects of the type (T: Type, T) if you adhere to parametrical polymorphism, really not. Except idT, all available maps from this type are constants.

Catching up the Type-Level
We would like to define a type former Nat-recT (ZeroT, SuccT) providing proper type for functions defined in such a way, and improved eliminator
    (T: Type, T)
    (ZeroT, zeroVal)
    (SuccT, succVal)
 ) : Nat-recT(ZeroT, SuccT)

Let's try to understand the structure of this type in terms of usual Π- and Σ-types. By employing indexed induction-recursion, we can define the type DepTuple(ZeroT, SuccT): Nat -> Type of dependent sequences truncated to a certain length, together with function prev returning all elements but last. Then we'd be able to define Nat-recT (ZeroT, SuccT) as a Π-Type
  (n: Nat) -> DepTuple(ZeroT, SuccT)(n)
together with rule that longer sequences extend the shorter ones, i.e.
  Nat-recT (ZeroT, SuccT) := (s: (n: Nat) -> DepTuple(ZeroT, SuccT)(n), (n: Nat) -> (s(n) = prev s(n + 1)))

The interesting part is the inductive-recursive definition of DepTuple:

  DepTuple(ZeroT, SuccT): Nat -> Type
    0 => ZeroT
    succ(n) => (prev: DepTuple(n)) × SuccT(n, last(n, prev))

  last(ZeroT, SuccT): (n: Nat, DepTuple(n)) -> (T: Type, T)
    (0, z: ZeroT) => (ZeroT, z)
    (succ(n), (prev: DepTuple(n), l: SuccT(n, last(n, prev))) => (SuccT(n, last(n, prev)), l)

The case of IIR seems to be perfectly admissible, the dependent pattern matching in definition of "last" does not seem to be a problem either in presence of definitional η-rules. Producing inhabitants of this type seems also quite obvious, we just have to provide a function that produces dependent tuples of fixed length n:

nat-elim-fst(ZeroT, SuccT, zeroVal, succVal): (n: Nat) -> DepTuple(ZeroT, SuccT)(n)
  0 => zeroVal
  succ(p) => nat-elim-fst(ZeroT, SuccT, zeroVal, succVal)(p)

The witness that this sequence is a compatible chain can be easily provided with help of propositional η-conversion.

Thus with help of indexed induction-recursion we obtain a form of very-dependent types. But I'm not sure this is the form we need, because it doesn't provide the strong enough elimination principle per ce.

Eliminators for *-recT: Open induction
Pointwise (aka componentwise if we talk about sequences) transformation of a function f: A -> B means postcomposing it with a function g: (arg: A, fVal: B) -> Y which is dependent on argument arg of f additionally to its value fVal = f(arg). In case of dependently typed function f: (a: A) -> B, the type of postcomposant must be g: (arg: A, fVal: B(arg)) -> Y. When we talk about very-dependent function, the situation gets more complicated. The postcomposant has now to depend on previous values of f and transform values of types of the form (ZeroT | SuccT(n: Nat, prevVal: DepTuple(ZeroT, SuccT)(n))), i.e. f has to be defined for a bi-indexed family of types, the first index is formed by values of inductive type X (domain of f), and the second by values of the type DepTuple. We'll need to be able to define such functions mutually (with respect to DepTuple) recursively (with respect to Nat).

I'm pretty sure such induction principle is exactly the right thing to proceed at the point where Mike Shulman stopped in [Homotopy Type Theory should eat itself]: "At this point I stopped, because I recognized the signs of the sort of infinite regress that stymies many other approaches to semisimplicial types: in order to prove coherence at the n-th level, you need to know (already or mutually) coherence at the (n + 1)-st level, making the whole definition impossible unless you could define infinitely many functions in one mutual recursion."

Very-dependent functions will be used in HoTT to carry the infinitary (but lazily computable) coherence information, we'll need to transform them component-wise by means of an infinite number of functions (one for each component), and define this infinite family of functions mutually-recursively in a way precisely corresponding to open induction a la Berger.

First let's consider the weakly dependent version. Say, we'll be defining function that transforms a sequence (n: Nat) -> Fin(n + 1) by adding element number to each element:
nat-seq-req: (
  InZeroT: Type
  InSuccT(n: Nat, _): Type
    Fin(n + 1)

  OutZeroT: Type
  OutSuccT(n: Nat, _): Type
    Fin(n + n + 1)

  mapZero: InZeroT -> OutZeroT
    n: Fin(1) => n
  mapSucc(n: Nat)(
    prevInValues: DepTuple(InZeroT, InSuccT)(n)
    lastInValue: InSuccT(n + 1, last(prevValues))
    lastOut: (T: Type, T)
  ) -> OutSuccT(n + 1, lastOut)
    (m: Fin(n)) => n + m
) : Nat-recT (InZeroT, InSuccT) -> Nat-recT (OutZeroT, OutSuccT)

And now there comes the crucial step: we'll allow stepTransformers (mapSucc(n) for succ(n) in case of Nat) to depend on ready sequence transformers restricted to subterms of the eliminated terms (i.e. to n, the only direct subterm of succ(n) in case of Nat). This would presumably allow to define hereditary substitutions in the internal model of HoTT recursively: the substitution function for a term (function which is being defined) can use subsitution functions for subterms as if they were readily defined. Such definition is computationally sane, the recursion will terminate after finite number of steps, because the functional we're defining is known to be continuous already by the fact that we're defining it constructively, but in order to prove it we'll need countable dependent choice. Anyway, here's the updated signature
nat-seq-req: (
  InZeroT: Type
  InSuccT(n: Nat, _): Type

  OutZeroT: Type
  OutSuccT(n: Nat, _): Type

  mapZero: InZeroT -> OutZeroT
  mapSucc(n: Nat)(
    prevInValues: DepTuple(InZeroT, InSuccT)(n)
    lastInValue: InSuccT(n + 1, last(prevValues))
    lastOut: (T: Type, T)
    transform: Nat-recT (InSuccT(n, prev(prevValues)), InSuccT) -> Nat-recT (lastOut.T, OutSuccT)
  ) -> OutSuccT(n, lastOut)
) : Nat-recT (InZeroT, InSuccT) -> Nat-recT (OutZeroT, OutSuccT)

I don't think such powerful form of induction would be readily available in HoTT+IIR, because open induction provides tools to implement a large portion of classical analysis intuitionistically (in particular all sigma-statements derivable under employment of classical (countable) dependent choice are derivable), and provides (modified-)realizability interpretation for the whole classical analysis. It points out that a theory capable of providing that much is much stronger proof-theoretically than usual MLTTs with induction-recursion are (they are known to have proof-theoretical ordinals around Mahlo, whereas the classical analysis Z2 is beyond the tools available in ordinal-theoretic proof theory at the moment).

But still, this form of induction is computationally justified (in contrary to LEM and AC), so it's highly desirable to have a variety of HoTT supporting it and thus capable of doing lots of analysis and higher category theory.
Tags: fprog

  • (no subject)

    Встретил фотографию толпы футбольных фанатов, и она меня скорее напугала, у меня уж точно нет желания быть там среди них. Но внезапно я понял, что…

  • Прогресс

    Десять дней назад, вторая ступень SpaceX'овского корабля Starship своим ходом слетала своим ходом на десять километров вверх, и усмепшно приземлилась…

  • О водосбережении

    Как известно, питьевая вода во многих странах дефицитный ресурс. И даже в дождливой Германии летом иногда случаются засухи, в результате которых она…

  • Post a new comment


    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.