proposition: Lemma compute_quotient_algebra_mapout : ∀ (s : Sort σ) (x : A s), hom_quotient_algebra_mapout s (class_of (Φ s) x) = f s x.
proof: Proof. reflexivity. Defined.
imports: HoTT.Classes.interfaces.ua_congruence HSet Colimits.Quotient Classes.implementations.list Classes.interfaces.canonical_names Classes.theory.ua_homomorphism