proposition: Lemma path_subalgebra_iff `{Univalence} (R : ∀ s x, P s x <-> Q s x) : A&&P = A&&Q.
proof: Proof. apply path_subalgebra. funext s x. apply (@path_universe _ _ _ (fst (R s x))). apply (equiv_equiv_iff_hprop _ _ (R s x)). Defined.
imports: HoTT.HProp HoTT.Types HoTT.Classes.theory.ua_homomorphism