English
SimplicialInsert inserts a into a list of naturals by placing a in front if it is smaller, otherwise it increments a and recurses on the rest.
Русский
SimplicialInsert вставляет число в список натуральных, помещая его в начало, если оно меньше первого элемента; иначе увеличивает число и рекурсивно продолжает с хвоста.
LaTeX
$$$\\\\text{simplicialInsert}(a, L) = \\begin{cases} [a], & L = [], \\\\ a :: L', & a < h \\\\ b :: \\text{simplicialInsert}(a+1, t), & \\text{otherwise} \\end{cases}$$$
Lean4
/-- The construction `simplicialInsert` describes inserting an element in a list of integer and
moving it to its "right place" according to the simplicial relations. Somewhat miraculously,
the algorithm is the same for the first or the fifth simplicial relations, making it "valid"
when we treat the list as a normal form for a morphism satisfying `P_δ`, or for a morphism
satisfying `P_σ`!
This is similar in nature to `List.orderedInsert`, but note that we increment one of the element
every time we perform an exchange, making it a different construction. -/
def simplicialInsert (a : ℕ) : List ℕ → List ℕ
| [] => [a]
| b :: l => if a < b then a :: b :: l else b :: simplicialInsert (a + 1) l
