Homomorphisms of algebras

module universal-algebra.homomorphisms-of-algebras where
Imports
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.universe-levels

open import linear-algebra.functoriality-vectors
open import linear-algebra.vectors

open import universal-algebra.algebraic-theories
open import universal-algebra.algebras-of-theories
open import universal-algebra.signatures

Idea

An algebra homomorphism from one algebra to another is a function between their underlying types such that all the structure is preserved.

Definitions

module _
  { l1 : Level} ( Sg : signature l1)
  { l2 : Level} ( Th : Theory Sg l2)
  { l3 l4 : Level}
  ( Alg1 : Algebra Sg Th l3)
  ( Alg2 : Algebra Sg Th l4)
  where

  preserves-operations-Algebra :
    (type-Algebra Sg Th Alg1  type-Algebra Sg Th Alg2) 
    UU (l1  l3  l4)
  preserves-operations-Algebra f =
    ( op : operation-signature Sg) 
    ( v : vec (type-Algebra Sg Th Alg1)
      ( arity-operation-signature Sg op)) 
        ( f (is-model-set-Algebra Sg Th Alg1 op v) 
          ( is-model-set-Algebra Sg Th Alg2 op (map-vec f v)))

  type-hom-Algebra : UU (l1  l3  l4)
  type-hom-Algebra =
    Σ ( type-Algebra Sg Th Alg1  type-Algebra Sg Th Alg2)
      ( preserves-operations-Algebra)

  map-hom-Algebra :
    type-hom-Algebra 
    type-Algebra Sg Th Alg1 
    type-Algebra Sg Th Alg2
  map-hom-Algebra = pr1

  preserves-operations-hom-Algebra :
    ( f : type-hom-Algebra) 
    preserves-operations-Algebra (map-hom-Algebra f)
  preserves-operations-hom-Algebra = pr2