Library HoTT.Classes.interfaces.ua_algebra

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.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 Algebras. In particular a signature specifies which operations (functions) an algebra for the signature is expected to provide. A signature consists of

A type of Sorts. 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.

Global Instance trunc_operation `{Funext} {σ : Signature}
  (A : Carriers σ) {n} `{!∀ s , IsTrunc n (A s )} (w : SymbolType σ)
  : IsTrunc n (Operation A w).
Proof.
  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 σ.
Proof.
  issig.
Defined.

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

Global Existing Instance trunc_carriers_algebra.

Notation IsHSetAlgebra := (IsTruncAlgebra 0).

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

Global Instance trunc_algebra_succ {σ : Signature} (A : Algebra σ)
  {n} `{!IsTruncAlgebra n A}
  : IsTruncAlgebra n .+1 A | 1000.
Proof.
  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.
Proof.
  destruct A,B. cbn in ×. 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.
Proof.
  destruct A as [A a], B as [B b]. cbn in ×. 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.
Proof.
  set (e := (equiv_ap (issig_algebra σ)^-1 A B)).
  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.
Proof.
  apply path_path_algebra.
  unshelve eapply path_path_sigma.
  - transitivity (ap carriers p); [by destruct p |].
    transitivity (ap carriers q); [exact r | by destruct q].
  - 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.