(** This file proves the third isomorphism theorem,
    [isomorphic_third_isomorphism]. *)
Require Import
  Colimits.Quotient
  Classes.interfaces.canonical_names
  Classes.theory.ua_quotient_algebra
  Classes.theory.ua_isomorphic
  Classes.theory.ua_first_isomorphism
  Spaces.List.Core.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

Import algebra_notations quotient_algebra_notations isomorphic_notations.

(** This section defines the quotient [cong_quotient] of two
    congruences [Φ] and [Ψ], where [Ψ] is a subcongruence of [Φ].
    It is shown that [cong_quotient] is a congruence. *)

Section cong_quotient.
  Context
    `{Univalence}
    {σ : Signature} {A : Algebra σ}
    (Φ : ∀ s, Relation (A s)) `{!IsCongruence A Φ}
    (Ψ : ∀ s, Relation (A s)) `{!IsCongruence A Ψ}
    (subrel : ∀ (s : Sort σ) (x y : A s), Ψ s x y → Φ s x y).

  Definition cong_quotient (_ : ∀ s x y, Ψ s x y → Φ s x y)
    (s : Sort σ) (a b : (A/Ψ) s)
    := ∀ (x y : A s), in_class (Ψ s) a x → in_class (Ψ s) b y → Φ s x y.

  Global Instance equivalence_relation_quotient (s : Sort σ)
    : EquivRel (cong_quotient subrel s).
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
EquivRel (cong_quotient subrel s)
  Proof.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
EquivRel (cong_quotient subrel s)
    constructor.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
Reflexive (cong_quotient subrel s)
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
Symmetric (cong_quotient subrel s)
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
Transitive (cong_quotient subrel s)
    -
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
Reflexive (cong_quotient subrel s) refine (Quotient_ind_hprop (Ψ s) _ _).
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
forall x : A s,
cong_quotient subrel s (class_of (Ψ s) x)
  (class_of (Ψ s) x) intros x y z P Q.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
x, y, z: A s
P: in_class (Ψ s) (class_of (Ψ s) x) y
Q: in_class (Ψ s) (class_of (Ψ s) x) z
Φ s y z
      apply subrel.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
x, y, z: A s
P: in_class (Ψ s) (class_of (Ψ s) x) y
Q: in_class (Ψ s) (class_of (Ψ s) x) z
Ψ s y z
      by transitivity x.
    -
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
Symmetric (cong_quotient subrel s) refine (Quotient_ind_hprop (Ψ s) _ _).
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
forall (x : A s) (y : (A / Ψ) s),
cong_quotient subrel s (class_of (Ψ s) x) y ->
cong_quotient subrel s y (class_of (Ψ s) x) intro x1.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
x1: A s
forall y : (A / Ψ) s,
cong_quotient subrel s (class_of (Ψ s) x1) y ->
cong_quotient subrel s y (class_of (Ψ s) x1)
      refine (Quotient_ind_hprop (Ψ s) _ _).
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
x1: A s
forall x : A s,
cong_quotient subrel s (class_of (Ψ s) x1)
  (class_of (Ψ s) x) ->
cong_quotient subrel s (class_of (Ψ s) x)
  (class_of (Ψ s) x1) intros x2 C y1 y2 P Q.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
x1, x2: A s
C: cong_quotient subrel s 
  (class_of (Ψ s) x1) 
  (class_of (Ψ s) x2)
y1, y2: A s
P: in_class (Ψ s) (class_of (Ψ s) x2) y1
Q: in_class (Ψ s) (class_of (Ψ s) x1) y2
Φ s y1 y2
      symmetry.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
x1, x2: A s
C: cong_quotient subrel s 
  (class_of (Ψ s) x1) 
  (class_of (Ψ s) x2)
y1, y2: A s
P: in_class (Ψ s) (class_of (Ψ s) x2) y1
Q: in_class (Ψ s) (class_of (Ψ s) x1) y2
Φ s y2 y1
      by apply C.
    -
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
Transitive (cong_quotient subrel s) refine (Quotient_ind_hprop (Ψ s) _ _).
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
forall (x : A s) (y z : (A / Ψ) s),
cong_quotient subrel s (class_of (Ψ s) x) y ->
cong_quotient subrel s y z ->
cong_quotient subrel s (class_of (Ψ s) x) z intro x1.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
x1: A s
forall y z : (A / Ψ) s,
cong_quotient subrel s (class_of (Ψ s) x1) y ->
cong_quotient subrel s y z ->
cong_quotient subrel s (class_of (Ψ s) x1) z
      refine (Quotient_ind_hprop (Ψ s) _ _).
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
x1: A s
forall (x : A s) (z : (A / Ψ) s),
cong_quotient subrel s (class_of (Ψ s) x1)
  (class_of (Ψ s) x) ->
cong_quotient subrel s (class_of (Ψ s) x) z ->
cong_quotient subrel s (class_of (Ψ s) x1) z intro x2.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
x1, x2: A s
forall z : (A / Ψ) s,
cong_quotient subrel s (class_of (Ψ s) x1)
  (class_of (Ψ s) x2) ->
cong_quotient subrel s (class_of (Ψ s) x2) z ->
cong_quotient subrel s (class_of (Ψ s) x1) z
      refine (Quotient_ind_hprop (Ψ s) _ _).
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
x1, x2: A s
forall x : A s,
cong_quotient subrel s (class_of (Ψ s) x1)
  (class_of (Ψ s) x2) ->
cong_quotient subrel s (class_of (Ψ s) x2)
  (class_of (Ψ s) x) ->
cong_quotient subrel s (class_of (Ψ s) x1)
  (class_of (Ψ s) x) intros x3 C D y1 y2 P Q.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
x1, x2, x3: A s
C: cong_quotient subrel s 
  (class_of (Ψ s) x1) 
  (class_of (Ψ s) x2)
D: cong_quotient subrel s 
  (class_of (Ψ s) x2) 
  (class_of (Ψ s) x3)
y1, y2: A s
P: in_class (Ψ s) (class_of (Ψ s) x1) y1
Q: in_class (Ψ s) (class_of (Ψ s) x3) y2
Φ s y1 y2
      transitivity x2.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
x1, x2, x3: A s
C: cong_quotient subrel s 
  (class_of (Ψ s) x1) 
  (class_of (Ψ s) x2)
D: cong_quotient subrel s 
  (class_of (Ψ s) x2) 
  (class_of (Ψ s) x3)
y1, y2: A s
P: in_class (Ψ s) (class_of (Ψ s) x1) y1
Q: in_class (Ψ s) (class_of (Ψ s) x3) y2
Φ s y1 x2
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
x1, x2, x3: A s
C: cong_quotient subrel s 
  (class_of (Ψ s) x1) 
  (class_of (Ψ s) x2)
D: cong_quotient subrel s 
  (class_of (Ψ s) x2) 
  (class_of (Ψ s) x3)
y1, y2: A s
P: in_class (Ψ s) (class_of (Ψ s) x1) y1
Q: in_class (Ψ s) (class_of (Ψ s) x3) y2
Φ s x2 y2
      +
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
x1, x2, x3: A s
C: cong_quotient subrel s 
  (class_of (Ψ s) x1) 
  (class_of (Ψ s) x2)
D: cong_quotient subrel s 
  (class_of (Ψ s) x2) 
  (class_of (Ψ s) x3)
y1, y2: A s
P: in_class (Ψ s) (class_of (Ψ s) x1) y1
Q: in_class (Ψ s) (class_of (Ψ s) x3) y2
Φ s y1 x2 exact (C y1 x2 P (EquivRel_Reflexive x2)).
      +
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
x1, x2, x3: A s
C: cong_quotient subrel s 
  (class_of (Ψ s) x1) 
  (class_of (Ψ s) x2)
D: cong_quotient subrel s 
  (class_of (Ψ s) x2) 
  (class_of (Ψ s) x3)
y1, y2: A s
P: in_class (Ψ s) (class_of (Ψ s) x1) y1
Q: in_class (Ψ s) (class_of (Ψ s) x3) y2
Φ s x2 y2 exact (D x2 y2 (EquivRel_Reflexive x2) Q).
  Defined.

  Lemma for_all_relation_quotient {w : list (Sort σ)} (a b : FamilyProd A w)
    : for_all_2_family_prod (A/Ψ) (A/Ψ) (cong_quotient subrel)
        (map_family_prod (λ s, class_of (Ψ s)) a)
        (map_family_prod (λ s, class_of (Ψ s)) b) →
      for_all_2_family_prod A A Φ a b.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
w: list (Sort σ)
a, b: FamilyProd A w
for_all_2_family_prod (A / Ψ) (A / Ψ)
  (cong_quotient subrel)
  (map_family_prod (λ s : Sort σ, class_of (Ψ s)) a)
  (map_family_prod (λ s : Sort σ, class_of (Ψ s)) b) ->
for_all_2_family_prod A A Φ a b
  Proof.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
w: list (Sort σ)
a, b: FamilyProd A w
for_all_2_family_prod (A / Ψ) (A / Ψ)
  (cong_quotient subrel)
  (map_family_prod (λ s : Sort σ, class_of (Ψ s)) a)
  (map_family_prod (λ s : Sort σ, class_of (Ψ s)) b) ->
for_all_2_family_prod A A Φ a b
    intro F.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
w: list (Sort σ)
a, b: FamilyProd A w
F: for_all_2_family_prod 
  (A / Ψ) (A / Ψ) (cong_quotient subrel)
  (map_family_prod (λ s : Sort σ, class_of (Ψ s))
     a)
  (map_family_prod (λ s : Sort σ, class_of (Ψ s))
     b)
for_all_2_family_prod A A Φ a b induction w; cbn in *.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
a, b, F: Unit
Unit
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
a0: Sort σ
w: list (Sort σ)
a, b: A a0 * FamilyProd A w
F: cong_quotient subrel a0 
  (class_of (Ψ a0) (fst a))
  (class_of (Ψ a0) (fst b)) *
for_all_2_family_prod
  (carriers_quotient_algebra A Ψ)
  (carriers_quotient_algebra A Ψ)
  (cong_quotient subrel)
  (map_family_prod (λ s : Sort σ, class_of (Ψ s))
     (snd a))
  (map_family_prod (λ s : Sort σ, class_of (Ψ s))
     (snd b))
IHw: forall a b : FamilyProd A w,
for_all_2_family_prod
  (carriers_quotient_algebra A Ψ)
  (carriers_quotient_algebra A Ψ)
  (cong_quotient subrel)
  (map_family_prod
     (λ s : Sort σ, class_of (Ψ s)) a)
  (map_family_prod
     (λ s : Sort σ, class_of (Ψ s)) b) ->
for_all_2_family_prod A A Φ a b
Φ a0 (fst a) (fst b) *
for_all_2_family_prod A A Φ (snd a) (snd b)
    -
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
a, b, F: Unit
Unit constructor.
    -
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
a0: Sort σ
w: list (Sort σ)
a, b: A a0 * FamilyProd A w
F: cong_quotient subrel a0 
  (class_of (Ψ a0) (fst a))
  (class_of (Ψ a0) (fst b)) *
for_all_2_family_prod
  (carriers_quotient_algebra A Ψ)
  (carriers_quotient_algebra A Ψ)
  (cong_quotient subrel)
  (map_family_prod (λ s : Sort σ, class_of (Ψ s))
     (snd a))
  (map_family_prod (λ s : Sort σ, class_of (Ψ s))
     (snd b))
IHw: forall a b : FamilyProd A w,
for_all_2_family_prod
  (carriers_quotient_algebra A Ψ)
  (carriers_quotient_algebra A Ψ)
  (cong_quotient subrel)
  (map_family_prod
     (λ s : Sort σ, class_of (Ψ s)) a)
  (map_family_prod
     (λ s : Sort σ, class_of (Ψ s)) b) ->
for_all_2_family_prod A A Φ a b
Φ a0 (fst a) (fst b) *
for_all_2_family_prod A A Φ (snd a) (snd b) destruct a as [x a], b as [y b], F as [Q F].
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
a0: Sort σ
w: list (Sort σ)
x: A a0
a: FamilyProd A w
y: A a0
b: FamilyProd A w
Q: cong_quotient subrel a0 
  (class_of (Ψ a0) x) 
  (class_of (Ψ a0) y)
F: for_all_2_family_prod
  (carriers_quotient_algebra A Ψ)
  (carriers_quotient_algebra A Ψ)
  (cong_quotient subrel)
  (map_family_prod (λ s : Sort σ, class_of (Ψ s))
     a)
  (map_family_prod (λ s : Sort σ, class_of (Ψ s))
     b)
IHw: forall a b : FamilyProd A w,
for_all_2_family_prod
  (carriers_quotient_algebra A Ψ)
  (carriers_quotient_algebra A Ψ)
  (cong_quotient subrel)
  (map_family_prod
     (λ s : Sort σ, class_of (Ψ s)) a)
  (map_family_prod
     (λ s : Sort σ, class_of (Ψ s)) b) ->
for_all_2_family_prod A A Φ a b
Φ a0 x y * for_all_2_family_prod A A Φ a b
      split.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
a0: Sort σ
w: list (Sort σ)
x: A a0
a: FamilyProd A w
y: A a0
b: FamilyProd A w
Q: cong_quotient subrel a0 
  (class_of (Ψ a0) x) 
  (class_of (Ψ a0) y)
F: for_all_2_family_prod
  (carriers_quotient_algebra A Ψ)
  (carriers_quotient_algebra A Ψ)
  (cong_quotient subrel)
  (map_family_prod (λ s : Sort σ, class_of (Ψ s))
     a)
  (map_family_prod (λ s : Sort σ, class_of (Ψ s))
     b)
IHw: forall a b : FamilyProd A w,
for_all_2_family_prod
  (carriers_quotient_algebra A Ψ)
  (carriers_quotient_algebra A Ψ)
  (cong_quotient subrel)
  (map_family_prod
     (λ s : Sort σ, class_of (Ψ s)) a)
  (map_family_prod
     (λ s : Sort σ, class_of (Ψ s)) b) ->
for_all_2_family_prod A A Φ a b
Φ a0 x y
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
a0: Sort σ
w: list (Sort σ)
x: A a0
a: FamilyProd A w
y: A a0
b: FamilyProd A w
Q: cong_quotient subrel a0 
  (class_of (Ψ a0) x) 
  (class_of (Ψ a0) y)
F: for_all_2_family_prod
  (carriers_quotient_algebra A Ψ)
  (carriers_quotient_algebra A Ψ)
  (cong_quotient subrel)
  (map_family_prod (λ s : Sort σ, class_of (Ψ s))
     a)
  (map_family_prod (λ s : Sort σ, class_of (Ψ s))
     b)
IHw: forall a b : FamilyProd A w,
for_all_2_family_prod
  (carriers_quotient_algebra A Ψ)
  (carriers_quotient_algebra A Ψ)
  (cong_quotient subrel)
  (map_family_prod
     (λ s : Sort σ, class_of (Ψ s)) a)
  (map_family_prod
     (λ s : Sort σ, class_of (Ψ s)) b) ->
for_all_2_family_prod A A Φ a b
for_all_2_family_prod A A Φ a b
      +
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
a0: Sort σ
w: list (Sort σ)
x: A a0
a: FamilyProd A w
y: A a0
b: FamilyProd A w
Q: cong_quotient subrel a0 
  (class_of (Ψ a0) x) 
  (class_of (Ψ a0) y)
F: for_all_2_family_prod
  (carriers_quotient_algebra A Ψ)
  (carriers_quotient_algebra A Ψ)
  (cong_quotient subrel)
  (map_family_prod (λ s : Sort σ, class_of (Ψ s))
     a)
  (map_family_prod (λ s : Sort σ, class_of (Ψ s))
     b)
IHw: forall a b : FamilyProd A w,
for_all_2_family_prod
  (carriers_quotient_algebra A Ψ)
  (carriers_quotient_algebra A Ψ)
  (cong_quotient subrel)
  (map_family_prod
     (λ s : Sort σ, class_of (Ψ s)) a)
  (map_family_prod
     (λ s : Sort σ, class_of (Ψ s)) b) ->
for_all_2_family_prod A A Φ a b
Φ a0 x y apply Q; simpl; reflexivity.
      +
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
a0: Sort σ
w: list (Sort σ)
x: A a0
a: FamilyProd A w
y: A a0
b: FamilyProd A w
Q: cong_quotient subrel a0 
  (class_of (Ψ a0) x) 
  (class_of (Ψ a0) y)
F: for_all_2_family_prod
  (carriers_quotient_algebra A Ψ)
  (carriers_quotient_algebra A Ψ)
  (cong_quotient subrel)
  (map_family_prod (λ s : Sort σ, class_of (Ψ s))
     a)
  (map_family_prod (λ s : Sort σ, class_of (Ψ s))
     b)
IHw: forall a b : FamilyProd A w,
for_all_2_family_prod
  (carriers_quotient_algebra A Ψ)
  (carriers_quotient_algebra A Ψ)
  (cong_quotient subrel)
  (map_family_prod
     (λ s : Sort σ, class_of (Ψ s)) a)
  (map_family_prod
     (λ s : Sort σ, class_of (Ψ s)) b) ->
for_all_2_family_prod A A Φ a b
for_all_2_family_prod A A Φ a b by apply IHw.
  Qed.

  Global Instance ops_compatible_quotient
    : OpsCompatible (A/Ψ) (cong_quotient subrel).
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
OpsCompatible (A / Ψ) (cong_quotient subrel)
  Proof.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
OpsCompatible (A / Ψ) (cong_quotient subrel)
    intros u.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
u: Symbol σ
OpCompatible (A / Ψ) (cong_quotient subrel) u.#(A / Ψ)
    refine (quotient_ind_prop_family_prod A Ψ _ _).
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
u: Symbol σ
forall (x : FamilyProd A (dom_symboltype (σ u)))
(b : FamilyProd (A / Ψ) (dom_symboltype (σ u))),
for_all_2_family_prod (A / Ψ) (A / Ψ)
  (cong_quotient subrel)
  (map_family_prod (λ s : Sort σ, class_of (Ψ s)) x) b ->
cong_quotient subrel (cod_symboltype (σ u))
  (ap_operation u.#(A / Ψ)
     (map_family_prod (λ s : Sort σ, class_of (Ψ s)) x))
  (ap_operation u.#(A / Ψ) b) intro a.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
u: Symbol σ
a: FamilyProd A (dom_symboltype (σ u))
forall b : FamilyProd (A / Ψ) (dom_symboltype (σ u)),
for_all_2_family_prod (A / Ψ) (A / Ψ)
  (cong_quotient subrel)
  (map_family_prod (λ s : Sort σ, class_of (Ψ s)) a) b ->
cong_quotient subrel (cod_symboltype (σ u))
  (ap_operation u.#(A / Ψ)
     (map_family_prod (λ s : Sort σ, class_of (Ψ s)) a))
  (ap_operation u.#(A / Ψ) b)
    refine (quotient_ind_prop_family_prod A Ψ _ _).
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
u: Symbol σ
a: FamilyProd A (dom_symboltype (σ u))
forall x : FamilyProd A (dom_symboltype (σ u)),
for_all_2_family_prod (A / Ψ) (A / Ψ)
  (cong_quotient subrel)
  (map_family_prod (λ s : Sort σ, class_of (Ψ s)) a)
  (map_family_prod (λ s : Sort σ, class_of (Ψ s)) x) ->
cong_quotient subrel (cod_symboltype (σ u))
  (ap_operation u.#(A / Ψ)
     (map_family_prod (λ s : Sort σ, class_of (Ψ s)) a))
  (ap_operation u.#(A / Ψ)
     (map_family_prod (λ s : Sort σ, class_of (Ψ s)) x)) intro b.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
u: Symbol σ
a, b: FamilyProd A (dom_symboltype (σ u))
for_all_2_family_prod (A / Ψ) (A / Ψ)
  (cong_quotient subrel)
  (map_family_prod (λ s : Sort σ, class_of (Ψ s)) a)
  (map_family_prod (λ s : Sort σ, class_of (Ψ s)) b) ->
cong_quotient subrel (cod_symboltype (σ u))
  (ap_operation u.#(A / Ψ)
     (map_family_prod (λ s : Sort σ, class_of (Ψ s)) a))
  (ap_operation u.#(A / Ψ)
     (map_family_prod (λ s : Sort σ, class_of (Ψ s)) b))
    (* It should not be necessary to provide the explicit types: *)
    destruct (compute_op_quotient A Ψ u a
              : ap_operation (u.#(A / Ψ))
                 (map_family_prod (λ s, class_of (Ψ s)) _) = _)^.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
u: Symbol σ
a, b: FamilyProd A (dom_symboltype (σ u))
for_all_2_family_prod (A / Ψ) (A / Ψ)
  (cong_quotient subrel)
  (map_family_prod (λ s : Sort σ, class_of (Ψ s)) a)
  (map_family_prod (λ s : Sort σ, class_of (Ψ s)) b) ->
cong_quotient subrel (cod_symboltype (σ u))
  (class_of (Ψ (cod_symboltype (σ u)))
     (ap_operation u.#A a))
  (ap_operation u.#(A / Ψ)
     (map_family_prod (λ s : Sort σ, class_of (Ψ s)) b))
    destruct (compute_op_quotient A Ψ u b
              : ap_operation (u.#(A / Ψ))
                 (map_family_prod (λ s, class_of (Ψ s)) _) = _)^.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
u: Symbol σ
a, b: FamilyProd A (dom_symboltype (σ u))
for_all_2_family_prod (A / Ψ) (A / Ψ)
  (cong_quotient subrel)
  (map_family_prod (λ s : Sort σ, class_of (Ψ s)) a)
  (map_family_prod (λ s : Sort σ, class_of (Ψ s)) b) ->
cong_quotient subrel (cod_symboltype (σ u))
  (class_of (Ψ (cod_symboltype (σ u)))
     (ap_operation u.#A a))
  (class_of (Ψ (cod_symboltype (σ u)))
     (ap_operation u.#A b))
    intros R x y P Q.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
u: Symbol σ
a, b: FamilyProd A (dom_symboltype (σ u))
R: for_all_2_family_prod 
  (A / Ψ) (A / Ψ) (cong_quotient subrel)
  (map_family_prod (λ s : Sort σ, class_of (Ψ s))
     a)
  (map_family_prod (λ s : Sort σ, class_of (Ψ s))
     b)
x, y: A (cod_symboltype (σ u))
P: in_class (Ψ (cod_symboltype (σ u)))
  (class_of (Ψ (cod_symboltype (σ u)))
     (ap_operation u.#A a)) x
Q: in_class (Ψ (cod_symboltype (σ u)))
  (class_of (Ψ (cod_symboltype (σ u)))
     (ap_operation u.#A b)) y
Φ (cod_symboltype (σ u)) x y
    apply subrel in P.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
u: Symbol σ
a, b: FamilyProd A (dom_symboltype (σ u))
R: for_all_2_family_prod 
  (A / Ψ) (A / Ψ) (cong_quotient subrel)
  (map_family_prod (λ s : Sort σ, class_of (Ψ s))
     a)
  (map_family_prod (λ s : Sort σ, class_of (Ψ s))
     b)
x, y: A (cod_symboltype (σ u))
P: Φ (cod_symboltype (σ u)) (ap_operation u.#A a) x
Q: in_class (Ψ (cod_symboltype (σ u)))
  (class_of (Ψ (cod_symboltype (σ u)))
     (ap_operation u.#A b)) y
Φ (cod_symboltype (σ u)) x y
    apply subrel in Q.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
u: Symbol σ
a, b: FamilyProd A (dom_symboltype (σ u))
R: for_all_2_family_prod 
  (A / Ψ) (A / Ψ) (cong_quotient subrel)
  (map_family_prod (λ s : Sort σ, class_of (Ψ s))
     a)
  (map_family_prod (λ s : Sort σ, class_of (Ψ s))
     b)
x, y: A (cod_symboltype (σ u))
P: Φ (cod_symboltype (σ u)) (ap_operation u.#A a) x
Q: Φ (cod_symboltype (σ u)) (ap_operation u.#A b) y
Φ (cod_symboltype (σ u)) x y
    transitivity (ap_operation u.#A a).
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
u: Symbol σ
a, b: FamilyProd A (dom_symboltype (σ u))
R: for_all_2_family_prod 
  (A / Ψ) (A / Ψ) (cong_quotient subrel)
  (map_family_prod (λ s : Sort σ, class_of (Ψ s))
     a)
  (map_family_prod (λ s : Sort σ, class_of (Ψ s))
     b)
x, y: A (cod_symboltype (σ u))
P: Φ (cod_symboltype (σ u)) (ap_operation u.#A a) x
Q: Φ (cod_symboltype (σ u)) (ap_operation u.#A b) y
Φ (cod_symboltype (σ u)) x (ap_operation u.#A a)
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
u: Symbol σ
a, b: FamilyProd A (dom_symboltype (σ u))
R: for_all_2_family_prod 
  (A / Ψ) (A / Ψ) (cong_quotient subrel)
  (map_family_prod (λ s : Sort σ, class_of (Ψ s))
     a)
  (map_family_prod (λ s : Sort σ, class_of (Ψ s))
     b)
x, y: A (cod_symboltype (σ u))
P: Φ (cod_symboltype (σ u)) (ap_operation u.#A a) x
Q: Φ (cod_symboltype (σ u)) (ap_operation u.#A b) y
Φ (cod_symboltype (σ u)) (ap_operation u.#A a) y
    -
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
u: Symbol σ
a, b: FamilyProd A (dom_symboltype (σ u))
R: for_all_2_family_prod 
  (A / Ψ) (A / Ψ) (cong_quotient subrel)
  (map_family_prod (λ s : Sort σ, class_of (Ψ s))
     a)
  (map_family_prod (λ s : Sort σ, class_of (Ψ s))
     b)
x, y: A (cod_symboltype (σ u))
P: Φ (cod_symboltype (σ u)) (ap_operation u.#A a) x
Q: Φ (cod_symboltype (σ u)) (ap_operation u.#A b) y
Φ (cod_symboltype (σ u)) x (ap_operation u.#A a) by symmetry.
    -
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
u: Symbol σ
a, b: FamilyProd A (dom_symboltype (σ u))
R: for_all_2_family_prod 
  (A / Ψ) (A / Ψ) (cong_quotient subrel)
  (map_family_prod (λ s : Sort σ, class_of (Ψ s))
     a)
  (map_family_prod (λ s : Sort σ, class_of (Ψ s))
     b)
x, y: A (cod_symboltype (σ u))
P: Φ (cod_symboltype (σ u)) (ap_operation u.#A a) x
Q: Φ (cod_symboltype (σ u)) (ap_operation u.#A b) y
Φ (cod_symboltype (σ u)) (ap_operation u.#A a) y transitivity (ap_operation u.#A b); try assumption.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
u: Symbol σ
a, b: FamilyProd A (dom_symboltype (σ u))
R: for_all_2_family_prod 
  (A / Ψ) (A / Ψ) (cong_quotient subrel)
  (map_family_prod (λ s : Sort σ, class_of (Ψ s))
     a)
  (map_family_prod (λ s : Sort σ, class_of (Ψ s))
     b)
x, y: A (cod_symboltype (σ u))
P: Φ (cod_symboltype (σ u)) (ap_operation u.#A a) x
Q: Φ (cod_symboltype (σ u)) (ap_operation u.#A b) y
Φ (cod_symboltype (σ u)) (ap_operation u.#A a)
  (ap_operation u.#A b)
      apply (ops_compatible A Φ u).
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
u: Symbol σ
a, b: FamilyProd A (dom_symboltype (σ u))
R: for_all_2_family_prod 
  (A / Ψ) (A / Ψ) (cong_quotient subrel)
  (map_family_prod (λ s : Sort σ, class_of (Ψ s))
     a)
  (map_family_prod (λ s : Sort σ, class_of (Ψ s))
     b)
x, y: A (cod_symboltype (σ u))
P: Φ (cod_symboltype (σ u)) (ap_operation u.#A a) x
Q: Φ (cod_symboltype (σ u)) (ap_operation u.#A b) y
for_all_2_family_prod A A Φ a b
      by apply for_all_relation_quotient.
  Defined.

  Global Instance is_congruence_quotient
    : IsCongruence (A/Ψ) (cong_quotient subrel)
    := BuildIsCongruence (A/Ψ) (cong_quotient subrel).

End cong_quotient.

Section third_isomorphism.
  Context
    `{Univalence}
    {σ : Signature} {A : Algebra σ}
    (Φ : ∀ s, Relation (A s)) `{!IsCongruence A Φ}
    (Ψ : ∀ s, Relation (A s)) `{!IsCongruence A Ψ}
    (subrel : ∀ (s : Sort σ) (x y : A s), Ψ s x y → Φ s x y).

  Lemma third_surjecton_well_def (s : Sort σ)
    (x y : A s) (P : Ψ s x y)
    : class_of (Φ s) x = class_of (Φ s) y.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
x, y: A s
P: Ψ s x y
class_of (Φ s) x = class_of (Φ s) y
  Proof.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
x, y: A s
P: Ψ s x y
class_of (Φ s) x = class_of (Φ s) y
    apply qglue.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
x, y: A s
P: Ψ s x y
Φ s x y exact (subrel s x y P).
  Defined.

  Definition def_third_surjection (s : Sort σ) : (A/Ψ) s → (A/Φ) s
    := Quotient_rec (Ψ s) _ (class_of (Φ s)) (third_surjecton_well_def s).

  Lemma oppreserving_third_surjection {w : SymbolType σ} (f : Operation A w)
    : ∀ (α : Operation (A/Φ) w) (Qα : ComputeOpQuotient A Φ f α)
        (β : Operation (A/Ψ) w) (Qβ : ComputeOpQuotient A Ψ f β),
      OpPreserving def_third_surjection β α.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
w: SymbolType σ
f: Operation A w
forall α : Operation (A / Φ) w,
ComputeOpQuotient A Φ f α ->
forall β : Operation (A / Ψ) w,
ComputeOpQuotient A Ψ f β ->
OpPreserving def_third_surjection β α
  Proof.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
w: SymbolType σ
f: Operation A w
forall α : Operation (A / Φ) w,
ComputeOpQuotient A Φ f α ->
forall β : Operation (A / Ψ) w,
ComputeOpQuotient A Ψ f β ->
OpPreserving def_third_surjection β α
    induction w.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
t: Sort σ
f: Operation A (ne_list.one t)
forall α : Operation (A / Φ) (ne_list.one t),
ComputeOpQuotient A Φ f α ->
forall β : Operation (A / Ψ) (ne_list.one t),
ComputeOpQuotient A Ψ f β ->
OpPreserving def_third_surjection β α
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
f: Operation A (ne_list.cons t w)
IHw: forall (f : Operation A w)
(α : Operation (A / Φ) w),
ComputeOpQuotient A Φ f α ->
forall β : Operation (A / Ψ) w,
ComputeOpQuotient A Ψ f β ->
OpPreserving def_third_surjection β α
forall α : Operation (A / Φ) (ne_list.cons t w),
ComputeOpQuotient A Φ f α ->
forall β : Operation (A / Ψ) (ne_list.cons t w),
ComputeOpQuotient A Ψ f β ->
OpPreserving def_third_surjection β α
    -
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
t: Sort σ
f: Operation A (ne_list.one t)
forall α : Operation (A / Φ) (ne_list.one t),
ComputeOpQuotient A Φ f α ->
forall β : Operation (A / Ψ) (ne_list.one t),
ComputeOpQuotient A Ψ f β ->
OpPreserving def_third_surjection β α refine (Quotient_ind_hprop (Φ t) _ _).
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
t: Sort σ
f: Operation A (ne_list.one t)
forall x : A t,
ComputeOpQuotient A Φ f (class_of (Φ t) x) ->
forall β : Operation (A / Ψ) (ne_list.one t),
ComputeOpQuotient A Ψ f β ->
OpPreserving def_third_surjection β (class_of (Φ t) x) intros α Qα.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
t: Sort σ
f: Operation A (ne_list.one t)
α: A t
Qα: ComputeOpQuotient A Φ f (class_of (Φ t) α)
forall β : Operation (A / Ψ) (ne_list.one t),
ComputeOpQuotient A Ψ f β ->
OpPreserving def_third_surjection β (class_of (Φ t) α)
      refine (Quotient_ind_hprop (Ψ t) _ _).
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
t: Sort σ
f: Operation A (ne_list.one t)
α: A t
Qα: ComputeOpQuotient A Φ f (class_of (Φ t) α)
forall x : A t,
ComputeOpQuotient A Ψ f (class_of (Ψ t) x) ->
OpPreserving def_third_surjection (class_of (Ψ t) x)
  (class_of (Φ t) α) intros β Qβ.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
t: Sort σ
f: Operation A (ne_list.one t)
α: A t
Qα: ComputeOpQuotient A Φ f (class_of (Φ t) α)
β: A t
Qβ: ComputeOpQuotient A Ψ f (class_of (Ψ t) β)
OpPreserving def_third_surjection (class_of (Ψ t) β)
  (class_of (Φ t) α)
      apply qglue.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
t: Sort σ
f: Operation A (ne_list.one t)
α: A t
Qα: ComputeOpQuotient A Φ f (class_of (Φ t) α)
β: A t
Qβ: ComputeOpQuotient A Ψ f (class_of (Ψ t) β)
Φ t β α
      transitivity f.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
t: Sort σ
f: Operation A (ne_list.one t)
α: A t
Qα: ComputeOpQuotient A Φ f (class_of (Φ t) α)
β: A t
Qβ: ComputeOpQuotient A Ψ f (class_of (Ψ t) β)
Φ t β f
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
t: Sort σ
f: Operation A (ne_list.one t)
α: A t
Qα: ComputeOpQuotient A Φ f (class_of (Φ t) α)
β: A t
Qβ: ComputeOpQuotient A Ψ f (class_of (Ψ t) β)
Φ t f α
      +
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
t: Sort σ
f: Operation A (ne_list.one t)
α: A t
Qα: ComputeOpQuotient A Φ f (class_of (Φ t) α)
β: A t
Qβ: ComputeOpQuotient A Ψ f (class_of (Ψ t) β)
Φ t β f apply subrel.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
t: Sort σ
f: Operation A (ne_list.one t)
α: A t
Qα: ComputeOpQuotient A Φ f (class_of (Φ t) α)
β: A t
Qβ: ComputeOpQuotient A Ψ f (class_of (Ψ t) β)
Ψ t β f apply (related_quotient_paths (Ψ t)).
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
t: Sort σ
f: Operation A (ne_list.one t)
α: A t
Qα: ComputeOpQuotient A Φ f (class_of (Φ t) α)
β: A t
Qβ: ComputeOpQuotient A Ψ f (class_of (Ψ t) β)
class_of (Ψ t) β = class_of (Ψ t) f exact (Qβ tt).
      +
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
t: Sort σ
f: Operation A (ne_list.one t)
α: A t
Qα: ComputeOpQuotient A Φ f (class_of (Φ t) α)
β: A t
Qβ: ComputeOpQuotient A Ψ f (class_of (Ψ t) β)
Φ t f α apply (related_quotient_paths (Φ t)).
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
t: Sort σ
f: Operation A (ne_list.one t)
α: A t
Qα: ComputeOpQuotient A Φ f (class_of (Φ t) α)
β: A t
Qβ: ComputeOpQuotient A Ψ f (class_of (Ψ t) β)
class_of (Φ t) f = class_of (Φ t) α symmetry.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
t: Sort σ
f: Operation A (ne_list.one t)
α: A t
Qα: ComputeOpQuotient A Φ f (class_of (Φ t) α)
β: A t
Qβ: ComputeOpQuotient A Ψ f (class_of (Ψ t) β)
class_of (Φ t) α = class_of (Φ t) f exact (Qα tt).
    -
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
f: Operation A (ne_list.cons t w)
IHw: forall (f : Operation A w)
(α : Operation (A / Φ) w),
ComputeOpQuotient A Φ f α ->
forall β : Operation (A / Ψ) w,
ComputeOpQuotient A Ψ f β ->
OpPreserving def_third_surjection β α
forall α : Operation (A / Φ) (ne_list.cons t w),
ComputeOpQuotient A Φ f α ->
forall β : Operation (A / Ψ) (ne_list.cons t w),
ComputeOpQuotient A Ψ f β ->
OpPreserving def_third_surjection β α intros α Qα β Qβ.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
f: Operation A (ne_list.cons t w)
IHw: forall (f : Operation A w)
(α : Operation (A / Φ) w),
ComputeOpQuotient A Φ f α ->
forall β : Operation (A / Ψ) w,
ComputeOpQuotient A Ψ f β ->
OpPreserving def_third_surjection β α
α: Operation (A / Φ) (ne_list.cons t w)
Qα: ComputeOpQuotient A Φ f α
β: Operation (A / Ψ) (ne_list.cons t w)
Qβ: ComputeOpQuotient A Ψ f β
OpPreserving def_third_surjection β α
      refine (Quotient_ind_hprop (Ψ t) _ _).
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
f: Operation A (ne_list.cons t w)
IHw: forall (f : Operation A w)
(α : Operation (A / Φ) w),
ComputeOpQuotient A Φ f α ->
forall β : Operation (A / Ψ) w,
ComputeOpQuotient A Ψ f β ->
OpPreserving def_third_surjection β α
α: Operation (A / Φ) (ne_list.cons t w)
Qα: ComputeOpQuotient A Φ f α
β: Operation (A / Ψ) (ne_list.cons t w)
Qβ: ComputeOpQuotient A Ψ f β
forall x : A t,
(fix OpPreserving (w : SymbolType σ) :
     Operation (A / Ψ) w ->
     Operation (A / Φ) w -> Type :=
   match
     w as w0
     return
       (Operation (A / Ψ) w0 ->
        Operation (A / Φ) w0 -> Type)
   with
   | ne_list.one s =>
       λ (α : Operation (A / Ψ) (ne_list.one s))
       (β : Operation (A / Φ) (ne_list.one s)),
       def_third_surjection s α = β
   | ne_list.cons s y =>
       λ (α : Operation (A / Ψ) (ne_list.cons s y))
       (β : Operation (A / Φ) (ne_list.cons s y)),
       forall x0 : (A / Ψ) s,
       OpPreserving y (α x0)
         (β (def_third_surjection s x0))
   end) w (β (class_of (Ψ t) x))
  (α (def_third_surjection t (class_of (Ψ t) x)))
      intro x.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
f: Operation A (ne_list.cons t w)
IHw: forall (f : Operation A w)
(α : Operation (A / Φ) w),
ComputeOpQuotient A Φ f α ->
forall β : Operation (A / Ψ) w,
ComputeOpQuotient A Ψ f β ->
OpPreserving def_third_surjection β α
α: Operation (A / Φ) (ne_list.cons t w)
Qα: ComputeOpQuotient A Φ f α
β: Operation (A / Ψ) (ne_list.cons t w)
Qβ: ComputeOpQuotient A Ψ f β
x: A t
(fix OpPreserving (w : SymbolType σ) :
     Operation (A / Ψ) w ->
     Operation (A / Φ) w -> Type :=
   match
     w as w0
     return
       (Operation (A / Ψ) w0 ->
        Operation (A / Φ) w0 -> Type)
   with
   | ne_list.one s =>
       λ (α : Operation (A / Ψ) (ne_list.one s))
       (β : Operation (A / Φ) (ne_list.one s)),
       def_third_surjection s α = β
   | ne_list.cons s y =>
       λ (α : Operation (A / Ψ) (ne_list.cons s y))
       (β : Operation (A / Φ) (ne_list.cons s y)),
       forall x : (A / Ψ) s,
       OpPreserving y (α x)
         (β (def_third_surjection s x))
   end) w (β (class_of (Ψ t) x))
  (α (def_third_surjection t (class_of (Ψ t) x)))
      exact (IHw (f x) (α (class_of (Φ t) x)) (λ a, Qα (x,a))
               (β (class_of (Ψ t) x)) (λ a, Qβ (x,a))).
  Defined.

 Global Instance is_homomorphism_third_surjection
    : IsHomomorphism def_third_surjection.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
IsHomomorphism def_third_surjection
  Proof.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
IsHomomorphism def_third_surjection
    intro u.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
u: Symbol σ
OpPreserving def_third_surjection u.#(A / Ψ)
  u.#(A / Φ)
    eapply oppreserving_third_surjection; apply compute_op_quotient.
  Defined.

  Definition hom_third_surjection : Homomorphism (A/Ψ) (A/Φ)
    := BuildHomomorphism def_third_surjection.

  Global Instance surjection_third_surjection (s : Sort σ)
    : IsSurjection (hom_third_surjection s).
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
ReflectiveSubuniverse.IsConnMap (Tr (-1))
  (hom_third_surjection s)
  Proof.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
ReflectiveSubuniverse.IsConnMap (Tr (-1))
  (hom_third_surjection s)
    apply BuildIsSurjection.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
forall b : (A / Φ) s,
merely (hfiber (hom_third_surjection s) b)
    refine (Quotient_ind_hprop (Φ s) _ _).
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
forall x : A s,
merely
  (hfiber (hom_third_surjection s) (class_of (Φ s) x))
    intro x.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
x: A s
merely
  (hfiber (hom_third_surjection s) (class_of (Φ s) x))
    apply tr.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
x: A s
hfiber (hom_third_surjection s) (class_of (Φ s) x)
    by exists (class_of (Ψ s) x).
  Qed.

  Local Notation Θ := (cong_quotient Φ Ψ subrel).

  Lemma path_quotient_algebras_third_surjection
    : A/Ψ / cong_ker hom_third_surjection = A/Ψ / Θ.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
A / Ψ / cong_ker hom_third_surjection = A / Ψ / Θ
  Proof.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
A / Ψ / cong_ker hom_third_surjection = A / Ψ / Θ
    apply path_quotient_algebra_iff.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
forall (s : Sort σ) (x y : (A / Ψ) s),
cong_ker hom_third_surjection s x y <-> Θ s x y intros s x y.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
x, y: (A / Ψ) s
cong_ker hom_third_surjection s x y <-> Θ s x y
    split; generalize dependent y; generalize dependent x;
           refine (Quotient_ind_hprop (Ψ s) _ _); intro x;
           refine (Quotient_ind_hprop (Ψ s) _ _); intro y.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
x, y: A s
cong_ker hom_third_surjection s (class_of (Ψ s) x)
  (class_of (Ψ s) y) ->
Θ s (class_of (Ψ s) x) (class_of (Ψ s) y)
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
x, y: A s
Θ s (class_of (Ψ s) x) (class_of (Ψ s) y) ->
cong_ker hom_third_surjection s 
  (class_of (Ψ s) x) 
  (class_of (Ψ s) y)
    -
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
x, y: A s
cong_ker hom_third_surjection s (class_of (Ψ s) x)
  (class_of (Ψ s) y) ->
Θ s (class_of (Ψ s) x) (class_of (Ψ s) y) intros K x' y' Cx Cy.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
x, y: A s
K: cong_ker hom_third_surjection s 
  (class_of (Ψ s) x) 
  (class_of (Ψ s) y)
x', y': A s
Cx: in_class (Ψ s) (class_of (Ψ s) x) x'
Cy: in_class (Ψ s) (class_of (Ψ s) y) y'
Φ s x' y'
      apply subrel in Cx.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
x, y: A s
K: cong_ker hom_third_surjection s 
  (class_of (Ψ s) x) 
  (class_of (Ψ s) y)
x', y': A s
Cx: Φ s x x'
Cy: in_class (Ψ s) (class_of (Ψ s) y) y'
Φ s x' y' apply subrel in Cy.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
x, y: A s
K: cong_ker hom_third_surjection s 
  (class_of (Ψ s) x) 
  (class_of (Ψ s) y)
x', y': A s
Cx: Φ s x x'
Cy: Φ s y y'
Φ s x' y'
      apply (related_quotient_paths (Φ s)) in K.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
x, y: A s
K: Φ s x y
x', y': A s
Cx: Φ s x x'
Cy: Φ s y y'
Φ s x' y'
      transitivity x.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
x, y: A s
K: Φ s x y
x', y': A s
Cx: Φ s x x'
Cy: Φ s y y'
Φ s x' x
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
x, y: A s
K: Φ s x y
x', y': A s
Cx: Φ s x x'
Cy: Φ s y y'
Φ s x y'
      +
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
x, y: A s
K: Φ s x y
x', y': A s
Cx: Φ s x x'
Cy: Φ s y y'
Φ s x' x by symmetry.
      +
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
x, y: A s
K: Φ s x y
x', y': A s
Cx: Φ s x x'
Cy: Φ s y y'
Φ s x y' by transitivity y.
    -
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
x, y: A s
Θ s (class_of (Ψ s) x) (class_of (Ψ s) y) ->
cong_ker hom_third_surjection s (class_of (Ψ s) x)
  (class_of (Ψ s) y) intro T.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
x, y: A s
T: Θ s (class_of (Ψ s) x) (class_of (Ψ s) y)
cong_ker hom_third_surjection s (class_of (Ψ s) x)
  (class_of (Ψ s) y)
      apply qglue.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
s: Sort σ
x, y: A s
T: Θ s (class_of (Ψ s) x) (class_of (Ψ s) y)
Φ s x y
      exact (T x y (EquivRel_Reflexive x) (EquivRel_Reflexive y)).
  Defined.

  Definition hom_third_isomorphism : Homomorphism (A/Ψ/Θ) (A/Φ)
    := transport (λ X, Homomorphism X (A/Φ))
          path_quotient_algebras_third_surjection
          (hom_first_isomorphism_surjection hom_third_surjection).

  Theorem is_isomorphism_third_isomorphism
    : IsIsomorphism hom_third_isomorphism.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
IsIsomorphism hom_third_isomorphism
  Proof.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
IsIsomorphism hom_third_isomorphism
    unfold hom_third_isomorphism.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
IsIsomorphism
  (transport (λ X : Algebra σ, Homomorphism X (A / Φ))
     path_quotient_algebras_third_surjection
     (hom_first_isomorphism_surjection
        hom_third_surjection))
    destruct path_quotient_algebras_third_surjection.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
IsIsomorphism
  (transport (λ X : Algebra σ, Homomorphism X (A / Φ))
     1
     (hom_first_isomorphism_surjection
        hom_third_surjection))
    exact _.
  Qed.

  Global Existing Instance is_isomorphism_third_isomorphism.

  (** The third isomorphism theorem. *)

  Corollary isomorphic_third_isomorphism : A/Ψ/Θ ≅ A/Φ.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
A / Ψ / Θ ≅ A / Φ
  Proof.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
A / Ψ / Θ ≅ A / Φ
    exact (BuildIsomorphic hom_third_isomorphism).
  Defined.

  Corollary id_third_isomorphism : A/Ψ/Θ = A/Φ.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
A / Ψ / Θ = A / Φ
  Proof.
H: Univalence
σ: Signature
A: Algebra σ
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
Ψ: forall s : Sort σ, Relation (A s)
IsCongruence1: IsCongruence A Ψ
subrel: forall (s : Sort σ) 
(x y : A s), Ψ s x y -> Φ s x y
A / Ψ / Θ = A / Φ
    exact (id_isomorphic isomorphic_third_isomorphism).
  Defined.
End third_isomorphism.