ua_second_isomorphism.v

(** The second isomorphism theorem [isomorphic_second_isomorphism]. *)

Require Import
  Basics.Notations
  HSet
  Colimits.Quotient
  Classes.interfaces.canonical_names
  Classes.theory.ua_isomorphic
  Classes.theory.ua_subalgebra
  Classes.theory.ua_quotient_algebra.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

Import
  algebra_notations
  quotient_algebra_notations
  subalgebra_notations
  isomorphic_notations.

Local Notation i := (hom_inc_subalgebra _ _).

(** This section defines [cong_trace] and proves that it is a
    congruence, the restriction of a congruence to a subalgebra. *)

Section cong_trace.
  Context
    {σ : Signature} {A : Algebra σ}
    (P : ∀ s, A s → Type) `{!IsSubalgebraPredicate A P}
    (Φ : ∀ s, Relation (A s)) `{!IsCongruence A Φ}.

  Definition cong_trace (s : Sort σ) (x : (A&&P) s) (y : (A&&P) s)
    := Φ s (i s x) (i s y).

  #[export] Instance equiv_rel_trace_congruence (s : Sort σ)
    : EquivRel (cong_trace s).σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
s: Sort σ
EquivRel (cong_trace s)
  Proof.σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
s: Sort σ
EquivRel (cong_trace s)
    unfold cong_trace.σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
s: Sort σ
EquivRel (λ x y : (A && P) s, Φ s (i s x) (i s y))
    constructor.σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
s: Sort σ
Reflexive (λ x y : (A && P) s, Φ s (i s x) (i s y))
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
s: Sort σ
Symmetric (λ x y : (A && P) s, Φ s (i s x) (i s y))
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
s: Sort σ
Transitive (λ x y : (A && P) s, Φ s (i s x) (i s y))
    -σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
s: Sort σ
Reflexive (λ x y : (A && P) s, Φ s (i s x) (i s y)) intros [y Y].σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
s: Sort σ
y: A s
Y: P s y
Φ s (i s (y; Y)) (i s (y; Y)) reflexivity.
    -σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
s: Sort σ
Symmetric (λ x y : (A && P) s, Φ s (i s x) (i s y)) intros [y1 Y1] [y2 Y2] S.σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
s: Sort σ
y1: A s
Y1: P s y1
y2: A s
Y2: P s y2
S: Φ s (i s (y1; Y1)) (i s (y2; Y2))
Φ s (i s (y2; Y2)) (i s (y1; Y1)) by symmetry.
    -σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
s: Sort σ
Transitive (λ x y : (A && P) s, Φ s (i s x) (i s y)) intros [y1 Y1] [y2 Y2] [y3 Y3] S T.σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
s: Sort σ
y1: A s
Y1: P s y1
y2: A s
Y2: P s y2
y3: A s
Y3: P s y3
S: Φ s (i s (y1; Y1)) (i s (y2; Y2))
T: Φ s (i s (y2; Y2)) (i s (y3; Y3))
Φ s (i s (y1; Y1)) (i s (y3; Y3)) by transitivity y2.
  Qed.

  Lemma for_all_2_family_prod_trace_congruence {w : SymbolType σ}
    (a b : FamilyProd (A&&P) (dom_symboltype w))
    (R : for_all_2_family_prod (A&&P) (A&&P) cong_trace a b)
    : for_all_2_family_prod A A Φ
        (map_family_prod i a) (map_family_prod i b).σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
w: SymbolType σ
a, b: FamilyProd (A && P) (dom_symboltype w)
R: for_all_2_family_prod 
  (A && P) (A && P) cong_trace a b
for_all_2_family_prod A A Φ (map_family_prod i a)
  (map_family_prod i b)
  Proof with try assumption.σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
w: SymbolType σ
a, b: FamilyProd (A && P) (dom_symboltype w)
R: for_all_2_family_prod 
  (A && P) (A && P) cong_trace a b
for_all_2_family_prod A A Φ (map_family_prod i a)
  (map_family_prod i b)
    induction w...σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
a, b: FamilyProd (A && P)
  (dom_symboltype (ne_list.cons t w))
R: for_all_2_family_prod 
  (A && P) (A && P) cong_trace a b
IHw: forall
a b : FamilyProd (A && P) (dom_symboltype w),
for_all_2_family_prod 
  (A && P) (A && P) cong_trace a b ->
for_all_2_family_prod A A Φ
  (map_family_prod i a) 
  (map_family_prod i b)
for_all_2_family_prod A A Φ (map_family_prod i a)
  (map_family_prod i b)
    destruct a as [x a], b as [y b], R as [C R].σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
x: (A && P) t
a: Core.fold_right
  (λ (i : Sort σ) (A0 : Type), (A && P) i * A0)
  Unit (dom_symboltype w)
y: (A && P) t
b: Core.fold_right
  (λ (i : Sort σ) (A0 : Type), (A && P) i * A0)
  Unit (dom_symboltype w)
C: cong_trace t x y
R: for_all_2_family_prod 
  (A && P) (A && P) cong_trace a b
IHw: forall
a b : FamilyProd (A && P) (dom_symboltype w),
for_all_2_family_prod 
  (A && P) (A && P) cong_trace a b ->
for_all_2_family_prod A A Φ
  (map_family_prod i a) 
  (map_family_prod i b)
for_all_2_family_prod A A Φ (map_family_prod i (x, a))
  (map_family_prod i (y, b))
    split...σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
x: (A && P) t
a: Core.fold_right
  (λ (i : Sort σ) (A0 : Type), (A && P) i * A0)
  Unit (dom_symboltype w)
y: (A && P) t
b: Core.fold_right
  (λ (i : Sort σ) (A0 : Type), (A && P) i * A0)
  Unit (dom_symboltype w)
C: cong_trace t x y
R: for_all_2_family_prod 
  (A && P) (A && P) cong_trace a b
IHw: forall
a b : FamilyProd (A && P) (dom_symboltype w),
for_all_2_family_prod 
  (A && P) (A && P) cong_trace a b ->
for_all_2_family_prod A A Φ
  (map_family_prod i a) 
  (map_family_prod i b)
for_all_2_family_prod A A Φ
  (snd (map_family_prod i (x, a)))
  (snd (map_family_prod i (y, b)))
    apply IHw...
  Qed.

  #[export] Instance ops_compatible_trace_trace
    : OpsCompatible (A&&P) cong_trace.σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
OpsCompatible (A && P) cong_trace
  Proof.σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
OpsCompatible (A && P) cong_trace
    intros u a b R.σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
u: Symbol σ
a, b: FamilyProd (A && P) (dom_symboltype (σ u))
R: for_all_2_family_prod 
  (A && P) (A && P) cong_trace a b
cong_trace (cod_symboltype (σ u))
  (ap_operation u.#(A && P) a)
  (ap_operation u.#(A && P) b)
    refine (transport (λ X, Φ _ X _)
              (path_homomorphism_ap_operation i u a)^ _).σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
u: Symbol σ
a, b: FamilyProd (A && P) (dom_symboltype (σ u))
R: for_all_2_family_prod 
  (A && P) (A && P) cong_trace a b
Φ (cod_symboltype (σ u))
  (ap_operation u.#A (map_family_prod i a))
  (i (cod_symboltype (σ u))
     (ap_operation u.#(A && P) b))
    refine (transport (λ X, Φ _ _ X)
              (path_homomorphism_ap_operation i u b)^ _).σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
u: Symbol σ
a, b: FamilyProd (A && P) (dom_symboltype (σ u))
R: for_all_2_family_prod 
  (A && P) (A && P) cong_trace a b
Φ (cod_symboltype (σ u))
  (ap_operation u.#A (map_family_prod i a))
  (ap_operation u.#A (map_family_prod i b))
    apply (ops_compatible_cong A Φ).σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
u: Symbol σ
a, b: FamilyProd (A && P) (dom_symboltype (σ u))
R: for_all_2_family_prod 
  (A && P) (A && P) cong_trace a b
for_all_2_family_prod A A Φ (map_family_prod i a)
  (map_family_prod i b)
    exact (for_all_2_family_prod_trace_congruence a b R).
  Qed.

  #[export] Instance is_congruence_trace : IsCongruence (A&&P) cong_trace.σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
IsCongruence (A && P) cong_trace
  Proof.σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
IsCongruence (A && P) cong_trace
    apply (@BuildIsCongruence _ (A&&P) cong_trace);
      [intros; apply (is_mere_relation_cong A Φ) | exact _ ..].
  Qed.
End cong_trace.

(** The following section defines the [is_subalgebra_class] subalgebra
    predicate, which induces a subalgebra of [A/Φ]. *)

Section is_subalgebra_class.
  Context `{Univalence}
    {σ : Signature} {A : Algebra σ}
    (P : ∀ s, A s → Type) `{!IsSubalgebraPredicate A P}
    (Φ : ∀ s, Relation (A s)) `{!IsCongruence A Φ}.

  Definition is_subalgebra_class (s : Sort σ) (x : (A/Φ) s) : HProp
    := hexists (λ (y : (A&&P) s), in_class (Φ s) x (i s y)).

  Lemma op_closed_subalgebra_is_subalgebra_class {w : SymbolType σ}
    (γ : Operation (A/Φ) w)
    (α : Operation A w)
    (Q : ComputeOpQuotient A Φ α γ)
    (C : ClosedUnderOp A P α)
    : ClosedUnderOp (A/Φ) is_subalgebra_class γ.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
w: SymbolType σ
γ: Operation (A / Φ) w
α: Operation A w
Q: ComputeOpQuotient A Φ α γ
C: ClosedUnderOp A P α
ClosedUnderOp (A / Φ)
  (λ (s : Sort σ) (x : (A / Φ) s),
   is_subalgebra_class s x) γ
  Proof.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
w: SymbolType σ
γ: Operation (A / Φ) w
α: Operation A w
Q: ComputeOpQuotient A Φ α γ
C: ClosedUnderOp A P α
ClosedUnderOp (A / Φ)
  (λ (s : Sort σ) (x : (A / Φ) s),
   is_subalgebra_class s x) γ
    induction w.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
t: Sort σ
γ: Operation (A / Φ) (ne_list.one t)
α: Operation A (ne_list.one t)
Q: ComputeOpQuotient A Φ α γ
C: ClosedUnderOp A P α
ClosedUnderOp (A / Φ)
  (λ (s : Sort σ) (x : (A / Φ) s),
   is_subalgebra_class s x) γ
H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
γ: Operation (A / Φ) (ne_list.cons t w)
α: Operation A (ne_list.cons t w)
Q: ComputeOpQuotient A Φ α γ
C: ClosedUnderOp A P α
IHw: forall (γ : Operation (A / Φ) w)
(α : Operation A w),
ComputeOpQuotient A Φ α γ ->
ClosedUnderOp A P α ->
ClosedUnderOp (A / Φ)
  (λ (s : Sort σ) 
   (x : (A / Φ) s), 
   is_subalgebra_class s x) γ
ClosedUnderOp (A / Φ)
  (λ (s : Sort σ) 
   (x : (A / Φ) s), 
   is_subalgebra_class s x) γ
    -H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
t: Sort σ
γ: Operation (A / Φ) (ne_list.one t)
α: Operation A (ne_list.one t)
Q: ComputeOpQuotient A Φ α γ
C: ClosedUnderOp A P α
ClosedUnderOp (A / Φ)
  (λ (s : Sort σ) (x : (A / Φ) s),
   is_subalgebra_class s x) γ specialize (Q tt).H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
t: Sort σ
γ: Operation (A / Φ) (ne_list.one t)
α: Operation A (ne_list.one t)
Q: ap_operation γ
  (map_family_prod 
     (λ s : Sort σ, class_of (Φ s)) tt) =
class_of (Φ (cod_symboltype (ne_list.one t)))
  (ap_operation α tt)
C: ClosedUnderOp A P α
ClosedUnderOp (A / Φ)
  (λ (s : Sort σ) (x : (A / Φ) s),
   is_subalgebra_class s x) γ apply tr.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
t: Sort σ
γ: Operation (A / Φ) (ne_list.one t)
α: Operation A (ne_list.one t)
Q: ap_operation γ
  (map_family_prod 
     (λ s : Sort σ, class_of (Φ s)) tt) =
class_of (Φ (cod_symboltype (ne_list.one t)))
  (ap_operation α tt)
C: ClosedUnderOp A P α
{y : (A && P) t & in_class (Φ t) γ (i t y)}
      exists (α; C).H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
t: Sort σ
γ: Operation (A / Φ) (ne_list.one t)
α: Operation A (ne_list.one t)
Q: ap_operation γ
  (map_family_prod 
     (λ s : Sort σ, class_of (Φ s)) tt) =
class_of (Φ (cod_symboltype (ne_list.one t)))
  (ap_operation α tt)
C: ClosedUnderOp A P α
in_class (Φ t) γ (i t (α; C))
      cbn in Q.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
t: Sort σ
γ: Operation (A / Φ) (ne_list.one t)
α: Operation A (ne_list.one t)
Q: γ = class_of (Φ t) α
C: ClosedUnderOp A P α
in_class (Φ t) γ (i t (α; C)) destruct Q^.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
t: Sort σ
α: Operation A (ne_list.one t)
Q: class_of (Φ t) α = class_of (Φ t) α
C: ClosedUnderOp A P α
in_class (Φ t) (class_of (Φ t) α) (i t (α; C))
      exact (EquivRel_Reflexive α).
    -H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
γ: Operation (A / Φ) (ne_list.cons t w)
α: Operation A (ne_list.cons t w)
Q: ComputeOpQuotient A Φ α γ
C: ClosedUnderOp A P α
IHw: forall (γ : Operation (A / Φ) w)
(α : Operation A w),
ComputeOpQuotient A Φ α γ ->
ClosedUnderOp A P α ->
ClosedUnderOp (A / Φ)
  (λ (s : Sort σ) 
   (x : (A / Φ) s), 
   is_subalgebra_class s x) γ
ClosedUnderOp (A / Φ)
  (λ (s : Sort σ) (x : (A / Φ) s),
   is_subalgebra_class s x) γ refine (Quotient_ind_hprop (Φ t) _ _).H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
γ: Operation (A / Φ) (ne_list.cons t w)
α: Operation A (ne_list.cons t w)
Q: ComputeOpQuotient A Φ α γ
C: ClosedUnderOp A P α
IHw: forall (γ : Operation (A / Φ) w)
(α : Operation A w),
ComputeOpQuotient A Φ α γ ->
ClosedUnderOp A P α ->
ClosedUnderOp (A / Φ)
  (λ (s : Sort σ) 
   (x : (A / Φ) s), 
   is_subalgebra_class s x) γ
forall a : A t,
is_subalgebra_class t (class_of (Φ t) a) ->
(fix ClosedUnderOp (w : SymbolType σ) :
     Operation (A / Φ) w -> Type :=
   match
     w as w0 return (Operation (A / Φ) w0 -> Type)
   with
   | ne_list.one s =>
       λ x : (A / Φ) s, is_subalgebra_class s x
   | ne_list.cons s w' =>
       λ α : (A / Φ) s -> Operation (A / Φ) w',
       forall x : (A / Φ) s,
       is_subalgebra_class s x ->
       ClosedUnderOp w' (α x)
   end) w (γ (class_of (Φ t) a)) intro x.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
γ: Operation (A / Φ) (ne_list.cons t w)
α: Operation A (ne_list.cons t w)
Q: ComputeOpQuotient A Φ α γ
C: ClosedUnderOp A P α
IHw: forall (γ : Operation (A / Φ) w)
(α : Operation A w),
ComputeOpQuotient A Φ α γ ->
ClosedUnderOp A P α ->
ClosedUnderOp (A / Φ)
  (λ (s : Sort σ) 
   (x : (A / Φ) s), 
   is_subalgebra_class s x) γ
x: A t
is_subalgebra_class t (class_of (Φ t) x) ->
(fix ClosedUnderOp (w : SymbolType σ) :
     Operation (A / Φ) w -> Type :=
   match
     w as w0 return (Operation (A / Φ) w0 -> Type)
   with
   | ne_list.one s =>
       λ x : (A / Φ) s, is_subalgebra_class s x
   | ne_list.cons s w' =>
       λ α : (A / Φ) s -> Operation (A / Φ) w',
       forall x : (A / Φ) s,
       is_subalgebra_class s x ->
       ClosedUnderOp w' (α x)
   end) w (γ (class_of (Φ t) x))
      refine (Trunc_rec _).H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
γ: Operation (A / Φ) (ne_list.cons t w)
α: Operation A (ne_list.cons t w)
Q: ComputeOpQuotient A Φ α γ
C: ClosedUnderOp A P α
IHw: forall (γ : Operation (A / Φ) w)
(α : Operation A w),
ComputeOpQuotient A Φ α γ ->
ClosedUnderOp A P α ->
ClosedUnderOp (A / Φ)
  (λ (s : Sort σ) 
   (x : (A / Φ) s), 
   is_subalgebra_class s x) γ
x: A t
{y : (A && P) t &
in_class (Φ t) (class_of (Φ t) x) (i t y)} ->
(fix ClosedUnderOp (w : SymbolType σ) :
     Operation (A / Φ) w -> Type :=
   match
     w as w0 return (Operation (A / Φ) w0 -> Type)
   with
   | ne_list.one s =>
       λ x : (A / Φ) s, is_subalgebra_class s x
   | ne_list.cons s w' =>
       λ α : (A / Φ) s -> Operation (A / Φ) w',
       forall x : (A / Φ) s,
       is_subalgebra_class s x ->
       ClosedUnderOp w' (α x)
   end) w (γ (class_of (Φ t) x))
      intros [y R].H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
γ: Operation (A / Φ) (ne_list.cons t w)
α: Operation A (ne_list.cons t w)
Q: ComputeOpQuotient A Φ α γ
C: ClosedUnderOp A P α
IHw: forall (γ : Operation (A / Φ) w)
(α : Operation A w),
ComputeOpQuotient A Φ α γ ->
ClosedUnderOp A P α ->
ClosedUnderOp (A / Φ)
  (λ (s : Sort σ) 
   (x : (A / Φ) s), 
   is_subalgebra_class s x) γ
x: A t
y: (A && P) t
R: in_class (Φ t) (class_of (Φ t) x) (i t y)
(fix ClosedUnderOp (w : SymbolType σ) :
     Operation (A / Φ) w -> Type :=
   match
     w as w0 return (Operation (A / Φ) w0 -> Type)
   with
   | ne_list.one s =>
       λ x : (A / Φ) s, is_subalgebra_class s x
   | ne_list.cons s w' =>
       λ α : (A / Φ) s -> Operation (A / Φ) w',
       forall x : (A / Φ) s,
       is_subalgebra_class s x ->
       ClosedUnderOp w' (α x)
   end) w (γ (class_of (Φ t) x))
      apply (IHw (γ (class_of (Φ t) x)) (α (i t y))).H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
γ: Operation (A / Φ) (ne_list.cons t w)
α: Operation A (ne_list.cons t w)
Q: ComputeOpQuotient A Φ α γ
C: ClosedUnderOp A P α
IHw: forall (γ : Operation (A / Φ) w)
(α : Operation A w),
ComputeOpQuotient A Φ α γ ->
ClosedUnderOp A P α ->
ClosedUnderOp (A / Φ)
  (λ (s : Sort σ) 
   (x : (A / Φ) s), 
   is_subalgebra_class s x) γ
x: A t
y: (A && P) t
R: in_class (Φ t) (class_of (Φ t) x) (i t y)
ComputeOpQuotient A Φ (α (i t y))
  (γ (class_of (Φ t) x))
H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
γ: Operation (A / Φ) (ne_list.cons t w)
α: Operation A (ne_list.cons t w)
Q: ComputeOpQuotient A Φ α γ
C: ClosedUnderOp A P α
IHw: forall (γ : Operation (A / Φ) w)
(α : Operation A w),
ComputeOpQuotient A Φ α γ ->
ClosedUnderOp A P α ->
ClosedUnderOp (A / Φ)
  (λ (s : Sort σ) 
   (x : (A / Φ) s), 
   is_subalgebra_class s x) γ
x: A t
y: (A && P) t
R: in_class (Φ t) (class_of (Φ t) x) (i t y)
ClosedUnderOp A P (α (i t y))
      +H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
γ: Operation (A / Φ) (ne_list.cons t w)
α: Operation A (ne_list.cons t w)
Q: ComputeOpQuotient A Φ α γ
C: ClosedUnderOp A P α
IHw: forall (γ : Operation (A / Φ) w)
(α : Operation A w),
ComputeOpQuotient A Φ α γ ->
ClosedUnderOp A P α ->
ClosedUnderOp (A / Φ)
  (λ (s : Sort σ) 
   (x : (A / Φ) s), 
   is_subalgebra_class s x) γ
x: A t
y: (A && P) t
R: in_class (Φ t) (class_of (Φ t) x) (i t y)
ComputeOpQuotient A Φ (α (i t y))
  (γ (class_of (Φ t) x)) intro a.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
γ: Operation (A / Φ) (ne_list.cons t w)
α: Operation A (ne_list.cons t w)
Q: ComputeOpQuotient A Φ α γ
C: ClosedUnderOp A P α
IHw: forall (γ : Operation (A / Φ) w)
(α : Operation A w),
ComputeOpQuotient A Φ α γ ->
ClosedUnderOp A P α ->
ClosedUnderOp (A / Φ)
  (λ (s : Sort σ) 
   (x : (A / Φ) s), 
   is_subalgebra_class s x) γ
x: A t
y: (A && P) t
R: in_class (Φ t) (class_of (Φ t) x) (i t y)
a: FamilyProd A (dom_symboltype w)
ap_operation (γ (class_of (Φ t) x))
  (map_family_prod (λ s : Sort σ, class_of (Φ s)) a) =
class_of (Φ (cod_symboltype w))
  (ap_operation (α (i t y)) a)
        destruct (qglue R)^.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
γ: Operation (A / Φ) (ne_list.cons t w)
α: Operation A (ne_list.cons t w)
Q: ComputeOpQuotient A Φ α γ
C: ClosedUnderOp A P α
IHw: forall (γ : Operation (A / Φ) w)
(α : Operation A w),
ComputeOpQuotient A Φ α γ ->
ClosedUnderOp A P α ->
ClosedUnderOp (A / Φ)
  (λ (s : Sort σ) 
   (x : (A / Φ) s), 
   is_subalgebra_class s x) γ
x: A t
y: (A && P) t
R: in_class (Φ t) (class_of (Φ t) (i t y)) (i t y)
a: FamilyProd A (dom_symboltype w)
ap_operation (γ (class_of (Φ t) (i t y)))
  (map_family_prod (λ s : Sort σ, class_of (Φ s)) a) =
class_of (Φ (cod_symboltype w))
  (ap_operation (α (i t y)) a)
        apply (Q (i t y,a)).
      +H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
γ: Operation (A / Φ) (ne_list.cons t w)
α: Operation A (ne_list.cons t w)
Q: ComputeOpQuotient A Φ α γ
C: ClosedUnderOp A P α
IHw: forall (γ : Operation (A / Φ) w)
(α : Operation A w),
ComputeOpQuotient A Φ α γ ->
ClosedUnderOp A P α ->
ClosedUnderOp (A / Φ)
  (λ (s : Sort σ) 
   (x : (A / Φ) s), 
   is_subalgebra_class s x) γ
x: A t
y: (A && P) t
R: in_class (Φ t) (class_of (Φ t) x) (i t y)
ClosedUnderOp A P (α (i t y)) apply C.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
γ: Operation (A / Φ) (ne_list.cons t w)
α: Operation A (ne_list.cons t w)
Q: ComputeOpQuotient A Φ α γ
C: ClosedUnderOp A P α
IHw: forall (γ : Operation (A / Φ) w)
(α : Operation A w),
ComputeOpQuotient A Φ α γ ->
ClosedUnderOp A P α ->
ClosedUnderOp (A / Φ)
  (λ (s : Sort σ) 
   (x : (A / Φ) s), 
   is_subalgebra_class s x) γ
x: A t
y: (A && P) t
R: in_class (Φ t) (class_of (Φ t) x) (i t y)
P t (i t y) exact y.2.
  Qed.

  Definition is_closed_under_ops_is_subalgebra_class
    : IsClosedUnderOps (A/Φ) is_subalgebra_class.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
IsClosedUnderOps (A / Φ)
  (λ (s : Sort σ) (x : (A / Φ) s),
   is_subalgebra_class s x)
  Proof.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
IsClosedUnderOps (A / Φ)
  (λ (s : Sort σ) (x : (A / Φ) s),
   is_subalgebra_class s x)
    intro u.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
u: Symbol σ
ClosedUnderOp (A / Φ)
  (λ (s : Sort σ) (x : (A / Φ) s),
   is_subalgebra_class s x) u.#(A / Φ)
    eapply op_closed_subalgebra_is_subalgebra_class.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
u: Symbol σ
ComputeOpQuotient A Φ ?α u.#(A / Φ)
H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
u: Symbol σ
ClosedUnderOp A P ?α
    -H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
u: Symbol σ
ComputeOpQuotient A Φ ?α u.#(A / Φ) apply compute_op_quotient.
    -H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
u: Symbol σ
ClosedUnderOp A P u.#A apply is_closed_under_ops_subalgebra_predicate.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
u: Symbol σ
IsSubalgebraPredicate A P exact _.
  Qed.

  #[export] Instance is_subalgebra_predicate_is_subalgebra_class
    : IsSubalgebraPredicate (A/Φ) is_subalgebra_class.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
IsSubalgebraPredicate (A / Φ)
  (λ (s : Sort σ) (x : (A / Φ) s),
   is_subalgebra_class s x)
  Proof.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
IsSubalgebraPredicate (A / Φ)
  (λ (s : Sort σ) (x : (A / Φ) s),
   is_subalgebra_class s x)
    apply BuildIsSubalgebraPredicate.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
IsClosedUnderOps (A / Φ)
  (λ (s : Sort σ) (x : (A / Φ) s),
   is_subalgebra_class s x)
    apply is_closed_under_ops_is_subalgebra_class.
  Qed.
End is_subalgebra_class.

(** The next section proves the second isomorphism theorem,

<<
      (A&&P) / (cong_trace P Φ) ≅ (A/Φ) && (is_subalgebra_class P Φ).
>>
*)

(* There is an alternative proof using the first isomorphism theorem,
   but the direct proof below seems simpler in HoTT. *)

Section second_isomorphism.
  Context `{Univalence}
    {σ : Signature} (A : Algebra σ)
    (P : ∀ s, A s → Type) `{!IsSubalgebraPredicate A P}
    (Φ : ∀ s, Relation (A s)) `{!IsCongruence A Φ}.

  Local Notation Ψ := (cong_trace P Φ).

  Local Notation Q := (is_subalgebra_class P Φ).

  Definition def_second_isomorphism (s : Sort σ)
    : ((A&&P) / Ψ) s → ((A/Φ) && Q) s
    := Quotient_rec (Ψ s) _ 
        (λ (x : (A&&P) s),
         (class_of (Φ s) (i s x); tr (x; EquivRel_Reflexive x)))
        (λ (x y : (A&&P) s) (T : Ψ s x y),
         path_sigma_hprop (class_of (Φ s) (i s x); _)
           (class_of (Φ s) (i s y); _) (@qglue _ (Φ s) _ _ T)).

  Lemma oppreserving_second_isomorphism {w : SymbolType σ}
    (α : Operation A w) (γ : Operation (A/Φ) w)
    (ζ : Operation ((A&&P) / Ψ) w) (CA : ClosedUnderOp (A/Φ) Q γ)
    (CB : ClosedUnderOp A P α) (QA : ComputeOpQuotient A Φ α γ)
    (QB : ComputeOpQuotient (A&&P) Ψ (op_subalgebra A P α CB) ζ)
    : OpPreserving def_second_isomorphism ζ (op_subalgebra (A/Φ) Q γ CA).H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
w: SymbolType σ
α: Operation A w
γ: Operation (A / Φ) w
ζ: Operation ((A && P) / Ψ) w
CA: ClosedUnderOp (A / Φ)
  (λ (s : Sort σ) (x : (A / Φ) s), Q s x) γ
CB: ClosedUnderOp A P α
QA: ComputeOpQuotient A Φ α γ
QB: ComputeOpQuotient 
  (A && P) Ψ (op_subalgebra A P α CB) ζ
OpPreserving def_second_isomorphism ζ
  (op_subalgebra (A / Φ)
     (λ (s : Sort σ) (x : (A / Φ) s), Q s x) γ CA)
  Proof.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
w: SymbolType σ
α: Operation A w
γ: Operation (A / Φ) w
ζ: Operation ((A && P) / Ψ) w
CA: ClosedUnderOp (A / Φ)
  (λ (s : Sort σ) (x : (A / Φ) s), Q s x) γ
CB: ClosedUnderOp A P α
QA: ComputeOpQuotient A Φ α γ
QB: ComputeOpQuotient 
  (A && P) Ψ (op_subalgebra A P α CB) ζ
OpPreserving def_second_isomorphism ζ
  (op_subalgebra (A / Φ)
     (λ (s : Sort σ) (x : (A / Φ) s), Q s x) γ CA)
    unfold ComputeOpQuotient in *.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
w: SymbolType σ
α: Operation A w
γ: Operation (A / Φ) w
ζ: Operation ((A && P) / Ψ) w
CA: ClosedUnderOp (A / Φ)
  (λ (s : Sort σ) (x : (A / Φ) s), Q s x) γ
CB: ClosedUnderOp A P α
QA: forall a : FamilyProd A (dom_symboltype w),
ap_operation γ
  (map_family_prod 
     (λ s : Sort σ, class_of (Φ s)) a) =
class_of (Φ (cod_symboltype w))
  (ap_operation α a)
QB: forall
a : FamilyProd (A && P) (dom_symboltype w),
ap_operation ζ
  (map_family_prod 
     (λ s : Sort σ, class_of (Ψ s)) a) =
class_of (Ψ (cod_symboltype w))
  (ap_operation (op_subalgebra A P α CB) a)
OpPreserving def_second_isomorphism ζ
  (op_subalgebra (A / Φ)
     (λ (s : Sort σ) (x : (A / Φ) s), Q s x) γ CA)
    induction w; cbn in *.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
t: Sort σ
α: A t
γ: carriers_quotient_algebra A Φ t
ζ: carriers_quotient_algebra (A && P) Ψ t
CA: Trunc (-1)
  {y : carriers_subalgebra A P t &
  in_class (Φ t) γ (def_inc_subalgebra A P t y)}
CB: P t α
QA: Unit -> γ = class_of (Φ t) α
QB: Unit -> ζ = class_of (Ψ t) (α; CB)
def_second_isomorphism t ζ = (γ; CA)
H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
α: A t -> Operation A w
γ: carriers_quotient_algebra A Φ t ->
Operation (carriers_quotient_algebra A Φ) w
ζ: carriers_quotient_algebra (A && P) Ψ t ->
Operation (carriers_quotient_algebra (A && P) Ψ) w
CA: forall x : carriers_quotient_algebra A Φ t,
Trunc (-1)
  {y : carriers_subalgebra A P t &
  in_class (Φ t) x (def_inc_subalgebra A P t y)} ->
ClosedUnderOp (A / Φ)
  (λ (s : Sort σ)
   (x0 : carriers_quotient_algebra A Φ s),
   Trunc (-1)
     {y : carriers_subalgebra A P s &
     in_class (Φ s) x0
       (def_inc_subalgebra A P s y)}) 
  (γ x)
CB: forall x : A t, P t x -> ClosedUnderOp A P (α x)
QA: forall a : A t * FamilyProd A (dom_symboltype w),
ap_operation (γ (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))
QB: forall
a : carriers_subalgebra A P t *
    FamilyProd (carriers_subalgebra A P)
      (dom_symboltype w),
ap_operation (ζ (class_of (Ψ t) (fst a)))
  (map_family_prod 
     (λ s : Sort σ, class_of (Ψ s)) 
     (snd a)) =
class_of (Ψ (cod_symboltype w))
  (ap_operation
     (op_subalgebra A P 
        (α (fst a).1) 
        (CB (fst a).1 (fst a).2)) 
     (snd a))
IHw: forall (α : Operation A w)
(γ : Operation (carriers_quotient_algebra A Φ) w)
(ζ : Operation
       (carriers_quotient_algebra (A && P) Ψ) w)
(CA : ClosedUnderOp 
        (A / Φ)
        (λ (s : Sort σ)
         (x : carriers_quotient_algebra A Φ s),
         Trunc (-1)
           {y : 
           carriers_subalgebra A P s &
           in_class 
             (Φ s) x
             (def_inc_subalgebra A P s y)}) γ)
(CB : ClosedUnderOp A P α),
(forall a : FamilyProd A (dom_symboltype w),
 ap_operation γ
   (map_family_prod
      (λ s : Sort σ, class_of (Φ s)) a) =
 class_of (Φ (cod_symboltype w))
   (ap_operation α a)) ->
(forall
 a : FamilyProd 
       (carriers_subalgebra A P)
       (dom_symboltype w),
 ap_operation ζ
   (map_family_prod
      (λ s : Sort σ, class_of (Ψ s)) a) =
 class_of (Ψ (cod_symboltype w))
   (ap_operation (op_subalgebra A P α CB) a)) ->
OpPreserving def_second_isomorphism ζ
  (op_subalgebra 
     (A / Φ)
     (λ (s : Sort σ)
      (x : carriers_quotient_algebra A Φ s),
      Trunc (-1)
        {y : carriers_subalgebra A P s &
        in_class 
          (Φ s) x 
          (def_inc_subalgebra A P s y)}) γ CA)
forall x : carriers_quotient_algebra (A && P) Ψ t,
OpPreserving def_second_isomorphism 
  (ζ x)
  (op_subalgebra 
     (A / Φ)
     (λ (s : Sort σ)
      (x0 : carriers_quotient_algebra A Φ s),
      Trunc (-1)
        {y : carriers_subalgebra A P s &
        in_class (Φ s) x0 (def_inc_subalgebra A P s y)})
     (γ (def_second_isomorphism t x).1)
     (CA (def_second_isomorphism t x).1
        (def_second_isomorphism t x).2))
    -H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
t: Sort σ
α: A t
γ: carriers_quotient_algebra A Φ t
ζ: carriers_quotient_algebra (A && P) Ψ t
CA: Trunc (-1)
  {y : carriers_subalgebra A P t &
  in_class (Φ t) γ (def_inc_subalgebra A P t y)}
CB: P t α
QA: Unit -> γ = class_of (Φ t) α
QB: Unit -> ζ = class_of (Ψ t) (α; CB)
def_second_isomorphism t ζ = (γ; CA) apply path_sigma_hprop.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
t: Sort σ
α: A t
γ: carriers_quotient_algebra A Φ t
ζ: carriers_quotient_algebra (A && P) Ψ t
CA: Trunc (-1)
  {y : carriers_subalgebra A P t &
  in_class (Φ t) γ (def_inc_subalgebra A P t y)}
CB: P t α
QA: Unit -> γ = class_of (Φ t) α
QB: Unit -> ζ = class_of (Ψ t) (α; CB)
(def_second_isomorphism t ζ).1 = (γ; CA).1
      cbn.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
t: Sort σ
α: A t
γ: carriers_quotient_algebra A Φ t
ζ: carriers_quotient_algebra (A && P) Ψ t
CA: Trunc (-1)
  {y : carriers_subalgebra A P t &
  in_class (Φ t) γ (def_inc_subalgebra A P t y)}
CB: P t α
QA: Unit -> γ = class_of (Φ t) α
QB: Unit -> ζ = class_of (Ψ t) (α; CB)
(def_second_isomorphism t ζ).1 = γ destruct (QB tt)^, (QA tt)^.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
t: Sort σ
α: A t
CA: Trunc (-1)
  {y : carriers_subalgebra A P t &
  in_class (Φ t) 
    (class_of (Φ t) α)
    (def_inc_subalgebra A P t y)}
CB: P t α
QA: Unit -> class_of (Φ t) α = class_of (Φ t) α
QB: Unit ->
class_of (Ψ t) (α; CB) = class_of (Ψ t) (α; CB)
(def_second_isomorphism t (class_of (Ψ t) (α; CB))).1 =
class_of (Φ t) α
      by apply qglue.
    -H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
α: A t -> Operation A w
γ: carriers_quotient_algebra A Φ t ->
Operation (carriers_quotient_algebra A Φ) w
ζ: carriers_quotient_algebra (A && P) Ψ t ->
Operation (carriers_quotient_algebra (A && P) Ψ) w
CA: forall x : carriers_quotient_algebra A Φ t,
Trunc (-1)
  {y : carriers_subalgebra A P t &
  in_class (Φ t) x (def_inc_subalgebra A P t y)} ->
ClosedUnderOp (A / Φ)
  (λ (s : Sort σ)
   (x0 : carriers_quotient_algebra A Φ s),
   Trunc (-1)
     {y : carriers_subalgebra A P s &
     in_class (Φ s) x0
       (def_inc_subalgebra A P s y)}) 
  (γ x)
CB: forall x : A t, P t x -> ClosedUnderOp A P (α x)
QA: forall a : A t * FamilyProd A (dom_symboltype w),
ap_operation (γ (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))
QB: forall
a : carriers_subalgebra A P t *
    FamilyProd (carriers_subalgebra A P)
      (dom_symboltype w),
ap_operation (ζ (class_of (Ψ t) (fst a)))
  (map_family_prod 
     (λ s : Sort σ, class_of (Ψ s)) 
     (snd a)) =
class_of (Ψ (cod_symboltype w))
  (ap_operation
     (op_subalgebra A P 
        (α (fst a).1) 
        (CB (fst a).1 (fst a).2)) 
     (snd a))
IHw: forall (α : Operation A w)
(γ : Operation (carriers_quotient_algebra A Φ) w)
(ζ : Operation
       (carriers_quotient_algebra (A && P) Ψ) w)
(CA : ClosedUnderOp 
        (A / Φ)
        (λ (s : Sort σ)
         (x : carriers_quotient_algebra A Φ s),
         Trunc (-1)
           {y : 
           carriers_subalgebra A P s &
           in_class 
             (Φ s) x
             (def_inc_subalgebra A P s y)}) γ)
(CB : ClosedUnderOp A P α),
(forall a : FamilyProd A (dom_symboltype w),
 ap_operation γ
   (map_family_prod
      (λ s : Sort σ, class_of (Φ s)) a) =
 class_of (Φ (cod_symboltype w))
   (ap_operation α a)) ->
(forall
 a : FamilyProd 
       (carriers_subalgebra A P)
       (dom_symboltype w),
 ap_operation ζ
   (map_family_prod
      (λ s : Sort σ, class_of (Ψ s)) a) =
 class_of (Ψ (cod_symboltype w))
   (ap_operation (op_subalgebra A P α CB) a)) ->
OpPreserving def_second_isomorphism ζ
  (op_subalgebra 
     (A / Φ)
     (λ (s : Sort σ)
      (x : carriers_quotient_algebra A Φ s),
      Trunc (-1)
        {y : carriers_subalgebra A P s &
        in_class 
          (Φ s) x 
          (def_inc_subalgebra A P s y)}) γ CA)
forall x : carriers_quotient_algebra (A && P) Ψ t,
OpPreserving def_second_isomorphism (ζ x)
  (op_subalgebra (A / Φ)
     (λ (s : Sort σ)
      (x0 : carriers_quotient_algebra A Φ s),
      Trunc (-1)
        {y : carriers_subalgebra A P s &
        in_class (Φ s) x0 (def_inc_subalgebra A P s y)})
     (γ (def_second_isomorphism t x).1)
     (CA (def_second_isomorphism t x).1
        (def_second_isomorphism t x).2)) refine (Quotient_ind_hprop (Ψ t) _ _).H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
α: A t -> Operation A w
γ: carriers_quotient_algebra A Φ t ->
Operation (carriers_quotient_algebra A Φ) w
ζ: carriers_quotient_algebra (A && P) Ψ t ->
Operation (carriers_quotient_algebra (A && P) Ψ) w
CA: forall x : carriers_quotient_algebra A Φ t,
Trunc (-1)
  {y : carriers_subalgebra A P t &
  in_class (Φ t) x (def_inc_subalgebra A P t y)} ->
ClosedUnderOp (A / Φ)
  (λ (s : Sort σ)
   (x0 : carriers_quotient_algebra A Φ s),
   Trunc (-1)
     {y : carriers_subalgebra A P s &
     in_class (Φ s) x0
       (def_inc_subalgebra A P s y)}) 
  (γ x)
CB: forall x : A t, P t x -> ClosedUnderOp A P (α x)
QA: forall a : A t * FamilyProd A (dom_symboltype w),
ap_operation (γ (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))
QB: forall
a : carriers_subalgebra A P t *
    FamilyProd (carriers_subalgebra A P)
      (dom_symboltype w),
ap_operation (ζ (class_of (Ψ t) (fst a)))
  (map_family_prod 
     (λ s : Sort σ, class_of (Ψ s)) 
     (snd a)) =
class_of (Ψ (cod_symboltype w))
  (ap_operation
     (op_subalgebra A P 
        (α (fst a).1) 
        (CB (fst a).1 (fst a).2)) 
     (snd a))
IHw: forall (α : Operation A w)
(γ : Operation (carriers_quotient_algebra A Φ) w)
(ζ : Operation
       (carriers_quotient_algebra (A && P) Ψ) w)
(CA : ClosedUnderOp 
        (A / Φ)
        (λ (s : Sort σ)
         (x : carriers_quotient_algebra A Φ s),
         Trunc (-1)
           {y : 
           carriers_subalgebra A P s &
           in_class 
             (Φ s) x
             (def_inc_subalgebra A P s y)}) γ)
(CB : ClosedUnderOp A P α),
(forall a : FamilyProd A (dom_symboltype w),
 ap_operation γ
   (map_family_prod
      (λ s : Sort σ, class_of (Φ s)) a) =
 class_of (Φ (cod_symboltype w))
   (ap_operation α a)) ->
(forall
 a : FamilyProd 
       (carriers_subalgebra A P)
       (dom_symboltype w),
 ap_operation ζ
   (map_family_prod
      (λ s : Sort σ, class_of (Ψ s)) a) =
 class_of (Ψ (cod_symboltype w))
   (ap_operation (op_subalgebra A P α CB) a)) ->
OpPreserving def_second_isomorphism ζ
  (op_subalgebra 
     (A / Φ)
     (λ (s : Sort σ)
      (x : carriers_quotient_algebra A Φ s),
      Trunc (-1)
        {y : carriers_subalgebra A P s &
        in_class 
          (Φ s) x 
          (def_inc_subalgebra A P s y)}) γ CA)
forall a : (A && P) t,
OpPreserving def_second_isomorphism
  (ζ (class_of (Ψ t) a))
  (op_subalgebra (A / Φ)
     (λ (s : Sort σ)
      (x : carriers_quotient_algebra A Φ s),
      Trunc (-1)
        {y : carriers_subalgebra A P s &
        in_class (Φ s) x (def_inc_subalgebra A P s y)})
     (γ
        (def_second_isomorphism t (class_of (Ψ t) a)).1)
     (CA
        (def_second_isomorphism t (class_of (Ψ t) a)).1
        (def_second_isomorphism t (class_of (Ψ t) a)).2)) intro x.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
α: A t -> Operation A w
γ: carriers_quotient_algebra A Φ t ->
Operation (carriers_quotient_algebra A Φ) w
ζ: carriers_quotient_algebra (A && P) Ψ t ->
Operation (carriers_quotient_algebra (A && P) Ψ) w
CA: forall x : carriers_quotient_algebra A Φ t,
Trunc (-1)
  {y : carriers_subalgebra A P t &
  in_class (Φ t) x (def_inc_subalgebra A P t y)} ->
ClosedUnderOp (A / Φ)
  (λ (s : Sort σ)
   (x0 : carriers_quotient_algebra A Φ s),
   Trunc (-1)
     {y : carriers_subalgebra A P s &
     in_class (Φ s) x0
       (def_inc_subalgebra A P s y)}) 
  (γ x)
CB: forall x : A t, P t x -> ClosedUnderOp A P (α x)
QA: forall a : A t * FamilyProd A (dom_symboltype w),
ap_operation (γ (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))
QB: forall
a : carriers_subalgebra A P t *
    FamilyProd (carriers_subalgebra A P)
      (dom_symboltype w),
ap_operation (ζ (class_of (Ψ t) (fst a)))
  (map_family_prod 
     (λ s : Sort σ, class_of (Ψ s)) 
     (snd a)) =
class_of (Ψ (cod_symboltype w))
  (ap_operation
     (op_subalgebra A P 
        (α (fst a).1) 
        (CB (fst a).1 (fst a).2)) 
     (snd a))
IHw: forall (α : Operation A w)
(γ : Operation (carriers_quotient_algebra A Φ) w)
(ζ : Operation
       (carriers_quotient_algebra (A && P) Ψ) w)
(CA : ClosedUnderOp 
        (A / Φ)
        (λ (s : Sort σ)
         (x : carriers_quotient_algebra A Φ s),
         Trunc (-1)
           {y : 
           carriers_subalgebra A P s &
           in_class 
             (Φ s) x
             (def_inc_subalgebra A P s y)}) γ)
(CB : ClosedUnderOp A P α),
(forall a : FamilyProd A (dom_symboltype w),
 ap_operation γ
   (map_family_prod
      (λ s : Sort σ, class_of (Φ s)) a) =
 class_of (Φ (cod_symboltype w))
   (ap_operation α a)) ->
(forall
 a : FamilyProd 
       (carriers_subalgebra A P)
       (dom_symboltype w),
 ap_operation ζ
   (map_family_prod
      (λ s : Sort σ, class_of (Ψ s)) a) =
 class_of (Ψ (cod_symboltype w))
   (ap_operation (op_subalgebra A P α CB) a)) ->
OpPreserving def_second_isomorphism ζ
  (op_subalgebra 
     (A / Φ)
     (λ (s : Sort σ)
      (x : carriers_quotient_algebra A Φ s),
      Trunc (-1)
        {y : carriers_subalgebra A P s &
        in_class 
          (Φ s) x 
          (def_inc_subalgebra A P s y)}) γ CA)
x: (A && P) t
OpPreserving def_second_isomorphism
  (ζ (class_of (Ψ t) x))
  (op_subalgebra (A / Φ)
     (λ (s : Sort σ)
      (x : carriers_quotient_algebra A Φ s),
      Trunc (-1)
        {y : carriers_subalgebra A P s &
        in_class (Φ s) x (def_inc_subalgebra A P s y)})
     (γ
        (def_second_isomorphism t (class_of (Ψ t) x)).1)
     (CA
        (def_second_isomorphism t (class_of (Ψ t) x)).1
        (def_second_isomorphism t (class_of (Ψ t) x)).2))
      apply (IHw (α (i t x)) (γ (class_of (Φ t) (i t x)))
              (ζ (class_of (Ψ t) x))
              (CA (class_of (Φ t) (i t x)) (tr (x; _)))
              (CB (i t x) x.2)).H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
α: A t -> Operation A w
γ: carriers_quotient_algebra A Φ t ->
Operation (carriers_quotient_algebra A Φ) w
ζ: carriers_quotient_algebra (A && P) Ψ t ->
Operation (carriers_quotient_algebra (A && P) Ψ) w
CA: forall x : carriers_quotient_algebra A Φ t,
Trunc (-1)
  {y : carriers_subalgebra A P t &
  in_class (Φ t) x (def_inc_subalgebra A P t y)} ->
ClosedUnderOp (A / Φ)
  (λ (s : Sort σ)
   (x0 : carriers_quotient_algebra A Φ s),
   Trunc (-1)
     {y : carriers_subalgebra A P s &
     in_class (Φ s) x0
       (def_inc_subalgebra A P s y)}) 
  (γ x)
CB: forall x : A t, P t x -> ClosedUnderOp A P (α x)
QA: forall a : A t * FamilyProd A (dom_symboltype w),
ap_operation (γ (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))
QB: forall
a : carriers_subalgebra A P t *
    FamilyProd (carriers_subalgebra A P)
      (dom_symboltype w),
ap_operation (ζ (class_of (Ψ t) (fst a)))
  (map_family_prod 
     (λ s : Sort σ, class_of (Ψ s)) 
     (snd a)) =
class_of (Ψ (cod_symboltype w))
  (ap_operation
     (op_subalgebra A P 
        (α (fst a).1) 
        (CB (fst a).1 (fst a).2)) 
     (snd a))
IHw: forall (α : Operation A w)
(γ : Operation (carriers_quotient_algebra A Φ) w)
(ζ : Operation
       (carriers_quotient_algebra (A && P) Ψ) w)
(CA : ClosedUnderOp 
        (A / Φ)
        (λ (s : Sort σ)
         (x : carriers_quotient_algebra A Φ s),
         Trunc (-1)
           {y : 
           carriers_subalgebra A P s &
           in_class 
             (Φ s) x
             (def_inc_subalgebra A P s y)}) γ)
(CB : ClosedUnderOp A P α),
(forall a : FamilyProd A (dom_symboltype w),
 ap_operation γ
   (map_family_prod
      (λ s : Sort σ, class_of (Φ s)) a) =
 class_of (Φ (cod_symboltype w))
   (ap_operation α a)) ->
(forall
 a : FamilyProd 
       (carriers_subalgebra A P)
       (dom_symboltype w),
 ap_operation ζ
   (map_family_prod
      (λ s : Sort σ, class_of (Ψ s)) a) =
 class_of (Ψ (cod_symboltype w))
   (ap_operation (op_subalgebra A P α CB) a)) ->
OpPreserving def_second_isomorphism ζ
  (op_subalgebra 
     (A / Φ)
     (λ (s : Sort σ)
      (x : carriers_quotient_algebra A Φ s),
      Trunc (-1)
        {y : carriers_subalgebra A P s &
        in_class 
          (Φ s) x 
          (def_inc_subalgebra A P s y)}) γ CA)
x: (A && P) t
forall a : FamilyProd A (dom_symboltype w),
ap_operation (γ (class_of (Φ t) (i t x)))
  (map_family_prod (λ s : Sort σ, class_of (Φ s)) a) =
class_of (Φ (cod_symboltype w))
  (ap_operation (α (i t x)) a)
H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
α: A t -> Operation A w
γ: carriers_quotient_algebra A Φ t ->
Operation (carriers_quotient_algebra A Φ) w
ζ: carriers_quotient_algebra (A && P) Ψ t ->
Operation (carriers_quotient_algebra (A && P) Ψ) w
CA: forall x : carriers_quotient_algebra A Φ t,
Trunc (-1)
  {y : carriers_subalgebra A P t &
  in_class (Φ t) x (def_inc_subalgebra A P t y)} ->
ClosedUnderOp (A / Φ)
  (λ (s : Sort σ)
   (x0 : carriers_quotient_algebra A Φ s),
   Trunc (-1)
     {y : carriers_subalgebra A P s &
     in_class (Φ s) x0
       (def_inc_subalgebra A P s y)}) 
  (γ x)
CB: forall x : A t, P t x -> ClosedUnderOp A P (α x)
QA: forall a : A t * FamilyProd A (dom_symboltype w),
ap_operation (γ (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))
QB: forall
a : carriers_subalgebra A P t *
    FamilyProd (carriers_subalgebra A P)
      (dom_symboltype w),
ap_operation (ζ (class_of (Ψ t) (fst a)))
  (map_family_prod 
     (λ s : Sort σ, class_of (Ψ s)) 
     (snd a)) =
class_of (Ψ (cod_symboltype w))
  (ap_operation
     (op_subalgebra A P 
        (α (fst a).1) 
        (CB (fst a).1 (fst a).2)) 
     (snd a))
IHw: forall (α : Operation A w)
(γ : Operation (carriers_quotient_algebra A Φ) w)
(ζ : Operation
       (carriers_quotient_algebra (A && P) Ψ) w)
(CA : ClosedUnderOp 
        (A / Φ)
        (λ (s : Sort σ)
         (x : carriers_quotient_algebra A Φ s),
         Trunc (-1)
           {y : 
           carriers_subalgebra A P s &
           in_class 
             (Φ s) x
             (def_inc_subalgebra A P s y)}) γ)
(CB : ClosedUnderOp A P α),
(forall a : FamilyProd A (dom_symboltype w),
 ap_operation γ
   (map_family_prod
      (λ s : Sort σ, class_of (Φ s)) a) =
 class_of (Φ (cod_symboltype w))
   (ap_operation α a)) ->
(forall
 a : FamilyProd 
       (carriers_subalgebra A P)
       (dom_symboltype w),
 ap_operation ζ
   (map_family_prod
      (λ s : Sort σ, class_of (Ψ s)) a) =
 class_of (Ψ (cod_symboltype w))
   (ap_operation (op_subalgebra A P α CB) a)) ->
OpPreserving def_second_isomorphism ζ
  (op_subalgebra 
     (A / Φ)
     (λ (s : Sort σ)
      (x : carriers_quotient_algebra A Φ s),
      Trunc (-1)
        {y : carriers_subalgebra A P s &
        in_class 
          (Φ s) x 
          (def_inc_subalgebra A P s y)}) γ CA)
x: (A && P) t
forall
a : FamilyProd (carriers_subalgebra A P)
      (dom_symboltype w),
ap_operation (ζ (class_of (Ψ t) x))
  (map_family_prod (λ s : Sort σ, class_of (Ψ s)) a) =
class_of (Ψ (cod_symboltype w))
  (ap_operation
     (op_subalgebra A P (α (i t x)) (CB (i t x) x.2))
     a)
      +H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
α: A t -> Operation A w
γ: carriers_quotient_algebra A Φ t ->
Operation (carriers_quotient_algebra A Φ) w
ζ: carriers_quotient_algebra (A && P) Ψ t ->
Operation (carriers_quotient_algebra (A && P) Ψ) w
CA: forall x : carriers_quotient_algebra A Φ t,
Trunc (-1)
  {y : carriers_subalgebra A P t &
  in_class (Φ t) x (def_inc_subalgebra A P t y)} ->
ClosedUnderOp (A / Φ)
  (λ (s : Sort σ)
   (x0 : carriers_quotient_algebra A Φ s),
   Trunc (-1)
     {y : carriers_subalgebra A P s &
     in_class (Φ s) x0
       (def_inc_subalgebra A P s y)}) 
  (γ x)
CB: forall x : A t, P t x -> ClosedUnderOp A P (α x)
QA: forall a : A t * FamilyProd A (dom_symboltype w),
ap_operation (γ (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))
QB: forall
a : carriers_subalgebra A P t *
    FamilyProd (carriers_subalgebra A P)
      (dom_symboltype w),
ap_operation (ζ (class_of (Ψ t) (fst a)))
  (map_family_prod 
     (λ s : Sort σ, class_of (Ψ s)) 
     (snd a)) =
class_of (Ψ (cod_symboltype w))
  (ap_operation
     (op_subalgebra A P 
        (α (fst a).1) 
        (CB (fst a).1 (fst a).2)) 
     (snd a))
IHw: forall (α : Operation A w)
(γ : Operation (carriers_quotient_algebra A Φ) w)
(ζ : Operation
       (carriers_quotient_algebra (A && P) Ψ) w)
(CA : ClosedUnderOp 
        (A / Φ)
        (λ (s : Sort σ)
         (x : carriers_quotient_algebra A Φ s),
         Trunc (-1)
           {y : 
           carriers_subalgebra A P s &
           in_class 
             (Φ s) x
             (def_inc_subalgebra A P s y)}) γ)
(CB : ClosedUnderOp A P α),
(forall a : FamilyProd A (dom_symboltype w),
 ap_operation γ
   (map_family_prod
      (λ s : Sort σ, class_of (Φ s)) a) =
 class_of (Φ (cod_symboltype w))
   (ap_operation α a)) ->
(forall
 a : FamilyProd 
       (carriers_subalgebra A P)
       (dom_symboltype w),
 ap_operation ζ
   (map_family_prod
      (λ s : Sort σ, class_of (Ψ s)) a) =
 class_of (Ψ (cod_symboltype w))
   (ap_operation (op_subalgebra A P α CB) a)) ->
OpPreserving def_second_isomorphism ζ
  (op_subalgebra 
     (A / Φ)
     (λ (s : Sort σ)
      (x : carriers_quotient_algebra A Φ s),
      Trunc (-1)
        {y : carriers_subalgebra A P s &
        in_class 
          (Φ s) x 
          (def_inc_subalgebra A P s y)}) γ CA)
x: (A && P) t
forall a : FamilyProd A (dom_symboltype w),
ap_operation (γ (class_of (Φ t) (i t x)))
  (map_family_prod (λ s : Sort σ, class_of (Φ s)) a) =
class_of (Φ (cod_symboltype w))
  (ap_operation (α (i t x)) a) intro a.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
α: A t -> Operation A w
γ: carriers_quotient_algebra A Φ t ->
Operation (carriers_quotient_algebra A Φ) w
ζ: carriers_quotient_algebra (A && P) Ψ t ->
Operation (carriers_quotient_algebra (A && P) Ψ) w
CA: forall x : carriers_quotient_algebra A Φ t,
Trunc (-1)
  {y : carriers_subalgebra A P t &
  in_class (Φ t) x (def_inc_subalgebra A P t y)} ->
ClosedUnderOp (A / Φ)
  (λ (s : Sort σ)
   (x0 : carriers_quotient_algebra A Φ s),
   Trunc (-1)
     {y : carriers_subalgebra A P s &
     in_class (Φ s) x0
       (def_inc_subalgebra A P s y)}) 
  (γ x)
CB: forall x : A t, P t x -> ClosedUnderOp A P (α x)
QA: forall a : A t * FamilyProd A (dom_symboltype w),
ap_operation (γ (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))
QB: forall
a : carriers_subalgebra A P t *
    FamilyProd (carriers_subalgebra A P)
      (dom_symboltype w),
ap_operation (ζ (class_of (Ψ t) (fst a)))
  (map_family_prod 
     (λ s : Sort σ, class_of (Ψ s)) 
     (snd a)) =
class_of (Ψ (cod_symboltype w))
  (ap_operation
     (op_subalgebra A P 
        (α (fst a).1) 
        (CB (fst a).1 (fst a).2)) 
     (snd a))
IHw: forall (α : Operation A w)
(γ : Operation (carriers_quotient_algebra A Φ) w)
(ζ : Operation
       (carriers_quotient_algebra (A && P) Ψ) w)
(CA : ClosedUnderOp 
        (A / Φ)
        (λ (s : Sort σ)
         (x : carriers_quotient_algebra A Φ s),
         Trunc (-1)
           {y : 
           carriers_subalgebra A P s &
           in_class 
             (Φ s) x
             (def_inc_subalgebra A P s y)}) γ)
(CB : ClosedUnderOp A P α),
(forall a : FamilyProd A (dom_symboltype w),
 ap_operation γ
   (map_family_prod
      (λ s : Sort σ, class_of (Φ s)) a) =
 class_of (Φ (cod_symboltype w))
   (ap_operation α a)) ->
(forall
 a : FamilyProd 
       (carriers_subalgebra A P)
       (dom_symboltype w),
 ap_operation ζ
   (map_family_prod
      (λ s : Sort σ, class_of (Ψ s)) a) =
 class_of (Ψ (cod_symboltype w))
   (ap_operation (op_subalgebra A P α CB) a)) ->
OpPreserving def_second_isomorphism ζ
  (op_subalgebra 
     (A / Φ)
     (λ (s : Sort σ)
      (x : carriers_quotient_algebra A Φ s),
      Trunc (-1)
        {y : carriers_subalgebra A P s &
        in_class 
          (Φ s) x 
          (def_inc_subalgebra A P s y)}) γ CA)
x: (A && P) t
a: FamilyProd A (dom_symboltype w)
ap_operation (γ (class_of (Φ t) (i t x)))
  (map_family_prod (λ s : Sort σ, class_of (Φ s)) a) =
class_of (Φ (cod_symboltype w))
  (ap_operation (α (i t x)) a) exact (QA (i t x, a)).
      +H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
α: A t -> Operation A w
γ: carriers_quotient_algebra A Φ t ->
Operation (carriers_quotient_algebra A Φ) w
ζ: carriers_quotient_algebra (A && P) Ψ t ->
Operation (carriers_quotient_algebra (A && P) Ψ) w
CA: forall x : carriers_quotient_algebra A Φ t,
Trunc (-1)
  {y : carriers_subalgebra A P t &
  in_class (Φ t) x (def_inc_subalgebra A P t y)} ->
ClosedUnderOp (A / Φ)
  (λ (s : Sort σ)
   (x0 : carriers_quotient_algebra A Φ s),
   Trunc (-1)
     {y : carriers_subalgebra A P s &
     in_class (Φ s) x0
       (def_inc_subalgebra A P s y)}) 
  (γ x)
CB: forall x : A t, P t x -> ClosedUnderOp A P (α x)
QA: forall a : A t * FamilyProd A (dom_symboltype w),
ap_operation (γ (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))
QB: forall
a : carriers_subalgebra A P t *
    FamilyProd (carriers_subalgebra A P)
      (dom_symboltype w),
ap_operation (ζ (class_of (Ψ t) (fst a)))
  (map_family_prod 
     (λ s : Sort σ, class_of (Ψ s)) 
     (snd a)) =
class_of (Ψ (cod_symboltype w))
  (ap_operation
     (op_subalgebra A P 
        (α (fst a).1) 
        (CB (fst a).1 (fst a).2)) 
     (snd a))
IHw: forall (α : Operation A w)
(γ : Operation (carriers_quotient_algebra A Φ) w)
(ζ : Operation
       (carriers_quotient_algebra (A && P) Ψ) w)
(CA : ClosedUnderOp 
        (A / Φ)
        (λ (s : Sort σ)
         (x : carriers_quotient_algebra A Φ s),
         Trunc (-1)
           {y : 
           carriers_subalgebra A P s &
           in_class 
             (Φ s) x
             (def_inc_subalgebra A P s y)}) γ)
(CB : ClosedUnderOp A P α),
(forall a : FamilyProd A (dom_symboltype w),
 ap_operation γ
   (map_family_prod
      (λ s : Sort σ, class_of (Φ s)) a) =
 class_of (Φ (cod_symboltype w))
   (ap_operation α a)) ->
(forall
 a : FamilyProd 
       (carriers_subalgebra A P)
       (dom_symboltype w),
 ap_operation ζ
   (map_family_prod
      (λ s : Sort σ, class_of (Ψ s)) a) =
 class_of (Ψ (cod_symboltype w))
   (ap_operation (op_subalgebra A P α CB) a)) ->
OpPreserving def_second_isomorphism ζ
  (op_subalgebra 
     (A / Φ)
     (λ (s : Sort σ)
      (x : carriers_quotient_algebra A Φ s),
      Trunc (-1)
        {y : carriers_subalgebra A P s &
        in_class 
          (Φ s) x 
          (def_inc_subalgebra A P s y)}) γ CA)
x: (A && P) t
forall
a : FamilyProd (carriers_subalgebra A P)
      (dom_symboltype w),
ap_operation (ζ (class_of (Ψ t) x))
  (map_family_prod (λ s : Sort σ, class_of (Ψ s)) a) =
class_of (Ψ (cod_symboltype w))
  (ap_operation
     (op_subalgebra A P (α (i t x)) (CB (i t x) x.2))
     a) intro a.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
α: A t -> Operation A w
γ: carriers_quotient_algebra A Φ t ->
Operation (carriers_quotient_algebra A Φ) w
ζ: carriers_quotient_algebra (A && P) Ψ t ->
Operation (carriers_quotient_algebra (A && P) Ψ) w
CA: forall x : carriers_quotient_algebra A Φ t,
Trunc (-1)
  {y : carriers_subalgebra A P t &
  in_class (Φ t) x (def_inc_subalgebra A P t y)} ->
ClosedUnderOp (A / Φ)
  (λ (s : Sort σ)
   (x0 : carriers_quotient_algebra A Φ s),
   Trunc (-1)
     {y : carriers_subalgebra A P s &
     in_class (Φ s) x0
       (def_inc_subalgebra A P s y)}) 
  (γ x)
CB: forall x : A t, P t x -> ClosedUnderOp A P (α x)
QA: forall a : A t * FamilyProd A (dom_symboltype w),
ap_operation (γ (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))
QB: forall
a : carriers_subalgebra A P t *
    FamilyProd (carriers_subalgebra A P)
      (dom_symboltype w),
ap_operation (ζ (class_of (Ψ t) (fst a)))
  (map_family_prod 
     (λ s : Sort σ, class_of (Ψ s)) 
     (snd a)) =
class_of (Ψ (cod_symboltype w))
  (ap_operation
     (op_subalgebra A P 
        (α (fst a).1) 
        (CB (fst a).1 (fst a).2)) 
     (snd a))
IHw: forall (α : Operation A w)
(γ : Operation (carriers_quotient_algebra A Φ) w)
(ζ : Operation
       (carriers_quotient_algebra (A && P) Ψ) w)
(CA : ClosedUnderOp 
        (A / Φ)
        (λ (s : Sort σ)
         (x : carriers_quotient_algebra A Φ s),
         Trunc (-1)
           {y : 
           carriers_subalgebra A P s &
           in_class 
             (Φ s) x
             (def_inc_subalgebra A P s y)}) γ)
(CB : ClosedUnderOp A P α),
(forall a : FamilyProd A (dom_symboltype w),
 ap_operation γ
   (map_family_prod
      (λ s : Sort σ, class_of (Φ s)) a) =
 class_of (Φ (cod_symboltype w))
   (ap_operation α a)) ->
(forall
 a : FamilyProd 
       (carriers_subalgebra A P)
       (dom_symboltype w),
 ap_operation ζ
   (map_family_prod
      (λ s : Sort σ, class_of (Ψ s)) a) =
 class_of (Ψ (cod_symboltype w))
   (ap_operation (op_subalgebra A P α CB) a)) ->
OpPreserving def_second_isomorphism ζ
  (op_subalgebra 
     (A / Φ)
     (λ (s : Sort σ)
      (x : carriers_quotient_algebra A Φ s),
      Trunc (-1)
        {y : carriers_subalgebra A P s &
        in_class 
          (Φ s) x 
          (def_inc_subalgebra A P s y)}) γ CA)
x: (A && P) t
a: FamilyProd (carriers_subalgebra A P)
  (dom_symboltype w)
ap_operation (ζ (class_of (Ψ t) x))
  (map_family_prod (λ s : Sort σ, class_of (Ψ s)) a) =
class_of (Ψ (cod_symboltype w))
  (ap_operation
     (op_subalgebra A P (α (i t x)) (CB (i t x) x.2))
     a) exact (QB (x, a)).
  Defined.

  #[export] Instance is_homomorphism_second_isomorphism
    : IsHomomorphism def_second_isomorphism.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
IsHomomorphism def_second_isomorphism
  Proof.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
IsHomomorphism def_second_isomorphism
    intro u.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
u: Symbol σ
OpPreserving def_second_isomorphism u.#((A && P) / Ψ)
  u.#(A / Φ && (λ (s : Sort σ) (x : (A / Φ) s), Q s x))
    eapply oppreserving_second_isomorphism.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
u: Symbol σ
ComputeOpQuotient A Φ ?α u.#(A / Φ)
H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
u: Symbol σ
ComputeOpQuotient 
  (A && P) Ψ (op_subalgebra A P ?α ?CB)
  u.#((A && P) / Ψ)
    -H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
u: Symbol σ
ComputeOpQuotient A Φ ?α u.#(A / Φ) apply (compute_op_quotient A).
    -H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
u: Symbol σ
ComputeOpQuotient (A && P) Ψ
  (op_subalgebra A P u.#A ?CB) u.#((A && P) / Ψ) apply (compute_op_quotient (A&&P)).
  Defined.

  Definition hom_second_isomorphism
    : Homomorphism ((A&&P) / Ψ) ((A/Φ) && Q)
    := BuildHomomorphism def_second_isomorphism.

  #[export] Instance embedding_second_isomorphism (s : Sort σ)
    : IsEmbedding (hom_second_isomorphism s).H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
s: Sort σ
IsEmbedding (hom_second_isomorphism s)
  Proof.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
s: Sort σ
IsEmbedding (hom_second_isomorphism s)
    apply isembedding_isinj_hset.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
s: Sort σ
IsInjective (hom_second_isomorphism s)
    refine (Quotient_ind_hprop (Ψ s) _ _).H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
s: Sort σ
forall (a : (A && P) s) (y : ((A && P) / Ψ) s),
hom_second_isomorphism s (class_of (Ψ s) a) =
hom_second_isomorphism s y -> class_of (Ψ s) a = y intro x.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
s: Sort σ
x: (A && P) s
forall y : ((A && P) / Ψ) s,
hom_second_isomorphism s (class_of (Ψ s) x) =
hom_second_isomorphism s y -> class_of (Ψ s) x = y
    refine (Quotient_ind_hprop (Ψ s) _ _).H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
s: Sort σ
x: (A && P) s
forall a : (A && P) s,
hom_second_isomorphism s (class_of (Ψ s) x) =
hom_second_isomorphism s (class_of (Ψ s) a) ->
class_of (Ψ s) x = class_of (Ψ s) a intros y p.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
s: Sort σ
x, y: (A && P) s
p: hom_second_isomorphism s (class_of (Ψ s) x) =
hom_second_isomorphism s (class_of (Ψ s) y)
class_of (Ψ s) x = class_of (Ψ s) y
    apply qglue.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
s: Sort σ
x, y: (A && P) s
p: hom_second_isomorphism s (class_of (Ψ s) x) =
hom_second_isomorphism s (class_of (Ψ s) y)
Ψ s x y
    exact (related_quotient_paths (Φ s) (i s x) (i s y) (p..1)).
  Qed.

  #[export] Instance surjection_second_isomorphism (s : Sort σ)
    : IsSurjection (hom_second_isomorphism s).H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
s: Sort σ
ReflectiveSubuniverse.IsConnMap (Tr (-1))
  (hom_second_isomorphism s)
  Proof.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
s: Sort σ
ReflectiveSubuniverse.IsConnMap (Tr (-1))
  (hom_second_isomorphism s)
    apply BuildIsSurjection.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
s: Sort σ
forall
b : (A / Φ && (λ (s : Sort σ) (x : (A / Φ) s), Q s x))
      s, merely (hfiber (hom_second_isomorphism s) b)
    intros [y S].H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
s: Sort σ
y: (A / Φ) s
S: Q s y
merely (hfiber (hom_second_isomorphism s) (y; S))
    generalize dependent S.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
s: Sort σ
y: (A / Φ) s
forall S : Q s y,
merely (hfiber (hom_second_isomorphism s) (y; S))
    generalize dependent y.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
s: Sort σ
forall (y : (A / Φ) s) (S : Q s y),
merely (hfiber (hom_second_isomorphism s) (y; S))
    refine (Quotient_ind_hprop (Φ s) _ _).H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
s: Sort σ
forall (a : A s) (S : Q s (class_of (Φ s) a)),
merely
  (hfiber (hom_second_isomorphism s)
     (class_of (Φ s) a; S)) intros y S.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
s: Sort σ
y: A s
S: Q s (class_of (Φ s) y)
merely
  (hfiber (hom_second_isomorphism s)
     (class_of (Φ s) y; S))
    refine (Trunc_rec _ S).H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
s: Sort σ
y: A s
S: Q s (class_of (Φ s) y)
{y0 : (A && P) s &
in_class (Φ s) (class_of (Φ s) y) (i s y0)} ->
merely
  (hfiber (hom_second_isomorphism s)
     (class_of (Φ s) y; S)) intros [y' S'].H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
s: Sort σ
y: A s
S: Q s (class_of (Φ s) y)
y': (A && P) s
S': in_class (Φ s) (class_of (Φ s) y) (i s y')
merely
  (hfiber (hom_second_isomorphism s)
     (class_of (Φ s) y; S)) apply tr.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
s: Sort σ
y: A s
S: Q s (class_of (Φ s) y)
y': (A && P) s
S': in_class (Φ s) (class_of (Φ s) y) (i s y')
hfiber (hom_second_isomorphism s)
  (class_of (Φ s) y; S)
    exists (class_of _ y').H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
s: Sort σ
y: A s
S: Q s (class_of (Φ s) y)
y': (A && P) s
S': in_class (Φ s) (class_of (Φ s) y) (i s y')
hom_second_isomorphism s (class_of (Ψ s) y') =
(class_of (Φ s) y; S)
    apply path_sigma_hprop.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
s: Sort σ
y: A s
S: Q s (class_of (Φ s) y)
y': (A && P) s
S': in_class (Φ s) (class_of (Φ s) y) (i s y')
(hom_second_isomorphism s (class_of (Ψ s) y')).1 =
(class_of (Φ s) y; S).1
    by apply qglue.
  Qed.

  Theorem is_isomorphism_second_isomorphism
    : IsIsomorphism hom_second_isomorphism.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
IsIsomorphism hom_second_isomorphism
  Proof.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
IsIsomorphism hom_second_isomorphism
    intro s.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
s: Sort σ
IsEquiv (hom_second_isomorphism s) apply isequiv_surj_emb; exact _.
  Qed.

  #[export] Existing Instance is_isomorphism_second_isomorphism.

  Theorem isomorphic_second_isomorphism : (A&&P) / Ψ ≅ (A/Φ) && Q.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
(A && P) / Ψ
≅ A / Φ && (λ (s : Sort σ) (x : (A / Φ) s), Q s x)
  Proof.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
(A && P) / Ψ
≅ A / Φ && (λ (s : Sort σ) (x : (A / Φ) s), Q s x)
    exact (BuildIsomorphic def_second_isomorphism).
  Defined.

  Corollary id_second_isomorphism : (A&&P) / Ψ = (A/Φ) && Q.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
(A && P) / Ψ =
A / Φ && (λ (s : Sort σ) (x : (A / Φ) s), Q s x)
  Proof.H: Univalence
σ: Signature
A: Algebra σ
P: forall s : Sort σ, A s -> Type
IsSubalgebraPredicate0: IsSubalgebraPredicate A P
Φ: forall s : Sort σ, Relation (A s)
IsCongruence0: IsCongruence A Φ
(A && P) / Ψ =
A / Φ && (λ (s : Sort σ) (x : (A / Φ) s), Q s x)
    exact (id_isomorphic isomorphic_second_isomorphism).
  Defined.
End second_isomorphism.