(unbundled) morphisms of monads

This file defines predicates on functions f : ∀ {α}, m α → n α that preserve functor, applicative, monadic, and alternative structure (IsFunctorHom, IsApplicativeHom, IsMonadHom, IsAlternativeHom, IsAlternativeMonadHom).

Rather than assuming lawfulness, they explicitly require compatibility with every operator defined by the corresponding typeclasses, with helper constructors that dismiss the derived operators when the structures are lawful.

Functor Homomorphisms

structure Cslib.IsFunctorHom (m : Type u_1 → Type u_2) (n : Type u_1 → Type u_3) [Functor m] [Functor n] (f : {α : Type u_1} → m α → n α) : Prop

A function f is a morphism of functors if it preserves <$> and Functor.mapConst.

• map_map {α β : Type u_1} (g : α → β) (x : m α) : f (g <$> x) = g <$> f x
• map_mapConst {α β : Type u_1} (a : α) (x : m β) : f (Functor.mapConst a x) = Functor.mapConst a (f x)

theorem Cslib.IsFunctorHom.mk' {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [Functor m] [Functor n] [LawfulFunctor m] [LawfulFunctor n] {f : {α : Type u_1} → m α → n α} (map_map : ∀ {α β : Type u_1} (g : α → β) (x : m α), f (g <$> x) = g <$> f x) : IsFunctorHom m n fun {α : Type u_1} => f

Construct an IsFunctorHom for lawful functors from map_map.

theorem Cslib.IsFunctorHom.id (m : Type u_1 → Type u_2) [Functor m] : IsFunctorHom m m fun {α : Type u_1} => id

theorem Cslib.IsFunctorHom.comp {m : Type u_1 → Type u_4} {n : Type u_1 → Type u_2} {p : Type u_1 → Type u_3} [Functor m] [Functor n] [Functor p] {f : {α : Type u_1} → n α → p α} {g : {α : Type u_1} → m α → n α} (hf : IsFunctorHom n p fun {α : Type u_1} => f) (hg : IsFunctorHom m n fun {α : Type u_1} => g) : IsFunctorHom m p fun {α : Type u_1} => f ∘ g

Applicative Homomorphisms

structure Cslib.IsApplicativeHom (m : Type u_1 → Type u_2) (n : Type u_1 → Type u_3) [Applicative m] [Applicative n] (f : {α : Type u_1} → m α → n α) extends Cslib.IsFunctorHom m n fun {α : Type u_1} => f : Prop

A function f is a morphism of applicatives if it preserves pure, <$>, <*>, <*, and *>.

• map_map {α β : Type u_1} (g : α → β) (x : m α) : f (g <$> x) = g <$> f x
• map_mapConst {α β : Type u_1} (a : α) (x : m β) : f (Functor.mapConst a x) = Functor.mapConst a (f x)
• map_pure {α : Type u_1} (a : α) : f (pure a) = pure a
• map_seq {α β : Type u_1} (x : m (α → β)) (y : Unit → m α) : f (x <*> y ()) = f x <*> f (y ())
• map_seqLeft {α β : Type u_1} (x : m α) (y : Unit → m β) : f (x <* y ()) = f x <* f (y ())
• map_seqRight {α β : Type u_1} (x : m α) (y : Unit → m β) : f (x *> y ()) = f x *> f (y ())

theorem Cslib.IsApplicativeHom.mk' {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [Applicative m] [Applicative n] [LawfulApplicative m] [LawfulApplicative n] {f : {α : Type u_1} → m α → n α} (map_pure : ∀ {α : Type u_1} (a : α), f (pure a) = pure a) (map_seq : ∀ {α β : Type u_1} (x : m (α → β)) (y : Unit → m α), f (x <*> y ()) = f x <*> f (y ())) : IsApplicativeHom m n fun {α : Type u_1} => f

Construct an IsApplicativeHom for lawful applicatives from map_pure and map_seq.

theorem Cslib.IsApplicativeHom.id (m : Type u_1 → Type u_2) [Applicative m] : IsApplicativeHom m m fun {α : Type u_1} => id

theorem Cslib.IsApplicativeHom.comp {m : Type u_1 → Type u_4} {n : Type u_1 → Type u_2} {p : Type u_1 → Type u_3} [Applicative m] [Applicative n] [Applicative p] {f : {α : Type u_1} → n α → p α} {g : {α : Type u_1} → m α → n α} (hf : IsApplicativeHom n p fun {α : Type u_1} => f) (hg : IsApplicativeHom m n fun {α : Type u_1} => g) : IsApplicativeHom m p fun {α : Type u_1} => f ∘ g

Monad Homomorphisms

structure Cslib.IsMonadHom (m : Type u_1 → Type u_2) (n : Type u_1 → Type u_3) [Monad m] [Monad n] (f : {α : Type u_1} → m α → n α) extends Cslib.IsApplicativeHom m n fun {α : Type u_1} => f : Prop

A function f is a morphism of monads if it preserves pure, >>=, <$>, <*>, <*, and *>.

• map_map {α β : Type u_1} (g : α → β) (x : m α) : f (g <$> x) = g <$> f x
• map_mapConst {α β : Type u_1} (a : α) (x : m β) : f (Functor.mapConst a x) = Functor.mapConst a (f x)
• map_pure {α : Type u_1} (a : α) : f (pure a) = pure a
• map_seq {α β : Type u_1} (x : m (α → β)) (y : Unit → m α) : f (x <*> y ()) = f x <*> f (y ())
• map_seqLeft {α β : Type u_1} (x : m α) (y : Unit → m β) : f (x <* y ()) = f x <* f (y ())
• map_seqRight {α β : Type u_1} (x : m α) (y : Unit → m β) : f (x *> y ()) = f x *> f (y ())
• map_bind {α β : Type u_1} (x : m α) (y : α → m β) : f (x >>= y) = do let x ← f x f (y x)

theorem Cslib.IsMonadHom.mk' {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [Monad m] [Monad n] [LawfulMonad m] [LawfulMonad n] {f : {α : Type u_1} → m α → n α} (map_pure : ∀ {α : Type u_1} (a : α), f (pure a) = pure a) (map_bind : ∀ {α β : Type u_1} (x : m α) (y : α → m β), f (x >>= y) = do let x ← f x f (y x)) : IsMonadHom m n fun {α : Type u_1} => f

Construct an IsMonadHom for lawful monads from map_pure and map_bind.

theorem Cslib.IsMonadHom.id (m : Type u_1 → Type u_2) [Monad m] : IsMonadHom m m fun {α : Type u_1} => id

theorem Cslib.IsMonadHom.comp {m : Type u_1 → Type u_4} {n : Type u_1 → Type u_2} {p : Type u_1 → Type u_3} [Monad m] [Monad n] [Monad p] {f : {α : Type u_1} → n α → p α} {g : {α : Type u_1} → m α → n α} (hf : IsMonadHom n p fun {α : Type u_1} => f) (hg : IsMonadHom m n fun {α : Type u_1} => g) : IsMonadHom m p fun {α : Type u_1} => f ∘ g

theorem Cslib.IsMonadHom.monadLift {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [Monad m] [Monad n] [LawfulMonad m] [LawfulMonad n] [MonadLift m n] [LawfulMonadLift m n] : IsMonadHom m n fun {α : Type u_1} => MonadLift.monadLift

theorem Cslib.IsMonadHom.monadLiftT {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [Monad m] [Monad n] [LawfulMonad m] [LawfulMonad n] [MonadLiftT m n] [LawfulMonadLiftT m n] : IsMonadHom m n fun {α : Type u_1} => monadLift

Alternative Homomorphisms

structure Cslib.IsAlternativeHom (m : Type u_1 → Type u_2) (n : Type u_1 → Type u_3) [Alternative m] [Alternative n] (f : {α : Type u_1} → m α → n α) extends Cslib.IsApplicativeHom m n fun {α : Type u_1} => f : Prop

A function f is a morphism of alternatives if it preserves pure, <$>, <*>, <*, *>, failure, and orElse.

• map_map {α β : Type u_1} (g : α → β) (x : m α) : f (g <$> x) = g <$> f x
• map_mapConst {α β : Type u_1} (a : α) (x : m β) : f (Functor.mapConst a x) = Functor.mapConst a (f x)
• map_pure {α : Type u_1} (a : α) : f (pure a) = pure a
• map_seq {α β : Type u_1} (x : m (α → β)) (y : Unit → m α) : f (x <*> y ()) = f x <*> f (y ())
• map_seqLeft {α β : Type u_1} (x : m α) (y : Unit → m β) : f (x <* y ()) = f x <* f (y ())
• map_seqRight {α β : Type u_1} (x : m α) (y : Unit → m β) : f (x *> y ()) = f x *> f (y ())
• map_failure {α : Type u_1} : f failure = failure
• map_orElse {α : Type u_1} (x : m α) (y : Unit → m α) : f (x <|> y ()) = (f x <|> f (y ()))

theorem Cslib.IsAlternativeHom.mk' {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [Alternative m] [Alternative n] [LawfulApplicative m] [LawfulApplicative n] {f : {α : Type u_1} → m α → n α} (map_pure : ∀ {α : Type u_1} (a : α), f (pure a) = pure a) (map_seq : ∀ {α β : Type u_1} (x : m (α → β)) (y : Unit → m α), f (x <*> y ()) = f x <*> f (y ())) (map_failure : ∀ {α : Type u_1}, f failure = failure) (map_orElse : ∀ {α : Type u_1} (x : m α) (y : Unit → m α), f (x <|> y ()) = (f x <|> f (y ()))) : IsAlternativeHom m n fun {α : Type u_1} => f

Construct an IsAlternativeHom for lawful applicatives from map_pure, map_seq, map_failure, and map_orElse.

theorem Cslib.IsAlternativeHom.id (m : Type u_1 → Type u_2) [Alternative m] : IsAlternativeHom m m fun {α : Type u_1} => id

theorem Cslib.IsAlternativeHom.comp {m : Type u_1 → Type u_4} {n : Type u_1 → Type u_2} {p : Type u_1 → Type u_3} [Alternative m] [Alternative n] [Alternative p] {f : {α : Type u_1} → n α → p α} {g : {α : Type u_1} → m α → n α} (hf : IsAlternativeHom n p fun {α : Type u_1} => f) (hg : IsAlternativeHom m n fun {α : Type u_1} => g) : IsAlternativeHom m p fun {α : Type u_1} => f ∘ g

Alternative Monad Homomorphisms

structure Cslib.IsAlternativeMonadHom (m : Type u_1 → Type u_2) (n : Type u_1 → Type u_3) [AlternativeMonad m] [AlternativeMonad n] (f : {α : Type u_1} → m α → n α) extends Cslib.IsMonadHom m n fun {α : Type u_1} => f, Cslib.IsAlternativeHom m n fun {α : Type u_1} => f : Prop

A function f is a morphism of alternative monads if it preserves monadic and alternative structure.

• map_map {α β : Type u_1} (g : α → β) (x : m α) : f (g <$> x) = g <$> f x
• map_mapConst {α β : Type u_1} (a : α) (x : m β) : f (Functor.mapConst a x) = Functor.mapConst a (f x)
• map_pure {α : Type u_1} (a : α) : f (pure a) = pure a
• map_seq {α β : Type u_1} (x : m (α → β)) (y : Unit → m α) : f (x <*> y ()) = f x <*> f (y ())
• map_seqLeft {α β : Type u_1} (x : m α) (y : Unit → m β) : f (x <* y ()) = f x <* f (y ())
• map_seqRight {α β : Type u_1} (x : m α) (y : Unit → m β) : f (x *> y ()) = f x *> f (y ())
• map_bind {α β : Type u_1} (x : m α) (y : α → m β) : f (x >>= y) = do let x ← f x f (y x)
• map_failure {α : Type u_1} : f failure = failure
• map_orElse {α : Type u_1} (x : m α) (y : Unit → m α) : f (x <|> y ()) = (f x <|> f (y ()))

theorem Cslib.IsAlternativeMonadHom.mk' {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [AlternativeMonad m] [AlternativeMonad n] [LawfulMonad m] [LawfulMonad n] {f : {α : Type u_1} → m α → n α} (map_pure : ∀ {α : Type u_1} (a : α), f (pure a) = pure a) (map_bind : ∀ {α β : Type u_1} (x : m α) (y : α → m β), f (x >>= y) = do let x ← f x f (y x)) (map_failure : ∀ {α : Type u_1}, f failure = failure) (map_orElse : ∀ {α : Type u_1} (x : m α) (y : Unit → m α), f (x <|> y ()) = (f x <|> f (y ()))) : IsAlternativeMonadHom m n fun {α : Type u_1} => f

Construct an IsAlternativeMonadHom for lawful monads from map_pure, map_bind, map_failure, and map_orElse.

theorem Cslib.IsAlternativeMonadHom.id (m : Type u_1 → Type u_2) [AlternativeMonad m] : IsAlternativeMonadHom m m fun {α : Type u_1} => id

theorem Cslib.IsAlternativeMonadHom.comp {m : Type u_1 → Type u_4} {n : Type u_1 → Type u_2} {p : Type u_1 → Type u_3} [AlternativeMonad m] [AlternativeMonad n] [AlternativeMonad p] {f : {α : Type u_1} → n α → p α} {g : {α : Type u_1} → m α → n α} (hf : IsAlternativeMonadHom n p fun {α : Type u_1} => f) (hg : IsAlternativeMonadHom m n fun {α : Type u_1} => g) : IsAlternativeMonadHom m p fun {α : Type u_1} => f ∘ g

theorem Cslib.IsMonadHom.wp {m : Type u_1 → Type u_2} {ps : Std.Do.PostShape} [Monad m] [Std.Do.WPMonad m ps] : IsMonadHom m (Std.Do.PredTrans ps) fun {α : Type u_1} => Std.Do.wp