Frex.Powers.Definition

The definition of what a power is

Definitions

record Parameterisation : (Pres : Presentation) -> Setoid -> Model Pres -> Type

  A parameterisation

Totality: total
Visibility: public export
Constructor: 

MkParameterisation : {0 Pres : Presentation} -> {0 X : Setoid} -> {0 A : Model Pres} -> (Model : Model Pres) -> X ~> (Model ~~> A) -> Parameterisation Pres X A

Projections:

.Eval : {0 Pres : Presentation} -> {0 X : Setoid} -> {0 A : Model Pres} -> ({rec:0} : Parameterisation Pres X A) -> X ~> (Model {rec:0} ~~> A)

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

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

Totality: total
Visibility: public export

Model : {0 Pres : Presentation} -> {0 X : Setoid} -> {0 A : Model Pres} -> Parameterisation Pres X A -> Model Pres

Totality: total
Visibility: public export

.Eval : {0 Pres : Presentation} -> {0 X : Setoid} -> {0 A : Model Pres} -> ({rec:0} : Parameterisation Pres X A) -> X ~> (Model {rec:0} ~~> A)

Totality: total
Visibility: public export

Eval : {0 Pres : Presentation} -> {0 X : Setoid} -> {0 A : Model Pres} -> ({rec:0} : Parameterisation Pres X A) -> X ~> (Model {rec:0} ~~> A)

Totality: total
Visibility: public export

0 PreservesEvaluation : {Pres : Presentation} -> {X : Setoid} -> {A : Model Pres} -> (v : Parameterisation Pres X A) -> (w : Parameterisation Pres X A) -> v .Model ~> w .Model -> Type

  Model/algebra homomorphism that is also a parametrisation morphism

Totality: total
Visibility: public export

record (~>) : {Pres : Presentation} -> {X : Setoid} -> {A : Model Pres} -> Parameterisation Pres X A -> Parameterisation Pres X A -> Type

Totality: total
Visibility: public export
Constructor: 

MkParameterisationMorphism : {Pres : Presentation} -> {X : Setoid} -> {A : Model Pres} -> {0 V : Parameterisation Pres X A} -> {0 W : Parameterisation Pres X A} -> (H : V .Model ~> W .Model) -> (0 _ : PreservesEvaluation V W H) -> V ~> W

Projections:

.H : {Pres : Presentation} -> {X : Setoid} -> {A : Model Pres} -> {0 V : Parameterisation Pres X A} -> {0 W : Parameterisation Pres X A} -> V ~> W -> V .Model ~> W .Model

0 .preserve : {Pres : Presentation} -> {X : Setoid} -> {A : Model Pres} -> {0 V : Parameterisation Pres X A} -> {0 W : Parameterisation Pres X A} -> ({rec:0} : V ~> W) -> PreservesEvaluation V W (H {rec:0})

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

.H : {Pres : Presentation} -> {X : Setoid} -> {A : Model Pres} -> {0 V : Parameterisation Pres X A} -> {0 W : Parameterisation Pres X A} -> V ~> W -> V .Model ~> W .Model

Totality: total
Visibility: public export

H : {Pres : Presentation} -> {X : Setoid} -> {A : Model Pres} -> {0 V : Parameterisation Pres X A} -> {0 W : Parameterisation Pres X A} -> V ~> W -> V .Model ~> W .Model

Totality: total
Visibility: public export

0 .preserve : {Pres : Presentation} -> {X : Setoid} -> {A : Model Pres} -> {0 V : Parameterisation Pres X A} -> {0 W : Parameterisation Pres X A} -> ({rec:0} : V ~> W) -> PreservesEvaluation V W (H {rec:0})

Totality: total
Visibility: public export

0 preserve : {Pres : Presentation} -> {X : Setoid} -> {A : Model Pres} -> {0 V : Parameterisation Pres X A} -> {0 W : Parameterisation Pres X A} -> ({rec:0} : V ~> W) -> PreservesEvaluation V W (H {rec:0})

Totality: total
Visibility: public export

0 Extension : {Pres : Presentation} -> {X : Setoid} -> {A : Model Pres} -> Parameterisation Pres X A -> Type

Totality: total
Visibility: public export

0 UniqueExtension : {Pres : Presentation} -> {X : Setoid} -> {A : Model Pres} -> (XtoA : Parameterisation Pres X A) -> (other : Parameterisation Pres X A) -> other ~> XtoA -> Type

Totality: total
Visibility: public export

0 Uniqueness : {Pres : Presentation} -> {X : Setoid} -> {A : Model Pres} -> (XtoA : Parameterisation Pres X A) -> Extension -> Type

Totality: total
Visibility: public export

record Universality : {Pres : Presentation} -> {X : Setoid} -> {A : Model Pres} -> Parameterisation Pres X A -> Type

Totality: total
Visibility: public export
Constructor: 

IsUniversal : {Pres : Presentation} -> {X : Setoid} -> {A : Model Pres} -> {0 XtoA : Parameterisation Pres X A} -> (Exists : Extension) -> (0 _ : Uniqueness Exists) -> Universality XtoA

Projections:

.Exists : {Pres : Presentation} -> {X : Setoid} -> {A : Model Pres} -> {0 XtoA : Parameterisation Pres X A} -> Universality XtoA -> Extension

0 .Unique : {Pres : Presentation} -> {X : Setoid} -> {A : Model Pres} -> {0 XtoA : Parameterisation Pres X A} -> ({rec:0} : Universality XtoA) -> Uniqueness (Exists {rec:0})

.Exists : {Pres : Presentation} -> {X : Setoid} -> {A : Model Pres} -> {0 XtoA : Parameterisation Pres X A} -> Universality XtoA -> Extension

Totality: total
Visibility: public export

Exists : {Pres : Presentation} -> {X : Setoid} -> {A : Model Pres} -> {0 XtoA : Parameterisation Pres X A} -> Universality XtoA -> Extension

Totality: total
Visibility: public export

0 .Unique : {Pres : Presentation} -> {X : Setoid} -> {A : Model Pres} -> {0 XtoA : Parameterisation Pres X A} -> ({rec:0} : Universality XtoA) -> Uniqueness (Exists {rec:0})

Totality: total
Visibility: public export

0 Unique : {Pres : Presentation} -> {X : Setoid} -> {A : Model Pres} -> {0 XtoA : Parameterisation Pres X A} -> ({rec:0} : Universality XtoA) -> Uniqueness (Exists {rec:0})

Totality: total
Visibility: public export

record Power : {Pres : Presentation} -> Setoid -> Model Pres -> Type

Totality: total
Visibility: public export
Constructor: 

MkPower : {0 Pres : Presentation} -> {0 X : Setoid} -> {0 A : Model Pres} -> (Data : Parameterisation Pres X A) -> Universality Data -> Power X A

Projections:

.Data : {0 Pres : Presentation} -> {0 X : Setoid} -> {0 A : Model Pres} -> Power X A -> Parameterisation Pres X A

.UP : {0 Pres : Presentation} -> {0 X : Setoid} -> {0 A : Model Pres} -> ({rec:0} : Power X A) -> Universality (Data {rec:0})

.Data : {0 Pres : Presentation} -> {0 X : Setoid} -> {0 A : Model Pres} -> Power X A -> Parameterisation Pres X A

Totality: total
Visibility: public export

Data : {0 Pres : Presentation} -> {0 X : Setoid} -> {0 A : Model Pres} -> Power X A -> Parameterisation Pres X A

Totality: total
Visibility: public export

.UP : {0 Pres : Presentation} -> {0 X : Setoid} -> {0 A : Model Pres} -> ({rec:0} : Power X A) -> Universality (Data {rec:0})

Totality: total
Visibility: public export

UP : {0 Pres : Presentation} -> {0 X : Setoid} -> {0 A : Model Pres} -> ({rec:0} : Power X A) -> Universality (Data {rec:0})

Totality: total
Visibility: public export