Frex.Free.Construction.ByFrex

Construct the free monoid over a setoid `s` by freely extending
the free monoid over the empty setoid by the setoid `s`

Definitions

record Parameters : Presentation -> Setoid -> Type

Totality: total
Visibility: public export
Constructor: 

MkParameters : {0 Pres : Presentation} -> (Initial : Free Pres (cast Void)) -> Frex ((Initial .Data) .Model) s -> Parameters Pres s

Projections:

.FrexBy : {0 Pres : Presentation} -> ({rec:0} : Parameters Pres s) -> Frex (((Initial {rec:0}) .Data) .Model) s

.Initial : {0 Pres : Presentation} -> Parameters Pres s -> Free Pres (cast Void)

.Initial : {0 Pres : Presentation} -> Parameters Pres s -> Free Pres (cast Void)

Visibility: public export

Initial : {0 Pres : Presentation} -> Parameters Pres s -> Free Pres (cast Void)

Visibility: public export

.FrexBy : {0 Pres : Presentation} -> ({rec:0} : Parameters Pres s) -> Frex (((Initial {rec:0}) .Data) .Model) s

Visibility: public export

FrexBy : {0 Pres : Presentation} -> ({rec:0} : Parameters Pres s) -> Frex (((Initial {rec:0}) .Data) .Model) s

Visibility: public export

.toModelOver : {auto param : Parameters pres s} -> Extension (((param .Initial) .Data) .Model) s -> ModelOver pres s

Visibility: public export

.OverVoid : Model pres -> ModelOver pres (cast Void)

Visibility: public export

.initiality : {auto param : Parameters pres s} -> (model : Model pres) -> ((param .Initial) .Data) .Model ~> model

Visibility: public export

.homomorphism : a .Model ~> b -> a ~> b .OverVoid

Visibility: public export

.toExtension : {auto param : Parameters pres s} -> ModelOver pres s -> Extension (((param .Initial) .Data) .Model) s

Visibility: public export

.toExtensionMorphism : {auto param : Parameters pres s} -> mod1 .toModelOver ~> mod2 -> mod1 ~> mod2 .toExtension

Visibility: public export

FreeModelOver : Parameters pres s -> ModelOver pres s

Visibility: public export

Extender : (param : Parameters pres s) -> Extender

Visibility: public export

Uniqueness : (param : Parameters pres s) -> Uniqueness

Visibility: public export

ByFrex : (initial : Free pres (cast Void)) -> Frex ((initial .Data) .Model) s -> Free pres s

Visibility: public export