Definition aprel_pr1 {X : UU} (ap : aprel X) : hrel X := pr1 ap.
Require Import UniMath.Foundations.Propositions. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions.