∀ (s : Sort σ), (A/Φ) s → B s := λ s, (equiv_quotient_ump (Φ s) (Build_HSet (B s)))^-1 (f s; R s).
Require Import Basics.Notations. Require Import Import algebra_notations ne_list.notations. Import quotient_algebra_notations.