I'm reading CH Isomorphism.
Let's divide into two stages:
Prop corresponds to types. so a proposition A $\wedge$ B corresponds to type A $\times$ B.
Proof corresponds to the program. What is the corresponding proof and program in this case ?
As far as I can guess the proof is a pair but how we denote program ? Is that a lambda term "pair" ?? What we mean by a proof here. coz proof is a complete derivation in case a pro example exists ?? Very confused . Can someone help ?