Data.Setoid.Vect.Inductive

The setoid of vectors over a given setoid, defined inductively

Definitions

data .VectEquality : (a : Setoid) -> Rel (Vect n (U a))

Totality: total
Visibility: public export
Constructors:

Nil : a .VectEquality [] []

(::) : (a .equivalence) .relation x y -> a .VectEquality xs ys -> a .VectEquality (x :: xs) (y :: ys)

(++) : a .VectEquality xs ys -> a .VectEquality as bs -> a .VectEquality (xs ++ as) (ys ++ bs)

Totality: total
Visibility: export
Fixity Declaration: infixr operator, level 7

.VectEqualityReflexive : (a : Setoid) -> (xs : Vect n (U a)) -> a .VectEquality xs xs

Totality: total
Visibility: public export

.VectEqualitySymmetric : (a : Setoid) -> (xs : Vect n (U a)) -> (ys : Vect n (U a)) -> a .VectEquality xs ys -> a .VectEquality ys xs

Totality: total
Visibility: public export

.VectEqualityTransitive : (a : Setoid) -> (xs : Vect n (U a)) -> (ys : Vect n (U a)) -> (zs : Vect n (U a)) -> a .VectEquality xs ys -> a .VectEquality ys zs -> a .VectEquality xs zs

Totality: total
Visibility: public export

VectSetoid : Nat -> Setoid -> Setoid

Totality: total
Visibility: public export

VectMapFunctionHomomorphism : (f : a ~> b) -> SetoidHomomorphism (VectSetoid n a) (VectSetoid n b) (map (f .H))

Totality: total
Visibility: public export

VectMapHomomorphism : a ~> b -> VectSetoid n a ~> VectSetoid n b

Totality: total
Visibility: public export

VectMapIsHomomorphism : SetoidHomomorphism (a ~~> b) (VectSetoid n a ~~> VectSetoid n b) VectMapHomomorphism

Totality: total
Visibility: public export

VectMap : (a ~~> b) ~> (VectSetoid n a ~~> VectSetoid n b)

Totality: total
Visibility: public export