Displayed families over PFunctor.FreeM

This file defines displayed algebras over the free monad of a polynomial functor.

For a polynomial/container P, a payload type α, and a tree s : PFunctor.FreeM P α, FreeM.Displayed D s is the family obtained by interpreting terminal payloads through D.leaf and internal positions through D.node.

This is the common substrate behind several familiar structures:

• decorations, where each node stores metadata and recursively decorates every child;
• paths, where each node chooses one child and recursively follows that child;
• compact observations, where some nodes may be skipped or otherwise reinterpreted.

Categorically, this is the displayed algebra generated over the initial FreeM algebra. A Displayed.Section D is a global dependent section: it chooses data in the displayed fiber over every tree. Constructor-local fold data produces such a section via Displayed.Section.ofConstructors.

structure PFunctor.FreeM.Displayed.Algebra (P : PFunctor.{uA, uB}) (α : Type v) : Type (max (max (max uA uB) v) w)

A large algebra generating displayed fibers over FreeM P α.

The leaf argument interprets terminal payloads. The node argument interprets a polynomial position a : P.A, given the already-generated displayed fibers for each child b : P.B a.

Special cases include node decorations, branch paths, and compact observation views that suppress uninformative nodes.

• leaf : α → Sort w

  The fiber assigned to a terminal payload x : α.

• node (a : P.A) : (P.B a → Sort w) → Sort w

  The fiber assigned to a node at position a, given the fibers already chosen for each child b : P.B a.

@[implicit_reducible]

def PFunctor.FreeM.Displayed {P : PFunctor.{uA, uB}} {α : Type v} (D : Displayed.Algebra P α) : P.FreeM α → Sort w

Evaluate a displayed algebra over a concrete FreeM tree.

This generates the displayed fiber at every tree by recursion on the free polynomial structure.

@[simp]

theorem PFunctor.FreeM.Displayed.pure_eq {P : PFunctor.{uA, uB}} {α : Type v} (D : Algebra P α) (x : α) : Displayed D (pure x) = D.leaf x

theorem PFunctor.FreeM.Displayed.liftBind_eq {P : PFunctor.{uA, uB}} {α : Type v} (D : Algebra P α) (a : P.A) (rest : P.B a → P.FreeM α) : Displayed D (liftBind a rest) = D.node a fun (b : P.B a) => Displayed D (rest b)

structure PFunctor.FreeM.Displayed.Over.Algebra {P : PFunctor.{uA, uB}} {α : Type v} (D : Displayed.Algebra P α) : Type (max (max (max (max uA uB) v) w) w₂)

A dependent displayed algebra over an existing displayed algebra.

If D assigns a fiber to each FreeM tree, then an Over.Algebra D assigns a second-layer fiber over each inhabitant of Displayed D s. This is the generic form of a dependent decoration over a base decoration.

• leaf (x : α) : D.leaf x → Sort w₂

  The second-layer fiber over a base leaf fiber at payload x : α.

• node (a : P.A) (children : P.B a → Sort w) : ((b : P.B a) → children b → Sort w₂) → D.node a children → Sort w₂

  The second-layer fiber over a base node fiber at position a, given the second-layer fibers already chosen over each child.

@[implicit_reducible]

def PFunctor.FreeM.Displayed.Over {P : PFunctor.{uA, uB}} {α : Type v} {D : Algebra P α} (E : Over.Algebra D) (s : P.FreeM α) : Displayed D s → Sort w₂

Evaluate a dependent displayed algebra over concrete displayed data.

This is the dependent analogue of Displayed: the base displayed data chooses which second-layer fiber is available at every node.

@[simp]

theorem PFunctor.FreeM.Displayed.Over.pure_eq {P : PFunctor.{uA, uB}} {α : Type v} {D : Displayed.Algebra P α} (E : Algebra D) (x : α) (d : D.leaf x) : Over E (pure x) d = E.leaf x d

theorem PFunctor.FreeM.Displayed.Over.liftBind_eq {P : PFunctor.{uA, uB}} {α : Type v} {D : Displayed.Algebra P α} (E : Algebra D) (a : P.A) (rest : P.B a → P.FreeM α) (d : D.node a fun (b : P.B a) => Displayed D (rest b)) : Over E (liftBind a rest) d = E.node a (fun (b : P.B a) => Displayed D (rest b)) (fun (b : P.B a) (d : Displayed D (rest b)) => Over E (rest b) d) d

@[reducible, inline]

abbrev PFunctor.FreeM.Displayed.Over.Total {P : PFunctor.{uA, uB}} {α : Type v} {D : Displayed.Algebra P α} (E : Algebra D) (s : P.FreeM α) : Sort (max (max 1 w) u_1)

The total space of a displayed family together with one displayed-over layer.

@[reducible, inline]

abbrev PFunctor.FreeM.Displayed.Section {P : PFunctor.{uA, uB}} {α : Type v} (D : Algebra P α) : Sort (imax (max (max (uB + 1) (uA + 1)) (v + 1)) u_1)

A section chooses displayed data over every FreeM tree.

def PFunctor.FreeM.Displayed.Section.ofConstructors {P : PFunctor.{uA, uB}} {α : Type v} {D : Algebra P α} (onLeaf : (x : α) → D.leaf x) (onNode : (a : P.A) → (children : P.B a → Sort w) → ((b : P.B a) → children b) → D.node a children) : Section D

Construct a section from constructor-local data.

This is the displayed-family specialization of the dependent recursor for FreeM.

@[simp]

theorem PFunctor.FreeM.Displayed.Section.ofConstructors_pure {P : PFunctor.{uA, uB}} {α : Type v} {D : Algebra P α} (onLeaf : (x : α) → D.leaf x) (onNode : (a : P.A) → (children : P.B a → Sort w) → ((b : P.B a) → children b) → D.node a children) (x : α) : ofConstructors onLeaf onNode (pure x) = onLeaf x

theorem PFunctor.FreeM.Displayed.Section.ofConstructors_liftBind {P : PFunctor.{uA, uB}} {α : Type v} {D : Algebra P α} (onLeaf : (x : α) → D.leaf x) (onNode : (a : P.A) → (children : P.B a → Sort w) → ((b : P.B a) → children b) → D.node a children) (a : P.A) (rest : P.B a → P.FreeM α) : ofConstructors onLeaf onNode (liftBind a rest) = onNode a (fun (b : P.B a) => Displayed D (rest b)) fun (b : P.B a) => ofConstructors onLeaf onNode (rest b)

structure PFunctor.FreeM.Displayed.Hom {P : PFunctor.{uA, uB}} {α : Type v} (D : Algebra P α) (E : Algebra P α) : Sort (max (max (max (max (uA + 1) (uB + 1)) (v + 1)) w) w₂)

A morphism between two displayed families over the same FreeM tree.

• toFun (s : P.FreeM α) : Displayed D s → Displayed E s

  The fiberwise action, mapping the D-fiber to the E-fiber over each tree s.

@[instance_reducible]

instance PFunctor.FreeM.Displayed.instCoeFunHomForallForall {P : PFunctor.{uA, uB}} {α : Type v} {D : Algebra P α} {E : Algebra P α} : CoeFun (Hom D E) fun (x : Hom D E) => (s : P.FreeM α) → Displayed D s → Displayed E s

theorem PFunctor.FreeM.Displayed.Hom.ext {P : PFunctor.{uA, uB}} {α : Type v} {D : Algebra P α} {E : Algebra P α} (f g : Hom D E) (h : ∀ (s : P.FreeM α) (d : Displayed D s), f.toFun s d = g.toFun s d) : f = g

theorem PFunctor.FreeM.Displayed.Hom.ext_iff {P : PFunctor.{uA, uB}} {α : Type v} {D : Algebra P α} {E : Algebra P α} {f g : Hom D E} : f = g ↔ ∀ (s : P.FreeM α) (d : Displayed D s), f.toFun s d = g.toFun s d

def PFunctor.FreeM.Displayed.Hom.id {P : PFunctor.{uA, uB}} {α : Type v} {D : Algebra P α} : Hom D D

Identity morphism of a displayed family.

def PFunctor.FreeM.Displayed.Hom.comp {P : PFunctor.{uA, uB}} {α : Type v} {D : Algebra P α} {E : Algebra P α} {F : Algebra P α} (g : Hom E F) (f : Hom D E) : Hom D F

Composition of displayed-family morphisms.

@[simp]

theorem PFunctor.FreeM.Displayed.Hom.id_apply {P : PFunctor.{uA, uB}} {α : Type v} {D : Algebra P α} (s : P.FreeM α) (d : Displayed D s) : Hom.id.toFun s d = d

@[simp]

theorem PFunctor.FreeM.Displayed.Hom.comp_apply {P : PFunctor.{uA, uB}} {α : Type v} {D : Algebra P α} {E : Algebra P α} {F : Algebra P α} (g : Hom E F) (f : Hom D E) (s : P.FreeM α) (d : Displayed D s) : (g.comp f).toFun s d = g.toFun s (f.toFun s d)

@[simp]

theorem PFunctor.FreeM.Displayed.Hom.comp_id {P : PFunctor.{uA, uB}} {α : Type v} {D : Algebra P α} {E : Algebra P α} (f : Hom D E) : Hom.id.comp f = f

@[simp]

theorem PFunctor.FreeM.Displayed.Hom.id_comp {P : PFunctor.{uA, uB}} {α : Type v} {D : Algebra P α} {E : Algebra P α} (f : Hom D E) : f.comp Hom.id = f

theorem PFunctor.FreeM.Displayed.Hom.comp_assoc {P : PFunctor.{uA, uB}} {α : Type v} {D : Algebra P α} {E : Algebra P α} {F : Algebra P α} {G : Algebra P α} (h : Hom F G) (g : Hom E F) (f : Hom D E) : h.comp (g.comp f) = (h.comp g).comp f

structure PFunctor.FreeM.Displayed.LocalMap {P : PFunctor.{uA, uB}} {α : Type v} (D : Algebra P α) (E : Algebra P α) : Type (max (max (max (max uA uB) v) w) w₂)

A constructor-local map between displayed algebras.

The mapNode field maps one node layer, given already-mapped recursive child data. This is transformation data sufficient to recursively produce a tree-indexed Displayed.Hom via LocalMap.toHom; it is intentionally not called a homomorphism because an arbitrary, potentially negative Algebra.node need not admit identity or composition at this local level.

• mapLeaf (x : α) : D.leaf x → E.leaf x

  The action on leaf fibers, mapping D.leaf x to E.leaf x.

• mapNode (a : P.A) (sourceChildren : P.B a → Sort w) (targetChildren : P.B a → Sort w₂) : ((b : P.B a) → sourceChildren b → targetChildren b) → D.node a sourceChildren → E.node a targetChildren

  The action on one node layer, mapping D.node to E.node given the already-mapped child data.

def PFunctor.FreeM.Displayed.LocalMap.toHomFun {P : PFunctor.{uA, uB}} {α : Type v} {D : Algebra P α} {E : Algebra P α} (η : LocalMap D E) (s : P.FreeM α) : Displayed D s → Displayed E s

The recursive function underlying LocalMap.toHom.

def PFunctor.FreeM.Displayed.LocalMap.toHom {P : PFunctor.{uA, uB}} {α : Type v} {D : Algebra P α} {E : Algebra P α} (η : LocalMap D E) : Hom D E

Interpret a constructor-local map as a tree-indexed displayed morphism.

@[simp]

theorem PFunctor.FreeM.Displayed.LocalMap.toHom_pure {P : PFunctor.{uA, uB}} {α : Type v} {D : Algebra P α} {E : Algebra P α} (η : LocalMap D E) (x : α) (d : D.leaf x) : η.toHom.toFun (pure x) d = η.mapLeaf x d

theorem PFunctor.FreeM.Displayed.LocalMap.toHom_liftBind {P : PFunctor.{uA, uB}} {α : Type v} {D : Algebra P α} {E : Algebra P α} (η : LocalMap D E) (a : P.A) (rest : P.B a → P.FreeM α) (d : D.node a fun (b : P.B a) => Displayed D (rest b)) : η.toHom.toFun (liftBind a rest) d = η.mapNode a (fun (b : P.B a) => Displayed D (rest b)) (fun (b : P.B a) => Displayed E (rest b)) (fun (b : P.B a) => η.toHom.toFun (rest b)) d

structure PFunctor.FreeM.Displayed.Over.Hom {P : PFunctor.{uA, uB}} {α : Type v} {D : Displayed.Algebra P α} {E : Displayed.Algebra P α} (η : Displayed.Hom D E) (R : Algebra D) (S : Algebra E) : Sort (max (max (max (max (max (uA + 1) (uB + 1)) (v + 1)) w) w₅) w₆)

A morphism between displayed-over families, lying over a morphism between their base displayed families.

When the base morphism is Displayed.Hom.id, this is a fiberwise morphism over the same displayed data.

• toFun (s : P.FreeM α) (d : Displayed D s) : Over R s d → Over S s (η.toFun s d)

  The fiberwise action on second-layer fibers, sending the R-fiber over d to the S-fiber over η s d.

@[instance_reducible]

instance PFunctor.FreeM.Displayed.Over.instCoeFunHomForallForallForallToFun {P : PFunctor.{uA, uB}} {α : Type v} {D : Displayed.Algebra P α} {E : Displayed.Algebra P α} {R : Algebra D} {S : Algebra E} {η : Displayed.Hom D E} : CoeFun (Hom η R S) fun (x : Hom η R S) => (s : P.FreeM α) → (d : Displayed D s) → Over R s d → Over S s (η.toFun s d)

theorem PFunctor.FreeM.Displayed.Over.Hom.ext {P : PFunctor.{uA, uB}} {α : Type v} {D : Displayed.Algebra P α} {E : Displayed.Algebra P α} {R : Algebra D} {S : Algebra E} {η : Displayed.Hom D E} (f g : Hom η R S) (h : ∀ (s : P.FreeM α) (d : Displayed D s) (r : Over R s d), f.toFun s d r = g.toFun s d r) : f = g

theorem PFunctor.FreeM.Displayed.Over.Hom.ext_iff {P : PFunctor.{uA, uB}} {α : Type v} {D : Displayed.Algebra P α} {E : Displayed.Algebra P α} {R : Algebra D} {S : Algebra E} {η : Displayed.Hom D E} {f g : Hom η R S} : f = g ↔ ∀ (s : P.FreeM α) (d : Displayed D s) (r : Over R s d), f.toFun s d r = g.toFun s d r

def PFunctor.FreeM.Displayed.Over.Hom.id {P : PFunctor.{uA, uB}} {α : Type v} {D : Displayed.Algebra P α} (R : Algebra D) : Hom Displayed.Hom.id R R

Identity morphism of a displayed-over family.

def PFunctor.FreeM.Displayed.Over.Hom.comp {P : PFunctor.{uA, uB}} {α : Type v} {D : Displayed.Algebra P α} {E : Displayed.Algebra P α} {F : Displayed.Algebra P α} {R : Algebra D} {S : Algebra E} {T : Algebra F} {η : Displayed.Hom D E} {θ : Displayed.Hom E F} (g : Hom θ S T) (f : Hom η R S) : Hom (θ.comp η) R T

Composition of displayed-over morphisms over composed base morphisms.

@[simp]

theorem PFunctor.FreeM.Displayed.Over.Hom.id_apply {P : PFunctor.{uA, uB}} {α : Type v} {D : Displayed.Algebra P α} {R : Algebra D} (s : P.FreeM α) (d : Displayed D s) (r : Over R s d) : (Hom.id R).toFun s d r = r

@[simp]

theorem PFunctor.FreeM.Displayed.Over.Hom.comp_apply {P : PFunctor.{uA, uB}} {α : Type v} {D : Displayed.Algebra P α} {E : Displayed.Algebra P α} {F : Displayed.Algebra P α} {R : Algebra D} {S : Algebra E} {T : Algebra F} {η : Displayed.Hom D E} {θ : Displayed.Hom E F} (g : Hom θ S T) (f : Hom η R S) (s : P.FreeM α) (d : Displayed D s) (r : Over R s d) : (g.comp f).toFun s d r = g.toFun s (η.toFun s d) (f.toFun s d r)

@[simp]

theorem PFunctor.FreeM.Displayed.Over.Hom.comp_id {P : PFunctor.{uA, uB}} {α : Type v} {D : Displayed.Algebra P α} {E : Displayed.Algebra P α} {R : Algebra D} {S : Algebra E} {η : Displayed.Hom D E} (f : Hom η R S) : (Hom.id S).comp f = f

@[simp]

theorem PFunctor.FreeM.Displayed.Over.Hom.id_comp {P : PFunctor.{uA, uB}} {α : Type v} {D : Displayed.Algebra P α} {E : Displayed.Algebra P α} {R : Algebra D} {S : Algebra E} {η : Displayed.Hom D E} (f : Hom η R S) : f.comp (Hom.id R) = f

theorem PFunctor.FreeM.Displayed.Over.Hom.comp_assoc {P : PFunctor.{uA, uB}} {α : Type v} {D : Displayed.Algebra P α} {E : Displayed.Algebra P α} {F : Displayed.Algebra P α} {G : Displayed.Algebra P α} {R : Algebra D} {S : Algebra E} {T : Algebra F} {η : Displayed.Hom D E} {θ : Displayed.Hom E F} {ι : Displayed.Hom F G} {U : Algebra G} (h : Hom ι T U) (g : Hom θ S T) (f : Hom η R S) : h.comp (g.comp f) = (h.comp g).comp f

def PFunctor.FreeM.Displayed.Over.map {P : PFunctor.{uA, uB}} {α : Type v} {D : Displayed.Algebra P α} {E : Displayed.Algebra P α} {R : Algebra D} {S : Algebra E} {η : Displayed.Hom D E} (f : Hom η R S) (s : P.FreeM α) (d : Displayed D s) : Over R s d → Over S s (η.toFun s d)

Map displayed-over data by a displayed-over morphism.

@[simp]

theorem PFunctor.FreeM.Displayed.Over.map_apply {P : PFunctor.{uA, uB}} {α : Type v} {D : Displayed.Algebra P α} {E : Displayed.Algebra P α} {R : Algebra D} {S : Algebra E} {η : Displayed.Hom D E} (f : Hom η R S) (s : P.FreeM α) (d : Displayed D s) (r : Over R s d) : map f s d r = f.toFun s d r

@[simp]

theorem PFunctor.FreeM.Displayed.Over.map_id {P : PFunctor.{uA, uB}} {α : Type v} {D : Displayed.Algebra P α} {R : Algebra D} (s : P.FreeM α) (d : Displayed D s) (r : Over R s d) : map (Hom.id R) s d r = r

@[simp]

theorem PFunctor.FreeM.Displayed.Over.map_comp {P : PFunctor.{uA, uB}} {α : Type v} {D : Displayed.Algebra P α} {E : Displayed.Algebra P α} {F : Displayed.Algebra P α} {R : Algebra D} {S : Algebra E} {T : Algebra F} {η : Displayed.Hom D E} {θ : Displayed.Hom E F} (g : Hom θ S T) (f : Hom η R S) (s : P.FreeM α) (d : Displayed D s) (r : Over R s d) : map (g.comp f) s d r = map g s (η.toFun s d) (map f s d r)

structure PFunctor.FreeM.Displayed.Over.FiberLocalMap {P : PFunctor.{uA, uB}} {α : Type v} {D : Displayed.Algebra P α} (R : Algebra D) (S : Algebra D) : Type (max (max (max (max (max uA uB) v) w) w₅) w₆)

A constructor-local fiber map between dependent displayed algebras over the same base displayed algebra.

This is transformation data for recursively mapping only the over-layer while keeping the base displayed data fixed. FiberLocalMap.toHom interprets it as a genuine tree-indexed Displayed.Over.Hom.

• mapLeaf (x : α) (d : D.leaf x) : R.leaf x d → S.leaf x d

  The action on leaf fibers, mapping R.leaf to S.leaf over the same base leaf data.

• mapNode (a : P.A) (children : P.B a → Sort w) (sourceOver : (b : P.B a) → children b → Sort w₅) (targetOver : (b : P.B a) → children b → Sort w₆) : ((b : P.B a) → (d : children b) → sourceOver b d → targetOver b d) → (d : D.node a children) → R.node a children sourceOver d → S.node a children targetOver d

  The action on one node layer, mapping R.node to S.node over the same base node data, given the already-mapped child data.

@[implicit_reducible]

def PFunctor.FreeM.Displayed.Over.FiberLocalMap.toHomFun {P : PFunctor.{uA, uB}} {α : Type v} {D : Displayed.Algebra P α} {R' : Algebra D} {S' : Algebra D} (η : FiberLocalMap R' S') (s : P.FreeM α) (d : Displayed D s) : Over R' s d → Over S' s d

The recursive function underlying FiberLocalMap.toHom.

@[implicit_reducible]

def PFunctor.FreeM.Displayed.Over.FiberLocalMap.toHom {P : PFunctor.{uA, uB}} {α : Type v} {D : Displayed.Algebra P α} {R' : Algebra D} {S' : Algebra D} (η : FiberLocalMap R' S') : Hom Displayed.Hom.id R' S'

Interpret a constructor-local fiber map as a displayed-over morphism.

@[simp]

theorem PFunctor.FreeM.Displayed.Over.FiberLocalMap.toHom_pure {P : PFunctor.{uA, uB}} {α : Type v} {D : Displayed.Algebra P α} {R' : Algebra D} {S' : Algebra D} (η : FiberLocalMap R' S') (x : α) (d : D.leaf x) (r : R'.leaf x d) : η.toHom.toFun (pure x) d r = η.mapLeaf x d r

theorem PFunctor.FreeM.Displayed.Over.FiberLocalMap.toHom_liftBind {P : PFunctor.{uA, uB}} {α : Type v} {D : Displayed.Algebra P α} {R' : Algebra D} {S' : Algebra D} (η : FiberLocalMap R' S') (a : P.A) (rest : P.B a → P.FreeM α) (d : D.node a fun (b : P.B a) => Displayed D (rest b)) (r : R'.node a (fun (b : P.B a) => Displayed D (rest b)) (fun (b : P.B a) (d : Displayed D (rest b)) => Over R' (rest b) d) d) : η.toHom.toFun (liftBind a rest) d r = η.mapNode a (fun (b : P.B a) => Displayed D (rest b)) (fun (b : P.B a) (d : Displayed D (rest b)) => Over R' (rest b) d) (fun (b : P.B a) (d : Displayed D (rest b)) => Over S' (rest b) d) (fun (b : P.B a) (d : Displayed D (rest b)) => η.toHom.toFun (rest b) d) d r

structure PFunctor.FreeM.Displayed.Over.LocalMap {P : PFunctor.{uA, uB}} {α : Type v} {D : Displayed.Algebra P α} {E : Displayed.Algebra P α} (η : Displayed.LocalMap D E) (R : Algebra D) (S : Algebra E) : Type (max (max (max (max (max (max uA uB) v) w) w₂) w₅) w₆)

A constructor-local map between dependent displayed algebras, lying over a constructor-local map between their base displayed algebras.

Its interpretation by Over.LocalMap.toHom is a genuine tree-indexed Displayed.Over.Hom over the interpreted base map.

• mapLeaf (x : α) (d : D.leaf x) : R.leaf x d → S.leaf x (η.mapLeaf x d)

  The action on leaf fibers, mapping R.leaf to S.leaf over the base leaf morphism η.mapLeaf.

• mapNode (a : P.A) (sourceChildren : P.B a → Sort w) (targetChildren : P.B a → Sort w₂) (mapChild : (b : P.B a) → sourceChildren b → targetChildren b) (sourceOver : (b : P.B a) → sourceChildren b → Sort w₅) (targetOver : (b : P.B a) → targetChildren b → Sort w₆) : ((b : P.B a) → (d : sourceChildren b) → sourceOver b d → targetOver b (mapChild b d)) → (d : D.node a sourceChildren) → R.node a sourceChildren sourceOver d → S.node a targetChildren targetOver (η.mapNode a sourceChildren targetChildren mapChild d)

  The action on one node layer, mapping R.node to S.node over the base node morphism η.mapNode, given the already-mapped child data.

def PFunctor.FreeM.Displayed.Over.LocalMap.toHomFun {P : PFunctor.{uA, uB}} {α : Type v} {D : Displayed.Algebra P α} {E : Displayed.Algebra P α} {R : Algebra D} {S : Algebra E} {η : Displayed.LocalMap D E} (φ : LocalMap η R S) (s : P.FreeM α) (d : Displayed D s) : Over R s d → Over S s (η.toHom.toFun s d)

The recursive function underlying Over.LocalMap.toHom.

def PFunctor.FreeM.Displayed.Over.LocalMap.toHom {P : PFunctor.{uA, uB}} {α : Type v} {D : Displayed.Algebra P α} {E : Displayed.Algebra P α} {R : Algebra D} {S : Algebra E} {η : Displayed.LocalMap D E} (φ : LocalMap η R S) : Hom η.toHom R S

Interpret a constructor-local over map as a displayed-over morphism over the interpreted base morphism.

@[simp]

theorem PFunctor.FreeM.Displayed.Over.LocalMap.toHom_pure {P : PFunctor.{uA, uB}} {α : Type v} {D : Displayed.Algebra P α} {E : Displayed.Algebra P α} {R : Algebra D} {S : Algebra E} {η : Displayed.LocalMap D E} (φ : LocalMap η R S) (x : α) (d : D.leaf x) (r : R.leaf x d) : φ.toHom.toFun (pure x) d r = φ.mapLeaf x d r

theorem PFunctor.FreeM.Displayed.Over.LocalMap.toHom_liftBind {P : PFunctor.{uA, uB}} {α : Type v} {D : Displayed.Algebra P α} {E : Displayed.Algebra P α} {R : Algebra D} {S : Algebra E} {η : Displayed.LocalMap D E} (φ : LocalMap η R S) (a : P.A) (rest : P.B a → P.FreeM α) (d : D.node a fun (b : P.B a) => Displayed D (rest b)) (r : R.node a (fun (b : P.B a) => Displayed D (rest b)) (fun (b : P.B a) (d : Displayed D (rest b)) => Over R (rest b) d) d) : φ.toHom.toFun (liftBind a rest) d r = φ.mapNode a (fun (b : P.B a) => Displayed D (rest b)) (fun (b : P.B a) => Displayed E (rest b)) (fun (b : P.B a) => η.toHom.toFun (rest b)) (fun (b : P.B a) (d : Displayed D (rest b)) => Over R (rest b) d) (fun (b : P.B a) (d : Displayed E (rest b)) => Over S (rest b) d) (fun (b : P.B a) (d : Displayed D (rest b)) => φ.toHom.toFun (rest b) d) d r

def PFunctor.FreeM.Displayed.map {P : PFunctor.{uA, uB}} {α : Type v} {D : Algebra P α} {E : Algebra P α} (f : Hom D E) (s : P.FreeM α) : Displayed D s → Displayed E s

Map displayed data by an interpreted morphism.

@[simp]

theorem PFunctor.FreeM.Displayed.map_apply {P : PFunctor.{uA, uB}} {α : Type v} {D : Algebra P α} {E : Algebra P α} (f : Hom D E) (s : P.FreeM α) (d : Displayed D s) : map f s d = f.toFun s d

@[simp]

theorem PFunctor.FreeM.Displayed.map_id {P : PFunctor.{uA, uB}} {α : Type v} {D : Algebra P α} (s : P.FreeM α) (d : Displayed D s) : map Hom.id s d = d

@[simp]

theorem PFunctor.FreeM.Displayed.map_comp {P : PFunctor.{uA, uB}} {α : Type v} {D : Algebra P α} {E : Algebra P α} {F : Algebra P α} (g : Hom E F) (f : Hom D E) (s : P.FreeM α) (d : Displayed D s) : map (g.comp f) s d = map g s (map f s d)