Lemma iseqclassdirprod {X Y : UU} {R : hrel X} {Q : hrel Y} {A : hsubtype X} {B : hsubtype Y} (isa : iseqclass R A) (isb : iseqclass Q B) : iseqclass (hreldirprod R Q) (subtypesdirprod A B). Proof. intros. set (XY := dirprod X Y). set (AB := subtypesdirprod A B). set (RQ := hreldirprod R Q). set (ax0 := ishinhsubtypedirprod A B (eqax0 isa) (eqax0 isb)). assert (ax1 : ∏ xy1 xy2 : XY, RQ xy1 xy2 -> AB xy1 -> AB xy2). { intros xy1 xy2 rq ab1. apply (make_dirprod (eqax1 isa _ _ (pr1 rq) (pr1 ab1)) (eqax1 isb _ _ (pr2 rq) (pr2 ab1))). } assert (ax2 : ∏ xy1 xy2 : XY, AB xy1 -> AB xy2 -> RQ xy1 xy2). { intros xy1 xy2 ab1 ab2. apply (make_dirprod (eqax2 isa _ _ (pr1 ab1) (pr1 ab2)) (eqax2 isb _ _ (pr2 ab1) (pr2 ab2))). } apply (iseqclassconstr _ ax0 ax1 ax2). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.