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`

zeroVal:

succVal: (n: Nat, prevVal: T) -> T

and produces a function Nat -> T, i.e. a sequence of the objects of the type T

`[n`_{0}, n_{1}, n_{2},..]

That's not the most general type of the sequence, a sequence might also have items of different types:

` [n`_{0} : T(0), n_{1} : T(1), n_{2} : T(2),..]

.Furthermore, type of each next component could be dependent on the value of the previous one:

` [n`_{0} : ZeroT, n_{1} : SuccT(0, n_{0}), n_{2} : SuccT(1, n_{1}),..]

.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:

` nat-rec(`

(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 id

_{T}, 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

` nat-elim(`

(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:

**mutual**

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**But I'm not sure this is the form we need, because it doesn't provide the strong enough elimination principle per ce.

*a form*of very-dependent types.**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

Fin(1)

InSuccT(n: Nat, _): Type

Fin(n + 1)

OutZeroT: Type

Fin(1)

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.