{- Build a list by copying the given element the specified number of times Examples: ``` ./replicate 9 Natural 1 = [ 1, 1, 1, 1, 1, 1, 1, 1, 1 ] ./replicate 0 Natural 1 = [] : List Natural ``` -} let replicate : Natural → ∀(a : Type) → a → List a = λ(n : Natural) → λ(a : Type) → λ(x : a) → List/build a ( λ(list : Type) → λ(cons : a → list → list) → Natural/fold n list (cons x) ) in replicate