Timings for ua_prod_algebra.v

Require Import
  HoTT.Types.Bool
  HoTT.Classes.theory.ua_homomorphism.

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.

  Global Instance trunc_prod_algebra {n : trunc_index}
    `{!∀ i, IsTruncAlgebra n (A i)}
    : IsTruncAlgebra n ProdAlgebra.
  Proof.
    intro 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) α.
  Proof.
    induction w.
    -
 exact P.
    -
 intro p.
 apply (IHw (λ i, v i (p i)) (α (p i))).
 f_ap.
  Defined.

  Global Instance is_homomorphism_proj_prod_algebra (i:I)
    : IsHomomorphism (def_proj_prod_algebra i).
  Proof.
    intro u.
    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 univarsal 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)).
  Proof.
    induction w.
    -
 funext i.
 apply P.
    -
 intro x.
 apply IHw.
 intro i.
 apply P.
  Defined.

  Global Instance is_homomorphism_prod_algebra_mapin
    (f : ∀ (i:I), Homomorphism C (A i))
    : IsHomomorphism (def_prod_algebra_mapin f).
  Proof.
    intro u.
    apply oppreserving_prod_algebra_mapin.
    intro 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).
  Proof.
    apply (equiv_adjointify hom_prod_algebra_mapin hom_prod_algebra_mapout).
    -
 intro f.
 by apply path_hset_homomorphism.
    -
 intro f.
 funext 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.

  Global Instance trunc_bin_prod_algebras {n : trunc_index}
    `{!IsTruncAlgebra n A} `{!IsTruncAlgebra n B}
    : ∀ (b:Bool), IsTruncAlgebra n (bin_prod_algebras b).
  Proof.
    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.

(** Specialisation of the product algebra univarsal 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).
  Proof.
    set (k := λ (b:Bool), Homomorphism C (bin_prod_algebras A B 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.