cubical-0.2.0: examples/opacity_fail.cub

module opacity_fail where

import primitives

Bool : U
data Bool = true | false

x : Bool
x = false

opaque x

y : Bool
y = x
  where x : Bool
        x = true

failure : Id Bool x y
failure = refl Bool x

transparent x