{- Concatenate a `List` of `List`s into a single `List` -} let concat : ∀(a : Type) → List (List a) → List a = λ(a : Type) → λ(xss : List (List a)) → List/build a ( λ(list : Type) → λ(cons : a → list → list) → λ(nil : list) → List/fold (List a) xss list (λ(xs : List a) → λ(ys : list) → List/fold a xs list cons ys) nil ) let example0 = assert : concat Natural [ [ 0, 1, 2 ], [ 3, 4 ], [ 5, 6, 7, 8 ] ] ≡ [ 0, 1, 2, 3, 4, 5, 6, 7, 8 ] let example1 = assert : concat Natural [ [] : List Natural, [] : List Natural, [] : List Natural ] ≡ ([] : List Natural) let example2 = assert : concat Natural ([] : List (List Natural)) ≡ ([] : List Natural) in concat