Iso_U(A,B) :=
	sigma f : A -> B .
	sigma g : B -> A .
	(pi a : A . Iso_A(g f a, a)) *
	(pi b : B . Iso_B(f g b, b))

Equiv_U(A,B) :=
	sigma f : A -> B .
	pi y : B .
	sigma x : (Fib f y) .
	pi x' : (Fib f y) .
	Iso_(Fib f y)(x,x')

Fib f y :=
	sigma x : A.
	Iso_B(f x, y)