LawfulTraversable instances

This file provides instances of LawfulTraversable for types from the core library: Option, List and Sum.

theorem Option.id_traverse {α : Type u_1} (x : Option α) : Option.traverse pure x = x

theorem Option.comp_traverse {F : Type u → Type u} {G : Type u → Type u} [Applicative F] [Applicative G] [LawfulApplicative G] {α : Type u_1} {β : Type u} {γ : Type u} (f : β → F γ) (g : α → G β) (x : Option α) : Option.traverse (Functor.Comp.mk ∘ (fun x x_1 => x <$> x_1) f ∘ g) x = Functor.Comp.mk (Option.traverse f <$> Option.traverse g x)

theorem Option.traverse_eq_map_id {α : Type u_1} {β : Type u_1} (f : α → β) (x : Option α) : Option.traverse (pure ∘ f) x = pure (f <$> x)

theorem Option.naturality {F : Type u → Type u} {G : Type u → Type u} [Applicative F] [Applicative G] [LawfulApplicative F] [LawfulApplicative G] (η : ApplicativeTransformation F G) {α : Type u_1} {β : Type u} (f : α → F β) (x : Option α) : (fun {α} => ApplicativeTransformation.app η α) (Option β) (Option.traverse f x) = Option.traverse ((fun {α} => ApplicativeTransformation.app η α) β ∘ f) x

instance instLawfulTraversableOptionInstTraversableOption : LawfulTraversable Option

Equations

• instLawfulTraversableOptionInstTraversableOption = instLawfulTraversableOptionInstTraversableOption.proof_1

theorem List.id_traverse {α : Type u_1} (xs : List α) : List.traverse pure xs = xs

theorem List.comp_traverse {F : Type u → Type u} {G : Type u → Type u} [Applicative F] [Applicative G] [LawfulApplicative G] {α : Type u_1} {β : Type u} {γ : Type u} (f : β → F γ) (g : α → G β) (x : List α) : List.traverse (Functor.Comp.mk ∘ (fun x x_1 => x <$> x_1) f ∘ g) x = Functor.Comp.mk (List.traverse f <$> List.traverse g x)

theorem List.traverse_eq_map_id {α : Type u_1} {β : Type u_1} (f : α → β) (x : List α) : List.traverse (pure ∘ f) x = pure (f <$> x)

theorem List.naturality {F : Type u → Type u} {G : Type u → Type u} [Applicative F] [Applicative G] [LawfulApplicative F] [LawfulApplicative G] (η : ApplicativeTransformation F G) {α : Type u_1} {β : Type u} (f : α → F β) (x : List α) : (fun {α} => ApplicativeTransformation.app η α) (List β) (List.traverse f x) = List.traverse ((fun {α} => ApplicativeTransformation.app η α) β ∘ f) x

instance List.instLawfulTraversableListInstTraversableList : LawfulTraversable List

Equations

• List.instLawfulTraversableListInstTraversableList = List.instLawfulTraversableListInstTraversableList.proof_1

@[simp]

theorem List.traverse_nil {F : Type u → Type u} [Applicative F] {α' : Type u} {β' : Type u} (f : α' → F β') : traverse f [] = pure []

@[simp]

theorem List.traverse_cons {F : Type u → Type u} [Applicative F] {α' : Type u} {β' : Type u} (f : α' → F β') (a : α') (l : List α') : traverse f (a :: l) = Seq.seq ((fun x x_1 => x :: x_1) <$> f a) fun x => traverse f l

@[simp]

theorem List.traverse_append {F : Type u → Type u} [Applicative F] {α' : Type u} {β' : Type u} (f : α' → F β') [LawfulApplicative F] (as : List α') (bs : List α') : traverse f (as ++ bs) = Seq.seq ((fun x x_1 => x ++ x_1) <$> traverse f as) fun x => traverse f bs

theorem List.mem_traverse {α' : Type u} {β' : Type u} {f : α' → Set β'} (l : List α') (n : List β') : n ∈ traverse f l ↔ List.Forall₂ (fun b a => b ∈ f a) n l

theorem Sum.traverse_map {σ : Type u} {G : Type u → Type u} [Applicative G] {α : Type u} {β : Type u} {γ : Type u} (g : α → β) (f : β → G γ) (x : σ ⊕ α) : Sum.traverse f (g <$> x) = Sum.traverse (f ∘ g) x

theorem Sum.id_traverse {σ : Type u_1} {α : Type u_1} (x : σ ⊕ α) : Sum.traverse pure x = x

theorem Sum.comp_traverse {σ : Type u} {F : Type u → Type u} {G : Type u → Type u} [Applicative F] [Applicative G] [LawfulApplicative G] {α : Type u} {β : Type u} {γ : Type u} (f : β → F γ) (g : α → G β) (x : σ ⊕ α) : Sum.traverse (Functor.Comp.mk ∘ (fun x x_1 => x <$> x_1) f ∘ g) x = Functor.Comp.mk (Sum.traverse f <$> Sum.traverse g x)

theorem Sum.traverse_eq_map_id {σ : Type u} {α : Type u} {β : Type u} (f : α → β) (x : σ ⊕ α) : Sum.traverse (pure ∘ f) x = pure (f <$> x)

theorem Sum.map_traverse {σ : Type u} {G : Type u → Type u} [Applicative G] [LawfulApplicative G] {α : Type u_1} {β : Type u} {γ : Type u} (g : α → G β) (f : β → γ) (x : σ ⊕ α) : (fun x x_1 => x <$> x_1) f <$> Sum.traverse g x = Sum.traverse ((fun x x_1 => x <$> x_1) f ∘ g) x

theorem Sum.naturality {σ : Type u} {F : Type u → Type u} {G : Type u → Type u} [Applicative F] [Applicative G] [LawfulApplicative F] [LawfulApplicative G] (η : ApplicativeTransformation F G) {α : Type u_1} {β : Type u} (f : α → F β) (x : σ ⊕ α) : (fun {α} => ApplicativeTransformation.app η α) (σ ⊕ β) (Sum.traverse f x) = Sum.traverse ((fun {α} => ApplicativeTransformation.app η α) β ∘ f) x

instance Sum.instLawfulTraversableSumInstTraversableSum {σ : Type u} : LawfulTraversable (Sum σ)

Equations

• @Sum.instLawfulTraversableSumInstTraversableSum = @Sum.instLawfulTraversableSumInstTraversableSum.proof_1