Polynomials in homotopy type theory as a Kleisli category

Elies Harington; Samuel Mimram

REVIEW 3 major objections 4 minor 32 references

Polynomials in homotopy type theory as a Kleisli category

T0 review · 3 major / 4 minor · reviewed 2026-08-12 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read The paper shows that polynomials are exactly the Kleisli category of a comonad on spans.

desk verdict Solid HoTT proof that V-ary polynomials form the Kleisli category of the free-commutative-monoid comonad on spans; the advertised 1-categorical model of linear logic rests on an unproven truncation claim. read the letter →

arxiv 2411.09950 v2 pith:HYZPGX75 submitted 2024-11-15 math.CT

Elies Harington , Samuel Mimram This is my paper · ORCID

classification math.CT MSC 18C2018M0518N99

keywords polynomialfunctorsKleislicategoryspanslinearlogichomotopytypetheoryexponentialcomonadSeelymultisets

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper refines the construction of polynomials in homotopy type theory by showing that they arise from a universal construction on spans. The exponential modality $!_V A := \sum_{E:V}(E \to A)$, which forms the free commutative monoid on a type with arities in a universe $V$, lifts from types to the wild category of spans and becomes a comonad by self-duality. The central theorem states that the associated Kleisli category $\mathrm{Span}(U)_{!_V}$ is equivalent to the wild category $\mathrm{Poly}_V$ of $V$-ary polynomials. Since the span category is a wild Seely category, this equivalence makes polynomials a homotopical model of linear logic, and truncating to a 1-category is claimed to yield a Seely category in the usual sense.

What carries the argument

The central object is the exponential modality $!_V A := \sum_{E:V}(E \to A)$, the free commutative monoid on a type $A$ with arities in a universe $V$; when $V$ is the universe of finite types this is the homotopical analogue of the multiset construction. The argument shows that the unit $\eta$ and multiplication $\mu$ of this monad are cartesian natural transformations, so by the functoriality of the span construction the monad lifts to $\mathrm{Span}(U)$, and the self-duality of spans turns it into a comonad. The Kleisli comparison rests on the equivalence $\mathrm{Poly}_V(I,J) \simeq \mathrm{Span}(!_V I, J)$, which rewrites a polynomial as a span out of the bang of its source. The Seely isomorphisms $m_2$ and $m_0$ are transported from type-level isomorphisms $l_2$ and $l_0$, and the main technical labour is proving the required diagrams commute in the homotopy-theoretic sense.

What would settle it

Compute, in the truncated category $\|\mathrm{Span}(U)\|_1$, whether the truncated Seely isomorphisms $m_2$ and $m_0$ are still invertible and whether the defining Seely diagram commutes; a single non-invertible truncation of $m_2$ for finite types $A,B$ would falsify Theorem 4.14 without contradicting the Kleisli equivalence of Theorem 5.9. Equivalently, one can compare the hom sets of the truncated Kleisli category with those of the truncation of $\mathrm{Poly}_V$ for $V = \mathrm{Fin}$ to test whether the equivalence survives truncation.

Watch

Extended reading notes

Core claim

The paper's central discovery is Theorem 5.9: for a universe $V$ of small arities, the Kleisli wild category $\mathrm{Span}(U)_{!_V}$ associated to the comonad $!_V$ on spans is equivalent to $\mathrm{Poly}_V$, the wild category of $V$-ary polynomials. The comparison functor fixes objects and sends a polynomial $I \leftarrow E \to_V B \to J$ to the span $!_V I \leftarrow B \to J$, reading each fiber of $E \to B$ as the multiset of variables of one monomial. The paper verifies that this map preserves identities and composition, so the equivalence is a genuine equivalence of wild categories. As a corollary, the Seely structure built on $\mathrm{Span}(U)$ transfers to polynomials, and after truncation the authors claim a Seely category and hence a model of linear logic.

Load-bearing premise

The load-bearing premise is that truncating the wild span category to a 1-category preserves the entire Seely structure — the symmetric monoidal closed structure, finite products, the exponential comonad, and the Seely isomorphisms; the paper states this is 'not difficult' but gives no proof, and Theorem 4.14 collapses if any piece is lost.

Editorial extensions

If this is right

If Theorem 5.9 is correct, the intuition that 'linear polynomials are spans' becomes a theorem: spans sit inside $V$-ary polynomials as the linear maps, and the bang modality accounts for the reuse of variables.
The Seely structure on $\mathrm{Span}(U)$ transfers along the equivalence, so $V$-ary polynomials become a homotopical model of intuitionistic linear logic, with products and coproducts of types supplying the additive connectives.
Choosing $V$ as the finite types recovers finitary polynomial functors over groupoids, reconnecting the Kleisli presentation with the earlier bicategorical construction; choosing $V$ as contractible types recovers spans themselves, so the parameter $V$ interpolates from linear to arbitrary polynomial maps.
Because $\mathrm{Span}(U)$ is $\ast$-autonomous, the model extends from intuitionistic to classical linear logic without extra work.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

An implication the authors leave implicit is that if the truncation claim holds, the resulting model has an underlying category equivalent to the homotopy category of spaces, which is known not to be concrete; the model is therefore of a different nature from set-based semantics such as coherence spaces.
The paper notes a connection to Melliès' template games; a natural extension, not developed here, is to refine the Seely structure into a model of differential linear logic, with the derivative operation carried by the polynomial data.
A testable extension would be to check whether varying $V$ yields a graded family of linear-non-linear adjunctions, interpolating between linear polynomials for contractible $V$ and arbitrary polynomials for large $V$.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Dear colleague,

Quick take: this is a genuinely useful paper. It proves in HoTT that V-ary polynomials form the Kleisli category of the free-commutative-monoid comonad on spans (Theorem 5.9), and it builds a wild Seely structure on spans (Theorem 4.13). The proof of 5.9 is concrete and convincing; I checked the key equivalences and the composition computation. The V-ary generalization and the lifting of the exponential monad to spans are real innovations beyond Street's earlier observation, which the paper openly credits. The comparison with Mellies' template games is also helpful.

Where it gets soft: the advertised model of linear logic as an actual 1-category rests on Theorem 4.14, which is dispatched in one sentence: 'It is not difficult to show that the categorical structures are preserved by truncation.' That is load-bearing. To get a Seely category from the wild one, you need the symmetric monoidal closed structure, finite products, the comonad, and the Seely isomorphisms m2 and m0 to survive ||-||_1, and every naturality and coherence diagram to recheck. This is not automatic from Proposition 2.6, which only covers univalence. The reader's stress-test note is exactly right. It is fixable, probably, but it is not a trivial diagram chase. If truncation does not preserve all of that, Theorem 4.14 fails even though Theorems 4.13 and 5.9 stand.

There are two smaller gaps. Proposition 5.7 (univalence of Poly_V) is only sketched, and the paper explicitly leaves the associativity and unitality of Poly_V to follow from Theorem 5.9. That is acceptable only because the computation in 5.9 establishes compatibility with the Kleisli composition, but the ordering is awkward. Also, the whole paper works at the wild level, so the 'homotopical model' claim is really a promise about a future infinity-categorical refinement; the authors say this clearly in the introduction, so it is an honest limitation, not a hidden one.

Bottom line: the central equivalence is solid, the bridge to linear logic is plausible but under-proved at the truncation step. This deserves a serious referee; I would send it to review and ask for a real proof of Theorem 4.14 or a downgrade of that claim. I would cite it, and I would bring it to a reading group.

Referee Report

3 major / 4 minor

Summary. The paper constructs, in homotopy type theory, the V-ary exponential !_V A := Σ_{E:V}(E→A), shows that it is a monad on the universe U, lifts it to a comonad on the wild category Span(U), and proves that the resulting wild Kleisli category is equivalent to the wild category Poly_V of V-ary polynomials (Theorem 5.9). Along the way, it establishes that Span(U) is symmetric monoidal closed with finite products, assembles these structures into a wild Seely category (Theorem 4.13), and asserts that truncation to a 1-category preserves this structure, yielding an ordinary Seely category and therefore a model of linear logic (Theorem 4.14). The paper also relates the construction to Melliès' template games and to Street's earlier Kleisli observation.

Significance. If the missing technical points are supplied, this is a valuable contribution: it gives a homotopical model of linear logic in which spans are the linear maps, the exponential modality is the free commutative monoid on types, and polynomials are exactly the Kleisli morphisms. The proof of the central Kleisli equivalence (Theorem 5.9) is direct and checkable, with explicit computations for the monad laws, pullback preservation, and composition compatibility. The paper is also honest about the unresolved ∞-categorical coherence issues and explicitly credits Street's prior observation. However, the advertised consequence for ordinary (truncated) categories currently rests on an unproved preservation statement, and the construction of the Seely isomorphisms in spans has a gap; these are load-bearing for the linear-logic model claim.

major comments (3)

[Section 4, before Theorem 4.14] The sentence 'It is not difficult to show that the categorical structures are preserved by truncation' is not a proof, and the preservation is not automatic. Definition 2.5 replaces the object type by its 1-truncation and each hom-type by its 0-truncation, so the symmetric monoidal closed structure, finite products, the exponential comonad, and the Seely isomorphisms m2 and m0 all have to be redefined by truncation elimination, and the naturality and coherence diagrams of Definition 2.7 have to be rechecked for the truncated data. Proposition 2.6 only covers univalence, not structure preservation. Since Theorem 4.14 is the advertised passage from a wild category to an ordinary model of linear logic, this is a load-bearing gap that should be filled by a detailed proof, or the statement should be weakened to a conjecture.
[Section 4.2, after Proposition 4.12] The claim that 'l2 being a natural isomorphism, its naturality squares are cartesian' is not generally true. For a commutative square whose top and bottom maps are isomorphisms, the square is a pullback if and only if the vertical map is an isomorphism; here the vertical map is !f × !g or its analogue, which is not an equivalence for arbitrary f and g. Proposition 3.7 only lifts natural transformations whose naturality squares are pullbacks, so the construction of m2 := R(l2) as a natural isomorphism of spans requires a separate proof of cartesianness. The same point applies to l0, though the verification there is easier. Because m2 and m0 are used in Theorem 4.13 and in Theorem 4.14, this gap is load-bearing.
[Section 5.1, Proposition 5.7] The definition of the wild category PolyV is not fully established. Proposition 5.7 says that unitality and associativity of composition 'will follow from Theorem 5.9', but Theorem 5.9 is stated as an equivalence of the Kleisli category with the wild category PolyV, so it presupposes that PolyV already satisfies the category laws. The proof of Theorem 5.9 does show that the assignment respects composition and identities, so the laws could be transferred from the Kleisli category, but this transfer is not spelled out. In addition, the univalence of PolyV is only sketched: the assertion that an invertible polynomial must have p an equivalence and hence be a span is stated without proof. These points should be made precise, for example by stating Theorem 5.9 for precategories and then deriving the category structure of PolyV, or by giving direct proofs in Section 5.1.

minor comments (4)

[Proof of Proposition 3.2] There is a typo: 'gollowing' should be 'following'.
[Section 6.1] The assertion that [8] 'only actually constructs a wild 2-coherent category' and is 3-truncated rather than a bicategory is a substantive correction to prior work and is stated without argument; it would be helpful to add a precise justification or a reference.
[Notation throughout] The notation E →_V B for maps with V-small fibers is introduced only informally; a precise definition before Definition 5.5 would improve readability.
[Section 4.2, proof of Proposition 4.12] The final sentence 'Like with η, one can check...' is an incomplete sentence; it should be completed, since the verification is part of the proof.

Circularity Check

0 steps flagged · score 2.0 of 10

No significant circularity: the main Kleisli-to-polynomial equivalence is a direct construction, and the flagged truncation step is an omitted proof rather than a circular one.

full rationale

The paper's central derivation is self-contained: the exponential !V A is defined explicitly as Σ_{E:V}(E→A), its monad and comonad structure are verified by direct computation (Propositions 4.8, 4.10–4.12), the wild Seely structure is checked by diagram computations (Theorem 4.13), and the equivalence between PolyV and the Kleisli category is exhibited as an explicit map on morphisms (Propositions 5.8 and Theorem 5.9). No parameter is fitted to a target, and no predicted quantity is equal to an input by construction. The proof of Theorem 5.9 genuinely shows that the direct composition of polynomials matches pullback-composition of spans, so the Kleisli equivalence is not a restatement of the definition of polynomial composition. The sentence before Theorem 4.14, 'It is not difficult to show that the categorical structures are preserved by truncation,' is an unsupported assertion and therefore a correctness or completeness risk: if truncation does not preserve the Seely structure, the advertised linear-logic model would fail even if the wild-level theorems hold. That is an omitted proof, not a circular reduction. Similarly, Proposition 5.7 defers the proof that polynomial composition is unital and associative to Theorem 5.9; read literally this is a compressed presentation, but the proof of Theorem 5.9 establishes compatibility of the direct composition with the Kleisli composition, from which the laws are inherited, so the argument is not circular in substance. The paper also credits Street for the prior Kleisli observation and explicitly corrects the earlier self-cited work [8], which is used as background and comparison rather than as a load-bearing justification. The minor self-citation to [8] does not force any conclusion of the present paper.

Assumptions & free parameters 0 free parameters · 3 assumptions · 0 invented entities

No fitted or hand-chosen numerical parameters appear; the construction is parameterized by a universe V of small types, which is axiomatized but not fitted. No new postulates (invented entities) are introduced beyond the definitions of wild categories, spans, and the exponential !V, all of which are explicit constructions. The key assumptions are the HoTT foundations and the closure properties of V.

assumptions (3)

standard math Univalence axiom, function extensionality, and the existence of propositional/set/groupoid truncations (HoTT book).
These are the foundational principles of homotopy type theory used throughout; they are cited from [31] and are not specific to this paper.
domain assumption The universe V of small types is closed under dependent sums, finite coproducts, and contains the terminal type.
Section 4.1 postulates these closure properties; they are used to define the exponential functor !V, the unit and multiplication of the monad, and the Seely isomorphisms. Examples are V=Fin (finite types) or a smaller universe in a cumulative hierarchy.
standard math The equivalence between types over B and type families B -> U (fibered/indexed equivalence), and singleton-type contractibility.
Used in the proofs of Proposition 4.10, 5.8, and Theorem 5.9; these are standard results from the HoTT book (Section 2.1 and Lemma 3.11.8).

how reviews work

0 comments

Cite this review

Pith. "Pith review of Polynomials in homotopy type theory as a Kleisli category." pith.science (2026). https://pith.science/paper/HYZPGX75

@misc{pith2026241109950,
  author       = {Pith},
  title        = {Pith review of: Polynomials in homotopy type theory as a Kleisli category},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/HYZPGX75}},
  note         = {Machine review of arXiv:2411.09950}
}

read the original abstract

Polynomials in a category have been studied as a generalization of the traditional notion in mathematics. Their construction has recently been extended to higher groupoids, as formalized in homotopy type theory, by Finster, Mimram, Lucas and Seiller, thus resulting in a cartesian closed bicategory. We refine and extend their work in multiple directions. We begin by generalizing the construction of the free symmetric monoid monad on types in order to handle arities in an arbitrary universe. Then, we extend this monad to the (wild) category of spans of types, and thus to a comonad by self-duality. Finally, we show that the resulting Kleisli category is equivalent to the traditional category of polynomials. This thus establishes polynomials as a (homotopical) model of linear logic. In fact, we explain that it is closely related to a bicategorical model of differential linear logic introduced by Melli\`es.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

32 extracted references · 18 canonical work pages

[1]

Ghani, P

Altenkirch, T., N. Ghani, P. Hancock, C. McBride and P. Mo rris, Indexed containers, Journal of Functional Programming 25 (2015). https://doi.org/10.1017/S095679681500009X

doi:10.1017/s095679681500009x 2015
[2]

Levy and S

Altenkirch, T., P. Levy and S. Staton, Higher-order containers , in: Programs, Proofs, Processes: 6th Conference on Computability in Europe, CiE 2010, Ponta Delgada, Azores, P ortugal, June 30–July 4, 2010. Proceedings 6 , pages 11–20, Springer (2010). https://doi.org/10.1007/978-3-642-13962-8_2

work page doi:10.1007/978-3-642-13962-8_2 2010
[3]

N., A mixed linear and non-linear logic: Proofs, terms and model s, in: International Workshop on Computer Science Logic, pages 121–135, Springer (1994)

Benton, P. N., A mixed linear and non-linear logic: Proofs, terms and model s, in: International Workshop on Computer Science Logic, pages 121–135, Springer (1994). https://doi.org/10.1007/BFb0022251

doi:10.1007/bfb0022251 1994
[4]

Bierman, G. M., What is a categorical model of intuitionistic linear logic? , in: Typed Lambda Calculi and Applications: Second International Conference on Typed Lambda Calculi an d Applications, TLCA’95 Edinburgh, United Kingdom, April 10–12, 1995 Proceedings 2 , pages 78–93, Springer (1995). https://doi.org/10.1007/BFb0014046

work page doi:10.1007/bfb0014046 1995
[5]

Workshop on Logic and higher structures,

Buchholtz, U., Update on semisimplicial types in homotopy type theory . Workshop on Logic and higher structures,. https://www.cirm-math.fr/RepOrga/2689/Slides/s_buchholtz.pdf

work page
[6]

Capriotti, P. and N. Kraus, Univalent higher categories via complete semi-segal types . https://doi.org/10.1145/3158132

doi:10.1145/3158132
[7]

Clairambault, P. and S. Forest, The cartesian closed bicategory of thin spans of groupoids , in: 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) , pages 1–13, IEEE (2023)

work page 2023
[8]

Mimram, M

Finster, E., S. Mimram, M. Lucas and T. Seiller, A cartesian bicategory of polynomial functors in homotopy t ype theory, in: 37th Conference on the Mathematical Foundations of Program ming Semantics (MFPS 2021) (2021). https://doi.org/10.4204/EPTCS.351.5

work page doi:10.4204/eptcs.351.5 2021

Show all 32 references

[9]

Gambino, M

Fiore, M., N. Gambino, M. Hyland and G. Winskel, The cartesian closed bicategory of generalised species of s tructures, Journal of the London Mathematical Society 77, pages 203–220 (2008). https://doi.org/10.1112/jlms/jdm096

2008 doi
[10]

https://doi.org/10.1007/BFb0058516

Freyd, P., Homotopy is not concrete , in: The Steenrod Algebra and Its Applications: A Conference to C elebrate NE Steenrod’s Sixtieth Birthday: Proceedings of the Conferen ce held at the Battelle Memorial Institute, Columbus, Ohio March 30th–April 4th, 1970 , pages 25–34, Spr...

1970 doi
[11]

Gambino, N. and J. Kock, Polynomial functors and polynomial monads , in: Mathematical proceedings of the cambridge philosophical society, volume 154, pages 153–192, Cambridge University Press (20 13). https://doi.org/10.1017/S0305004112000394

doi
[12]

Haugseng and J

Gepner, D., R. Haugseng and J. Kock, ∞ -operads as analytic monads , International Mathematics Research Notices 2022, pages 12516–12624 (2022). https://doi.org/10.1093/imrn/rnaa332

2022 doi
[13]

https://doi.org/10.1016/0168-0072(88)90025-5

Girard, J.-Y., Normal functors, power series and λ -calculus, Annals of pure and applied logic 37, pages 129–177 (1988). https://doi.org/10.1016/0168-0072(88)90025-5

1988 doi
[14]

Gordon, R., A. J. Power and R. Street, Coherence for tricategories, volume 558, American Mathematical Society (1995). https://doi.org/10.1090/memo/0558

1995 doi
[15]

https://doi.org/10.1090/surv/063

Hovey, M., Model categories, 63, American Mathematical Society (2007). https://doi.org/10.1090/surv/063

2007 doi
[16]

https://doi.org/10.2168/LMCS-10(2:2)2014 Harington, Mimram 11–23

Hyvernat, P., A Linear Category of Polynomial Functors (extensional part ), Logical Methods in Computer Science 10 (2014). https://doi.org/10.2168/LMCS-10(2:2)2014 Harington, Mimram 11–23

2014 doi
[17]

https://doi.org/10.1016/0001-8708(81)90052-9

Joyal, A., Une th´ eorie combinatoire des s´ eries formelles, Advances in Mathematics 42, pages 1–82 (1981). https://doi.org/10.1016/0001-8708(81)90052-9

1981 doi
[18]

Kapulkin, K. and P. L. Lumsdaine, The simplicial model of univalent foundations (after voevo dsky), Journal of the European Mathematical Society 23, pages 2071–2126 (2021). https://doi.org/10.4171/JEMS/1050

2021 doi
[19]

https://doi.org/10.1093/imrn/rnq068

Kock, J., Polynomial Functors and Trees, International Mathematics Research Notices 2011, pages 609–673 (2010), ISSN 1073-7928. https://doi.org/10.1093/imrn/rnq068

2010 doi
[20]

https://doi.org/10.1016/j.entcs.2013.01.001

Kock, J., Data types with symmetries and polynomial functors over gro upoids, Electronic Notes in Theoretical Computer Science 286, pages 351–365 (2012). https://doi.org/10.1016/j.entcs.2013.01.001

2012 doi
[21]

L., Weak ω -categories from intensional type theory , Logical Methods in Computer Science 6 (2010)

Lumsdaine, P. L., Weak ω -categories from intensional type theory , Logical Methods in Computer Science 6 (2010). https://doi.org/10.2168/LMCS-6(3:24)2010

2010 doi
[22]

https://people.math.harvard.edu/~lurie/papers/HA.pdf

Lurie, J., Higher Algebra. https://people.math.harvard.edu/~lurie/papers/HA.pdf
[23]

https://doi.org/10.1515/9781400830558

Lurie, J., Higher topos theory , Princeton University Press (2009). https://doi.org/10.1515/9781400830558

2009 doi
[24]

https://doi.org/10.1007/978-1-4757-4721-8

Mac Lane, S., Categories for the working mathematician , volume 5, Springer Science & Business Media (2013). https://doi.org/10.1007/978-1-4757-4721-8

2013 doi
[25]

https://doi.org/10.1109/LICS.2019.8785830

Mellies, P.-A., Template games and diﬀerential linear logic , in: 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) , pages 1–13, IEEE, ISBN 978-1-72813-608-0. https://doi.org/10.1109/LICS.2019.8785830

2019
[26]

Melli` es, P.-A., Categorical semantics of linear logic , Panoramas et syntheses 27, pages 15–215 (2009)

2009
[27]

A., Linear logic, ∗-autonomous categories and cofree coalgebras , volume 92 (1989)

Seely, R. A., Linear logic, ∗-autonomous categories and cofree coalgebras , volume 92 (1989). https://doi.org/10.1090/conm/092/1003210

1989 doi
[28]

1301.1053

Stay, M., Compact closed bicategories , Theory and Applications of Categories 31, pages 755–798 (2016). 1301.1053

2016 arXiv
[29]

https://doi.org/10.48550/arXiv.1903.03890

Street, R., Polynomials as spans . https://doi.org/10.48550/arXiv.1903.03890

1903 doi arXiv
[30]

https://doi.org/10.1007/BFb0018351

Taylor, P., Quantitative domains, groupoids and linear logic , in: Category Theory and Computer Science: Manchester, UK, September 5–8, 1989 Proceedings , pages 155–181, Springer (1989). https://doi.org/10.1007/BFb0018351

1989 doi
[31]

Univalent Foundations Program, T., Homotopy Type Theory: Univalent Foundations of Mathematic s, https://homotopytypetheory.org/book, Institute for Advanced Study (2013)

2013
[32]

Van Den Berg, B. and R. Garner, Types are weak ω -groupoids, Proceedings of the London mathematical society 102, pages 370–394 (2011). https://doi.org/10.1112/plms/pdq026

2011 doi

Pith tools

Reviewed August 12, 2026 · model on record in the stance chip above.

[1] [1]

Ghani, P

Altenkirch, T., N. Ghani, P. Hancock, C. McBride and P. Mo rris, Indexed containers, Journal of Functional Programming 25 (2015). https://doi.org/10.1017/S095679681500009X

doi:10.1017/s095679681500009x 2015

[2] [2]

Levy and S

Altenkirch, T., P. Levy and S. Staton, Higher-order containers , in: Programs, Proofs, Processes: 6th Conference on Computability in Europe, CiE 2010, Ponta Delgada, Azores, P ortugal, June 30–July 4, 2010. Proceedings 6 , pages 11–20, Springer (2010). https://doi.org/10.1007/978-3-642-13962-8_2

work page doi:10.1007/978-3-642-13962-8_2 2010

[3] [3]

N., A mixed linear and non-linear logic: Proofs, terms and model s, in: International Workshop on Computer Science Logic, pages 121–135, Springer (1994)

Benton, P. N., A mixed linear and non-linear logic: Proofs, terms and model s, in: International Workshop on Computer Science Logic, pages 121–135, Springer (1994). https://doi.org/10.1007/BFb0022251

doi:10.1007/bfb0022251 1994

[4] [4]

Bierman, G. M., What is a categorical model of intuitionistic linear logic? , in: Typed Lambda Calculi and Applications: Second International Conference on Typed Lambda Calculi an d Applications, TLCA’95 Edinburgh, United Kingdom, April 10–12, 1995 Proceedings 2 , pages 78–93, Springer (1995). https://doi.org/10.1007/BFb0014046

work page doi:10.1007/bfb0014046 1995

[5] [5]

Workshop on Logic and higher structures,

Buchholtz, U., Update on semisimplicial types in homotopy type theory . Workshop on Logic and higher structures,. https://www.cirm-math.fr/RepOrga/2689/Slides/s_buchholtz.pdf

work page

[6] [6]

Capriotti, P. and N. Kraus, Univalent higher categories via complete semi-segal types . https://doi.org/10.1145/3158132

doi:10.1145/3158132

[7] [7]

Clairambault, P. and S. Forest, The cartesian closed bicategory of thin spans of groupoids , in: 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) , pages 1–13, IEEE (2023)

work page 2023

[8] [8]

Mimram, M

Finster, E., S. Mimram, M. Lucas and T. Seiller, A cartesian bicategory of polynomial functors in homotopy t ype theory, in: 37th Conference on the Mathematical Foundations of Program ming Semantics (MFPS 2021) (2021). https://doi.org/10.4204/EPTCS.351.5

work page doi:10.4204/eptcs.351.5 2021