English
Let Filter be endowed with an applicative structure given by map and pure. This structure satisfies the usual laws of a lawful applicative functor (map_pure, seqLeft_eq, seqRight_eq, seq_pure, pure_seq, seq_assoc).
Русский
Пусть у типа Filter имеется структура аппликативного функторa, задаваемая операциями map и pure. Эта структура удовлетворяет обычным законам законной аппликативности (map_pure, seqLeft_eq, seqRight_eq, seq_pure, pure_seq, seq_assoc).
LaTeX
$$$\\text{Filter}$ with $\\mathrm{map}$ and $\\mathrm{pure}$ forms a lawful applicative functor, i.e. the standard applicative laws hold: $\\mathrm{map\\_pure}$, $\\mathrm{seqLeft\\_eq}$, $\\mathrm{seqRight\\_eq}$, $\\mathrm{seq\\_pure}$, $\\mathrm{pure\\_seq}$, $\\mathrm{seq\\_assoc}$.$$
Lean4
instance : LawfulApplicative (Filter : Type u → Type u)
where
map_pure := map_pure
seqLeft_eq _ _ := rfl
seqRight_eq _ _ := rfl
seq_pure := seq_pure
pure_seq := pure_seq_eq_map
seq_assoc := seq_assoc
