A construction from Bart Jacobs’ “Categorical Logic and Type Theory” book (sec. 10.4.7, pp.616–617):

[figure: 1I; \{1I\}; 1I; I; X; \{X\}; X; pX; 1I; I; 1\{Y \}; \{Y \}; Y; \{Y \}; Y; pY; \{1I\}; I; π_{1I}; \{1I\}; I; η_{I}; \{1I\}; \{X\}; \{g\}; I; \{X\}; g^{∨}; 1I; X; g; I; pX; u; \{X\}; pX; π_{X}; X; Y; f; \{X\}; \{Y \}; \{f\}; pX; pY; pf; 1I; 1\{Y \}; 1v; 1\{Y \}; Y; ϵ_{Y}; I; \{Y \}; v; \{Y \}; \{Y \}; id; \{Y \}; pY; π_{Y}; (\begin{matrix}∗ \\ i \end{matrix}); i; (\begin{matrix}∗ \\ i \end{matrix}); i, ∗; _{(\begin{matrix}b \\ a \end{matrix})}; a, b; _{(\begin{matrix}b \\ a \end{matrix})}; a; _{(\begin{matrix}∗ \\ i \end{matrix})}; i; _{(\begin{matrix}∗ \\ c, d \end{matrix})}; c, d; _{(\begin{matrix}d \\ c \end{matrix})}; c, d; _{(\begin{matrix}d \\ c \end{matrix})}; c; (\begin{matrix}∗ \\ i \end{matrix}); _{(\begin{matrix}b \\ a \end{matrix})}; i, ∗; i; i, ∗; a, b; i; a, b; i; a; _{(\begin{matrix}b \\ a \end{matrix})}; _{(\begin{matrix}d \\ c \end{matrix})}; □; a, b; a; a, b; c, d; a; c; _{(\begin{matrix}∗ \\ i \end{matrix})}; _{(\begin{matrix}∗ \\ c, d \end{matrix})}; _{(\begin{matrix}∗ \\ c, d \end{matrix})}; _{(\begin{matrix}d \\ c \end{matrix})}; i; c, d; c, d; c, d; c, d; c]

Two examples of diagrams with phantom nodes:

[figure: A; F A; A; GA; F A; GA; T A; A; A; F A; A; GA; F A; GA; T A; A; O]
[figure: A; F A; A; B; f; F A; F B; F f; B; F B; A; F A; A; B; f; F A; F B; F f; B; F B; O; O]

A diagram with relative phantom nodes:

[figure: P (X); P (U); P (X); P (V); P (U); P (W); P (V); P (W); P (W); P (∅); {p_{X}, p′_{X}}; {p_{U}}; {p_{U}}; {p_{V} , p′_{V} }; {p_{U}}; {p_{W} }; {p_{W} }; {p_{W} }; {p_{W} }; {p_{∅}}]

Same, but with the relative phantom nodes in red:

[figure: P (X); P (U); P (X); P (V); P (U); P (W); P (V); P (W); P (W); P (∅); {p_{X}, p′_{X}}; p_{X}; {p_{U}}; p′_{X}; {p_{U}}; p_{X}; p_{V}; p′_{X}; p_{V}; {p_{V} , p′_{V} }; {p_{U}}; {p_{W} }; p_{V}; {p_{W} }; p′_{V}; {p_{W} }; {p_{W} }; {p_{∅}}]

Coolored nodes and arrows: [figure: red; green; red; blue; green; blue] Some β-reductions from Bierman and de Paiva’s “On an intuitionistic modal logic” paper:

\begin{matrix}N : A & [x : A]^{1} Γ ; ⋮ . ; M : B ; (λx : A.M) : A → B [figure]I; 1 \\ (λx : A.M)N : B \end{matrix} ; [figure]E  N : A Γ ; ⋮ . ; M[x := N] : B

\begin{matrix}\begin{matrix}M : A & N : B \\ ⟨M, N⟩ : A × B \end{matrix} & ∧I \\ fst⟨M, N⟩ : A × B \end{matrix} ; ^{∧E^{1}} ⇝_{β} M : A

{M : A \atop inl(M) : A + B} ∨I [x : A]^{1} Γ ; ⋮ . ; N : C [y : B]^{1} Δ ; ⋮ . ; P : C case inl(M) of inl(x) → N || inr(y) → P ∨E ⇝_{β} M : A Γ ; ⋮ . ; N[x := M] : C

Γ ⋮ . ; M⃗ : □A [x⃗ : □A⃗]^{1} ; ⋮ . ; N : B box N with M⃗ for x⃗ : □B □I; 1 unbox(box N with M⃗ for x⃗ : □B) □E ⇝_{β} Γ ⋮ . ; M⃗ : □A⃗ ; ⋮ . ; N[x⃗ := M⃗] : B

\begin{matrix}Γ ⋮ . ; M⃗ : □A & Δ ⋮ . ; N : B ; ♢N : ♢B ♢I & [x⃗ : □A⃗ y : B]^{1} ; ⋮ . ; P : ♢C \\ P [x⃗ := M⃗, ♢y := ♢N] : ♢C \end{matrix} ; ♢E; 1 ⇝_{β} Γ ⋮ . ; M⃗ : □A Δ ⋮ . ; N : B ; ⋮ . ; P [x⃗ := M⃗, y := N] : ♢C

“P [x⃗ := M⃗, ♢y := ♢N]” is a shorthand for “let ♢y ⇐ ♢N in P with M⃗ for x⃗”.