Given instances and Curry-Howard correspondence, How to do?

Question
1

Hi,

In the post Scala implicits and the Curry-Howard correspondence, the logic implication is coded as (here in Scala 3)

trait A
given proofOfA: A()

trait B
given `A implies B`(using a: A): B()

summon[B] // passed

But the post coded the conjunction and disjunction using product type and sum type.

If the conjunction and disjunction are defined as the following using implication, how to code them in Scala 3? or it cannot be coded in Scala 3 at all and what has done in the post is the best.

A ∧ B ≡ ΠC : * .(A → B → C) → C, i.e., for all C, (A implies (B implies C)) implies C
A ∨ B ≡ ΠC : * .(A → C) → (B → C) → C, i.e., for all C, (A → C implies that (B → C implies C))

Your help is appreciated.

Guofeng

2

I am not completely sure I got this right, but I believe the first one is as simple as this:

trait A
given proofOfA: A()

trait B
given `A implies B`(using a: A): B()

trait C
given `B implies C`(using b: B): C()

// (A implies (B implies C)) implies C
summon[C]

For the second one I believe it would be like this:

trait A
 
trait B

trait C
given `A | B implies C`(using ab: A | B): C()

// Or alternatively
given `A implies C`(using a: A): C()
given `B implies C`(using b: B): C()

This means that if you have either an A or a B you can have a C

All the code here: Scastie - An interactive playground for Scala.