namespace http://cds.omdoc.org/urtheories❚

theory Products : ?PLF =
   product : type ⟶ type ⟶ type❘ # 1 PROD 2❙
   pair : {a, b} a ⟶ b ⟶ a PROD b❘# PAIR 3 4❙
   projectLeft : {a,b} a PROD b ⟶ a❘# PI1 3❙
   projectRight : {a,b} a PROD b ⟶ b❘# PI2 3❙

❚