ALGEBRAIC STRUCTURE

Results presented here are formalized in Ground Zero library using Lean Theorem Prover.

ALGEBRA

Definition. Signature over given types (called indices) is an element of type .
Where denotes coproduct type.

Definition. Vector of length over type (denoted ) is a type:
Where denotes unit type that contains only .

Definition. Assume we have types , function , and a natural number . Then we define function :

Definition. -ary algebraic operation over given type is an element of type:

Definition. -ary algebraic relation over given type is an element of type:
Where denotes type of all propositions, i.e.

Definition. Algebraic structure over signature constists of: (i) 0-Type called carrier, (ii) -ary algebraic operation for each , (iii) -ary algebraic relation for each .
Or, more explicitly:
We will write for carrier of algebraic structure , for its algebraic operations, and for its relations.

Mappings

(Homomorphism). Given two algebraic structures over signature and a function between them , we say that is homomorphism iff holds:
(i) ,
(ii) ,
for each or and .

Composition of two homomorphisms is also homomorphism.

(Isomorphism). We say that is an ismorphism iff it is bijective and homomorphism. Then we can say that and are isomorphic and write .

Isomorphism is an equivalence relation, i.e.
(i) ,
(ii) ,
(iii) .

(Univalence for Algebraic Structures).