Lemma iscomprelrellogeqf1 {X : UU} {R R' : hrel X} (L : hrel X) (lg : hrellogeq R R') (is : iscomprelrel R L) : iscomprelrel R' L. Proof. intros. apply (iscomprelfun2logeqf lg L is). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.