hi,

I am new to Scala’s typelevel programming. In type theory, the universal and existential quantification can be encoded as the following:

∀x∈S(P(x)) encoded as Πx : S . Px

∃x∈S(P(x)) encoded as Πα : ∗ . ((Πx : S . (P x → α)) → α)

where x∈S is the subscript of x.

How could the above encodings be coded in Scala 3?

Any advice is appreciated.

Thanks!

Guofeng