Require Export HoTT.Classes.interfaces.ua_congruence.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

Require Import
  HSet
  Colimits.Quotient
  Spaces.List.Core
  Classes.interfaces.canonical_names
  Classes.theory.ua_homomorphism.

Local Open Scope list_scope.
Import algebra_notations ne_list.notations.

Section quotient_algebra.
  Context
    `{Funext} {σ : Signature} (A : Algebra σ)
    (Φ : ∀ s, Relation (A s)) `{!IsCongruence A Φ}.

(** The quotient algebra carriers is the family of set-quotients
    induced by [Φ]. *)

  Definition carriers_quotient_algebra : Carriers σ
    := λ s, Quotient (Φ s).

(** Specialization of [quotient_ind_prop]. Suppose
    [P : FamilyProd carriers_quotient_algebra w → Type] and
    [∀ a, IsHProp (P a)]. To show that [P a] holds for all [a :
    FamilyProd carriers_quotient_algebra w], it is sufficient to show
    that [P (class_of _ x1, ..., class_of _ xn, tt)] holds for all
    [(x1, ..., xn, tt) : FamilyProd A w]. *)

  Fixpoint quotient_ind_prop_family_prod {w : list (Sort σ)}
    : ∀ (P : FamilyProd carriers_quotient_algebra w → Type)
        `{!∀ a, IsHProp (P a)}
        (dclass : ∀ x, P (map_family_prod (λ s, class_of (Φ s)) x))
        (a : FamilyProd carriers_quotient_algebra w), P a
    := match w with
       | nil => λ P _ dclass 'tt, dclass tt
       | s :: w' => λ P _ dclass a,
         Quotient_ind_hprop (Φ s) (λ a, ∀ b, P (a,b))
           (λ a, quotient_ind_prop_family_prod
                  (λ c, P (class_of (Φ s) a, c)) (λ c, dclass (a, c)))
           (fst a) (snd a)
       end.

(** Let [f : Operation A w], [g : Operation carriers_quotient_algebra w].
    If [g] is the quotient algebra operation induced by [f], then we want
    [ComputeOpQuotient f g] to hold, since then

<<
      β (class_of _ a1, class_of _ a2, ..., class_of _ an)
      = class_of _ (α (a1, a2, ..., an)),
>>

    where [α] is the uncurried [f] operation and [β] is the uncurried
    [g] operation. *)

  Definition ComputeOpQuotient {w : SymbolType σ}
    (f : Operation A w) (g : Operation carriers_quotient_algebra w)
    := ∀ (a : FamilyProd A (dom_symboltype w)),
         ap_operation g (map_family_prod (λ s, class_of (Φ s)) a)
         = class_of (Φ (cod_symboltype w)) (ap_operation f a).

  Local Notation QuotOp w :=
    (∀ (f : Operation A w),
     OpCompatible A Φ f →
     ∃ g : Operation carriers_quotient_algebra w,
     ComputeOpQuotient f g) (only parsing).

  Local Notation op_qalg_cons q f P x :=
    (q _ (f x) (op_compatible_cons Φ _ _ f x P)).1 (only parsing).

  Lemma op_quotient_algebra_well_def
    (q : ∀ (w : SymbolType σ), QuotOp w)
    (s : Sort σ) (w : SymbolType σ) (f : Operation A (s ::: w))
    (P : OpCompatible A Φ f) (x y : A s) (C : Φ s x y)
    : op_qalg_cons q f P x = op_qalg_cons q f P y.
H: Funext
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
q: forall (w : SymbolType σ) 
(f : Operation A w),
OpCompatible A Φ f ->
{g : Operation carriers_quotient_algebra w &
ComputeOpQuotient f g}
s: Sort σ
w: SymbolType σ
f: Operation A (s ::: w)
P: OpCompatible A Φ f
x, y: A s
C: Φ s x y
(q w (f x) (op_compatible_cons Φ s w f x P)).1 =
(q w (f y) (op_compatible_cons Φ s w f y P)).1
  Proof.
H: Funext
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
q: forall (w : SymbolType σ) 
(f : Operation A w),
OpCompatible A Φ f ->
{g : Operation carriers_quotient_algebra w &
ComputeOpQuotient f g}
s: Sort σ
w: SymbolType σ
f: Operation A (s ::: w)
P: OpCompatible A Φ f
x, y: A s
C: Φ s x y
(q w (f x) (op_compatible_cons Φ s w f x P)).1 =
(q w (f y) (op_compatible_cons Φ s w f y P)).1
    apply (@path_forall_ap_operation _ σ).
H: Funext
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
q: forall (w : SymbolType σ) 
(f : Operation A w),
OpCompatible A Φ f ->
{g : Operation carriers_quotient_algebra w &
ComputeOpQuotient f g}
s: Sort σ
w: SymbolType σ
f: Operation A (s ::: w)
P: OpCompatible A Φ f
x, y: A s
C: Φ s x y
forall
a : FamilyProd carriers_quotient_algebra
      (dom_symboltype w),
ap_operation
  (q w (f x) (op_compatible_cons Φ s w f x P)).1 a =
ap_operation
  (q w (f y) (op_compatible_cons Φ s w f y P)).1 a
    apply quotient_ind_prop_family_prod; try exact _.
H: Funext
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
q: forall (w : SymbolType σ) 
(f : Operation A w),
OpCompatible A Φ f ->
{g : Operation carriers_quotient_algebra w &
ComputeOpQuotient f g}
s: Sort σ
w: SymbolType σ
f: Operation A (s ::: w)
P: OpCompatible A Φ f
x, y: A s
C: Φ s x y
forall x0 : FamilyProd A (dom_symboltype w),
ap_operation
  (q w (f x) (op_compatible_cons Φ s w f x P)).1
  (map_family_prod (λ s : Sort σ, class_of (Φ s)) x0) =
ap_operation
  (q w (f y) (op_compatible_cons Φ s w f y P)).1
  (map_family_prod (λ s : Sort σ, class_of (Φ s)) x0)
    intro a.
H: Funext
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
q: forall (w : SymbolType σ) 
(f : Operation A w),
OpCompatible A Φ f ->
{g : Operation carriers_quotient_algebra w &
ComputeOpQuotient f g}
s: Sort σ
w: SymbolType σ
f: Operation A (s ::: w)
P: OpCompatible A Φ f
x, y: A s
C: Φ s x y
a: FamilyProd A (dom_symboltype w)
ap_operation
  (q w (f x) (op_compatible_cons Φ s w f x P)).1
  (map_family_prod (λ s : Sort σ, class_of (Φ s)) a) =
ap_operation
  (q w (f y) (op_compatible_cons Φ s w f y P)).1
  (map_family_prod (λ s : Sort σ, class_of (Φ s)) a)
    destruct (q _ _ (op_compatible_cons Φ s w f x P)) as [g1 P1].
H: Funext
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
q: forall (w : SymbolType σ) 
(f : Operation A w),
OpCompatible A Φ f ->
{g : Operation carriers_quotient_algebra w &
ComputeOpQuotient f g}
s: Sort σ
w: SymbolType σ
f: Operation A (s ::: w)
P: OpCompatible A Φ f
x, y: A s
C: Φ s x y
a: FamilyProd A (dom_symboltype w)
g1: Operation carriers_quotient_algebra w
P1: ComputeOpQuotient (f x) g1
ap_operation (g1; P1).1
  (map_family_prod (λ s : Sort σ, class_of (Φ s)) a) =
ap_operation
  (q w (f y) (op_compatible_cons Φ s w f y P)).1
  (map_family_prod (λ s : Sort σ, class_of (Φ s)) a)
    destruct (q _ _ (op_compatible_cons Φ s w f y P)) as [g2 P2].
H: Funext
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
q: forall (w : SymbolType σ) 
(f : Operation A w),
OpCompatible A Φ f ->
{g : Operation carriers_quotient_algebra w &
ComputeOpQuotient f g}
s: Sort σ
w: SymbolType σ
f: Operation A (s ::: w)
P: OpCompatible A Φ f
x, y: A s
C: Φ s x y
a: FamilyProd A (dom_symboltype w)
g1: Operation carriers_quotient_algebra w
P1: ComputeOpQuotient (f x) g1
g2: Operation carriers_quotient_algebra w
P2: ComputeOpQuotient (f y) g2
ap_operation (g1; P1).1
  (map_family_prod (λ s : Sort σ, class_of (Φ s)) a) =
ap_operation (g2; P2).1
  (map_family_prod (λ s : Sort σ, class_of (Φ s)) a)
    refine ((P1 a) @ _ @ (P2 a)^).
H: Funext
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
q: forall (w : SymbolType σ) 
(f : Operation A w),
OpCompatible A Φ f ->
{g : Operation carriers_quotient_algebra w &
ComputeOpQuotient f g}
s: Sort σ
w: SymbolType σ
f: Operation A (s ::: w)
P: OpCompatible A Φ f
x, y: A s
C: Φ s x y
a: FamilyProd A (dom_symboltype w)
g1: Operation carriers_quotient_algebra w
P1: ComputeOpQuotient (f x) g1
g2: Operation carriers_quotient_algebra w
P2: ComputeOpQuotient (f y) g2
class_of (Φ (cod_symboltype w)) (ap_operation (f x) a) =
class_of (Φ (cod_symboltype w)) (ap_operation (f y) a)
    apply qglue.
H: Funext
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
q: forall (w : SymbolType σ) 
(f : Operation A w),
OpCompatible A Φ f ->
{g : Operation carriers_quotient_algebra w &
ComputeOpQuotient f g}
s: Sort σ
w: SymbolType σ
f: Operation A (s ::: w)
P: OpCompatible A Φ f
x, y: A s
C: Φ s x y
a: FamilyProd A (dom_symboltype w)
g1: Operation carriers_quotient_algebra w
P1: ComputeOpQuotient (f x) g1
g2: Operation carriers_quotient_algebra w
P2: ComputeOpQuotient (f y) g2
Φ (cod_symboltype w) (ap_operation (f x) a)
  (ap_operation (f y) a)
    exact (P (x,a) (y,a) (C, reflexive_for_all_2_family_prod A Φ a)).
  Defined.

(* Given an operation [f : A s1 → A s2 → ... A sn → A t] and a witness
   [C : OpCompatible A Φ f], then [op_quotient_algebra f C] is a
   dependent pair with first component an operation [g : Q s1 → Q s2
   → ... Q sn → Q t], where [Q := carriers_quotient_algebra], and
   second component a proof of [ComputeOpQuotient f g]. The first
   component [g] is the quotient algebra operation corresponding to [f].
   The second component proof of [ComputeOpQuotient f g] is passed to
   the [op_quotient_algebra_well_def] lemma, which is used to show that
   the quotient algebra operation [g] is well defined, i.e. that

<<
    Φ s1 x1 y1 ∧ Φ s2 x2 y2 ∧ ... ∧ Φ sn xn yn
>>

   implies

<<
    g (class_of _ x1) (class_of _ x2) ... (class_of _ xn)
    = g (class_of _ y1) (class_of _ y2) ... (class_of _ yn).
>>
*)

  Fixpoint op_quotient_algebra {w : SymbolType σ} : QuotOp w.
H: Funext
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
op_quotient_algebra: forall (w : SymbolType σ)
(f : Operation A w),
OpCompatible A Φ f ->
{g
: Operation
    carriers_quotient_algebra w
& ComputeOpQuotient f g}
w: SymbolType σ
forall f : Operation A w,
OpCompatible A Φ f ->
{g : Operation carriers_quotient_algebra w &
ComputeOpQuotient f g}
  Proof.
H: Funext
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
op_quotient_algebra: forall (w : SymbolType σ)
(f : Operation A w),
OpCompatible A Φ f ->
{g
: Operation
    carriers_quotient_algebra w
& ComputeOpQuotient f g}
w: SymbolType σ
forall f : Operation A w,
OpCompatible A Φ f ->
{g : Operation carriers_quotient_algebra w &
ComputeOpQuotient f g} refine (
      match w return QuotOp w with
      | [:s:] => λ (f : A s) P, (class_of (Φ s) f; λ a, idpath)
      | s ::: w' => λ (f : A s → Operation A w') P,
        (Quotient_rec (Φ s) _
          (λ (x : A s), op_qalg_cons op_quotient_algebra f P x)
          (op_quotient_algebra_well_def op_quotient_algebra s w' f P)
        ; _)
      end
    ).
H: Funext
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
op_quotient_algebra: forall (w : SymbolType σ)
(f : Operation A w),
OpCompatible A Φ f ->
{g
: Operation
    carriers_quotient_algebra w
& ComputeOpQuotient f g}
w: SymbolType σ
s: Sort σ
w': ne_list (Sort σ)
f: A s -> Operation A w'
P: OpCompatible A Φ f
ComputeOpQuotient f
  (Quotient_rec (Φ s)
     (Operation carriers_quotient_algebra w')
     (λ x : A s,
      (op_quotient_algebra w' (f x)
         (op_compatible_cons Φ s w' f x P)).1)
     (op_quotient_algebra_well_def op_quotient_algebra
        s w' f P))
    intros [x a].
H: Funext
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
op_quotient_algebra: forall (w : SymbolType σ)
(f : Operation A w),
OpCompatible A Φ f ->
{g
: Operation
    carriers_quotient_algebra w
& ComputeOpQuotient f g}
w: SymbolType σ
s: Sort σ
w': ne_list (Sort σ)
f: A s -> Operation A w'
P: OpCompatible A Φ f
x: A s
a: fold_right (λ (i : Sort σ) (A0 : Type), A i * A0)
  Unit (dom_symboltype w')
ap_operation
  (Quotient_rec (Φ s)
     (Operation carriers_quotient_algebra w')
     (λ x : A s,
      (op_quotient_algebra w' (f x)
         (op_compatible_cons Φ s w' f x P)).1)
     (op_quotient_algebra_well_def op_quotient_algebra
        s w' f P))
  (map_family_prod (λ s : Sort σ, class_of (Φ s))
     (x, a)) =
class_of (Φ (cod_symboltype (s ::: w')))
  (ap_operation f (x, a))
    apply (op_quotient_algebra w' (f x) (op_compatible_cons Φ s w' f x P)).
  Defined.

  Definition ops_quotient_algebra (u : Symbol σ)
    : Operation carriers_quotient_algebra (σ u)
    := (op_quotient_algebra u.#A (ops_compatible_cong A Φ u)).1.

(** Definition of quotient algebra. See Lemma [compute_op_quotient]
    below for the computation rule of quotient algebra operations. *)

  Definition QuotientAlgebra : Algebra σ
    := BuildAlgebra carriers_quotient_algebra ops_quotient_algebra.

(** The quotient algebra carriers are always sets. *)

  Global Instance hset_quotient_algebra
    : IsHSetAlgebra QuotientAlgebra.
H: Funext
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
IsHSetAlgebra QuotientAlgebra
  Proof.
H: Funext
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
IsHSetAlgebra QuotientAlgebra
    intro s.
H: Funext
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
s: Sort σ
IsHSet (QuotientAlgebra s) exact _.
  Qed.

(** The following lemma gives the computation rule for the quotient
    algebra operations. It says that for
    [(a1, a2, ..., an) : A s1 * A s2 * ... * A sn],

<<
      β (class_of _ a1, class_of _ a2, ..., class_of _ an)
      = class_of _ (α (a1, a2, ..., an))
>>

    where [α] is the uncurried [u.#A] operation and [β] is the
    uncurried [u.#QuotientAlgebra] operation. *)

  Lemma compute_op_quotient (u : Symbol σ)
    : ComputeOpQuotient u.#A u.#QuotientAlgebra.
H: Funext
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
u: Symbol σ
ComputeOpQuotient u.#A u.#QuotientAlgebra
  Proof.
H: Funext
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
u: Symbol σ
ComputeOpQuotient u.#A u.#QuotientAlgebra
    apply op_quotient_algebra.
  Defined.
End quotient_algebra.

Module quotient_algebra_notations.
  Global Notation "A / Φ" := (QuotientAlgebra A Φ) : Algebra_scope.
End quotient_algebra_notations.

Import quotient_algebra_notations.

(** The next section shows that A/Φ = A/Ψ whenever
    [Φ s x y <-> Ψ s x y] for all [s], [x], [y]. *)

Section path_quotient_algebra.
  Context
    {σ : Signature} (A : Algebra σ)
    (Φ : ∀ s, Relation (A s)) {CΦ : IsCongruence A Φ}
    (Ψ : ∀ s, Relation (A s)) {CΨ : IsCongruence A Ψ}.

  Lemma path_quotient_algebra `{Funext} (p : Φ = Ψ) : A/Φ = A/Ψ.
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
CΦ: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
CΨ: IsCongruence A Ψ
H: Funext
p: Φ = Ψ
A / Φ = A / Ψ
  Proof.
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
CΦ: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
CΨ: IsCongruence A Ψ
H: Funext
p: Φ = Ψ
A / Φ = A / Ψ
    by destruct p, (path_ishprop CΦ CΨ).
  Defined.

  Lemma path_quotient_algebra_iff `{Univalence}
    (R : ∀ s x y, Φ s x y <-> Ψ s x y)
    : A/Φ = A/Ψ.
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
CΦ: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
CΨ: IsCongruence A Ψ
H: Univalence
R: forall (s : Sort σ) (x y : A s),
Φ s x y <-> Ψ s x y
A / Φ = A / Ψ
  Proof.
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
CΦ: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
CΨ: IsCongruence A Ψ
H: Univalence
R: forall (s : Sort σ) (x y : A s),
Φ s x y <-> Ψ s x y
A / Φ = A / Ψ
    apply path_quotient_algebra.
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
CΦ: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
CΨ: IsCongruence A Ψ
H: Univalence
R: forall (s : Sort σ) (x y : A s),
Φ s x y <-> Ψ s x y
Φ = Ψ
    funext s x y.
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
CΦ: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
CΨ: IsCongruence A Ψ
H: Univalence
R: forall (s : Sort σ) (x y : A s),
Φ s x y <-> Ψ s x y
s: Sort σ
x, y: A s
Φ s x y = Ψ s x y
    refine (path_universe_uncurried _).
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
CΦ: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
CΨ: IsCongruence A Ψ
H: Univalence
R: forall (s : Sort σ) (x y : A s),
Φ s x y <-> Ψ s x y
s: Sort σ
x, y: A s
Φ s x y <~> Ψ s x y
    apply equiv_iff_hprop; apply R.
  Defined.
End path_quotient_algebra.

(** The following section defines the quotient homomorphism
    [hom_quotient : Homomorphism A (A/Φ)]. *)

Section hom_quotient.
  Context
    `{Funext} {σ} {A : Algebra σ}
    (Φ : ∀ s, Relation (A s)) `{!IsCongruence A Φ}.

  Definition def_hom_quotient : ∀ (s : Sort σ), A s → (A/Φ) s :=
    λ s x, class_of (Φ s) x.

  Lemma oppreserving_quotient `{Funext} (w : SymbolType σ)
      (g : Operation (A/Φ) w) (α : Operation A w)
      (G : ComputeOpQuotient A Φ α g)
      : OpPreserving def_hom_quotient α g.
H: Funext
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
H0: Funext
w: SymbolType σ
g: Operation (A / Φ) w
α: Operation A w
G: ComputeOpQuotient A Φ α g
OpPreserving def_hom_quotient α g
  Proof.
H: Funext
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
H0: Funext
w: SymbolType σ
g: Operation (A / Φ) w
α: Operation A w
G: ComputeOpQuotient A Φ α g
OpPreserving def_hom_quotient α g
    unfold ComputeOpQuotient in G.
H: Funext
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
H0: Funext
w: SymbolType σ
g: Operation (A / Φ) w
α: Operation A w
G: forall a : FamilyProd A (dom_symboltype w),
ap_operation g
  (map_family_prod (λ s : Sort σ, class_of (Φ s))
     a) =
class_of (Φ (cod_symboltype w)) (ap_operation α a)
OpPreserving def_hom_quotient α g
    induction w; cbn in *.
H: Funext
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
H0: Funext
t: Sort σ
g: carriers_quotient_algebra A Φ t
α: A t
G: Unit -> g = class_of (Φ t) α
def_hom_quotient t α = g
H: Funext
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
H0: Funext
t: Sort σ
w: ne_list (Sort σ)
g: carriers_quotient_algebra A Φ t ->
Operation (carriers_quotient_algebra A Φ) w
α: A t -> Operation A w
G: forall a : A t * FamilyProd A (dom_symboltype w),
ap_operation (g (class_of (Φ t) (fst a)))
  (map_family_prod (λ s : Sort σ, class_of (Φ s))
     (snd a)) =
class_of (Φ (cod_symboltype w))
  (ap_operation (α (fst a)) (snd a))
IHw: forall
(g : Operation (carriers_quotient_algebra A Φ) w)
(α : Operation A w),
(forall a : FamilyProd A (dom_symboltype w),
 ap_operation g
   (map_family_prod
      (λ s : Sort σ, class_of (Φ s)) a) =
 class_of (Φ (cod_symboltype w))
   (ap_operation α a)) ->
OpPreserving def_hom_quotient α g
forall x : A t,
OpPreserving def_hom_quotient 
  (α x) (g (def_hom_quotient t x))
    -
H: Funext
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
H0: Funext
t: Sort σ
g: carriers_quotient_algebra A Φ t
α: A t
G: Unit -> g = class_of (Φ t) α
def_hom_quotient t α = g by destruct (G tt)^.
    -
H: Funext
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
H0: Funext
t: Sort σ
w: ne_list (Sort σ)
g: carriers_quotient_algebra A Φ t ->
Operation (carriers_quotient_algebra A Φ) w
α: A t -> Operation A w
G: forall a : A t * FamilyProd A (dom_symboltype w),
ap_operation (g (class_of (Φ t) (fst a)))
  (map_family_prod (λ s : Sort σ, class_of (Φ s))
     (snd a)) =
class_of (Φ (cod_symboltype w))
  (ap_operation (α (fst a)) (snd a))
IHw: forall
(g : Operation (carriers_quotient_algebra A Φ) w)
(α : Operation A w),
(forall a : FamilyProd A (dom_symboltype w),
 ap_operation g
   (map_family_prod
      (λ s : Sort σ, class_of (Φ s)) a) =
 class_of (Φ (cod_symboltype w))
   (ap_operation α a)) ->
OpPreserving def_hom_quotient α g
forall x : A t,
OpPreserving def_hom_quotient (α x)
  (g (def_hom_quotient t x)) intro x.
H: Funext
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
H0: Funext
t: Sort σ
w: ne_list (Sort σ)
g: carriers_quotient_algebra A Φ t ->
Operation (carriers_quotient_algebra A Φ) w
α: A t -> Operation A w
G: forall a : A t * FamilyProd A (dom_symboltype w),
ap_operation (g (class_of (Φ t) (fst a)))
  (map_family_prod (λ s : Sort σ, class_of (Φ s))
     (snd a)) =
class_of (Φ (cod_symboltype w))
  (ap_operation (α (fst a)) (snd a))
IHw: forall
(g : Operation (carriers_quotient_algebra A Φ) w)
(α : Operation A w),
(forall a : FamilyProd A (dom_symboltype w),
 ap_operation g
   (map_family_prod
      (λ s : Sort σ, class_of (Φ s)) a) =
 class_of (Φ (cod_symboltype w))
   (ap_operation α a)) ->
OpPreserving def_hom_quotient α g
x: A t
OpPreserving def_hom_quotient (α x)
  (g (def_hom_quotient t x)) apply IHw.
H: Funext
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
H0: Funext
t: Sort σ
w: ne_list (Sort σ)
g: carriers_quotient_algebra A Φ t ->
Operation (carriers_quotient_algebra A Φ) w
α: A t -> Operation A w
G: forall a : A t * FamilyProd A (dom_symboltype w),
ap_operation (g (class_of (Φ t) (fst a)))
  (map_family_prod (λ s : Sort σ, class_of (Φ s))
     (snd a)) =
class_of (Φ (cod_symboltype w))
  (ap_operation (α (fst a)) (snd a))
IHw: forall
(g : Operation (carriers_quotient_algebra A Φ) w)
(α : Operation A w),
(forall a : FamilyProd A (dom_symboltype w),
 ap_operation g
   (map_family_prod
      (λ s : Sort σ, class_of (Φ s)) a) =
 class_of (Φ (cod_symboltype w))
   (ap_operation α a)) ->
OpPreserving def_hom_quotient α g
x: A t
forall a : FamilyProd A (dom_symboltype w),
ap_operation (g (def_hom_quotient t x))
  (map_family_prod (λ s : Sort σ, class_of (Φ s)) a) =
class_of (Φ (cod_symboltype w)) (ap_operation (α x) a) intro a.
H: Funext
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
H0: Funext
t: Sort σ
w: ne_list (Sort σ)
g: carriers_quotient_algebra A Φ t ->
Operation (carriers_quotient_algebra A Φ) w
α: A t -> Operation A w
G: forall a : A t * FamilyProd A (dom_symboltype w),
ap_operation (g (class_of (Φ t) (fst a)))
  (map_family_prod (λ s : Sort σ, class_of (Φ s))
     (snd a)) =
class_of (Φ (cod_symboltype w))
  (ap_operation (α (fst a)) (snd a))
IHw: forall
(g : Operation (carriers_quotient_algebra A Φ) w)
(α : Operation A w),
(forall a : FamilyProd A (dom_symboltype w),
 ap_operation g
   (map_family_prod
      (λ s : Sort σ, class_of (Φ s)) a) =
 class_of (Φ (cod_symboltype w))
   (ap_operation α a)) ->
OpPreserving def_hom_quotient α g
x: A t
a: FamilyProd A (dom_symboltype w)
ap_operation (g (def_hom_quotient t x))
  (map_family_prod (λ s : Sort σ, class_of (Φ s)) a) =
class_of (Φ (cod_symboltype w)) (ap_operation (α x) a) apply (G (x,a)).
  Defined.

  Global Instance is_homomorphism_quotient `{Funext}
    : IsHomomorphism def_hom_quotient.
H: Funext
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
H0: Funext
IsHomomorphism def_hom_quotient
  Proof.
H: Funext
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
H0: Funext
IsHomomorphism def_hom_quotient
    intro u.
H: Funext
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
H0: Funext
u: Symbol σ
OpPreserving def_hom_quotient u.#A u.#(A / Φ) apply oppreserving_quotient, compute_op_quotient.
  Defined.

  Definition hom_quotient : Homomorphism A (A/Φ)
    := BuildHomomorphism def_hom_quotient.

  Global Instance surjection_quotient
    : ∀ s, IsSurjection (hom_quotient s).
H: Funext
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
forall s : Sort σ,
ReflectiveSubuniverse.IsConnMap (Tr (-1))
  (hom_quotient s)
  Proof.
H: Funext
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
forall s : Sort σ,
ReflectiveSubuniverse.IsConnMap (Tr (-1))
  (hom_quotient s)
    intro s.
H: Funext
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
s: Sort σ
ReflectiveSubuniverse.IsConnMap (Tr (-1))
  (hom_quotient s) apply issurj_class_of.
  Qed.
End hom_quotient.

(** If [Φ s x y] implies [x = y], then homomorphism [hom_quotient Φ]
    is an isomorphism. *)

Global Instance is_isomorphism_quotient `{Univalence}
  {σ : Signature} {A : Algebra σ} (Φ : ∀ s, Relation (A s))
  `{!IsCongruence A Φ} (P : ∀ s x y, Φ s x y → x = y)
  : IsIsomorphism (hom_quotient Φ).
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
P: forall (s : Sort σ) (x y : A s), Φ s x y -> x = y
IsIsomorphism (hom_quotient Φ)
Proof.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
P: forall (s : Sort σ) (x y : A s), Φ s x y -> x = y
IsIsomorphism (hom_quotient Φ)
  intro s.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
P: forall (s : Sort σ) (x y : A s), Φ s x y -> x = y
s: Sort σ
IsEquiv (hom_quotient Φ s)
  apply isequiv_surj_emb; [exact _ |].
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
P: forall (s : Sort σ) (x y : A s), Φ s x y -> x = y
s: Sort σ
IsEmbedding (hom_quotient Φ s)
  apply isembedding_isinj_hset.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
P: forall (s : Sort σ) (x y : A s), Φ s x y -> x = y
s: Sort σ
isinj (hom_quotient Φ s)
  intros x y p.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
P: forall (s : Sort σ) (x y : A s), Φ s x y -> x = y
s: Sort σ
x, y: A s
p: hom_quotient Φ s x = hom_quotient Φ s y
x = y
  by apply P, (related_quotient_paths (Φ s)).
Qed.

(** This section develops the universal mapping property
    [ump_quotient_algebra] of the quotient algebra. *)

Section ump_quotient_algebra.
  Context
    `{Univalence} {σ} {A B : Algebra σ} `{!IsHSetAlgebra B}
    (Φ : ∀ s, Relation (A s)) `{!IsCongruence A Φ}.

(** In the nested section below we show that if [f : Homomorphism A B]
    maps elements related by [Φ] to equal elements, there is a
    [Homomorphism (A/Φ) B] out of the quotient algebra satisfying
    [compute_quotient_algebra_mapout] below. *)

  Section quotient_algebra_mapout.
    Context
      (f : Homomorphism A B)
      (R : ∀ s (x y : A s), Φ s x y → f s x = f s y).

    Definition def_hom_quotient_algebra_mapout
      : ∀ (s : Sort σ), (A/Φ) s → B s
      := λ s, (equiv_quotient_ump (Φ s) (Build_HSet (B s)))^-1 (f s; R s).

    Lemma oppreserving_quotient_algebra_mapout {w : SymbolType σ}
      (g : Operation (A/Φ) w) (α : Operation A w) (β : Operation B w)
      (G : ComputeOpQuotient A Φ α g) (P : OpPreserving f α β)
      : OpPreserving def_hom_quotient_algebra_mapout g β.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
f: Homomorphism A B
R: forall (s : Sort σ) 
(x y : A s), Φ s x y -> f s x = f s y
w: SymbolType σ
g: Operation (A / Φ) w
α: Operation A w
β: Operation B w
G: ComputeOpQuotient A Φ α g
P: OpPreserving f α β
OpPreserving def_hom_quotient_algebra_mapout g β
    Proof.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
f: Homomorphism A B
R: forall (s : Sort σ) 
(x y : A s), Φ s x y -> f s x = f s y
w: SymbolType σ
g: Operation (A / Φ) w
α: Operation A w
β: Operation B w
G: ComputeOpQuotient A Φ α g
P: OpPreserving f α β
OpPreserving def_hom_quotient_algebra_mapout g β
      unfold ComputeOpQuotient in G.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
f: Homomorphism A B
R: forall (s : Sort σ) 
(x y : A s), Φ s x y -> f s x = f s y
w: SymbolType σ
g: Operation (A / Φ) w
α: Operation A w
β: Operation B w
G: forall a : FamilyProd A (dom_symboltype w),
ap_operation g
  (map_family_prod (λ s : Sort σ, class_of (Φ s))
     a) =
class_of (Φ (cod_symboltype w)) (ap_operation α a)
P: OpPreserving f α β
OpPreserving def_hom_quotient_algebra_mapout g β
      induction w; cbn in *.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
f: Homomorphism A B
R: forall (s : Sort σ) 
(x y : A s), Φ s x y -> f s x = f s y
t: Sort σ
g: carriers_quotient_algebra A Φ t
α: A t
β: B t
G: Unit -> g = class_of (Φ t) α
P: f t α = β
Quotient_rec (Φ t) (B t) (f t) (R t) g = β
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
f: Homomorphism A B
R: forall (s : Sort σ) 
(x y : A s), Φ s x y -> f s x = f s y
t: Sort σ
w: ne_list (Sort σ)
g: carriers_quotient_algebra A Φ t ->
Operation (carriers_quotient_algebra A Φ) w
α: A t -> Operation A w
β: B t -> Operation B w
G: forall a : A t * FamilyProd A (dom_symboltype w),
ap_operation (g (class_of (Φ t) (fst a)))
  (map_family_prod (λ s : Sort σ, class_of (Φ s))
     (snd a)) =
class_of (Φ (cod_symboltype w))
  (ap_operation (α (fst a)) (snd a))
P: forall x : A t, OpPreserving f (α x) (β (f t x))
IHw: forall
(g : Operation (carriers_quotient_algebra A Φ) w)
(α : Operation A w) 
(β : Operation B w),
(forall a : FamilyProd A (dom_symboltype w),
 ap_operation g
   (map_family_prod
      (λ s : Sort σ, class_of (Φ s)) a) =
 class_of (Φ (cod_symboltype w))
   (ap_operation α a)) ->
OpPreserving f α β ->
OpPreserving def_hom_quotient_algebra_mapout g β
forall x : carriers_quotient_algebra A Φ t,
OpPreserving def_hom_quotient_algebra_mapout 
  (g x) (β (Quotient_rec (Φ t) (B t) (f t) (R t) x))
      -
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
f: Homomorphism A B
R: forall (s : Sort σ) 
(x y : A s), Φ s x y -> f s x = f s y
t: Sort σ
g: carriers_quotient_algebra A Φ t
α: A t
β: B t
G: Unit -> g = class_of (Φ t) α
P: f t α = β
Quotient_rec (Φ t) (B t) (f t) (R t) g = β destruct (G tt)^.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
f: Homomorphism A B
R: forall (s : Sort σ) 
(x y : A s), Φ s x y -> f s x = f s y
t: Sort σ
α: A t
β: B t
G: Unit -> class_of (Φ t) α = class_of (Φ t) α
P: f t α = β
Quotient_rec (Φ t) (B t) (f t) (R t)
  (class_of (Φ t) α) = β apply P.
      -
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
f: Homomorphism A B
R: forall (s : Sort σ) 
(x y : A s), Φ s x y -> f s x = f s y
t: Sort σ
w: ne_list (Sort σ)
g: carriers_quotient_algebra A Φ t ->
Operation (carriers_quotient_algebra A Φ) w
α: A t -> Operation A w
β: B t -> Operation B w
G: forall a : A t * FamilyProd A (dom_symboltype w),
ap_operation (g (class_of (Φ t) (fst a)))
  (map_family_prod (λ s : Sort σ, class_of (Φ s))
     (snd a)) =
class_of (Φ (cod_symboltype w))
  (ap_operation (α (fst a)) (snd a))
P: forall x : A t, OpPreserving f (α x) (β (f t x))
IHw: forall
(g : Operation (carriers_quotient_algebra A Φ) w)
(α : Operation A w) 
(β : Operation B w),
(forall a : FamilyProd A (dom_symboltype w),
 ap_operation g
   (map_family_prod
      (λ s : Sort σ, class_of (Φ s)) a) =
 class_of (Φ (cod_symboltype w))
   (ap_operation α a)) ->
OpPreserving f α β ->
OpPreserving def_hom_quotient_algebra_mapout g β
forall x : carriers_quotient_algebra A Φ t,
OpPreserving def_hom_quotient_algebra_mapout (g x)
  (β (Quotient_rec (Φ t) (B t) (f t) (R t) x)) refine (Quotient_ind_hprop (Φ t) _ _).
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
f: Homomorphism A B
R: forall (s : Sort σ) 
(x y : A s), Φ s x y -> f s x = f s y
t: Sort σ
w: ne_list (Sort σ)
g: carriers_quotient_algebra A Φ t ->
Operation (carriers_quotient_algebra A Φ) w
α: A t -> Operation A w
β: B t -> Operation B w
G: forall a : A t * FamilyProd A (dom_symboltype w),
ap_operation (g (class_of (Φ t) (fst a)))
  (map_family_prod (λ s : Sort σ, class_of (Φ s))
     (snd a)) =
class_of (Φ (cod_symboltype w))
  (ap_operation (α (fst a)) (snd a))
P: forall x : A t, OpPreserving f (α x) (β (f t x))
IHw: forall
(g : Operation (carriers_quotient_algebra A Φ) w)
(α : Operation A w) 
(β : Operation B w),
(forall a : FamilyProd A (dom_symboltype w),
 ap_operation g
   (map_family_prod
      (λ s : Sort σ, class_of (Φ s)) a) =
 class_of (Φ (cod_symboltype w))
   (ap_operation α a)) ->
OpPreserving f α β ->
OpPreserving def_hom_quotient_algebra_mapout g β
forall x : A t,
OpPreserving def_hom_quotient_algebra_mapout
  (g (class_of (Φ t) x))
  (β
     (Quotient_rec (Φ t) (B t) (f t) (R t)
        (class_of (Φ t) x))) intro x.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
f: Homomorphism A B
R: forall (s : Sort σ) 
(x y : A s), Φ s x y -> f s x = f s y
t: Sort σ
w: ne_list (Sort σ)
g: carriers_quotient_algebra A Φ t ->
Operation (carriers_quotient_algebra A Φ) w
α: A t -> Operation A w
β: B t -> Operation B w
G: forall a : A t * FamilyProd A (dom_symboltype w),
ap_operation (g (class_of (Φ t) (fst a)))
  (map_family_prod (λ s : Sort σ, class_of (Φ s))
     (snd a)) =
class_of (Φ (cod_symboltype w))
  (ap_operation (α (fst a)) (snd a))
P: forall x : A t, OpPreserving f (α x) (β (f t x))
IHw: forall
(g : Operation (carriers_quotient_algebra A Φ) w)
(α : Operation A w) 
(β : Operation B w),
(forall a : FamilyProd A (dom_symboltype w),
 ap_operation g
   (map_family_prod
      (λ s : Sort σ, class_of (Φ s)) a) =
 class_of (Φ (cod_symboltype w))
   (ap_operation α a)) ->
OpPreserving f α β ->
OpPreserving def_hom_quotient_algebra_mapout g β
x: A t
OpPreserving def_hom_quotient_algebra_mapout
  (g (class_of (Φ t) x))
  (β
     (Quotient_rec (Φ t) (B t) (f t) (R t)
        (class_of (Φ t) x)))
        apply (IHw (g (class_of (Φ t) x)) (α x) (β (f t x))).
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
f: Homomorphism A B
R: forall (s : Sort σ) 
(x y : A s), Φ s x y -> f s x = f s y
t: Sort σ
w: ne_list (Sort σ)
g: carriers_quotient_algebra A Φ t ->
Operation (carriers_quotient_algebra A Φ) w
α: A t -> Operation A w
β: B t -> Operation B w
G: forall a : A t * FamilyProd A (dom_symboltype w),
ap_operation (g (class_of (Φ t) (fst a)))
  (map_family_prod (λ s : Sort σ, class_of (Φ s))
     (snd a)) =
class_of (Φ (cod_symboltype w))
  (ap_operation (α (fst a)) (snd a))
P: forall x : A t, OpPreserving f (α x) (β (f t x))
IHw: forall
(g : Operation (carriers_quotient_algebra A Φ) w)
(α : Operation A w) 
(β : Operation B w),
(forall a : FamilyProd A (dom_symboltype w),
 ap_operation g
   (map_family_prod
      (λ s : Sort σ, class_of (Φ s)) a) =
 class_of (Φ (cod_symboltype w))
   (ap_operation α a)) ->
OpPreserving f α β ->
OpPreserving def_hom_quotient_algebra_mapout g β
x: A t
forall a : FamilyProd A (dom_symboltype w),
ap_operation (g (class_of (Φ t) x))
  (map_family_prod (λ s : Sort σ, class_of (Φ s)) a) =
class_of (Φ (cod_symboltype w)) (ap_operation (α x) a)
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
f: Homomorphism A B
R: forall (s : Sort σ) 
(x y : A s), Φ s x y -> f s x = f s y
t: Sort σ
w: ne_list (Sort σ)
g: carriers_quotient_algebra A Φ t ->
Operation (carriers_quotient_algebra A Φ) w
α: A t -> Operation A w
β: B t -> Operation B w
G: forall a : A t * FamilyProd A (dom_symboltype w),
ap_operation (g (class_of (Φ t) (fst a)))
  (map_family_prod (λ s : Sort σ, class_of (Φ s))
     (snd a)) =
class_of (Φ (cod_symboltype w))
  (ap_operation (α (fst a)) (snd a))
P: forall x : A t, OpPreserving f (α x) (β (f t x))
IHw: forall
(g : Operation (carriers_quotient_algebra A Φ) w)
(α : Operation A w) 
(β : Operation B w),
(forall a : FamilyProd A (dom_symboltype w),
 ap_operation g
   (map_family_prod
      (λ s : Sort σ, class_of (Φ s)) a) =
 class_of (Φ (cod_symboltype w))
   (ap_operation α a)) ->
OpPreserving f α β ->
OpPreserving def_hom_quotient_algebra_mapout g β
x: A t
OpPreserving f (α x) (β (f t x))
        +
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
f: Homomorphism A B
R: forall (s : Sort σ) 
(x y : A s), Φ s x y -> f s x = f s y
t: Sort σ
w: ne_list (Sort σ)
g: carriers_quotient_algebra A Φ t ->
Operation (carriers_quotient_algebra A Φ) w
α: A t -> Operation A w
β: B t -> Operation B w
G: forall a : A t * FamilyProd A (dom_symboltype w),
ap_operation (g (class_of (Φ t) (fst a)))
  (map_family_prod (λ s : Sort σ, class_of (Φ s))
     (snd a)) =
class_of (Φ (cod_symboltype w))
  (ap_operation (α (fst a)) (snd a))
P: forall x : A t, OpPreserving f (α x) (β (f t x))
IHw: forall
(g : Operation (carriers_quotient_algebra A Φ) w)
(α : Operation A w) 
(β : Operation B w),
(forall a : FamilyProd A (dom_symboltype w),
 ap_operation g
   (map_family_prod
      (λ s : Sort σ, class_of (Φ s)) a) =
 class_of (Φ (cod_symboltype w))
   (ap_operation α a)) ->
OpPreserving f α β ->
OpPreserving def_hom_quotient_algebra_mapout g β
x: A t
forall a : FamilyProd A (dom_symboltype w),
ap_operation (g (class_of (Φ t) x))
  (map_family_prod (λ s : Sort σ, class_of (Φ s)) a) =
class_of (Φ (cod_symboltype w)) (ap_operation (α x) a) intro a.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
f: Homomorphism A B
R: forall (s : Sort σ) 
(x y : A s), Φ s x y -> f s x = f s y
t: Sort σ
w: ne_list (Sort σ)
g: carriers_quotient_algebra A Φ t ->
Operation (carriers_quotient_algebra A Φ) w
α: A t -> Operation A w
β: B t -> Operation B w
G: forall a : A t * FamilyProd A (dom_symboltype w),
ap_operation (g (class_of (Φ t) (fst a)))
  (map_family_prod (λ s : Sort σ, class_of (Φ s))
     (snd a)) =
class_of (Φ (cod_symboltype w))
  (ap_operation (α (fst a)) (snd a))
P: forall x : A t, OpPreserving f (α x) (β (f t x))
IHw: forall
(g : Operation (carriers_quotient_algebra A Φ) w)
(α : Operation A w) 
(β : Operation B w),
(forall a : FamilyProd A (dom_symboltype w),
 ap_operation g
   (map_family_prod
      (λ s : Sort σ, class_of (Φ s)) a) =
 class_of (Φ (cod_symboltype w))
   (ap_operation α a)) ->
OpPreserving f α β ->
OpPreserving def_hom_quotient_algebra_mapout g β
x: A t
a: FamilyProd A (dom_symboltype w)
ap_operation (g (class_of (Φ t) x))
  (map_family_prod (λ s : Sort σ, class_of (Φ s)) a) =
class_of (Φ (cod_symboltype w)) (ap_operation (α x) a) apply (G (x,a)).
        +
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
f: Homomorphism A B
R: forall (s : Sort σ) 
(x y : A s), Φ s x y -> f s x = f s y
t: Sort σ
w: ne_list (Sort σ)
g: carriers_quotient_algebra A Φ t ->
Operation (carriers_quotient_algebra A Φ) w
α: A t -> Operation A w
β: B t -> Operation B w
G: forall a : A t * FamilyProd A (dom_symboltype w),
ap_operation (g (class_of (Φ t) (fst a)))
  (map_family_prod (λ s : Sort σ, class_of (Φ s))
     (snd a)) =
class_of (Φ (cod_symboltype w))
  (ap_operation (α (fst a)) (snd a))
P: forall x : A t, OpPreserving f (α x) (β (f t x))
IHw: forall
(g : Operation (carriers_quotient_algebra A Φ) w)
(α : Operation A w) 
(β : Operation B w),
(forall a : FamilyProd A (dom_symboltype w),
 ap_operation g
   (map_family_prod
      (λ s : Sort σ, class_of (Φ s)) a) =
 class_of (Φ (cod_symboltype w))
   (ap_operation α a)) ->
OpPreserving f α β ->
OpPreserving def_hom_quotient_algebra_mapout g β
x: A t
OpPreserving f (α x) (β (f t x)) apply P.
    Defined.

    Global Instance is_homomorphism_quotient_algebra_mapout
      : IsHomomorphism def_hom_quotient_algebra_mapout.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
f: Homomorphism A B
R: forall (s : Sort σ) 
(x y : A s), Φ s x y -> f s x = f s y
IsHomomorphism def_hom_quotient_algebra_mapout
    Proof.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
f: Homomorphism A B
R: forall (s : Sort σ) 
(x y : A s), Φ s x y -> f s x = f s y
IsHomomorphism def_hom_quotient_algebra_mapout
      intro u.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
f: Homomorphism A B
R: forall (s : Sort σ) 
(x y : A s), Φ s x y -> f s x = f s y
u: Symbol σ
OpPreserving def_hom_quotient_algebra_mapout
  u.#(A / Φ) u.#B
      eapply oppreserving_quotient_algebra_mapout.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
f: Homomorphism A B
R: forall (s : Sort σ) 
(x y : A s), Φ s x y -> f s x = f s y
u: Symbol σ
ComputeOpQuotient A Φ ?α u.#(A / Φ)
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
f: Homomorphism A B
R: forall (s : Sort σ) 
(x y : A s), Φ s x y -> f s x = f s y
u: Symbol σ
OpPreserving f ?α u.#B
      -
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
f: Homomorphism A B
R: forall (s : Sort σ) 
(x y : A s), Φ s x y -> f s x = f s y
u: Symbol σ
ComputeOpQuotient A Φ ?α u.#(A / Φ) apply compute_op_quotient.
      -
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
f: Homomorphism A B
R: forall (s : Sort σ) 
(x y : A s), Φ s x y -> f s x = f s y
u: Symbol σ
OpPreserving f u.#A u.#B apply f.
    Defined.

    Definition hom_quotient_algebra_mapout
      : Homomorphism (A/Φ) B
      := BuildHomomorphism def_hom_quotient_algebra_mapout.

(** The computation rule for [hom_quotient_algebra_mapout] is

<<
      hom_quotient_algebra_mapout s (class_of (Φ s) x) = f s x.
>>
*)

    Lemma compute_quotient_algebra_mapout
      : ∀ (s : Sort σ) (x : A s),
        hom_quotient_algebra_mapout s (class_of (Φ s) x) = f s x.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
f: Homomorphism A B
R: forall (s : Sort σ) 
(x y : A s), Φ s x y -> f s x = f s y
forall (s : Sort σ) (x : A s),
hom_quotient_algebra_mapout s (class_of (Φ s) x) =
f s x
    Proof.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
f: Homomorphism A B
R: forall (s : Sort σ) 
(x y : A s), Φ s x y -> f s x = f s y
forall (s : Sort σ) (x : A s),
hom_quotient_algebra_mapout s (class_of (Φ s) x) =
f s x
      reflexivity.
    Defined.

  End quotient_algebra_mapout.

  Definition hom_quotient_algebra_mapin (g : Homomorphism (A/Φ) B)
    : Homomorphism A B
    := hom_compose g (hom_quotient Φ).

  Lemma ump_quotient_algebra_lr :
    {f : Homomorphism A B | ∀ s (x y : A s), Φ s x y → f s x = f s y}
    → Homomorphism (A/Φ) B.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
{f : Homomorphism A B &
forall (s : Sort σ) (x y : A s),
Φ s x y -> f s x = f s y} -> Homomorphism (A / Φ) B
  Proof.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
{f : Homomorphism A B &
forall (s : Sort σ) (x y : A s),
Φ s x y -> f s x = f s y} -> Homomorphism (A / Φ) B
    intros [f P].
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
f: Homomorphism A B
P: forall (s : Sort σ) 
(x y : A s), Φ s x y -> f s x = f s y
Homomorphism (A / Φ) B exists (hom_quotient_algebra_mapout f P).
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
f: Homomorphism A B
P: forall (s : Sort σ) 
(x y : A s), Φ s x y -> f s x = f s y
IsHomomorphism (hom_quotient_algebra_mapout f P) exact _.
  Defined.

  Lemma ump_quotient_algebra_rl :
    Homomorphism (A/Φ) B →
    {f : Homomorphism A B | ∀ s (x y : A s), Φ s x y → f s x = f s y}.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Homomorphism (A / Φ) B ->
{f : Homomorphism A B &
forall (s : Sort σ) (x y : A s),
Φ s x y -> f s x = f s y}
  Proof.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Homomorphism (A / Φ) B ->
{f : Homomorphism A B &
forall (s : Sort σ) (x y : A s),
Φ s x y -> f s x = f s y}
    intro g.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
g: Homomorphism (A / Φ) B
{f : Homomorphism A B &
forall (s : Sort σ) (x y : A s),
Φ s x y -> f s x = f s y}
    exists (hom_quotient_algebra_mapin g).
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
g: Homomorphism (A / Φ) B
forall (s : Sort σ) (x y : A s),
Φ s x y ->
hom_quotient_algebra_mapin g s x =
hom_quotient_algebra_mapin g s y
    intros s x y E.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
g: Homomorphism (A / Φ) B
s: Sort σ
x, y: A s
E: Φ s x y
hom_quotient_algebra_mapin g s x =
hom_quotient_algebra_mapin g s y
    exact (transport (λ z, g s (class_of (Φ s) x) = g s z)
            (qglue E) idpath).
  Defined.

(** The universal mapping property of the quotient algebra. For each
    homomorphism [f : Homomorphism A B], mapping elements related by
    [Φ] to equal elements, there is a unique homomorphism
    [g : Homomorphism (A/Φ) B] satisfying

<<
      f = hom_compose g (hom_quotient Φ).
>>
*)

  Lemma ump_quotient_algebra
    : {f : Homomorphism A B | ∀ s (x y : A s), Φ s x y → f s x = f s y}
     <~>
      Homomorphism (A/Φ) B.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
{f : Homomorphism A B &
forall (s : Sort σ) (x y : A s),
Φ s x y -> f s x = f s y} <~> Homomorphism (A / Φ) B
  Proof.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
{f : Homomorphism A B &
forall (s : Sort σ) (x y : A s),
Φ s x y -> f s x = f s y} <~> Homomorphism (A / Φ) B
    apply (equiv_adjointify
             ump_quotient_algebra_lr ump_quotient_algebra_rl).
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
(λ x : Homomorphism (A / Φ) B,
 ump_quotient_algebra_lr (ump_quotient_algebra_rl x)) ==
idmap
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
(λ
 x : {f : Homomorphism A B &
     forall (s : Sort σ) 
     (x y : A s), Φ s x y -> f s x = f s y},
 ump_quotient_algebra_rl (ump_quotient_algebra_lr x)) ==
idmap
    -
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
(λ x : Homomorphism (A / Φ) B,
 ump_quotient_algebra_lr (ump_quotient_algebra_rl x)) ==
idmap intro G.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
G: Homomorphism (A / Φ) B
ump_quotient_algebra_lr (ump_quotient_algebra_rl G) =
G
      apply path_hset_homomorphism.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
G: Homomorphism (A / Φ) B
ump_quotient_algebra_lr (ump_quotient_algebra_rl G) =
G
      funext s.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
G: Homomorphism (A / Φ) B
s: Sort σ
ump_quotient_algebra_lr (ump_quotient_algebra_rl G) s =
G s
      exact (eissect (equiv_quotient_ump (Φ s) _) (G s)).
    -
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
(λ
 x : {f : Homomorphism A B &
     forall (s : Sort σ) (x y : A s),
     Φ s x y -> f s x = f s y},
 ump_quotient_algebra_rl (ump_quotient_algebra_lr x)) ==
idmap intro F.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
F: {f : Homomorphism A B &
forall (s : Sort σ) 
(x y : A s), Φ s x y -> f s x = f s y}
ump_quotient_algebra_rl (ump_quotient_algebra_lr F) =
F
      apply path_sigma_hprop.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
F: {f : Homomorphism A B &
forall (s : Sort σ) 
(x y : A s), Φ s x y -> f s x = f s y}
(ump_quotient_algebra_rl (ump_quotient_algebra_lr F)).1 =
F.1
      by apply path_hset_homomorphism.
  Defined.
End ump_quotient_algebra.