(** This file defines [Algebra]. *)

Require Export
  HoTT.Utf8Minimal
  HoTT.Basics
  HoTT.Classes.implementations.ne_list
  HoTT.Classes.implementations.family_prod.

Require Import
  HoTT.Types
  HoTT.Universes.HSet
  HoTT.Spaces.List.Core.

Import ne_list.notations.

Declare Scope Algebra_scope.

Delimit Scope Algebra_scope with Algebra.

Open Scope Algebra_scope.

Definition SymbolType_internal : Type → Type := ne_list.

(** A [Signature] is used to characterise [Algebra]s. In particular
    a signature specifies which operations (functions) an algebra for
    the signature is expected to provide. A signature consists of
    - A type of [Sort]s. An algebra for the signature must provide
      a type for each [s : Sort].
    - A type of function symbols [Symbol]. For each function symbol
      [u : Symbol], an algebra for the signature must provide a
      corresponding operation.
    - The field [symbol_types σ u] indicates which type the operation
      corresponding to [u] should have. *)

Record Signature : Type := BuildSignature
  { Sort : Type
  ; Symbol : Type
  ; symbol_types : Symbol → SymbolType_internal Sort }.

(** We have this implicit coercion allowing us to use a signature
    [σ:Signature] as a map [Symbol σ → SymbolType σ]
    (see [SymbolType] below). *)

Global Coercion symbol_types : Signature >-> Funclass.

(** A single sorted [Signature] is a signature with [Sort = Unit]. *)

Definition BuildSingleSortedSignature (sym : Type) (arities : sym → nat)
  : Signature
  := BuildSignature Unit sym (ne_list.replicate_Sn tt o arities).

(** Let [σ:Signature]. For each symbol [u : Symbol σ], [σ u]
    associates [u] to a [SymbolType σ]. This represents the required
    type of the algebra operation corresponding to [u]. *)

Definition SymbolType (σ : Signature) : Type := ne_list (Sort σ).

(** For [s : SymbolType σ], [cod_symboltype σ] is the codomain of the
    symbol type [s]. *)

Definition cod_symboltype {σ} : SymbolType σ → Sort σ
  := ne_list.last.

(** For [s : SymbolType σ], [cod_symboltype σ] is the domain of the
    symbol type [s]. *)

Definition dom_symboltype {σ} : SymbolType σ → list (Sort σ)
  := ne_list.front.

(** For [s : SymbolType σ], [cod_symboltype σ] is the arity of the
    symbol type [s]. That is the number [n:nat] of arguments of the
    [SymbolType σ]. *)

Definition arity_symboltype {σ} : SymbolType σ → nat
  := length o dom_symboltype.

(** An [Algebra] must provide a family of [Carriers σ] indexed by
    [Sort σ]. These carriers are the "objects" (types) of the algebra. *)

(* [Carriers] is a notation because it will be used for an implicit
   coercion [Algebra >-> Funclass] below. *)

Notation Carriers σ := (Sort σ → Type).

(** The function [Operation] maps a family of carriers [A : Carriers σ]
    and [w : SymbolType σ] to the corresponding function type.

<<
      Operation A [:s1; s2; ...; sn; t:] = A s1 → A s2 → ... → A sn → A t
>>

    where [[:s1; s2; ...; sn; t:] : SymbolType σ] is a symbol type
    with domain [[s1; s2; ...; sn]] and codomain [t]. *)

Fixpoint Operation {σ} (A : Carriers σ) (w : SymbolType σ) : Type
  := match w with
     | [:s:] => A s
     | s ::: w' => A s → Operation A w'
     end.

Instance trunc_operation `{Funext} {σ : Signature}
  (A : Carriers σ) {n} `{!∀ s, IsTrunc n (A s)} (w : SymbolType σ)
  : IsTrunc n (Operation A w).
H: Funext
σ: Signature
A: Carriers σ
n: trunc_index
H0: forall s : Sort σ, IsTrunc n (A s)
w: SymbolType σ
IsTrunc n (Operation A w)
Proof.
H: Funext
σ: Signature
A: Carriers σ
n: trunc_index
H0: forall s : Sort σ, IsTrunc n (A s)
w: SymbolType σ
IsTrunc n (Operation A w)
  induction w; exact _.
Defined.

(** Uncurry of an [f : Operation A w], such that

<<
      ap_operation f (x1,x2,...,xn) = f x1 x2 ... xn
>>
*)

Fixpoint ap_operation {σ} {A : Carriers σ} {w : SymbolType σ}
    : Operation A w →
      FamilyProd A (dom_symboltype w) →
      A (cod_symboltype w)
    := match w with
       | [:s:] => λ f _, f
       | s ::: w' => λ f '(x, l), ap_operation (f x) l
       end.

(** Funext for uncurried [Operation A w]. If

<<
      ap_operation f (x1,x2,...,xn) = ap_operation g (x1,x2,...,xn)
>>

    for all [(x1,x2,...,xn) : A s1 * A s2 * ... * A sn], then [f = g]. *)

Fixpoint path_forall_ap_operation `{Funext} {σ : Signature}
  {A : Carriers σ} {w : SymbolType σ}
  : ∀ (f g : Operation A w),
    (∀ a : FamilyProd A (dom_symboltype w),
       ap_operation f a = ap_operation g a)
    -> f = g
  := match w with
     | [:s:] => λ (f g : A s) p, p tt
     | s ::: w' =>
         λ (f g : A s → Operation A w') p,
          path_forall f g
            (λ x, path_forall_ap_operation (f x) (g x) (λ a, p (x,a)))
     end.

(** An [Algebra σ] for a signature [σ] consists of a family [carriers :
    Carriers σ] indexed by the sorts [s : Sort σ], and for each symbol
    [u : Symbol σ], an operation of type [Operation carriers (σ u)],
    where [σ u : SymbolType σ] is the symbol type of [u]. *)

Record Algebra {σ : Signature} : Type := BuildAlgebra
  { carriers : Carriers σ
  ; operations : ∀ (u : Symbol σ), Operation carriers (σ u) }.

Arguments Algebra : clear implicits.

Arguments BuildAlgebra {σ} carriers operations.

(** We have a convenient implicit coercion from an algebra to the
    family of carriers. *)
Global Coercion carriers : Algebra >-> Funclass.

Bind Scope Algebra_scope with Algebra.

Definition SigAlgebra (σ : Signature) : Type
  := {c : Carriers σ | ∀ (u : Symbol σ), Operation c (σ u) }.

Lemma issig_algebra (σ : Signature) : SigAlgebra σ <~> Algebra σ.
σ: Signature
SigAlgebra σ <~> Algebra σ
Proof.
σ: Signature
SigAlgebra σ <~> Algebra σ
  issig.
Defined.

Class IsTruncAlgebra (n : trunc_index) {σ : Signature} (A : Algebra σ)
  := trunc_carriers_algebra :: ∀ (s : Sort σ), IsTrunc n (A s).

Notation IsHSetAlgebra := (IsTruncAlgebra 0).

Instance hprop_is_trunc_algebra `{Funext} (n : trunc_index)
  {σ : Signature} (A : Algebra σ)
  : IsHProp (IsTruncAlgebra n A).
H: Funext
n: trunc_index
σ: Signature
A: Algebra σ
IsHProp (IsTruncAlgebra n A)
Proof.
H: Funext
n: trunc_index
σ: Signature
A: Algebra σ
IsHProp (IsTruncAlgebra n A)
  apply istrunc_forall.
Qed.

Instance trunc_algebra_succ {σ : Signature} (A : Algebra σ)
  {n} `{!IsTruncAlgebra n A}
  : IsTruncAlgebra n.+1 A | 1000.
σ: Signature
A: Algebra σ
n: trunc_index
IsTruncAlgebra0: IsTruncAlgebra n A
IsTruncAlgebra n.+1 A
Proof.
σ: Signature
A: Algebra σ
n: trunc_index
IsTruncAlgebra0: IsTruncAlgebra n A
IsTruncAlgebra n.+1 A
  intro; exact _.
Qed.

(** To find a path between two algebras [A B : Algebra σ] it suffices
    to find paths between the carriers and the operations. *)

Lemma path_algebra {σ : Signature} (A B : Algebra σ)
  (p : carriers A = carriers B)
  (q : transport (λ X, ∀ u, Operation X (σ u)) p (operations A)
       = operations B)
  : A = B.
σ: Signature
A, B: Algebra σ
p: A = B
q: transport (λ X : Carriers σ, forall u : Symbol σ, Operation X (σ u)) p
  (operations A) =
operations B
A = B
Proof.
σ: Signature
A, B: Algebra σ
p: A = B
q: transport (λ X : Carriers σ, forall u : Symbol σ, Operation X (σ u)) p
  (operations A) =
operations B
A = B
  destruct A,B.
σ: Signature
carriers0: Carriers σ
operations0: forall u : Symbol σ, Operation carriers0 (σ u)
carriers1: Carriers σ
operations1: forall u : Symbol σ, Operation carriers1 (σ u)
p: {| carriers := carriers0; operations := operations0 |} =
{| carriers := carriers1; operations := operations1 |}
q: transport (λ X : Carriers σ, forall u : Symbol σ, Operation X (σ u)) p
  (operations {| carriers := carriers0; operations := operations0 |}) =
operations {| carriers := carriers1; operations := operations1 |}
{| carriers := carriers0; operations := operations0 |} =
{| carriers := carriers1; operations := operations1 |} cbn in *.
σ: Signature
carriers0: Carriers σ
operations0: forall u : Symbol σ, Operation carriers0 (σ u)
carriers1: Carriers σ
operations1: forall u : Symbol σ, Operation carriers1 (σ u)
p: carriers0 = carriers1
q: transport (λ X : Carriers σ, forall u : Symbol σ, Operation X (σ u)) p
  operations0 =
operations1
{| carriers := carriers0; operations := operations0 |} =
{| carriers := carriers1; operations := operations1 |} by path_induction.
Defined.

Lemma path_ap_carriers_path_algebra {σ} (A B : Algebra σ)
  (p : carriers A = carriers B)
  (q : transport (λ X, ∀ u, Operation X (σ u)) p (operations A)
       = operations B)
  : ap carriers (path_algebra A B p q) = p.
σ: Signature
A, B: Algebra σ
p: A = B
q: transport (λ X : Carriers σ, forall u : Symbol σ, Operation X (σ u)) p
  (operations A) =
operations B
ap carriers (path_algebra A B p q) = p
Proof.
σ: Signature
A, B: Algebra σ
p: A = B
q: transport (λ X : Carriers σ, forall u : Symbol σ, Operation X (σ u)) p
  (operations A) =
operations B
ap carriers (path_algebra A B p q) = p
  destruct A as [A a], B as [B b].
σ: Signature
A: Carriers σ
a: forall u : Symbol σ, Operation A (σ u)
B: Carriers σ
b: forall u : Symbol σ, Operation B (σ u)
p: {| carriers := A; operations := a |} = {| carriers := B; operations := b |}
q: transport (λ X : Carriers σ, forall u : Symbol σ, Operation X (σ u)) p
  (operations {| carriers := A; operations := a |}) =
operations {| carriers := B; operations := b |}
ap carriers
  (path_algebra {| carriers := A; operations := a |}
     {| carriers := B; operations := b |} p q) =
p cbn in *.
σ: Signature
A: Carriers σ
a: forall u : Symbol σ, Operation A (σ u)
B: Carriers σ
b: forall u : Symbol σ, Operation B (σ u)
p: A = B
q: transport (λ X : Carriers σ, forall u : Symbol σ, Operation X (σ u)) p a = b
ap carriers
  (path_algebra {| carriers := A; operations := a |}
     {| carriers := B; operations := b |} p q) =
p by destruct p,q.
Defined.

(** Suppose [p],[q] are paths in [Algebra σ]. To show that [p = q] it
    suffices to find a path [r] between the paths corresponding to
    [p] and [q] in [SigAlgebra σ]. *)

Lemma path_path_algebra {σ : Signature} {A B : Algebra σ} (p q : A = B)
  (r : ap (issig_algebra σ)^-1 p = ap (issig_algebra σ)^-1 q)
  : p = q.
σ: Signature
A, B: Algebra σ
p, q: A = B
r: ap (issig_algebra σ)^-1 p = ap (issig_algebra σ)^-1 q
p = q
Proof.
σ: Signature
A, B: Algebra σ
p, q: A = B
r: ap (issig_algebra σ)^-1 p = ap (issig_algebra σ)^-1 q
p = q
  set (e := (equiv_ap (issig_algebra σ)^-1 A B)).
σ: Signature
A, B: Algebra σ
p, q: A = B
r: ap (issig_algebra σ)^-1 p = ap (issig_algebra σ)^-1 q
e:= equiv_ap (issig_algebra σ)^-1 A B: A = B <~> (issig_algebra σ)^-1 A = (issig_algebra σ)^-1 B
p = q
  by apply (@equiv_inv _ _ (ap e) (Equivalences.isequiv_ap _ _)).
Defined.

(** If [p q : A = B] and [IsHSetAlgebra B].
    Then [ap carriers p = ap carriers q] implies [p = q]. *)

Lemma path_path_hset_algebra `{Funext} {σ : Signature}
  {A B : Algebra σ} `{IsHSetAlgebra B}
  (p q : A = B) (r : ap carriers p = ap carriers q)
  : p = q.
H: Funext
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
p, q: A = B
r: ap carriers p = ap carriers q
p = q
Proof.
H: Funext
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
p, q: A = B
r: ap carriers p = ap carriers q
p = q
  apply path_path_algebra.
H: Funext
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
p, q: A = B
r: ap carriers p = ap carriers q
ap (issig_algebra σ)^-1 p = ap (issig_algebra σ)^-1 q
  unshelve eapply path_path_sigma.
H: Funext
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
p, q: A = B
r: ap carriers p = ap carriers q
(ap (issig_algebra σ)^-1 p) ..1 = (ap (issig_algebra σ)^-1 q) ..1
H: Funext
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
p, q: A = B
r: ap carriers p = ap carriers q
transport
  (λ x : ((issig_algebra σ)^-1 A).1 = ((issig_algebra σ)^-1 B).1,
   transport (λ c : Carriers σ, forall u : Symbol σ, Operation c (σ u)) x
     ((issig_algebra σ)^-1 A).2 =
   ((issig_algebra σ)^-1 B).2)
  ?r (ap (issig_algebra σ)^-1 p) ..2 =
(ap (issig_algebra σ)^-1 q) ..2
  -
H: Funext
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
p, q: A = B
r: ap carriers p = ap carriers q
(ap (issig_algebra σ)^-1 p) ..1 = (ap (issig_algebra σ)^-1 q) ..1 transitivity (ap carriers p); [by destruct p |].
H: Funext
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
p, q: A = B
r: ap carriers p = ap carriers q
ap carriers p = (ap (issig_algebra σ)^-1 q) ..1
    transitivity (ap carriers q); [exact r | by destruct q].
  -
H: Funext
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
p, q: A = B
r: ap carriers p = ap carriers q
transport
  (λ x : ((issig_algebra σ)^-1 A).1 = ((issig_algebra σ)^-1 B).1,
   transport (λ c : Carriers σ, forall u : Symbol σ, Operation c (σ u)) x
     ((issig_algebra σ)^-1 A).2 =
   ((issig_algebra σ)^-1 B).2)
  (match
     p as p0 in (_ = a)
     return
       (IsHSetAlgebra a ->
        forall q0 : A = a,
        ap carriers p0 = ap carriers q0 ->
        (ap (issig_algebra σ)^-1 p0) ..1 = ap carriers p0)
   with
   | 1 =>
       λ (_ : IsHSetAlgebra A) (q0 : A = A)
       (_ : ap carriers 1 = ap carriers q0), 1
   end IsHSetAlgebra0 q r @
   (r @
    match
      q as p0 in (_ = a)
      return
        (IsHSetAlgebra a ->
         forall p1 : A = a,
         ap carriers p1 = ap carriers p0 ->
         ap carriers p0 = (ap (issig_algebra σ)^-1 p0) ..1)
    with
    | 1 =>
        λ (_ : IsHSetAlgebra A) (p0 : A = A)
        (_ : ap carriers p0 = ap carriers 1), 1
    end IsHSetAlgebra0 p r))
  (ap (issig_algebra σ)^-1 p) ..2 =
(ap (issig_algebra σ)^-1 q) ..2 apply path_ishprop.
Defined.

Module algebra_notations.

(** Given [A : Algebra σ] and function symbol [u : Symbol σ], we use
    the notation [u .# A] to refer to the corresponding algebra
    operation of type [Operation A (σ u)]. *)
  Global Notation "u .# A" := (operations A u) : Algebra_scope.

End algebra_notations.