linear/non-linear setting like ours, but we think that our presentation is
simpler and more compact, because we simply interpret type expressions as
functors $T:\mathbf{A}_{e}\times\mathbf{B}_{e}\to\mathbf{B}_{e}$. In addition,
our categorical models can be easily simplified for languages that have only
inductive datatypes (recursive types allowing only $\otimes$ and $+$). In such
a case, $\mathbf{CPO}$-enrichment from the model may be removed and our
semantics can be adapted quite easily.

In [PPRZ20a, PPRZ20b], the authors present a denotational semantics for the
first-order quantum programming language QPL extended with inductive datatypes
(i.e., datatypes formed using $\otimes$ and $+$, but not $\multimap$ and $!$).
This type system is not equipped with $\multimap$ and $!$ types and in order
to model copying of classical information, the authors use methods based on
the work reported here (and in [LMZ19]) that shows how to construct the
required comonoids.

##  9\. Conclusion and Future Work

We introduced a new language called LNL-FPC, which can be seen as extending
FPC with a mixed linear/non-linear typing discipline (§2). An interesting
feature of our type system is that it has implicit weakening and contraction
rules – the users of the language do not have to explicitly specify when to
copy and discard non-linear variables, while still enjoying linear type
checking for the linear variables.

We presented a big-step call-by-value operational semantics for the language
and showed that a previously known canonical fixpoint operator on terms
[LMZ18] may be derived via the isorecursive type structure, thereby recreating
an important result from FPC (§3).

In preparation for the denotational semantics of the language, we first had to
establish some new coherence properties between (parameterised) initial
algebras defined in potentially different categories and related by
appropriate mediating functors (§4).

We then described our categorical model, which is a $\mathbf{CPO}$-enriched
model of Intuitionistic Linear Logic with suitable $\omega$-colimits (§5). A
crucial insight of our approach and of our model, is that non-linear types
that correspond to mixed-variance functors can be seen as _covariant_ functors
both on the linear category of embeddings, but also on the non-linear category
of _pre-embeddings_. We also presented an entire class of concrete models that
have found applications not only in classical functional programming, but also
in programming languages for certain emerging fields (quantum computation and
diagrammatic languages).

We proved our denotational semantics sound (§6) and cemented our results by
demonstrating a computational adequacy result (§7). In doing so, we provided
two kinds of denotational interpretations for non-linear types, terms and
contexts – a standard interpretation within the linear category, and one
within the cartesian category – that we showed are very strongly related to
one another via a coherent natural isomorphism. This isomorphism, in turn,
allowed us to elegantly interpret the substructural operations of
Intuitionistic Linear Logic and in particular we precisely described the
canonical comonoid structure of the non-linear (recursive) types. This, in
turn, required developing new techniques for solving recursive domain
equations within a cartesian category, which is perhaps the main contribution
of this paper. More specifically, we showed that the solution of many (mixed-
variance) recursive domain equations on the linear side (constructed over
embeddings) can be reflected onto the cartesian side (by constructing them
over pre-embeddings) and this result can be of interest even without our sound
and adequate semantics.

As part of future work we would like to investigate what additional
categorical structure (if any) is required in order to design and model a type
system similar to ours, but where the substructural rules for promotion and
dereliction are also implicit. In practical terms, this would result in a
programming language that is more convenient for use, while still retaining
the benefits of linear type checking. In theoretical terms, the categorical
treatment could lead to a better understanding of the underlying design
principles.

Another line of future work is to consider a more abstract model of LNL-FPC
where the $\mathbf{CPO}$-enrichment of our model is axiomatised away. This is
a challenging problem, but if resolved, this could help to discover additional
models of LNL-FPC.

## Acknowledgments

We thank Samson Abramsky, Chris Heunen, Mathys Rennela, Francisco Rios and
Peter Selinger for discussions regarding this paper. We also thank the
anonymous ICFP and LMCS referees for their feedback, which led to multiple
improvements of the paper. We thank the Simons Institute for the Theory of
Computing where the initial part of this work took place. We also thank
Schloss Dagstuhl \- Leibniz Center for Informatics for hosting us during the
Quantum Programming Languages seminar where another part of the work took
place.

This work was partially funded by the AFOSR under the MURI grant number
FA9550-16-1-0082 entitled, "Semantics, Formal Reasoning, and Tool Support for
Quantum Programming". Vladimir Zamdzhiev is also supported by the French
projects ANR-17-CE25-0009 SoftQPro and PIA-GDN/Quantex.

## References

  * [Abr93] Samson Abramsky.  Computational interpretations of linear logic.  Theor. Comput. Sci., 111(1&2):3–57, 1993.
  * [Adá74] Jiří Adámek.  Free algebras and automata realizations in the language of categories.  Commentationes Mathematicae Universitatis Carolinae, 15(4):589–602, 1974.
  * [AF96] M. Abadi and M. P. Fiore.  Syntactic considerations on recursive types.  In Proceedings 11th Annual IEEE Symposium on Logic in Computer Science, pages 242–252, July 1996.
  * [AJ94] S. Abramsky and A. Jung.  Handbook of logic in computer science (vol. 3).  chapter Domain Theory, pages 1–168. Oxford University Press, Oxford, UK, 1994.
  * [AMM18] Jiří Adámek, Stefan Milius, and Lawrence S Moss.  Fixed points of functors.  Journal of Logical and Algebraic Methods in Programming, 95:41–81, 2018.
  * [Bar96] Andrew Barber.  Dual intuitionistic linear logic, 1996.  Technical Report, University of Edinburgh.
  * [BBN+17] Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R. Newton, Simon Peyton Jones, and Arnaud Spiwack.  Linear haskell: Practical linearity in a higher-order polymorphic language.  Proc. ACM Program. Lang., 2(POPL):5:1–5:29, December 2017.
  * [Ben95] P.N. Benton.  A mixed linear and non-linear logic: Proofs, terms and models.  In Computer Science Logic: 8th Workshop, CSL ’94, Selected Papaers, 1995.
  * [Bor94] F. Borceux.  Handbook of Categorical Algebra 2: Categories and Structures.  Cambridge University Press, 1994.
  * [BPR00] Gavin M. Bierman, Andrew M. Pitts, and Claudio V. Russo.  Operational properties of lily, a polymorphic linear lambda calculus with recursion.  Electr. Notes Theor. Comput. Sci., 41(3):70–88, 2000.
  * [Bra97] T. Braüner.  A general adequacy result for a linear funcitonal language.  Theoretical Computer Science, 177:27–58, 1997.
  * [BW96] P. N. Benton and P. Wadler.  Linear logic, monads and the lambda calculus.  In LICS 1996, 1996.
  * [CPT16] L. Caires, F. Pfenning, and B. Toninho.  Linear logic propositions as session types.  Mathematical Structures in Computer Science, 26(3):367–423, 2016\.
  * [Day74] B. Day.  On closed categories of functors ii.  In Category Seminar: Proceedings Sydney Category Theory Seminar 1972/1973, pages 20–54, 1974.
  * [Epp03] Adam Eppendahl.  Categories and types for axiomatic domain theory.  PhD thesis, Queen Mary University of London, UK, 2003.
  * [Fio94] M. P. Fiore.  Axiomatic domain theory in categories of partial maps.  PhD thesis, University of Edinburgh, UK, 1994.
  * [FP94] Marcelo Fiore and Gordon Plotkin.  An axiomatization of computationally adequate domain theoretic models of FPC.  In LICS, pages 92–102. IEEE Computer Society, 1994.
  * [Gir87] J.-Y. Girard.  Linear logic.  Theoretical Computer Science, 50:1 – 101, 1987.
  * [Lev04] Paul Blain Levy.  Call-By-Push-Value: A Functional/Imperative Synthesis.  Springer, 2004.
  * [LMZ18] Bert Lindenhovius, Michael Mislove, and Vladimir Zamdzhiev.  Enriching a linear/non-linear lambda calculus: A programming language for string diagrams.  In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 659–668. ACM, 2018.
  * [LMZ19] Bert Lindenhovius, Michael Mislove, and Vladimir Zamdzhiev.  Mixed linear and non-linear recursive types.  Proc. ACM Program. Lang., 3(ICFP):111:1–111:29, August 2019.
  * [LMZ20] Bert Lindenhovius, Michael Mislove, and Vladimir Zamdzhiev.  Semantics for a lambda calculus for string diagrams, 2020.  Preprint.
  * [LS81] Daniel J Lehmann and Michael B Smyth.  Algebraic specification of data types: A synthetic approach.  Mathematical Systems Theory, 1981.
  * [MBR08] Rasmus Ejlers Møgelberg, Lars Birkedal, and Giuseppe Rosolini.  Synthetic domain theory and models of linear abadi & plotkin logic.  Ann. Pure Appl. Logic, 155(2):115–133, 2008.
  * [ML98] Saunders Mac Lane.  Categories for the Working Mathematician (2nd ed.).  Springer, 1998.
  * [Mor16] J. Garrett Morris.  The best of both worlds: Linear functional programming without compromise.  SIGPLAN Not., 51(9):448–461, September 2016.
  * [MSS13] Octavio Malherbe, Philip Scott, and Peter Selinger.  Presheaf Models of Quantum Computation: An Outline, pages 178–194.  Springer Berlin Heidelberg, Berlin, Heidelberg, 2013.
  * [Pit96] Andrew M. Pitts.  Relational properties of domains.  Inf. Comput., 127(2):66–90, 1996.
  * [Plo85] G. D. Plotkin.  Lectures on predomains and partial functions. notes for a course given at csli stanford university., 1985.
  * [PPRZ20a] Romain Péchoux, Simon Perdrix, Mathys Rennela, and Vladimir Zamdzhiev.  Quantum programming with inductive datatypes, 2020.  Preprint.
  * [PPRZ20b] Romain Péchoux, Simon Perdrix, Mathys Rennela, and Vladimir Zamdzhiev.  Quantum programming with inductive datatypes: Causality and affine type theory.  In Foundations of Software Science and Computation Structures - 23rd International Conference, FOSSACS 2020, volume 12077 of Lecture Notes in Computer Science, pages 562–581. Springer, 2020.
  * [PSV14] Michele Pagani, Peter Selinger, and Benoît Valiron.  Applying quantitative semantics to higher-order quantum computing.  In Suresh Jagannathan and Peter Sewell, editors, The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20-21, 2014, pages 647–658. ACM, 2014\.
  * [RS04] Giuseppe Rosolini and Alex Simpson.  Using synthetic domain theory to prove operational properties of a polymorphic programming language based on strictness, 2004.  Manuscript.
  * [RS17] Francisco Rios and Peter Selinger.  A categorical model for a quantum circuit description language.  In QPL 2017, volume 266 of EPTCS, 2017.
  * [RS18] Mathys Rennela and Sam Staton.  Classical control and quantum circuits in enriched category theory.  Electr. Notes Theor. Comput. Sci., 336:257–279, 2018.
  * [SP82] M.B. Smyth and G.D. Plotkin.  The category-theoretic solution of recursive domain equations.  Siam J. Comput., 1982.
  * [TP11] Jesse A. Tov and Riccardo Pucella.  Practical affine types.  In POPL ’11, 2011.
  * [Wad90] Philip Wadler.  Linear types can change the world!  In PROGRAMMING CONCEPTS AND METHODS. North, 1990.

##  Appendix A Omitted Proofs

###  A.1. Proof of Lemma 13

######  Proof A.1.

For brevity we write $T_{A},T_{B},T_{f}$ for $T(A,-),T(B,-),T(f,-)$
respectively.

First, observe that $(T_{f}^{*n})_{X}=T(f,T(f,\cdots T(f,X)\cdots).$

Therefore, $(S(T_{f}))_{n}=(T_{f}^{*n})_{\varnothing}=T(f,T(f,\cdots
T(f,\varnothing)\cdots).$

Next, observe that $T_{A}^{n}(g)=T(A,T(A,\cdots T(A,g)\cdots).$

Next, we have

$\displaystyle(T_{f}*S(T_{f}))_{n}=((T_{f}*S(T_{B}))\circ(T_{A}*S(T_{f})))_{n}$
$\displaystyle=T(f,T_{B}^{n}(\varnothing))\circ
T(A,(T^{*n}_{f})_{\varnothing})$
$\displaystyle=T(f,(T^{*n}_{f})_{\varnothing})=(T_{f}^{*n+1})_{\varnothing}.$

And therefore

$\displaystyle((T_{f}*S(T_{f}))\circ s^{T_{A}})_{n}$
$\displaystyle=(T_{f}^{*n+1})_{\varnothing}\circ
T_{A}^{n}(\iota_{T_{A}\varnothing})$ $\displaystyle=T(f,T(f,\cdots
T(f,T(f,\varnothing))\cdots)\circ T(A,T(A,\cdots
T(A,\iota_{T_{A}\varnothing})\cdots)$ $\displaystyle=T(f,T(f,\cdots
T(f,T(f,\varnothing)\circ\iota_{T_{A}\varnothing})\cdots)$
$\displaystyle=T(f,T(f,\cdots T(f,\iota_{T_{B}\varnothing})\cdots)$
$\displaystyle=T_{B}^{n}(\iota_{T_{B}\varnothing})\circ(T_{f}^{*n})_{\varnothing}$
$\displaystyle=(s^{T_{B}}\circ S(T_{f}))_{n}$

###  A.2. Proof of Lemma 14

######  Proof A.2.

Composing $\tau_{n}:D_{n}\to D_{n}^{\prime}$ with
$d_{n}^{\prime}:D_{n}^{\prime}\to D_{\omega}^{\prime}$ yields a morphism
$d_{n}^{\prime}\circ\tau_{n}:D_{n}\to D_{\omega}^{\prime}$ for each
$n\in\omega$, which forms a cocone of the diagram $D$. Since $D_{\omega}$ is
the colimit of $D$, then $\mathrm{colim}(\tau):D_{\omega}\to
D_{\omega}^{\prime}$ is by definition the unique map such that

$\mathrm{colim}(\tau)\circ d_{n}=d^{\prime}_{n}\circ\tau_{n},$

hence by functoriality of $T$, we obtain

$T\mathrm{colim}(\tau)\circ Td_{n}=Td^{\prime}_{n}\circ T\tau_{n}$ (14)

for each $n\in\omega$. Now, $T\circ D:\omega\to\mathbf{B}$ is an
$\omega$-diagram and since $T$ preserves the colimit of $D$, it follows
$TD_{\omega}$ is the colimit of $T\circ D$ with colimiting morphisms
$Td_{n}:TD_{n}\to TD_{\omega}$ for each $n\in\omega$. Similarly,
$TD_{\omega}^{\prime}$ is the colimit of $T\circ D^{\prime}$ with colimiting
morphisms ${Td_{n}^{\prime}:TD_{n}^{\prime}\to TD_{\omega}^{\prime}}$. Then
$Td^{\prime}_{n}\circ T\tau_{n}:TD_{n}\to TD_{\omega}^{\prime}$ forms a cocone
of the diagram $T\circ D$, and by definition
$\mathrm{colim}(T\tau):TD_{\omega}\to TD_{\omega}^{\prime}$ is the unique
morphism such that

$\mathrm{colim}(T\tau)\circ Td_{n}=Td^{\prime}_{n}\circ T\tau_{n}.$

It follows now from (14) that $T\mathrm{colim}(\tau)=\mathrm{colim}(T\tau)$.

###  A.3. Proof of Lemma 15

######  Proof A.3.

By Notation 4.3, $(D_{\omega},d_{n})_{n\in\omega}$ is the colimiting cocone of
$D$. By definition of $\omega$-functors, it follows that
$(TD_{\omega},Td_{n})_{n\in\omega}$ and $(HD_{\omega},Hd_{n})_{n\in\omega}$
are the colimiting cocones of $T\circ D$ and $H\circ D$, respectively. Then
$(HD_{\omega},Hd_{n}\circ\tau_{D_{n}})_{n\in\omega}$ is a cocone of $TD$, and
by definition $\mathrm{colim}(\tau D):TD_{\omega}\to HD_{\omega}$ is the
unique morphism such that

$\mathrm{colim}(\tau D)\circ Td_{n}=Hd_{n}\circ\tau_{D_{n}}$

for each $n\in\omega$. On the other hand, by naturality of $\tau:T\Rightarrow
H$, we have

$\tau_{D_{\omega}}\circ Td_{n}=Hd_{n}\circ\tau_{D_{n}},$

for each $n\in\omega$, hence we must have $\mathrm{colim}(\tau
D)=\tau_{D_{\omega}}$.

###  A.4. Proof of Lemma 20

######  Proof A.4.

First, we have to show that for each $A\in\mathbf{A}$, we have that

$\alpha^{*}_{A}:S(T(NA,-))\Rightarrow M\circ S(H(A,-):\omega\to\mathbf{D}$

is natural in $\omega$, i.e., we have to show that

$MS(H(A,-))(n\leq n+1)\circ(\alpha_{A}^{*})_{n}=(\alpha^{*}_{A})_{n+1}\circ
S(T(NA,-)(n\leq n+1))$ (15)

for each $n\in\omega$. Let $\iota_{1}:0\to T(NA,0)$ and
$\iota_{2}:\varnothing\to H(A,\varnothing)$ be the indicated unique morphisms.
By definition, equation (15) is then equivalent to:

$MH(A,-)^{n}\iota_{2}\circ(\alpha^{*}_{A})_{n}=(\alpha^{*}_{A})_{n+1}\circ
T(NA,-)^{n}\iota_{1}.$ (16)

When $n=0$, the equality becomes $M\iota_{2}\circ
z=(\alpha^{*}_{A})_{1}\circ\iota_{1},$ which is true by initiality. We proceed
by induction, so assume that (16) holds for $n$. Expanding the equality for
$n+1$, by definition of $\alpha^{*}_{A}$, we get following diagram:

$\mathbf{C}$$\mathbf{L}$$F$

$\vdash$

$G$$T(A_{1},T^{\dagger}A_{1})$$T(A_{2},T^{\dagger}A_{2})$$T(f,T^{\dagger}f)$$T^{\dagger}A_{1}$$T^{\dagger}A_{2}$$\phi^{T}_{A_{1}}$$\phi^{T}_{A_{2}}$$T^{\dagger}f$$T(A_{1},T^{\dagger}A_{1})$$T(A_{1},T^{\dagger}A_{2})$$T(A_{1},T^{\dagger}f)$$T^{\dagger}A_{1}$$T^{\dagger}A_{2}$$\phi^{T}_{A_{1}}$$T(A_{2},T^{\dagger}A_{2})$$T(f,T^{\dagger}A_{2})$$\phi^{T}_{A_{2}}$$T^{\dagger}f$$S(T(A,-))$$T(A,-)\circ
S(T(A,-))$$T(B,-)\circ
S(T(B,-))$$S(T(B,-))$$S(T(f,-))$$T(f,-)*S(T(f,-))$$s^{T(A,-)}$$s^{T(B,-)}$$T(\mathrm{colim}(\tau))$$T(\mathrm{colim}(D))$$\mathrm{colim}(T\circ
D)$$\mathrm{colim}(T\tau)$$T(\mathrm{colim}(D^{\prime}))$$\mathrm{colim}(T\circ
D^{\prime})$$\tau_{\mathrm{colim}(D)}$$T(\mathrm{colim}(D))$$\mathrm{colim}(T\circ
D)$$\mathrm{colim}(\tau D)$$H(\mathrm{colim}(D))$$\mathrm{colim}(H\circ
D)$$T^{\dagger}A$$\mathrm{colim}(S(T_{A}))$$\mathrm{colim}(T_{A}\circ
S(T_{A}))$$T_{A}\mathrm{colim}(S(T_{A}))$$T(A,T^{\dagger}A)$$T^{\dagger}B$$\mathrm{colim}(S(T_{B}))$$\mathrm{colim}(T_{B}\circ
S(T_{B}))$$T_{B}\mathrm{colim}(S(T_{B}))$$T(B,T^{\dagger}B)$$\mathrm{colim}(s^{T_{A}})$$T(f,T^{\dagger}f)$$\mathrm{colim}(T_{f}*S(T_{f}))$$\mathrm{colim}(S(T_{f}))$$T^{\dagger}f$$\mathrm{colim}(s^{T_{B}})$$T_{f}\mathrm{colim}(S(T_{f}))$(1)(4)(3)(2)$T_{A}{\mathrm{colim}(S(T_{f}))}$$T_{A}(\mathrm{colim}(S(T_{A})))$$\mathrm{colim}(T_{A}\circ
S(T_{A})$$\mathrm{colim}(T_{A}S(T_{f}))$$T_{A}(\mathrm{colim}(S(T_{B})))$$\mathrm{colim}(T_{A}S(T_{B}))$$\mathrm{colim}(T_{f}S(T_{B}))$$T_{f}\mathrm{colim}(S(T_{B}))$$T_{B}(\mathrm{colim}(S(T_{B})))$$\mathrm{colim}(T_{B}\circ
S(T_{B}))$$\mathbf{C}\times\mathbf{D}$$\mathbf{A}\times\mathbf{B}$$\mathbf{D}$$\mathbf{B}$$T$$M$$N\times
M$$H$$\alpha$$T^{\dagger}NA$$\mathrm{colim}(T^{*}NA)$$\mathrm{colim}(MH^{*}A)$$M\mathrm{colim}(H^{*}A)$$MH^{\dagger}A$$T^{\dagger}NB$$\mathrm{colim}(T^{*}NB)$$\mathrm{colim}(MH^{*}B)$$M\mathrm{colim}(H^{*}B)$$MH^{\dagger}B$$\mathrm{colim}(\alpha_{A}^{*})$$MH^{\dagger}f$$\mathrm{colim}(MH^{*}f)$$\mathrm{colim}(T^{*}Nf)$$T^{\dagger}Nf$$\mathrm{colim}(\alpha_{B}^{*})$$M\mathrm{colim}(H^{*}f)$(1)(4)(3)(2)$S(T)$$MS(H)$$MHS(H)$$TS(T)$$TMS(H)$$s^{T}$$\alpha^{*}$$Ms^{H}$$T\alpha^{*}$$\alpha*S(H)$$M\circ
H\circ\langle\text{Id},H^{\dagger}\rangle$$T\circ\langle N,T^{\dagger}\circ
N\rangle$$T\circ\langle N,M\circ
H^{\dagger}\rangle$$T\circ\langle\text{Id},T^{\dagger}\rangle\circ
N$$T\circ(N\times M)\circ\langle\text{Id},H^{\dagger}\rangle$$M\circ
H^{\dagger}$$T^{\dagger}\circ
N$$\alpha\langle\text{Id},H^{\dagger}\rangle$$M\phi^{H}$$\phi^{T}N$$T\langle
N,\alpha^{\dagger}\rangle$$\alpha^{\dagger}$$MH^{\prime}Y(H^{\prime})$$T^{\prime}Y(T^{\prime})$$T^{\prime}\alpha^{\dagger}_{A}$$T^{\prime}MY(H^{\prime})$$\alpha_{A,Y(H^{\prime})}$$MY(H^{\prime})$$Y(T^{\prime})$$y^{T^{\prime}}$$My^{H^{\prime}}$$\alpha^{\dagger}_{A}$$\mathbf{C}$$\mathbf{D}$$T\circ\langle\text{Id},T^{\dagger}\rangle$$T^{\dagger}$$\phi^{T}$$\mathbf{A}$$\mathbf{B}$$H\circ\langle\text{Id},H^{\dagger}\rangle$$H^{\dagger}$$\phi^{H}$$M$$N$$\mathbf{C}$$\mathbf{L}$$F$

$\vdash$

$G$$\mathbf{C}$$\mathbf{L}$$F$

$\vdash$

$G$$\mathbf{CPO}$$\mathbf{CPO}_{\perp!}$$(-)_{\perp}$

$\vdash$

$U$$\mathbf{CPO}_{\perp!}$$\widehat{}\mathbf{M}$$-\circledcirc I$

$\vdash$

$\widehat{}\mathbf{M}(I,-)$$\mathbf{CPO}$$\mathbf{CPO}_{\perp!}$$(-)_{\perp}$

$\vdash$

$U$$\widehat{}\mathbf{M}$$-\circledcirc I$

$\vdash$

$\widehat{}\mathbf{M}(I,-)$${\llbracket\Theta\vdash
P\rrbracket}$$F_{pe}^{\times|\Theta|}$$\mathbf{C}_{pe}$$\mathbf{L}_{e}$$\mathbf{C}_{pe}^{|\Theta|}$${\llparenthesis\Theta\vdash
P\rrparenthesis}$$F_{pe}$$\mathbf{L}_{e}^{|\Theta|}$$\alpha$${\llbracket\Theta\vdash
P[R/X]\rrbracket}\circ
F_{pe}^{\times|\Theta|}$$F_{pe}\circ{\llparenthesis\Theta\vdash
P[R/X]\rrparenthesis}$$F_{pe}\circ{\llparenthesis\Theta,X\vdash
P\rrparenthesis}\circ\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle$${\llbracket\Theta,X\vdash P\rrbracket}\circ\langle
F_{pe}^{\times|\Theta|},{\llbracket\Theta\vdash R\rrbracket}\circ
F_{pe}^{\times|\Theta|}\rangle$${\llbracket\Theta,X\vdash
P\rrbracket}\circ\langle
F_{pe}^{\times|\Theta|},F_{pe}\circ{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle$${\llbracket\Theta,X\vdash
P\rrbracket}\circ\langle\text{Id},{\llbracket\Theta\vdash
R\rrbracket}\rangle\circ F_{pe}^{\times|\Theta|}$${\llbracket\Theta,X\vdash
P\rrbracket}\circ
F_{pe}^{\times(|\Theta|+1)}\circ\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle$$\alpha\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle$${\llbracket\Theta,X\vdash P\rrbracket}\langle
F_{pe}^{\times|\Theta|},\alpha\rangle$$\alpha$$F_{pe}\gamma^{-1}$${\llbracket\Theta\vdash
P[\mu X.P/X]\rrbracket}\circ
F_{pe}^{\times|\Theta|}$$F_{pe}\circ{\llparenthesis\Theta\vdash P[\mu
X.P/X]\rrparenthesis}$$\alpha$${\llbracket\Theta\vdash\mu X.P\rrbracket}\circ
F_{pe}^{\times|\Theta|}$$F_{pe}\circ{\llparenthesis\Theta\vdash\mu
X.P\rrparenthesis}$$\alpha$$\mathrm{fold}F_{pe}^{\times|\Theta|}$$F_{pe}\mathpzc{fold}$$\mathbf{R}(A)_{e}\times\mathbf{R}(B)_{e}$$\mathbf{R}(A\star
B)_{e}$$\star_{e}^{A,B}$$\mathbf{L}_{e}\times\mathbf{L}_{e}$$\mathbf{L}_{e}$$\star_{e}$$U^{A\star
B}_{e}$$U^{A}_{e}\times
U^{B}_{e}$$!_{e}$$\mathbf{R}(!A)_{e}$$U^{A}_{e}$$\mathbf{L}_{e}$$\mathbf{R}(A)_{e}$$!_{e}^{A}$$U^{!A}_{e}$$\mathbf{L}_{e}$$\mathbf{R}(C_{1})_{e}\times\cdots\times\mathbf{R}(C_{n})_{e}$$\mathbf{R}(A[\vec{C}/\Theta])_{e}$${{\lVert\Theta\vdash
A\rVert^{\vec{C}}}}$$\mathbf{L}_{e}\times\cdots\times\mathbf{L}_{e}$$\mathbf{L}_{e}$${\llbracket\Theta\vdash
A\rrbracket}$$U^{A[\vec{C}/\Theta]}_{e}$$U^{C_{1}}_{e}\times\cdots\times
U^{C_{n}}_{e}$$\mathbf{R}(C_{1})_{e}\times\cdots\times\mathbf{R}(C_{n})_{e}$$\mathbf{R}(A[\vec{C}/\Theta])_{e}$$\phi$$\mathbf{L}_{e}\times\cdots\times\mathbf{L}_{e}$$\mathbf{L}_{e}$${\llbracket\Theta,X\vdash
A\rrbracket}\circ\langle\text{Id},{\llbracket\Theta\vdash\mu
X.A\rrbracket}\rangle$$\phi$${{\lVert\Theta\vdash\mu
X.A\rVert^{\vec{C}}}}$${\llbracket\Theta\vdash\mu
X.A\rrbracket}$$U^{A[\vec{C}/\Theta]}_{e}$$U^{C_{1}}_{e}\times\cdots\times
U^{C_{n}}_{e}$$\mathbb{I}^{\mu
X.A[\vec{C}/\Theta]}_{e}\circ{\lVert\Theta,X\vdash A\rVert^{\vec{C},\mu
X.A[\vec{C}/\Theta]}}\circ\langle\text{Id},{{\lVert\Theta\vdash\mu
X.A\rVert^{\vec{C}}}}\rangle$$MH(A,-)^{n+2}\varnothing$$MH(A,-)^{n+1}\varnothing$$T(NA,MH(A,-)^{n+1}\varnothing)$$\alpha_{A,H(A,-)^{n}\varnothing}$$T(NA,MH(A,-)^{n}\iota_{2})$$\alpha_{A,H(A,-)^{n+1}\varnothing}$$T(NA,(\alpha^{*}_{A})_{n})$$T(NA,(\alpha^{*}_{A})_{n+1})$$T(NA,-)^{n+1}0$$T(NA,-)^{n+2}0$$MH(A,-)^{n+1}\iota_{2}$$T(NA,-)^{n+1}\iota_{1}$$(2)$$(1)$$T(NA,MH(A,-)^{n}\varnothing)$

Here the outer square is just equation (16) for $n+1$. Subdiagram (2) commutes
by naturality of $\alpha$, whereas (1) commutes because it is $T(NA,-)$
applied to equation (16), which is the induction step. We conclude that
$(\alpha^{*}_{A})_{n}$ is indeed natural in $n$.

Next, we have to show that $\alpha^{*}_{A}$ is also natural in $A$. Hence let
$f:A_{1}\to A_{2}$ be a morphism in $\mathbf{A}$. Then we need to show that

$MS(H(f,-))\circ\alpha^{*}_{A_{1}}=\alpha^{*}_{A_{2}}\circ S(T(Nf,-)).$

This equality holds if and only it holds for all its components $n$, i.e., if

$MH(f,-)^{n}\varnothing\circ(\alpha^{*}_{A_{1}})_{n}=(\alpha^{*}_{A_{2}})_{n}\circ
T(Nf,-)^{n}0$ (17)

holds for each $n\in\omega$. For $n=0$, it reduces to $\text{id}\circ
z=z\circ\text{id}$, which indeed holds. We proceed by induction. Assume that
(17) holds for $n$. Consider the following diagram:

$\mathbf{C}$$\mathbf{L}$$F$

$\vdash$

$G$$T(A_{1},T^{\dagger}A_{1})$$T(A_{2},T^{\dagger}A_{2})$$T(f,T^{\dagger}f)$$T^{\dagger}A_{1}$$T^{\dagger}A_{2}$$\phi^{T}_{A_{1}}$$\phi^{T}_{A_{2}}$$T^{\dagger}f$$T(A_{1},T^{\dagger}A_{1})$$T(A_{1},T^{\dagger}A_{2})$$T(A_{1},T^{\dagger}f)$$T^{\dagger}A_{1}$$T^{\dagger}A_{2}$$\phi^{T}_{A_{1}}$$T(A_{2},T^{\dagger}A_{2})$$T(f,T^{\dagger}A_{2})$$\phi^{T}_{A_{2}}$$T^{\dagger}f$$S(T(A,-))$$T(A,-)\circ
S(T(A,-))$$T(B,-)\circ
S(T(B,-))$$S(T(B,-))$$S(T(f,-))$$T(f,-)*S(T(f,-))$$s^{T(A,-)}$$s^{T(B,-)}$$T(\mathrm{colim}(\tau))$$T(\mathrm{colim}(D))$$\mathrm{colim}(T\circ
D)$$\mathrm{colim}(T\tau)$$T(\mathrm{colim}(D^{\prime}))$$\mathrm{colim}(T\circ
D^{\prime})$$\tau_{\mathrm{colim}(D)}$$T(\mathrm{colim}(D))$$\mathrm{colim}(T\circ
D)$$\mathrm{colim}(\tau D)$$H(\mathrm{colim}(D))$$\mathrm{colim}(H\circ
D)$$T^{\dagger}A$$\mathrm{colim}(S(T_{A}))$$\mathrm{colim}(T_{A}\circ
S(T_{A}))$$T_{A}\mathrm{colim}(S(T_{A}))$$T(A,T^{\dagger}A)$$T^{\dagger}B$$\mathrm{colim}(S(T_{B}))$$\mathrm{colim}(T_{B}\circ
S(T_{B}))$$T_{B}\mathrm{colim}(S(T_{B}))$$T(B,T^{\dagger}B)$$\mathrm{colim}(s^{T_{A}})$$T(f,T^{\dagger}f)$$\mathrm{colim}(T_{f}*S(T_{f}))$$\mathrm{colim}(S(T_{f}))$$T^{\dagger}f$$\mathrm{colim}(s^{T_{B}})$$T_{f}\mathrm{colim}(S(T_{f}))$(1)(4)(3)(2)$T_{A}{\mathrm{colim}(S(T_{f}))}$$T_{A}(\mathrm{colim}(S(T_{A})))$$\mathrm{colim}(T_{A}\circ
S(T_{A})$$\mathrm{colim}(T_{A}S(T_{f}))$$T_{A}(\mathrm{colim}(S(T_{B})))$$\mathrm{colim}(T_{A}S(T_{B}))$$\mathrm{colim}(T_{f}S(T_{B}))$$T_{f}\mathrm{colim}(S(T_{B}))$$T_{B}(\mathrm{colim}(S(T_{B})))$$\mathrm{colim}(T_{B}\circ
S(T_{B}))$$\mathbf{C}\times\mathbf{D}$$\mathbf{A}\times\mathbf{B}$$\mathbf{D}$$\mathbf{B}$$T$$M$$N\times
M$$H$$\alpha$$T^{\dagger}NA$$\mathrm{colim}(T^{*}NA)$$\mathrm{colim}(MH^{*}A)$$M\mathrm{colim}(H^{*}A)$$MH^{\dagger}A$$T^{\dagger}NB$$\mathrm{colim}(T^{*}NB)$$\mathrm{colim}(MH^{*}B)$$M\mathrm{colim}(H^{*}B)$$MH^{\dagger}B$$\mathrm{colim}(\alpha_{A}^{*})$$MH^{\dagger}f$$\mathrm{colim}(MH^{*}f)$$\mathrm{colim}(T^{*}Nf)$$T^{\dagger}Nf$$\mathrm{colim}(\alpha_{B}^{*})$$M\mathrm{colim}(H^{*}f)$(1)(4)(3)(2)$S(T)$$MS(H)$$MHS(H)$$TS(T)$$TMS(H)$$s^{T}$$\alpha^{*}$$Ms^{H}$$T\alpha^{*}$$\alpha*S(H)$$M\circ
H\circ\langle\text{Id},H^{\dagger}\rangle$$T\circ\langle N,T^{\dagger}\circ
N\rangle$$T\circ\langle N,M\circ
H^{\dagger}\rangle$$T\circ\langle\text{Id},T^{\dagger}\rangle\circ
N$$T\circ(N\times M)\circ\langle\text{Id},H^{\dagger}\rangle$$M\circ
H^{\dagger}$$T^{\dagger}\circ
N$$\alpha\langle\text{Id},H^{\dagger}\rangle$$M\phi^{H}$$\phi^{T}N$$T\langle
N,\alpha^{\dagger}\rangle$$\alpha^{\dagger}$$MH^{\prime}Y(H^{\prime})$$T^{\prime}Y(T^{\prime})$$T^{\prime}\alpha^{\dagger}_{A}$$T^{\prime}MY(H^{\prime})$$\alpha_{A,Y(H^{\prime})}$$MY(H^{\prime})$$Y(T^{\prime})$$y^{T^{\prime}}$$My^{H^{\prime}}$$\alpha^{\dagger}_{A}$$\mathbf{C}$$\mathbf{D}$$T\circ\langle\text{Id},T^{\dagger}\rangle$$T^{\dagger}$$\phi^{T}$$\mathbf{A}$$\mathbf{B}$$H\circ\langle\text{Id},H^{\dagger}\rangle$$H^{\dagger}$$\phi^{H}$$M$$N$$\mathbf{C}$$\mathbf{L}$$F$

$\vdash$

$G$$\mathbf{C}$$\mathbf{L}$$F$

$\vdash$

$G$$\mathbf{CPO}$$\mathbf{CPO}_{\perp!}$$(-)_{\perp}$

$\vdash$

$U$$\mathbf{CPO}_{\perp!}$$\widehat{}\mathbf{M}$$-\circledcirc I$

$\vdash$

$\widehat{}\mathbf{M}(I,-)$$\mathbf{CPO}$$\mathbf{CPO}_{\perp!}$$(-)_{\perp}$

$\vdash$

$U$$\widehat{}\mathbf{M}$$-\circledcirc I$

$\vdash$

$\widehat{}\mathbf{M}(I,-)$${\llbracket\Theta\vdash
P\rrbracket}$$F_{pe}^{\times|\Theta|}$$\mathbf{C}_{pe}$$\mathbf{L}_{e}$$\mathbf{C}_{pe}^{|\Theta|}$${\llparenthesis\Theta\vdash
P\rrparenthesis}$$F_{pe}$$\mathbf{L}_{e}^{|\Theta|}$$\alpha$${\llbracket\Theta\vdash
P[R/X]\rrbracket}\circ
F_{pe}^{\times|\Theta|}$$F_{pe}\circ{\llparenthesis\Theta\vdash
P[R/X]\rrparenthesis}$$F_{pe}\circ{\llparenthesis\Theta,X\vdash
P\rrparenthesis}\circ\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle$${\llbracket\Theta,X\vdash P\rrbracket}\circ\langle
F_{pe}^{\times|\Theta|},{\llbracket\Theta\vdash R\rrbracket}\circ
F_{pe}^{\times|\Theta|}\rangle$${\llbracket\Theta,X\vdash
P\rrbracket}\circ\langle
F_{pe}^{\times|\Theta|},F_{pe}\circ{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle$${\llbracket\Theta,X\vdash
P\rrbracket}\circ\langle\text{Id},{\llbracket\Theta\vdash
R\rrbracket}\rangle\circ F_{pe}^{\times|\Theta|}$${\llbracket\Theta,X\vdash
P\rrbracket}\circ
F_{pe}^{\times(|\Theta|+1)}\circ\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle$$\alpha\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle$${\llbracket\Theta,X\vdash P\rrbracket}\langle
F_{pe}^{\times|\Theta|},\alpha\rangle$$\alpha$$F_{pe}\gamma^{-1}$${\llbracket\Theta\vdash
P[\mu X.P/X]\rrbracket}\circ
F_{pe}^{\times|\Theta|}$$F_{pe}\circ{\llparenthesis\Theta\vdash P[\mu
X.P/X]\rrparenthesis}$$\alpha$${\llbracket\Theta\vdash\mu X.P\rrbracket}\circ
F_{pe}^{\times|\Theta|}$$F_{pe}\circ{\llparenthesis\Theta\vdash\mu
X.P\rrparenthesis}$$\alpha$$\mathrm{fold}F_{pe}^{\times|\Theta|}$$F_{pe}\mathpzc{fold}$$\mathbf{R}(A)_{e}\times\mathbf{R}(B)_{e}$$\mathbf{R}(A\star
B)_{e}$$\star_{e}^{A,B}$$\mathbf{L}_{e}\times\mathbf{L}_{e}$$\mathbf{L}_{e}$$\star_{e}$$U^{A\star
B}_{e}$$U^{A}_{e}\times
U^{B}_{e}$$!_{e}$$\mathbf{R}(!A)_{e}$$U^{A}_{e}$$\mathbf{L}_{e}$$\mathbf{R}(A)_{e}$$!_{e}^{A}$$U^{!A}_{e}$$\mathbf{L}_{e}$$\mathbf{R}(C_{1})_{e}\times\cdots\times\mathbf{R}(C_{n})_{e}$$\mathbf{R}(A[\vec{C}/\Theta])_{e}$${{\lVert\Theta\vdash
A\rVert^{\vec{C}}}}$$\mathbf{L}_{e}\times\cdots\times\mathbf{L}_{e}$$\mathbf{L}_{e}$${\llbracket\Theta\vdash
A\rrbracket}$$U^{A[\vec{C}/\Theta]}_{e}$$U^{C_{1}}_{e}\times\cdots\times
U^{C_{n}}_{e}$$\mathbf{R}(C_{1})_{e}\times\cdots\times\mathbf{R}(C_{n})_{e}$$\mathbf{R}(A[\vec{C}/\Theta])_{e}$$\phi$$\mathbf{L}_{e}\times\cdots\times\mathbf{L}_{e}$$\mathbf{L}_{e}$${\llbracket\Theta,X\vdash
A\rrbracket}\circ\langle\text{Id},{\llbracket\Theta\vdash\mu
X.A\rrbracket}\rangle$$\phi$${{\lVert\Theta\vdash\mu
X.A\rVert^{\vec{C}}}}$${\llbracket\Theta\vdash\mu
X.A\rrbracket}$$U^{A[\vec{C}/\Theta]}_{e}$$U^{C_{1}}_{e}\times\cdots\times
U^{C_{n}}_{e}$$\mathbb{I}^{\mu
X.A[\vec{C}/\Theta]}_{e}\circ{\lVert\Theta,X\vdash A\rVert^{\vec{C},\mu
X.A[\vec{C}/\Theta]}}\circ\langle\text{Id},{{\lVert\Theta\vdash\mu
X.A\rVert^{\vec{C}}}}\rangle$$MH(A,-)^{n+2}\varnothing$$MH(A,-)^{n+1}\varnothing$$T(NA,MH(A,-)^{n+1}\varnothing)$$\alpha_{A,H(A,-)^{n}\varnothing}$$T(NA,MH(A,-)^{n}\iota_{2})$$\alpha_{A,H(A,-)^{n+1}\varnothing}$$T(NA,(\alpha^{*}_{A})_{n})$$T(NA,(\alpha^{*}_{A})_{n+1})$$T(NA,-)^{n+1}0$$T(NA,-)^{n+2}0$$MH(A,-)^{n+1}\iota_{2}$$T(NA,-)^{n+1}\iota_{1}$$(2)$$(1)$$T(NA,MH(A,-)^{n}\varnothing)$$MH(A_{2},-)^{n+1}\varnothing$$MH(A_{1},-)^{n+1}\varnothing$$T(NA_{2},MH(A_{2},-)^{n}\varnothing)$$\alpha_{A_{1},H(A_{1},-)^{n}\varnothing}$$\alpha_{A_{2},H(A_{2},-)^{n}\varnothing}$$T(NA_{1},MH(f,-)^{n}\varnothing)$$T(NA_{2},(\alpha^{*}_{A_{2}})_{n})$$T(NA_{1},-)^{n+1}0$$T(NA_{1},MH(A_{1},-)^{n}\varnothing)$$T(NA_{1},T(NA_{2},-)^{n}0)$$MH(f,-)^{n+1}\varnothing$$T(NA_{1},MH(A_{2},-)^{n}\varnothing)$$(2)$$(1)$$T(NA_{2},-)^{n+1}0$$T(NA_{1},T(Nf,-)^{n}0)$$T(Nf,MH(A_{2},-)^{n}\varnothing)$$T(NA_{1},(\alpha^{*}_{A_{1}})_{n})$$(3)$$T(Nf,T(NA_{2},-)^{n}0)$$T(NA_{1},(\alpha^{*}_{A_{2}})_{n})$

Here the outer square is just (17) for $n+1$. Subdiagram (1) commutes because
it is $TN(A_{1},-)$ acting on equation (17) for $n$, the induction step.
Subdiagram (2) because $T$ is a bifunctor. Subdiagram (3) commutes by
naturality of $\alpha$. We conclude that (17) also holds for $n+1$ and
therefore $\alpha^{*}$ is a natural transformation.

Finally, a simple induction argument shows that every component
$\alpha^{*}_{A}$ is an isomorphism and therefore $\alpha^{*}$ is a natural
isomorphism.

###  A.5. Proof of Lemma 25

######  Proof A.5.

For (1), notice $\beta$ can be seen as a natural transformation
$\beta:H\circ(\text{Id}\times\text{Id})\Rightarrow\text{Id}\circ H^{\prime}$,
hence $\beta^{*}$ becomes a natural transformation
$\beta^{*}:H^{*}\circ\text{Id}\Rightarrow(\text{Id}\triangleright-)\circ(H^{\prime})^{*}$,
defined by

$\displaystyle(\beta^{*}_{A})_{0}$
$\displaystyle\coloneqq\left(\varnothing\xrightarrow{\text{id}_{\varnothing}}\varnothing\right)$
$\displaystyle(\beta^{*}_{A})_{n+1}$
$\displaystyle\coloneqq\left(H(A,-)^{n+1}\varnothing\xrightarrow{H(A,(\beta_{A}^{*})_{n})}H(A,H^{\prime}(A,-)^{n}\varnothing)\xrightarrow{\beta_{A,H^{\prime}(A,-)^{n}\varnothing}}H^{\prime}(A,-)^{n+1}\varnothing\right).$

Furthermore, we have a natural transformation
$M\beta\circ\alpha:T\circ(N\times M)\Rightarrow M\circ H^{\prime}$, hence
$(M\beta\circ\alpha)^{*}:T^{*}\circ
N\Rightarrow(M\triangleright-)\circ(H^{\prime})^{*}$ is a natural
transformation defined by

$\displaystyle((M\beta\circ\alpha)^{*}_{A})_{0}\coloneqq\left(0\xrightarrow{z}M\varnothing\right)$
$\displaystyle((M\beta\circ\alpha)^{*}_{A})_{n+1}\coloneqq$
$\displaystyle\qquad\left(T(NA,-)^{n+1}0\xrightarrow{T(NA,(\delta_{A}^{*})_{n})}T(NA,MH^{\prime}(A,-)^{n}\varnothing)\xrightarrow{\delta_{A,H^{\prime}(A,-)^{n}\varnothing}}MH^{\prime}(A,-)^{n+1}\varnothing\right).$

where $\delta=M\beta\circ\alpha$. We have to show that we have
$(M\beta\circ\alpha)_{A}^{*}=M\beta_{A}^{*}\circ\alpha_{A}^{*}$. Base case:

$((M\beta\circ\alpha)^{*}_{A})_{0}=z=M(\text{id}_{\varnothing})\circ
z=M(\beta_{A}^{*})_{0}\circ(\alpha_{A}^{*})_{0}.$

Assume as an induction hypothesis that
$((M\beta\circ\alpha)^{*}_{A})_{n}=(M\beta^{*}_{A}\circ\alpha^{*}_{A})_{n},$
and consider the following diagram.

$\mathbf{C}$$\mathbf{L}$$F$

$\vdash$

$G$$T(A_{1},T^{\dagger}A_{1})$$T(A_{2},T^{\dagger}A_{2})$$T(f,T^{\dagger}f)$$T^{\dagger}A_{1}$$T^{\dagger}A_{2}$$\phi^{T}_{A_{1}}$$\phi^{T}_{A_{2}}$$T^{\dagger}f$$T(A_{1},T^{\dagger}A_{1})$$T(A_{1},T^{\dagger}A_{2})$$T(A_{1},T^{\dagger}f)$$T^{\dagger}A_{1}$$T^{\dagger}A_{2}$$\phi^{T}_{A_{1}}$$T(A_{2},T^{\dagger}A_{2})$$T(f,T^{\dagger}A_{2})$$\phi^{T}_{A_{2}}$$T^{\dagger}f$$S(T(A,-))$$T(A,-)\circ
S(T(A,-))$$T(B,-)\circ
S(T(B,-))$$S(T(B,-))$$S(T(f,-))$$T(f,-)*S(T(f,-))$$s^{T(A,-)}$$s^{T(B,-)}$$T(\mathrm{colim}(\tau))$$T(\mathrm{colim}(D))$$\mathrm{colim}(T\circ
D)$$\mathrm{colim}(T\tau)$$T(\mathrm{colim}(D^{\prime}))$$\mathrm{colim}(T\circ
D^{\prime})$$\tau_{\mathrm{colim}(D)}$$T(\mathrm{colim}(D))$$\mathrm{colim}(T\circ
D)$$\mathrm{colim}(\tau D)$$H(\mathrm{colim}(D))$$\mathrm{colim}(H\circ
D)$$T^{\dagger}A$$\mathrm{colim}(S(T_{A}))$$\mathrm{colim}(T_{A}\circ
S(T_{A}))$$T_{A}\mathrm{colim}(S(T_{A}))$$T(A,T^{\dagger}A)$$T^{\dagger}B$$\mathrm{colim}(S(T_{B}))$$\mathrm{colim}(T_{B}\circ
S(T_{B}))$$T_{B}\mathrm{colim}(S(T_{B}))$$T(B,T^{\dagger}B)$$\mathrm{colim}(s^{T_{A}})$$T(f,T^{\dagger}f)$$\mathrm{colim}(T_{f}*S(T_{f}))$$\mathrm{colim}(S(T_{f}))$$T^{\dagger}f$$\mathrm{colim}(s^{T_{B}})$$T_{f}\mathrm{colim}(S(T_{f}))$(1)(4)(3)(2)$T_{A}{\mathrm{colim}(S(T_{f}))}$$T_{A}(\mathrm{colim}(S(T_{A})))$$\mathrm{colim}(T_{A}\circ
S(T_{A})$$\mathrm{colim}(T_{A}S(T_{f}))$$T_{A}(\mathrm{colim}(S(T_{B})))$$\mathrm{colim}(T_{A}S(T_{B}))$$\mathrm{colim}(T_{f}S(T_{B}))$$T_{f}\mathrm{colim}(S(T_{B}))$$T_{B}(\mathrm{colim}(S(T_{B})))$$\mathrm{colim}(T_{B}\circ
S(T_{B}))$$\mathbf{C}\times\mathbf{D}$$\mathbf{A}\times\mathbf{B}$$\mathbf{D}$$\mathbf{B}$$T$$M$$N\times
M$$H$$\alpha$$T^{\dagger}NA$$\mathrm{colim}(T^{*}NA)$$\mathrm{colim}(MH^{*}A)$$M\mathrm{colim}(H^{*}A)$$MH^{\dagger}A$$T^{\dagger}NB$$\mathrm{colim}(T^{*}NB)$$\mathrm{colim}(MH^{*}B)$$M\mathrm{colim}(H^{*}B)$$MH^{\dagger}B$$\mathrm{colim}(\alpha_{A}^{*})$$MH^{\dagger}f$$\mathrm{colim}(MH^{*}f)$$\mathrm{colim}(T^{*}Nf)$$T^{\dagger}Nf$$\mathrm{colim}(\alpha_{B}^{*})$$M\mathrm{colim}(H^{*}f)$(1)(4)(3)(2)$S(T)$$MS(H)$$MHS(H)$$TS(T)$$TMS(H)$$s^{T}$$\alpha^{*}$$Ms^{H}$$T\alpha^{*}$$\alpha*S(H)$$M\circ
H\circ\langle\text{Id},H^{\dagger}\rangle$$T\circ\langle N,T^{\dagger}\circ
N\rangle$$T\circ\langle N,M\circ
H^{\dagger}\rangle$$T\circ\langle\text{Id},T^{\dagger}\rangle\circ
N$$T\circ(N\times M)\circ\langle\text{Id},H^{\dagger}\rangle$$M\circ
H^{\dagger}$$T^{\dagger}\circ
N$$\alpha\langle\text{Id},H^{\dagger}\rangle$$M\phi^{H}$$\phi^{T}N$$T\langle
N,\alpha^{\dagger}\rangle$$\alpha^{\dagger}$$MH^{\prime}Y(H^{\prime})$$T^{\prime}Y(T^{\prime})$$T^{\prime}\alpha^{\dagger}_{A}$$T^{\prime}MY(H^{\prime})$$\alpha_{A,Y(H^{\prime})}$$MY(H^{\prime})$$Y(T^{\prime})$$y^{T^{\prime}}$$My^{H^{\prime}}$$\alpha^{\dagger}_{A}$$\mathbf{C}$$\mathbf{D}$$T\circ\langle\text{Id},T^{\dagger}\rangle$$T^{\dagger}$$\phi^{T}$$\mathbf{A}$$\mathbf{B}$$H\circ\langle\text{Id},H^{\dagger}\rangle$$H^{\dagger}$$\phi^{H}$$M$$N$$\mathbf{C}$$\mathbf{L}$$F$

$\vdash$

$G$$\mathbf{C}$$\mathbf{L}$$F$

$\vdash$

$G$$\mathbf{CPO}$$\mathbf{CPO}_{\perp!}$$(-)_{\perp}$

$\vdash$

$U$$\mathbf{CPO}_{\perp!}$$\widehat{}\mathbf{M}$$-\circledcirc I$

$\vdash$

$\widehat{}\mathbf{M}(I,-)$$\mathbf{CPO}$$\mathbf{CPO}_{\perp!}$$(-)_{\perp}$

$\vdash$

$U$$\widehat{}\mathbf{M}$$-\circledcirc I$

$\vdash$

$\widehat{}\mathbf{M}(I,-)$${\llbracket\Theta\vdash
P\rrbracket}$$F_{pe}^{\times|\Theta|}$$\mathbf{C}_{pe}$$\mathbf{L}_{e}$$\mathbf{C}_{pe}^{|\Theta|}$${\llparenthesis\Theta\vdash
P\rrparenthesis}$$F_{pe}$$\mathbf{L}_{e}^{|\Theta|}$$\alpha$${\llbracket\Theta\vdash
P[R/X]\rrbracket}\circ
F_{pe}^{\times|\Theta|}$$F_{pe}\circ{\llparenthesis\Theta\vdash
P[R/X]\rrparenthesis}$$F_{pe}\circ{\llparenthesis\Theta,X\vdash
P\rrparenthesis}\circ\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle$${\llbracket\Theta,X\vdash P\rrbracket}\circ\langle
F_{pe}^{\times|\Theta|},{\llbracket\Theta\vdash R\rrbracket}\circ
F_{pe}^{\times|\Theta|}\rangle$${\llbracket\Theta,X\vdash
P\rrbracket}\circ\langle
F_{pe}^{\times|\Theta|},F_{pe}\circ{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle$${\llbracket\Theta,X\vdash
P\rrbracket}\circ\langle\text{Id},{\llbracket\Theta\vdash
R\rrbracket}\rangle\circ F_{pe}^{\times|\Theta|}$${\llbracket\Theta,X\vdash
P\rrbracket}\circ
F_{pe}^{\times(|\Theta|+1)}\circ\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle$$\alpha\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle$${\llbracket\Theta,X\vdash P\rrbracket}\langle
F_{pe}^{\times|\Theta|},\alpha\rangle$$\alpha$$F_{pe}\gamma^{-1}$${\llbracket\Theta\vdash
P[\mu X.P/X]\rrbracket}\circ
F_{pe}^{\times|\Theta|}$$F_{pe}\circ{\llparenthesis\Theta\vdash P[\mu
X.P/X]\rrparenthesis}$$\alpha$${\llbracket\Theta\vdash\mu X.P\rrbracket}\circ
F_{pe}^{\times|\Theta|}$$F_{pe}\circ{\llparenthesis\Theta\vdash\mu
X.P\rrparenthesis}$$\alpha$$\mathrm{fold}F_{pe}^{\times|\Theta|}$$F_{pe}\mathpzc{fold}$$\mathbf{R}(A)_{e}\times\mathbf{R}(B)_{e}$$\mathbf{R}(A\star
B)_{e}$$\star_{e}^{A,B}$$\mathbf{L}_{e}\times\mathbf{L}_{e}$$\mathbf{L}_{e}$$\star_{e}$$U^{A\star
B}_{e}$$U^{A}_{e}\times
U^{B}_{e}$$!_{e}$$\mathbf{R}(!A)_{e}$$U^{A}_{e}$$\mathbf{L}_{e}$$\mathbf{R}(A)_{e}$$!_{e}^{A}$$U^{!A}_{e}$$\mathbf{L}_{e}$$\mathbf{R}(C_{1})_{e}\times\cdots\times\mathbf{R}(C_{n})_{e}$$\mathbf{R}(A[\vec{C}/\Theta])_{e}$${{\lVert\Theta\vdash
A\rVert^{\vec{C}}}}$$\mathbf{L}_{e}\times\cdots\times\mathbf{L}_{e}$$\mathbf{L}_{e}$${\llbracket\Theta\vdash
A\rrbracket}$$U^{A[\vec{C}/\Theta]}_{e}$$U^{C_{1}}_{e}\times\cdots\times
U^{C_{n}}_{e}$$\mathbf{R}(C_{1})_{e}\times\cdots\times\mathbf{R}(C_{n})_{e}$$\mathbf{R}(A[\vec{C}/\Theta])_{e}$$\phi$$\mathbf{L}_{e}\times\cdots\times\mathbf{L}_{e}$$\mathbf{L}_{e}$${\llbracket\Theta,X\vdash
A\rrbracket}\circ\langle\text{Id},{\llbracket\Theta\vdash\mu
X.A\rrbracket}\rangle$$\phi$${{\lVert\Theta\vdash\mu
X.A\rVert^{\vec{C}}}}$${\llbracket\Theta\vdash\mu
X.A\rrbracket}$$U^{A[\vec{C}/\Theta]}_{e}$$U^{C_{1}}_{e}\times\cdots\times
U^{C_{n}}_{e}$$\mathbb{I}^{\mu
X.A[\vec{C}/\Theta]}_{e}\circ{\lVert\Theta,X\vdash A\rVert^{\vec{C},\mu
X.A[\vec{C}/\Theta]}}\circ\langle\text{Id},{{\lVert\Theta\vdash\mu
X.A\rVert^{\vec{C}}}}\rangle$$MH(A,-)^{n+2}\varnothing$$MH(A,-)^{n+1}\varnothing$$T(NA,MH(A,-)^{n+1}\varnothing)$$\alpha_{A,H(A,-)^{n}\varnothing}$$T(NA,MH(A,-)^{n}\iota_{2})$$\alpha_{A,H(A,-)^{n+1}\varnothing}$$T(NA,(\alpha^{*}_{A})_{n})$$T(NA,(\alpha^{*}_{A})_{n+1})$$T(NA,-)^{n+1}0$$T(NA,-)^{n+2}0$$MH(A,-)^{n+1}\iota_{2}$$T(NA,-)^{n+1}\iota_{1}$$(2)$$(1)$$T(NA,MH(A,-)^{n}\varnothing)$$MH(A_{2},-)^{n+1}\varnothing$$MH(A_{1},-)^{n+1}\varnothing$$T(NA_{2},MH(A_{2},-)^{n}\varnothing)$$\alpha_{A_{1},H(A_{1},-)^{n}\varnothing}$$\alpha_{A_{2},H(A_{2},-)^{n}\varnothing}$$T(NA_{1},MH(f,-)^{n}\varnothing)$$T(NA_{2},(\alpha^{*}_{A_{2}})_{n})$$T(NA_{1},-)^{n+1}0$$T(NA_{1},MH(A_{1},-)^{n}\varnothing)$$T(NA_{1},T(NA_{2},-)^{n}0)$$MH(f,-)^{n+1}\varnothing$$T(NA_{1},MH(A_{2},-)^{n}\varnothing)$$(2)$$(1)$$T(NA_{2},-)^{n+1}0$$T(NA_{1},T(Nf,-)^{n}0)$$T(Nf,MH(A_{2},-)^{n}\varnothing)$$T(NA_{1},(\alpha^{*}_{A_{1}})_{n})$$(3)$$T(Nf,T(NA_{2},-)^{n}0)$$T(NA_{1},(\alpha^{*}_{A_{2}})_{n})$$T(NA,MH^{\prime}(A,-)^{n}\varnothing)$$T(NA,MH(A,-)^{n}\varnothing)$$T(NA,-)^{n+1}0$$MH(A,-)^{n+1}\varnothing$$T(NA,(\alpha_{A}^{*})_{n})$$T(NA,-)^{n+1}0$$T(NA,((M\beta\circ\alpha)_{A}^{*})_{n})$$MH(A,H^{\prime}(A,-)^{n}\varnothing)$$MH^{\prime}(A,-)^{n+1}\varnothing$$T(NA,M(\beta_{A}^{*})_{n})$$M\beta_{A,H^{\prime}(A,-)^{n}\varnothing}$$M(\beta_{A}^{*})_{n+1}$(1)$MH(A,(\beta_{A}^{*})_{n})$$\alpha_{A,H(A,-)^{n}\varnothing}$$\alpha_{A,H^{\prime}(A,-)^{n}\varnothing}$$(\alpha_{A}^{*})_{n+1}$(2)(3)(4)

Here (1) commutes, because it is $T(NA,-)$ applied to the induction
hypothesis, (2) commutes by definition of $\alpha_{A}^{*}$, (3) commutes by
naturality of $\alpha$, and (4) commutes by definition of $\beta_{A}^{*}$. The
outer right column of the diagram equals by definition
$((M\beta\circ\alpha)_{A}^{*})_{n+1}$. It follows that

$((M\beta\circ\alpha)^{*}_{A})_{n+1}=(M\beta^{*}_{A}\circ\alpha^{*}_{A})_{n+1},$

which concludes the proof of the first statement.

For the second statement, base case:

$\displaystyle((\alpha(Q\times\text{Id})\circ T(\gamma\times M))^{*}_{E})_{0}$
$\displaystyle=z$ $\displaystyle(\text{Definition of }(-)^{*})$
$\displaystyle=z\circ\text{id}_{0}$
$\displaystyle=(\alpha^{*}_{QE})_{0}\circ(T^{*}\gamma_{E})_{0}$
$\displaystyle(\text{Definition of }(-)^{*}\text{ and }T^{*})$

For the induction step, assume that $((\alpha(Q\times\text{Id})\circ
T(\gamma\times
M))^{*}_{E})_{n}=(\alpha^{*}_{QE})_{n}\circ(T^{*}\gamma_{E})_{n}.$ Using the
induction hypothesis, then $((\alpha(Q\times\text{Id})\circ T(\gamma\times
M))^{*}_{E})_{n+1}$ is given by the composition of the right and top sides of
the diagram:

$\mathbf{C}$$\mathbf{L}$$F$

$\vdash$

$G$$T(A_{1},T^{\dagger}A_{1})$$T(A_{2},T^{\dagger}A_{2})$$T(f,T^{\dagger}f)$$T^{\dagger}A_{1}$$T^{\dagger}A_{2}$$\phi^{T}_{A_{1}}$$\phi^{T}_{A_{2}}$$T^{\dagger}f$$T(A_{1},T^{\dagger}A_{1})$$T(A_{1},T^{\dagger}A_{2})$$T(A_{1},T^{\dagger}f)$$T^{\dagger}A_{1}$$T^{\dagger}A_{2}$$\phi^{T}_{A_{1}}$$T(A_{2},T^{\dagger}A_{2})$$T(f,T^{\dagger}A_{2})$$\phi^{T}_{A_{2}}$$T^{\dagger}f$$S(T(A,-))$$T(A,-)\circ
S(T(A,-))$$T(B,-)\circ
S(T(B,-))$$S(T(B,-))$$S(T(f,-))$$T(f,-)*S(T(f,-))$$s^{T(A,-)}$$s^{T(B,-)}$$T(\mathrm{colim}(\tau))$$T(\mathrm{colim}(D))$$\mathrm{colim}(T\circ
D)$$\mathrm{colim}(T\tau)$$T(\mathrm{colim}(D^{\prime}))$$\mathrm{colim}(T\circ
D^{\prime})$$\tau_{\mathrm{colim}(D)}$$T(\mathrm{colim}(D))$$\mathrm{colim}(T\circ
D)$$\mathrm{colim}(\tau D)$$H(\mathrm{colim}(D))$$\mathrm{colim}(H\circ
D)$$T^{\dagger}A$$\mathrm{colim}(S(T_{A}))$$\mathrm{colim}(T_{A}\circ
S(T_{A}))$$T_{A}\mathrm{colim}(S(T_{A}))$$T(A,T^{\dagger}A)$$T^{\dagger}B$$\mathrm{colim}(S(T_{B}))$$\mathrm{colim}(T_{B}\circ
S(T_{B}))$$T_{B}\mathrm{colim}(S(T_{B}))$$T(B,T^{\dagger}B)$$\mathrm{colim}(s^{T_{A}})$$T(f,T^{\dagger}f)$$\mathrm{colim}(T_{f}*S(T_{f}))$$\mathrm{colim}(S(T_{f}))$$T^{\dagger}f$$\mathrm{colim}(s^{T_{B}})$$T_{f}\mathrm{colim}(S(T_{f}))$(1)(4)(3)(2)$T_{A}{\mathrm{colim}(S(T_{f}))}$$T_{A}(\mathrm{colim}(S(T_{A})))$$\mathrm{colim}(T_{A}\circ
S(T_{A})$$\mathrm{colim}(T_{A}S(T_{f}))$$T_{A}(\mathrm{colim}(S(T_{B})))$$\mathrm{colim}(T_{A}S(T_{B}))$$\mathrm{colim}(T_{f}S(T_{B}))$$T_{f}\mathrm{colim}(S(T_{B}))$$T_{B}(\mathrm{colim}(S(T_{B})))$$\mathrm{colim}(T_{B}\circ
S(T_{B}))$$\mathbf{C}\times\mathbf{D}$$\mathbf{A}\times\mathbf{B}$$\mathbf{D}$$\mathbf{B}$$T$$M$$N\times
M$$H$$\alpha$$T^{\dagger}NA$$\mathrm{colim}(T^{*}NA)$$\mathrm{colim}(MH^{*}A)$$M\mathrm{colim}(H^{*}A)$$MH^{\dagger}A$$T^{\dagger}NB$$\mathrm{colim}(T^{*}NB)$$\mathrm{colim}(MH^{*}B)$$M\mathrm{colim}(H^{*}B)$$MH^{\dagger}B$$\mathrm{colim}(\alpha_{A}^{*})$$MH^{\dagger}f$$\mathrm{colim}(MH^{*}f)$$\mathrm{colim}(T^{*}Nf)$$T^{\dagger}Nf$$\mathrm{colim}(\alpha_{B}^{*})$$M\mathrm{colim}(H^{*}f)$(1)(4)(3)(2)$S(T)$$MS(H)$$MHS(H)$$TS(T)$$TMS(H)$$s^{T}$$\alpha^{*}$$Ms^{H}$$T\alpha^{*}$$\alpha*S(H)$$M\circ
H\circ\langle\text{Id},H^{\dagger}\rangle$$T\circ\langle N,T^{\dagger}\circ
N\rangle$$T\circ\langle N,M\circ
H^{\dagger}\rangle$$T\circ\langle\text{Id},T^{\dagger}\rangle\circ
N$$T\circ(N\times M)\circ\langle\text{Id},H^{\dagger}\rangle$$M\circ
H^{\dagger}$$T^{\dagger}\circ
N$$\alpha\langle\text{Id},H^{\dagger}\rangle$$M\phi^{H}$$\phi^{T}N$$T\langle
N,\alpha^{\dagger}\rangle$$\alpha^{\dagger}$$MH^{\prime}Y(H^{\prime})$$T^{\prime}Y(T^{\prime})$$T^{\prime}\alpha^{\dagger}_{A}$$T^{\prime}MY(H^{\prime})$$\alpha_{A,Y(H^{\prime})}$$MY(H^{\prime})$$Y(T^{\prime})$$y^{T^{\prime}}$$My^{H^{\prime}}$$\alpha^{\dagger}_{A}$$\mathbf{C}$$\mathbf{D}$$T\circ\langle\text{Id},T^{\dagger}\rangle$$T^{\dagger}$$\phi^{T}$$\mathbf{A}$$\mathbf{B}$$H\circ\langle\text{Id},H^{\dagger}\rangle$$H^{\dagger}$$\phi^{H}$$M$$N$$\mathbf{C}$$\mathbf{L}$$F$

$\vdash$

$G$$\mathbf{C}$$\mathbf{L}$$F$

$\vdash$

$G$$\mathbf{CPO}$$\mathbf{CPO}_{\perp!}$$(-)_{\perp}$

$\vdash$

$U$$\mathbf{CPO}_{\perp!}$$\widehat{}\mathbf{M}$$-\circledcirc I$

$\vdash$

$\widehat{}\mathbf{M}(I,-)$$\mathbf{CPO}$$\mathbf{CPO}_{\perp!}$$(-)_{\perp}$

$\vdash$

$U$$\widehat{}\mathbf{M}$$-\circledcirc I$

$\vdash$

$\widehat{}\mathbf{M}(I,-)$${\llbracket\Theta\vdash
P\rrbracket}$$F_{pe}^{\times|\Theta|}$$\mathbf{C}_{pe}$$\mathbf{L}_{e}$$\mathbf{C}_{pe}^{|\Theta|}$${\llparenthesis\Theta\vdash
P\rrparenthesis}$$F_{pe}$$\mathbf{L}_{e}^{|\Theta|}$$\alpha$${\llbracket\Theta\vdash
P[R/X]\rrbracket}\circ
F_{pe}^{\times|\Theta|}$$F_{pe}\circ{\llparenthesis\Theta\vdash
P[R/X]\rrparenthesis}$$F_{pe}\circ{\llparenthesis\Theta,X\vdash
P\rrparenthesis}\circ\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle$${\llbracket\Theta,X\vdash P\rrbracket}\circ\langle
F_{pe}^{\times|\Theta|},{\llbracket\Theta\vdash R\rrbracket}\circ
F_{pe}^{\times|\Theta|}\rangle$${\llbracket\Theta,X\vdash
P\rrbracket}\circ\langle
F_{pe}^{\times|\Theta|},F_{pe}\circ{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle$${\llbracket\Theta,X\vdash
P\rrbracket}\circ\langle\text{Id},{\llbracket\Theta\vdash
R\rrbracket}\rangle\circ F_{pe}^{\times|\Theta|}$${\llbracket\Theta,X\vdash
P\rrbracket}\circ
F_{pe}^{\times(|\Theta|+1)}\circ\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle$$\alpha\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle$${\llbracket\Theta,X\vdash P\rrbracket}\langle
F_{pe}^{\times|\Theta|},\alpha\rangle$$\alpha$$F_{pe}\gamma^{-1}$${\llbracket\Theta\vdash
P[\mu X.P/X]\rrbracket}\circ
F_{pe}^{\times|\Theta|}$$F_{pe}\circ{\llparenthesis\Theta\vdash P[\mu
X.P/X]\rrparenthesis}$$\alpha$${\llbracket\Theta\vdash\mu X.P\rrbracket}\circ
F_{pe}^{\times|\Theta|}$$F_{pe}\circ{\llparenthesis\Theta\vdash\mu
X.P\rrparenthesis}$$\alpha$$\mathrm{fold}F_{pe}^{\times|\Theta|}$$F_{pe}\mathpzc{fold}$$\mathbf{R}(A)_{e}\times\mathbf{R}(B)_{e}$$\mathbf{R}(A\star
B)_{e}$$\star_{e}^{A,B}$$\mathbf{L}_{e}\times\mathbf{L}_{e}$$\mathbf{L}_{e}$$\star_{e}$$U^{A\star
B}_{e}$$U^{A}_{e}\times
U^{B}_{e}$$!_{e}$$\mathbf{R}(!A)_{e}$$U^{A}_{e}$$\mathbf{L}_{e}$$\mathbf{R}(A)_{e}$$!_{e}^{A}$$U^{!A}_{e}$$\mathbf{L}_{e}$$\mathbf{R}(C_{1})_{e}\times\cdots\times\mathbf{R}(C_{n})_{e}$$\mathbf{R}(A[\vec{C}/\Theta])_{e}$${{\lVert\Theta\vdash
A\rVert^{\vec{C}}}}$$\mathbf{L}_{e}\times\cdots\times\mathbf{L}_{e}$$\mathbf{L}_{e}$${\llbracket\Theta\vdash
A\rrbracket}$$U^{A[\vec{C}/\Theta]}_{e}$$U^{C_{1}}_{e}\times\cdots\times
U^{C_{n}}_{e}$$\mathbf{R}(C_{1})_{e}\times\cdots\times\mathbf{R}(C_{n})_{e}$$\mathbf{R}(A[\vec{C}/\Theta])_{e}$$\phi$$\mathbf{L}_{e}\times\cdots\times\mathbf{L}_{e}$$\mathbf{L}_{e}$${\llbracket\Theta,X\vdash
A\rrbracket}\circ\langle\text{Id},{\llbracket\Theta\vdash\mu
X.A\rrbracket}\rangle$$\phi$${{\lVert\Theta\vdash\mu
X.A\rVert^{\vec{C}}}}$${\llbracket\Theta\vdash\mu
X.A\rrbracket}$$U^{A[\vec{C}/\Theta]}_{e}$$U^{C_{1}}_{e}\times\cdots\times
U^{C_{n}}_{e}$$\mathbb{I}^{\mu
X.A[\vec{C}/\Theta]}_{e}\circ{\lVert\Theta,X\vdash A\rVert^{\vec{C},\mu
X.A[\vec{C}/\Theta]}}\circ\langle\text{Id},{{\lVert\Theta\vdash\mu
X.A\rVert^{\vec{C}}}}\rangle$$MH(A,-)^{n+2}\varnothing$$MH(A,-)^{n+1}\varnothing$$T(NA,MH(A,-)^{n+1}\varnothing)$$\alpha_{A,H(A,-)^{n}\varnothing}$$T(NA,MH(A,-)^{n}\iota_{2})$$\alpha_{A,H(A,-)^{n+1}\varnothing}$$T(NA,(\alpha^{*}_{A})_{n})$$T(NA,(\alpha^{*}_{A})_{n+1})$$T(NA,-)^{n+1}0$$T(NA,-)^{n+2}0$$MH(A,-)^{n+1}\iota_{2}$$T(NA,-)^{n+1}\iota_{1}$$(2)$$(1)$$T(NA,MH(A,-)^{n}\varnothing)$$MH(A_{2},-)^{n+1}\varnothing$$MH(A_{1},-)^{n+1}\varnothing$$T(NA_{2},MH(A_{2},-)^{n}\varnothing)$$\alpha_{A_{1},H(A_{1},-)^{n}\varnothing}$$\alpha_{A_{2},H(A_{2},-)^{n}\varnothing}$$T(NA_{1},MH(f,-)^{n}\varnothing)$$T(NA_{2},(\alpha^{*}_{A_{2}})_{n})$$T(NA_{1},-)^{n+1}0$$T(NA_{1},MH(A_{1},-)^{n}\varnothing)$$T(NA_{1},T(NA_{2},-)^{n}0)$$MH(f,-)^{n+1}\varnothing$$T(NA_{1},MH(A_{2},-)^{n}\varnothing)$$(2)$$(1)$$T(NA_{2},-)^{n+1}0$$T(NA_{1},T(Nf,-)^{n}0)$$T(Nf,MH(A_{2},-)^{n}\varnothing)$$T(NA_{1},(\alpha^{*}_{A_{1}})_{n})$$(3)$$T(Nf,T(NA_{2},-)^{n}0)$$T(NA_{1},(\alpha^{*}_{A_{2}})_{n})$$T(NA,MH^{\prime}(A,-)^{n}\varnothing)$$T(NA,MH(A,-)^{n}\varnothing)$$T(NA,-)^{n+1}0$$MH(A,-)^{n+1}\varnothing$$T(NA,(\alpha_{A}^{*})_{n})$$T(NA,-)^{n+1}0$$T(NA,((M\beta\circ\alpha)_{A}^{*})_{n})$$MH(A,H^{\prime}(A,-)^{n}\varnothing)$$MH^{\prime}(A,-)^{n+1}\varnothing$$T(NA,M(\beta_{A}^{*})_{n})$$M\beta_{A,H^{\prime}(A,-)^{n}\varnothing}$$M(\beta_{A}^{*})_{n+1}$(1)$MH(A,(\beta_{A}^{*})_{n})$$\alpha_{A,H(A,-)^{n}\varnothing}$$\alpha_{A,H^{\prime}(A,-)^{n}\varnothing}$$(\alpha_{A}^{*})_{n+1}$(2)(3)(4)$T(PE,-)^{n+1}0$$T(PE,T(NQE,-)^{n}0)$$T(PE,(T^{*}\gamma_{E})_{n})$$T(PE,MH(QE,-)^{n}\varnothing)$$T(PE,(\alpha^{*}_{QE})_{n})$$T(NQE,MH(QE,-)^{n}\varnothing)$$T(\gamma_{E},MH(QE,-)^{n}\varnothing)$$T(NQE,T(NQE,-)^{n}0)$$T(\gamma_{E},T(NQE,-)^{n}0)$$T(NQE,(\alpha^{*}_{QE})_{n})$$MH(QE,-)^{n+1}\varnothing$$\alpha_{(QE,H(QE,-)^{n}\varnothing)}$$(\alpha^{*}_{QE})_{n+1}$$(T^{*}\gamma_{E})_{n+1}$$(1)$$(2)$$(3)$

Triangle (1) commutes by definition of $T^{*}$ and the Godement product:

$\displaystyle(T^{*}\gamma_{E})_{n+1}=T(\gamma_{E},-)^{*(n+1)}=T(\gamma_{E},-)*T(\gamma_{E},-)^{*n}=T(\gamma_{E},T(NQE,-)^{n}0)\circ
T(PE,(T^{*}\gamma_{E})_{n}).$

Square (2) commutes by bifunctoriality of $T$ and (3) commutes by definition
of $\alpha^{*}$.

###  A.6. Proof of Lemma 28

######  Proof A.6.

The two compositions are natural transformations of $\omega$-diagrams in
$\mathbf{D},$ so we prove this by induction on $n\in\omega$. We first note
that if $\mathbf{A}$ is taken to be trivial, then $T^{*}=S(T)$ and
$H^{*}=S(H)$. Recall that $S(T)(n)=T^{n}0$, and $S(H)(n)=H^{n}\varnothing$.
Let $\iota_{T0}:0\to T0$ and $\iota_{H\varnothing}:\varnothing\to
H\varnothing$ be the unique initial maps. Then we have
$(s^{T})_{n}=T^{n}(\iota_{T0})$ and $(s^{H})_{n}=H^{n}(\iota_{H\varnothing})$.
Then $\alpha^{*}:T^{*}\Rightarrow MH^{*}:\omega\to\mathbf{D}$ is a natural
transformation given by:

$\displaystyle\alpha^{*}_{0}$
$\displaystyle\coloneqq\left(0\xrightarrow{z}M\varnothing\right)$
$\displaystyle\alpha^{*}_{n+1}$
$\displaystyle\coloneqq\left(T^{n+1}0\xrightarrow{T\alpha_{n}^{*}}TMH^{n}\varnothing\xrightarrow{\alpha_{H^{n}\varnothing}}MH^{n+1}\varnothing\right).$

In order to check that the diagram of natural transformations commutes, we
first consider the $0$-component as a basis step. Then we have to show that

$(Ms^{H}\circ\alpha^{*})_{0}=(\alpha*S(H)\circ T\alpha^{*}\circ s^{T})_{0}.$

Since the object $S(T)(0)$ that is the source of both sides of the last
equality is the initial object $0$, it follows that the last equality indeed
holds. Next, as an induction hypothesis, we assume that the $n$-component of
the diagram commutes, hence

$(Ms^{H}\circ\alpha^{*})_{n}=(\alpha*S(H)\circ T\alpha^{*}\circ s^{T})_{n},$
(18)

and we aim to show that the $(n+1)$-component commutes as well. Note that

$\displaystyle(\alpha*S(H)\circ T\alpha^{*}\circ s^{T})_{n}$
$\displaystyle=(\alpha*S(H))_{n}\circ T\alpha^{*}_{n}\circ
s^{T}_{n}=\alpha_{S(H)(n)}\circ T\alpha^{*}_{n}\circ s^{T}_{n}$
$\displaystyle=\alpha_{H^{n}\varnothing}\circ T\alpha_{n}^{*}\circ
s^{T}_{n}=\alpha_{n+1}^{*}\circ s^{T}_{n},$

hence (18) becomes

$Ms^{H}_{n}\circ\alpha^{*}_{n}=\alpha_{n+1}^{*}\circ s^{T}_{n}.$ (19)

Consider now the following diagram:

$\mathbf{C}$$\mathbf{L}$$F$

$\vdash$

$G$$T(A_{1},T^{\dagger}A_{1})$$T(A_{2},T^{\dagger}A_{2})$$T(f,T^{\dagger}f)$$T^{\dagger}A_{1}$$T^{\dagger}A_{2}$$\phi^{T}_{A_{1}}$$\phi^{T}_{A_{2}}$$T^{\dagger}f$$T(A_{1},T^{\dagger}A_{1})$$T(A_{1},T^{\dagger}A_{2})$$T(A_{1},T^{\dagger}f)$$T^{\dagger}A_{1}$$T^{\dagger}A_{2}$$\phi^{T}_{A_{1}}$$T(A_{2},T^{\dagger}A_{2})$$T(f,T^{\dagger}A_{2})$$\phi^{T}_{A_{2}}$$T^{\dagger}f$$S(T(A,-))$$T(A,-)\circ
S(T(A,-))$$T(B,-)\circ
S(T(B,-))$$S(T(B,-))$$S(T(f,-))$$T(f,-)*S(T(f,-))$$s^{T(A,-)}$$s^{T(B,-)}$$T(\mathrm{colim}(\tau))$$T(\mathrm{colim}(D))$$\mathrm{colim}(T\circ
D)$$\mathrm{colim}(T\tau)$$T(\mathrm{colim}(D^{\prime}))$$\mathrm{colim}(T\circ
D^{\prime})$$\tau_{\mathrm{colim}(D)}$$T(\mathrm{colim}(D))$$\mathrm{colim}(T\circ
D)$$\mathrm{colim}(\tau D)$$H(\mathrm{colim}(D))$$\mathrm{colim}(H\circ
D)$$T^{\dagger}A$$\mathrm{colim}(S(T_{A}))$$\mathrm{colim}(T_{A}\circ
S(T_{A}))$$T_{A}\mathrm{colim}(S(T_{A}))$$T(A,T^{\dagger}A)$$T^{\dagger}B$$\mathrm{colim}(S(T_{B}))$$\mathrm{colim}(T_{B}\circ
S(T_{B}))$$T_{B}\mathrm{colim}(S(T_{B}))$$T(B,T^{\dagger}B)$$\mathrm{colim}(s^{T_{A}})$$T(f,T^{\dagger}f)$$\mathrm{colim}(T_{f}*S(T_{f}))$$\mathrm{colim}(S(T_{f}))$$T^{\dagger}f$$\mathrm{colim}(s^{T_{B}})$$T_{f}\mathrm{colim}(S(T_{f}))$(1)(4)(3)(2)$T_{A}{\mathrm{colim}(S(T_{f}))}$$T_{A}(\mathrm{colim}(S(T_{A})))$$\mathrm{colim}(T_{A}\circ
S(T_{A})$$\mathrm{colim}(T_{A}S(T_{f}))$$T_{A}(\mathrm{colim}(S(T_{B})))$$\mathrm{colim}(T_{A}S(T_{B}))$$\mathrm{colim}(T_{f}S(T_{B}))$$T_{f}\mathrm{colim}(S(T_{B}))$$T_{B}(\mathrm{colim}(S(T_{B})))$$\mathrm{colim}(T_{B}\circ
S(T_{B}))$$\mathbf{C}\times\mathbf{D}$$\mathbf{A}\times\mathbf{B}$$\mathbf{D}$$\mathbf{B}$$T$$M$$N\times
M$$H$$\alpha$$T^{\dagger}NA$$\mathrm{colim}(T^{*}NA)$$\mathrm{colim}(MH^{*}A)$$M\mathrm{colim}(H^{*}A)$$MH^{\dagger}A$$T^{\dagger}NB$$\mathrm{colim}(T^{*}NB)$$\mathrm{colim}(MH^{*}B)$$M\mathrm{colim}(H^{*}B)$$MH^{\dagger}B$$\mathrm{colim}(\alpha_{A}^{*})$$MH^{\dagger}f$$\mathrm{colim}(MH^{*}f)$$\mathrm{colim}(T^{*}Nf)$$T^{\dagger}Nf$$\mathrm{colim}(\alpha_{B}^{*})$$M\mathrm{colim}(H^{*}f)$(1)(4)(3)(2)$S(T)$$MS(H)$$MHS(H)$$TS(T)$$TMS(H)$$s^{T}$$\alpha^{*}$$Ms^{H}$$T\alpha^{*}$$\alpha*S(H)$$M\circ
H\circ\langle\text{Id},H^{\dagger}\rangle$$T\circ\langle N,T^{\dagger}\circ
N\rangle$$T\circ\langle N,M\circ
H^{\dagger}\rangle$$T\circ\langle\text{Id},T^{\dagger}\rangle\circ
N$$T\circ(N\times M)\circ\langle\text{Id},H^{\dagger}\rangle$$M\circ
H^{\dagger}$$T^{\dagger}\circ
N$$\alpha\langle\text{Id},H^{\dagger}\rangle$$M\phi^{H}$$\phi^{T}N$$T\langle
N,\alpha^{\dagger}\rangle$$\alpha^{\dagger}$$MH^{\prime}Y(H^{\prime})$$T^{\prime}Y(T^{\prime})$$T^{\prime}\alpha^{\dagger}_{A}$$T^{\prime}MY(H^{\prime})$$\alpha_{A,Y(H^{\prime})}$$MY(H^{\prime})$$Y(T^{\prime})$$y^{T^{\prime}}$$My^{H^{\prime}}$$\alpha^{\dagger}_{A}$$\mathbf{C}$$\mathbf{D}$$T\circ\langle\text{Id},T^{\dagger}\rangle$$T^{\dagger}$$\phi^{T}$$\mathbf{A}$$\mathbf{B}$$H\circ\langle\text{Id},H^{\dagger}\rangle$$H^{\dagger}$$\phi^{H}$$M$$N$$\mathbf{C}$$\mathbf{L}$$F$

$\vdash$

$G$$\mathbf{C}$$\mathbf{L}$$F$

$\vdash$

$G$$\mathbf{CPO}$$\mathbf{CPO}_{\perp!}$$(-)_{\perp}$

$\vdash$

$U$$\mathbf{CPO}_{\perp!}$$\widehat{}\mathbf{M}$$-\circledcirc I$

$\vdash$

$\widehat{}\mathbf{M}(I,-)$$\mathbf{CPO}$$\mathbf{CPO}_{\perp!}$$(-)_{\perp}$

$\vdash$

$U$$\widehat{}\mathbf{M}$$-\circledcirc I$

$\vdash$

$\widehat{}\mathbf{M}(I,-)$${\llbracket\Theta\vdash
P\rrbracket}$$F_{pe}^{\times|\Theta|}$$\mathbf{C}_{pe}$$\mathbf{L}_{e}$$\mathbf{C}_{pe}^{|\Theta|}$${\llparenthesis\Theta\vdash
P\rrparenthesis}$$F_{pe}$$\mathbf{L}_{e}^{|\Theta|}$$\alpha$${\llbracket\Theta\vdash
P[R/X]\rrbracket}\circ
F_{pe}^{\times|\Theta|}$$F_{pe}\circ{\llparenthesis\Theta\vdash
P[R/X]\rrparenthesis}$$F_{pe}\circ{\llparenthesis\Theta,X\vdash
P\rrparenthesis}\circ\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle$${\llbracket\Theta,X\vdash P\rrbracket}\circ\langle
F_{pe}^{\times|\Theta|},{\llbracket\Theta\vdash R\rrbracket}\circ
F_{pe}^{\times|\Theta|}\rangle$${\llbracket\Theta,X\vdash
P\rrbracket}\circ\langle
F_{pe}^{\times|\Theta|},F_{pe}\circ{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle$${\llbracket\Theta,X\vdash
P\rrbracket}\circ\langle\text{Id},{\llbracket\Theta\vdash
R\rrbracket}\rangle\circ F_{pe}^{\times|\Theta|}$${\llbracket\Theta,X\vdash
P\rrbracket}\circ
F_{pe}^{\times(|\Theta|+1)}\circ\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle$$\alpha\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle$${\llbracket\Theta,X\vdash P\rrbracket}\langle
F_{pe}^{\times|\Theta|},\alpha\rangle$$\alpha$$F_{pe}\gamma^{-1}$${\llbracket\Theta\vdash
P[\mu X.P/X]\rrbracket}\circ
F_{pe}^{\times|\Theta|}$$F_{pe}\circ{\llparenthesis\Theta\vdash P[\mu
X.P/X]\rrparenthesis}$$\alpha$${\llbracket\Theta\vdash\mu X.P\rrbracket}\circ
F_{pe}^{\times|\Theta|}$$F_{pe}\circ{\llparenthesis\Theta\vdash\mu
X.P\rrparenthesis}$$\alpha$$\mathrm{fold}F_{pe}^{\times|\Theta|}$$F_{pe}\mathpzc{fold}$$\mathbf{R}(A)_{e}\times\mathbf{R}(B)_{e}$$\mathbf{R}(A\star
B)_{e}$$\star_{e}^{A,B}$$\mathbf{L}_{e}\times\mathbf{L}_{e}$$\mathbf{L}_{e}$$\star_{e}$$U^{A\star
B}_{e}$$U^{A}_{e}\times
U^{B}_{e}$$!_{e}$$\mathbf{R}(!A)_{e}$$U^{A}_{e}$$\mathbf{L}_{e}$$\mathbf{R}(A)_{e}$$!_{e}^{A}$$U^{!A}_{e}$$\mathbf{L}_{e}$$\mathbf{R}(C_{1})_{e}\times\cdots\times\mathbf{R}(C_{n})_{e}$$\mathbf{R}(A[\vec{C}/\Theta])_{e}$${{\lVert\Theta\vdash
A\rVert^{\vec{C}}}}$$\mathbf{L}_{e}\times\cdots\times\mathbf{L}_{e}$$\mathbf{L}_{e}$${\llbracket\Theta\vdash
A\rrbracket}$$U^{A[\vec{C}/\Theta]}_{e}$$U^{C_{1}}_{e}\times\cdots\times
U^{C_{n}}_{e}$$\mathbf{R}(C_{1})_{e}\times\cdots\times\mathbf{R}(C_{n})_{e}$$\mathbf{R}(A[\vec{C}/\Theta])_{e}$$\phi$$\mathbf{L}_{e}\times\cdots\times\mathbf{L}_{e}$$\mathbf{L}_{e}$${\llbracket\Theta,X\vdash
A\rrbracket}\circ\langle\text{Id},{\llbracket\Theta\vdash\mu
X.A\rrbracket}\rangle$$\phi$${{\lVert\Theta\vdash\mu
X.A\rVert^{\vec{C}}}}$${\llbracket\Theta\vdash\mu
X.A\rrbracket}$$U^{A[\vec{C}/\Theta]}_{e}$$U^{C_{1}}_{e}\times\cdots\times
U^{C_{n}}_{e}$$\mathbb{I}^{\mu
X.A[\vec{C}/\Theta]}_{e}\circ{\lVert\Theta,X\vdash A\rVert^{\vec{C},\mu
X.A[\vec{C}/\Theta]}}\circ\langle\text{Id},{{\lVert\Theta\vdash\mu
X.A\rVert^{\vec{C}}}}\rangle$$MH(A,-)^{n+2}\varnothing$$MH(A,-)^{n+1}\varnothing$$T(NA,MH(A,-)^{n+1}\varnothing)$$\alpha_{A,H(A,-)^{n}\varnothing}$$T(NA,MH(A,-)^{n}\iota_{2})$$\alpha_{A,H(A,-)^{n+1}\varnothing}$$T(NA,(\alpha^{*}_{A})_{n})$$T(NA,(\alpha^{*}_{A})_{n+1})$$T(NA,-)^{n+1}0$$T(NA,-)^{n+2}0$$MH(A,-)^{n+1}\iota_{2}$$T(NA,-)^{n+1}\iota_{1}$$(2)$$(1)$$T(NA,MH(A,-)^{n}\varnothing)$$MH(A_{2},-)^{n+1}\varnothing$$MH(A_{1},-)^{n+1}\varnothing$$T(NA_{2},MH(A_{2},-)^{n}\varnothing)$$\alpha_{A_{1},H(A_{1},-)^{n}\varnothing}$$\alpha_{A_{2},H(A_{2},-)^{n}\varnothing}$$T(NA_{1},MH(f,-)^{n}\varnothing)$$T(NA_{2},(\alpha^{*}_{A_{2}})_{n})$$T(NA_{1},-)^{n+1}0$$T(NA_{1},MH(A_{1},-)^{n}\varnothing)$$T(NA_{1},T(NA_{2},-)^{n}0)$$MH(f,-)^{n+1}\varnothing$$T(NA_{1},MH(A_{2},-)^{n}\varnothing)$$(2)$$(1)$$T(NA_{2},-)^{n+1}0$$T(NA_{1},T(Nf,-)^{n}0)$$T(Nf,MH(A_{2},-)^{n}\varnothing)$$T(NA_{1},(\alpha^{*}_{A_{1}})_{n})$$(3)$$T(Nf,T(NA_{2},-)^{n}0)$$T(NA_{1},(\alpha^{*}_{A_{2}})_{n})$$T(NA,MH^{\prime}(A,-)^{n}\varnothing)$$T(NA,MH(A,-)^{n}\varnothing)$$T(NA,-)^{n+1}0$$MH(A,-)^{n+1}\varnothing$$T(NA,(\alpha_{A}^{*})_{n})$$T(NA,-)^{n+1}0$$T(NA,((M\beta\circ\alpha)_{A}^{*})_{n})$$MH(A,H^{\prime}(A,-)^{n}\varnothing)$$MH^{\prime}(A,-)^{n+1}\varnothing$$T(NA,M(\beta_{A}^{*})_{n})$$M\beta_{A,H^{\prime}(A,-)^{n}\varnothing}$$M(\beta_{A}^{*})_{n+1}$(1)$MH(A,(\beta_{A}^{*})_{n})$$\alpha_{A,H(A,-)^{n}\varnothing}$$\alpha_{A,H^{\prime}(A,-)^{n}\varnothing}$$(\alpha_{A}^{*})_{n+1}$(2)(3)(4)$T(PE,-)^{n+1}0$$T(PE,T(NQE,-)^{n}0)$$T(PE,(T^{*}\gamma_{E})_{n})$$T(PE,MH(QE,-)^{n}\varnothing)$$T(PE,(\alpha^{*}_{QE})_{n})$$T(NQE,MH(QE,-)^{n}\varnothing)$$T(\gamma_{E},MH(QE,-)^{n}\varnothing)$$T(NQE,T(NQE,-)^{n}0)$$T(\gamma_{E},T(NQE,-)^{n}0)$$T(NQE,(\alpha^{*}_{QE})_{n})$$MH(QE,-)^{n+1}\varnothing$$\alpha_{(QE,H(QE,-)^{n}\varnothing)}$$(\alpha^{*}_{QE})_{n+1}$$(T^{*}\gamma_{E})_{n+1}$$(1)$$(2)$$(3)$$TMH^{n}\varnothing$$T^{n+1}0$$T^{n+2}0$$TMH^{n+1}\varnothing$$T\alpha_{n}^{*}$$T\alpha_{n+1}^{*}$$s_{n+1}^{T}=Ts_{n}^{T}$$TMs_{n}^{H}$(2)$\alpha_{H^{n}\varnothing}$$\alpha_{S(H)(n)}=\alpha_{H^{n+1}\varnothing}$$Ms_{n+1}^{H}=MHs_{n}^{H}$(3)$MH^{n+1}\varnothing$$MH^{n+2}\varnothing$$\alpha_{n+1}^{*}$(1)

Here the outside of the diagram is exactly the identity we aim to show, namely
the $(n+1)$-component. (1) commutes by definition of $\alpha_{n+1}^{*}$, (2)
commutes, since this is $T$ applied to equation (19), and finally (3) commutes
since $\alpha$ is natural.

###  A.7. Proof of Theorem 32

######  Proof A.7.

Using [SP82, Theorem 2], we get the following implications:

$(4)\iff(3)\iff(1)\Rightarrow(2)\iff(5).$

To finish the proof we will show $(2)\Rightarrow(3),$ which is stated in a
slightly weaker form in the same paper (but its proof is the same).

Assume $\mu$ is a colimiting cocone of $D$ in $\mathbf{C}_{e}$. Let $\nu:D\to
B$ be a colimiting cocone of $D$ in $\mathbf{C}$. Since $(1)\Rightarrow(3)$
and $(1)\Rightarrow(2)$ it follows that:

  1. 1.

Each $\nu_{i}$ is an embedding, $(\nu_{i}\circ\nu_{i}^{\bullet})_{i}$ is an
increasing sequence and
$\bigvee_{i}\nu_{i}\circ\nu^{\bullet}_{i}=\text{id}_{B}$;

  2. 2.

$\nu$ is a colimiting cocone of $D$ in $\mathbf{C}_{e}$.

Therefore, $\mu$ and $\nu$ are isomorphic as cocones and therefore there
exists an isomorphism $h:B\to A$, such that $\mu_{i}=h\circ\nu_{i}.$ Therefore
$\mu_{i}$ is an embedding (for every $i$) and for $i\leq j$, we have:

$\mu_{i}\circ\mu_{i}^{\bullet}=h\circ\nu_{i}\circ\nu_{i}^{\bullet}\circ
h^{\bullet}\leq h\circ\nu_{j}\circ\nu_{j}^{\bullet}\circ
h^{\bullet}=\mu_{j}\circ\mu_{j}^{\bullet}$

so that $(\mu_{i}\circ\mu_{i}^{\bullet})_{i}$ forms an increasing sequence
and:

$\bigvee_{i}\mu_{i}\circ\mu_{i}^{\bullet}=\bigvee_{i}h\circ\nu_{i}\circ\nu_{i}^{\bullet}\circ
h^{\bullet}=h\circ\left(\bigvee_{i}\nu_{i}\circ\nu_{i}^{\bullet}\right)\circ
h^{\bullet}=h\circ\text{id}_{B}\circ h^{-1}=\text{id}_{A}.$

###  A.8. Proof of Theorem 45

######  Proof A.8.

By induction on the derivation of $\Theta\vdash P.$ Let $|\Theta|=n$. The case
$\Theta\vdash\Theta_{i}$ is given by:

$\displaystyle{\llbracket\Theta\vdash\Theta_{i}\rrbracket}\circ F_{pe}^{\times
n}=\Pi_{i}\circ F_{pe}^{\times
n}=F_{pe}\circ\Pi_{i}=F_{pe}\circ{\llparenthesis\Theta\vdash\Theta_{i}\rrparenthesis}.$

So that $\alpha^{\Theta\vdash\Theta_{i}}=\text{id}$, as required. The case
$\Theta\vdash!A$ is given by:

$\displaystyle{\llbracket\Theta\vdash!A\rrbracket}\circ F_{pe}^{\times n}$
$\displaystyle=\,!_{e}\circ{\llbracket\Theta\vdash A\rrbracket}\circ
F_{pe}^{\times n}=F_{pe}\circ G_{pe}\circ{\llbracket\Theta\vdash
A\rrbracket}\circ F_{pe}^{\times
n}=F_{pe}\circ{\llparenthesis\Theta\vdash!A\rrparenthesis}$

So that $\alpha^{\Theta\vdash!A}=\text{id}$, as required.

The case $\Theta\vdash P\odot Q$ is given by:

$\displaystyle{\llbracket\Theta\vdash P\odot Q\rrbracket}\circ F_{pe}^{\times
n}$ $\displaystyle=\odot_{e}\circ\langle{\llbracket\Theta\vdash
P\rrbracket},{\llbracket\Theta\vdash Q\rrbracket}\rangle\circ F_{pe}^{\times
n}$ $\displaystyle(\text{Definition})$
$\displaystyle=\odot_{e}\circ\langle{\llbracket\Theta\vdash P\rrbracket}\circ
F_{pe}^{\times n},{\llbracket\Theta\vdash Q\rrbracket}\circ F_{pe}^{\times
n}\rangle$ $\displaystyle\cong\odot_{e}\circ\langle
F_{pe}\circ{\llparenthesis\Theta\vdash
P\rrparenthesis},F_{pe}\circ{\llparenthesis\Theta\vdash
Q\rrparenthesis}\rangle$ $\displaystyle(\text{IH})$
$\displaystyle=\odot_{e}\circ(F_{pe}\times
F_{pe})\circ\langle{\llparenthesis\Theta\vdash
P\rrparenthesis},{\llparenthesis\Theta\vdash Q\rrparenthesis}\rangle$
$\displaystyle\cong
F_{pe}\circ\boxdot_{pe}\circ\langle{\llparenthesis\Theta\vdash
P\rrparenthesis},{\llparenthesis\Theta\vdash Q\rrparenthesis}\rangle$
$\displaystyle(\text{Theorem~{}\ref{thm:boxdot is continuous}})$
$\displaystyle=F_{pe}\circ{\llparenthesis\Theta\vdash P\odot Q\rrparenthesis}$
$\displaystyle(\text{Definition})$

Reading off the morphism, we get $\alpha^{\Theta\vdash P\odot
Q}=\beta^{pe}\langle{\llparenthesis\Theta\vdash
P\rrparenthesis},{\llparenthesis\Theta\vdash
Q\rrparenthesis}\rangle\circ\odot_{e}\langle\alpha^{\Theta\vdash
P},\alpha^{\Theta\vdash Q}\rangle$, as required.

The case $\Theta\vdash\mu X.P$ is given by:

$\begin{array}[]{rclr}{\llbracket\Theta\vdash\mu X.P\rrbracket}\circ
F_{pe}^{\times n}&=&{\llbracket\Theta,X\vdash P\rrbracket}^{\dagger}\circ
F_{pe}^{\times n}&\\\ &\cong&F_{pe}\circ{\llparenthesis\Theta,X\vdash
P\rrparenthesis}^{\dagger}&(\text{Theorem }\ref{thm:alpha-dagger-def})\\\
&=&F_{pe}\circ{\llparenthesis\Theta\vdash\mu X.P\rrparenthesis}&\end{array}$

Reading off the morphism, we get $\alpha^{\Theta\vdash\mu
X.P}=(\alpha^{\Theta,X\vdash P})^{\dagger},$ as required.

###  A.9. Proof of Lemma 48

######  Proof A.9.

For (1): Essentially the same as [Fio94, Lemma C.0.3].

For (2): By induction on the derivation of $\Theta,X\vdash P.$ Let
$|\Theta|=n.$

Case $\Theta,X\vdash\Theta_{i}$:

${\llparenthesis\Theta\vdash\Theta_{i}[R/X]\rrparenthesis}={\llparenthesis\Theta\vdash\Theta_{i}\rrparenthesis}=\Pi_{i}=\Pi_{i}\circ\langle\Pi_{1},\ldots,\Pi_{n},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle={\llparenthesis\Theta,X\vdash\Theta_{i}\rrparenthesis}\circ\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle.$

so that $\gamma^{\Theta\vdash\Theta_{i}[R/X]}=\text{id},$ as required.

Case $\Theta,X\vdash X$:

${\llparenthesis\Theta\vdash X[R/X]\rrparenthesis}={\llparenthesis\Theta\vdash
R\rrparenthesis}=\Pi_{n+1}\circ\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle={\llparenthesis\Theta,X\vdash
X\rrparenthesis}\circ\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle$

so that $\gamma^{\Theta\vdash X[R/X]}=\text{id},$ as required.

Case $\Theta,X\vdash!A$:

$\displaystyle{\llparenthesis\Theta\vdash!A[R/X]\rrparenthesis}$
$\displaystyle={\llparenthesis\Theta\vdash!(A[R/X])\rrparenthesis}$
$\displaystyle=G_{pe}\circ{\llbracket\Theta\vdash A[R/X]\rrbracket}\circ
F_{pe}^{\times n}$ $\displaystyle=G_{pe}\circ{\llbracket\Theta,X\vdash
A\rrbracket}\circ\langle\text{Id},{\llbracket\Theta\vdash
R\rrbracket}\rangle\circ F_{pe}^{\times n}$
$\displaystyle(\text{Lemma~{}\ref{lem:alpha-substitution} (1)})$
$\displaystyle=G_{pe}\circ{\llbracket\Theta,X\vdash A\rrbracket}\circ\langle
F_{pe}^{\times n},{\llbracket\Theta\vdash R\rrbracket}\circ F_{pe}^{\times
n}\rangle$ $\displaystyle\cong G_{pe}\circ{\llbracket\Theta,X\vdash
A\rrbracket}\circ\langle F_{pe}^{\times
n},F_{pe}\circ{\llparenthesis\Theta\vdash R\rrparenthesis}\rangle$
$\displaystyle(\text{Theorem~{}\ref{thm:alpha-def}})$
$\displaystyle=G_{pe}\circ{\llbracket\Theta,X\vdash A\rrbracket}\circ
F_{pe}^{\times(n+1)}\circ\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle$
$\displaystyle={\llparenthesis\Theta,X\vdash!A\rrparenthesis}\circ\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle$

so that $\gamma^{\Theta\vdash!A[R/X]}=G_{pe}{\llbracket\Theta,X\vdash
A\rrbracket}\langle F_{pe}^{\times n},\alpha^{\Theta\vdash R}\rangle$.

Case $\Theta,X\vdash P\odot Q$:

$\displaystyle{\llparenthesis\Theta\vdash(P\odot Q)[R/X]\rrparenthesis}$
$\displaystyle={\llparenthesis\Theta\vdash P[R/X]\odot Q[R/X]\rrparenthesis}$
$\displaystyle=\boxdot_{pe}\circ\langle{\llparenthesis\Theta\vdash
P[R/X]\rrparenthesis},{\llparenthesis\Theta\vdash
Q[R/X]\rrparenthesis}\rangle$
$\displaystyle\cong\boxdot_{pe}\circ\langle{\llparenthesis\Theta,X\vdash
P\rrparenthesis}\circ\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle,{\llparenthesis\Theta,X\vdash
Q\rrparenthesis}\circ\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle\rangle$ $\displaystyle(\text{IH})$
$\displaystyle=\boxdot_{pe}\circ\langle{\llparenthesis\Theta,X\vdash
P\rrparenthesis},{\llparenthesis\Theta,X\vdash
Q\rrparenthesis}\rangle\circ\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle$ $\displaystyle={\llparenthesis\Theta,X\vdash P\odot
Q\rrparenthesis}\circ\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle$

so that $\gamma^{\Theta\vdash(P\odot
Q)[R/X]}=\boxdot_{pe}\langle\gamma^{\Theta\vdash P[R/X]},\gamma^{\Theta\vdash
Q[R/X]}\rangle$.

Case $\Theta,X\vdash\mu Y.P$:

$\displaystyle\phantom{bbb}{\llparenthesis\Theta\vdash\mu
Y.P[R/X]\rrparenthesis}$ $\displaystyle={\llparenthesis\Theta,Y\vdash
P[R/X]\rrparenthesis}^{\dagger}$
$\displaystyle\cong\left({\llparenthesis\Theta,Y,X\vdash
P\rrparenthesis}\circ\langle\text{Id},{\llparenthesis\Theta,Y\vdash
R\rrparenthesis}\rangle\right)^{\dagger}$ (IH and Remark 27)
$\displaystyle=\left({\llparenthesis\Theta,X,Y\vdash
P\rrparenthesis}\circ\emph{swap}_{n,0}\circ\langle\text{Id},{\llparenthesis\Theta,Y\vdash
R\rrparenthesis}\rangle\right)^{\dagger}$
$\displaystyle(\text{Lemma~{}\ref{lem:permutation} (2)})$
$\displaystyle=\left({\llparenthesis\Theta,X,Y\vdash
P\rrparenthesis}\circ\langle\text{Id},{\llparenthesis\Theta,Y\vdash
R\rrparenthesis},\Pi_{n+1}\rangle\right)^{\dagger}$
$\displaystyle=\left({\llparenthesis\Theta,X,Y\vdash
P\rrparenthesis}\circ\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\circ\emph{drop}_{n,0},\Pi_{n+1}\rangle\right)^{\dagger}$
$\displaystyle(\text{Lemma~{}\ref{lem:contraction} (2)})$
$\displaystyle=\left({\llparenthesis\Theta,X,Y\vdash
P\rrparenthesis}\circ(\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle\times\text{Id})\right)^{\dagger}$
$\displaystyle={\llparenthesis\Theta,X,Y\vdash
P\rrparenthesis}^{\dagger}\circ\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle$ $\displaystyle(\text{Proposition~{}\ref{prop:dagger-
equal}})$ $\displaystyle={\llparenthesis\Theta,X\vdash\mu
Y.P\rrparenthesis}\circ\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle$

so that $\gamma^{\Theta\vdash\mu Y.P[R/X]}=(\gamma^{\Theta,Y\vdash
P[R/X]})^{\dagger}$.

For (3): Let $|\Theta|=n$ and let $\vec{Z}:=(Z_{1},\ldots,Z_{n})\in
Ob(\mathbf{C}_{pe}^{\times n})$ be an arbitrary object. We shall prove the
equivalent statement

$F_{pe}\gamma^{\Theta\vdash P[R/X]}\circ\alpha^{\Theta\vdash
P[R/X]}=\alpha^{\Theta,X\vdash P}\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle\circ{\llbracket\Theta,X\vdash P\rrbracket}\langle
F_{pe}^{\times n},\alpha^{\Theta\vdash R}\rangle.$

We do so by induction on the derivation of $\Theta,X\vdash P.$

Case $\Theta,X\vdash\Theta_{i}$:

$\displaystyle(F_{pe}\gamma^{\Theta\vdash\Theta_{i}[R/X]}\circ\alpha^{\Theta\vdash\Theta_{i}[R/X]})_{\vec{Z}}$
$\displaystyle=\text{id}_{F(Z_{i})}$
$\displaystyle=(\alpha^{\Theta,X\vdash\Theta_{i}}\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle\circ{\llbracket\Theta,X\vdash\Theta_{i}\rrbracket}\langle
F_{pe}^{\times n},\alpha^{\Theta\vdash R}\rangle)_{\vec{Z}}$

Case $\Theta,X\vdash X$:

$\displaystyle(F_{pe}\gamma^{\Theta\vdash X[R/X]}\circ\alpha^{\Theta\vdash
X[R/X]})_{\vec{Z}}$ $\displaystyle=\alpha^{\Theta\vdash R}_{\vec{Z}}$
$\displaystyle=(\alpha^{\Theta,X\vdash
X}\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle\circ{\llbracket\Theta,X\vdash X\rrbracket}\langle
F_{pe}^{\times n},\alpha^{\Theta\vdash R}\rangle)_{\vec{Z}}$

Case $\Theta,X\vdash!A$:

$\displaystyle
F_{pe}\gamma^{\Theta\vdash!A[R/X]}\circ\alpha^{\Theta\vdash!A[R/X]}$
$\displaystyle=F_{pe}G_{pe}{\llbracket\Theta,X\vdash A\rrbracket}\langle
F_{pe}^{\times n},\alpha^{\Theta\vdash R}\rangle\circ\text{id}$
$\displaystyle=!_{e}{\llbracket\Theta,X\vdash A\rrbracket}\langle
F_{pe}^{\times n},\alpha^{\Theta\vdash R}\rangle$
$\displaystyle={\llbracket\Theta,X\vdash!A\rrbracket}\langle F_{pe}^{\times
n},\alpha^{\Theta\vdash R}\rangle$
$\displaystyle=\text{id}\circ{\llbracket\Theta,X\vdash!A\rrbracket}\langle
F_{pe}^{\times n},\alpha^{\Theta\vdash R}\rangle$
$\displaystyle=\alpha^{\Theta,X\vdash!A}\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle\circ{\llbracket\Theta,X\vdash!A\rrbracket}\langle
F_{pe}^{\times n},\alpha^{\Theta\vdash R}\rangle.$

Case $\Theta,X\vdash P\odot Q:$

Let $|\Theta|=n$ and let $\vec{Z}:=(Z_{1},\ldots,Z_{n})\in
Ob(\mathbf{C}_{pe}^{\times n})$ be an arbitrary object. Then the $\vec{Z}$
component of $\gamma^{\Theta\vdash P[R/X]}$ is a morphism

$\gamma^{\Theta\vdash P[R/X]}_{\vec{Z}}:{\llparenthesis\Theta\vdash
P[R/X]\rrparenthesis}\vec{Z}\to{\llparenthesis\Theta,X\vdash
P\rrparenthesis}\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle\vec{Z}$

hence we obtain from Theorem 41:

$\displaystyle\phantom{bbb}F_{pe}\big{(}\gamma_{\vec{Z}}^{\Theta\vdash
P[R/X]}\boxdot_{pe}\gamma_{\vec{Z}}^{\Theta\vdash
Q[R/X]}\big{)}\circ\beta^{pe}_{{\llparenthesis\Theta\vdash
P[R/X]\rrparenthesis}\vec{Z},{\llparenthesis\Theta\vdash
Q[R/X]\rrparenthesis}\vec{Z}}$
$\displaystyle=\beta^{pe}_{{\llparenthesis\Theta,X\vdash
P\rrparenthesis}\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle\vec{Z},{\llparenthesis\Theta,X\vdash
Q\rrparenthesis}\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle\vec{Z}}\circ\big{(}F_{pe}\gamma_{\vec{Z}}^{\Theta\vdash
P[R/X]}\odot_{e}F_{pe}\gamma_{\vec{Z}}^{\Theta\vdash Q[R/X]}\big{)},$

hence we find

$\displaystyle\phantom{bbb}F_{pe}\boxdot\langle\gamma^{\Theta\vdash
P[R/X]},\gamma^{\Theta\vdash
Q[R/X]}\rangle\circ\beta^{pe}\langle{\llparenthesis\Theta\vdash
P[R/X]\rrparenthesis},{\llparenthesis\Theta\vdash
Q[R/X]\rrparenthesis}\rangle$
$\displaystyle=\beta^{pe}\langle{\llparenthesis\Theta,X\vdash
P\rrparenthesis}\circ\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle,{\llparenthesis\Theta,X\vdash
Q\rrparenthesis}\circ\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle\rangle\circ$ $\displaystyle\qquad\odot_{e}\langle
F_{pe}\gamma^{\Theta\vdash P[R/X]},F_{pe}\gamma^{\Theta\vdash Q[R/X]}\rangle$
$\displaystyle=\beta^{pe}\langle{\llparenthesis\Theta,X\vdash
P\rrparenthesis},{\llparenthesis\Theta,X\vdash
Q\rrparenthesis}\rangle\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle\circ\odot_{e}\langle F_{pe}\gamma^{\Theta\vdash
P[R/X]},F_{pe}\gamma^{\Theta\vdash Q[R/X]}\rangle,$ (20)

Then, surpressing superscripts to improve readability:

$\displaystyle\phantom{bbb}F_{pe}\gamma\circ\alpha$
$\displaystyle=F_{pe}\boxdot_{pe}\langle\gamma,\gamma\rangle\circ\beta^{pe}\langle{\llparenthesis\Theta\vdash
P[R/X]\rrparenthesis},{\llparenthesis\Theta\vdash
Q[R/X]\rrparenthesis}\rangle\circ\odot_{e}\langle\alpha,\alpha\rangle$
$\displaystyle=\beta^{pe}\langle{\llparenthesis\Theta,X\vdash
P\rrparenthesis},{\llparenthesis\Theta,X\vdash
Q\rrparenthesis}\rangle\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle\circ\odot_{e}\langle
F_{pe}\gamma,F_{pe}\gamma\rangle\circ\odot_{e}\langle\alpha,\alpha\rangle$
$\displaystyle=\beta^{pe}\langle{\llparenthesis\Theta,X\vdash
P\rrparenthesis},{\llparenthesis\Theta,X\vdash
Q\rrparenthesis}\rangle\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle\circ\odot_{e}\langle
F_{pe}\gamma\circ\alpha,F_{pe}\gamma\circ\alpha\rangle$
$\displaystyle=\beta^{pe}\langle{\llparenthesis\Theta,X\vdash
P\rrparenthesis},{\llparenthesis\Theta,X\vdash
Q\rrparenthesis}\rangle\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle\circ$
$\displaystyle\qquad\odot_{e}\big{\langle}\alpha\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle\circ{\llbracket\Theta,X\vdash P\rrbracket}\langle
F_{pe}^{\times
n},\alpha\rangle,\alpha\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle\circ{\llbracket\Theta,X\vdash Q\rrbracket}\langle
F_{pe}^{\times n},\alpha\rangle\big{\rangle}$
$\displaystyle=\beta^{pe}\langle{\llparenthesis\Theta,X\vdash
P\rrparenthesis},{\llparenthesis\Theta,X\vdash
Q\rrparenthesis}\rangle\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle\circ$
$\displaystyle\qquad\odot_{e}\big{\langle}\alpha\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle,\alpha\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle\big{\rangle}\circ\odot_{e}\big{\langle}{\llbracket\Theta,X\vdash
P\rrbracket}\langle F_{pe}^{\times n},\alpha\rangle,{\llbracket\Theta,X\vdash
Q\rrbracket}\langle F_{pe}^{\times n},\alpha\rangle\big{\rangle}$
$\displaystyle=\beta^{pe}\langle{\llparenthesis\Theta,X\vdash
P\rrparenthesis},{\llparenthesis\Theta,X\vdash
Q\rrparenthesis}\rangle\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle\circ\odot_{e}\langle\alpha,\alpha\rangle\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle\circ$
$\displaystyle\qquad\odot_{e}\langle{\llbracket\Theta,X\vdash
P\rrbracket},{\llbracket\Theta,X\vdash Q\rrbracket}\rangle\langle
F_{pe}^{\times n},\alpha\rangle$
$\displaystyle=\left(\beta^{pe}\langle{\llparenthesis\Theta,X\vdash
P\rrparenthesis},{\llparenthesis\Theta,X\vdash
Q\rrparenthesis}\rangle\circ\odot_{e}\langle\alpha,\alpha\rangle\right)\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle\circ$
$\displaystyle\qquad\odot_{e}\langle{\llbracket\Theta,X\vdash
P\rrbracket},{\llbracket\Theta,X\vdash Q\rrbracket}\rangle\langle
F_{pe}^{\times n},\alpha\rangle$
$\displaystyle=\alpha\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle\circ{\llbracket\Theta,X\vdash P\odot
Q\rrbracket}\langle F_{pe}^{\times n},\alpha\rangle$

where the first and the last equalities are by definition, the second equality
is (A.9), the third and the fifth equalities are by functoriality of $\odot$,
the fourth equality is the induction hypothesis, and the penultimate equality
follows from $(\rho\circ\sigma)K=\rho K\circ\sigma K$ for any composable
functor $K$ and natural transformations $\rho$ and $\sigma$.

Case $\Theta,X\vdash\mu Y.P$:

$\displaystyle\phantom{bbb}F_{pe}\gamma^{\Theta\vdash\mu
Y.P[R/X]}\circ\alpha^{\Theta\vdash\mu Y.P[R/X]}$
$\displaystyle=F_{pe}(\gamma^{\Theta,Y\vdash
P[R/X]})^{\dagger}\circ(\alpha^{\Theta,Y\vdash P[R/X]})^{\dagger}$
$\displaystyle(\text{Definition})$
$\displaystyle=(F_{pe}\gamma^{\Theta,Y\vdash
P[R/X]}\circ\alpha^{\Theta,Y\vdash P[R/X]})^{\dagger}$
$\displaystyle(\text{Lemma~{}\ref{lem:alpha-operations} (1)})$
$\displaystyle=(\alpha^{\Theta,Y,X\vdash
P}\langle\text{Id},{\llparenthesis\Theta,Y\vdash
R\rrparenthesis}\rangle\circ{\llbracket\Theta,Y,X\vdash P\rrbracket}\langle
F_{pe}^{\times n+1},\alpha^{\Theta,Y\vdash R}\rangle)^{\dagger}$
$\displaystyle(\text{IH})$ $\displaystyle=(\alpha^{\Theta,X,Y\vdash
P}\emph{swap}_{n,0}\langle\text{Id},{\llparenthesis\Theta,Y\vdash
R\rrparenthesis}\rangle\circ$ $\displaystyle\qquad{\llbracket\Theta,X,Y\vdash
P\rrbracket}\emph{swap}_{n,0}\langle F_{pe}^{\times
n+1},\alpha^{\Theta,Y\vdash R}\rangle)^{\dagger}$
$\displaystyle(\text{Lemma~{}\ref{lem:permutation}})$
$\displaystyle=(\alpha^{\Theta,X,Y\vdash
P}\langle\Pi_{1},\ldots,\Pi_{n},{\llparenthesis\Theta,Y\vdash
R\rrparenthesis},\Pi_{n+1}\rangle\circ$
$\displaystyle\qquad{\llbracket\Theta,X,Y\vdash P\rrbracket}\langle
F_{pe}\Pi_{1},\ldots,F_{pe}\Pi_{n},\alpha^{\Theta,Y\vdash
R},F_{pe}\Pi_{n+1}\rangle)^{\dagger}$ $\displaystyle=(\alpha^{\Theta,X,Y\vdash
P}(\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle\times\text{Id})\circ{\llbracket\Theta,X,Y\vdash
P\rrbracket}(\langle F_{pe}^{\times n},\alpha^{\Theta\vdash R}\rangle\times
F_{pe}))^{\dagger}$ $\displaystyle(\text{Lemma~{}\ref{lem:contraction}})$
$\displaystyle=(\alpha^{\Theta,X,Y\vdash
P})^{\dagger}\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle\circ{\llbracket\Theta,X,Y\vdash
P\rrbracket}^{\dagger}\langle F_{pe}^{\times n},\alpha^{\Theta\vdash
R}\rangle$ $\displaystyle(\text{Lemma~{}\ref{lem:alpha-operations} (2)})$
$\displaystyle=\alpha^{\Theta,X\vdash\mu
Y.P}\langle\text{Id},{\llparenthesis\Theta\vdash
R\rrparenthesis}\rangle\circ{\llbracket\Theta,X\vdash\mu Y.P\rrbracket}\langle
F_{pe}^{\times n},\alpha^{\Theta\vdash R}\rangle$
$\displaystyle(\text{Definition})~{}~{}~{}~{}\quad$