Frex.Powers.Construction

Definitions

PowerSetoid : {0 Sig : Signature} -> Setoid -> SetoidAlgebra Sig -> Setoid

Totality: total
Visibility: public export

PowerAlgebra : {0 Sig : Signature} -> Setoid -> SetoidAlgebra Sig -> Algebra Sig

Totality: total
Visibility: public export

(~~>) : {0 Sig : Signature} -> Setoid -> SetoidAlgebra Sig -> SetoidAlgebra Sig

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 5

eval : {0 Sig : Signature} -> {X : Setoid} -> {A : SetoidAlgebra Sig} -> U X -> (~~>) ~> A

Totality: total
Visibility: public export

pointwiseBind : {0 Sig : Signature} -> {X : Setoid} -> {A : SetoidAlgebra Sig} -> (t : Term Sig y) -> (env : (y -> U (~~>))) -> (x : U X) -> (A .equivalence) .relation (((~~>) .Sem t env) .H x) (A .Sem t (\i => (env i) .H x))

Totality: total
Visibility: public export

(~~>) : Setoid -> Model pres -> Model pres

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 5

(^) : (a : Model pres) -> (x : Setoid) -> Power x a

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 10