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