Polynomial free monads with an empty result type

When α is empty, a tree in P.FreeM α has only operation nodes. The equivalence PFunctor.FreeM.equivWOfIsEmpty identifies these trees with the W-type P.W.

def PFunctor.FreeM.toWOfIsEmpty {P : PFunctor.{uA, uB}} {α : Type u} [IsEmpty α] : P.FreeM α → P.W

Regard a free polynomial tree with no return values as a W-type.

Equations

• (PFunctor.FreeM.pure a).toWOfIsEmpty = isEmptyElim a
• (PFunctor.FreeM.liftBind a cont).toWOfIsEmpty = PFunctor.W.mk (PFunctor.Obj.mk a fun (b : P.B a) => (cont b).toWOfIsEmpty)

def PFunctor.W.toFreeM {P : PFunctor.{uA, uB}} {α : Type u} : P.W → P.FreeM α

Regard a W-type as a free polynomial tree with no return nodes.

Equations

• PFunctor.W.toFreeM (WType.mk a cont) = PFunctor.FreeM.liftBind a fun (b : P.B a) => PFunctor.W.toFreeM (cont b)

@[simp]

theorem PFunctor.FreeM.toWOfIsEmpty_lift_bind {P : PFunctor.{uA, uB}} {α : Type u} [IsEmpty α] (a : P.A) (cont : P.B a → P.FreeM α) : ((lift a).bind cont).toWOfIsEmpty = W.mk (Obj.mk a fun (b : P.B a) => (cont b).toWOfIsEmpty)

@[simp]

theorem PFunctor.FreeM.toWOfIsEmpty_lift_bind' {P : PFunctor.{uA, uB}} {α : Type uB} [IsEmpty α] (a : P.A) (cont : P.B a → P.FreeM α) : (lift a >>= cont).toWOfIsEmpty = W.mk (Obj.mk a fun (b : P.B a) => (cont b).toWOfIsEmpty)

@[simp]

theorem PFunctor.W.toFreeM_mk {P : PFunctor.{uA, uB}} {α : Type u} (a : P.A) (cont : P.B a → P.W) : (mk (Obj.mk a cont)).toFreeM = (FreeM.lift a).bind fun (b : P.B a) => (cont b).toFreeM

@[simp]

theorem PFunctor.FreeM.toWOfIsEmpty_toFreeM {P : PFunctor.{uA, uB}} {α : Type u} [IsEmpty α] (x : P.W) : x.toFreeM.toWOfIsEmpty = x

@[simp]

theorem PFunctor.W.toFreeM_toWOfIsEmpty {P : PFunctor.{uA, uB}} {α : Type u} [IsEmpty α] (x : P.FreeM α) : x.toWOfIsEmpty.toFreeM = x

def PFunctor.FreeM.equivWOfIsEmpty {P : PFunctor.{uA, uB}} {α : Type u} [IsEmpty α] : P.FreeM α ≃ P.W

With an empty result type, the free polynomial monad is equivalent to its W-type.

Equations

• PFunctor.FreeM.equivWOfIsEmpty = { toFun := PFunctor.FreeM.toWOfIsEmpty, invFun := PFunctor.W.toFreeM, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem PFunctor.FreeM.equivWOfIsEmpty_apply {P : PFunctor.{uA, uB}} {α : Type u} [IsEmpty α] (a✝ : P.FreeM α) : equivWOfIsEmpty a✝ = a✝.toWOfIsEmpty

@[simp]

theorem PFunctor.FreeM.equivWOfIsEmpty_symm_apply {P : PFunctor.{uA, uB}} {α : Type u} [IsEmpty α] (a✝ : P.W) : equivWOfIsEmpty.symm a✝ = a✝.toFreeM