You say you have dependent types OK, could you define this? data Eq : {a : Type} -> a -> a -> Type where Refl : Eq x x sym : {x : a} -> {y :

You say you have dependent types OK, could you define this? data Eq : {a : Type} -> a -> a -> Type where Refl : Eq x x sym : {x : a} -> {y : a} -> Eq x y -> Eq y x sym Refl = Refl replace : {a : Type} -> {x : a} -> {y : a} -> {f : a -> Type} -> Eq x y -> f x -> f y replace Refl p = p