Share the proofs of ×-comm and ⊎-comm of type isomorphisms and add a pairing operation#2868

Taneb merged 4 commits intoagda:masteragda/agda-stdlib:masterfrom

shhyou:typeisoshhyou/agda-stdlib:typeisoCopy head branch name to clipboard