Definition compfuncomp {X : UU} (R : hrel X) {S S' : UU} (f : compfun R S) (g : S -> S') : compfun R S'. Proof. intros. split with (funcomp f g). intros x x' r. apply (maponpaths g (pr2 f x x' r)). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.