Как же будет выглядеть открытая рекурсия?
Mike Shulman recently succeed in constructing HITs H with paths in all dimensions. Is there a way to define a type $H of all sequences of the elements e: H, together with their automorphisms e1: Id H e e, their equivalences e2: Id (Id H e e) e1 e1, etc? It seems to be a very natural way to define separable second-countable T0 spaces with semidecidable apartness relation.
Has anyone already thought about connections between such types and open induction? In appears that some such induction would provide the only generic way to prove stuff for elements of $H.
Open induction is a generalization of transfinite induction:
Let U: Seq T → Prop be an open property on infinite sequences of T, _<_: (T, T) → Prop a decidable wellfounded relation on T. The relation _<_ can be lexicographically extended to sequences of T, the resulting relation is not necessarily wellfounded anymore, but still
[∀(a: Seq T, b: Seq T) a < b → U b → U a] → ∀(s: Seq T) U(s)
What's the recursion counterpart to the open induction?