Fam: Mono(A, B) → [A1, Nat(y^A2, B)] Yon: Nat(y^A2, B) → B(A2) Fam; [A1, Yon] : Mon(A, B) → [A1, B(A2)] Split: [A1, B1×A2^B2] → [A1, B1]×[A1, A2^B2] UnCurry: [A1, A2^B2] → [A1×B2, A2] Split;([A1, B1]×UnCurry) : [A1, B1×A2^B2] → [A1, B1]×[A…