Functoriality of Set

This file defines the functor structure of Set.

ink

instance Set.monad : Monad Set

Equations

• Set.monad = Monad.mk

ink

@[simp]

theorem Set.bind_def {α : Type u} {β : Type u} {s : Set α} {f : α → Set β} : s >>= f = Set.unionᵢ fun i => Set.unionᵢ fun h => f i

ink

@[simp]

theorem Set.fmap_eq_image {α : Type u} {β : Type u} {s : Set α} (f : α → β) : f <$> s = f '' s

ink

@[simp]

theorem Set.seq_eq_set_seq {α : Type u} {β : Type u} (s : Set (α → β)) (t : Set α) : (Seq.seq s fun x => t) = Set.seq s t

ink

@[simp]

theorem Set.pure_def {α : Type u} (a : α) : pure a = {a}

ink

theorem Set.image2_def {α : Type u_1} {β : Type u_1} {γ : Type u_1} (f : α → β → γ) (s : Set α) (t : Set β) : Set.image2 f s t = Seq.seq (f <$> s) fun x => t

Set.image2 in terms of monadic operations. Note that this can't be taken as the definition because of the lack of universe polymorphism.

ink

instance Set.instLawfulMonadSetMonad : LawfulMonad Set

Equations

• Set.instLawfulMonadSetMonad = Set.instLawfulMonadSetMonad.proof_1

ink

instance Set.instCommApplicativeSetToApplicativeMonad : CommApplicative Set

Equations

• Set.instCommApplicativeSetToApplicativeMonad = Set.instCommApplicativeSetToApplicativeMonad.proof_1

ink

instance Set.instAlternativeSet : Alternative Set

Equations

• Set.instAlternativeSet = let src := Set.monad; Alternative.mk (fun {α} => ∅) fun {α} s t => s ∪ t ()