Frex.Powers.Abstract

Abstract properties of powers

Definitions

id : (param : Parameterisation pres x a) -> param ~> param

Totality: total
Visibility: public export

(.) : param2 ~> param3 -> param1 ~> param2 -> param1 ~> param3

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 9

transportParameterisation : (param : Parameterisation pres x a) -> (param .Model) .Algebra <~> b -> Parameterisation pres x a

  Transport a parameterisation across an isomorphism

Totality: total
Visibility: public export

coherence : (param : Parameterisation pres x a) -> (iso : (param .Model) .Algebra <~> b) -> param ~> transportParameterisation param iso

Totality: total
Visibility: public export

coherenceSym : (param : Parameterisation pres x a) -> (iso : (param .Model) .Algebra <~> b) -> transportParameterisation param iso ~> param

Totality: total
Visibility: public export

transport : (power : Power x a) -> ((power .Data) .Model) .Algebra <~> b -> Power x a

  Transport a power along an algebra isomorphism

Totality: total
Visibility: public export