HoTT.Algebra.Universal.Algebra.v.alectryon.json

(** 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.

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 :=
                                 transport
                                   (fun i : Carriers σ =>
                                    forall u0 : Symbol σ, Operation i (σ u0))
                                   1 a;
                               hset_algebra := hb
                             |} (σ u) =>
                     forall s : Sort σ,
                     IsHSet
                       ({|
                          carriers := A;
                          operations :=
                            transport
                              (fun i : Carriers σ =>
                               forall u : Symbol σ, Operation i (σ u))
                              1 a;
                          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 (σ u)) =>
                       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 as p0 in (_ = a)
     return
       (forall q0 : A = a,
        ap carriers p0 = ap carriers q0 ->
        (ap (issig_algebra σ)^-1 p0) ..1 = ap carriers p0)
   with
   | 1 => fun (q0 : A = A) (_ : ap carriers 1 = ap carriers q0) => 1
   end q r @
   (r @
    match
      q as p0 in (_ = a)
      return
        (forall p1 : A = a,
         ap carriers p1 = ap carriers p0 ->
         ap carriers p0 = (ap (issig_algebra σ)^-1 p0) ..1)
    with
    | 1 => fun (p0 : A = A) (_ : ap carriers p0 = 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.