(** This file implements [IsHomomorphism] and [IsIsomorphism].
    It develops basic algebra homomorphisms and isomorphims. The main
    theorem in this file is the [path_isomorphism] theorem, which
    states that there is a path between isomorphic algebras. *)

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

Require Import
  HoTT.Types
  HoTT.Tactics.

Import algebra_notations ne_list.notations.

Section is_homomorphism.
  Context {σ} {A B : Algebra σ} (f : ∀ (s : Sort σ), A s → B s).

(** The family of functions [f] above is [OpPreserving α β] with
    respect to operations [α : A s1 → A s2 → ... → A sn → A t] and
    [β : B s1 → B s2 → ... → B sn → B t] if

<<
      f t (α x1 x2 ... xn) = β (f s1 x1) (f s2 x2) ... (f sn xn)
>>
*)

  Fixpoint OpPreserving {w : SymbolType σ}
    : Operation A w → Operation B w → Type
    := match w with
       | [:s:] => λ α β, f s α = β
       | s ::: y => λ α β, ∀ (x : A s), OpPreserving (α x) (β (f s x))
       end.

  #[export] Instance trunc_oppreserving `{Funext} {n : trunc_index}
    `{!IsTruncAlgebra n.+1 B} {w : SymbolType σ}
    (α : Operation A w) (β : Operation B w)
    : IsTrunc n (OpPreserving α β).
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
H: Funext
n: trunc_index
IsTruncAlgebra0: IsTruncAlgebra n.+1 B
w: SymbolType σ
α: Operation A w
β: Operation B w
IsTrunc n (OpPreserving α β)
  Proof.
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
H: Funext
n: trunc_index
IsTruncAlgebra0: IsTruncAlgebra n.+1 B
w: SymbolType σ
α: Operation A w
β: Operation B w
IsTrunc n (OpPreserving α β)
    induction w; exact _.
  Qed.

(** The family of functions [f : ∀ (s : Sort σ), A s → B s] above is
    a homomorphism if for each function symbol [u : Symbol σ], it is
    [OpPreserving u.#A u.#B] with respect to the algebra
    operations [u.#A] and [u.#B] corresponding to [u]. *)

  Class IsHomomorphism : Type
    := oppreserving_hom : ∀ (u : Symbol σ), OpPreserving u.#A u.#B.

  #[export] Instance trunc_is_homomorphism `{Funext} {n : trunc_index}
    `{!IsTruncAlgebra n.+1 B}
    : IsTrunc n IsHomomorphism.
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
H: Funext
n: trunc_index
IsTruncAlgebra0: IsTruncAlgebra n.+1 B
IsTrunc n IsHomomorphism
  Proof.
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
H: Funext
n: trunc_index
IsTruncAlgebra0: IsTruncAlgebra n.+1 B
IsTrunc n IsHomomorphism
    apply istrunc_forall.
  Qed.
End is_homomorphism.

Record Homomorphism {σ} {A B : Algebra σ} : Type := BuildHomomorphism
  { def_hom : ∀ (s : Sort σ), A s → B s
  ; is_homomorphism_hom :: IsHomomorphism def_hom }.

Arguments Homomorphism {σ}.

Arguments BuildHomomorphism {σ A B} def_hom {is_homomorphism_hom}.

(** We the implicit coercion from [Homomorphism A B] to the family
    of functions [∀ s, A s → B s]. *)
Global Coercion def_hom : Homomorphism >-> Funclass.

Lemma apD10_homomorphism {σ} {A B : Algebra σ} {f g : Homomorphism A B}
  : f = g → ∀ s, f s == g s.
σ: Signature
A, B: Algebra σ
f, g: Homomorphism A B
f = g -> forall s : Sort σ, f s == g s
Proof.
σ: Signature
A, B: Algebra σ
f, g: Homomorphism A B
f = g -> forall s : Sort σ, f s == g s
  intro p.
σ: Signature
A, B: Algebra σ
f, g: Homomorphism A B
p: f = g
forall s : Sort σ, f s == g s by destruct p.
Defined.

Definition SigHomomorphism {σ} (A B : Algebra σ) : Type :=
  { def_hom : ∀ s, A s → B s | IsHomomorphism def_hom }.

Lemma issig_homomorphism {σ} (A B : Algebra σ)
  : SigHomomorphism A B <~> Homomorphism A B.
σ: Signature
A, B: Algebra σ
SigHomomorphism A B <~> Homomorphism A B
Proof.
σ: Signature
A, B: Algebra σ
SigHomomorphism A B <~> Homomorphism A B
  issig.
Defined.

Instance trunc_homomorphism `{Funext} {σ} {A B : Algebra σ}
  {n : trunc_index} `{!IsTruncAlgebra n B}
  : IsTrunc n (Homomorphism A B).
H: Funext
σ: Signature
A, B: Algebra σ
n: trunc_index
IsTruncAlgebra0: IsTruncAlgebra n B
IsTrunc n (Homomorphism A B)
Proof.
H: Funext
σ: Signature
A, B: Algebra σ
n: trunc_index
IsTruncAlgebra0: IsTruncAlgebra n B
IsTrunc n (Homomorphism A B)
  apply (istrunc_equiv_istrunc _ (issig_homomorphism A B)).
Qed.

(** To find a path between two homomorphisms [f g : Homomorphism A B]
    it suffices to find a path between the defining families of
    functions and the [is_homomorphism_hom] witnesses. *)

Lemma path_homomorphism {σ} {A B : Algebra σ} (f g : Homomorphism A B)
  (p : def_hom f = def_hom g)
  (q : p#(is_homomorphism_hom f) = is_homomorphism_hom g)
  : f = g.
σ: Signature
A, B: Algebra σ
f, g: Homomorphism A B
p: f = g
q: transport IsHomomorphism p (is_homomorphism_hom f) =
is_homomorphism_hom g
f = g
Proof.
σ: Signature
A, B: Algebra σ
f, g: Homomorphism A B
p: f = g
q: transport IsHomomorphism p (is_homomorphism_hom f) =
is_homomorphism_hom g
f = g
  destruct f, g.
σ: Signature
A, B: Algebra σ
def_hom0: forall s : Sort σ, A s -> B s
is_homomorphism_hom0: IsHomomorphism def_hom0
def_hom1: forall s : Sort σ, A s -> B s
is_homomorphism_hom1: IsHomomorphism def_hom1
p: {|
  def_hom := def_hom0;
  is_homomorphism_hom := is_homomorphism_hom0
|} =
{|
  def_hom := def_hom1;
  is_homomorphism_hom := is_homomorphism_hom1
|}
q: transport IsHomomorphism p
  (is_homomorphism_hom
     {|
       def_hom := def_hom0;
       is_homomorphism_hom := is_homomorphism_hom0
     |}) =
is_homomorphism_hom
  {|
    def_hom := def_hom1;
    is_homomorphism_hom := is_homomorphism_hom1
  |}
{|
  def_hom := def_hom0;
  is_homomorphism_hom := is_homomorphism_hom0
|} =
{|
  def_hom := def_hom1;
  is_homomorphism_hom := is_homomorphism_hom1
|} simpl in *.
σ: Signature
A, B: Algebra σ
def_hom0: forall s : Sort σ, A s -> B s
is_homomorphism_hom0: IsHomomorphism def_hom0
def_hom1: forall s : Sort σ, A s -> B s
is_homomorphism_hom1: IsHomomorphism def_hom1
p: def_hom0 = def_hom1
q: transport IsHomomorphism p is_homomorphism_hom0 =
is_homomorphism_hom1
{|
  def_hom := def_hom0;
  is_homomorphism_hom := is_homomorphism_hom0
|} =
{|
  def_hom := def_hom1;
  is_homomorphism_hom := is_homomorphism_hom1
|} by path_induction.
Defined.

(** To find a path between two homomorphisms [f g : Homomorphism A B]
    it suffices to find a path between the defining families of
    functions if [IsHSetAlgebra B]. *)

Lemma path_hset_homomorphism `{Funext} {σ} {A B : Algebra σ}
  `{!IsHSetAlgebra B} (f g : Homomorphism A B)
  (p : def_hom f = def_hom g)
  : f = g.
H: Funext
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f, g: Homomorphism A B
p: f = g
f = g
Proof.
H: Funext
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f, g: Homomorphism A B
p: f = g
f = g
  apply (path_homomorphism f g p).
H: Funext
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
f, g: Homomorphism A B
p: f = g
transport IsHomomorphism p (is_homomorphism_hom f) =
is_homomorphism_hom g apply path_ishprop.
Defined.

(** A family of functions [f : ∀ s, A s → B s] is an isomorphism if it is
    a homomorphism, and for each [s : Sort σ], [f s] is an equivalence. *)

(* We make [IsHomomorphism] an argument here, rather than a field, so
   having both [f : Homomorphism A B] and [X : IsIsomorphism f] in
   context does not result in having two proofs of [IsHomomorphism f]
   in context. *)

Class IsIsomorphism {σ : Signature} {A B : Algebra σ}
  (f : ∀ s, A s → B s) `{!IsHomomorphism f}
  := isequiv_isomorphism :: ∀ (s : Sort σ), IsEquiv (f s).

Definition equiv_isomorphism {σ : Signature} {A B : Algebra σ}
  (f : ∀ s, A s → B s) `{IsIsomorphism σ A B f}
  : ∀ (s : Sort σ), A s <~> B s.
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
H: IsIsomorphism f
forall s : Sort σ, A s <~> B s
Proof.
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
H: IsIsomorphism f
forall s : Sort σ, A s <~> B s
  intro s.
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
H: IsIsomorphism f
s: Sort σ
A s <~> B s rapply (Build_Equiv _ _ (f s)).
Defined.

Instance hprop_is_isomorphism `{Funext} {σ : Signature}
  {A B : Algebra σ} (f : ∀ s, A s → B s) `{!IsHomomorphism f}
  : IsHProp (IsIsomorphism f).
H: Funext
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
IsHProp (IsIsomorphism f)
Proof.
H: Funext
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
IsHProp (IsIsomorphism f)
  apply istrunc_forall.
Qed.

(** Let [f : ∀ s, A s → B s] be a homomorphism. The following
    section proves that [f] is "OpPreserving" with respect to
    uncurried algebra operations in the sense that

<<
      f t (α (x1,x2,...,xn,tt)) = β (f s1 x1,f s2 x1,...,f sn xn,tt)
>>

    for all [(x1,x2,...,xn,tt) : FamilyProd A [s1;s2;...;sn]], where
    [α] and [β] are uncurried algebra operations in [A] and [B]
    respectively.
*)

Section homomorphism_ap_operation.
  Context {σ : Signature} {A B : Algebra σ}.

  Lemma path_oppreserving_ap_operation (f : ∀ s, A s → B s)
    {w : SymbolType σ} (a : FamilyProd A (dom_symboltype w))
    (α : Operation A w) (β : Operation B w) (P : OpPreserving f α β)
    : f (cod_symboltype w) (ap_operation α a)
      = ap_operation β (map_family_prod f a).
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
w: SymbolType σ
a: FamilyProd A (dom_symboltype w)
α: Operation A w
β: Operation B w
P: OpPreserving f α β
f (cod_symboltype w) (ap_operation α a) =
ap_operation β (map_family_prod f a)
  Proof.
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
w: SymbolType σ
a: FamilyProd A (dom_symboltype w)
α: Operation A w
β: Operation B w
P: OpPreserving f α β
f (cod_symboltype w) (ap_operation α a) =
ap_operation β (map_family_prod f a)
    induction w.
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
t: Sort σ
a: FamilyProd A (dom_symboltype [:t:])
α: Operation A [:t:]
β: Operation B [:t:]
P: OpPreserving f α β
f (cod_symboltype [:t:]) (ap_operation α a) =
ap_operation β (map_family_prod f a)
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
t: Sort σ
w: ne_list (Sort σ)
a: FamilyProd A (dom_symboltype (t ::: w))
α: Operation A (t ::: w)
β: Operation B (t ::: w)
P: OpPreserving f α β
IHw: forall (a : FamilyProd A (dom_symboltype w)) (α : Operation A w)
(β : Operation B w),
OpPreserving f α β ->
f (cod_symboltype w) (ap_operation α a) =
ap_operation β (map_family_prod f a)
f (cod_symboltype (t ::: w)) (ap_operation α a) =
ap_operation β (map_family_prod f a)
    -
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
t: Sort σ
a: FamilyProd A (dom_symboltype [:t:])
α: Operation A [:t:]
β: Operation B [:t:]
P: OpPreserving f α β
f (cod_symboltype [:t:]) (ap_operation α a) =
ap_operation β (map_family_prod f a) assumption.
    -
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
t: Sort σ
w: ne_list (Sort σ)
a: FamilyProd A (dom_symboltype (t ::: w))
α: Operation A (t ::: w)
β: Operation B (t ::: w)
P: OpPreserving f α β
IHw: forall (a : FamilyProd A (dom_symboltype w)) (α : Operation A w)
(β : Operation B w),
OpPreserving f α β ->
f (cod_symboltype w) (ap_operation α a) =
ap_operation β (map_family_prod f a)
f (cod_symboltype (t ::: w)) (ap_operation α a) =
ap_operation β (map_family_prod f a) destruct a as [x a].
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
t: Sort σ
w: ne_list (Sort σ)
x: A t
a: Core.fold_right
  (λ (i : Sort σ) (A0 : Type), A i * A0) Unit
  (dom_symboltype w)
α: Operation A (t ::: w)
β: Operation B (t ::: w)
P: OpPreserving f α β
IHw: forall (a : FamilyProd A (dom_symboltype w)) (α : Operation A w)
(β : Operation B w),
OpPreserving f α β ->
f (cod_symboltype w) (ap_operation α a) =
ap_operation β (map_family_prod f a)
f (cod_symboltype (t ::: w)) (ap_operation α (x, a)) =
ap_operation β (map_family_prod f (x, a)) apply IHw.
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
t: Sort σ
w: ne_list (Sort σ)
x: A t
a: Core.fold_right
  (λ (i : Sort σ) (A0 : Type), A i * A0) Unit
  (dom_symboltype w)
α: Operation A (t ::: w)
β: Operation B (t ::: w)
P: OpPreserving f α β
IHw: forall (a : FamilyProd A (dom_symboltype w)) (α : Operation A w)
(β : Operation B w),
OpPreserving f α β ->
f (cod_symboltype w) (ap_operation α a) =
ap_operation β (map_family_prod f a)
OpPreserving f (α x)
  (β (fst (map_family_prod f (x, a)))) apply P.
  Defined.

(** A homomorphism [f : ∀ s, A s → B s] satisfies

<<
      f t (α (a1, a2, ..., an, tt))
      = β (f s1 a1, f s2 a2, ..., f sn an, tt)
>>

    where [(a1, a2, ..., an, tt) : FamilyProd A [s1; s2; ...; sn]] and
    [α], [β] uncurried versions of [u.#A], [u.#B] respectively. *)

  Lemma path_homomorphism_ap_operation (f : ∀ s, A s → B s)
    `{!IsHomomorphism f}
    : ∀ (u : Symbol σ) (a : FamilyProd A (dom_symboltype (σ u))),
      f (cod_symboltype (σ u)) (ap_operation u.#A a)
      = ap_operation u.#B (map_family_prod f a).
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
forall (u : Symbol σ)
(a : FamilyProd A (dom_symboltype (σ u))),
f (cod_symboltype (σ u)) (ap_operation u.#A a) =
ap_operation u.#B (map_family_prod f a)
  Proof.
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
forall (u : Symbol σ)
(a : FamilyProd A (dom_symboltype (σ u))),
f (cod_symboltype (σ u)) (ap_operation u.#A a) =
ap_operation u.#B (map_family_prod f a)
    intros u a.
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
u: Symbol σ
a: FamilyProd A (dom_symboltype (σ u))
f (cod_symboltype (σ u)) (ap_operation u.#A a) =
ap_operation u.#B (map_family_prod f a) by apply path_oppreserving_ap_operation.
  Defined.
End homomorphism_ap_operation.

(** The next section shows that the family of identity functions,
    [λ s x, x] is an isomorphism. *)

Section hom_id.
  Context {σ} (A : Algebra σ).

  #[export] Instance is_homomorphism_id
    : IsHomomorphism (λ s (x : A s), x).
σ: Signature
A: Algebra σ
IsHomomorphism (λ (s : Sort σ) (x : A s), x)
  Proof.
σ: Signature
A: Algebra σ
IsHomomorphism (λ (s : Sort σ) (x : A s), x)
    intro u.
σ: Signature
A: Algebra σ
u: Symbol σ
OpPreserving (λ (s : Sort σ) (x : A s), x) u.#A u.#A generalize u.#A.
σ: Signature
A: Algebra σ
u: Symbol σ
forall o : Operation A (σ u),
OpPreserving (λ (s : Sort σ) (x : A s), x) o o intro w.
σ: Signature
A: Algebra σ
u: Symbol σ
w: Operation A (σ u)
OpPreserving (λ (s : Sort σ) (x : A s), x) w w induction (σ u).
σ: Signature
A: Algebra σ
u: Symbol σ
t: Sort σ
w: Operation A [:t:]
OpPreserving (λ (s : Sort σ) (x : A s), x) w w
σ: Signature
A: Algebra σ
u: Symbol σ
t: Sort σ
s: ne_list (Sort σ)
w: Operation A (t ::: s)
IHs: forall w : Operation A s, OpPreserving (λ (s : Sort σ) (x : A s), x) w w
OpPreserving (λ (s : Sort σ) (x : A s), x) w w
    -
σ: Signature
A: Algebra σ
u: Symbol σ
t: Sort σ
w: Operation A [:t:]
OpPreserving (λ (s : Sort σ) (x : A s), x) w w reflexivity.
    -
σ: Signature
A: Algebra σ
u: Symbol σ
t: Sort σ
s: ne_list (Sort σ)
w: Operation A (t ::: s)
IHs: forall w : Operation A s, OpPreserving (λ (s : Sort σ) (x : A s), x) w w
OpPreserving (λ (s : Sort σ) (x : A s), x) w w by intro x.
  Defined.

  #[export] Instance is_isomorphism_id
    : IsIsomorphism (λ s (x : A s), x).
σ: Signature
A: Algebra σ
IsIsomorphism (λ (s : Sort σ) (x : A s), x)
  Proof.
σ: Signature
A: Algebra σ
IsIsomorphism (λ (s : Sort σ) (x : A s), x)
    intro s.
σ: Signature
A: Algebra σ
s: Sort σ
IsEquiv idmap exact _.
  Qed.

  Definition hom_id : Homomorphism A A
    := BuildHomomorphism (λ s x, x).

End hom_id.

(** Suppose [f : ∀ s, A s → B s] is an isomorphism. The following
    section shows that the family of inverse functions, [λ s, (f s)^-1]
    is an isomorphism. *)

Section hom_inv.
  Context
    {σ} {A B : Algebra σ}
    (f : ∀ s, A s → B s) `{IsIsomorphism σ A B f}.

  #[export] Instance is_homomorphism_inv : IsHomomorphism (λ s, (f s)^-1).
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
H: IsIsomorphism f
IsHomomorphism (λ s : Sort σ, (f s)^-1)
  Proof.
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
H: IsIsomorphism f
IsHomomorphism (λ s : Sort σ, (f s)^-1)
   intro u.
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
H: IsIsomorphism f
u: Symbol σ
OpPreserving (λ s : Sort σ, (f s)^-1) u.#B u.#A
   generalize u.#A u.#B (oppreserving_hom f u).
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
H: IsIsomorphism f
u: Symbol σ
forall (o : Operation A (σ u))
(o0 : Operation B (σ u)),
OpPreserving f o o0 ->
OpPreserving (λ s : Sort σ, (f s)^-1) o0 o
   intros a b P.
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
H: IsIsomorphism f
u: Symbol σ
a: Operation A (σ u)
b: Operation B (σ u)
P: OpPreserving f a b
OpPreserving (λ s : Sort σ, (f s)^-1) b a
   induction (σ u).
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
H: IsIsomorphism f
u: Symbol σ
t: Sort σ
a: Operation A [:t:]
b: Operation B [:t:]
P: OpPreserving f a b
OpPreserving (λ s : Sort σ, (f s)^-1) b a
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
H: IsIsomorphism f
u: Symbol σ
t: Sort σ
s: ne_list (Sort σ)
a: Operation A (t ::: s)
b: Operation B (t ::: s)
P: OpPreserving f a b
IHs: forall (a : Operation A s) 
(b : Operation B s),
OpPreserving f a b ->
OpPreserving (λ s : Sort σ, (f s)^-1) b a
OpPreserving (λ s : Sort σ, (f s)^-1) b a
   -
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
H: IsIsomorphism f
u: Symbol σ
t: Sort σ
a: Operation A [:t:]
b: Operation B [:t:]
P: OpPreserving f a b
OpPreserving (λ s : Sort σ, (f s)^-1) b a destruct P.
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
H: IsIsomorphism f
u: Symbol σ
t: Sort σ
a: Operation A [:t:]
OpPreserving (λ s : Sort σ, (f s)^-1) (f t a) a apply (eissect (f t)).
   -
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
H: IsIsomorphism f
u: Symbol σ
t: Sort σ
s: ne_list (Sort σ)
a: Operation A (t ::: s)
b: Operation B (t ::: s)
P: OpPreserving f a b
IHs: forall (a : Operation A s) 
(b : Operation B s),
OpPreserving f a b ->
OpPreserving (λ s : Sort σ, (f s)^-1) b a
OpPreserving (λ s : Sort σ, (f s)^-1) b a intro.
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
H: IsIsomorphism f
u: Symbol σ
t: Sort σ
s: ne_list (Sort σ)
a: Operation A (t ::: s)
b: Operation B (t ::: s)
P: OpPreserving f a b
IHs: forall (a : Operation A s) 
(b : Operation B s),
OpPreserving f a b ->
OpPreserving (λ s : Sort σ, (f s)^-1) b a
x: B t
OpPreserving (λ s : Sort σ, (f s)^-1) (b x)
  (a ((f t)^-1 x)) apply IHs.
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
H: IsIsomorphism f
u: Symbol σ
t: Sort σ
s: ne_list (Sort σ)
a: Operation A (t ::: s)
b: Operation B (t ::: s)
P: OpPreserving f a b
IHs: forall (a : Operation A s) 
(b : Operation B s),
OpPreserving f a b ->
OpPreserving (λ s : Sort σ, (f s)^-1) b a
x: B t
OpPreserving f (a ((f t)^-1 x)) (b x)
     exact (transport (λ y, OpPreserving f _ (b y))
              (eisretr (f t) x) (P (_^-1 x))).
  Defined.

  #[export] Instance is_isomorphism_inv : IsIsomorphism (λ s, (f s)^-1).
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
H: IsIsomorphism f
IsIsomorphism (λ s : Sort σ, (f s)^-1)
  Proof.
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
H: IsIsomorphism f
IsIsomorphism (λ s : Sort σ, (f s)^-1)
    intro s.
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
H: IsIsomorphism f
s: Sort σ
IsEquiv (f s)^-1 exact _.
  Qed.

  Definition hom_inv : Homomorphism B A
    := BuildHomomorphism (λ s, (f s)^-1).

End hom_inv.

(** Let [f : ∀ s, A s → B s] and [g : ∀ s, B s → C s]. The
    next section shows that composition given by [λ (s : Sort σ),
    g s o f s] is again a homomorphism. If both [f] and [g] are
    isomorphisms, then the composition is an isomorphism. *)

Section hom_compose.
  Context {σ} {A B C : Algebra σ}.

  Lemma oppreserving_compose (g : ∀ s, B s → C s) `{!IsHomomorphism g}
    (f : ∀ s, A s → B s) `{!IsHomomorphism f} {w : SymbolType σ}
    (α : Operation A w) (β : Operation B w) (γ : Operation C w)
    (G : OpPreserving g β γ) (F : OpPreserving f α β)
    : OpPreserving (λ s, g s o f s) α γ.
σ: Signature
A, B, C: Algebra σ
g: forall s : Sort σ, B s -> C s
IsHomomorphism0: IsHomomorphism g
f: forall s : Sort σ, A s -> B s
IsHomomorphism1: IsHomomorphism f
w: SymbolType σ
α: Operation A w
β: Operation B w
γ: Operation C w
G: OpPreserving g β γ
F: OpPreserving f α β
OpPreserving (λ s : Sort σ, g s o f s) α γ
  Proof.
σ: Signature
A, B, C: Algebra σ
g: forall s : Sort σ, B s -> C s
IsHomomorphism0: IsHomomorphism g
f: forall s : Sort σ, A s -> B s
IsHomomorphism1: IsHomomorphism f
w: SymbolType σ
α: Operation A w
β: Operation B w
γ: Operation C w
G: OpPreserving g β γ
F: OpPreserving f α β
OpPreserving (λ s : Sort σ, g s o f s) α γ
    induction w; simpl in *.
σ: Signature
A, B, C: Algebra σ
g: forall s : Sort σ, B s -> C s
IsHomomorphism0: IsHomomorphism g
f: forall s : Sort σ, A s -> B s
IsHomomorphism1: IsHomomorphism f
t: Sort σ
α: A t
β: B t
γ: C t
G: g t β = γ
F: f t α = β
g t (f t α) = γ
σ: Signature
A, B, C: Algebra σ
g: forall s : Sort σ, B s -> C s
IsHomomorphism0: IsHomomorphism g
f: forall s : Sort σ, A s -> B s
IsHomomorphism1: IsHomomorphism f
t: Sort σ
w: ne_list (Sort σ)
α: A t -> Operation A w
β: B t -> Operation B w
γ: C t -> Operation C w
G: forall x : B t, OpPreserving g (β x) (γ (g t x))
F: forall x : A t, OpPreserving f (α x) (β (f t x))
IHw: forall (α : Operation A w) 
(β : Operation B w) 
(γ : Operation C w),
OpPreserving g β γ ->
OpPreserving f α β ->
OpPreserving
  (λ (s : Sort σ) (x : A s), g s (f s x)) α γ
forall x : A t,
OpPreserving (λ (s : Sort σ) (x0 : A s), g s (f s x0))
  (α x) (γ (g t (f t x)))
    -
σ: Signature
A, B, C: Algebra σ
g: forall s : Sort σ, B s -> C s
IsHomomorphism0: IsHomomorphism g
f: forall s : Sort σ, A s -> B s
IsHomomorphism1: IsHomomorphism f
t: Sort σ
α: A t
β: B t
γ: C t
G: g t β = γ
F: f t α = β
g t (f t α) = γ by path_induction.
    -
σ: Signature
A, B, C: Algebra σ
g: forall s : Sort σ, B s -> C s
IsHomomorphism0: IsHomomorphism g
f: forall s : Sort σ, A s -> B s
IsHomomorphism1: IsHomomorphism f
t: Sort σ
w: ne_list (Sort σ)
α: A t -> Operation A w
β: B t -> Operation B w
γ: C t -> Operation C w
G: forall x : B t, OpPreserving g (β x) (γ (g t x))
F: forall x : A t, OpPreserving f (α x) (β (f t x))
IHw: forall (α : Operation A w) 
(β : Operation B w) 
(γ : Operation C w),
OpPreserving g β γ ->
OpPreserving f α β ->
OpPreserving
  (λ (s : Sort σ) (x : A s), g s (f s x)) α γ
forall x : A t,
OpPreserving (λ (s : Sort σ) (x0 : A s), g s (f s x0))
  (α x) (γ (g t (f t x))) intro x.
σ: Signature
A, B, C: Algebra σ
g: forall s : Sort σ, B s -> C s
IsHomomorphism0: IsHomomorphism g
f: forall s : Sort σ, A s -> B s
IsHomomorphism1: IsHomomorphism f
t: Sort σ
w: ne_list (Sort σ)
α: A t -> Operation A w
β: B t -> Operation B w
γ: C t -> Operation C w
G: forall x : B t, OpPreserving g (β x) (γ (g t x))
F: forall x : A t, OpPreserving f (α x) (β (f t x))
IHw: forall (α : Operation A w) 
(β : Operation B w) 
(γ : Operation C w),
OpPreserving g β γ ->
OpPreserving f α β ->
OpPreserving
  (λ (s : Sort σ) (x : A s), g s (f s x)) α γ
x: A t
OpPreserving (λ (s : Sort σ) (x : A s), g s (f s x))
  (α x) (γ (g t (f t x))) by apply (IHw _ (β (f _ x))).
  Defined.

  #[export] Instance is_homomorphism_compose
    (g : ∀ s, B s → C s) `{!IsHomomorphism g}
    (f : ∀ s, A s → B s) `{!IsHomomorphism f}
    : IsHomomorphism (λ s, g s o f s).
σ: Signature
A, B, C: Algebra σ
g: forall s : Sort σ, B s -> C s
IsHomomorphism0: IsHomomorphism g
f: forall s : Sort σ, A s -> B s
IsHomomorphism1: IsHomomorphism f
IsHomomorphism (λ s : Sort σ, g s o f s)
  Proof.
σ: Signature
A, B, C: Algebra σ
g: forall s : Sort σ, B s -> C s
IsHomomorphism0: IsHomomorphism g
f: forall s : Sort σ, A s -> B s
IsHomomorphism1: IsHomomorphism f
IsHomomorphism (λ s : Sort σ, g s o f s)
    intro u.
σ: Signature
A, B, C: Algebra σ
g: forall s : Sort σ, B s -> C s
IsHomomorphism0: IsHomomorphism g
f: forall s : Sort σ, A s -> B s
IsHomomorphism1: IsHomomorphism f
u: Symbol σ
OpPreserving (λ (s : Sort σ) (x : A s), g s (f s x))
  u.#A u.#C
    by apply (oppreserving_compose g f u.#A u.#B u.#C).
  Defined.

  #[export] Instance is_isomorphism_compose
    (g : ∀ s, B s → C s) `{IsIsomorphism σ B C g}
    (f : ∀ s, A s → B s) `{IsIsomorphism σ A B f}
    : IsIsomorphism (λ s, g s o f s).
σ: Signature
A, B, C: Algebra σ
g: forall s : Sort σ, B s -> C s
IsHomomorphism0: IsHomomorphism g
H: IsIsomorphism g
f: forall s : Sort σ, A s -> B s
IsHomomorphism1: IsHomomorphism f
H0: IsIsomorphism f
IsIsomorphism (λ s : Sort σ, g s o f s)
  Proof.
σ: Signature
A, B, C: Algebra σ
g: forall s : Sort σ, B s -> C s
IsHomomorphism0: IsHomomorphism g
H: IsIsomorphism g
f: forall s : Sort σ, A s -> B s
IsHomomorphism1: IsHomomorphism f
H0: IsIsomorphism f
IsIsomorphism (λ s : Sort σ, g s o f s)
    intro s.
σ: Signature
A, B, C: Algebra σ
g: forall s : Sort σ, B s -> C s
IsHomomorphism0: IsHomomorphism g
H: IsIsomorphism g
f: forall s : Sort σ, A s -> B s
IsHomomorphism1: IsHomomorphism f
H0: IsIsomorphism f
s: Sort σ
IsEquiv (λ x : A s, g s (f s x)) rapply isequiv_compose.
  Qed.

  Definition hom_compose
    (g : Homomorphism B C) (f : Homomorphism A B)
    : Homomorphism A C
    := BuildHomomorphism (λ s, g s o f s).

End hom_compose.

(** The following section shows that there is a path between
    isomorphic algebras. *)

Section path_isomorphism.
  Context `{Univalence} {σ : Signature} {A B : Algebra σ}.

(** Let [F G : I → Type]. If [f : ∀ (i:I), F i <~> G i] is a family of
    equivalences, then by function extensionality composed with
    univalence there is a path [F = G]. *)

  Local Notation path_equiv_family f
    := (path_forall _ _ (λ i, path_universe (f i))).

(** Given a family of equivalences [f : ∀ (s : Sort σ), A s <~> B s]
    which is [OpPreserving f α β] with respect to algebra operations

<<
      α : A s1 → A s2 → ... → A sn → A t
      β : B s1 → B s2 → ... → B sn → B t
>>

    By transporting [α] along the path [path_equiv_family f] we
    find a path from the transported operation [α] to [β]. *)

  Lemma path_operations_equiv {w : SymbolType σ}
    (α : Operation A w) (β : Operation B w)
    (f : ∀ (s : Sort σ), A s <~> B s) (P : OpPreserving f α β)
    : transport (λ C : Carriers σ, Operation C w)
        (path_equiv_family f) α
      = β.
H: Univalence
σ: Signature
A, B: Algebra σ
w: SymbolType σ
α: Operation A w
β: Operation B w
f: forall s : Sort σ, A s <~> B s
P: OpPreserving (λ s : Sort σ, f s) α β
transport (λ C : Carriers σ, Operation C w)
  (path_forall A B (λ i : Sort σ, path_universe (f i)))
  α = β
  Proof.
H: Univalence
σ: Signature
A, B: Algebra σ
w: SymbolType σ
α: Operation A w
β: Operation B w
f: forall s : Sort σ, A s <~> B s
P: OpPreserving (λ s : Sort σ, f s) α β
transport (λ C : Carriers σ, Operation C w)
  (path_forall A B (λ i : Sort σ, path_universe (f i)))
  α = β
    induction w; simpl in *.
H: Univalence
σ: Signature
A, B: Algebra σ
t: Sort σ
α: A t
β: B t
f: forall s : Sort σ, A s <~> B s
P: f t α = β
transport (λ C : Carriers σ, C t)
  (path_forall A B (λ i : Sort σ, path_universe (f i)))
  α = β
H: Univalence
σ: Signature
A, B: Algebra σ
t: Sort σ
w: ne_list (Sort σ)
α: A t -> Operation A w
β: B t -> Operation B w
f: forall s : Sort σ, A s <~> B s
P: forall x : A t,
OpPreserving (λ s : Sort σ, f s) (α x) (β (f t x))
IHw: forall (α : Operation A w) (β : Operation B w),
OpPreserving (λ s : Sort σ, f s) α β ->
transport (λ C : Carriers σ, Operation C w)
(path_forall A B (λ i : Sort σ, path_universe (f i))) α = β
transport (λ C : Carriers σ, C t -> Operation C w)
  (path_forall A B (λ i : Sort σ, path_universe (f i)))
  α = β
    -
H: Univalence
σ: Signature
A, B: Algebra σ
t: Sort σ
α: A t
β: B t
f: forall s : Sort σ, A s <~> B s
P: f t α = β
transport (λ C : Carriers σ, C t)
  (path_forall A B (λ i : Sort σ, path_universe (f i)))
  α = β transport_path_forall_hammer.
H: Univalence
σ: Signature
A, B: Algebra σ
t: Sort σ
α: A t
β: B t
f: forall s : Sort σ, A s <~> B s
P: f t α = β
transport idmap (path_universe (f t)) α = β
      exact (ap10 (transport_idmap_path_universe (f t)) α @ P).
    -
H: Univalence
σ: Signature
A, B: Algebra σ
t: Sort σ
w: ne_list (Sort σ)
α: A t -> Operation A w
β: B t -> Operation B w
f: forall s : Sort σ, A s <~> B s
P: forall x : A t,
OpPreserving (λ s : Sort σ, f s) (α x) (β (f t x))
IHw: forall (α : Operation A w) (β : Operation B w),
OpPreserving (λ s : Sort σ, f s) α β ->
transport (λ C : Carriers σ, Operation C w)
(path_forall A B (λ i : Sort σ, path_universe (f i))) α = β
transport (λ C : Carriers σ, C t -> Operation C w)
  (path_forall A B (λ i : Sort σ, path_universe (f i)))
  α = β funext y.
H: Univalence
σ: Signature
A, B: Algebra σ
t: Sort σ
w: ne_list (Sort σ)
α: A t -> Operation A w
β: B t -> Operation B w
f: forall s : Sort σ, A s <~> B s
P: forall x : A t,
OpPreserving (λ s : Sort σ, f s) (α x) (β (f t x))
IHw: forall (α : Operation A w) (β : Operation B w),
OpPreserving (λ s : Sort σ, f s) α β ->
transport (λ C : Carriers σ, Operation C w)
(path_forall A B (λ i : Sort σ, path_universe (f i))) α = β
y: B t
transport (λ C : Carriers σ, C t -> Operation C w)
  (path_forall A B (λ i : Sort σ, path_universe (f i)))
  α y = β y
      transport_path_forall_hammer.
H: Univalence
σ: Signature
A, B: Algebra σ
t: Sort σ
w: ne_list (Sort σ)
α: A t -> Operation A w
β: B t -> Operation B w
f: forall s : Sort σ, A s <~> B s
P: forall x : A t,
OpPreserving (λ s : Sort σ, f s) (α x) (β (f t x))
IHw: forall (α : Operation A w) (β : Operation B w),
OpPreserving (λ s : Sort σ, f s) α β ->
transport (λ C : Carriers σ, Operation C w)
(path_forall A B (λ i : Sort σ, path_universe (f i))) α = β
y: B t
transport (λ x : Carriers σ, B t -> Operation x w)
  (path_forall A B (λ i : Sort σ, path_universe (f i)))
  (transport (λ y : Type, y -> Operation A w)
     (path_universe (f t)) α) y = β y
      rewrite transport_forall_constant.
H: Univalence
σ: Signature
A, B: Algebra σ
t: Sort σ
w: ne_list (Sort σ)
α: A t -> Operation A w
β: B t -> Operation B w
f: forall s : Sort σ, A s <~> B s
P: forall x : A t,
OpPreserving (λ s : Sort σ, f s) (α x) (β (f t x))
IHw: forall (α : Operation A w) (β : Operation B w),
OpPreserving (λ s : Sort σ, f s) α β ->
transport (λ C : Carriers σ, Operation C w)
(path_forall A B (λ i : Sort σ, path_universe (f i))) α = β
y: B t
transport (λ x : Carriers σ, Operation x w)
  (path_forall A B (λ i : Sort σ, path_universe (f i)))
  (transport (λ y : Type, y -> Operation A w)
     (path_universe (f t)) α y) = β y
      rewrite transport_arrow_toconst.
H: Univalence
σ: Signature
A, B: Algebra σ
t: Sort σ
w: ne_list (Sort σ)
α: A t -> Operation A w
β: B t -> Operation B w
f: forall s : Sort σ, A s <~> B s
P: forall x : A t,
OpPreserving (λ s : Sort σ, f s) (α x) (β (f t x))
IHw: forall (α : Operation A w) (β : Operation B w),
OpPreserving (λ s : Sort σ, f s) α β ->
transport (λ C : Carriers σ, Operation C w)
(path_forall A B (λ i : Sort σ, path_universe (f i))) α = β
y: B t
transport (λ x : Carriers σ, Operation x w)
  (path_forall A B (λ i : Sort σ, path_universe (f i)))
  (α (transport idmap (path_universe (f t))^ y)) = 
β y
      rewrite (transport_path_universe_V (f t)).
H: Univalence
σ: Signature
A, B: Algebra σ
t: Sort σ
w: ne_list (Sort σ)
α: A t -> Operation A w
β: B t -> Operation B w
f: forall s : Sort σ, A s <~> B s
P: forall x : A t,
OpPreserving (λ s : Sort σ, f s) (α x) (β (f t x))
IHw: forall (α : Operation A w) (β : Operation B w),
OpPreserving (λ s : Sort σ, f s) α β ->
transport (λ C : Carriers σ, Operation C w)
(path_forall A B (λ i : Sort σ, path_universe (f i))) α = β
y: B t
transport (λ x : Carriers σ, Operation x w)
  (path_forall A B (λ i : Sort σ, path_universe (f i)))
  (α ((f t)^-1 y)) = β y
      apply IHw.
H: Univalence
σ: Signature
A, B: Algebra σ
t: Sort σ
w: ne_list (Sort σ)
α: A t -> Operation A w
β: B t -> Operation B w
f: forall s : Sort σ, A s <~> B s
P: forall x : A t,
OpPreserving (λ s : Sort σ, f s) (α x) (β (f t x))
IHw: forall (α : Operation A w) (β : Operation B w),
OpPreserving (λ s : Sort σ, f s) α β ->
transport (λ C : Carriers σ, Operation C w)
(path_forall A B (λ i : Sort σ, path_universe (f i))) α = β
y: B t
OpPreserving (λ s : Sort σ, f s) (α ((f t)^-1 y))
  (β y)
      specialize (P ((f t)^-1 y)).
H: Univalence
σ: Signature
A, B: Algebra σ
t: Sort σ
w: ne_list (Sort σ)
α: A t -> Operation A w
β: B t -> Operation B w
f: forall s : Sort σ, A s <~> B s
y: B t
P: OpPreserving (λ s : Sort σ, f s) (α ((f t)^-1 y))
  (β (f t ((f t)^-1 y)))
IHw: forall (α : Operation A w) (β : Operation B w),
OpPreserving (λ s : Sort σ, f s) α β ->
transport (λ C : Carriers σ, Operation C w)
(path_forall A B (λ i : Sort σ, path_universe (f i))) α = β
OpPreserving (λ s : Sort σ, f s) (α ((f t)^-1 y))
  (β y)
      by rewrite (eisretr (f t) y) in P.
  Qed.

(** Suppose [u : Symbol σ] is a function symbol. Recall that
    [u.#A] is notation for [operations A u : Operation A (σ u)]. This
    is the algebra operation corresponding to function symbol [u]. *)

(** An isomorphism [f : ∀ s, A s → B s] induces a family of
    equivalences [e : ∀ (s : Sort σ), A s <~> B s]. Let [u : Symbol σ]
    be a function symbol. Since [f] is a homomorphism, the induced
    family of equivalences [e] satisfies [OpPreserving e (u.#A) (u.#B)].
    By [path_operations_equiv] above, we can then transport [u.#A] along
    the path [path_equiv_family e] and obtain a path to [u.#B]. *)

  Lemma path_operations_isomorphism (f : ∀ s, A s → B s)
    `{IsIsomorphism σ A B f} (u : Symbol σ)
    : transport (λ C : Carriers σ, Operation C (σ u))
        (path_equiv_family (equiv_isomorphism f)) u.#A
      = u.#B.
H: Univalence
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
H0: IsIsomorphism f
u: Symbol σ
transport (λ C : Carriers σ, Operation C (σ u))
  (path_forall A B
     (λ i : Sort σ,
      path_universe (equiv_isomorphism f i))) u.#A =
u.#B
  Proof.
H: Univalence
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
H0: IsIsomorphism f
u: Symbol σ
transport (λ C : Carriers σ, Operation C (σ u))
  (path_forall A B
     (λ i : Sort σ,
      path_universe (equiv_isomorphism f i))) u.#A =
u.#B
    by apply path_operations_equiv.
  Defined.

(** If there is an isomorphism [f : ∀ s, A s → B s] then [A = B]. *)

  Theorem path_isomorphism (f : ∀ s, A s → B s) `{IsIsomorphism σ A B f}
    : A = B.
H: Univalence
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
H0: IsIsomorphism f
A = B
  Proof.
H: Univalence
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
H0: IsIsomorphism f
A = B
    apply (path_algebra _ _ (path_equiv_family (equiv_isomorphism f))).
H: Univalence
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
IsHomomorphism0: IsHomomorphism f
H0: IsIsomorphism f
transport
  (λ X : Carriers σ,
   forall u : Symbol σ, Operation X (σ u))
  (path_forall A B
     (λ i : Sort σ,
      path_universe (equiv_isomorphism f i)))
  (operations A) = operations B
(* Make the last part abstract because it relies on [path_operations_equiv],
   which is opaque. In cases where the involved algebras are set algebras,
   then this part is a mere proposition. *)
    abstract (
      funext u;
      exact (transport_forall_constant _ _ u
             @ path_operations_isomorphism f u)).
  Defined.
End path_isomorphism.