Frexlet.Monoid.Frex.Structure

The structure of the frex for (mere) monoids
Its elements are given by a 'polynomial' of the form:

an * xn * ... a1 * x1 * a0

Its unit is 1, and multiplication is given by:

(an * xn * ... a1 * x1 * a0) *(bm * ym * ... b1 * y1 * b0)
:= an * xn * ... a1 * x1 * (a0*bm) * ym ... * y1 * b0

and some care is required for the edge cases.

Definitions

data UltList : Type -> Type -> Type

  A list of elements alternating between two types starting and
  ending with an `ult`imate.

Totality: total
Visibility: public export
Constructors:

Ultimate : ult -> UltList pen ult

ConsUlt : ult -> pen -> UltList pen ult -> UltList pen ult

Hints:

Uninhabited (UltListEquality penRel ultRel (Ultimate i) (ConsUlt j1 y js))

Uninhabited (UltListEquality penRel ultRel (ConsUlt i1 x is) (Ultimate j))

Nil : ()

Totality: total
Visibility: public export

(::) : ult -> () -> UltList pen ult

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 7

(::) : (ult, pen) -> UltList pen ult -> UltList pen ult

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 7

.mult : (a : Monoid) -> U a -> UltList pen (U a) -> UltList pen (U a)

Totality: total
Visibility: public export

(++) : UltList pen (U a) -> UltList pen (U a) -> UltList pen (U a)

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 7

data UltListEquality : (pen -> pen -> Type) -> (ult -> ult -> Type) -> UltList pen ult -> UltList pen ult -> Type

  Equality for UltList pen ult

Totality: total
Visibility: public export
Constructors:

Ultimate : ultRel i j -> UltListEquality penRel ultRel (Ultimate i) (Ultimate j)

ConsUlt : ultRel i j -> penRel x y -> UltListEquality penRel ultRel is js -> UltListEquality penRel ultRel ((i, x) :: is) ((j, y) :: js)

Hints:

Uninhabited (UltListEquality penRel ultRel (Ultimate i) (ConsUlt j1 y js))

Uninhabited (UltListEquality penRel ultRel (ConsUlt i1 x is) (Ultimate j))

(::) : ultRel i j -> () -> UltListEquality penRel ultRel (Ultimate i) (Ultimate j)

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 7

(::) : (ultRel i j, penRel x y) -> UltListEquality penRel ultRel is js -> UltListEquality penRel ultRel ((i, x) :: is) ((j, y) :: js)

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 7

UltListReflexive : (pen : Setoid) -> (ult : Setoid) -> (is : UltList (U pen) (U ult)) -> UltListEquality ((pen .equivalence) .relation) ((ult .equivalence) .relation) is is

Totality: total
Visibility: public export

UltListSymmetric : (pen : Setoid) -> (ult : Setoid) -> (is : UltList (U pen) (U ult)) -> (js : UltList (U pen) (U ult)) -> UltListEquality ((pen .equivalence) .relation) ((ult .equivalence) .relation) is js -> UltListEquality ((pen .equivalence) .relation) ((ult .equivalence) .relation) js is

Totality: total
Visibility: public export

UltListTransitive : (pen : Setoid) -> (ult : Setoid) -> (is : UltList (U pen) (U ult)) -> (js : UltList (U pen) (U ult)) -> (ks : UltList (U pen) (U ult)) -> UltListEquality ((pen .equivalence) .relation) ((ult .equivalence) .relation) is js -> UltListEquality ((pen .equivalence) .relation) ((ult .equivalence) .relation) js ks -> UltListEquality ((pen .equivalence) .relation) ((ult .equivalence) .relation) is ks

Totality: total
Visibility: public export

UltListSetoid : Setoid -> Setoid -> Setoid

Totality: total
Visibility: public export

MultHomomorphism : (a : Monoid) -> (s : Setoid) -> SetoidHomomorphism (Pair (cast a) (UltListSetoid s (cast a))) (UltListSetoid s (cast a)) (uncurry (a .mult))

Totality: total
Visibility: public export

AppendHomomorphismProperty : (a : Monoid) -> (x : Setoid) -> (is1 : UltList (U x) (U a)) -> (is2 : UltList (U x) (U a)) -> (js1 : UltList (U x) (U a)) -> (js2 : UltList (U x) (U a)) -> ((UltListSetoid x (cast a)) .equivalence) .relation is1 is2 -> ((UltListSetoid x (cast a)) .equivalence) .relation js1 js2 -> ((UltListSetoid x (cast a)) .equivalence) .relation (is1 ++ js1) (is2 ++ js2)

Totality: total
Visibility: public export

AppendHomomorphism : (a : Monoid) -> (x : Setoid) -> SetoidHomomorphism (Pair (UltListSetoid x (cast a)) (UltListSetoid x (cast a))) (UltListSetoid x (cast a)) (uncurry (++))

Totality: total
Visibility: public export

0 FrexCarrier : Monoid -> Setoid -> Type

Totality: total
Visibility: public export

.sta : (a : Monoid) -> U a -> UltList x (U a)

  Embedding of concrete elements in the frex by identifying
  i with the singleton i

Totality: total
Visibility: public export

.dyn : (a : Monoid) -> x -> UltList x (U a)

  Embedding variables in the frex by identifying
  x with 1 * x * 1

Totality: total
Visibility: public export

FrexAlgebraStructure : (a : Monoid) -> (x : Setoid) -> algebraOver' Signature (FrexCarrier a x)

Totality: total
Visibility: public export

FrexStructure : Monoid -> Setoid -> MonoidStructure

Totality: total
Visibility: public export

FrexSetoid : Monoid -> Setoid -> Setoid

Totality: total
Visibility: public export

MonAction : (a : Monoid) -> (s : Setoid) -> ActionData (U a) (FrexCarrier a s)

Totality: total
Visibility: public export