Reintroduce the minus operation and a (really) short example file
Clean the example on univalence and give the lifted version