I was studying Haskell and happened to know the church encoding of algebraic data types. For example, the unit type in Haskell can be encoded as a polymorphic function type. But one can also define a Unit' type that is isomorphic to Unit but essentially treated as a distinct type from Unit. Then we have Unit :: Unit and Unit' :: Unit' as elements from different domains. How to do this in church encoding?
data Unit = Unit
type UnitChurch = forall x. x -> x
data Unit' = Unit'
type UnitChurch' = ?
I tried to search google for questions alike but did not find an answer. My guess is that maybe we can define UnitChurch' as:
type UnitChurch' = forall u. (UnitChurch -> u) -> u
which is similar to newtype in Haskell.