Frex.Powers.Fin

When the exponent is `Fin n`, we can represent the power Fin n
`Power` A using `Vect n A`.

Definitions

FinPowerSetoid : Nat -> SetoidAlgebra sig -> Setoid

Totality: total
Visibility: public export

FinPowerAlgebra : Nat -> SetoidAlgebra sig -> Algebra sig

Totality: total
Visibility: public export

indexHomomorphismLemma : (n : Nat) -> (a : SetoidAlgebra sig) -> (i : Fin n) -> (op : Op sig) -> (zss : Vect (arity op) (U (FinPowerSetoid n a))) -> (a .equivalence) .relation (index i (map (a .Sem op) (transpose zss))) ((a .algebra) .Sem op (map (index i) zss))

Totality: total
Visibility: public export

FinPowerSetoidAlgebra : Nat -> SetoidAlgebra sig -> SetoidAlgebra sig

Totality: total
Visibility: public export

eval : Fin n -> FinPowerSetoidAlgebra n a ~> a

Totality: total
Visibility: public export

pointwiseBind : (t : Term sig y) -> (env : (y -> Vect n (U a))) -> (x : Fin n) -> (a .equivalence) .relation (index x ((FinPowerSetoidAlgebra n a) .Sem t env)) (a .Sem t (index x . env))

Totality: total
Visibility: public export

representation : FinPowerSetoidAlgebra n a <~> (~~>)

Totality: total
Visibility: public export

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

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

(^) : (a : Model pres) -> (n : Nat) -> Power (cast (Fin n)) a

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