Pith. sign in

REVIEW 2 major objections 5 minor 45 references

Comparing semantic frameworks for dependently-sorted algebraic theories

T0 review · 2 major / 5 minor · reviewed 2026-08-10 · deepseek-v4-flash

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

Pith's one-line read The paper claims that comprehension categories — categories of contexts with a fibration of types and a comprehension operation — form a unified 2-categorical home in which almost all established categorical models of dependently-sorted…

desk verdict A solid, genuinely useful 2-categorical map of semantic frameworks; central claim holds up in the declared set-theoretic scope, and the paper deserves peer review. read the letter →

arxiv 2412.19946 v2 pith:W366J6DE submitted 2024-12-27 math.CT cs.PLmath.LO

Benedikt Ahrens , Peter LeFanu Lumsdaine , Paige Randall North This is my paper · ORCID
classification math.CTcs.PLmath.LO MSC 18C1018C3518D3018N10
keywords dependenttypetheorycomprehensioncategoriesdisplaymapwithfamiliescontextualnaturalmodels2-categoriescategoricalsemantics
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

This paper is a map of the many categorical structures used to model algebraic theories whose sorts depend on previous sorts. It argues that most of these structures are not independent inventions but variants of a single object, the comprehension category, and it proves the translations between them. Concretely, it shows that display map categories, structured display map categories, clans, finite-limit categories, categories with attributes, categories with families, natural models, and contextual categories all embed as sub-2-categories — usually full — of the 2-category of comprehension categories. The differences between the models reduce to conditions on the fibration of types and on the comprehension functor. A sympathetic reader should care because the paper replaces scattered and partly folkloric comparisons with one reference framework and explicit equivalence, isomorphism, and adjunction results.

What carries the argument

The central object is the comprehension category, a category $C$ of contexts together with a fibration $p: T \to C$ of types and a comprehension functor $\chi: T \to C^{\to}$ that sends each type to its 'context extension' projection, lying strictly over the codomain functor and cartesian with respect to pullbacks. The paper arranges these into a 2-category with pseudo maps, which preserve context extension only up to isomorphism, plus variants with strict maps and transformations as 2-cells. The entire classification is driven by two families of conditions: conditions on the fibration (split, discrete) and conditions on the comprehension functor (full, subcategory inclusion, replete, composition-closed, trivial, contextual). The 'contextual slice' construction, which turns a comprehension category into one whose objects are finite sequences of types, relates contextual and non-contextual models. It is this parameterized structure, rather than any single theorem, that carries the argument.

What would settle it

Reprove Theorems 1.16 and 2.22 in univalent foundations with univalent categories: if the displayed isomorphisms do not remain isomorphisms, or even equivalent 2-categories, then the paper's central organizing claim is foundation-dependent rather than fully categorical.

Watch

Extended reading notes

Core claim

The central discovery is that the loose family of categorical models for dependent sorts can be organized around comprehension categories without forcing a single model on anyone. Working with the 2-category of comprehension categories and pseudo maps, the paper establishes a web of exact comparisons: display map categories appear as the sub-2-category of replete subcategorical comprehension categories, structured display map categories as the strict-map sub-2-category of subcategorical ones, clans as rooted replete composition-closed ones, finite-limit categories as rooted trivial ones, categories with attributes as discrete comprehension categories, categories with families as full split comprehension categories, and contextual categories as discrete contextual ones. Alongside these embeddings there are adjunctions such as fullification, repletion, composition closure, and the contextual-core construction. The paper is careful to separate strict maps, pseudo maps, and transformations, and it documents cases, such as structured display map categories, where pseudo and strict behaviour genuinely diverge.

Load-bearing premise

The comparisons assume a mathematical world in which you can ask whether two objects of a category are literally equal, not merely isomorphic; in foundations where that question is not available, some of the stated isomorphisms and adjunctions must be weakened to equivalences.

Editorial extensions

If this is right

  • Because display map categories are exactly the replete subcategorical comprehension categories, any construction or result for comprehension categories in that sub-2-category applies verbatim to display map categories.
  • Categories with attributes, categories with families, and natural models form a chain of 2-equivalences, so the choice among them is a matter of presentation, not mathematical content.
  • For contextual categories, pseudo maps and strict maps agree up to equivalence, so the 2-categorical and 1-categorical perspectives coincide for this class of models.
  • The adjunctions between comprehension categories and their subclasses — repletion, fullification, composition closure, and contextual core — give canonical ways to move from a coarser model to a finer one and back, which is exactly what a unified semantics of dependent type theory needs.

Reading between the lines

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

  • Our inference: the 2-categorical embeddings imply that any 2-categorical limit, colimit, or adjunction computed in the ambient 2-category of comprehension categories restricts to the embedded models where it exists; the paper does not spell out this transfer principle, but it follows directly from the embeddings being 2-functors.
  • Our inference: a newly proposed semantic framework for dependent sorts can be classified by checking whether its category of models is 2-equivalent to a full sub-2-category of comprehension categories satisfying a combination of the listed conditions; this gives a cheap test for whether the framework is genuinely new or a repackaging of an existing one.
  • Our inference: the paper's set-theoretic strict-equality caveat suggests that, in univalent foundations, the printed isomorphisms such as $\mathrm{sDMC} \cong \mathrm{CompCat}^{\mathrm{str2}}_{\mathrm{sub}}$ are likely to become equivalences or biequivalences rather than literal isomorphisms; re-proving the diagrams there would clarify which of the comparisons are structural and which are artifact
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

2 major / 5 minor

Summary. The paper proposes comprehension categories with pseudo maps as a unifying 2-categorical language for models of dependently-sorted algebraic theories. It establishes, or sketches, a series of embeddings, isomorphisms, and equivalences between display-map-style models (display map categories, structured display map categories, clans, finite-limit categories) and type-primitive models (categories with attributes, categories with families, natural models, contextual categories, C-systems, B-systems). The relationships are summarised in diagrams for the rooted and unrooted cases, and the paper distinguishes carefully between strict maps, pseudo maps, and transformations. The authors flag at the end that some results rely on a setting with strict equality of objects.

Significance. If correct, the paper provides a valuable systematisation of a scattered literature, organizing the main categorical models of dependent type theory around comprehension categories and making explicit where the comparisons are equivalences, adjunctions, or mere embeddings. Its strengths include a clear 2-categorical treatment of pseudo versus strict maps, a uniform notation for the relevant subclasses of comprehension categories, and an honest discussion of non-invariance and foundational caveats. The main comparisons are coherent within the stated set-theoretic scope, and I agree with the reader that the strict-equality caveat is a scope limitation rather than a hidden error.

major comments (2)
  1. [§3.1, Theorem 2.22] The stated isomorphism sDMC ≅ CompCat^{str2}_{sub} is asserted without a proof; the text immediately contrasts it with Theorem 1.16 but gives no argument. Since the non-replete case is precisely where the paper claims strict and pseudo maps diverge, and since this result is one of the headline identifications of Section 3.1, please provide a proof or at least a complete sketch, showing that the object map, the 1-cell map, and the 2-cell map are bijections on the nose.
  2. [§4.1, Propositions 3.8 and 3.9] The pseudo-map equivalences CwA^{ps} ≃ CompCat^{ps}_{disc} and CwA^{ps} ≃ CompCat^{ps,spl}_{full,spl} are not established by the cited Blanco results, which are 1-categorical. The proofs say 'similarly direct'/'direct'; because the paper's contribution is precisely the 2-categorical comparison, please expand these proofs or provide precise references for the 2-categorical statements.
minor comments (5)
  1. [§1 and Definition 1.1] The sentence 'All our 2-categories and functors are strict' is potentially confusing, since the paper's main 1-cells are pseudo maps; please clarify that strictness refers to the composition of 2-cells and the sense in which functors between the 2-categories are strict.
  2. [Definition 7.3 and Proposition 3.9] The notation CompCat^{str1,spl}_{full,spl} and CompCat^{ps,spl}_{full,spl} is hard to parse, with 'spl' appearing both as a condition on objects and as a restriction on maps; please define the convention explicitly at first use.
  3. [§3.1, Example 2.23] The description of the display maps in C' appears garbled: the sentence contrasting left and right point inclusions is self-contradictory as printed. Please correct the example so that the intended failure of strict preservation of display maps is unambiguous.
  4. [Figures 3–5] The diagrams use ⊥ to denote adjunctions but do not indicate whether the displayed arrow is the left or right adjoint; the text states the directions, but a note in the captions would make the figures self-contained.
  5. [Further Directions] The strict-equality caveat is placed only in the final section; since it affects the isomorphisms in Theorems 1.16 and 2.22 as well as Section 4, please state the caveat in the introduction or at the first use of these comparison results.

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity: the comparison theorems are coherent, and the self-citations used are supporting inputs rather than load-bearing conclusions.

full rationale

The paper's central claim is that comprehension categories serve as a unifying 2-categorical language into which established models embed. This is a comparison result, not a derivation of predictions from fitted inputs. The comprehension category formalism is taken from Jacobs, not defined in terms of the target models; the subclasses such as full, subcategorical, replete, discrete, and composition-closed are explicitly chosen to match the compared structures, but the theorems (Theorem 1.16, Theorem 2.22, Theorem 3.1, Propositions 3.8, 3.9, 4.1, 4.3) prove the relevant 2-categorical isomorphisms and equivalences rather than assuming them. The self-citations to ALV18 and AENR23 are used for supporting equivalences among established reformulations (CwF/CwA comparison formalized in univalent foundations, and C-system/B-system equivalence), but these are not the basis for the paper's main embedding claims, and they are published with independent proofs or formalization. The foundational caveat about strict equality of objects in Section 4 is explicitly flagged in Further Directions, so it is a scope limitation rather than a hidden circularity. The paper does not fit parameters, rename a known result as a prediction, or invoke a uniqueness theorem from the authors' own work to forbid alternatives. All load-bearing derivations are either proven in the text or supported by external/independent sources, so no circular step meeting the required evidentiary standard is present.

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

The paper introduces no fitted parameters and no new entities; it works within established categorical structures. Its load-bearing axioms are the standard foundations of 2-category theory and fibrations, plus a set-theoretic foundation with strict equality of objects (flagged by the authors in Further Directions). It also imports several specific prior results as black boxes, which are clearly cited.

assumptions (4)
  • standard math Standard 2-category theory, fibrations, and the Grothendieck construction (presheaves correspond to discrete fibrations) are taken as background.
    Used throughout, especially in Definition 2.1 and Proposition 3.8.
  • domain assumption A set-theoretic foundation in which strict equality of objects in a category is available.
    The authors state in Further Directions that Section 4 results rely on this; needed for claims of isomorphism versus equivalence (e.g., Theorems 1.16 and 2.22).
  • domain assumption The definitions of the various models (DMC, sDMC, clan, Lex, CwA, CwF, natural model, contextual category) are taken as given from the cited literature, and the paper's chosen variants (e.g., unrooted by default) are adopted.
    The comparisons are as good as the definitions; Remark 2.9 notes the unrooted default is a departure from some established definitions.
  • domain assumption Prior equivalence results are used as black boxes: ALV 2018 (CwF versus type categories), AENR 2023 (B-systems versus C-systems), and Hofmann 1997 (CwF versus CwA).
    These underpin Propositions 4.1 and 4.5; they are cited as established, not proved in this paper.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Comparing semantic frameworks for dependently-sorted algebraic theories." pith.science (2026). https://pith.science/paper/W366J6DE

@misc{pith2026241219946,
  author       = {Pith},
  title        = {Pith review of: Comparing semantic frameworks for dependently-sorted algebraic theories},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/W366J6DE}},
  note         = {Machine review of arXiv:2412.19946}
}
read the original abstract

Algebraic theories with dependency between sorts form the structural core of Martin-L\"of type theory and similar systems. Their denotational semantics are typically studied using categorical techniques; many different categorical structures have been introduced to model them (contextual categories, categories with families, display map categories, etc.) Comparisons of these models are scattered throughout the literature, and a detailed, big-picture analysis of their relationships has been lacking. We aim to provide a clear and comprehensive overview of the relationships between as many such models as possible. Specifically, we take *comprehension categories* as a unifying language and show how almost all established notions of model embed as sub-2-categories (usually full) of the 2-category of comprehension categories.

Figures

Figures reproduced from arXiv: 2412.19946 by the authors.

Figure 1
Figure 1. Models with types as display maps (Section 3) (Comprehension categories) (Cats with attributes) (Discrete comp cats) (Cats with families) (Natural models) (Discrete pointed comp cats) (Contextual categories) (Contextual discrete comp cats) (C-systems) (B-systems) ≃ ≃ ≃ ⊥ ≃ ≃ ≃ [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Models with types as primitive (Section 4) common home in which to compare those notions and others introduced since. In this section we set up the 2-categories of comprehension categories into which we will later embed the other notions considered, along with key constructions and properties of comprehension categories for later use. ‘roughout, we denote isomorphisms by , equivalences of (1- and 2-) cat￾egories by… view at source ↗
Figure 3
Figure 3. Notions with types as maps, unrooted 17 [PITH_FULL_IMAGE:figures/full_fig_p017_3.png] view at source ↗
Figures from the paper (2 more)
Figure 4
Figure 4. Figure 4: Notions with types as maps, rooted CompCatdisc CwAps CwFwk NatModps CompCatstr1 disc CwAstr1 CwFstr1 NatModstr1 CompCatdisc,⋄ CwAps ⋄ CompCatstr2 disc,⋄ CwAstr1 ⋄ CompCatdisc,cxl CxlCat CompCatstr2 disc,cxl ≃ Pr.38 ≃ Pr.41 ≃ Pr.43 ≃ Pr.38 ≃ Pr.41 ≃ Pr.43 ⊥ ≃ ⊥ ≃ ≃ Pr.4…
Figure 5
Figure 5. Figure 5: Notions with types primitive 18 [PITH_FULL_IMAGE:figures/full_fig_p018_5.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

45 extracted references · 36 canonical work pages

  1. [1]

    Benedikt Ahrens, Jacopo Emmenegger, Paige Randall North, and Egbert Rijke, B -systems and C -systems are equivalent , The Journal of Symbolic Logic (2023), 1–9, http://dx.doi.org/10.1017/jsl.2023.41 doi:10.1017/jsl.2023.41

    work page doi:10.1017/jsl.2023.41 2023

  2. [2]

    3, 213--227, http://dx.doi.org/10.1007/s000120050111 doi:10.1007/s000120050111

    Ji r \' Ad\' a mek, Michel H\' e bert, and Ji r \' Rosick\' y , On essentially algebraic theories and their generalizations, Algebra Universalis 41 (1999), no. 3, 213--227, http://dx.doi.org/10.1007/s000120050111 doi:10.1007/s000120050111

    work page doi:10.1007/s000120050111 1999

  3. [3]

    3--22, http://dx.doi.org/10.1007/978-981-97-8943-6_1 doi:10.1007/978-981-97-8943-6_1

    Benedikt Ahrens, Peter LeFanu Lumsdaine, and Paige Randall North, Comparing semantic frameworks for dependently-sorted algebraic theories, Programming Languages and Systems (Oleg Kiselyov, ed.), Springer Nature Singapore, 2025, pp. 3--22, http://dx.doi.org/10.1007/978-981-97-8943-6_1 doi:10.1007/978-981-97-8943-6_1

    work page doi:10.1007/978-981-97-8943-6_1 2025

  4. [4]

    Categorical structures for type theory in univalent foundations

    Benedikt Ahrens, Peter LeFanu Lumsdaine, and Vladimir Voevodsky, Categorical structures for type theory in univalent foundations, Logical Methods in Computer Science 14 (2018), no. 3, 1--18, http://arxiv.org/abs/1705.04310 arXiv:1705.04310 , http://dx.doi.org/10.23638/LMCS-14(3:18)2018 doi:10.23638/LMCS-14(3:18)2018 , https://lmcs.episciences.org/4814

    work page Pith review arXiv 2018

  5. [5]

    189, Cambridge University Press, Cambridge, 1994, http://dx.doi.org/10.1017/CBO9780511600579 doi:10.1017/CBO9780511600579

    Ji r \' Ad \'a mek and Ji r \' Rosick \'y , Locally presentable and accessible categories, London Mathematical Society Lecture Note Series, vol. 189, Cambridge University Press, Cambridge, 1994, http://dx.doi.org/10.1017/CBO9780511600579 doi:10.1017/CBO9780511600579

    doi:10.1017/cbo9780511600579 1994

  6. [6]

    Homotopy theoretic models of identity types

    Steve Awodey and Michael A. Warren, Homotopy theoretic models of identity types, Math. Proc. Camb. Phil. Soc. 146 (2009), no. 1, 45--55, http://arxiv.org/abs/0709.0248 arXiv:0709.0248 , http://dx.doi.org/10.1017/S0305004108001783 doi:10.1017/S0305004108001783

    work page Pith review arXiv 2009

  7. [7]

    Steve Awodey, Natural models of homotopy type theory, Math. Struct. Comput. Sci. 28 (2018), no. 2, 241--286, http://arxiv.org/abs/1406.3219 arXiv:1406.3219 , http://dx.doi.org/10.1017/S0960129516000268 doi:10.1017/S0960129516000268

    arXiv 2018

  8. [8]

    Modal Dependent Type Theory and Dependent Right Adjoints

    Lars Birkedal, Ranald Clouston, Bassel Mannaa, Rasmus Ejlers M gelberg, Andrew M. Pitts, and Bas Spitters, Modal dependent type theory and dependent right adjoints, Math. Structures Comput. Sci. 30 (2020), no. 2, 118--138, http://arxiv.org/abs/1804.05236 arXiv:1804.05236 , http://dx.doi.org/10.1017/s0960129519000197 doi:10.1017/s0960129519000197

    work page Pith review arXiv 2020

Show all 45 references
  1. [9]

    Nijmegen

    Javier Blanco, Relating categorical approaches to type dependency, 1991, Masters thesis, Univ. Nijmegen

    1991

  2. [10]

    thesis, Oxford, 1978

    John Cartmell, Generalised algebraic theories and contextual categories, Ph.D. thesis, Oxford, 1978

    1978

  3. [11]

    Pure Appl

    , Generalised algebraic theories and contextual categories, Ann. Pure Appl. Logic 32 (1986), no. 3, 209--243

    1986

  4. [12]

    Structures Comput

    Pierre Clairambault and Peter Dybjer, The biequivalence of locally cartesian closed categories and M artin- L \" o f type theories , Math. Structures Comput. Sci. 24 (2014), no. 6, e240606, 54, http://arxiv.org/abs/1112.3456 arXiv:1112.3456 , http://dx.doi.org/10.1017/S0960129...

    2014 arXiv

  5. [13]

    42, 1476--1512, http://arxiv.org/abs/2403.03085 arXiv:2403.03085 , http://www.tac.mta.ca/tac/volumes/41/42/41-42abs.html

    Greta Coraglia and Jacopo Emmenegger, A 2-categorical analysis of context comprehension, Theory and Applications of Categories 41 (2024), no. 42, 1476--1512, http://arxiv.org/abs/2403.03085 arXiv:2403.03085 , http://www.tac.mta.ca/tac/volumes/41/42/41-42abs.html

    2024 arXiv

  6. [14]

    Pierre - Louis Curien, Richard Garner, and Martin Hofmann, Revisiting the categorical interpretation of dependent type theory, Theor. Comput. Sci. 546 (2014), 99--119, http://dx.doi.org/10.1016/J.TCS.2014.03.003 doi:10.1016/J.TCS.2014.03.003 , https://doi.org/10.1016/j.tcs.2014.03.003

    2014 doi

  7. [15]

    Menno de Boer, A proof and formalization of the initiality conjecture of dependent type theory, 2020, Licentiate thesis, Stockholm University, http://www.diva-portal.org/smash/record.jsf?pid=diva2

    2020

  8. [16]

    Sci., vol

    Peter Dybjer, Internal type theory, Types for proofs and programs ( T orino, 1995) (Berlin, Heidelberg) (Stefano Berardi and Mario Coppo, eds.), Lecture Notes in Comput. Sci., vol. 1158, Springer, 1996, pp. 120--134, http://dx.doi.org/10.1007/3-540-61780-9_66 doi:10.1007/3-540...

    1995 doi

  9. [17]

    Marcelo Fiore, Discrete generalised polynomial functors, 2012, Slides from talk given at ICALP 2012, http://www.cl.cam.ac.uk/ mpf23/talks/ICALP2012.pdf

    2012

  10. [18]

    1, 1–76, http://dx.doi.org/10.1017/S0004972700044828 doi:10.1017/S0004972700044828

    Peter Freyd, Aspects of topoi, Bulletin of the Australian Mathematical Society 7 (1972), no. 1, 1–76, http://dx.doi.org/10.1017/S0004972700044828 doi:10.1017/S0004972700044828

    1972 doi

  11. [19]

    Richard Garner, Combinatorial structure of type dependency, Journal of Pure and Applied Algebra 219 (2015), no. 6, 1885--1914, http://arxiv.org/abs/1402.6799 arXiv:1402.6799 , http://dx.doi.org/10.1016/j.jpaa.2014.07.015 doi:10.1016/j.jpaa.2014.07.015 , https://www.sciencedire...

    2015 arXiv

  12. [20]

    221, Springer-Verlag, Berlin-New York, 1971, http://dx.doi.org/10.1007/BFb0059396 doi:10.1007/BFb0059396

    Peter Gabriel and Friedrich Ulmer, Lokal pr\" a sentierbare K ategorien , Lecture Notes in Mathematics, vol. 221, Springer-Verlag, Berlin-New York, 1971, http://dx.doi.org/10.1007/BFb0059396 doi:10.1007/BFb0059396

    1971 doi

  13. [21]

    Sci., vol

    Martin Hofmann, On the interpretation of type theory in locally C artesian closed categories , Computer science logic ( K azimierz, 1994), Lecture Notes in Comput. Sci., vol. 933, Springer, Berlin, 1995, pp. 427--441, http://dx.doi.org/10.1007/BFb0022273 doi:10.1007/BFb0022273

    1994 doi

  14. [22]

    Newton Inst., vol

    , Syntax and semantics of dependent types, Semantics and logics of computation ( C ambridge, 1995), Publ. Newton Inst., vol. 14, Cambridge Univ. Press, Cambridge, 1997, pp. 79--130, http://dx.doi.org/10.1017/CBO9780511526619.004 doi:10.1017/CBO9780511526619.004

    1995 doi

  15. [23]

    Martin E

    J. Martin E. Hyland and Andrew M. Pitts, The theory of constructions: categorical semantics and topos-theoretic models, Categories in computer science and logic ( B oulder, CO , 1987), Contemp. Math., vol. 92, Amer. Math. Soc., Providence, RI, 1989, pp. 137--199, http://dx.doi...

    1987 doi

  16. [24]

    Bart Jacobs, Comprehension categories and the semantics of type dependency, Theoret. Comput. Sci. 107 (1993), no. 2, 169--207, http://dx.doi.org/10.1016/0304-3975(93)90169-T doi:10.1016/0304-3975(93)90169-T

    1993 doi

  17. [25]

    Johnstone, Sketches of an elephant: a topos theory compendium, Oxford Logic Guides, vol

    Peter T. Johnstone, Sketches of an elephant: a topos theory compendium, Oxford Logic Guides, vol. 43,44, The Clarendon Press Oxford University Press, New York, 2002

    2002

  18. [26]

    Andre Joyal, Notes on clans and tribes, Unpublished notes, 2017, http://arxiv.org/abs/1710.10238 arXiv:1710.10238 , https://arxiv.org/abs/1710.10238

    2017 arXiv

  19. [27]

    G. M. Kelly, On the essentially-algebraic theory generated by a sketch, Bull. Austral. Math. Soc. 26 (1982), no. 1, 45--56, http://dx.doi.org/10.1017/S0004972700005591 doi:10.1017/S0004972700005591

    1982 doi

  20. [28]

    Pure Appl

    Krzysztof Kapulkin and Peter LeFanu Lumsdaine, Homotopical inverse diagrams in categories with attributes, J. Pure Appl. Algebra 225 (2021), no. 4, Paper No. 106563, 44, http://arxiv.org/abs/1808.01816 arXiv:1808.01816 , http://dx.doi.org/10.1016/j.jpaa.2020.106563 doi:10.1016...

    2021

  21. [29]

    12, 107126, http://dx.doi.org/10.1016/j.jpaa.2022.107126 doi:10.1016/j.jpaa.2022.107126 , https://www.sciencedirect.com/science/article/pii/S0022404922001220

    Fernando Lucatelli Nunes and Lurdes Sousa, On lax epimorphisms and the associated factorization, Journal of Pure and Applied Algebra 226 (2022), no. 12, 107126, http://dx.doi.org/10.1016/j.jpaa.2022.107126 doi:10.1016/j.jpaa.2022.107126 , https://www.sciencedirect.com/science/...

    2022

  22. [30]

    Michael Makkai, First order logic with dependent sorts, with applications to category theory, Unpublished note, 1995, http://www.math.mcgill.ca/makkai/folds/foldsinpdf/FOLDS.pdf

    1995

  23. [31]

    Lecture Notes, vol

    Per Martin-L \"o f, Intuitionistic type theory, Studies in Proof Theory. Lecture Notes, vol. 1, Bibliopolis, Naples, 1984

    1984

  24. [32]

    Structures Comput

    Eugenio Moggi, A category-theoretic account of program modules, Math. Structures Comput. Sci. 1 (1991), no. 1, 103--139, http://dx.doi.org/10.1017/S0960129500000074 doi:10.1017/S0960129500000074

    1991 doi

  25. [33]

    thesis, Carnegie Mellon University, 2018, http://arxiv.org/abs/2103.06155 arXiv:2103.06155 , https://arxiv.org/abs/2103.06155

    Clive Newstead, Algebraic models of dependent type theory, Ph.D. thesis, Carnegie Mellon University, 2018, http://arxiv.org/abs/2103.06155 arXiv:2103.06155 , https://arxiv.org/abs/2103.06155

    2018 arXiv

  26. [34]

    Pitts, Categorical logic, Handbook of Logic in Computer Science, vol

    Andrew M. Pitts, Categorical logic, Handbook of Logic in Computer Science, vol. 5, Oxford Univ. Press, New York, 2000, pp. 39--128, http://dx.doi.org/10.1093/oso/9780198537816.001.0001 doi:10.1093/oso/9780198537816.001.0001

    2000

  27. [35]

    Report NS-98-7, Basic Research in Computer Science, Aarhus, August 1998, https://www.brics.dk/NS/98/7/index.html

    John Power, 2-categories, Tech. Report NS-98-7, Basic Research in Computer Science, Aarhus, August 1998, https://www.brics.dk/NS/98/7/index.html

    1998

  28. [36]

    Vickers, Partial horn logic and C artesian categories , Ann

    Erik Palmgren and Steven J. Vickers, Partial horn logic and C artesian categories , Ann. Pure Appl. Logic 145 (2007), no. 3, 314--353, http://dx.doi.org/10.1016/j.apal.2006.10.001 doi:10.1016/j.apal.2006.10.001

    2007 doi

  29. [37]

    Thomas Streicher, Semantics of type theory, Progress in Theoretical Computer Science, Birkh\"a user, Boston, MA, 1991, http://dx.doi.org/10.1007/978-1-4612-0433-6 doi:10.1007/978-1-4612-0433-6

    1991 doi

  30. [38]

    thesis, Université Paris Diderot, 2021, http://arxiv.org/abs/2110.02804 arXiv:2110.02804 , http://dx.doi.org/10.48550/arXiv.2110.02804 doi:10.48550/arXiv.2110.02804

    Chaitanya Leena Subramaniam, From dependent type theory to higher algebraic structures, Ph.D. thesis, Université Paris Diderot, 2021, http://arxiv.org/abs/2110.02804 arXiv:2110.02804 , http://dx.doi.org/10.48550/arXiv.2110.02804 doi:10.48550/arXiv.2110.02804

    2021 doi arXiv

  31. [39]

    thesis, University of Cambridge, 1986, https://www.paultaylor.eu/domains/recdic.pdf

    Paul Taylor, Recursive domains, indexed category theory and polymorphism, Ph.D. thesis, University of Cambridge, 1986, https://www.paultaylor.eu/domains/recdic.pdf

    1986

  32. [40]

    59, Cambridge University Press, Cambridge, 1999, https://www.paultaylor.eu/ pt/prafm/

    , Practical foundations of mathematics, Cambridge Studies in Advanced Mathematics, vol. 59, Cambridge University Press, Cambridge, 1999, https://www.paultaylor.eu/ pt/prafm/

    1999

  33. [41]

    Taichi Uemura, A general framework for the semantics of type theory, Math. Struct. Comput. Sci. 33 (2023), no. 3, 134--179, http://arxiv.org/abs/1904.04097 arXiv:1904.04097 , http://dx.doi.org/10.1017/S0960129523000208 doi:10.1017/S0960129523000208 , https://doi.org/10.1017/s0...

    2023 arXiv

  34. [42]

    Benno van den Berg and Richard Garner, Topological and simplicial models of identity types, ACM Trans. Comput. Log. 13 (2012), no. 1, Art. 3, 44, http://arxiv.org/abs/1007.4638v1 arXiv:1007.4638v1 , http://dx.doi.org/10.1145/2071368.2071371 doi:10.1145/2071368.2071371

    2012 arXiv

  35. [43]

    Vladimir Voevodsky, B-systems, Unpublished manuscript, revision of arXiv:1410.5389 https://arxiv.org/abs/1410.5389, 2016, https://www.math.ias.edu/Voevodsky/files/files-annotated/Dropbox/Unfinished_papers/Type_systems/Notes_on_Type_Systems/Bsystems/B_systems_current.pdf

    2016 arXiv

  36. [44]

    Math., vol

    , Subsystems and regular quotients of C -systems , A panorama of mathematics: pure and applied, Contemp. Math., vol. 658, Amer. Math. Soc., Providence, RI, 2016, pp. 127--137, http://arxiv.org/abs/1406.7413 arXiv:1406.7413 , http://dx.doi.org/10.1090/conm/658/13124 doi:10.1090...

    2016 arXiv

  37. [45]

    6, 107283, http://arxiv.org/abs/1602.00352 arXiv:1602.00352 , http://dx.doi.org/10.1016/j.jpaa.2022.107283 doi:10.1016/j.jpaa.2022.107283

    , C -system of a module over a Jf -relative monad , Journal of Pure and Applied Algebra 227 (2023), no. 6, 107283, http://arxiv.org/abs/1602.00352 arXiv:1602.00352 , http://dx.doi.org/10.1016/j.jpaa.2022.107283 doi:10.1016/j.jpaa.2022.107283

    2023 arXiv

Pith tools

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