Alexander Kuklev (akuklev) wrote,
Alexander Kuklev

Fully coherent HITs and open recursion

For n-truncated higher inductive types

> Infinitary loop types
Loop space of A: Type is the type ΩA(a: A) := (p: a = a) that contains paths from a to a, i.e. loops. For example the loop space of a S1 is Z. Higher loop spaces may be also defined:

Ω^2 a := (p1: a = a) × (p2: p1 = p1)
Ω^3 a := (p1: a = a) × (p2: p1 = p1) × (p3: p2 = p2)

One can also define the infinitary loop type
data ω: {T: Type} -> (e: T) -> Type where
  triv: (e: T) -> ω(e)
  cons: (e: T) -> (l: Ω(e)) -> ω(l) -> ω(e)
  triv-to-cons: (e: T) -> ((triv e) = (cons e (refl e) (triv refl e)))

head: ω(e) -> Ω(e)
head (triv e) = refl e
head (cons e p ps) = a

tail: (x: ω(e)) -> ω(head x)
tail (triv e) = triv (refl e)
tail (cons e p ps) = cons p (head ps) (tail ps)

So, the triv constructor is used to denote an element followed by an infinite chain of refl's, and the cons constructor is used to construct the nontrivial values. Every map f: (x: X) -> Y between HITs A and B induces the map coh(f): ω(x) -> ω(f x)

(Note to self: probably, ω should be defined as a 0-truncation of the above definition.)

For n-truncated types T, the infinitary loop type ω should be equal to Ω^m for m >= n, but for the HITs of infinite h-level the infinitary loop type ω necessarily contains at least sequences of arbitrary length, but might also contain (it's the case if T is has constructor branching at every level) sequences of infinite length. In this case, the infinitary loop type ω has structure of a cantor set.

> Open recursion
Open recursion comes into play when we want to define a function from a type of infinite h-level. Typically, it's easy to define the action of the function on the constructors of the source type, but hard (or impossible with usual means) to show that the function respects all the coherence conditions of the source type, i.e. that nontrivialy equal source terms are mapped onto equal target terms.

Usual recursion on inductive types goes as follows: to define f: (x: X) -> Y(x) you provide a recursor for each constructor c(a, b,.., z) of X. The recursor is an expression defining the value of f(c(a, b,.., z)) assuming the values of f for each subterm a, b,..,c of c(a, b,.., z) is already known.

When performing recursion on HITs we should in a fact construct not only the function f(x), but also the coherence map coh(f)(x). This can be naturally done by simultaneously providing f(x) and coh(f)(x) for each constructor of a HIT while assuming that f(x) and coh(f)(x) are both known for subterms of x. This generalization allows functions to have nontrivial actions on loop spaces and restricts equalities of HITs to be infinitely coherent syntactically. This form of recursion is strictly stronger than the usual one. It is is equivalent to open recursion as introduced by Berger[1], which is tightly connected to bar recursion.

[1] Ulrich Berger, "A Computational Interpretation of Open Induction",

  • Towards Univalent Construction Calculus

    Modern constructive Martin-Löf Type Theories (MLTTs) are exceptionally expressive and convenient languages for mathematical reasoning. By “modern”…

  • (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.