M-types

M types are potentially infinite tree-like structures. They are defined as the greatest fixpoint of a polynomial functor.

inductive PFunctor.Approx.CofixA (F : PFunctor) : ℕ → Type u

• continue: {F : PFunctor} → PFunctor.Approx.CofixA F 0
• intro: {F : PFunctor} → {n : ℕ} → (a : F.A) → (PFunctor.B F a → PFunctor.Approx.CofixA F n) → PFunctor.Approx.CofixA F (Nat.succ n)

CofixA F n is an n level approximation of an M-type

def PFunctor.Approx.CofixA.default (F : PFunctor) [Inhabited F.A] (n : ℕ) : PFunctor.Approx.CofixA F n

default inhabitant of CofixA

Equations

• PFunctor.Approx.CofixA.default F 0 = PFunctor.Approx.CofixA.continue
• PFunctor.Approx.CofixA.default F (Nat.succ n) = PFunctor.Approx.CofixA.intro default fun x => PFunctor.Approx.CofixA.default F n

instance PFunctor.Approx.instInhabitedCofixA (F : PFunctor) [Inhabited F.A] {n : ℕ} : Inhabited (PFunctor.Approx.CofixA F n)

theorem PFunctor.Approx.cofixA_eq_zero (F : PFunctor) (x : PFunctor.Approx.CofixA F 0) (y : PFunctor.Approx.CofixA F 0) : x = y

def PFunctor.Approx.head' {F : PFunctor} {n : ℕ} : PFunctor.Approx.CofixA F (Nat.succ n) → F.A

The label of the root of the tree for a non-trivial approximation of the cofix of a pfunctor.

def PFunctor.Approx.children' {F : PFunctor} {n : ℕ} (x : PFunctor.Approx.CofixA F (Nat.succ n)) : PFunctor.B F (PFunctor.Approx.head' x) → PFunctor.Approx.CofixA F n

for a non-trivial approximation, return all the subtrees of the root

theorem PFunctor.Approx.approx_eta {F : PFunctor} {n : ℕ} (x : PFunctor.Approx.CofixA F (n + 1)) : x = PFunctor.Approx.CofixA.intro (PFunctor.Approx.head' x) (PFunctor.Approx.children' x)

inductive PFunctor.Approx.Agree {F : PFunctor} {n : ℕ} : PFunctor.Approx.CofixA F n → PFunctor.Approx.CofixA F (n + 1) → Prop

• continu: ∀ {F : PFunctor} (x : PFunctor.Approx.CofixA F 0) (y : PFunctor.Approx.CofixA F 1), PFunctor.Approx.Agree x y
• intro: ∀ {F : PFunctor} {n : ℕ} {a : F.A} (x : PFunctor.B F a → PFunctor.Approx.CofixA F n) (x' : PFunctor.B F a → PFunctor.Approx.CofixA F (n + 1)), (∀ (i : PFunctor.B F a), PFunctor.Approx.Agree (x i) (x' i)) → PFunctor.Approx.Agree (PFunctor.Approx.CofixA.intro a x) (PFunctor.Approx.CofixA.intro a x')

Relation between two approximations of the cofix of a pfunctor that state they both contain the same data until one of them is truncated

def PFunctor.Approx.AllAgree {F : PFunctor} (x : (n : ℕ) → PFunctor.Approx.CofixA F n) : Prop

Given an infinite series of approximations approx, AllAgree approx states that they are all consistent with each other.

@[simp]

theorem PFunctor.Approx.agree_trival {F : PFunctor} {x : PFunctor.Approx.CofixA F 0} {y : PFunctor.Approx.CofixA F 1} : PFunctor.Approx.Agree x y

theorem PFunctor.Approx.agree_children {F : PFunctor} {n : ℕ} (x : PFunctor.Approx.CofixA F (Nat.succ n)) (y : PFunctor.Approx.CofixA F (Nat.succ n + 1)) {i : PFunctor.B F (PFunctor.Approx.head' x)} {j : PFunctor.B F (PFunctor.Approx.head' y)} (h₀ : HEq i j) (h₁ : PFunctor.Approx.Agree x y) : PFunctor.Approx.Agree (PFunctor.Approx.children' x i) (PFunctor.Approx.children' y j)

def PFunctor.Approx.truncate {F : PFunctor} {n : ℕ} : PFunctor.Approx.CofixA F (n + 1) → PFunctor.Approx.CofixA F n

truncate a turns a into a more limited approximation

Equations

• PFunctor.Approx.truncate (PFunctor.Approx.CofixA.intro a a_1) = PFunctor.Approx.CofixA.continue
• PFunctor.Approx.truncate (PFunctor.Approx.CofixA.intro i f) = PFunctor.Approx.CofixA.intro i (PFunctor.Approx.truncate ∘ f)

theorem PFunctor.Approx.truncate_eq_of_agree {F : PFunctor} {n : ℕ} (x : PFunctor.Approx.CofixA F n) (y : PFunctor.Approx.CofixA F (Nat.succ n)) (h : PFunctor.Approx.Agree x y) : PFunctor.Approx.truncate y = x

def PFunctor.Approx.sCorec {F : PFunctor} {X : Type w} (f : X → PFunctor.Obj F X) : X → (n : ℕ) → PFunctor.Approx.CofixA F n

sCorec f i n creates an approximation of height n of the final coalgebra of f

Equations

• PFunctor.Approx.sCorec f x 0 = PFunctor.Approx.CofixA.continue
• PFunctor.Approx.sCorec f x (Nat.succ n) = PFunctor.Approx.CofixA.intro (f x).fst fun i => PFunctor.Approx.sCorec f (Sigma.snd F.A (fun x => PFunctor.B F x → X) (f x) i) n

theorem PFunctor.Approx.P_corec {F : PFunctor} {X : Type w} (f : X → PFunctor.Obj F X) (i : X) (n : ℕ) : PFunctor.Approx.Agree (PFunctor.Approx.sCorec f i n) (PFunctor.Approx.sCorec f i (Nat.succ n))

def PFunctor.Approx.Path (F : PFunctor) : Type u

Path F provides indices to access internal nodes in Corec F

instance PFunctor.Approx.Path.inhabited {F : PFunctor} : Inhabited (PFunctor.Approx.Path F)

instance PFunctor.Approx.CofixA.instSubsingleton {F : PFunctor} : Subsingleton (PFunctor.Approx.CofixA F 0)

theorem PFunctor.Approx.head_succ' {F : PFunctor} (n : ℕ) (m : ℕ) (x : (n : ℕ) → PFunctor.Approx.CofixA F n) (Hconsistent : PFunctor.Approx.AllAgree x) : PFunctor.Approx.head' (x (Nat.succ n)) = PFunctor.Approx.head' (x (Nat.succ m))

structure PFunctor.MIntl (F : PFunctor) : Type u

• approx : (n : ℕ) → PFunctor.Approx.CofixA F n

  An n-th level approximation, for each depth n

• consistent : PFunctor.Approx.AllAgree s.approx

  Each approximation agrees with the next

Internal definition for M. It is needed to avoid name clashes between M.mk and M.cases_on and the declarations generated for the structure

def PFunctor.M (F : PFunctor) : Type u

For polynomial functor F, M F is its final coalgebra

theorem PFunctor.M.default_consistent (F : PFunctor) [Inhabited F.A] (n : ℕ) : PFunctor.Approx.Agree default default

instance PFunctor.M.inhabited (F : PFunctor) [Inhabited F.A] : Inhabited (PFunctor.M F)

instance PFunctor.MIntl.inhabited (F : PFunctor) [Inhabited F.A] : Inhabited (PFunctor.MIntl F)

theorem PFunctor.M.ext' (F : PFunctor) (x : PFunctor.M F) (y : PFunctor.M F) (H : ∀ (i : ℕ), PFunctor.MIntl.approx x i = PFunctor.MIntl.approx y i) : x = y

def PFunctor.M.corec {F : PFunctor} {X : Type u_1} (f : X → PFunctor.Obj F X) (i : X) : PFunctor.M F

Corecursor for the M-type defined by F.

def PFunctor.M.head {F : PFunctor} (x : PFunctor.M F) : F.A

given a tree generated by F, head gives us the first piece of data it contains

def PFunctor.M.children {F : PFunctor} (x : PFunctor.M F) (i : PFunctor.B F (PFunctor.M.head x)) : PFunctor.M F

return all the subtrees of the root of a tree x : M F

def PFunctor.M.ichildren {F : PFunctor} [Inhabited (PFunctor.M F)] [DecidableEq F.A] (i : PFunctor.IdxCat F) (x : PFunctor.M F) : PFunctor.M F

select a subtree using an i : F.Idx or return an arbitrary tree if i designates no subtree of x

theorem PFunctor.M.head_succ {F : PFunctor} (n : ℕ) (m : ℕ) (x : PFunctor.M F) : PFunctor.Approx.head' (PFunctor.MIntl.approx x (Nat.succ n)) = PFunctor.Approx.head' (PFunctor.MIntl.approx x (Nat.succ m))

theorem PFunctor.M.head_eq_head' {F : PFunctor} (x : PFunctor.M F) (n : ℕ) : PFunctor.M.head x = PFunctor.Approx.head' (PFunctor.MIntl.approx x (n + 1))

theorem PFunctor.M.head'_eq_head {F : PFunctor} (x : PFunctor.M F) (n : ℕ) : PFunctor.Approx.head' (PFunctor.MIntl.approx x (n + 1)) = PFunctor.M.head x

theorem PFunctor.M.truncate_approx {F : PFunctor} (x : PFunctor.M F) (n : ℕ) : PFunctor.Approx.truncate (PFunctor.MIntl.approx x (n + 1)) = PFunctor.MIntl.approx x n

def PFunctor.M.dest {F : PFunctor} : PFunctor.M F → PFunctor.Obj F (PFunctor.M F)

unfold an M-type

def PFunctor.M.Approx.sMk {F : PFunctor} (x : PFunctor.Obj F (PFunctor.M F)) (n : ℕ) : PFunctor.Approx.CofixA F n

generates the approximations needed for M.mk

theorem PFunctor.M.Approx.P_mk {F : PFunctor} (x : PFunctor.Obj F (PFunctor.M F)) : PFunctor.Approx.AllAgree (PFunctor.M.Approx.sMk x)

def PFunctor.M.mk {F : PFunctor} (x : PFunctor.Obj F (PFunctor.M F)) : PFunctor.M F

constructor for M-types

inductive PFunctor.M.Agree' {F : PFunctor} : ℕ → PFunctor.M F → PFunctor.M F → Prop

• trivial: ∀ {F : PFunctor} (x y : PFunctor.M F), PFunctor.M.Agree' 0 x y
• step: ∀ {F : PFunctor} {n : ℕ} {a : F.A} (x y : PFunctor.B F a → PFunctor.M F) {x' y' : PFunctor.M F}, x' = PFunctor.M.mk { fst := a, snd := x } → y' = PFunctor.M.mk { fst := a, snd := y } → (∀ (i : PFunctor.B F a), PFunctor.M.Agree' n (x i) (y i)) → PFunctor.M.Agree' (Nat.succ n) x' y'

Agree' n relates two trees of type M F that are the same up to depth n

@[simp]

theorem PFunctor.M.dest_mk {F : PFunctor} (x : PFunctor.Obj F (PFunctor.M F)) : PFunctor.M.dest (PFunctor.M.mk x) = x

@[simp]

theorem PFunctor.M.mk_dest {F : PFunctor} (x : PFunctor.M F) : PFunctor.M.mk (PFunctor.M.dest x) = x

theorem PFunctor.M.mk_inj {F : PFunctor} {x : PFunctor.Obj F (PFunctor.M F)} {y : PFunctor.Obj F (PFunctor.M F)} (h : PFunctor.M.mk x = PFunctor.M.mk y) : x = y

def PFunctor.M.cases {F : PFunctor} {r : PFunctor.M F → Sort w} (f : (x : PFunctor.Obj F (PFunctor.M F)) → r (PFunctor.M.mk x)) (x : PFunctor.M F) : r x

destructor for M-types

def PFunctor.M.casesOn {F : PFunctor} {r : PFunctor.M F → Sort w} (x : PFunctor.M F) (f : (x : PFunctor.Obj F (PFunctor.M F)) → r (PFunctor.M.mk x)) : r x

destructor for M-types

def PFunctor.M.casesOn' {F : PFunctor} {r : PFunctor.M F → Sort w} (x : PFunctor.M F) (f : (a : F.A) → (f : PFunctor.B F a → PFunctor.M F) → r (PFunctor.M.mk { fst := a, snd := f })) : r x

destructor for M-types, similar to casesOn but also gives access directly to the root and subtrees on an M-type

theorem PFunctor.M.approx_mk {F : PFunctor} (a : F.A) (f : PFunctor.B F a → PFunctor.M F) (i : ℕ) : PFunctor.MIntl.approx (PFunctor.M.mk { fst := a, snd := f }) (Nat.succ i) = PFunctor.Approx.CofixA.intro a fun j => PFunctor.MIntl.approx (f j) i

@[simp]

theorem PFunctor.M.agree'_refl {F : PFunctor} {n : ℕ} (x : PFunctor.M F) : PFunctor.M.Agree' n x x

theorem PFunctor.M.agree_iff_agree' {F : PFunctor} {n : ℕ} (x : PFunctor.M F) (y : PFunctor.M F) : PFunctor.Approx.Agree (PFunctor.MIntl.approx x n) (PFunctor.MIntl.approx y (n + 1)) ↔ PFunctor.M.Agree' n x y

@[simp]

theorem PFunctor.M.cases_mk {F : PFunctor} {r : PFunctor.M F → Sort u_2} (x : PFunctor.Obj F (PFunctor.M F)) (f : (x : PFunctor.Obj F (PFunctor.M F)) → r (PFunctor.M.mk x)) : PFunctor.M.cases f (PFunctor.M.mk x) = f x

@[simp]

theorem PFunctor.M.casesOn_mk {F : PFunctor} {r : PFunctor.M F → Sort u_2} (x : PFunctor.Obj F (PFunctor.M F)) (f : (x : PFunctor.Obj F (PFunctor.M F)) → r (PFunctor.M.mk x)) : PFunctor.M.casesOn (PFunctor.M.mk x) f = f x

@[simp]

theorem PFunctor.M.casesOn_mk' {F : PFunctor} {r : PFunctor.M F → Sort u_2} {a : F.A} (x : PFunctor.B F a → PFunctor.M F) (f : (a : F.A) → (f : PFunctor.B F a → PFunctor.M F) → r (PFunctor.M.mk { fst := a, snd := f })) : PFunctor.M.casesOn' (PFunctor.M.mk { fst := a, snd := x }) f = f a x

inductive PFunctor.M.IsPath {F : PFunctor} : PFunctor.Approx.Path F → PFunctor.M F → Prop

• nil: ∀ {F : PFunctor} (x : PFunctor.M F), PFunctor.M.IsPath [] x
• cons: ∀ {F : PFunctor} (xs : PFunctor.Approx.Path F) {a : F.A} (x : PFunctor.M F) (f : PFunctor.B F a → PFunctor.M F) (i : PFunctor.B F a), x = PFunctor.M.mk { fst := a, snd := f } → PFunctor.M.IsPath xs (f i) → PFunctor.M.IsPath ({ fst := a, snd := i } :: xs) x

IsPath p x tells us if p is a valid path through x

theorem PFunctor.M.isPath_cons {F : PFunctor} {xs : PFunctor.Approx.Path F} {a : F.A} {a' : F.A} {f : PFunctor.B F a → PFunctor.M F} {i : PFunctor.B F a'} : PFunctor.M.IsPath ({ fst := a', snd := i } :: xs) (PFunctor.M.mk { fst := a, snd := f }) → a = a'

theorem PFunctor.M.isPath_cons' {F : PFunctor} {xs : PFunctor.Approx.Path F} {a : F.A} {f : PFunctor.B F a → PFunctor.M F} {i : PFunctor.B F a} : PFunctor.M.IsPath ({ fst := a, snd := i } :: xs) (PFunctor.M.mk { fst := a, snd := f }) → PFunctor.M.IsPath xs (f i)

def PFunctor.M.isubtree {F : PFunctor} [DecidableEq F.A] [Inhabited (PFunctor.M F)] : PFunctor.Approx.Path F → PFunctor.M F → PFunctor.M F

follow a path through a value of M F and return the subtree found at the end of the path if it is a valid path for that value and return a default tree

Equations

• One or more equations did not get rendered due to their size.
• PFunctor.M.isubtree [] x = x

def PFunctor.M.iselect {F : PFunctor} [DecidableEq F.A] [Inhabited (PFunctor.M F)] (ps : PFunctor.Approx.Path F) : PFunctor.M F → F.A

similar to isubtree but returns the data at the end of the path instead of the whole subtree

theorem PFunctor.M.iselect_eq_default {F : PFunctor} [DecidableEq F.A] [Inhabited (PFunctor.M F)] (ps : PFunctor.Approx.Path F) (x : PFunctor.M F) (h : ¬PFunctor.M.IsPath ps x) : PFunctor.M.iselect ps x = PFunctor.M.head default

@[simp]

theorem PFunctor.M.head_mk {F : PFunctor} (x : PFunctor.Obj F (PFunctor.M F)) : PFunctor.M.head (PFunctor.M.mk x) = x.fst

theorem PFunctor.M.children_mk {F : PFunctor} {a : F.A} (x : PFunctor.B F a → PFunctor.M F) (i : PFunctor.B F (PFunctor.M.head (PFunctor.M.mk { fst := a, snd := x }))) : PFunctor.M.children (PFunctor.M.mk { fst := a, snd := x }) i = x (cast (_ : PFunctor.B F (PFunctor.M.head (PFunctor.M.mk { fst := a, snd := x })) = PFunctor.B F a) i)

@[simp]

theorem PFunctor.M.ichildren_mk {F : PFunctor} [DecidableEq F.A] [Inhabited (PFunctor.M F)] (x : PFunctor.Obj F (PFunctor.M F)) (i : PFunctor.IdxCat F) : PFunctor.M.ichildren i (PFunctor.M.mk x) = PFunctor.Obj.iget x i

@[simp]

theorem PFunctor.M.isubtree_cons {F : PFunctor} [DecidableEq F.A] [Inhabited (PFunctor.M F)] (ps : PFunctor.Approx.Path F) {a : F.A} (f : PFunctor.B F a → PFunctor.M F) {i : PFunctor.B F a} : PFunctor.M.isubtree ({ fst := a, snd := i } :: ps) (PFunctor.M.mk { fst := a, snd := f }) = PFunctor.M.isubtree ps (f i)

@[simp]

theorem PFunctor.M.iselect_nil {F : PFunctor} [DecidableEq F.A] [Inhabited (PFunctor.M F)] {a : F.A} (f : PFunctor.B F a → PFunctor.M F) : PFunctor.M.iselect [] (PFunctor.M.mk { fst := a, snd := f }) = a

@[simp]

theorem PFunctor.M.iselect_cons {F : PFunctor} [DecidableEq F.A] [Inhabited (PFunctor.M F)] (ps : PFunctor.Approx.Path F) {a : F.A} (f : PFunctor.B F a → PFunctor.M F) {i : PFunctor.B F a} : PFunctor.M.iselect ({ fst := a, snd := i } :: ps) (PFunctor.M.mk { fst := a, snd := f }) = PFunctor.M.iselect ps (f i)

theorem PFunctor.M.corec_def {F : PFunctor} {X : Type u} (f : X → PFunctor.Obj F X) (x₀ : X) : PFunctor.M.corec f x₀ = PFunctor.M.mk (PFunctor.M.corec f <$> f x₀)

theorem PFunctor.M.ext_aux {F : PFunctor} [Inhabited (PFunctor.M F)] [DecidableEq F.A] {n : ℕ} (x : PFunctor.M F) (y : PFunctor.M F) (z : PFunctor.M F) (hx : PFunctor.M.Agree' n z x) (hy : PFunctor.M.Agree' n z y) (hrec : ∀ (ps : PFunctor.Approx.Path F), n = List.length ps → PFunctor.M.iselect ps x = PFunctor.M.iselect ps y) : PFunctor.MIntl.approx x (n + 1) = PFunctor.MIntl.approx y (n + 1)

theorem PFunctor.M.ext {F : PFunctor} [Inhabited (PFunctor.M F)] (x : PFunctor.M F) (y : PFunctor.M F) (H : ∀ (ps : PFunctor.Approx.Path F), PFunctor.M.iselect ps x = PFunctor.M.iselect ps y) : x = y

structure PFunctor.M.IsBisimulation {F : PFunctor} (R : PFunctor.M F → PFunctor.M F → Prop) : Prop

• head : ∀ {a a' : F.A} {f : PFunctor.B F a → PFunctor.M F} {f' : PFunctor.B F a' → PFunctor.M F}, R (PFunctor.M.mk { fst := a, snd := f }) (PFunctor.M.mk { fst := a', snd := f' }) → a = a'

  The head of the trees are equal

• tail : ∀ {a : F.A} {f f' : PFunctor.B F a → PFunctor.M F}, R (PFunctor.M.mk { fst := a, snd := f }) (PFunctor.M.mk { fst := a, snd := f' }) → ∀ (i : PFunctor.B F a), R (f i) (f' i)

  The tails are equal

Bisimulation is the standard proof technique for equality between infinite tree-like structures

theorem PFunctor.M.nth_of_bisim {F : PFunctor} (R : PFunctor.M F → PFunctor.M F → Prop) [Inhabited (PFunctor.M F)] (bisim : PFunctor.M.IsBisimulation R) (s₁ : PFunctor.M F) (s₂ : PFunctor.M F) (ps : PFunctor.Approx.Path F) : R s₁ s₂ → PFunctor.M.IsPath ps s₁ ∨ PFunctor.M.IsPath ps s₂ → PFunctor.M.iselect ps s₁ = PFunctor.M.iselect ps s₂ ∧ ∃ a f f', PFunctor.M.isubtree ps s₁ = PFunctor.M.mk { fst := a, snd := f } ∧ PFunctor.M.isubtree ps s₂ = PFunctor.M.mk { fst := a, snd := f' } ∧ ((i : PFunctor.B F a) → R (f i) (f' i))

theorem PFunctor.M.eq_of_bisim {F : PFunctor} (R : PFunctor.M F → PFunctor.M F → Prop) [Nonempty (PFunctor.M F)] (bisim : PFunctor.M.IsBisimulation R) (s₁ : PFunctor.M F) (s₂ : PFunctor.M F) : R s₁ s₂ → s₁ = s₂

def PFunctor.M.corecOn {F : PFunctor} {X : Type u_2} (x₀ : X) (f : X → PFunctor.Obj F X) : PFunctor.M F

corecursor for M F with swapped arguments

theorem PFunctor.M.dest_corec {P : PFunctor} {α : Type u} (g : α → PFunctor.Obj P α) (x : α) : PFunctor.M.dest (PFunctor.M.corec g x) = PFunctor.M.corec g <$> g x

theorem PFunctor.M.bisim {P : PFunctor} (R : PFunctor.M P → PFunctor.M P → Prop) (h : ∀ (x y : PFunctor.M P), R x y → ∃ a f f', PFunctor.M.dest x = { fst := a, snd := f } ∧ PFunctor.M.dest y = { fst := a, snd := f' } ∧ ((i : PFunctor.B P a) → R (f i) (f' i))) (x : PFunctor.M P) (y : PFunctor.M P) : R x y → x = y

theorem PFunctor.M.bisim' {P : PFunctor} {α : Type u_2} (Q : α → Prop) (u : α → PFunctor.M P) (v : α → PFunctor.M P) (h : ∀ (x : α), Q x → ∃ a f f', PFunctor.M.dest (u x) = { fst := a, snd := f } ∧ PFunctor.M.dest (v x) = { fst := a, snd := f' } ∧ ∀ (i : PFunctor.B P a), ∃ x', Q x' ∧ f i = u x' ∧ f' i = v x') (x : α) : Q x → u x = v x

theorem PFunctor.M.bisim_equiv {P : PFunctor} (R : PFunctor.M P → PFunctor.M P → Prop) (h : ∀ (x y : PFunctor.M P), R x y → ∃ a f f', PFunctor.M.dest x = { fst := a, snd := f } ∧ PFunctor.M.dest y = { fst := a, snd := f' } ∧ ((i : PFunctor.B P a) → R (f i) (f' i))) (x : PFunctor.M P) (y : PFunctor.M P) : R x y → x = y

theorem PFunctor.M.corec_unique {P : PFunctor} {α : Type u} (g : α → PFunctor.Obj P α) (f : α → PFunctor.M P) (hyp : ∀ (x : α), PFunctor.M.dest (f x) = f <$> g x) : f = PFunctor.M.corec g

def PFunctor.M.corec₁ {P : PFunctor} {α : Type u} (F : (X : Type u) → (α → X) → α → PFunctor.Obj P X) : α → PFunctor.M P

corecursor where the state of the computation can be sent downstream in the form of a recursive call

def PFunctor.M.corec' {P : PFunctor} {α : Type u} (F : {X : Type u} → (α → X) → α → PFunctor.M P ⊕ PFunctor.Obj P X) (x : α) : PFunctor.M P

corecursor where it is possible to return a fully formed value at any point of the computation