X and Y <=> forall Y, A -> B -> Y

We have a R, R satisfies:

A -> B -> R

forall Y, A -> B -> R -> Y

we name R as product type.

X or Y <=> forall Y, (A -> Y) -> (B -> Y) -> Y

We have a R, R satisfies:

A -> R

B -> R

forall Y, (A -> Y) -> (B -> Y) -> R -> Y

we name R as sum type.

exist X, P(X) <=> forall Y, (forall X, P(X) -> Y) -> Y

We have a R, R satisfies:

forall X, P(X) -> R

forall Y, (forall X, P(X) -> Y) -> R -> Y

we name R as existential type.