### Properties of Terms and the Term Algebra

This is the Terms.Properties module of the Agda Universal Algebra Library.

```{-# OPTIONS --without-K --exact-split --safe #-}

open import Algebras.Basic using ( π ; π₯ ; Signature )

module Terms.Properties {π : Signature π π₯} where

-- Imports from Agda and the Agda Standard Library --------------------------------------
open import Axiom.Extensionality.Propositional
using () renaming (Extensionality to funext)
open import Agda.Primitive         using ( Level ; _β_ ; lsuc ) renaming ( Set to Type )
open import Data.Product           using ( _,_ ; Ξ£-syntax )
open import Function.Base          using ( _β_ )
open import Data.Empty.Polymorphic using ( β₯ )
open import Relation.Binary        using ( IsEquivalence ; Setoid )
open import Relation.Binary.Definitions
using (Reflexive ; Symmetric ; Transitive )
open import Relation.Binary.PropositionalEquality
using ( _β‘_ ; refl ; module β‘-Reasoning ; cong )

-- Imports from the Agda Universal Algebra Library ----------------------------------------
open import Overture.Preliminaries      using ( _β»ΒΉ ; ππ ; β£_β£ ; β₯_β₯)
open import Overture.Inverses           using ( Inv ; InvIsInverseΚ³ ; Image_β_; eq )
open import Overture.Surjective         using ( IsSurjective )
open import Equality.Welldefined        using ( swelldef )
open import Algebras.Basic              using ( Algebra ; _Μ_ )
open import Algebras.Products   {π = π} using ( ov )
open import Homomorphisms.Basic {π = π} using ( hom )
open import Terms.Basic         {π = π}

private variable Ξ± Ξ² Ο : Level

```

#### The universal property

The term algebra `π» X` is absolutely free (or universal, or initial) for algebras in the signature `π`. That is, for every π-algebra `π¨`, the following hold.

1. Every function from `π` to `β£ π¨ β£` lifts to a homomorphism from `π» X` to `π¨`.
2. The homomorphism that exists by item 1 is unique.

We now prove this in Agda, starting with the fact that every map from `X` to `β£ π¨ β£` lifts to a map from `β£ π» X β£` to `β£ π¨ β£` in a natural way, by induction on the structure of the given term.

```private variable X : Type Ο

free-lift : (π¨ : Algebra Ξ± π)(h : X β β£ π¨ β£) β β£ π» X β£ β β£ π¨ β£
free-lift _ h (β x) = h x
free-lift π¨ h (node f π‘) = (f Μ π¨) (Ξ» i β free-lift π¨ h (π‘ i))

```

Naturally, at the base step of the induction, when the term has the form `generator` x, the free lift of `h` agrees with `h`. For the inductive step, when the given term has the form `node f π‘`, the free lift is defined as follows: Assuming (the induction hypothesis) that we know the image of each subterm `π‘ i` under the free lift of `h`, define the free lift at the full term by applying `f Μ π¨` to the images of the subterms.

The free lift so defined is a homomorphism by construction. Indeed, here is the trivial proof.

```lift-hom : (π¨ : Algebra Ξ± π) β (X β β£ π¨ β£) β hom (π» X) π¨
lift-hom π¨ h = free-lift π¨ h , Ξ» f a β cong (f Μ π¨) refl

```

Finally, we prove that the homomorphism is unique. This requires `funext π₯ Ξ±` (i.e., function extensionality at universe levels `π₯` and `Ξ±`) which we postulate by making it part of the premise in the following function type definition.

```open β‘-Reasoning

free-unique : swelldef π₯ Ξ± β (π¨ : Algebra Ξ± π)(g h : hom (π» X) π¨)
β            (β x β β£ g β£ (β x) β‘ β£ h β£ (β x))
----------------------------------------
β            β (t : Term X) β  β£ g β£ t β‘ β£ h β£ t

free-unique _ _ _ _ p (β x) = p x

free-unique wd π¨ g h p (node π π‘) =

β£ g β£ (node π π‘)    β‘β¨ β₯ g β₯ π π‘ β©
(π Μ π¨)(β£ g β£ β π‘)  β‘β¨ wd (π Μ π¨)(β£ g β£ β π‘)(β£ h β£ β π‘)(Ξ» i β free-unique wd π¨ g h p (π‘ i)) β©
(π Μ π¨)(β£ h β£ β π‘)  β‘β¨ (β₯ h β₯ π π‘)β»ΒΉ β©
β£ h β£ (node π π‘)    β

```

Letβs account for what we have proved thus far about the term algebra. If we postulate a type `X : Type Ο` (representing an arbitrary collection of variable symbols) such that for each `π`-algebra `π¨` there is a map from `X` to the domain of `π¨`, then it follows that for every `π`-algebra `π¨` there is a homomorphism from `π» X` to `β£ π¨ β£` that βagrees with the original map on `X`,β by which we mean that for all `x : X` the lift evaluated at `β x` is equal to the original function evaluated at `x`.

If we further assume that each of the mappings from `X` to `β£ π¨ β£` is surjective, then the homomorphisms constructed with `free-lift` and `lift-hom` are epimorphisms, as we now prove.

```lift-of-epi-is-epi : (π¨ : Algebra Ξ± π){hβ : X β β£ π¨ β£}
β                   IsSurjective hβ β IsSurjective β£ lift-hom π¨ hβ β£

lift-of-epi-is-epi π¨ {hβ} hE y = Goal
where
hββ»ΒΉy = Inv hβ (hE y)

Ξ· : y β‘ β£ lift-hom π¨ hβ β£ (β hββ»ΒΉy)
Ξ· = (InvIsInverseΚ³ (hE y))β»ΒΉ

Goal : Image β£ lift-hom π¨ hβ β£ β y
Goal = eq (β hββ»ΒΉy) Ξ·

```

The `lift-hom` and `lift-of-epi-is-epi` types will be called to action when such epimorphisms are needed later (e.g., in the Varieties module).