(** This file defines [Algebra], which is a generalization of group,
    ring, module, etc. An [Algebra] moreover generalizes structures
    with infinitary operations, such as infinite complete lattice. *)

Local Unset Elimination Schemes.

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

Require Import
  HoTT.Types.

Declare Scope Algebra_scope.
Delimit Scope Algebra_scope with Algebra.

(** The below definition [SymbolTypeOf] is used to specify algebra
    operations. See [SymbolType] and [Operation] below. *)

Record SymbolTypeOf {Sort : Type} := Build_SymbolTypeOf
  { Arity : Type
  ; sorts_dom : Arity -> Sort
  ; sort_cod : Sort }.

Arguments SymbolTypeOf : clear implicits.
Arguments Build_SymbolTypeOf {Sort}.

(** A [Signature] is used to specify [Algebra]s. A signature describes
    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 provides
      a type for each [Sort] element.
    - A type of function symbols [Symbol]. For each function symbol
      [u : Symbol], an algebra for the signature provides a
      corresponding operation.
    - The field [symbol_types σ u] indicates which type the operation
      corresponding to [u] is expected to have. *)

Record Signature := Build_Signature
  { Sort : Type
  ; Symbol : Type
  ; symbol_types : Symbol -> SymbolTypeOf Sort
  ; hset_sort :: IsHSet Sort
  ; hset_symbol :: IsHSet Symbol }.

Notation SymbolType σ := (SymbolTypeOf (Sort σ)).

Global Coercion symbol_types : Signature >-> Funclass.

(** Each [Algebra] has a collection of carrier types [Carriers σ],
    indexed by the type of sorts [Sort σ]. *)

Notation Carriers σ := (Sort σ -> Type).

(** Given [A : Carriers σ] and [w : SymbolType σ], the domain of an
    algebra operation [DomOperation A w] is a product of carrier types
    from [A], indexed by [Arity w]. *)

Notation DomOperation A w
  := (forall i : Arity w, A (sorts_dom w i)) (only parsing).

(** Given a symbol type [w : SymbolType σ], an algebra with carriers
    [A : Carriers σ] provides a corresponding operation of type
    [Operation A w]. See below for definition [Algerba].

    Algebra operations are developed further in
    [HoTT.Algebra.Universal.Operation]. *)

Definition Operation {σ} (A : Carriers σ) (w : SymbolType σ) : Type
  := DomOperation A w -> A (sort_cod w).

(** An [Algebra σ] for a signature [σ] consists of a collection of
    carriers [Carriers σ], and for each symbol [u : Symbol σ], an
    operation/function of type [Operation carriers (σ u)],
    where [σ u : SymbolType σ] is the symbol type of [u].
    Notice that [Algebra] does not specify equations involving
    carriers and operations. Equations are defined elsewhere. *)

Record Algebra {σ : Signature} : Type := Build_Algebra
  { carriers : Carriers σ
  ; operations : forall (u : Symbol σ), Operation carriers (σ u)
  ; hset_algebra :: forall (s : Sort σ), IsHSet (carriers s) }.

Arguments Algebra : clear implicits.

Arguments Build_Algebra {σ} carriers operations {hset_algebra}.

Global Coercion carriers : Algebra >-> Funclass.

Bind Scope Algebra_scope with Algebra.

Definition SigAlgebra (σ : Signature) : Type
  := {c : Carriers σ
        | { _ : forall (u : Symbol σ), Operation c (σ u)
              | forall (s : Sort σ), IsHSet (c s) } }.

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

Lemma path_algebra `{Funext} {σ : Signature} (A B : Algebra σ)
  (p : carriers A = carriers B)
  (q : transport (fun i => forall u, Operation i (σ u)) p (operations A)
       = operations B)
  : A = B.
H: Funext
σ: Signature
A, B: Algebra σ
p: A = B
q: transport
  (fun i : Carriers σ =>
   forall u : Symbol σ, Operation i (σ u)) p
  (operations A) = operations B
A = B
Proof.
H: Funext
σ: Signature
A, B: Algebra σ
p: A = B
q: transport
  (fun i : Carriers σ =>
   forall u : Symbol σ, Operation i (σ u)) p
  (operations A) = operations B
A = B
  apply (ap (issig_algebra σ)^-1)^-1; cbn.
H: Funext
σ: Signature
A, B: Algebra σ
p: A = B
q: transport
  (fun i : Carriers σ =>
   forall u : Symbol σ, Operation i (σ u)) p
  (operations A) = operations B
(A; operations A; hset_algebra A) =
(B; operations B; hset_algebra B)
  apply (path_sigma' _ p).
H: Funext
σ: Signature
A, B: Algebra σ
p: A = B
q: transport
  (fun i : Carriers σ =>
   forall u : Symbol σ, Operation i (σ u)) p
  (operations A) = operations B
transport
  (fun c : Carriers σ =>
   {_ : forall u : Symbol σ, Operation c (σ u) &
   forall s : Sort σ, IsHSet (c s)}) p
  (operations A; hset_algebra A) =
(operations B; hset_algebra B)
  refine (transport_sigma p _ @ _).
H: Funext
σ: Signature
A, B: Algebra σ
p: A = B
q: transport
  (fun i : Carriers σ =>
   forall u : Symbol σ, Operation i (σ u)) p
  (operations A) = operations B
(transport
   (fun x : Carriers σ =>
    forall u : Symbol σ, Operation x (σ u)) p
   (operations A; hset_algebra A).1;
transportD
  (fun x : Carriers σ =>
   forall u : Symbol σ, Operation x (σ u))
  (fun (x : Carriers σ)
     (_ : forall u : Symbol σ, Operation x (σ u)) =>
   forall s : Sort σ, IsHSet (x s)) p
  (operations A; hset_algebra A).1
  (operations A; hset_algebra A).2) =
(operations B; hset_algebra B)
  apply path_sigma_hprop.
H: Funext
σ: Signature
A, B: Algebra σ
p: A = B
q: transport
  (fun i : Carriers σ =>
   forall u : Symbol σ, Operation i (σ u)) p
  (operations A) = operations B
(transport
   (fun x : Carriers σ =>
    forall u : Symbol σ, Operation x (σ u)) p
   (operations A; hset_algebra A).1;
transportD
  (fun x : Carriers σ =>
   forall u : Symbol σ, Operation x (σ u))
  (fun (x : Carriers σ)
     (_ : forall u : Symbol σ, Operation x (σ u)) =>
   forall s : Sort σ, IsHSet (x s)) p
  (operations A; hset_algebra A).1
  (operations A; hset_algebra A).2).1 =
(operations B; hset_algebra B).1
  exact q.
Defined.

Arguments path_algebra {_} {_} (A B)%_Algebra_scope (p q)%_path_scope.

Lemma path_ap_carriers_path_algebra `{Funext} {σ} (A B : Algebra σ)
  (p : carriers A = carriers B)
  (q : transport (fun i => forall u, Operation i (σ u)) p (operations A)
       = operations B)
  : ap carriers (path_algebra A B p q) = p.
H: Funext
σ: Signature
A, B: Algebra σ
p: A = B
q: transport
  (fun i : Carriers σ =>
   forall u : Symbol σ, Operation i (σ u)) p
  (operations A) = operations B
ap carriers (path_algebra A B p q) = p
Proof.
H: Funext
σ: Signature
A, B: Algebra σ
p: A = B
q: transport
  (fun i : Carriers σ =>
   forall u : Symbol σ, Operation i (σ u)) p
  (operations A) = operations B
ap carriers (path_algebra A B p q) = p
  destruct A as [A a ha], B as [B b hb]; cbn in p, q.
H: Funext
σ: Signature
A: Carriers σ
a: forall u : Symbol σ, Operation A (σ u)
ha: forall s : Sort σ, IsHSet (A s)
B: Carriers σ
b: forall u : Symbol σ, Operation B (σ u)
hb: forall s : Sort σ, IsHSet (B s)
p: A = B
q: transport
  (fun i : Carriers σ =>
   forall u : Symbol σ, Operation i (σ u)) p a = b
ap carriers
  (path_algebra
     {|
       carriers := A;
       operations := a;
       hset_algebra := ha
     |}
     {|
       carriers := B;
       operations := b;
       hset_algebra := hb
     |} p q) = p
  destruct p, q.
H: Funext
σ: Signature
A: Carriers σ
a: forall u : Symbol σ, Operation A (σ u)
ha, hb: forall s : Sort σ, IsHSet (A s)
ap carriers
  (path_algebra
     {|
       carriers := A;
       operations := a;
       hset_algebra := ha
     |}
     {|
       carriers := A;
       operations :=
         transport
           (fun i : Carriers σ =>
            forall u : Symbol σ, Operation i (σ u)) 1
           a;
       hset_algebra := hb
     |} 1 1) = 1
  unfold path_algebra, path_sigma_hprop, path_sigma_uncurried.
H: Funext
σ: Signature
A: Carriers σ
a: forall u : Symbol σ, Operation A (σ u)
ha, hb: forall s : Sort σ, IsHSet (A s)
ap carriers
  ((ap (issig_algebra σ)^-1)^-1
     (path_sigma'
        (fun c : Carriers σ =>
         {_ : forall u : Symbol σ, Operation c (σ u) &
         forall s : Sort σ, IsHSet (c s)}) 1
        (transport_sigma 1 (a; ha) @
         match
           (pr1^-1 1).2 in (_ = v2)
           return
             ((transport
                 (fun x : Carriers σ =>
                  forall u : Symbol σ,
                  Operation x (σ u)) 1 (a; ha).1;
              transportD
                (fun x : Carriers σ =>
                 forall u : Symbol σ,
                 Operation x (σ u))
                (fun (x : Carriers σ)
                   (_ : forall u : Symbol σ,
                        Operation x (σ u)) =>
                 forall s : Sort σ, IsHSet (x s)) 1
                (a; ha).1 (a; ha).2) =
              ((transport
                  (fun i : Carriers σ =>
                   forall u : Symbol σ,
                   Operation i (σ u)) 1 a; hb).1; v2))
         with
         | 1 =>
             match
               (pr1^-1 1).1 as p in (_ = v1)
               return
                 ((transport
                     (fun x : Carriers σ =>
                      forall u : Symbol σ,
                      Operation x (σ u)) 1 (a; ha).1;
                  transportD
                    (fun x : Carriers σ =>
                     forall u : Symbol σ,
                     Operation x (σ u))
                    (fun (x : Carriers σ)
                       (_ : forall u : Symbol σ,
                            Operation x (σ u)) =>
                     forall s : Sort σ, IsHSet (x s))
                    1 (a; ha).1 (a; ha).2) =
                  (v1;
                  transport
                    (fun
                       _ : forall u : Symbol σ,
                           Operation
                             {|
                               carriers := A;
                               operations := ...;
                               hset_algebra := hb
                             |} (σ u) =>
                     forall s : Sort σ,
                     IsHSet
                       ({|
                          carriers := A;
                          operations := ...;
                          hset_algebra := hb
                        |} s)) p
                    (transport
                       (fun x : Carriers σ =>
                        forall u : Symbol σ,
                        Operation x (σ u)) 1 (a; ha).1;
                    transportD
                      (fun x : Carriers σ =>
                       forall u : Symbol σ,
                       Operation x (σ u))
                      (fun (x : Carriers σ)
                         (_ : forall u : Symbol σ,
                              Operation x (...)) =>
                       forall s : Sort σ, IsHSet (x s))
                      1 (a; ha).1 (a; ha).2).2))
             with
             | 1 => 1
             end
         end))) = 1
  cbn -[center].
H: Funext
σ: Signature
A: Carriers σ
a: forall u : Symbol σ, Operation A (σ u)
ha, hb: forall s : Sort σ, IsHSet (A s)
ap carriers
  ((1 @
    ap
      (fun u : SigAlgebra σ =>
       {|
         carriers := u.1;
         operations := (u.2).1;
         hset_algebra := (u.2).2
       |})
      (path_sigma'
         (fun c : Carriers σ =>
          {_ : forall u : Symbol σ, Operation c (σ u)
          & forall s : Sort σ, IsHSet (c s)}) 1
         (1 @
          match
            center (ha = hb) in (_ = v2)
            return ((a; ha) = (a; v2))
          with
          | 1 => 1
          end))) @ 1) = 1
  by destruct (center (ha = hb)).
Defined.

Arguments path_ap_carriers_path_algebra {_} {_} (A B)%_Algebra_scope (p q)%_path_scope.

Lemma path_path_algebra_issig {σ : 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.

Arguments path_path_algebra_issig {_} {A B}%_Algebra_scope (p q r)%_path_scope.

Lemma path_path_algebra `{Funext} {σ} {A B : Algebra σ}
  (p q : A = B) (r : ap carriers p = ap carriers q)
  : p = q.
H: Funext
σ: Signature
A, B: Algebra σ
p, q: A = B
r: ap carriers p = ap carriers q
p = q
Proof.
H: Funext
σ: Signature
A, B: Algebra σ
p, q: A = B
r: ap carriers p = ap carriers q
p = q
  apply path_path_algebra_issig.
H: Funext
σ: Signature
A, B: Algebra σ
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 σ
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 σ
p, q: A = B
r: ap carriers p = ap carriers q
transport
  (fun
     x : ((issig_algebra σ)^-1 A).1 =
         ((issig_algebra σ)^-1 B).1 =>
   transport
     (fun c : Carriers σ =>
      {_ : forall u : Symbol σ, Operation c (σ u) &
      forall s : Sort σ, IsHSet (c s)}) 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 σ
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 σ
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 σ
p, q: A = B
r: ap carriers p = ap carriers q
transport
  (fun
     x : ((issig_algebra σ)^-1 A).1 =
         ((issig_algebra σ)^-1 B).1 =>
   transport
     (fun c : Carriers σ =>
      {_ : forall u : Symbol σ, Operation c (σ u) &
      forall s : Sort σ, IsHSet (c s)}) x
     ((issig_algebra σ)^-1 A).2 =
   ((issig_algebra σ)^-1 B).2)
  (match
     p in (_ = a)
     return
       (forall q : A = a,
        ap carriers p = ap carriers q ->
        (ap (issig_algebra σ)^-1 p) ..1 =
        ap carriers p)
   with
   | 1 =>
       fun (q : A = A)
         (_ : ap carriers 1 = ap carriers q) => 1
   end q r @
   (r @
    match
      q as p in (_ = a)
      return
        (forall p0 : A = a,
         ap carriers p0 = ap carriers p ->
         ap carriers p =
         (ap (issig_algebra σ)^-1 p) ..1)
    with
    | 1 =>
        fun (p : A = A)
          (_ : ap carriers p = ap carriers 1) => 1
    end p r)) (ap (issig_algebra σ)^-1 p) ..2 =
(ap (issig_algebra σ)^-1 q) ..2 apply path_ishprop.
Defined.

Arguments path_path_algebra {_} {σ} {A B}%_Algebra_scope (p q r)%_path_scope.

Global Notation "u .# A" := (operations A u) : Algebra_scope.