(** This file defines the kernel of a homomorphism [cong_ker], the
    image of a homomorphism [in_image_hom], and it proves the first
    isomorphism theorem [isomorphic_first_isomorphism]. The first
    identification theorem [id_first_isomorphism] follows. *)

Require Import
  Basics.Notations
  HSet
  Colimits.Quotient
  Classes.interfaces.canonical_names
  Classes.theory.ua_isomorphic
  Classes.theory.ua_subalgebra
  Classes.theory.ua_quotient_algebra.

Import
  algebra_notations
  quotient_algebra_notations
  subalgebra_notations
  isomorphic_notations.

(** The following section defines the kernel of a homomorphism
    [cong_ker], and shows that it is a congruence.*)

Section cong_ker.
  Context
    {σ : Signature} {A B : Algebra σ} `{IsHSetAlgebra B}
    (f : ∀ s, A s → B s) `{!IsHomomorphism f}.

  Definition cong_ker (s : Sort σ) : Relation (A s)
    := λ (x y : A s), f s x = f s y.

(* Leave the following results about [cong_ker] opaque because they
   are h-props. *)

  #[export] Instance equiv_rel_ker (s : Sort σ)
    : EquivRel (cong_ker s).
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s0 : Sort σ, A s0 -> B s0
IsHomomorphism0: IsHomomorphism f
s: Sort σ
EquivRel (cong_ker s)
  Proof.
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s0 : Sort σ, A s0 -> B s0
IsHomomorphism0: IsHomomorphism f
s: Sort σ
EquivRel (cong_ker s)
    repeat constructor.
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s0 : Sort σ, A s0 -> B s0
IsHomomorphism0: IsHomomorphism f
s: Sort σ
Symmetric (cong_ker s)
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s0 : Sort σ, A s0 -> B s0
IsHomomorphism0: IsHomomorphism f
s: Sort σ
Transitive (cong_ker s)
    -
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s0 : Sort σ, A s0 -> B s0
IsHomomorphism0: IsHomomorphism f
s: Sort σ
Symmetric (cong_ker s) intros x y.
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s0 : Sort σ, A s0 -> B s0
IsHomomorphism0: IsHomomorphism f
s: Sort σ
x, y: A s
cong_ker s x y -> cong_ker s y x exact inverse.
    -
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s0 : Sort σ, A s0 -> B s0
IsHomomorphism0: IsHomomorphism f
s: Sort σ
Transitive (cong_ker s) intros x y z.
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s0 : Sort σ, A s0 -> B s0
IsHomomorphism0: IsHomomorphism f
s: Sort σ
x, y, z: A s
cong_ker s x y -> cong_ker s y z -> cong_ker s x z exact concat.
  Qed.

  Lemma path_ap_operation_ker_related {w : SymbolType σ}
    (β : Operation B w) (a b : FamilyProd A (dom_symboltype w))
    (R : for_all_2_family_prod A A cong_ker a b)
    : ap_operation β (map_family_prod f a)
      = ap_operation β (map_family_prod f b).
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
w: SymbolType σ
β: Operation B w
a, b: FamilyProd A (dom_symboltype w)
R: for_all_2_family_prod A A cong_ker a b
ap_operation β (map_family_prod f a) = ap_operation β (map_family_prod f b)
  Proof.
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
w: SymbolType σ
β: Operation B w
a, b: FamilyProd A (dom_symboltype w)
R: for_all_2_family_prod A A cong_ker a b
ap_operation β (map_family_prod f a) = ap_operation β (map_family_prod f b)
    induction w.
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
t: Sort σ
β: Operation B (ne_list.one t)
a, b: FamilyProd A (dom_symboltype (ne_list.one t))
R: for_all_2_family_prod A A cong_ker a b
ap_operation β (map_family_prod f a) = ap_operation β (map_family_prod f b)
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
β: Operation B (ne_list.cons t w)
a, b: FamilyProd A (dom_symboltype (ne_list.cons t w))
R: for_all_2_family_prod A A cong_ker a b
IHw: forall (β0 : Operation B w) (a0 b0 : FamilyProd A (dom_symboltype w)),
for_all_2_family_prod A A cong_ker a0 b0 ->
ap_operation β0 (map_family_prod f a0) =
ap_operation β0 (map_family_prod f b0)
ap_operation β (map_family_prod f a) = ap_operation β (map_family_prod f b)
    -
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
t: Sort σ
β: Operation B (ne_list.one t)
a, b: FamilyProd A (dom_symboltype (ne_list.one t))
R: for_all_2_family_prod A A cong_ker a b
ap_operation β (map_family_prod f a) = ap_operation β (map_family_prod f b) reflexivity.
    -
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
β: Operation B (ne_list.cons t w)
a, b: FamilyProd A (dom_symboltype (ne_list.cons t w))
R: for_all_2_family_prod A A cong_ker a b
IHw: forall (β0 : Operation B w) (a0 b0 : FamilyProd A (dom_symboltype w)),
for_all_2_family_prod A A cong_ker a0 b0 ->
ap_operation β0 (map_family_prod f a0) =
ap_operation β0 (map_family_prod f b0)
ap_operation β (map_family_prod f a) = ap_operation β (map_family_prod f b) destruct a as [x a], b as [y b], R as [r R].
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
β: Operation B (ne_list.cons t w)
x: A t
a: Core.fold_right (λ (i : Sort σ) (A0 : Type), A i * A0) Unit
  (dom_symboltype w)
y: A t
b: Core.fold_right (λ (i : Sort σ) (A0 : Type), A i * A0) Unit
  (dom_symboltype w)
r: cong_ker t x y
R: for_all_2_family_prod A A cong_ker a b
IHw: forall (β0 : Operation B w) (a0 b0 : FamilyProd A (dom_symboltype w)),
for_all_2_family_prod A A cong_ker a0 b0 ->
ap_operation β0 (map_family_prod f a0) =
ap_operation β0 (map_family_prod f b0)
ap_operation β (map_family_prod f (x, a)) =
ap_operation β (map_family_prod f (y, b))
      cbn.
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
β: Operation B (ne_list.cons t w)
x: A t
a: Core.fold_right (λ (i : Sort σ) (A0 : Type), A i * A0) Unit
  (dom_symboltype w)
y: A t
b: Core.fold_right (λ (i : Sort σ) (A0 : Type), A i * A0) Unit
  (dom_symboltype w)
r: cong_ker t x y
R: for_all_2_family_prod A A cong_ker a b
IHw: forall (β0 : Operation B w) (a0 b0 : FamilyProd A (dom_symboltype w)),
for_all_2_family_prod A A cong_ker a0 b0 ->
ap_operation β0 (map_family_prod f a0) =
ap_operation β0 (map_family_prod f b0)
ap_operation (β (f t x)) (map_family_prod f a) =
ap_operation (β (f t y)) (map_family_prod f b) destruct r.
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
β: Operation B (ne_list.cons t w)
x: A t
a: Core.fold_right (λ (i : Sort σ) (A0 : Type), A i * A0) Unit
  (dom_symboltype w)
y: A t
b: Core.fold_right (λ (i : Sort σ) (A0 : Type), A i * A0) Unit
  (dom_symboltype w)
R: for_all_2_family_prod A A cong_ker a b
IHw: forall (β0 : Operation B w) (a0 b0 : FamilyProd A (dom_symboltype w)),
for_all_2_family_prod A A cong_ker a0 b0 ->
ap_operation β0 (map_family_prod f a0) =
ap_operation β0 (map_family_prod f b0)
ap_operation (β (f t x)) (map_family_prod f a) =
ap_operation (β (f t x)) (map_family_prod f b) by apply IHw.
  Qed.

  #[export] Instance ops_compatible_ker : OpsCompatible A cong_ker.
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
OpsCompatible A cong_ker
  Proof.
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
OpsCompatible A cong_ker
    intros u a b R.
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
u: Symbol σ
a, b: FamilyProd A (dom_symboltype (σ u))
R: for_all_2_family_prod A A cong_ker a b
cong_ker (cod_symboltype (σ u)) (ap_operation u.#A a) (ap_operation u.#A b)
    unfold cong_ker.
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
u: Symbol σ
a, b: FamilyProd A (dom_symboltype (σ u))
R: for_all_2_family_prod A A cong_ker a b
f (cod_symboltype (σ u)) (ap_operation u.#A a) =
f (cod_symboltype (σ u)) (ap_operation u.#A b)
    destruct (path_homomorphism_ap_operation f u a)^.
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
u: Symbol σ
a, b: FamilyProd A (dom_symboltype (σ u))
R: for_all_2_family_prod A A cong_ker a b
ap_operation u.#B (map_family_prod f a) =
f (cod_symboltype (σ u)) (ap_operation u.#A b)
    destruct (path_homomorphism_ap_operation f u b)^.
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
u: Symbol σ
a, b: FamilyProd A (dom_symboltype (σ u))
R: for_all_2_family_prod A A cong_ker a b
ap_operation u.#B (map_family_prod f a) =
ap_operation u.#B (map_family_prod f b)
    by apply path_ap_operation_ker_related.
  Qed.

  #[export] Instance is_congruence_ker : IsCongruence A cong_ker
    := BuildIsCongruence A cong_ker.

End cong_ker.

(** The next section defines an "in image predicate", [in_image_hom].
    It gives rise to the homomorphic image of a homomorphism. *)

Section in_image_hom.
  Context
    `{Funext} {σ : Signature} {A B : Algebra σ}
    (f : ∀ s, A s → B s) {hom : IsHomomorphism f}.

  Definition in_image_hom (s : Sort σ) (y : B s) : HProp
    := merely (hfiber (f s) y).

  Lemma closed_under_op_in_image_hom {w : SymbolType σ}
    (α : Operation A w) (β : Operation B w) (P : OpPreserving f α β)
    : ClosedUnderOp B in_image_hom β.
H: Funext
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
hom: IsHomomorphism f
w: SymbolType σ
α: Operation A w
β: Operation B w
P: OpPreserving f α β
ClosedUnderOp B (λ (s : Sort σ) (y : B s), in_image_hom s y) β
  Proof.
H: Funext
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
hom: IsHomomorphism f
w: SymbolType σ
α: Operation A w
β: Operation B w
P: OpPreserving f α β
ClosedUnderOp B (λ (s : Sort σ) (y : B s), in_image_hom s y) β
    induction w.
H: Funext
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
hom: IsHomomorphism f
t: Sort σ
α: Operation A (ne_list.one t)
β: Operation B (ne_list.one t)
P: OpPreserving f α β
ClosedUnderOp B (λ (s : Sort σ) (y : B s), in_image_hom s y) β
H: Funext
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
hom: IsHomomorphism f
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
α: Operation A (ne_list.cons t w)
β: Operation B (ne_list.cons t w)
P: OpPreserving f α β
IHw: forall (α0 : Operation A w) (β0 : Operation B w),
OpPreserving f α0 β0 ->
ClosedUnderOp B (λ (s : Sort σ) (y : B s), in_image_hom s y) β0
ClosedUnderOp B (λ (s : Sort σ) (y : B s), in_image_hom s y) β
    -
H: Funext
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
hom: IsHomomorphism f
t: Sort σ
α: Operation A (ne_list.one t)
β: Operation B (ne_list.one t)
P: OpPreserving f α β
ClosedUnderOp B (λ (s : Sort σ) (y : B s), in_image_hom s y) β exact (tr (α; P)).
    -
H: Funext
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
hom: IsHomomorphism f
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
α: Operation A (ne_list.cons t w)
β: Operation B (ne_list.cons t w)
P: OpPreserving f α β
IHw: forall (α0 : Operation A w) (β0 : Operation B w),
OpPreserving f α0 β0 ->
ClosedUnderOp B (λ (s : Sort σ) (y : B s), in_image_hom s y) β0
ClosedUnderOp B (λ (s : Sort σ) (y : B s), in_image_hom s y) β intro y.
H: Funext
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
hom: IsHomomorphism f
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
α: Operation A (ne_list.cons t w)
β: Operation B (ne_list.cons t w)
P: OpPreserving f α β
IHw: forall (α0 : Operation A w) (β0 : Operation B w),
OpPreserving f α0 β0 ->
ClosedUnderOp B (λ (s : Sort σ) (y0 : B s), in_image_hom s y0) β0
y: B t
in_image_hom t y ->
ClosedUnderOp B (λ (s : Sort σ) (y0 : B s), in_image_hom s y0) (β y)
      refine (Trunc_rec _).
H: Funext
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
hom: IsHomomorphism f
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
α: Operation A (ne_list.cons t w)
β: Operation B (ne_list.cons t w)
P: OpPreserving f α β
IHw: forall (α0 : Operation A w) (β0 : Operation B w),
OpPreserving f α0 β0 ->
ClosedUnderOp B (λ (s : Sort σ) (y0 : B s), in_image_hom s y0) β0
y: B t
hfiber (f t) y ->
ClosedUnderOp B (λ (s : Sort σ) (y0 : B s), in_image_hom s y0) (β y) intros [x p].
H: Funext
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
hom: IsHomomorphism f
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
α: Operation A (ne_list.cons t w)
β: Operation B (ne_list.cons t w)
P: OpPreserving f α β
IHw: forall (α0 : Operation A w) (β0 : Operation B w),
OpPreserving f α0 β0 ->
ClosedUnderOp B (λ (s : Sort σ) (y0 : B s), in_image_hom s y0) β0
y: B t
x: A t
p: f t x = y
ClosedUnderOp B (λ (s : Sort σ) (y0 : B s), in_image_hom s y0) (β y)
      apply (IHw (α x)).
H: Funext
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
hom: IsHomomorphism f
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
α: Operation A (ne_list.cons t w)
β: Operation B (ne_list.cons t w)
P: OpPreserving f α β
IHw: forall (α0 : Operation A w) (β0 : Operation B w),
OpPreserving f α0 β0 ->
ClosedUnderOp B (λ (s : Sort σ) (y0 : B s), in_image_hom s y0) β0
y: B t
x: A t
p: f t x = y
OpPreserving f (α x) (β y)
      by destruct p.
  Qed.

  Lemma is_closed_under_ops_in_image_hom
    : IsClosedUnderOps B in_image_hom.
H: Funext
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
hom: IsHomomorphism f
IsClosedUnderOps B (λ (s : Sort σ) (y : B s), in_image_hom s y)
  Proof.
H: Funext
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
hom: IsHomomorphism f
IsClosedUnderOps B (λ (s : Sort σ) (y : B s), in_image_hom s y)
    intro u.
H: Funext
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
hom: IsHomomorphism f
u: Symbol σ
ClosedUnderOp B (λ (s : Sort σ) (y : B s), in_image_hom s y) u.#B eapply closed_under_op_in_image_hom, hom.
  Qed.

  #[export] Instance is_subalgebra_predicate_in_image_hom
    : IsSubalgebraPredicate B in_image_hom
    := BuildIsSubalgebraPredicate is_closed_under_ops_in_image_hom.
End in_image_hom.

(** The following section proves the first isomorphism theorem,
    [isomorphic_first_isomorphism] and the first identification
    theorem [id_first_isomorphism]. *)

Section first_isomorphism.
  Context
    `{Univalence} {σ} {A B : Algebra σ} `{IsHSetAlgebra B}
    (f : ∀ s, A s → B s) {hom : IsHomomorphism f}.

(** The homomorphism [def_first_isomorphism] is informally given by

<<
      def_first_isomorphism s (class_of _ x) := f s x.
>>
*)

  Definition def_first_isomorphism (s : Sort σ)
    : (A / cong_ker f) s → (B && in_image_hom f) s.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s0 : Sort σ, A s0 -> B s0
hom: IsHomomorphism f
s: Sort σ
(A / cong_ker f) s ->
(B && (λ (s0 : Sort σ) (y : B s0), in_image_hom f s0 y)) s
  Proof.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s0 : Sort σ, A s0 -> B s0
hom: IsHomomorphism f
s: Sort σ
(A / cong_ker f) s ->
(B && (λ (s0 : Sort σ) (y : B s0), in_image_hom f s0 y)) s
    refine (Quotient_rec (cong_ker f s) _ (λ x, (f s x; tr (x; idpath))) _).
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s0 : Sort σ, A s0 -> B s0
hom: IsHomomorphism f
s: Sort σ
forall a b : A s, cong_ker f s a b -> (f s a; tr (a; 1)) = (f s b; tr (b; 1))
    intros x y p.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s0 : Sort σ, A s0 -> B s0
hom: IsHomomorphism f
s: Sort σ
x, y: A s
p: cong_ker f s x y
(f s x; tr (x; 1)) = (f s y; tr (y; 1))
    by apply path_sigma_hprop.
  Defined.

  Lemma oppreserving_first_isomorphism {w : SymbolType σ}
    (α : Operation A w)
    (β : Operation B w)
    (γ : Operation (A / cong_ker f) w)
    (C : ClosedUnderOp B (in_image_hom f) β)
    (P : OpPreserving f α β)
    (G : ComputeOpQuotient A (cong_ker f) α γ)
    : OpPreserving def_first_isomorphism γ
        (op_subalgebra B (in_image_hom f) β C).
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
hom: IsHomomorphism f
w: SymbolType σ
α: Operation A w
β: Operation B w
γ: Operation (A / cong_ker f) w
C: ClosedUnderOp B (λ (s : Sort σ) (y : B s), in_image_hom f s y) β
P: OpPreserving f α β
G: ComputeOpQuotient A (cong_ker f) α γ
OpPreserving def_first_isomorphism γ
  (op_subalgebra B (λ (s : Sort σ) (y : B s), in_image_hom f s y) β C)
  Proof.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
hom: IsHomomorphism f
w: SymbolType σ
α: Operation A w
β: Operation B w
γ: Operation (A / cong_ker f) w
C: ClosedUnderOp B (λ (s : Sort σ) (y : B s), in_image_hom f s y) β
P: OpPreserving f α β
G: ComputeOpQuotient A (cong_ker f) α γ
OpPreserving def_first_isomorphism γ
  (op_subalgebra B (λ (s : Sort σ) (y : B s), in_image_hom f s y) β C)
    induction w.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
hom: IsHomomorphism f
t: Sort σ
α: Operation A (ne_list.one t)
β: Operation B (ne_list.one t)
γ: Operation (A / cong_ker f) (ne_list.one t)
C: ClosedUnderOp B (λ (s : Sort σ) (y : B s), in_image_hom f s y) β
P: OpPreserving f α β
G: ComputeOpQuotient A (cong_ker f) α γ
OpPreserving def_first_isomorphism γ
  (op_subalgebra B (λ (s : Sort σ) (y : B s), in_image_hom f s y) β C)
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
hom: IsHomomorphism f
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
α: Operation A (ne_list.cons t w)
β: Operation B (ne_list.cons t w)
γ: Operation (A / cong_ker f) (ne_list.cons t w)
C: ClosedUnderOp B (λ (s : Sort σ) (y : B s), in_image_hom f s y) β
P: OpPreserving f α β
G: ComputeOpQuotient A (cong_ker f) α γ
IHw: forall (α0 : Operation A w) (β0 : Operation B w)
(γ0 : Operation (A / cong_ker f) w)
(C0 : ClosedUnderOp B (λ (s : Sort σ) (y : B s), in_image_hom f s y) β0),
OpPreserving f α0 β0 ->
ComputeOpQuotient A (cong_ker f) α0 γ0 ->
OpPreserving def_first_isomorphism γ0
  (op_subalgebra B (λ (s : Sort σ) (y : B s), in_image_hom f s y) β0 C0)
OpPreserving def_first_isomorphism γ
  (op_subalgebra B (λ (s : Sort σ) (y : B s), in_image_hom f s y) β C)
    -
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
hom: IsHomomorphism f
t: Sort σ
α: Operation A (ne_list.one t)
β: Operation B (ne_list.one t)
γ: Operation (A / cong_ker f) (ne_list.one t)
C: ClosedUnderOp B (λ (s : Sort σ) (y : B s), in_image_hom f s y) β
P: OpPreserving f α β
G: ComputeOpQuotient A (cong_ker f) α γ
OpPreserving def_first_isomorphism γ
  (op_subalgebra B (λ (s : Sort σ) (y : B s), in_image_hom f s y) β C) apply path_sigma_hprop.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
hom: IsHomomorphism f
t: Sort σ
α: Operation A (ne_list.one t)
β: Operation B (ne_list.one t)
γ: Operation (A / cong_ker f) (ne_list.one t)
C: ClosedUnderOp B (λ (s : Sort σ) (y : B s), in_image_hom f s y) β
P: OpPreserving f α β
G: ComputeOpQuotient A (cong_ker f) α γ
(def_first_isomorphism t γ).1 =
(op_subalgebra B (λ (s : Sort σ) (y : B s), in_image_hom f s y) β C).1
      generalize dependent γ.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
hom: IsHomomorphism f
t: Sort σ
α: Operation A (ne_list.one t)
β: Operation B (ne_list.one t)
C: ClosedUnderOp B (λ (s : Sort σ) (y : B s), in_image_hom f s y) β
P: OpPreserving f α β
forall γ : Operation (A / cong_ker f) (ne_list.one t),
ComputeOpQuotient A (cong_ker f) α γ ->
(def_first_isomorphism t γ).1 =
(op_subalgebra B (λ (s : Sort σ) (y : B s), in_image_hom f s y) β C).1
      refine (Quotient_ind_hprop (cong_ker f t) _ _).
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
hom: IsHomomorphism f
t: Sort σ
α: Operation A (ne_list.one t)
β: Operation B (ne_list.one t)
C: ClosedUnderOp B (λ (s : Sort σ) (y : B s), in_image_hom f s y) β
P: OpPreserving f α β
forall a : A t,
ComputeOpQuotient A (cong_ker f) α (class_of (cong_ker f t) a) ->
(def_first_isomorphism t (class_of (cong_ker f t) a)).1 =
(op_subalgebra B (λ (s : Sort σ) (y : B s), in_image_hom f s y) β C).1 intros x G.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
hom: IsHomomorphism f
t: Sort σ
α: Operation A (ne_list.one t)
β: Operation B (ne_list.one t)
C: ClosedUnderOp B (λ (s : Sort σ) (y : B s), in_image_hom f s y) β
P: OpPreserving f α β
x: A t
G: ComputeOpQuotient A (cong_ker f) α (class_of (cong_ker f t) x)
(def_first_isomorphism t (class_of (cong_ker f t) x)).1 =
(op_subalgebra B (λ (s : Sort σ) (y : B s), in_image_hom f s y) β C).1
      destruct P.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
hom: IsHomomorphism f
t: Sort σ
α: Operation A (ne_list.one t)
C: ClosedUnderOp B (λ (s : Sort σ) (y : B s), in_image_hom f s y) (f t α)
x: A t
G: ComputeOpQuotient A (cong_ker f) α (class_of (cong_ker f t) x)
(def_first_isomorphism t (class_of (cong_ker f t) x)).1 =
(op_subalgebra B (λ (s : Sort σ) (y : B s), in_image_hom f s y) (f t α) C).1
      apply (related_quotient_paths (cong_ker f t) _ _ (G tt)).
    -
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
hom: IsHomomorphism f
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
α: Operation A (ne_list.cons t w)
β: Operation B (ne_list.cons t w)
γ: Operation (A / cong_ker f) (ne_list.cons t w)
C: ClosedUnderOp B (λ (s : Sort σ) (y : B s), in_image_hom f s y) β
P: OpPreserving f α β
G: ComputeOpQuotient A (cong_ker f) α γ
IHw: forall (α0 : Operation A w) (β0 : Operation B w)
(γ0 : Operation (A / cong_ker f) w)
(C0 : ClosedUnderOp B (λ (s : Sort σ) (y : B s), in_image_hom f s y) β0),
OpPreserving f α0 β0 ->
ComputeOpQuotient A (cong_ker f) α0 γ0 ->
OpPreserving def_first_isomorphism γ0
  (op_subalgebra B (λ (s : Sort σ) (y : B s), in_image_hom f s y) β0 C0)
OpPreserving def_first_isomorphism γ
  (op_subalgebra B (λ (s : Sort σ) (y : B s), in_image_hom f s y) β C) refine (Quotient_ind_hprop (cong_ker f t) _ _).
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
hom: IsHomomorphism f
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
α: Operation A (ne_list.cons t w)
β: Operation B (ne_list.cons t w)
γ: Operation (A / cong_ker f) (ne_list.cons t w)
C: ClosedUnderOp B (λ (s : Sort σ) (y : B s), in_image_hom f s y) β
P: OpPreserving f α β
G: ComputeOpQuotient A (cong_ker f) α γ
IHw: forall (α0 : Operation A w) (β0 : Operation B w)
(γ0 : Operation (A / cong_ker f) w)
(C0 : ClosedUnderOp B (λ (s : Sort σ) (y : B s), in_image_hom f s y) β0),
OpPreserving f α0 β0 ->
ComputeOpQuotient A (cong_ker f) α0 γ0 ->
OpPreserving def_first_isomorphism γ0
  (op_subalgebra B (λ (s : Sort σ) (y : B s), in_image_hom f s y) β0 C0)
forall a : A t,
(fix OpPreserving (w0 : SymbolType σ) :
     Operation (A / cong_ker f) w0 ->
     Operation (B && (λ (s : Sort σ) (y : B s), in_image_hom f s y)) w0 ->
     Type :=
   match
     w0 as w1
     return
       (Operation (A / cong_ker f) w1 ->
        Operation (B && (λ (s : Sort σ) (y : B s), in_image_hom f s y)) w1 ->
        Type)
   with
   | ne_list.one s =>
       λ (α0 : Operation (A / cong_ker f) (ne_list.one s))
       (β0 : Operation
               (B && (λ (s0 : Sort σ) (y : B s0), in_image_hom f s0 y))
               (ne_list.one s)),
       def_first_isomorphism s α0 = β0
   | ne_list.cons s y =>
       λ (α0 : Operation (A / cong_ker f) (ne_list.cons s y))
       (β0 : Operation
               (B && (λ (s0 : Sort σ) (y0 : B s0), in_image_hom f s0 y0))
               (ne_list.cons s y)),
       forall x : (A / cong_ker f) s,
       OpPreserving y (α0 x) (β0 (def_first_isomorphism s x))
   end)
  w (γ (class_of (cong_ker f t) a))
  (op_subalgebra B (λ (s : Sort σ) (y : B s), in_image_hom f s y) β C
     (def_first_isomorphism t (class_of (cong_ker f t) a))) intro x.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
hom: IsHomomorphism f
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
α: Operation A (ne_list.cons t w)
β: Operation B (ne_list.cons t w)
γ: Operation (A / cong_ker f) (ne_list.cons t w)
C: ClosedUnderOp B (λ (s : Sort σ) (y : B s), in_image_hom f s y) β
P: OpPreserving f α β
G: ComputeOpQuotient A (cong_ker f) α γ
IHw: forall (α0 : Operation A w) (β0 : Operation B w)
(γ0 : Operation (A / cong_ker f) w)
(C0 : ClosedUnderOp B (λ (s : Sort σ) (y : B s), in_image_hom f s y) β0),
OpPreserving f α0 β0 ->
ComputeOpQuotient A (cong_ker f) α0 γ0 ->
OpPreserving def_first_isomorphism γ0
  (op_subalgebra B (λ (s : Sort σ) (y : B s), in_image_hom f s y) β0 C0)
x: A t
(fix OpPreserving (w0 : SymbolType σ) :
     Operation (A / cong_ker f) w0 ->
     Operation (B && (λ (s : Sort σ) (y : B s), in_image_hom f s y)) w0 ->
     Type :=
   match
     w0 as w1
     return
       (Operation (A / cong_ker f) w1 ->
        Operation (B && (λ (s : Sort σ) (y : B s), in_image_hom f s y)) w1 ->
        Type)
   with
   | ne_list.one s =>
       λ (α0 : Operation (A / cong_ker f) (ne_list.one s))
       (β0 : Operation
               (B && (λ (s0 : Sort σ) (y : B s0), in_image_hom f s0 y))
               (ne_list.one s)),
       def_first_isomorphism s α0 = β0
   | ne_list.cons s y =>
       λ (α0 : Operation (A / cong_ker f) (ne_list.cons s y))
       (β0 : Operation
               (B && (λ (s0 : Sort σ) (y0 : B s0), in_image_hom f s0 y0))
               (ne_list.cons s y)),
       forall x0 : (A / cong_ker f) s,
       OpPreserving y (α0 x0) (β0 (def_first_isomorphism s x0))
   end)
  w (γ (class_of (cong_ker f t) x))
  (op_subalgebra B (λ (s : Sort σ) (y : B s), in_image_hom f s y) β C
     (def_first_isomorphism t (class_of (cong_ker f t) x)))
      apply (IHw (α x) (β (f t x)) (γ (class_of _ x))).
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
hom: IsHomomorphism f
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
α: Operation A (ne_list.cons t w)
β: Operation B (ne_list.cons t w)
γ: Operation (A / cong_ker f) (ne_list.cons t w)
C: ClosedUnderOp B (λ (s : Sort σ) (y : B s), in_image_hom f s y) β
P: OpPreserving f α β
G: ComputeOpQuotient A (cong_ker f) α γ
IHw: forall (α0 : Operation A w) (β0 : Operation B w)
(γ0 : Operation (A / cong_ker f) w)
(C0 : ClosedUnderOp B (λ (s : Sort σ) (y : B s), in_image_hom f s y) β0),
OpPreserving f α0 β0 ->
ComputeOpQuotient A (cong_ker f) α0 γ0 ->
OpPreserving def_first_isomorphism γ0
  (op_subalgebra B (λ (s : Sort σ) (y : B s), in_image_hom f s y) β0 C0)
x: A t
OpPreserving f (α x) (β (f t x))
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
hom: IsHomomorphism f
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
α: Operation A (ne_list.cons t w)
β: Operation B (ne_list.cons t w)
γ: Operation (A / cong_ker f) (ne_list.cons t w)
C: ClosedUnderOp B (λ (s : Sort σ) (y : B s), in_image_hom f s y) β
P: OpPreserving f α β
G: ComputeOpQuotient A (cong_ker f) α γ
IHw: forall (α0 : Operation A w) (β0 : Operation B w)
(γ0 : Operation (A / cong_ker f) w)
(C0 : ClosedUnderOp B (λ (s : Sort σ) (y : B s), in_image_hom f s y) β0),
OpPreserving f α0 β0 ->
ComputeOpQuotient A (cong_ker f) α0 γ0 ->
OpPreserving def_first_isomorphism γ0
  (op_subalgebra B (λ (s : Sort σ) (y : B s), in_image_hom f s y) β0 C0)
x: A t
ComputeOpQuotient A (cong_ker f) (α x) (γ (class_of (cong_ker f t) x))
      +
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
hom: IsHomomorphism f
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
α: Operation A (ne_list.cons t w)
β: Operation B (ne_list.cons t w)
γ: Operation (A / cong_ker f) (ne_list.cons t w)
C: ClosedUnderOp B (λ (s : Sort σ) (y : B s), in_image_hom f s y) β
P: OpPreserving f α β
G: ComputeOpQuotient A (cong_ker f) α γ
IHw: forall (α0 : Operation A w) (β0 : Operation B w)
(γ0 : Operation (A / cong_ker f) w)
(C0 : ClosedUnderOp B (λ (s : Sort σ) (y : B s), in_image_hom f s y) β0),
OpPreserving f α0 β0 ->
ComputeOpQuotient A (cong_ker f) α0 γ0 ->
OpPreserving def_first_isomorphism γ0
  (op_subalgebra B (λ (s : Sort σ) (y : B s), in_image_hom f s y) β0 C0)
x: A t
OpPreserving f (α x) (β (f t x)) exact (P x).
      +
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
hom: IsHomomorphism f
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
α: Operation A (ne_list.cons t w)
β: Operation B (ne_list.cons t w)
γ: Operation (A / cong_ker f) (ne_list.cons t w)
C: ClosedUnderOp B (λ (s : Sort σ) (y : B s), in_image_hom f s y) β
P: OpPreserving f α β
G: ComputeOpQuotient A (cong_ker f) α γ
IHw: forall (α0 : Operation A w) (β0 : Operation B w)
(γ0 : Operation (A / cong_ker f) w)
(C0 : ClosedUnderOp B (λ (s : Sort σ) (y : B s), in_image_hom f s y) β0),
OpPreserving f α0 β0 ->
ComputeOpQuotient A (cong_ker f) α0 γ0 ->
OpPreserving def_first_isomorphism γ0
  (op_subalgebra B (λ (s : Sort σ) (y : B s), in_image_hom f s y) β0 C0)
x: A t
ComputeOpQuotient A (cong_ker f) (α x) (γ (class_of (cong_ker f t) x)) intro a.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
hom: IsHomomorphism f
t: Sort σ
w: ne_list.notations.ne_list (Sort σ)
α: Operation A (ne_list.cons t w)
β: Operation B (ne_list.cons t w)
γ: Operation (A / cong_ker f) (ne_list.cons t w)
C: ClosedUnderOp B (λ (s : Sort σ) (y : B s), in_image_hom f s y) β
P: OpPreserving f α β
G: ComputeOpQuotient A (cong_ker f) α γ
IHw: forall (α0 : Operation A w) (β0 : Operation B w)
(γ0 : Operation (A / cong_ker f) w)
(C0 : ClosedUnderOp B (λ (s : Sort σ) (y : B s), in_image_hom f s y) β0),
OpPreserving f α0 β0 ->
ComputeOpQuotient A (cong_ker f) α0 γ0 ->
OpPreserving def_first_isomorphism γ0
  (op_subalgebra B (λ (s : Sort σ) (y : B s), in_image_hom f s y) β0 C0)
x: A t
a: FamilyProd A (dom_symboltype w)
ap_operation (γ (class_of (cong_ker f t) x))
  (map_family_prod (λ s : Sort σ, class_of (cong_ker f s)) a) =
class_of (cong_ker f (cod_symboltype w)) (ap_operation (α x) a) exact (G (x,a)).
  Qed.

(* Leave [is_homomorphism_first_isomorphism] opaque because
   [IsHomomorphism] is an hprop when [B] is a set algebra. *)

  #[export] Instance is_homomorphism_first_isomorphism
    : IsHomomorphism def_first_isomorphism.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
hom: IsHomomorphism f
IsHomomorphism def_first_isomorphism
  Proof.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
hom: IsHomomorphism f
IsHomomorphism def_first_isomorphism
    intro u.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
hom: IsHomomorphism f
u: Symbol σ
OpPreserving def_first_isomorphism u.#(A / cong_ker f)
  u.#(B && (λ (s : Sort σ) (y : B s), in_image_hom f s y)) apply (oppreserving_first_isomorphism u.#A).
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
hom: IsHomomorphism f
u: Symbol σ
OpPreserving f u.#A u.#B
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
hom: IsHomomorphism f
u: Symbol σ
ComputeOpQuotient A (cong_ker f) u.#A u.#(A / cong_ker f)
    -
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
hom: IsHomomorphism f
u: Symbol σ
OpPreserving f u.#A u.#B apply hom.
    -
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
hom: IsHomomorphism f
u: Symbol σ
ComputeOpQuotient A (cong_ker f) u.#A u.#(A / cong_ker f) apply compute_op_quotient.
  Qed.

  Definition hom_first_isomorphism
    : Homomorphism (A / cong_ker f) (B && in_image_hom f)
    := BuildHomomorphism def_first_isomorphism.

  #[export] Instance embedding_first_isomorphism (s : Sort σ)
    : IsEmbedding (hom_first_isomorphism s).
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s0 : Sort σ, A s0 -> B s0
hom: IsHomomorphism f
s: Sort σ
IsEmbedding (hom_first_isomorphism s)
  Proof.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s0 : Sort σ, A s0 -> B s0
hom: IsHomomorphism f
s: Sort σ
IsEmbedding (hom_first_isomorphism s)
    apply isembedding_isinj_hset.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s0 : Sort σ, A s0 -> B s0
hom: IsHomomorphism f
s: Sort σ
IsInjective (hom_first_isomorphism s)
    refine (Quotient_ind_hprop (cong_ker f s) _ _).
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s0 : Sort σ, A s0 -> B s0
hom: IsHomomorphism f
s: Sort σ
forall (a : A s) (y : (A / cong_ker f) s),
hom_first_isomorphism s (class_of (cong_ker f s) a) =
hom_first_isomorphism s y -> class_of (cong_ker f s) a = y intro x.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s0 : Sort σ, A s0 -> B s0
hom: IsHomomorphism f
s: Sort σ
x: A s
forall y : (A / cong_ker f) s,
hom_first_isomorphism s (class_of (cong_ker f s) x) =
hom_first_isomorphism s y -> class_of (cong_ker f s) x = y
    refine (Quotient_ind_hprop (cong_ker f s) _ _).
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s0 : Sort σ, A s0 -> B s0
hom: IsHomomorphism f
s: Sort σ
x: A s
forall a : A s,
hom_first_isomorphism s (class_of (cong_ker f s) x) =
hom_first_isomorphism s (class_of (cong_ker f s) a) ->
class_of (cong_ker f s) x = class_of (cong_ker f s) a intros y p.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s0 : Sort σ, A s0 -> B s0
hom: IsHomomorphism f
s: Sort σ
x, y: A s
p: hom_first_isomorphism s (class_of (cong_ker f s) x) =
hom_first_isomorphism s (class_of (cong_ker f s) y)
class_of (cong_ker f s) x = class_of (cong_ker f s) y
    apply qglue.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s0 : Sort σ, A s0 -> B s0
hom: IsHomomorphism f
s: Sort σ
x, y: A s
p: hom_first_isomorphism s (class_of (cong_ker f s) x) =
hom_first_isomorphism s (class_of (cong_ker f s) y)
cong_ker f s x y
    exact (p..1).
  Qed.

  #[export] Instance surjection_first_isomorphism (s : Sort σ)
    : IsSurjection (hom_first_isomorphism s).
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s0 : Sort σ, A s0 -> B s0
hom: IsHomomorphism f
s: Sort σ
ReflectiveSubuniverse.IsConnMap (Tr (-1)) (hom_first_isomorphism s)
  Proof.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s0 : Sort σ, A s0 -> B s0
hom: IsHomomorphism f
s: Sort σ
ReflectiveSubuniverse.IsConnMap (Tr (-1)) (hom_first_isomorphism s)
    apply BuildIsSurjection.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s0 : Sort σ, A s0 -> B s0
hom: IsHomomorphism f
s: Sort σ
forall b : (B && (λ (s0 : Sort σ) (y : B s0), in_image_hom f s0 y)) s,
merely (hfiber (hom_first_isomorphism s) b)
    intros [x M].
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s0 : Sort σ, A s0 -> B s0
hom: IsHomomorphism f
s: Sort σ
x: B s
M: in_image_hom f s x
merely (hfiber (hom_first_isomorphism s) (x; M))
    refine (Trunc_rec _ M).
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s0 : Sort σ, A s0 -> B s0
hom: IsHomomorphism f
s: Sort σ
x: B s
M: in_image_hom f s x
hfiber (f s) x -> merely (hfiber (hom_first_isomorphism s) (x; M)) intros [y Y].
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s0 : Sort σ, A s0 -> B s0
hom: IsHomomorphism f
s: Sort σ
x: B s
M: in_image_hom f s x
y: A s
Y: f s y = x
merely (hfiber (hom_first_isomorphism s) (x; M))
    apply tr.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s0 : Sort σ, A s0 -> B s0
hom: IsHomomorphism f
s: Sort σ
x: B s
M: in_image_hom f s x
y: A s
Y: f s y = x
hfiber (hom_first_isomorphism s) (x; M)
    exists (class_of _ y).
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s0 : Sort σ, A s0 -> B s0
hom: IsHomomorphism f
s: Sort σ
x: B s
M: in_image_hom f s x
y: A s
Y: f s y = x
hom_first_isomorphism s (class_of (cong_ker f s) y) = (x; M)
    by apply path_sigma_hprop.
  Qed.

  #[export] Instance is_isomorphism_first_isomorphism
    : IsIsomorphism hom_first_isomorphism.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
hom: IsHomomorphism f
IsIsomorphism hom_first_isomorphism
  Proof.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
hom: IsHomomorphism f
IsIsomorphism hom_first_isomorphism
    intro s.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s0 : Sort σ, A s0 -> B s0
hom: IsHomomorphism f
s: Sort σ
IsEquiv (hom_first_isomorphism s) apply isequiv_surj_emb; exact _.
  Qed.

  Theorem isomorphic_first_isomorphism
    : A / cong_ker f ≅ B && in_image_hom f.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
hom: IsHomomorphism f
A / cong_ker f ≅ B && (λ (s : Sort σ) (y : B s), in_image_hom f s y)
  Proof.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
hom: IsHomomorphism f
A / cong_ker f ≅ B && (λ (s : Sort σ) (y : B s), in_image_hom f s y)
    exact (BuildIsomorphic def_first_isomorphism).
  Defined.

(* The first identification theorem [id_first_isomorphism] is an
   h-prop, so we can leave it opaque. *)

  Corollary id_first_isomorphism : A / cong_ker f = B && in_image_hom f.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
hom: IsHomomorphism f
A / cong_ker f = B && (λ (s : Sort σ) (y : B s), in_image_hom f s y)
  Proof.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
hom: IsHomomorphism f
A / cong_ker f = B && (λ (s : Sort σ) (y : B s), in_image_hom f s y)
    exact (id_isomorphic isomorphic_first_isomorphism).
  Qed.
End first_isomorphism.

(** The next section gives a specialization of the first isomorphism
    theorem, where the homomorphism is surjective. *)

Section first_isomorphism_surjection.
  Context
    `{Univalence} {σ} {A B : Algebra σ} `{IsHSetAlgebra B}
    (f : ∀ s, A s → B s) `{!IsHomomorphism f} {S : ∀ s, IsSurjection (f s)}.

  #[export] Instance is_isomorphism_inc_first_isomorphism_surjection
    : IsIsomorphism (hom_inc_subalgebra B (in_image_hom f)).
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
S: forall s : Sort σ, ReflectiveSubuniverse.IsConnMap (Tr (-1)) (f s)
IsIsomorphism
  (hom_inc_subalgebra B (λ (s : Sort σ) (y : B s), in_image_hom f s y))
  Proof.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
S: forall s : Sort σ, ReflectiveSubuniverse.IsConnMap (Tr (-1)) (f s)
IsIsomorphism
  (hom_inc_subalgebra B (λ (s : Sort σ) (y : B s), in_image_hom f s y))
    apply is_isomorphism_inc_improper_subalgebra.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
S: forall s : Sort σ, ReflectiveSubuniverse.IsConnMap (Tr (-1)) (f s)
forall (s : Sort σ) (x : B s), in_image_hom f s x
    intros s x; cbn.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s0 : Sort σ, A s0 -> B s0
IsHomomorphism0: IsHomomorphism f
S: forall s0 : Sort σ, ReflectiveSubuniverse.IsConnMap (Tr (-1)) (f s0)
s: Sort σ
x: B s
Trunc (-1) (hfiber (f s) x)
    apply center, S.
  Qed.

(** The homomorphism [hom_first_isomorphism_surjection] is the
    composition of two isomorphisms, so it is an isomorphism. *)

  Definition hom_first_isomorphism_surjection
    : Homomorphism (A / cong_ker f) B
    := hom_compose
          (hom_inc_subalgebra B (in_image_hom f))
          (hom_first_isomorphism f).

  Theorem isomorphic_first_isomorphism_surjection : A / cong_ker f ≅ B.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
S: forall s : Sort σ, ReflectiveSubuniverse.IsConnMap (Tr (-1)) (f s)
A / cong_ker f ≅ B
  Proof.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
S: forall s : Sort σ, ReflectiveSubuniverse.IsConnMap (Tr (-1)) (f s)
A / cong_ker f ≅ B
    exact (BuildIsomorphic hom_first_isomorphism_surjection).
  Defined.

  Corollary id_first_isomorphism_surjection : (A / cong_ker f) = B.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
S: forall s : Sort σ, ReflectiveSubuniverse.IsConnMap (Tr (-1)) (f s)
A / cong_ker f = B
  Proof.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
S: forall s : Sort σ, ReflectiveSubuniverse.IsConnMap (Tr (-1)) (f s)
A / cong_ker f = B
    exact (id_isomorphic isomorphic_first_isomorphism_surjection).
  Qed.
End first_isomorphism_surjection.

(** The next section specializes the first isomorphism theorem to the
    case where the homomorphism is injective. It proves that an
    injective homomorphism is an isomorphism between its domain
    and its image. *)

Section first_isomorphism_inj.
  Context
    `{Univalence} {σ} {A B : Algebra σ} `{IsHSetAlgebra B}
    (f : ∀ s, A s → B s) `{!IsHomomorphism f} (inj : ∀ s, IsInjective (f s)).

  #[export] Instance is_isomorphism_quotient_first_isomorphism_inj
    : IsIsomorphism (hom_quotient (cong_ker f)).
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
inj: forall s : Sort σ, IsInjective (f s)
IsIsomorphism (hom_quotient (cong_ker f))
  Proof.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
inj: forall s : Sort σ, IsInjective (f s)
IsIsomorphism (hom_quotient (cong_ker f))
    apply is_isomorphism_quotient.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
inj: forall s : Sort σ, IsInjective (f s)
forall (s : Sort σ) (x y : A s), cong_ker f s x y -> x = y intros s x y p.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s0 : Sort σ, A s0 -> B s0
IsHomomorphism0: IsHomomorphism f
inj: forall s0 : Sort σ, IsInjective (f s0)
s: Sort σ
x, y: A s
p: cong_ker f s x y
x = y apply inj, p.
  Qed.

(** The homomorphism [hom_first_isomorphism_inj] is the
    composition of two isomorphisms, so it is an isomorphism. *)

  Definition hom_first_isomorphism_inj
    : Homomorphism A (B && in_image_hom f)
    := hom_compose
          (hom_first_isomorphism f)
          (hom_quotient (cong_ker f)).

  Definition isomorphic_first_isomorphism_inj : A ≅ B && in_image_hom f
    := BuildIsomorphic hom_first_isomorphism_inj.

  Definition id_first_isomorphism_inj : A = B && in_image_hom f
    := id_isomorphic isomorphic_first_isomorphism_inj.

End first_isomorphism_inj.