(** 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.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

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 s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
s: Sort σ
EquivRel (cong_ker s)
  Proof.
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
s: Sort σ
EquivRel (cong_ker s)
    repeat constructor.
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
s: Sort σ
Symmetric (cong_ker s)
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
s: Sort σ
Transitive (cong_ker s)
    -
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
s: Sort σ
Symmetric (cong_ker s) intros x y.
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
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 s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
s: Sort σ
Transitive (cong_ker s) intros x y z.
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
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 (β : Operation B w)
(a b : FamilyProd A (dom_symboltype w)),
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)
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 (β : Operation B w)
(a b : FamilyProd A (dom_symboltype w)),
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)
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 (β : Operation B w)
(a b : FamilyProd A (dom_symboltype w)),
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)
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 (β : Operation B w)
(a b : FamilyProd A (dom_symboltype w)),
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)
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 (β : Operation B w)
(a b : FamilyProd A (dom_symboltype w)),
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)
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 (α : Operation A w) (β : Operation B w),
OpPreserving f α β ->
ClosedUnderOp B (λ (s : Sort σ) (y : B s), in_image_hom s y) β
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 (α : Operation A w) (β : Operation B w),
OpPreserving f α β ->
ClosedUnderOp B (λ (s : Sort σ) (y : B s), in_image_hom s y) β
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 (α : Operation A w) (β : Operation B w),
OpPreserving f α β ->
ClosedUnderOp B (λ (s : Sort σ) (y : B s), in_image_hom s y) β
y: B t
in_image_hom t y ->
ClosedUnderOp B
  (λ (s : Sort σ) (y : B s), in_image_hom s y) (β 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 (α : Operation A w) (β : Operation B w),
OpPreserving f α β ->
ClosedUnderOp B (λ (s : Sort σ) (y : B s), in_image_hom s y) β
y: B t
hfiber (f t) y ->
ClosedUnderOp B
  (λ (s : Sort σ) (y : B s), in_image_hom s y) (β 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 (α : Operation A w) (β : Operation B w),
OpPreserving f α β ->
ClosedUnderOp B (λ (s : Sort σ) (y : B s), in_image_hom s y) β
y: B t
x: A t
p: f t x = y
ClosedUnderOp B
  (λ (s : Sort σ) (y : B s), in_image_hom s y) (β 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 (α : Operation A w) (β : Operation B w),
OpPreserving f α β ->
ClosedUnderOp B (λ (s : Sort σ) (y : B s), in_image_hom s y) β
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 s : Sort σ, A s -> B s
hom: IsHomomorphism f
s: Sort σ
(A / cong_ker f) s ->
(B && (λ (s : Sort σ) (y : B s), in_image_hom f s y))
  s
  Proof.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
hom: IsHomomorphism f
s: Sort σ
(A / cong_ker f) s ->
(B && (λ (s : Sort σ) (y : B s), in_image_hom f s 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 s : Sort σ, A s -> B s
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 s : Sort σ, A s -> B s
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 (α : 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) β),
OpPreserving f α β ->
ComputeOpQuotient A (cong_ker f) α γ ->
OpPreserving def_first_isomorphism γ
  (op_subalgebra B
     (λ (s : Sort σ) 
      (y : B s), in_image_hom f s y) β C)
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 (α : 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) β),
OpPreserving f α β ->
ComputeOpQuotient A (cong_ker f) α γ ->
OpPreserving def_first_isomorphism γ
  (op_subalgebra B
     (λ (s : Sort σ) 
      (y : B s), in_image_hom f s y) β C)
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 (α : 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) β),
OpPreserving f α β ->
ComputeOpQuotient A (cong_ker f) α γ ->
OpPreserving def_first_isomorphism γ
  (op_subalgebra B
     (λ (s : Sort σ) 
      (y : B s), in_image_hom f s y) β C)
forall a : A t,
(fix OpPreserving (w : SymbolType σ) :
     Operation (A / cong_ker f) w ->
     Operation
       (B &&
        (λ (s : Sort σ) (y : B s), in_image_hom f s y))
       w -> Type :=
   match
     w as w0
     return
       (Operation (A / cong_ker f) w0 ->
        Operation
          (B &&
           (λ (s : Sort σ) (y : B s),
            in_image_hom f s y)) w0 -> Type)
   with
   | ne_list.one s =>
       λ
       (α : Operation (A / cong_ker f) (ne_list.one s))
       (β : Operation
              (B &&
               (λ (s0 : Sort σ) (y : B s0),
                in_image_hom f s0 y)) (ne_list.one s)),
       def_first_isomorphism s α = β
   | ne_list.cons s y =>
       λ
       (α : Operation (A / cong_ker f)
              (ne_list.cons s y))
       (β : 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 (α x)
         (β (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 (α : 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) β),
OpPreserving f α β ->
ComputeOpQuotient A (cong_ker f) α γ ->
OpPreserving def_first_isomorphism γ
  (op_subalgebra B
     (λ (s : Sort σ) 
      (y : B s), in_image_hom f s y) β C)
x: A t
(fix OpPreserving (w : SymbolType σ) :
     Operation (A / cong_ker f) w ->
     Operation
       (B &&
        (λ (s : Sort σ) (y : B s), in_image_hom f s y))
       w -> Type :=
   match
     w as w0
     return
       (Operation (A / cong_ker f) w0 ->
        Operation
          (B &&
           (λ (s : Sort σ) (y : B s),
            in_image_hom f s y)) w0 -> Type)
   with
   | ne_list.one s =>
       λ
       (α : Operation (A / cong_ker f) (ne_list.one s))
       (β : Operation
              (B &&
               (λ (s0 : Sort σ) (y : B s0),
                in_image_hom f s0 y)) (ne_list.one s)),
       def_first_isomorphism s α = β
   | ne_list.cons s y =>
       λ
       (α : Operation (A / cong_ker f)
              (ne_list.cons s y))
       (β : 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 (α x)
         (β (def_first_isomorphism s x))
   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 (α : 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) β),
OpPreserving f α β ->
ComputeOpQuotient A (cong_ker f) α γ ->
OpPreserving def_first_isomorphism γ
  (op_subalgebra B
     (λ (s : Sort σ) 
      (y : B s), in_image_hom f s y) β C)
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 (α : 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) β),
OpPreserving f α β ->
ComputeOpQuotient A (cong_ker f) α γ ->
OpPreserving def_first_isomorphism γ
  (op_subalgebra B
     (λ (s : Sort σ) 
      (y : B s), in_image_hom f s y) β C)
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 (α : 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) β),
OpPreserving f α β ->
ComputeOpQuotient A (cong_ker f) α γ ->
OpPreserving def_first_isomorphism γ
  (op_subalgebra B
     (λ (s : Sort σ) 
      (y : B s), in_image_hom f s y) β C)
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 (α : 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) β),
OpPreserving f α β ->
ComputeOpQuotient A (cong_ker f) α γ ->
OpPreserving def_first_isomorphism γ
  (op_subalgebra B
     (λ (s : Sort σ) 
      (y : B s), in_image_hom f s y) β C)
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 (α : 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) β),
OpPreserving f α β ->
ComputeOpQuotient A (cong_ker f) α γ ->
OpPreserving def_first_isomorphism γ
  (op_subalgebra B
     (λ (s : Sort σ) 
      (y : B s), in_image_hom f s y) β C)
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 s : Sort σ, A s -> B s
hom: IsHomomorphism f
s: Sort σ
IsEmbedding (hom_first_isomorphism s)
  Proof.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
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 s : Sort σ, A s -> B s
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 s : Sort σ, A s -> B s
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 s : Sort σ, A s -> B s
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 s : Sort σ, A s -> B s
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 s : Sort σ, A s -> B s
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 s : Sort σ, A s -> B s
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 s : Sort σ, A s -> B s
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 s : Sort σ, A s -> B s
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 s : Sort σ, A s -> B s
hom: IsHomomorphism f
s: Sort σ
forall
b : (B &&
     (λ (s : Sort σ) (y : B s), in_image_hom f s y)) s,
merely (hfiber (hom_first_isomorphism s) b)
    intros [x M].
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f: forall s : Sort σ, A s -> B s
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 s : Sort σ, A s -> B s
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 s : Sort σ, A s -> B s
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 s : Sort σ, A s -> B s
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 s : Sort σ, A s -> B s
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 s : Sort σ, A s -> B s
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 s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
S: forall s : Sort σ,
ReflectiveSubuniverse.IsConnMap (Tr (-1)) (f s)
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 s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
inj: forall s : Sort σ, IsInjective (f s)
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.