Definition qeq {X Y : UU} (R : hrel X) := total2 (λ phi : F X Y R, ∏ psi : F X Y R -> Y, paths (psi phi) (Fv R (compfuncomp R (make_compfun R _ (iscompFi R)) psi) phi)).
Require Import UniMath.Foundations.UnivalenceAxiom.