Displayed families over PFunctor.FreeM

This file defines displayed-family shapes 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 the corresponding displayed catamorphism: it chooses data in the displayed fiber over every tree.

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

A displayed-family shape over FreeM P α.

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

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

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

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

Evaluate a displayed-family shape 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 : Shape P α) (x : α) : Displayed D (pure x) = D.leaf x

@[simp]

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

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

A displayed family over an existing displayed family.

If D assigns a fiber to each FreeM tree, then an OverShape 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₂
• node (a : P.A) (child : P.B a → Sort w) : ((b : P.B a) → child b → Sort w₂) → D.node a child → Sort w₂

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

Evaluate a displayed-over shape 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 : Shape P α} (E : OverShape D) (x : α) (d : D.leaf x) : Over E (pure x) d = E.leaf x d

@[simp]

theorem PFunctor.FreeM.Displayed.Over.roll_eq {P : PFunctor.{uA, uB}} {α : Type v} {D : Shape P α} (E : OverShape 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 (roll a rest) d = E.node a (fun (b : P.B a) => Displayed D (rest b)) (fun (b : P.B a) (d : (fun (b : P.B a) => Displayed D (rest b)) b) => Over E (rest b) d) d

@[reducible, inline]

abbrev PFunctor.FreeM.Displayed.Total {P : PFunctor.{uA, uB}} {α : Type v} {D : Shape P α} (E : OverShape 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 : Shape 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.ofConstruct {P : PFunctor.{uA, uB}} {α : Type v} {D : Shape P α} (leafSec : (x : α) → D.leaf x) (nodeSec : (a : P.A) → (child : P.B a → Sort w) → ((b : P.B a) → child b) → D.node a child) : 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.ofConstruct_pure {P : PFunctor.{uA, uB}} {α : Type v} {D : Shape P α} (leafSec : (x : α) → D.leaf x) (nodeSec : (a : P.A) → (child : P.B a → Sort w) → ((b : P.B a) → child b) → D.node a child) (x : α) : ofConstruct leafSec nodeSec (pure x) = leafSec x

@[simp]

theorem PFunctor.FreeM.Displayed.Section.ofConstruct_roll {P : PFunctor.{uA, uB}} {α : Type v} {D : Shape P α} (leafSec : (x : α) → D.leaf x) (nodeSec : (a : P.A) → (child : P.B a → Sort w) → ((b : P.B a) → child b) → D.node a child) (a : P.A) (rest : P.B a → P.FreeM α) : ofConstruct leafSec nodeSec (roll a rest) = nodeSec a (fun (b : P.B a) => Displayed D (rest b)) fun (b : P.B a) => ofConstruct leafSec nodeSec (rest b)

structure PFunctor.FreeM.Displayed.Hom {P : PFunctor.{uA, uB}} {α : Type v} (D : Shape P α) (E : Shape 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

@[implicit_reducible]

instance PFunctor.FreeM.Displayed.instCoeFunHomForallForall {P : PFunctor.{uA, uB}} {α : Type v} {D : Shape P α} {E : Shape 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 : Shape P α} {E : Shape 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 : Shape P α} {E : Shape 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 : Shape P α} : Hom D D

Identity morphism of a displayed family.

def PFunctor.FreeM.Displayed.Hom.comp {P : PFunctor.{uA, uB}} {α : Type v} {D : Shape P α} {E : Shape P α} {F : Shape 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 : Shape 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 : Shape P α} {E : Shape P α} {F : Shape 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 : Shape P α} {E : Shape 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 : Shape P α} {E : Shape P α} (f : Hom D E) : f.comp Hom.id = f

theorem PFunctor.FreeM.Displayed.Hom.comp_assoc {P : PFunctor.{uA, uB}} {α : Type v} {D : Shape P α} {E : Shape P α} {F : Shape P α} {G : Shape 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.LocalHom {P : PFunctor.{uA, uB}} {α : Type v} (D : Shape P α) (E : Shape P α) : Type (max (max (max (max uA uB) v) w) w₂)

A constructor-local morphism between displayed-family shapes.

The mapChild field maps one node layer, given already-mapped recursive child data.

• mapLeaf (x : α) : D.leaf x → E.leaf x
• mapChild (a : P.A) (childD : P.B a → Sort w) (childE : P.B a → Sort w₂) : ((b : P.B a) → childD b → childE b) → D.node a childD → E.node a childE

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

The recursive function underlying LocalHom.toHom.

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

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

@[simp]

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

@[simp]

theorem PFunctor.FreeM.Displayed.LocalHom.toHom_roll {P : PFunctor.{uA, uB}} {α : Type v} {D : Shape P α} {E : Shape P α} (η : LocalHom 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 (roll a rest) d = η.mapChild 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 : Shape P α} {E : Shape P α} (η : Displayed.Hom D E) (R : OverShape D) (S : OverShape E) : Sort (max (max (max (max (max (uA + 1) (uB + 1)) u_1) u_2) (v + 1)) 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)

@[implicit_reducible]

instance PFunctor.FreeM.Displayed.Over.instCoeFunHomForallForallForallToFun {P : PFunctor.{uA, uB}} {α : Type v} {D : Shape P α} {E : Shape P α} {R : OverShape D} {S : OverShape 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 : Shape P α} {E : Shape P α} {R : OverShape D} {S : OverShape 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 : Shape P α} {E : Shape P α} {R : OverShape D} {S : OverShape 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 : Shape P α} (R : OverShape 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 : Shape P α} {E : Shape P α} {F : Shape P α} {R : OverShape D} {S : OverShape E} {T : OverShape 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 : Shape P α} {R : OverShape 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 : Shape P α} {E : Shape P α} {F : Shape P α} {R : OverShape D} {S : OverShape E} {T : OverShape 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 : Shape P α} {E : Shape P α} {R : OverShape D} {S : OverShape 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 : Shape P α} {E : Shape P α} {R : OverShape D} {S : OverShape 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 : Shape P α} {E : Shape P α} {F : Shape P α} {G : Shape P α} {R : OverShape D} {S : OverShape E} {T : OverShape F} {η : Displayed.Hom D E} {θ : Displayed.Hom E F} {ι : Displayed.Hom F G} {U : OverShape 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 : Shape P α} {E : Shape P α} {R : OverShape D} {S : OverShape 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 : Shape P α} {E : Shape P α} {R : OverShape D} {S : OverShape 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 : Shape P α} {R : OverShape 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 : Shape P α} {E : Shape P α} {F : Shape P α} {R : OverShape D} {S : OverShape E} {T : OverShape 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.FiberLocalHom {P : PFunctor.{uA, uB}} {α : Type v} {D : Shape P α} (R : OverShape D) (S : OverShape D) : Type (max (max (max (max (max uA uB) v) w) w₅) w₆)

A constructor-local morphism between displayed-over families over the same base displayed family.

This is the local recursion principle for maps that change only the over-layer data and keep the base displayed data fixed.

• mapLeaf (x : α) (d : D.leaf x) : R.leaf x d → S.leaf x d
• mapChild (a : P.A) (child : P.B a → Sort w) (overR : (b : P.B a) → child b → Sort w₅) (overS : (b : P.B a) → child b → Sort w₆) : ((b : P.B a) → (d : child b) → overR b d → overS b d) → (d : D.node a child) → R.node a child overR d → S.node a child overS d

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

The recursive function underlying FiberLocalHom.toHom.

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

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

@[simp]

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

@[simp]

theorem PFunctor.FreeM.Displayed.Over.FiberLocalHom.toHom_roll {P : PFunctor.{uA, uB}} {α : Type v} {D : Shape P α} {R' : OverShape D} {S' : OverShape D} (η : FiberLocalHom 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 : (fun (b : P.B a) => Displayed D (rest b)) b) => Over R' (rest b) d) d) : η.toHom.toFun (roll a rest) d r = η.mapChild a (fun (b : P.B a) => Displayed D (rest b)) (fun (b : P.B a) (d : (fun (b : P.B a) => Displayed D (rest b)) b) => Over R' (rest b) d) (fun (b : P.B a) (d : (fun (b : P.B a) => Displayed D (rest b)) b) => Over S' (rest b) d) (fun (b : P.B a) (d : (fun (b : P.B a) => Displayed D (rest b)) b) => η.toHom.toFun (rest b) d) d r

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

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

• mapLeaf (x : α) (d : D.leaf x) : R.leaf x d → S.leaf x (η.mapLeaf x d)
• mapChild (a : P.A) (childD : P.B a → Sort w) (childE : P.B a → Sort w₂) (baseChild : (b : P.B a) → childD b → childE b) (overR : (b : P.B a) → childD b → Sort w₅) (overS : (b : P.B a) → childE b → Sort w₆) : ((b : P.B a) → (d : childD b) → overR b d → overS b (baseChild b d)) → (d : D.node a childD) → R.node a childD overR d → S.node a childE overS (η.mapChild a childD childE baseChild d)

def PFunctor.FreeM.Displayed.Over.LocalHom.toHomFun {P : PFunctor.{uA, uB}} {α : Type v} {D : Shape P α} {E : Shape P α} {R : OverShape D} {S : OverShape E} {η : Displayed.LocalHom D E} (φ : LocalHom η 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.LocalHom.toHom.

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

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

@[simp]

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

@[simp]

theorem PFunctor.FreeM.Displayed.Over.LocalHom.toHom_roll {P : PFunctor.{uA, uB}} {α : Type v} {D : Shape P α} {E : Shape P α} {R : OverShape D} {S : OverShape E} {η : Displayed.LocalHom D E} (φ : LocalHom η 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 : (fun (b : P.B a) => Displayed D (rest b)) b) => Over R (rest b) d) d) : φ.toHom.toFun (roll a rest) d r = φ.mapChild 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 : (fun (b : P.B a) => Displayed D (rest b)) b) => Over R (rest b) d) (fun (b : P.B a) (d : (fun (b : P.B a) => Displayed E (rest b)) b) => Over S (rest b) d) (fun (b : P.B a) (d : (fun (b : P.B a) => Displayed D (rest b)) b) => φ.toHom.toFun (rest b) d) d r

def PFunctor.FreeM.Displayed.map {P : PFunctor.{uA, uB}} {α : Type v} {D : Shape P α} {E : Shape 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 : Shape P α} {E : Shape 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 : Shape 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 : Shape P α} {E : Shape P α} {F : Shape 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)