Frex.Free.Definition

Definition of a free model over a setoid

Definitions

record ModelOver : Presentation -> Setoid -> Type

  A model over a setoid `X` is a model that can also interpret the
  elements of `X`.
  
  For example, the monads associated to a presentation are the
  choices of a free model over each set(oid).

Totality: total
Visibility: public export
Constructor: 

MkModelOver : {0 Pres : Presentation} -> {0 X : Setoid} -> (Model : Model Pres) -> X ~> cast Model -> ModelOver Pres X

Projections:

.Env : {0 Pres : Presentation} -> {0 X : Setoid} -> ({rec:0} : ModelOver Pres X) -> X ~> cast (Model {rec:0})

.Model : {0 Pres : Presentation} -> {0 X : Setoid} -> ModelOver Pres X -> Model Pres

Hints:

pres .signature = sig => Semantic (ModelOver pres x) (Op sig)

pres .signature = sig => Semantic (ModelOver pres x) (Term sig y)

.Model : {0 Pres : Presentation} -> {0 X : Setoid} -> ModelOver Pres X -> Model Pres

Totality: total
Visibility: public export

Model : {0 Pres : Presentation} -> {0 X : Setoid} -> ModelOver Pres X -> Model Pres

Totality: total
Visibility: public export

.Env : {0 Pres : Presentation} -> {0 X : Setoid} -> ({rec:0} : ModelOver Pres X) -> X ~> cast (Model {rec:0})

Totality: total
Visibility: public export

Env : {0 Pres : Presentation} -> {0 X : Setoid} -> ({rec:0} : ModelOver Pres X) -> X ~> cast (Model {rec:0})

Totality: total
Visibility: public export

0 PreservesEnv : {Pres : Presentation} -> {X : Setoid} -> (a : ModelOver Pres X) -> (b : ModelOver Pres X) -> cast (a .Model) ~> cast (b .Model) -> Type

  States: Homomorphism between the models over X.

Totality: total
Visibility: public export

record (~>) : {Pres : Presentation} -> {X : Setoid} -> ModelOver Pres X -> ModelOver Pres X -> Type

  A `Pres`-model over X homomorphism

Totality: total
Visibility: public export
Constructor: 

MkHomomorphism : {0 Pres : Presentation} -> {0 X : Setoid} -> {0 A : ModelOver Pres X} -> {0 B : ModelOver Pres X} -> (H : A .Model ~> B .Model) -> PreservesEnv A B (H .H) -> A ~> B

Projections:

.H : {0 Pres : Presentation} -> {0 X : Setoid} -> {0 A : ModelOver Pres X} -> {0 B : ModelOver Pres X} -> A ~> B -> A .Model ~> B .Model

.preserves : {0 Pres : Presentation} -> {0 X : Setoid} -> {0 A : ModelOver Pres X} -> {0 B : ModelOver Pres X} -> ({rec:0} : A ~> B) -> PreservesEnv A B ((H {rec:0}) .H)

Fixity Declarations:
infix operator, level 5
infix operator, level 5
infix operator, level 5

.H : {0 Pres : Presentation} -> {0 X : Setoid} -> {0 A : ModelOver Pres X} -> {0 B : ModelOver Pres X} -> A ~> B -> A .Model ~> B .Model

Totality: total
Visibility: public export

H : {0 Pres : Presentation} -> {0 X : Setoid} -> {0 A : ModelOver Pres X} -> {0 B : ModelOver Pres X} -> A ~> B -> A .Model ~> B .Model

Totality: total
Visibility: public export

.preserves : {0 Pres : Presentation} -> {0 X : Setoid} -> {0 A : ModelOver Pres X} -> {0 B : ModelOver Pres X} -> ({rec:0} : A ~> B) -> PreservesEnv A B ((H {rec:0}) .H)

Totality: total
Visibility: public export

preserves : {0 Pres : Presentation} -> {0 X : Setoid} -> {0 A : ModelOver Pres X} -> {0 B : ModelOver Pres X} -> ({rec:0} : A ~> B) -> PreservesEnv A B ((H {rec:0}) .H)

Totality: total
Visibility: public export

0 Extender : {Pres : Presentation} -> {X : Setoid} -> ModelOver Pres X -> Type

  Weak initiality: for any other model over X there is a morphism from FX into it.

Totality: total
Visibility: public export

0 ExtenderFunction : {Pres : Presentation} -> {X : Setoid} -> ModelOver Pres X -> Type

Totality: total
Visibility: public export

0 ExtenderSetoidHomomorphism : {Pres : Presentation} -> {X : Setoid} -> ModelOver Pres X -> Type

Totality: total
Visibility: public export

0 ExtenderAlgebraHomomorphism : {Pres : Presentation} -> {X : Setoid} -> ModelOver Pres X -> Type

Totality: total
Visibility: public export

0 Uniqueness : {Pres : Presentation} -> {X : Setoid} -> ModelOver Pres X -> Type

  There's at most one homomorphism of models over X from FX

Totality: total
Visibility: public export

record Freeness : {Pres : Presentation} -> {X : Setoid} -> ModelOver Pres X -> Type

Totality: total
Visibility: public export
Constructor: 

IsFree : {0 Pres : Presentation} -> {0 X : Setoid} -> {0 FX : ModelOver Pres X} -> Extender -> Uniqueness -> Freeness FX

Projections:

.Exists : {0 Pres : Presentation} -> {0 X : Setoid} -> {0 FX : ModelOver Pres X} -> Freeness FX -> Extender

.Unique : {0 Pres : Presentation} -> {0 X : Setoid} -> {0 FX : ModelOver Pres X} -> Freeness FX -> Uniqueness

.Exists : {0 Pres : Presentation} -> {0 X : Setoid} -> {0 FX : ModelOver Pres X} -> Freeness FX -> Extender

Totality: total
Visibility: public export

Exists : {0 Pres : Presentation} -> {0 X : Setoid} -> {0 FX : ModelOver Pres X} -> Freeness FX -> Extender

Totality: total
Visibility: public export

.Unique : {0 Pres : Presentation} -> {0 X : Setoid} -> {0 FX : ModelOver Pres X} -> Freeness FX -> Uniqueness

Totality: total
Visibility: public export

Unique : {0 Pres : Presentation} -> {0 X : Setoid} -> {0 FX : ModelOver Pres X} -> Freeness FX -> Uniqueness

Totality: total
Visibility: public export

record Free : Presentation -> Setoid -> Type

Totality: total
Visibility: public export
Constructor: 

MkFree : {0 Pres : Presentation} -> {0 X : Setoid} -> (Data : ModelOver Pres X) -> Freeness Data -> Free Pres X

Projections:

.Data : {0 Pres : Presentation} -> {0 X : Setoid} -> Free Pres X -> ModelOver Pres X

.UP : {0 Pres : Presentation} -> {0 X : Setoid} -> ({rec:0} : Free Pres X) -> Freeness (Data {rec:0})

Hints:

pres .signature = sig => Semantic (Free pres x) (Op sig)

pres .signature = sig => Semantic (Free pres x) (Term sig y)

.Data : {0 Pres : Presentation} -> {0 X : Setoid} -> Free Pres X -> ModelOver Pres X

Totality: total
Visibility: public export

Data : {0 Pres : Presentation} -> {0 X : Setoid} -> Free Pres X -> ModelOver Pres X

Totality: total
Visibility: public export

.UP : {0 Pres : Presentation} -> {0 X : Setoid} -> ({rec:0} : Free Pres X) -> Freeness (Data {rec:0})

Totality: total
Visibility: public export

UP : {0 Pres : Presentation} -> {0 X : Setoid} -> ({rec:0} : Free Pres X) -> Freeness (Data {rec:0})

Totality: total
Visibility: public export