let Integer/add = https://prelude.dhall-lang.org/Integer/add.dhall sha256:7da1306a0bf87c5668beead2a1db1b18861e53d7ce1f38057b2964b649f59c3b let negate = https://prelude.dhall-lang.org/Integer/negate.dhall sha256:2373c992e1de93634bc6a8781eb073b2a92a70170133e49762a785f3a136df5d let Integer/succ : Integer → Integer = λ(n : Integer) → Integer/add n +1 let build : ( ∀(integer : Type) → ∀(succ : integer → integer) → ∀(negate : integer → integer) → ∀(zero : integer) → integer ) → Integer = λ ( builder : ∀(integer : Type) → ∀(succ : integer → integer) → ∀(negate : integer → integer) → ∀(zero : integer) → integer ) → builder Integer Integer/succ negate +0 in build