Eq : (a:Type) -> a -> a -> Type;
Eq = \ a x y -> (P : a -> Type) -> P x -> P y;

refl : (a:Type) -> (x:a) -> Eq a x x;
refl = \ a x P px -> px;

A : Type;
a : A;

b : A;
b = a;

t0 : Eq A a b;
t0 = refl A a;

{-
c : A;
t1 : Eq A a c;
t1 = refl A a;
-}

d : ^A;
d = [a];

t2 : Eq (^A) d [a];
t2 = refl (^A) [a];

{-
t3 : Eq (^A) [a] [b];
t3 = refl (^A) [a];
-}

e : A;
e = a;

t4 : Eq (^A) [e] [b];
t4 = refl (^A) [e];

id : A -> A;
id = \ x -> x;

f : A;
f = id a;

t5 : Eq (^A) [f] [b];
t5 = refl (^A) [f];
{-
? f = b
? id a = a [f=b=b]
-}

t6 : Eq A (id a) a;
t6 = refl A a;