foo.agda

data _≡_ {i} {A : Set i} (x : A) : A -> Set i where
  refl : x ≡ x
{-# BUILTIN EQUALITY _≡_ #-}

data Unit : Set where
  unit : Unit

refl_unit : unit ≡ unit
refl_unit = refl

refl_unit2 : (u : Unit) -> u ≡ u
refl_unit2 unit = refl

refl_unit3 : (u1 u2 : Unit) -> u1 ≡ u2
refl_unit3 unit unit = refl


data Two : Set where
  zero : Two
  one : Two

g : one ≡ one
g = refl {x = one}

flip : Two → Two
flip zero = one
flip one = zero

f : ( x : Two ) -> x ≡ one -> flip x ≡ zero
f num p = {!!}