module propua where

open import preliminaries
open import isprop

postulate prop-ua : {i : 𝕃} {P Q : U i}  isProp P  isProp Q  (P  Q)  (Q  P)  P  Q