Lemma iscomprelfun_funcomp {X Y Z : UU} {R : hrel X} {S : hrel Y} {f : X → Y} {g : Y → Z} (Hf : iscomprelrelfun R S f) (Hg : iscomprelfun S g) : iscomprelfun R (g ∘ f). Proof. intros x x' r. exact (Hg _ _ (Hf x x' r)). Defined.