Data.Setoid.List

Setoid of lists over a setoid and associated definitions

Definitions

data .ListEquality : (a : Setoid) -> Rel (List (U a))

Totality: total
Visibility: public export
Constructors:

Nil : a .ListEquality [] []

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

.ListEqualityReflexive : (a : Setoid) -> (xs : List (U a)) -> a .ListEquality xs xs

Totality: total
Visibility: public export

.ListEqualitySymmetric : (a : Setoid) -> (xs : List (U a)) -> (ys : List (U a)) -> a .ListEquality xs ys -> a .ListEquality ys xs

Totality: total
Visibility: public export

.ListEqualityTransitive : (a : Setoid) -> (xs : List (U a)) -> (ys : List (U a)) -> (zs : List (U a)) -> a .ListEquality xs ys -> a .ListEquality ys zs -> a .ListEquality xs zs

Totality: total
Visibility: public export

ListSetoid : Setoid -> Setoid

Totality: total
Visibility: public export

ListMapFunctionHomomorphism : (f : a ~> b) -> SetoidHomomorphism (ListSetoid a) (ListSetoid b) (map (f .H))

Totality: total
Visibility: public export

ListMapHomomorphism : a ~> b -> ListSetoid a ~> ListSetoid b

Totality: total
Visibility: public export

ListMapIsHomomorphism : SetoidHomomorphism (a ~~> b) (ListSetoid a ~~> ListSetoid b) ListMapHomomorphism

Totality: total
Visibility: public export

ListMap : (a ~~> b) ~> (ListSetoid a ~~> ListSetoid b)

Totality: total
Visibility: public export

reverseHomomorphic : (x : List (U a)) -> (y : List (U a)) -> a .ListEquality x y -> a .ListEquality (reverse x) (reverse y)

Totality: total
Visibility: public export

appendCongruence : (x1 : List (U a)) -> (x2 : List (U a)) -> (y1 : List (U a)) -> (y2 : List (U a)) -> a .ListEquality x1 y1 -> a .ListEquality x2 y2 -> a .ListEquality (x1 ++ x2) (y1 ++ y2)

Totality: total
Visibility: public export