[derkha]

Yes, that is a valid alternative encoding: https://en.wikipedia.org/wiki/Church_encoding#Represent_the_...

In general, what you describe is representing an inductive type by its _eliminator_: https://www.quora.com/In-type-theory-what-is-an-eliminator-a...