module weq where

import univ

com : U -> U
com = pair (A -> A -> A) (