Frexlet.Monoid.Frex.Construction

Constructing the frex of a monoid by a setoid

Definitions

reify : (a : Monoid) -> (s : Setoid) -> FrexCarrier a s -> Term Signature (Either (U a) (U s))

Totality: total
Visibility: public export

normalForm : (a : Monoid) -> (s : Setoid) -> (is : FrexCarrier a s) -> (FrexMonoid a s) .rel ((FrexMonoid a s) .Sem (reify a s is) (either (Delay (a .sta)) (Delay (a .dyn)))) is

Totality: total
Visibility: public export

staIsHomo : (a : Monoid) -> (s : Setoid) -> Homomorphism (a .Algebra) (FrexStructure a s) (a .sta)

Totality: total
Visibility: public export

staHomo : (a : Monoid) -> (s : Setoid) -> a ~> FrexMonoid a s

Totality: total
Visibility: public export

dynHomo : (a : Monoid) -> (s : Setoid) -> s ~> FrexSetoid a s

Totality: total
Visibility: public export

Extension : (a : Monoid) -> (s : Setoid) -> Extension a s

Totality: total
Visibility: public export

ExtenderFunction : (a : Monoid) -> (s : Setoid) -> ExtenderFunction (Extension a s)

Totality: total
Visibility: public export

ExtenderPreservesMult : (a : Monoid) -> (s : Setoid) -> (other : Extension a s) -> (i : U a) -> (is : FrexCarrier a s) -> (other .Model) .rel (ExtenderFunction a s other (i *. is)) (((other .Embed) .H) .H i .*. ExtenderFunction a s other is)

Totality: total
Visibility: public export

ExtenderPreservesProd : (a : Monoid) -> (s : Setoid) -> (other : Extension a s) -> (is : FrexCarrier a s) -> (js : FrexCarrier a s) -> (other .Model) .rel (h (is .*. js)) (h is .*. h js)

Totality: total
Visibility: public export

ExtenderIsHomomorphism : (a : Monoid) -> (s : Setoid) -> ExtenderIsHomomorphism (Extension a s) (ExtenderFunction a s)

Totality: total
Visibility: public export

ExtenderIsSetoidHomomorphism : (a : Monoid) -> (s : Setoid) -> (other : Extension a s) -> (is : FrexCarrier a s) -> (js : FrexCarrier a s) -> (FrexMonoid a s) .rel is js -> (other .Model) .rel (ExtenderFunction a s other is) (ExtenderFunction a s other js)

Totality: total
Visibility: public export

ExtenderHomomorphism : (a : Monoid) -> (s : Setoid) -> ExtenderHomomorphism (Extension a s)

Totality: total
Visibility: public export

ExtenderPreservesEmbedding : (a : Monoid) -> (s : Setoid) -> ExtenderPreservesEmbedding (Extension a s) (ExtenderHomomorphism a s)

Totality: total
Visibility: public export

ExtenderPreservesVars : (a : Monoid) -> (s : Setoid) -> ExtenderPreservesVars (Extension a s) (ExtenderHomomorphism a s)

Totality: total
Visibility: public export

Extender : (a : Monoid) -> (s : Setoid) -> Extender (Extension a s)

Totality: total
Visibility: public export

Uniqueness : (a : Monoid) -> (s : Setoid) -> Uniqueness (Extension a s)

Totality: total
Visibility: public export

MonoidFrex : (a : Monoid) -> (s : Setoid) -> Frex a s

Totality: total
Visibility: public export

MonoidFrexlet : Frexlet

Totality: total
Visibility: public export