Require Import
  HoTT.Types.Bool
  HoTT.Classes.theory.ua_homomorphism.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

Import algebra_notations ne_list.notations.

(** The following section defines product algebra [ProdAlgebra].
    Section [bin_prod_algebra] specialises the definition to
    binary product algebra. *)

Section prod_algebra.
  Context `{Funext} {σ : Signature} (I : Type) (A : I → Algebra σ).

  Definition carriers_prod_algebra : Carriers σ
    := λ (s : Sort σ), ∀ (i:I), A i s.

  Fixpoint op_prod_algebra (w : SymbolType σ)
      : (∀ i, Operation (A i) w) →
        Operation carriers_prod_algebra w :=
    match w return (∀ i, Operation (A i) w) →
                    Operation carriers_prod_algebra w
    with
    | [:_:] => idmap
    | _ ::: g => λ f p, op_prod_algebra g (λ i, f i (p i))
    end.

  Definition ops_prod_algebra (u : Symbol σ)
    : Operation carriers_prod_algebra (σ u)
    := op_prod_algebra (σ u) (λ (i:I), u.#(A i)).

  Definition ProdAlgebra : Algebra σ
    := BuildAlgebra carriers_prod_algebra ops_prod_algebra.

  #[export] Instance trunc_prod_algebra {n : trunc_index}
    `{!∀ i, IsTruncAlgebra n (A i)}
    : IsTruncAlgebra n ProdAlgebra.
H: Funext
σ: Signature
I: Type
A: I -> Algebra σ
n: trunc_index
H0: forall i : I, IsTruncAlgebra n (A i)
IsTruncAlgebra n ProdAlgebra
  Proof.
H: Funext
σ: Signature
I: Type
A: I -> Algebra σ
n: trunc_index
H0: forall i : I, IsTruncAlgebra n (A i)
IsTruncAlgebra n ProdAlgebra
    intro s.
H: Funext
σ: Signature
I: Type
A: I -> Algebra σ
n: trunc_index
H0: forall i : I, IsTruncAlgebra n (A i)
s: Sort σ
IsTrunc n (ProdAlgebra s) exact _.
  Qed.
End prod_algebra.

(** The next section defines the product projection homomorphisms. *)

Section hom_proj_prod_algebra.
  Context `{Funext} {σ : Signature} (I : Type) (A : I → Algebra σ).

  Definition def_proj_prod_algebra (i:I) (s : Sort σ) (c : ProdAlgebra I A s)
    : A i s
    := c i.

  Lemma oppreserving_proj_prod_algebra {w : SymbolType σ}
    (i : I) (v : ∀ i : I, Operation (A i) w) (α : Operation (A i) w)
    (P : v i = α)
    : OpPreserving (def_proj_prod_algebra i)
        (op_prod_algebra I A w v) α.
H: Funext
σ: Signature
I: Type
A: I -> Algebra σ
w: SymbolType σ
i: I
v: forall i : I, Operation (A i) w
α: Operation (A i) w
P: v i = α
OpPreserving (def_proj_prod_algebra i)
  (op_prod_algebra I A w v) α
  Proof.
H: Funext
σ: Signature
I: Type
A: I -> Algebra σ
w: SymbolType σ
i: I
v: forall i : I, Operation (A i) w
α: Operation (A i) w
P: v i = α
OpPreserving (def_proj_prod_algebra i)
  (op_prod_algebra I A w v) α
    induction w.
H: Funext
σ: Signature
I: Type
A: I -> Algebra σ
t: Sort σ
i: I
v: forall i : I, Operation (A i) [:t:]
α: Operation (A i) [:t:]
P: v i = α
OpPreserving (def_proj_prod_algebra i)
  (op_prod_algebra I A [:t:] v) α
H: Funext
σ: Signature
I: Type
A: I -> Algebra σ
t: Sort σ
w: ne_list (Sort σ)
i: I
v: forall i : I, Operation (A i) (t ::: w)
α: Operation (A i) (t ::: w)
P: v i = α
IHw: forall (v : forall i : I, Operation (A i) w) (α : Operation (A i) w),
v i = α -> OpPreserving (def_proj_prod_algebra i) (op_prod_algebra I A w v) α
OpPreserving (def_proj_prod_algebra i)
  (op_prod_algebra I A (t ::: w) v) α
    -
H: Funext
σ: Signature
I: Type
A: I -> Algebra σ
t: Sort σ
i: I
v: forall i : I, Operation (A i) [:t:]
α: Operation (A i) [:t:]
P: v i = α
OpPreserving (def_proj_prod_algebra i)
  (op_prod_algebra I A [:t:] v) α exact P.
    -
H: Funext
σ: Signature
I: Type
A: I -> Algebra σ
t: Sort σ
w: ne_list (Sort σ)
i: I
v: forall i : I, Operation (A i) (t ::: w)
α: Operation (A i) (t ::: w)
P: v i = α
IHw: forall (v : forall i : I, Operation (A i) w) (α : Operation (A i) w),
v i = α -> OpPreserving (def_proj_prod_algebra i) (op_prod_algebra I A w v) α
OpPreserving (def_proj_prod_algebra i)
  (op_prod_algebra I A (t ::: w) v) α intro p.
H: Funext
σ: Signature
I: Type
A: I -> Algebra σ
t: Sort σ
w: ne_list (Sort σ)
i: I
v: forall i : I, Operation (A i) (t ::: w)
α: Operation (A i) (t ::: w)
P: v i = α
IHw: forall (v : forall i : I, Operation (A i) w) (α : Operation (A i) w),
v i = α -> OpPreserving (def_proj_prod_algebra i) (op_prod_algebra I A w v) α
p: ProdAlgebra I A t
OpPreserving (def_proj_prod_algebra i)
  (op_prod_algebra I A (t ::: w) v p)
  (α (def_proj_prod_algebra i t p)) apply (IHw (λ i, v i (p i)) (α (p i))).
H: Funext
σ: Signature
I: Type
A: I -> Algebra σ
t: Sort σ
w: ne_list (Sort σ)
i: I
v: forall i : I, Operation (A i) (t ::: w)
α: Operation (A i) (t ::: w)
P: v i = α
IHw: forall (v : forall i : I, Operation (A i) w) (α : Operation (A i) w),
v i = α -> OpPreserving (def_proj_prod_algebra i) (op_prod_algebra I A w v) α
p: ProdAlgebra I A t
v i (p i) = α (p i) f_ap.
  Defined.

  #[export] Instance is_homomorphism_proj_prod_algebra (i:I)
    : IsHomomorphism (def_proj_prod_algebra i).
H: Funext
σ: Signature
I: Type
A: I -> Algebra σ
i: I
IsHomomorphism (def_proj_prod_algebra i)
  Proof.
H: Funext
σ: Signature
I: Type
A: I -> Algebra σ
i: I
IsHomomorphism (def_proj_prod_algebra i)
    intro u.
H: Funext
σ: Signature
I: Type
A: I -> Algebra σ
i: I
u: Symbol σ
OpPreserving (def_proj_prod_algebra i)
  u.#(ProdAlgebra I A) u.#(A i)
    by apply oppreserving_proj_prod_algebra.
  Defined.

  Definition hom_proj_prod_algebra (i : I)
    : Homomorphism (ProdAlgebra I A) (A i)
    := BuildHomomorphism (def_proj_prod_algebra i).

End hom_proj_prod_algebra.

(** The product algebra universal mapping property [ump_prod_algebra]. *)

Section ump_prod_algebra.
  Context
    `{Funext}
    {σ : Signature}
    (I : Type)
    (A : I → Algebra σ)
    (C : Algebra σ).

  Definition hom_prod_algebra_mapout
    (f : Homomorphism C (ProdAlgebra I A)) (i:I)
    : Homomorphism C (A i)
    := hom_compose (hom_proj_prod_algebra I A i) f.

  Definition def_prod_algebra_mapin (f : ∀ (i:I) s, C s → A i s)
    : ∀ (s : Sort σ) , C s → ProdAlgebra I A s
    := λ (s : Sort σ) (x : C s) (i : I), f i s x.

  Lemma oppreserving_prod_algebra_mapin {w : SymbolType σ}
    (f : ∀ (i:I) s, C s → A i s)
    (α : ∀ (i:I), Operation (A i) w) (β : Operation C w)
    (P : ∀ (i:I), OpPreserving (f i) β (α i))
    : OpPreserving (def_prod_algebra_mapin f) β
        (op_prod_algebra I A w (λ i, α i)).
H: Funext
σ: Signature
I: Type
A: I -> Algebra σ
C: Algebra σ
w: SymbolType σ
f: forall (i : I) (s : Sort σ), C s -> A i s
α: forall i : I, Operation (A i) w
β: Operation C w
P: forall i : I, OpPreserving (f i) β (α i)
OpPreserving (def_prod_algebra_mapin f) β
  (op_prod_algebra I A w (λ i : I, α i))
  Proof.
H: Funext
σ: Signature
I: Type
A: I -> Algebra σ
C: Algebra σ
w: SymbolType σ
f: forall (i : I) (s : Sort σ), C s -> A i s
α: forall i : I, Operation (A i) w
β: Operation C w
P: forall i : I, OpPreserving (f i) β (α i)
OpPreserving (def_prod_algebra_mapin f) β
  (op_prod_algebra I A w (λ i : I, α i))
    induction w.
H: Funext
σ: Signature
I: Type
A: I -> Algebra σ
C: Algebra σ
t: Sort σ
f: forall (i : I) (s : Sort σ), C s -> A i s
α: forall i : I, Operation (A i) [:t:]
β: Operation C [:t:]
P: forall i : I, OpPreserving (f i) β (α i)
OpPreserving (def_prod_algebra_mapin f) β
  (op_prod_algebra I A [:t:] (λ i : I, α i))
H: Funext
σ: Signature
I: Type
A: I -> Algebra σ
C: Algebra σ
t: Sort σ
w: ne_list (Sort σ)
f: forall (i : I) (s : Sort σ), C s -> A i s
α: forall i : I, Operation (A i) (t ::: w)
β: Operation C (t ::: w)
P: forall i : I, OpPreserving (f i) β (α i)
IHw: forall (α : forall i : I, Operation (A i) w) (β : Operation C w),
(forall i : I, OpPreserving (f i) β (α i)) ->
OpPreserving (def_prod_algebra_mapin f) β
(op_prod_algebra I A w (λ i : I, α i))
OpPreserving (def_prod_algebra_mapin f) β
  (op_prod_algebra I A (t ::: w) (λ i : I, α i))
    -
H: Funext
σ: Signature
I: Type
A: I -> Algebra σ
C: Algebra σ
t: Sort σ
f: forall (i : I) (s : Sort σ), C s -> A i s
α: forall i : I, Operation (A i) [:t:]
β: Operation C [:t:]
P: forall i : I, OpPreserving (f i) β (α i)
OpPreserving (def_prod_algebra_mapin f) β
  (op_prod_algebra I A [:t:] (λ i : I, α i)) funext i.
H: Funext
σ: Signature
I: Type
A: I -> Algebra σ
C: Algebra σ
t: Sort σ
f: forall (i : I) (s : Sort σ), C s -> A i s
α: forall i : I, Operation (A i) [:t:]
β: Operation C [:t:]
P: forall i : I, OpPreserving (f i) β (α i)
i: I
def_prod_algebra_mapin f t β i =
op_prod_algebra I A [:t:] (λ i : I, α i) i apply P.
    -
H: Funext
σ: Signature
I: Type
A: I -> Algebra σ
C: Algebra σ
t: Sort σ
w: ne_list (Sort σ)
f: forall (i : I) (s : Sort σ), C s -> A i s
α: forall i : I, Operation (A i) (t ::: w)
β: Operation C (t ::: w)
P: forall i : I, OpPreserving (f i) β (α i)
IHw: forall (α : forall i : I, Operation (A i) w) (β : Operation C w),
(forall i : I, OpPreserving (f i) β (α i)) ->
OpPreserving (def_prod_algebra_mapin f) β
(op_prod_algebra I A w (λ i : I, α i))
OpPreserving (def_prod_algebra_mapin f) β
  (op_prod_algebra I A (t ::: w) (λ i : I, α i)) intro x.
H: Funext
σ: Signature
I: Type
A: I -> Algebra σ
C: Algebra σ
t: Sort σ
w: ne_list (Sort σ)
f: forall (i : I) (s : Sort σ), C s -> A i s
α: forall i : I, Operation (A i) (t ::: w)
β: Operation C (t ::: w)
P: forall i : I, OpPreserving (f i) β (α i)
IHw: forall (α : forall i : I, Operation (A i) w) (β : Operation C w),
(forall i : I, OpPreserving (f i) β (α i)) ->
OpPreserving (def_prod_algebra_mapin f) β
(op_prod_algebra I A w (λ i : I, α i))
x: C t
OpPreserving (def_prod_algebra_mapin f) (β x)
  (op_prod_algebra I A (t ::: w) (λ i : I, α i)
     (def_prod_algebra_mapin f t x)) apply IHw.
H: Funext
σ: Signature
I: Type
A: I -> Algebra σ
C: Algebra σ
t: Sort σ
w: ne_list (Sort σ)
f: forall (i : I) (s : Sort σ), C s -> A i s
α: forall i : I, Operation (A i) (t ::: w)
β: Operation C (t ::: w)
P: forall i : I, OpPreserving (f i) β (α i)
IHw: forall (α : forall i : I, Operation (A i) w) (β : Operation C w),
(forall i : I, OpPreserving (f i) β (α i)) ->
OpPreserving (def_prod_algebra_mapin f) β
(op_prod_algebra I A w (λ i : I, α i))
x: C t
forall i : I,
OpPreserving (f i) (β x)
  (α i (def_prod_algebra_mapin f t x i)) intro i.
H: Funext
σ: Signature
I: Type
A: I -> Algebra σ
C: Algebra σ
t: Sort σ
w: ne_list (Sort σ)
f: forall (i : I) (s : Sort σ), C s -> A i s
α: forall i : I, Operation (A i) (t ::: w)
β: Operation C (t ::: w)
P: forall i : I, OpPreserving (f i) β (α i)
IHw: forall (α : forall i : I, Operation (A i) w) (β : Operation C w),
(forall i : I, OpPreserving (f i) β (α i)) ->
OpPreserving (def_prod_algebra_mapin f) β
(op_prod_algebra I A w (λ i : I, α i))
x: C t
i: I
OpPreserving (f i) (β x)
  (α i (def_prod_algebra_mapin f t x i)) apply P.
  Defined.

  #[export] Instance is_homomorphism_prod_algebra_mapin
    (f : ∀ (i:I), Homomorphism C (A i))
    : IsHomomorphism (def_prod_algebra_mapin f).
H: Funext
σ: Signature
I: Type
A: I -> Algebra σ
C: Algebra σ
f: forall i : I, Homomorphism C (A i)
IsHomomorphism (def_prod_algebra_mapin (λ i : I, f i))
  Proof.
H: Funext
σ: Signature
I: Type
A: I -> Algebra σ
C: Algebra σ
f: forall i : I, Homomorphism C (A i)
IsHomomorphism (def_prod_algebra_mapin (λ i : I, f i))
    intro u.
H: Funext
σ: Signature
I: Type
A: I -> Algebra σ
C: Algebra σ
f: forall i : I, Homomorphism C (A i)
u: Symbol σ
OpPreserving (def_prod_algebra_mapin (λ i : I, f i))
  u.#C u.#(ProdAlgebra I A)
    apply oppreserving_prod_algebra_mapin.
H: Funext
σ: Signature
I: Type
A: I -> Algebra σ
C: Algebra σ
f: forall i : I, Homomorphism C (A i)
u: Symbol σ
forall i : I, OpPreserving (f i) u.#C u.#(A i)
    intro i.
H: Funext
σ: Signature
I: Type
A: I -> Algebra σ
C: Algebra σ
f: forall i : I, Homomorphism C (A i)
u: Symbol σ
i: I
OpPreserving (f i) u.#C u.#(A i)
    apply f.
  Defined.

  Definition hom_prod_algebra_mapin (f : ∀ i, Homomorphism C (A i))
    : Homomorphism C (ProdAlgebra I A)
    := BuildHomomorphism (def_prod_algebra_mapin f).

  (** Given a family of homomorphisms [h : ∀ (i:I), Homomorphism C (A i)]
      there is a unique homomorphism [f : Homomorphism C (ProdAlgebra I A)]
      such that [h i = hom_compose (pr i) f], where

<<
        pr i = hom_proj_prod_algebra I A i
>>

      is the ith projection homomorphism. *)

 Lemma ump_prod_algebra `{!∀ i, IsHSetAlgebra (A i)}
   : (∀ (i:I), Homomorphism C (A i)) <~> Homomorphism C (ProdAlgebra I A).
H: Funext
σ: Signature
I: Type
A: I -> Algebra σ
C: Algebra σ
H0: forall i : I, IsHSetAlgebra (A i)
(forall i : I, Homomorphism C (A i)) <~>
Homomorphism C (ProdAlgebra I A)
  Proof.
H: Funext
σ: Signature
I: Type
A: I -> Algebra σ
C: Algebra σ
H0: forall i : I, IsHSetAlgebra (A i)
(forall i : I, Homomorphism C (A i)) <~>
Homomorphism C (ProdAlgebra I A)
    apply (equiv_adjointify hom_prod_algebra_mapin hom_prod_algebra_mapout).
H: Funext
σ: Signature
I: Type
A: I -> Algebra σ
C: Algebra σ
H0: forall i : I, IsHSetAlgebra (A i)
(λ x : Homomorphism C (ProdAlgebra I A),
 hom_prod_algebra_mapin (hom_prod_algebra_mapout x)) ==
idmap
H: Funext
σ: Signature
I: Type
A: I -> Algebra σ
C: Algebra σ
H0: forall i : I, IsHSetAlgebra (A i)
(λ x : forall i : I, Homomorphism C (A i),
 hom_prod_algebra_mapout (hom_prod_algebra_mapin x)) ==
idmap
    -
H: Funext
σ: Signature
I: Type
A: I -> Algebra σ
C: Algebra σ
H0: forall i : I, IsHSetAlgebra (A i)
(λ x : Homomorphism C (ProdAlgebra I A),
 hom_prod_algebra_mapin (hom_prod_algebra_mapout x)) ==
idmap intro f.
H: Funext
σ: Signature
I: Type
A: I -> Algebra σ
C: Algebra σ
H0: forall i : I, IsHSetAlgebra (A i)
f: Homomorphism C (ProdAlgebra I A)
hom_prod_algebra_mapin (hom_prod_algebra_mapout f) = f by apply path_hset_homomorphism.
    -
H: Funext
σ: Signature
I: Type
A: I -> Algebra σ
C: Algebra σ
H0: forall i : I, IsHSetAlgebra (A i)
(λ x : forall i : I, Homomorphism C (A i),
 hom_prod_algebra_mapout (hom_prod_algebra_mapin x)) ==
idmap intro f.
H: Funext
σ: Signature
I: Type
A: I -> Algebra σ
C: Algebra σ
H0: forall i : I, IsHSetAlgebra (A i)
f: forall i : I, Homomorphism C (A i)
hom_prod_algebra_mapout (hom_prod_algebra_mapin f) = f funext i.
H: Funext
σ: Signature
I: Type
A: I -> Algebra σ
C: Algebra σ
H0: forall i : I, IsHSetAlgebra (A i)
f: forall i : I, Homomorphism C (A i)
i: I
hom_prod_algebra_mapout (hom_prod_algebra_mapin f) i =
f i by apply path_hset_homomorphism.
  Defined.
End ump_prod_algebra.

(** Binary product algebra. *)

Section bin_prod_algebra.
  Context `{Funext} {σ : Signature} (A B : Algebra σ).

  Definition bin_prod_algebras (b:Bool) : Algebra σ
    := if b then B else A.

  #[export] Instance trunc_bin_prod_algebras {n : trunc_index}
    `{!IsTruncAlgebra n A} `{!IsTruncAlgebra n B}
    : ∀ (b:Bool), IsTruncAlgebra n (bin_prod_algebras b).
H: Funext
σ: Signature
A, B: Algebra σ
n: trunc_index
IsTruncAlgebra0: IsTruncAlgebra n A
IsTruncAlgebra1: IsTruncAlgebra n B
forall b : Bool,
IsTruncAlgebra n (bin_prod_algebras b)
  Proof.
H: Funext
σ: Signature
A, B: Algebra σ
n: trunc_index
IsTruncAlgebra0: IsTruncAlgebra n A
IsTruncAlgebra1: IsTruncAlgebra n B
forall b : Bool,
IsTruncAlgebra n (bin_prod_algebras b)
    intros []; exact _.
  Qed.

  Definition BinProdAlgebra : Algebra σ :=
    ProdAlgebra Bool bin_prod_algebras.

  Definition fst_prod_algebra : Homomorphism BinProdAlgebra A
    := hom_proj_prod_algebra Bool bin_prod_algebras false.

  Definition snd_prod_algebra : Homomorphism BinProdAlgebra B
    := hom_proj_prod_algebra Bool bin_prod_algebras true.
End bin_prod_algebra.

Module prod_algebra_notations.
  Global Notation "A × B" := (BinProdAlgebra A B) : Algebra_scope.
End prod_algebra_notations.

Import prod_algebra_notations.

(** Specialization of the product algebra universal mapping property
    to binary product. *)

Section ump_bin_prod_algebra.
  Context
    `{Funext}
    {σ : Signature}
    (A B C : Algebra σ)
    `{!IsHSetAlgebra A} `{!IsHSetAlgebra B}.

 Lemma ump_bin_prod_algebra
   : Homomorphism C A * Homomorphism C B <~> Homomorphism C (A × B).
H: Funext
σ: Signature
A, B, C: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra A
IsHSetAlgebra1: IsHSetAlgebra B
Homomorphism C A * Homomorphism C B <~>
Homomorphism C (A × B)
  Proof.
H: Funext
σ: Signature
A, B, C: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra A
IsHSetAlgebra1: IsHSetAlgebra B
Homomorphism C A * Homomorphism C B <~>
Homomorphism C (A × B)
    set (k := λ (b:Bool), Homomorphism C (bin_prod_algebras A B b)).
H: Funext
σ: Signature
A, B, C: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra A
IsHSetAlgebra1: IsHSetAlgebra B
k:= λ b : Bool,
Homomorphism C (bin_prod_algebras A B b): Bool -> Type
Homomorphism C A * Homomorphism C B <~>
Homomorphism C (A × B)
    exact (equiv_compose
            (ump_prod_algebra Bool (bin_prod_algebras A B) C)
            (equiv_bool_forall_prod k)^-1).
  Defined.
End ump_bin_prod_algebra.