Algebra.v

(** 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 Existing Instance hset_sort. Global Existing Instance hset_symbol. 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 Existing Instance 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

now 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.