Owen Lynch 2025 2 28 https://forest.topos.site/ocl-006Y/ https://forest.topos.site/ocl-006Y /ocl-006Y/ Abstraction without semantic expansion Notes on the applications of two-level type theory Owen Lynch 2025 2 28 https://forest.topos.site/ocl-006Z/ https://forest.topos.site/ocl-006Z /ocl-006Z/ Introduction Owen Lynch 2025 5 12 https://forest.topos.site/ocl-00ER/ https://forest.topos.site/ocl-00ER /ocl-00ER/ Warnings This is work-in-progress; I am fairly sure most of what I have written is correct, but the sections on the semantics of EMTT need work I have recently discovered that a large amount of EMTT that I believed was original is in fact a rediscovery of the work in András Kovács's thesis. On one hand, this is good news, because it means that I can draw upon a much larger body of work than I previously knew about, and some of my “future work” has in fact already been done. On the other hand, this will require a substantial reworking of this paper to be up-to-date with the more recent literature. Owen Lynch 2025 2 28 https://forest.topos.site/ocl-0078/ https://forest.topos.site/ocl-0078 /ocl-0078/ The meaning of “abstraction without semantic expansion” Category theory has been used as a semantic framework for programming languages, going at least back to Reference , but possibly earlier (see the nlab article on computational trilogy). The central idea of this is that certain classes of category support “internal languages” that can be used to compactly and efficiently reason about morphisms in that category. Most classically, the internal language of a cartesian closed category is simply typed lambda calculus. Often working in this internal language is far more efficient and convenient than working “externally” in a combinator style. For instance, building up morphisms in a cartesian closed category by just directly using the cartesian and closed structures (e.g., projections, evaluations, etc.) can be vastly more difficult and unintuitive than working with simply typed lambda calculus. In certain situations, the internal language of the type of category that one cares about is rich enough to support good abstraction features. For instance, in simply typed lambda calculus, one can produce “higher-order” functions like map : (a -> b) -> List a -> List b which encapsulate a general pattern (iterating over a list to produce a new list) and allow the “inner” part of the iteration to be instantiated to many different functions by the user. However, in many situations this is not the case. For instance, if one is working in the category of finite-dimensional smooth manifolds (or an appropriate relaxation, like some appropriate subcategory of the opposite category of -algebras, as discussed in Reference or Reference ), as the category of smooth manifolds has products, simple type theory without function types is an appropriate internal language. In fact, even dependent type theory (again, without function types) could be an appropriate internal language, which would allow the tangent bundle for a space to be expressed as . But the disallowal of function types is important, because one might want to, for instance, provide a meta-linguistic feature where for any type , any derivation of the judgment can be plugged into an ordinary differential equation solver. Various features of a language (function types, but also if statements) can complicate this (by making types non-finite-dimensional, or destroying differentiability), so it is desirable to control their usage if the language is being used to write down vector fields. And even in the case of simply typed lambda calculus, while one may abstract over functions, one cannot abstract over types. One approach to this problem is to move to dependent type theory with a universe (ignoring inconsistency from size issues for the time being). However, that changes the semantics of the language; we now must carry around types at runtime. Instead, the standard solution is something like System F, which is not the internal language of any one single category (rather, it can be seen as the internal language of a bundle of categories of types fibered over a category of kinds). We propose that in general in the situation where the internal language of a class of categories is not rich enough for abstraction, the way to recover facilities for abstraction without compromising certain semantical properties is to move to a two-level type theory, where certain types used for abstraction only exist at “compile time”. This is the meaning of the slogan “abstraction without semantic expansion”. “Abstraction without semantic expansion” is by no means a novel idea. In programming languages, there is a principle of a zero-cost abstraction, which is an abstraction that can be “compiled away” to achieve the same performance as code which did not use the abstraction and instead just manually repeated the same pattern with small variations in various places. Owen Lynch 2025 3 22 https://forest.topos.site/ocl-00C1/ https://forest.topos.site/ocl-00C1 /ocl-00C1/ Function traits in Rust example Rust does not have function types. Instead, it has a Fn trait, which could be used like B>(xs: Vec) -> Vec { let out: Vec = Vec::new(); for x in xs.iter() { out.push(f(x)); } out }]]> When map is used, Rust is able to at compile time see which implementation of the Fn trait will be used, and this enables the code to be compiled to = Vec::new(); for x in xs.iter() { out.push(x + 1); } out]]> which does not require the function |x| x + 1 to exist at runtime. Another instantiation of abstraction without semantic expansion is the use of “embedded domain specific languages” in functional programming. The idea embedded domain specific language is to implement a domain specific language as a library in a more powerful language, essentially using the more powerful language to manipulate the syntax of the domain specific language. The advantage of an embedded domain specific language is that the host language can be used for metaprogramming. One perspective on two-level type theory is that it is a way of designing a host language and embedded language simultaneously, so that the compiler may be aware of more features in the embedded language than would be possible in general. 2025 2 28 https://forest.topos.site/ocl-007A/ https://forest.topos.site/ocl-007A /ocl-007A/ Overview In this paper, we present a two-level type theory called EMTT (Element Model Type Theory) which follows the principle of “abstraction without semantic expansion” in allowing the user to abstract over finite limit theories without adding function or universe types to the finite limit theories themselves. Specifically, the outer-level types in EMTT correspond to finite limit theories, and their outer-level terms are the models of those finite limit theories. The inner-level types are types internal to a finite limit theory, and the inner-level terms are the elements of those types. EMTT is an interesting type theory with a variety of applications. First of all, EMTT can be used for equational reasoning in universal algebra, using e-graphs in conversion checking to do a limited form of derivation reconstruction for extensional equalities. EMTT can also be used to construct finitely-presented models of theories in a compositional manner, including the theories used in CatColab. However, we are also interested in EMTT as a stepping stone in a larger research program of investigating how two-level type theory may be used to realize abstraction without semantic expansion. Thus, our exposition of EMTT emphasizes how choices we made at various points in the design could be made in different ways, and the resulting type theory would likely be similarly interesting. In other words, we aim to make type theory feel less like an ad-hoc collection of rules, and more like a “garden of forking paths”. The paper is structured in the following way. We begin in § with a review of categorical algebra. This is because essential to our exposition of the “garden of forking paths” is the concept of an -theory, the origins of which are found in categorical algebra. We then move on in § to an exposition of type theory from the -theory point of view. Specifically, we treat the 3-theories of simple type theory, dependent type theory, and two-level type theory. The 3-theory of two-level type theory is the most interesting 3-theory for us, and this is the place where the “garden of forking paths” is most apparent, as constructs from regular dependent type theory may be imported into the two-level setting in a multitude of ways. § is the place in which we discuss EMTT, which is the main original contribution of this paper. The impatient reader may wish to skip to § , which introduces EMTT by code examples. We then give the rules § , semantics § , and some implementation details § , § . Finally, we have an extensive “future work” section in § . EMTT is just the beginning of our studies of two-level type theory, and we have a number of projects which we plan to turn our attention to next. This current paper might be best understood as a “work in progress” report, which was necessary to understand the prototype EMTT implementation, but as it stands the EMTT implementation is more of an interesting toy and not directly applicable to many of the problems that it aims to solve. For instance, the only type one can write down in the empty context is the unit type; we have joked that EMTT should be pronounced “empty-tee”. § sketches out plans for how to build on top of EMTT for interesting applications. Owen Lynch 2025 3 24 https://forest.topos.site/ocl-00CD/ https://forest.topos.site/ocl-00CD /ocl-00CD/ Related work In some ways, it might be easier to write an “unrelated work” section, as this paper is explicitly intended to tie together a wide variety of research themes. However, there is a core to this paper, which is the development of a type theory for finite limit theories, and accordingly in this section we will focus more narrowly on work related to to this type theory. Element Model Type Theory would not exist if it were not for the year and a half that the main author spent working on GATlab Reference . In the introduction to the GATlab paper, we endeavored to give a reasonably broad overview of the history of algebraic theories and their software implementations. However, there were some developments which we either missed or were not around at the time of writing that paper. One such development is Kammar and Wright's semantic reflection library, with accompanying extended abstract Reference . This works with algebraic theories as a deeply-embedded DSL within Idris 2, by extending the Idris 2 elaborator. This is an approach to two-level type theory which takes as the outer level a full dependent type theory. This is quite convenient, because one can do many things with full dependent type theory that one cannot do in EMTT. However, the outer level types in EMTT can all be interpreted as finite limit theories, which is not true of Idris types. What EMTT gives up for this is the ability to play nicely with the wide variety of other mathematics formalized in Idris, and we imagine that elaborator reflection is significantly easier to implement than writing an elaborator from scratch. Related to the above is the Frex project, which integrates reasoning over algebraic theories into dependently-typed programming languages. In contrast to EMTT, frex emphasizes the development of normal-form computations for specific algebraic theories, and like the semantic-reflection library frex integrates into pre-existing programming languages rather than using a programming language written from scratch. This supports a much more predictable style of programming with algebraic theories, where equations like are automatically handled without the user needing to explicitly cite axioms as in EMTT. For some intended applications of EMTT (for instance, as the backing type theory of CatColab), it is not desirable to integrate with a full dependent programming language like Idris or Agda. However, taking a normal-form approach to rewriting rather than an e-graph approach is attractive for computer algebra applications, and so we hope to integrate more with the ideas behind frex in the future. Another software which takes very seriously the concept of 2-theories is the CAP project, (Categories, Algorithms, and Programming) which is a quite advanced computer algebra system whose core is given by 2-adjunctions between various 2-categories that allow constructions to be done in great generality. One contrast between EMTT and CAP is that when CAP considers free (rings/modules/etc.), it takes as its set of variables a collection of strings. In contrast, EMTT's use of dependent records as presentations for free algebraic structure naturally supports namespacing, like a.x, a.y, b.q.y, which we consider to be essential for compositional systems theory. There are likely other projects that we have missed; we encourage the reader to send references and we will update this section accordingly. Owen Lynch 2025 2 28 https://forest.topos.site/ocl-0070/ https://forest.topos.site/ocl-0070 /ocl-0070/ A review of categorical algebra In § , we give a review of type theory from the perspective of -theories. In this section, we give a brief overview of the history of the idea of -theories, focusing on a few specific examples. Owen Lynch 2025 2 28 https://forest.topos.site/ocl-007B/ https://forest.topos.site/ocl-007B /ocl-007B/ Finite product theories For an overview of the history of finite product theories, we refer the reader to section 1.2 of Reference . The modern (starting with Reference ) treatment of finite product theories starts with the following definition. Owen Lynch 2025 3 22 https://forest.topos.site/ocl-00C2/ https://forest.topos.site/ocl-00C2 /ocl-00C2/ Finite Product Theory definition An finite product theory is a category with finite products and an identity-on-objects, finite-product-preserving functor . The category of finite product theories is given by the subcategory of on the identity-on-objects functors. This definition is equivalent to the more common definition (an finite product theory is a finite product category whose objects are freely generated by a single object), but is slightly more precise about what “objects being freely generated” means. That is, is the free finite product category on a single object, so a category with a product-preserving, identity-on-objects functor from can be said “to have its objects freely generated by a single object”. Owen Lynch 2025 3 22 https://forest.topos.site/ocl-00C4/ https://forest.topos.site/ocl-00C4 /ocl-00C4/ Model of an finite product theory definition A model of an finite product theory is a finite-product-preserving functor . Let be the category of models of , with natural transformations as morphisms. It is somewhat tricky to write down finite product theories directly without some means of “presenting” them, but at least the theory of monoids is not too hard to describe. First, we review the definition of a monoid. Owen Lynch 2025 3 22 https://forest.topos.site/ocl-00C5/ https://forest.topos.site/ocl-00C5 /ocl-00C5/ Monoid definition A monoid is a set equipped with a function and an element , such that For all , For all , Owen Lynch 2025 3 22 https://forest.topos.site/ocl-00C3/ https://forest.topos.site/ocl-00C3 /ocl-00C3/ The finite product theory of monoids example Let be the functor sending a set to the set of lists with elements taken from . Then is a monad on , so we may form its Kleisli category , and let be the full subcategory of on finite sets. By general arguments, has finite coproducts, so thus is a finite product category with an identity-on-objects functor from , e.g. an finite product theory. This category has two important morphisms. One is the morphism that sends to , and the other is the morphism that sends to . These morphisms represent “multiplication” and “the identity”. Specifically, in a model , then we have: And then one can check that associativity and unitality are satisfied using the definitions of product and composition in . A signature feature of Lawvere's development of finite product theories is a pervasive use of adjoint functors. For instance, the following. Owen Lynch 2025 3 23 https://forest.topos.site/ocl-00C6/ https://forest.topos.site/ocl-00C6 /ocl-00C6/ The free-forgetful adjunction for a finite product theory definition Given any finite product theory , there is always an adjunction udmj30}{} \newcommand\yo{\!\text{\usefont{U}{min}{m}{n}\symbol{'207}}\!} \DeclareUnicodeCharacter{3088}{\yo} \usepackage{tikz, tikz-cd, mathtools, amssymb, stmaryrd,xcolor} \usetikzlibrary{matrix,arrows} \usetikzlibrary{backgrounds,fit,positioning,calc,shapes} \usetikzlibrary{decorations.pathreplacing} \usetikzlibrary{decorations.pathmorphing} \usetikzlibrary{decorations.markings} % `tikz-cd` is necessary to draw commutative diagrams. \RequirePackage{tikz-cd} % `amssymb` is necessary for `\lrcorner` and `\ulcorner`. \RequirePackage{amssymb} % `calc` is necessary to draw curved arrows. \usetikzlibrary{calc} % `pathmorphing` is necessary to draw squiggly arrows. \usetikzlibrary{decorations.pathmorphing} % `spath3` is necessary to draw shortened edges. \usetikzlibrary{spath3} % A TikZ style for curved arrows of a fixed height, due to AndréC. \tikzset{curve/.style={settings={#1},to path={(\tikztostart) .. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) .. (\tikztotarget)\tikztonodes}}, settings/.code={\tikzset{quiver/.cd,#1} \def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}}, quiver/.cd,pos/.initial=0.35,height/.initial=0} % A TikZ style for shortening paths without the poor behaviour of `shorten <' and `shorten >'. \tikzset{between/.style n args={2}{/tikz/spath/at end path construction={ \tikzset{spath/split at keep middle={current}{#1}{#2}} }}} % TikZ arrowhead/tail styles. \tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}} \tikzset{2tail/.code={\pgfsetarrowsstart{Implies[reversed]}}} \tikzset{2tail reversed/.code={\pgfsetarrowsstart{Implies}}} % TikZ arrow styles. \tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}} \newcommand{\triplecolon}{% \mathrel{\vbox{\baselineskip=2pt \hbox{.}\hbox{.}\hbox{.}}}% } \DeclareUnicodeCharacter{2AF6}{\triplecolon} \usepackage{mathpartir} ]]> between the category of models of and , where is induced by precomposition with and the equivalence between and the category of finite-product-preserving functors .More concretely, .The left adjoint may be shown to exist by either left Kan extension or the adjoint functor theorem (after proving that preserves limits).Intuitively, the left adjoint sends a set to the “free model of with generators taken from ”. And it turns out that this adjunction is always monadic, so that the category of models for is equivalent to the category of algebras for the monad . We can go the other way too, which was hinted at in example . If we start with a finitary monad (finitary meaning that it preserves filtered colimits), then the category of algebras for is equivalent to the category of models of the finite product theory given by restricted to finite sets. But how are we to define a finite product theory without starting from an explicit description of the monad like in example ? The answer is more adjunctions. Owen Lynch 2025 3 23 https://forest.topos.site/ocl-00C7/ https://forest.topos.site/ocl-00C7 /ocl-00C7/ Free finite product theory on a signature definition A signature consists of a collection of sets for each natural number . We call the operations of arity . The category of signatures is given by . Then there is a forgetful functor from to , which sends a finite product theory to . This forgetful functor has a left adjoint , and we call the free finite product theory on a signature . Owen Lynch 2025 3 23 https://forest.topos.site/ocl-00C8/ https://forest.topos.site/ocl-00C8 /ocl-00C8/ The signature for monoids example The signature for monoids is given by , , and for . The free finite product theory on this signature may be called the “theory of a pointed magma”; models for this are given by sets with a binary operation and a nullary operation , but no laws. To produce a general finite product theory, we then ask for certain pairs of parallel morphisms in to be identified; this allows us to impose laws like associativity and unitality on our finite product theories. Owen Lynch 2025 3 23 https://forest.topos.site/ocl-00C9/ https://forest.topos.site/ocl-00C9 /ocl-00C9/ Presented finite product theory definition A finite product theory presentation consists of a signature , along with a selection of equated pairs of morphisms. As any finite product theory induces an algebra for the monad on , given , we may ask whether . Thus, there is a forgetful functor from finite product theories to finite product theory presentations, which sends to with the above choice of equated pairs. The left adjoint to the forgetful functor sends a finite product theory presentation to the finite product theory that it presents. Finite product theories may be considered “paradigmatic” for categorical logic, in that the selection of results that we have presented here will show up in analogous form for most other subjects in categorical algebra. Specifically: Theories may be identified with certain categories, and models of those theories are functors out of those categories into some concrete category like There is an equivalent presentation of theories which involves monads and their algebras. This equivalent presentation is induced by the free-forgetful adjunction between models of a theory and sets. Theories may be presented via generators and relations. Finally, we will note that for simplicity we have only treated the “single-sorted” case of finite product theories. In general, one can replace with for a set of “sorts” in the definition of finite product theory, and then the rest of the development is analogous. 2025 2 28 https://forest.topos.site/ocl-007C/ https://forest.topos.site/ocl-007C /ocl-007C/ Finite limit theories There are many algebraic structures which do not arise as the models of any finite product theory. Perhaps the most famous one of these is categories. Roughly speaking is because in a category, when one composes morphisms one must first check that the codomain and domain match up, and finite product theories do not provide an affordance for this.Finit limit theories are similar to finite product theories, except that we require that the theory has all finite limits instead of just finite products, and additionally that models (which are functors out of the theory into ) preserve those limits.This allows us to express composition in a category in the following way.Let be the set of objects in the category, and be the set of morphisms, with the domain and codomain functions respectively. Then composition is given by the function in the following diagram udmj30}{} \newcommand\yo{\!\text{\usefont{U}{min}{m}{n}\symbol{'207}}\!} \DeclareUnicodeCharacter{3088}{\yo} \usepackage{tikz, tikz-cd, mathtools, amssymb, stmaryrd,xcolor} \usetikzlibrary{matrix,arrows} \usetikzlibrary{backgrounds,fit,positioning,calc,shapes} \usetikzlibrary{decorations.pathreplacing} \usetikzlibrary{decorations.pathmorphing} \usetikzlibrary{decorations.markings} % `tikz-cd` is necessary to draw commutative diagrams. \RequirePackage{tikz-cd} % `amssymb` is necessary for `\lrcorner` and `\ulcorner`. \RequirePackage{amssymb} % `calc` is necessary to draw curved arrows. \usetikzlibrary{calc} % `pathmorphing` is necessary to draw squiggly arrows. \usetikzlibrary{decorations.pathmorphing} % `spath3` is necessary to draw shortened edges. \usetikzlibrary{spath3} % A TikZ style for curved arrows of a fixed height, due to AndréC. \tikzset{curve/.style={settings={#1},to path={(\tikztostart) .. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) .. (\tikztotarget)\tikztonodes}}, settings/.code={\tikzset{quiver/.cd,#1} \def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}}, quiver/.cd,pos/.initial=0.35,height/.initial=0} % A TikZ style for shortening paths without the poor behaviour of `shorten <' and `shorten >'. \tikzset{between/.style n args={2}{/tikz/spath/at end path construction={ \tikzset{spath/split at keep middle={current}{#1}{#2}} }}} % TikZ arrowhead/tail styles. \tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}} \tikzset{2tail/.code={\pgfsetarrowsstart{Implies[reversed]}}} \tikzset{2tail reversed/.code={\pgfsetarrowsstart{Implies}}} % TikZ arrow styles. \tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}} \newcommand{\triplecolon}{% \mathrel{\vbox{\baselineskip=2pt \hbox{.}\hbox{.}\hbox{.}}}% } \DeclareUnicodeCharacter{2AF6}{\triplecolon} \usepackage{mathpartir} ]]> where is the set of pairs of morphisms such that .Finite limit theories are significantly trickier to deal with than finite product theories, because general finite limits generate a much larger class of objects than products. We will discuss finite limit theories in greater detail in § under the heading of “sketches”.For now, we will simply say that a finite limit theory is a category that has all finite limits; we refer the reader to Reference and Reference for more details. Owen Lynch 2025 2 28 https://forest.topos.site/ocl-007D/ https://forest.topos.site/ocl-007D /ocl-007D/ Doctrines (2-theories) Both § and § dealt with what we will now call 1-theories, which are theories that have a category of models. However, there are some “theories” which naturally have a 2-category of models. For instance, the “theory of monoidal categories” naturally has a 2-category of models, where the objects are monoidal categories, the morphisms are (some choice of strict/pseudo/lax/colax) monoidal functors, and the 2-cells are natural transformations. Classically, such a theory has been called a doctrine. Early references on doctrines include Reference and Reference . For uniformity, we will refer to doctrines as 2-theories, following Shulman Reference . In fact, the 2-category of categories with finite products, finite product preserving functors, and natural transformations can itself be thought of as the 2-category of models of some “2-theory of finite products”. This leads to our real definition of 1-theory; a 1-theory is a model of a 2-theory! This likewise suggests that a 2-theory should be thought of as some model of a 3-theory. However, this leads to an infinite regress. In practice, we will fix some to be our “highest level”, define -theories concretely, and then not worry about what the precise structure of the -theory that we have implicitly defined is. So for instance in § , we will talk about different 3-theories without ever defining what a 3-theory is; informally a 3-theory is a “paradigm of 2-theories”. If we take this down a level, and say that “informally, a 2-theory is a paradigm of 1-theories”, then we can think of § and § as defining two particular 2-theories. But it is often profitable to “work a level higher”. In this section, we will briefly touch upon some historical and modern formal notions of 2-theory (each of which may be thought of as a 3-theory). Owen Lynch 2025 3 23 https://forest.topos.site/ocl-00CA/ https://forest.topos.site/ocl-00CA /ocl-00CA/ 2-theories as 2-monads on In Reference , Lawvere defines an equational doctrine to be precisely what a modern category theorist would call a 2-monad on . An exposition of the theory of 2-monads is beyond the scope of this work, but the interested reader is encouraged to refer to Reference .In this section, we simply go through an example of the 2-theory for monoidal categories.Owen Lynch2025323https://forest.topos.site/ocl-00CB/https://forest.topos.site/ocl-00CB/ocl-00CB/The free monoidal category on a categorydefinitionGiven a category , let be the following monoidal category.The objects of are lists of objects in , that is elements of . The morphisms of are likewise lists of morphismsin , that is elements of . The domain and codomain of such a list of morphisms is given by , so if . The monoidal structure on is given by list concatenation.I claim that is a monad on the 1-category . In general, this is not the same as a 2-monad on the 2-category , but an endo-2-functor of that is a 1-monad is also a 2-monad.The unit for , , is given by singleton lists:Likewise, the multiplication for , is given by list flattening:It then not hard to show that strict monoidal categories are algebras of the 2-monad in definition . Moreover, strict monoidal functors are algebra morphisms, and thus there is a 2-category of strict monoidal categories, strict monoidal functors, and natural transformations.One of the nice things about 2-monads is that we are not limited to the strict algebras. Specifically, we may define a pseudo-algebra to be a functor where the commutative squares in the definition of algebra commute only up to isomorphism, such as udmj30}{} \newcommand\yo{\!\text{\usefont{U}{min}{m}{n}\symbol{'207}}\!} \DeclareUnicodeCharacter{3088}{\yo} \usepackage{tikz, tikz-cd, mathtools, amssymb, stmaryrd,xcolor} \usetikzlibrary{matrix,arrows} \usetikzlibrary{backgrounds,fit,positioning,calc,shapes} \usetikzlibrary{decorations.pathreplacing} \usetikzlibrary{decorations.pathmorphing} \usetikzlibrary{decorations.markings} % `tikz-cd` is necessary to draw commutative diagrams. \RequirePackage{tikz-cd} % `amssymb` is necessary for `\lrcorner` and `\ulcorner`. \RequirePackage{amssymb} % `calc` is necessary to draw curved arrows. \usetikzlibrary{calc} % `pathmorphing` is necessary to draw squiggly arrows. \usetikzlibrary{decorations.pathmorphing} % `spath3` is necessary to draw shortened edges. \usetikzlibrary{spath3} % A TikZ style for curved arrows of a fixed height, due to AndréC. \tikzset{curve/.style={settings={#1},to path={(\tikztostart) .. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) .. (\tikztotarget)\tikztonodes}}, settings/.code={\tikzset{quiver/.cd,#1} \def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}}, quiver/.cd,pos/.initial=0.35,height/.initial=0} % A TikZ style for shortening paths without the poor behaviour of `shorten <' and `shorten >'. \tikzset{between/.style n args={2}{/tikz/spath/at end path construction={ \tikzset{spath/split at keep middle={current}{#1}{#2}} }}} % TikZ arrowhead/tail styles. \tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}} \tikzset{2tail/.code={\pgfsetarrowsstart{Implies[reversed]}}} \tikzset{2tail reversed/.code={\pgfsetarrowsstart{Implies}}} % TikZ arrow styles. \tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}} \newcommand{\triplecolon}{% \mathrel{\vbox{\baselineskip=2pt \hbox{.}\hbox{.}\hbox{.}}}% } \DeclareUnicodeCharacter{2AF6}{\triplecolon} \usepackage{mathpartir} ]]> (and those isomorphisms satisfy coherences).Considering pseudoalgebras for gives us a 2-category of weak monoidal categories, weak monoidal functors, and natural transformations. Owen Lynch 2025 3 23 https://forest.topos.site/ocl-00CC/ https://forest.topos.site/ocl-00CC /ocl-00CC/ 2-theories as cartesian double theories In the case of finite product theories, there is a correspondence between finite product theories and finitary monads on . A natural question to ask is whether there is a presentation of 2-theories which is analogous to finite product theories rather than monads. In Reference , Lambert and Patterson give a notion of “cartesian double theory” which brings us closer to answering this question in the affirmative. It is not yet known the precise relationship between 2-monads and cartesian double theories, but many of the natural 2-theories one would like to consider appear as both 2-monads and as cartesian double theories, so it seems likely that some formal relationship could hold. Note that in the 1-theory case, the correspondence is between monads on and finite product theories generated by a single object, so one might expect that the relationship would be between 2-monads on and cartesian double theories generated by a single object and single proarrow, rather than a full correspondence. Similar to this approach is the “algebraic 2-theories” of Reference , which uses 2-categories instead of double categories. We will not discuss cartesian double theories at length here. We will note, however, that cartesian double theories form the backbone of CatColab, and one of the intended applications of EMTT is to provide the theoretical background for compositional notebooks in CatColab, so at some point we may develop a closer connection between EMTT and cartesian double theories. Owen Lynch 2025 2 28 https://forest.topos.site/ocl-0075/ https://forest.topos.site/ocl-0075 /ocl-0075/ Type theory as organized into 3-theories In this section, we give an overview of type theory from the -theory point of view. Here, we note a couple things before we start. First of all, this overview is neither comprehensive, pedagogical, or original. Rather, it is intended to organize subject matter that the reader has prior exposure with into some kind of semi-unified whole which may be discussed later on in a condensed manner. The reader without previous exposure to type theory but with exposure to category theory is encouraged to read Reference before reading this. Secondly, while this overview has some pretension at unification, the reader should know that a more unified and precise account of a wider variety of type theories may be found in Reference . The only thing that the present account has to recommend it over this more general story is that we are more narrowly focused on getting to two-level type theory, and thus pay more attention to the exposition of two-level type theory in particular. Finally, and this is somewhat of a technical point which is likely only to be understood after § , what we call two-level type theory should really be known as something like “dependent-dependent type theory”, to emphasize that the type theory is dependent at each level. One might also posit 3-theories of simple-simple type theory (examples would include System F (the two levels are kinds and types) or first-order logic (the two levels are types and propositions)), or dependent-simple type theory (examples would perhaps include the closure-free type theory of Reference , we are less sure of this), and these also deserve the name of two-level type theory. We do not treat these 3-theories here, but they are certainly equally worthy of study. Owen Lynch 2025 2 28 https://forest.topos.site/ocl-0071/ https://forest.topos.site/ocl-0071 /ocl-0071/ The 3-theory of simple type theories () In this section, we discuss the syntax and semantics of the 3-theory of simple type theories, which we refer to as . The substance of this section is mostly derived from Chapter 2 of Reference , though we treat the type theory in less detail and we take more explicit the perspective of Reference . Where we have diverged from Shulman, it is for the purpose of establishing notation and conceptualization that harmonizes better with the following sections. Owen Lynch 2025 2 28 https://forest.topos.site/ocl-007M/ https://forest.topos.site/ocl-007M /ocl-007M/ Judgment structure of In this section, we review the judgment structure of , which might be thought of as the “syntactic 3-theory” of . It is typical when presenting a type theory to begin with so-called “judgment formers”. These might be given in the following way. Owen Lynch 2025 3 11 https://forest.topos.site/ocl-009C/ https://forest.topos.site/ocl-009C /ocl-009C/ Example judgments for table JudgmentPronunciation is a type In context , is a term of type (where ) In context , the terms and of type are judgmentally equal However, what does this actually mean? There is much going on under the surface which is obscured by the notation. First of all, we should make a distinction between judgments and their derivations. Derivations are natural deduction trees whose base is a certain judgment. When we write , we are are identifying with some derivation of the judgment . Similarly, when we write , we identify (modulo renaming of and ) with a derivation of the judgment . The reader is encouraged to read section 1.2.2 of Reference to understand exactly how this shorthand works, and why it is important. It is the job of a machine implementation of type theory to elaborate term syntax into derivations. Owen Lynch 2025 3 11 https://forest.topos.site/ocl-009B/ https://forest.topos.site/ocl-009B /ocl-009B/ Judgments in a formal metalanguage aside In an Agda-like language, we might define judgment and derivations mutually inductively as in the following, where we have left Judgment empty for now (in general, what goes in Judgment will depend on the 2-theory and the 1-theory in addition to the 3-theory). Ty -> Judgment JEq : (Γ : Ctx) -> (A : Ty) -> Tm Γ A -> Tm Γ A -> Judgment data Derivation : Judgment -> Set where ...]]> This may not be the most practical way to implement type theory, but it hopefully does somewhat clarify the structure. Specifically, one can see that definition is an informal presentation of the Judgment type. We now give what are known as “structural rules” for . Generally speaking, the structural rules for a 3-theory tell you how you are allowed to use variables. When working type-theoretically, it is important that as much as possible these rules become admissible rather than being taken as primitive. In general, some of these rules must be primitive, but generally it is desirable for substitution to be admissible (though, see remark for a discussion of substitution as a primitive). However, it is essential that these rules are true, whether or not they are actually taken as primitive, which leads to contraints on how other rules get added to a type theory. 2025 2 28 https://forest.topos.site/ocl-0089/ https://forest.topos.site/ocl-0089 /ocl-0089/ The variable rule for rule 2025 2 28 https://forest.topos.site/ocl-008A/ https://forest.topos.site/ocl-008A /ocl-008A/ The weakening rule for rule We use the notation to indicate that is a subcontext of , in the sense that every typing judgment in also appears in . 2025 2 28 https://forest.topos.site/ocl-008B/ https://forest.topos.site/ocl-008B /ocl-008B/ The substitution rule for rule Note that this particular collection of rules is by no means the only way of presenting the structural rules for simple type theory. For instance, instead of rule , we could instead use rule (and in practice, this rule is closer to the actual implementation). But again, we emphasize that such distinctions, while extremely important in practice, are orthogonal to the issue at hand, which is to understand the classification of type theories into different 3-theories. 2025 2 28 https://forest.topos.site/ocl-008C/ https://forest.topos.site/ocl-008C /ocl-008C/ An alternative variable rule for rule Owen Lynch 2025 3 11 https://forest.topos.site/ocl-009A/ https://forest.topos.site/ocl-009A /ocl-009A/ Substitution as a primitive remark Almost all languages in fact do have a substitution primitive, in the form of let bindings. To see this, consider the typing rule for a let binding. This is more or less precisely the same typing for substitutions, it's just that we have rather than . It is still advantageous for substitution to be admissible, because then the evaluation semantics for let statements can use substitution, but it is worth pointing out that “substitution as a primitive” is actually a useful and commonplace operation. 2025 2 28 https://forest.topos.site/ocl-007N/ https://forest.topos.site/ocl-007N /ocl-007N/ 1-theories in the initial 2-theory for Just as how in finite product theories there was an initial 1-theory whose models were sets, in simple type theory there is an initial 2-theory. We will discuss the models (1-theories) of this initial 2-theory in this section. This is important, because just as in finite product theories, a model can be thought of as a “set with some structure”, a 1-theory of a general 2-theory may be thought of as a “1-theory of the initial 2-theory with some structure”. Informally speaking, a 1-theory is a postulation of primitive derivations of certain judgments. This will be easiest to explain by considering a couple of examples. 2025 2 28 https://forest.topos.site/ocl-008E/ https://forest.topos.site/ocl-008E /ocl-008E/ The 1-theory of graphs in example The 1-theory of graphs is given by taking as primitives the following derivations of judgments.A perhaps more accurate but less intuitive way of writing these “postulations of derivations” would be the following: And then in order to recover substitution as admissible, we would use and in a slightly different style. or, annotated with terms Although here it looks like we are postulating arbitrary inference rules, it is important to see that these inference rules are equivalent to postulating derivations of directly and taking substitution as a primitive; the reformulation so that substitution need not be a primitive is a technical detail. 2025 2 28 https://forest.topos.site/ocl-008D/ https://forest.topos.site/ocl-008D /ocl-008D/ The 1-theory of monoids in example The 1-theory of monoids is given by postulating the following primitive derivations of judgments.As in example , this is really a notation for something which technically looks more like: In § we will give a more precise definition of 1-theory. Owen Lynch 2025 2 28 https://forest.topos.site/ocl-007O/ https://forest.topos.site/ocl-007O /ocl-007O/ Cartesian multicategories The categorical semantics for is based around cartesian multicategories, so we start by reviewing some multicategory theory. For the reader who has expected the semantics to be in cartesian categories, we will discuss the difference in § , but before we can explain what the difference between the two approaches is we must first explain multicategories. 2025 2 28 https://forest.topos.site/ocl-008H/ https://forest.topos.site/ocl-008H /ocl-008H/ Multicategory informal definition A multicategory is like a category, except the domain of a morphism is a list of objects rather than a single object. To emphasize this, we call such morphisms “multimorphisms”.Notationally, if are objects in a multicategory , then we would write the set of multimorphisms from to as . We can visually depict a morphism in the following way: udmj30}{} \newcommand\yo{\!\text{\usefont{U}{min}{m}{n}\symbol{'207}}\!} \DeclareUnicodeCharacter{3088}{\yo} \usepackage{tikz, tikz-cd, mathtools, amssymb, stmaryrd,xcolor} \usetikzlibrary{matrix,arrows} \usetikzlibrary{backgrounds,fit,positioning,calc,shapes} \usetikzlibrary{decorations.pathreplacing} \usetikzlibrary{decorations.pathmorphing} \usetikzlibrary{decorations.markings} % `tikz-cd` is necessary to draw commutative diagrams. \RequirePackage{tikz-cd} % `amssymb` is necessary for `\lrcorner` and `\ulcorner`. \RequirePackage{amssymb} % `calc` is necessary to draw curved arrows. \usetikzlibrary{calc} % `pathmorphing` is necessary to draw squiggly arrows. \usetikzlibrary{decorations.pathmorphing} % `spath3` is necessary to draw shortened edges. \usetikzlibrary{spath3} % A TikZ style for curved arrows of a fixed height, due to AndréC. \tikzset{curve/.style={settings={#1},to path={(\tikztostart) .. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) .. (\tikztotarget)\tikztonodes}}, settings/.code={\tikzset{quiver/.cd,#1} \def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}}, quiver/.cd,pos/.initial=0.35,height/.initial=0} % A TikZ style for shortening paths without the poor behaviour of `shorten <' and `shorten >'. \tikzset{between/.style n args={2}{/tikz/spath/at end path construction={ \tikzset{spath/split at keep middle={current}{#1}{#2}} }}} % TikZ arrowhead/tail styles. \tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}} \tikzset{2tail/.code={\pgfsetarrowsstart{Implies[reversed]}}} \tikzset{2tail reversed/.code={\pgfsetarrowsstart{Implies}}} % TikZ arrow styles. \tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}} \newcommand{\triplecolon}{% \mathrel{\vbox{\baselineskip=2pt \hbox{.}\hbox{.}\hbox{.}}}% } \DeclareUnicodeCharacter{2AF6}{\triplecolon} \usepackage{mathpartir} ]]> Composition in multicategories is slightly annoying to write down, but fairly intuitive once visualized. Suppose that we have multimorphisms . Then they have a composite , which can be visualized as the following: udmj30}{} \newcommand\yo{\!\text{\usefont{U}{min}{m}{n}\symbol{'207}}\!} \DeclareUnicodeCharacter{3088}{\yo} \usepackage{tikz, tikz-cd, mathtools, amssymb, stmaryrd,xcolor} \usetikzlibrary{matrix,arrows} \usetikzlibrary{backgrounds,fit,positioning,calc,shapes} \usetikzlibrary{decorations.pathreplacing} \usetikzlibrary{decorations.pathmorphing} \usetikzlibrary{decorations.markings} % `tikz-cd` is necessary to draw commutative diagrams. \RequirePackage{tikz-cd} % `amssymb` is necessary for `\lrcorner` and `\ulcorner`. \RequirePackage{amssymb} % `calc` is necessary to draw curved arrows. \usetikzlibrary{calc} % `pathmorphing` is necessary to draw squiggly arrows. \usetikzlibrary{decorations.pathmorphing} % `spath3` is necessary to draw shortened edges. \usetikzlibrary{spath3} % A TikZ style for curved arrows of a fixed height, due to AndréC. \tikzset{curve/.style={settings={#1},to path={(\tikztostart) .. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) .. (\tikztotarget)\tikztonodes}}, settings/.code={\tikzset{quiver/.cd,#1} \def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}}, quiver/.cd,pos/.initial=0.35,height/.initial=0} % A TikZ style for shortening paths without the poor behaviour of `shorten <' and `shorten >'. \tikzset{between/.style n args={2}{/tikz/spath/at end path construction={ \tikzset{spath/split at keep middle={current}{#1}{#2}} }}} % TikZ arrowhead/tail styles. \tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}} \tikzset{2tail/.code={\pgfsetarrowsstart{Implies[reversed]}}} \tikzset{2tail reversed/.code={\pgfsetarrowsstart{Implies}}} % TikZ arrow styles. \tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}} \newcommand{\triplecolon}{% \mathrel{\vbox{\baselineskip=2pt \hbox{.}\hbox{.}\hbox{.}}}% } \DeclareUnicodeCharacter{2AF6}{\triplecolon} \usepackage{mathpartir} ]]> Identities are just as in categories; there is an identity for every object .There are also associative and unital conditions, but these are more annoying to write down in the current style because they would involve many indices. The interested reader can derive these conditions from the formal definition in definition . The reader eager to see how multicategories are connected to simple type theory may skip ahead to § , and the reader skeptical of informal definitions may continue on to definition . 2025 2 28 https://forest.topos.site/ocl-008I/ https://forest.topos.site/ocl-008I /ocl-008I/ Multicategory definition This is the definition of multicategory which may be found in Reference .Let be the list monad on , defined byA multicategory is a monad in the double category of -spans, where a loose morphism is a diagram udmj30}{} \newcommand\yo{\!\text{\usefont{U}{min}{m}{n}\symbol{'207}}\!} \DeclareUnicodeCharacter{3088}{\yo} \usepackage{tikz, tikz-cd, mathtools, amssymb, stmaryrd,xcolor} \usetikzlibrary{matrix,arrows} \usetikzlibrary{backgrounds,fit,positioning,calc,shapes} \usetikzlibrary{decorations.pathreplacing} \usetikzlibrary{decorations.pathmorphing} \usetikzlibrary{decorations.markings} % `tikz-cd` is necessary to draw commutative diagrams. \RequirePackage{tikz-cd} % `amssymb` is necessary for `\lrcorner` and `\ulcorner`. \RequirePackage{amssymb} % `calc` is necessary to draw curved arrows. \usetikzlibrary{calc} % `pathmorphing` is necessary to draw squiggly arrows. \usetikzlibrary{decorations.pathmorphing} % `spath3` is necessary to draw shortened edges. \usetikzlibrary{spath3} % A TikZ style for curved arrows of a fixed height, due to AndréC. \tikzset{curve/.style={settings={#1},to path={(\tikztostart) .. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) .. (\tikztotarget)\tikztonodes}}, settings/.code={\tikzset{quiver/.cd,#1} \def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}}, quiver/.cd,pos/.initial=0.35,height/.initial=0} % A TikZ style for shortening paths without the poor behaviour of `shorten <' and `shorten >'. \tikzset{between/.style n args={2}{/tikz/spath/at end path construction={ \tikzset{spath/split at keep middle={current}{#1}{#2}} }}} % TikZ arrowhead/tail styles. \tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}} \tikzset{2tail/.code={\pgfsetarrowsstart{Implies[reversed]}}} \tikzset{2tail reversed/.code={\pgfsetarrowsstart{Implies}}} % TikZ arrow styles. \tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}} \newcommand{\triplecolon}{% \mathrel{\vbox{\baselineskip=2pt \hbox{.}\hbox{.}\hbox{.}}}% } \DeclareUnicodeCharacter{2AF6}{\triplecolon} \usepackage{mathpartir} ]]> 2025 3 1 https://forest.topos.site/ocl-008J/ https://forest.topos.site/ocl-008J /ocl-008J/ Comparing definition and informal definition remark In this remark, we aim to make the connection between informal definition and definition explicit.A monad in the double category of -spans consists of a endo--span udmj30}{} \newcommand\yo{\!\text{\usefont{U}{min}{m}{n}\symbol{'207}}\!} \DeclareUnicodeCharacter{3088}{\yo} \usepackage{tikz, tikz-cd, mathtools, amssymb, stmaryrd,xcolor} \usetikzlibrary{matrix,arrows} \usetikzlibrary{backgrounds,fit,positioning,calc,shapes} \usetikzlibrary{decorations.pathreplacing} \usetikzlibrary{decorations.pathmorphing} \usetikzlibrary{decorations.markings} % `tikz-cd` is necessary to draw commutative diagrams. \RequirePackage{tikz-cd} % `amssymb` is necessary for `\lrcorner` and `\ulcorner`. \RequirePackage{amssymb} % `calc` is necessary to draw curved arrows. \usetikzlibrary{calc} % `pathmorphing` is necessary to draw squiggly arrows. \usetikzlibrary{decorations.pathmorphing} % `spath3` is necessary to draw shortened edges. \usetikzlibrary{spath3} % A TikZ style for curved arrows of a fixed height, due to AndréC. \tikzset{curve/.style={settings={#1},to path={(\tikztostart) .. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) .. (\tikztotarget)\tikztonodes}}, settings/.code={\tikzset{quiver/.cd,#1} \def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}}, quiver/.cd,pos/.initial=0.35,height/.initial=0} % A TikZ style for shortening paths without the poor behaviour of `shorten <' and `shorten >'. \tikzset{between/.style n args={2}{/tikz/spath/at end path construction={ \tikzset{spath/split at keep middle={current}{#1}{#2}} }}} % TikZ arrowhead/tail styles. \tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}} \tikzset{2tail/.code={\pgfsetarrowsstart{Implies[reversed]}}} \tikzset{2tail reversed/.code={\pgfsetarrowsstart{Implies}}} % TikZ arrow styles. \tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}} \newcommand{\triplecolon}{% \mathrel{\vbox{\baselineskip=2pt \hbox{.}\hbox{.}\hbox{.}}}% } \DeclareUnicodeCharacter{2AF6}{\triplecolon} \usepackage{mathpartir} ]]> with a unit, multiplication, and some conditions. Before we discus the other stuff, we first interpret this endo--span. The apex consists of all of the multimorphisms in the multicategory. The domain map assigns to a multimorphism its list of objects that form its domain, and the codomain map assigns to a multimorphism its single object that is its codomain. So, specifically, we can translate the notation into .The unit for consists of a 2-cell from the identity -span to which picks out the identity multimorphism at each object. As a 2-cell in a double category, this looks like udmj30}{} \newcommand\yo{\!\text{\usefont{U}{min}{m}{n}\symbol{'207}}\!} \DeclareUnicodeCharacter{3088}{\yo} \usepackage{tikz, tikz-cd, mathtools, amssymb, stmaryrd,xcolor} \usetikzlibrary{matrix,arrows} \usetikzlibrary{backgrounds,fit,positioning,calc,shapes} \usetikzlibrary{decorations.pathreplacing} \usetikzlibrary{decorations.pathmorphing} \usetikzlibrary{decorations.markings} % `tikz-cd` is necessary to draw commutative diagrams. \RequirePackage{tikz-cd} % `amssymb` is necessary for `\lrcorner` and `\ulcorner`. \RequirePackage{amssymb} % `calc` is necessary to draw curved arrows. \usetikzlibrary{calc} % `pathmorphing` is necessary to draw squiggly arrows. \usetikzlibrary{decorations.pathmorphing} % `spath3` is necessary to draw shortened edges. \usetikzlibrary{spath3} % A TikZ style for curved arrows of a fixed height, due to AndréC. \tikzset{curve/.style={settings={#1},to path={(\tikztostart) .. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) .. (\tikztotarget)\tikztonodes}}, settings/.code={\tikzset{quiver/.cd,#1} \def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}}, quiver/.cd,pos/.initial=0.35,height/.initial=0} % A TikZ style for shortening paths without the poor behaviour of `shorten <' and `shorten >'. \tikzset{between/.style n args={2}{/tikz/spath/at end path construction={ \tikzset{spath/split at keep middle={current}{#1}{#2}} }}} % TikZ arrowhead/tail styles. \tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}} \tikzset{2tail/.code={\pgfsetarrowsstart{Implies[reversed]}}} \tikzset{2tail reversed/.code={\pgfsetarrowsstart{Implies}}} % TikZ arrow styles. \tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}} \newcommand{\triplecolon}{% \mathrel{\vbox{\baselineskip=2pt \hbox{.}\hbox{.}\hbox{.}}}% } \DeclareUnicodeCharacter{2AF6}{\triplecolon} \usepackage{mathpartir} ]]>=4pt, Rightarrow, from=0, to=1] \end {tikzcd} ]]> In terms of actual -spans, this becomes. udmj30}{} \newcommand\yo{\!\text{\usefont{U}{min}{m}{n}\symbol{'207}}\!} \DeclareUnicodeCharacter{3088}{\yo} \usepackage{tikz, tikz-cd, mathtools, amssymb, stmaryrd,xcolor} \usetikzlibrary{matrix,arrows} \usetikzlibrary{backgrounds,fit,positioning,calc,shapes} \usetikzlibrary{decorations.pathreplacing} \usetikzlibrary{decorations.pathmorphing} \usetikzlibrary{decorations.markings} % `tikz-cd` is necessary to draw commutative diagrams. \RequirePackage{tikz-cd} % `amssymb` is necessary for `\lrcorner` and `\ulcorner`. \RequirePackage{amssymb} % `calc` is necessary to draw curved arrows. \usetikzlibrary{calc} % `pathmorphing` is necessary to draw squiggly arrows. \usetikzlibrary{decorations.pathmorphing} % `spath3` is necessary to draw shortened edges. \usetikzlibrary{spath3} % A TikZ style for curved arrows of a fixed height, due to AndréC. \tikzset{curve/.style={settings={#1},to path={(\tikztostart) .. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) .. (\tikztotarget)\tikztonodes}}, settings/.code={\tikzset{quiver/.cd,#1} \def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}}, quiver/.cd,pos/.initial=0.35,height/.initial=0} % A TikZ style for shortening paths without the poor behaviour of `shorten <' and `shorten >'. \tikzset{between/.style n args={2}{/tikz/spath/at end path construction={ \tikzset{spath/split at keep middle={current}{#1}{#2}} }}} % TikZ arrowhead/tail styles. \tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}} \tikzset{2tail/.code={\pgfsetarrowsstart{Implies[reversed]}}} \tikzset{2tail reversed/.code={\pgfsetarrowsstart{Implies}}} % TikZ arrow styles. \tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}} \newcommand{\triplecolon}{% \mathrel{\vbox{\baselineskip=2pt \hbox{.}\hbox{.}\hbox{.}}}% } \DeclareUnicodeCharacter{2AF6}{\triplecolon} \usepackage{mathpartir} ]]> The multiplication for implements the composition of multimorphisms. Double categorically, this looks like: udmj30}{} \newcommand\yo{\!\text{\usefont{U}{min}{m}{n}\symbol{'207}}\!} \DeclareUnicodeCharacter{3088}{\yo} \usepackage{tikz, tikz-cd, mathtools, amssymb, stmaryrd,xcolor} \usetikzlibrary{matrix,arrows} \usetikzlibrary{backgrounds,fit,positioning,calc,shapes} \usetikzlibrary{decorations.pathreplacing} \usetikzlibrary{decorations.pathmorphing} \usetikzlibrary{decorations.markings} % `tikz-cd` is necessary to draw commutative diagrams. \RequirePackage{tikz-cd} % `amssymb` is necessary for `\lrcorner` and `\ulcorner`. \RequirePackage{amssymb} % `calc` is necessary to draw curved arrows. \usetikzlibrary{calc} % `pathmorphing` is necessary to draw squiggly arrows. \usetikzlibrary{decorations.pathmorphing} % `spath3` is necessary to draw shortened edges. \usetikzlibrary{spath3} % A TikZ style for curved arrows of a fixed height, due to AndréC. \tikzset{curve/.style={settings={#1},to path={(\tikztostart) .. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) .. (\tikztotarget)\tikztonodes}}, settings/.code={\tikzset{quiver/.cd,#1} \def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}}, quiver/.cd,pos/.initial=0.35,height/.initial=0} % A TikZ style for shortening paths without the poor behaviour of `shorten <' and `shorten >'. \tikzset{between/.style n args={2}{/tikz/spath/at end path construction={ \tikzset{spath/split at keep middle={current}{#1}{#2}} }}} % TikZ arrowhead/tail styles. \tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}} \tikzset{2tail/.code={\pgfsetarrowsstart{Implies[reversed]}}} \tikzset{2tail reversed/.code={\pgfsetarrowsstart{Implies}}} % TikZ arrow styles. \tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}} \newcommand{\triplecolon}{% \mathrel{\vbox{\baselineskip=2pt \hbox{.}\hbox{.}\hbox{.}}}% } \DeclareUnicodeCharacter{2AF6}{\triplecolon} \usepackage{mathpartir} ]]> If we work this out in terms of actual spans, it looks like the following: udmj30}{} \newcommand\yo{\!\text{\usefont{U}{min}{m}{n}\symbol{'207}}\!} \DeclareUnicodeCharacter{3088}{\yo} \usepackage{tikz, tikz-cd, mathtools, amssymb, stmaryrd,xcolor} \usetikzlibrary{matrix,arrows} \usetikzlibrary{backgrounds,fit,positioning,calc,shapes} \usetikzlibrary{decorations.pathreplacing} \usetikzlibrary{decorations.pathmorphing} \usetikzlibrary{decorations.markings} % `tikz-cd` is necessary to draw commutative diagrams. \RequirePackage{tikz-cd} % `amssymb` is necessary for `\lrcorner` and `\ulcorner`. \RequirePackage{amssymb} % `calc` is necessary to draw curved arrows. \usetikzlibrary{calc} % `pathmorphing` is necessary to draw squiggly arrows. \usetikzlibrary{decorations.pathmorphing} % `spath3` is necessary to draw shortened edges. \usetikzlibrary{spath3} % A TikZ style for curved arrows of a fixed height, due to AndréC. \tikzset{curve/.style={settings={#1},to path={(\tikztostart) .. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) .. (\tikztotarget)\tikztonodes}}, settings/.code={\tikzset{quiver/.cd,#1} \def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}}, quiver/.cd,pos/.initial=0.35,height/.initial=0} % A TikZ style for shortening paths without the poor behaviour of `shorten <' and `shorten >'. \tikzset{between/.style n args={2}{/tikz/spath/at end path construction={ \tikzset{spath/split at keep middle={current}{#1}{#2}} }}} % TikZ arrowhead/tail styles. \tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}} \tikzset{2tail/.code={\pgfsetarrowsstart{Implies[reversed]}}} \tikzset{2tail reversed/.code={\pgfsetarrowsstart{Implies}}} % TikZ arrow styles. \tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}} \newcommand{\triplecolon}{% \mathrel{\vbox{\baselineskip=2pt \hbox{.}\hbox{.}\hbox{.}}}% } \DeclareUnicodeCharacter{2AF6}{\triplecolon} \usepackage{mathpartir} ]]> It is a little hard to parse, but with some thought the reader can work out that the apex of the span composition consists of the set of pairs with , which is precisely the setup for multimorphism composition in informal definition . We now give a hint as to how the semantics of will work. We cannot give the full semantics yet, because the full semantics are in cartesian multicategories and we have not yet defined cartesian multicategories, but we can start to give the correspondence between multicategories and type theory that will eventually turn into a proper semantics, and this will help motivate why we care about cartesian multicategories. Owen Lynch 2025 3 2 https://forest.topos.site/ocl-008K/ https://forest.topos.site/ocl-008K /ocl-008K/ A correspondence between and multicategory theory We present the correspondence via a translation table. In the type theory column we give judgments, and in the multicategory theory column we say how they translate into the setting of multicategories. Owen Lynch 2025 3 2 Judgments in simple type theory and their semantics table Simple type theoryMulticategory theory is an object is a multimorphism from to and are equal multimorphisms. The identity multimorphism on We can now say why we use multicategories rather than just categories: multicategories more faithfully reflect the fact that a context consists of a list of varaibles. We cannot yet interpret rule or rule ; to do that we need to first introduce cartesian multicategories. Intuitively, a cartesian multicategory is the multicategory version of a cartesian monoidal category. The following definition is somewhat dense, but we follow it with explication that makes the connection clearer. 2025 2 12 https://forest.topos.site/ocl-006C/ https://forest.topos.site/ocl-006C /ocl-006C/ Cartesian multicategory definition The following is distilled from Categorical logic from a categorical point of view, page 116. A cartesian multicategory is a multicategory equipped with operations for all functions , satisfying the following axioms , where is the arity of and is lifted in the natural way to be a function which is “block-wise the identity”. 2025 2 12 https://forest.topos.site/ocl-006D/ https://forest.topos.site/ocl-006D /ocl-006D/ Unpacking the definition of Cartesian multicategory We can understand the meaning of Cartesian multicategory by considering certain special classes of . In the special case where is a bijection, we can see that the operation makes into a symmetric multicategory. In the special case where , we get the projections . These interpret the extended variable rule rule . In the special case where is an injection, we get weakening (rule ). Combining a special surjective with multimorphism composition, we may derive rule . In general, the action of various means that when we form terms in a simple type theory, we may use each variable as many times as we like in any order that we like. Owen Lynch 2025 3 3 https://forest.topos.site/ocl-008M/ https://forest.topos.site/ocl-008M /ocl-008M/ Contrasting cartesian multicategories with cartesian categories. With the following two definitions, we can go back and forth between cartesian multicategories and cartesian categories. Owen Lynch 2025 3 8 https://forest.topos.site/ocl-0098/ https://forest.topos.site/ocl-0098 /ocl-0098/ The multicategory of tuple-argument morphisms associated to a cartesian category definition Given a cartesian category we may associate to it a multicategory of tuple-argument morphisms, where the objects of are the objects of and the multimorphisms of from to are the morphisms in . This category is so named because it reflects the fact that in a programming language with no multi-argument functions but with tuple types, one can simulate a multi-argument function via a function out of a tuple type. Owen Lynch 2025 3 8 https://forest.topos.site/ocl-0099/ https://forest.topos.site/ocl-0099 /ocl-0099/ The cartesian category of substitutions associated to a cartesian multicategory definition Given a cartesian multicategory , we may form a cartesian category . The objects of are lists of objects in and a morphism from is a list of multimorphisms where . The cartesian product is then given by list appending. We call this the category of substitutions for , in reference to the fact that if is modeling a simple type theory then a morphism in is precisely a substitution between contexts. That is, each “variable” in is assigned a “term” in . For those who like 2-category theory, and form a 2-adjunction between the 2-category of cartesian categories and the 2-category of cartesian multicategories. The core of this 2-adjunction is given by the 2-category of cartesian categories, which is identified with the 2-category of representable cartesian multicategories as we will see in definition . So there is a close connection between cartesian categories and cartesian multicategories. Why then do we use cartesian multicategories as opposed to cartesian categories to model simple type theory? There are several reasons. As we noted before in § , multicategories more faithfully reflect the fact that a context consists of a list of variables. Given a category where products exist, one must equip it with a choice of products in order to talk about multimorphisms, and this choice of products is non-canonical. However, to define a cartesian multicategory, one need not make any non-canonical choices. Owen Lynch 2025 3 3 https://forest.topos.site/ocl-008N/ https://forest.topos.site/ocl-008N /ocl-008N/ Model theory of free simple type 1-theories In general, the formal relationship between type theory and category theory is that the syntax of a specific type theory forms the initial object of a corresponding category of models. In this section, we discuss how this works in the special case of free simple type 1-theories. In example and example we gave some examples of simple type 1-theories. In general, a simple type 1-theory involves types, terms, and equations. A free simple type 1-theory only involves types and terms, and it can be presented by a multigraph. Owen Lynch 2025 3 6 https://forest.topos.site/ocl-008P/ https://forest.topos.site/ocl-008P /ocl-008P/ Multigraphs definition A multigraph is an endomorphism in the category of -spans.More concretely, a multigraph consists of a set of vertices, a set of edges, and a -span udmj30}{} \newcommand\yo{\!\text{\usefont{U}{min}{m}{n}\symbol{'207}}\!} \DeclareUnicodeCharacter{3088}{\yo} \usepackage{tikz, tikz-cd, mathtools, amssymb, stmaryrd,xcolor} \usetikzlibrary{matrix,arrows} \usetikzlibrary{backgrounds,fit,positioning,calc,shapes} \usetikzlibrary{decorations.pathreplacing} \usetikzlibrary{decorations.pathmorphing} \usetikzlibrary{decorations.markings} % `tikz-cd` is necessary to draw commutative diagrams. \RequirePackage{tikz-cd} % `amssymb` is necessary for `\lrcorner` and `\ulcorner`. \RequirePackage{amssymb} % `calc` is necessary to draw curved arrows. \usetikzlibrary{calc} % `pathmorphing` is necessary to draw squiggly arrows. \usetikzlibrary{decorations.pathmorphing} % `spath3` is necessary to draw shortened edges. \usetikzlibrary{spath3} % A TikZ style for curved arrows of a fixed height, due to AndréC. \tikzset{curve/.style={settings={#1},to path={(\tikztostart) .. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) .. (\tikztotarget)\tikztonodes}}, settings/.code={\tikzset{quiver/.cd,#1} \def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}}, quiver/.cd,pos/.initial=0.35,height/.initial=0} % A TikZ style for shortening paths without the poor behaviour of `shorten <' and `shorten >'. \tikzset{between/.style n args={2}{/tikz/spath/at end path construction={ \tikzset{spath/split at keep middle={current}{#1}{#2}} }}} % TikZ arrowhead/tail styles. \tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}} \tikzset{2tail/.code={\pgfsetarrowsstart{Implies[reversed]}}} \tikzset{2tail reversed/.code={\pgfsetarrowsstart{Implies}}} % TikZ arrow styles. \tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}} \newcommand{\triplecolon}{% \mathrel{\vbox{\baselineskip=2pt \hbox{.}\hbox{.}\hbox{.}}}% } \DeclareUnicodeCharacter{2AF6}{\triplecolon} \usepackage{mathpartir} ]]> There is a category of multigraphs, where a morphism is of the form udmj30}{} \newcommand\yo{\!\text{\usefont{U}{min}{m}{n}\symbol{'207}}\!} \DeclareUnicodeCharacter{3088}{\yo} \usepackage{tikz, tikz-cd, mathtools, amssymb, stmaryrd,xcolor} \usetikzlibrary{matrix,arrows} \usetikzlibrary{backgrounds,fit,positioning,calc,shapes} \usetikzlibrary{decorations.pathreplacing} \usetikzlibrary{decorations.pathmorphing} \usetikzlibrary{decorations.markings} % `tikz-cd` is necessary to draw commutative diagrams. \RequirePackage{tikz-cd} % `amssymb` is necessary for `\lrcorner` and `\ulcorner`. \RequirePackage{amssymb} % `calc` is necessary to draw curved arrows. \usetikzlibrary{calc} % `pathmorphing` is necessary to draw squiggly arrows. \usetikzlibrary{decorations.pathmorphing} % `spath3` is necessary to draw shortened edges. \usetikzlibrary{spath3} % A TikZ style for curved arrows of a fixed height, due to AndréC. \tikzset{curve/.style={settings={#1},to path={(\tikztostart) .. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) .. (\tikztotarget)\tikztonodes}}, settings/.code={\tikzset{quiver/.cd,#1} \def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}}, quiver/.cd,pos/.initial=0.35,height/.initial=0} % A TikZ style for shortening paths without the poor behaviour of `shorten <' and `shorten >'. \tikzset{between/.style n args={2}{/tikz/spath/at end path construction={ \tikzset{spath/split at keep middle={current}{#1}{#2}} }}} % TikZ arrowhead/tail styles. \tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}} \tikzset{2tail/.code={\pgfsetarrowsstart{Implies[reversed]}}} \tikzset{2tail reversed/.code={\pgfsetarrowsstart{Implies}}} % TikZ arrow styles. \tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}} \newcommand{\triplecolon}{% \mathrel{\vbox{\baselineskip=2pt \hbox{.}\hbox{.}\hbox{.}}}% } \DeclareUnicodeCharacter{2AF6}{\triplecolon} \usepackage{mathpartir} ]]> We can identify free simple type 1-theories with finite multigraphs. Each vertex in the multigraph represents a primitive type, and each edge represents a primitive operation. Owen Lynch 2025 3 6 https://forest.topos.site/ocl-008Q/ https://forest.topos.site/ocl-008Q /ocl-008Q/ Underlying multigraph of a multicategory definition By the definition of multicategory, every multicategory has an underlying multigraph where the vertices are the objects of the multicategory and the edges are multimorphisms. Moreover, the assignment is functorial. Owen Lynch 2025 3 6 https://forest.topos.site/ocl-008R/ https://forest.topos.site/ocl-008R /ocl-008R/ Models of a free simple type 1-theory definition Given a free simple type 1-theory , represented as a multigraph, a model of it consists of a cartesian multicategory with a multigraph homomorphism . There is a category of such models, which is simply the slice category . Arguably the entire point of type theory is to be able to prove analogues of following. Owen Lynch 2025 3 6 https://forest.topos.site/ocl-008V/ https://forest.topos.site/ocl-008V /ocl-008V/ Initial model of a theory proposition Given a multigraph , extend the type theory of § with the following rules. Owen Lynch 2025 3 6 https://forest.topos.site/ocl-008W/ https://forest.topos.site/ocl-008W /ocl-008W/ Primitive types rule Owen Lynch 2025 3 6 https://forest.topos.site/ocl-008X/ https://forest.topos.site/ocl-008X /ocl-008X/ Primitive functions rule There is then a multicategory for that type theory described in the following way. The objects are derivations of A multimorphism from to are derivation of the judgment . Composition is given by substitution (which is admissible). Identities are given by the identity structural rule. This multicategory is the initial model for . A similar theorem can be proven about simple type 1-theories which involve equations, but the definition of such a simple type 1-theory is slightly more complicated. Owen Lynch 2025 2 28 https://forest.topos.site/ocl-007P/ https://forest.topos.site/ocl-007P /ocl-007P/ 2-theories in and their semantics Up to now, the only rules in simple type theory have been the structural rules and “primitive rules”. In this section, we discuss how to add additional rules to type theory which go beyond this. In general, these rules will tell us how to form new types, and then determine the elements of those new types via universal properties. We call these “rules of inference”. We will see that postulating certain rules of inference is equivalent to considering cartesian multicategories with 2-algebraic structure determined by universal properties. That is, when we think about, for instance “simple type theory with product types”, its model theory will consist of cartesian multicategories with some extra structure, where that structure is determined via universal properties. Correspondingly, we term rules of inference “type 2-theories” (this of course again follows Shulman's use of the term). This will probably make the most sense after considering some examples. Owen Lynch 2025 2 28 https://forest.topos.site/ocl-007Q/ https://forest.topos.site/ocl-007Q /ocl-007Q/ Product types Product types are determined type-theoretically by the following rules. Owen Lynch 2025 3 6 https://forest.topos.site/ocl-008Z/ https://forest.topos.site/ocl-008Z /ocl-008Z/ Product formation rule Owen Lynch 2025 3 6 https://forest.topos.site/ocl-0090/ https://forest.topos.site/ocl-0090 /ocl-0090/ Product introduction and elimination rule Owen Lynch 2025 3 6 https://forest.topos.site/ocl-0091/ https://forest.topos.site/ocl-0091 /ocl-0091/ Product beta and eta rule This corresponds to the structure of a representable cartesian multicategory. To define representable cartesian multicategory, we first make use of an auxilary definition. Owen Lynch 2025 3 6 https://forest.topos.site/ocl-0093/ https://forest.topos.site/ocl-0093 /ocl-0093/ The context construction for cartesian multicategories definition In this definition, we explore a structure on cartesian multicategories which more directly interprets the substitution rule for simple type theory. Given a cartesian muliticategory and a list of objects in , then let be the cartesian multicategory with the same objects as , but where a multimorphism from to is a multimorphism in from to . Composition in critically relies on being able to duplicate contexts, and thus on the cartesian multicategory structure. We can now see that the substitution rule interprets multimorphism composition in with “constants” in (which are multimorphisms out of in ). Owen Lynch 2025 3 6 https://forest.topos.site/ocl-0092/ https://forest.topos.site/ocl-0092 /ocl-0092/ Representable cartesian multicategory definition We say that cartesian multicategory is representable if we have an operation on objects such that for every list of objects , the functor given by is represented by , that is we have a natural isomorphism . It is a good exercise to show that the introduction, elimination, beta and eta rules are jointly sufficient and necessary to deduce the natural isomorphism. It is no coincidence that an isomorphism has 4 parts: a function in either direction and a proofs that both composites are each equal to the identity. It is also a good exercise to show that if a is the multicategory associated to a cartesian monoidal category, then is a representable cartesian multicategory. Because in most cases, we are in fact working with the multicategory associated to some cartesian monoidal category, adding product types is a quite mild assumption that does not restrict our semantics too much; many categories have finite products. Owen Lynch 2025 2 28 https://forest.topos.site/ocl-007R/ https://forest.topos.site/ocl-007R /ocl-007R/ Function types Function types are determined type-theoretically by the following rules. Owen Lynch 2025 3 6 https://forest.topos.site/ocl-0094/ https://forest.topos.site/ocl-0094 /ocl-0094/ Function formation rule Owen Lynch 2025 3 6 https://forest.topos.site/ocl-0095/ https://forest.topos.site/ocl-0095 /ocl-0095/ Function introduction and elimination rule Owen Lynch 2025 3 6 https://forest.topos.site/ocl-0096/ https://forest.topos.site/ocl-0096 /ocl-0096/ Function beta and eta rule Function types correspond categorically to being a closed cartesian multicategory, which we shall now define. Owen Lynch 2025 3 6 https://forest.topos.site/ocl-0097/ https://forest.topos.site/ocl-0097 /ocl-0097/ Closed cartesian multicategory definition Just like for representable cartesian multicategories, a closed cartesian multicategory is defined by an operation on objects , along with a characterization of in terms of the representability of a certain functor. Specifically, for a cartesian multicategory , consider the contravariant functor sending to , where is the category of substitutions for . Then a cartesian multicategory is closed if is represented by . That is, multimorphisms are in natural bijection with multimorphisms . An equivalent definition of closed cartesian multicategory may be found in Reference . In contrast to product types, the existence of function types is a strong assumption for a type theory, as there are many cartesian multicategories which are not closed. The intuition for why this is the case is that, in general, function types might be too “large”. For instance, the category of finite-dimensional manifolds with smooth maps between them is a cartesian category (and thus has a cartesian multicategory of tuple-argument functions), but it is certainly not closed, as function spaces of smooth maps between manifolds are in general infinite dimensional. Similarly, in a programming language, function types necessarily have no bound in terms of the amount of memory that they take up, because a lambda may close over arbitrary many variables. In general runtime techniques like garbage collection and dynamic dispatch must be used to support the elements of such function types, which imposes a performance penalty that compilers spend significant amounts of complexity trying to work around via static analysis. In general, the syntactic component of type 2-theories will be the postulation of certain inference rules, and the semantic component will be the representability of certain functors, or in other words, the postulation of objects satisfying some universal properties. It is somewhat of an art to pick inference rules such that the derivations with respect to those inference rules admit substitution and have other good properties, but often taking the isomorphism that characterizes a representability result and adding rules for both directions (introduction and elimination) along with how each is a section of the other (beta and eta), works fairly well. One might also postulate structure which is not uniquely-up-to-isomorphism characterized by universal properties. This might correspond to postulating that your model is an algebra of an arbitraty 2-monad on the 2-category of multicategories. However, generally this is ill-advised. The beauty of structure characterized by universal properties is that 2-theories become trivially composable, so one may postulate product types and function types without needing any rules to say how the product types and function types interact. In contrast, structure not characterized by universal properties might need additional rules to say how it interacts with other structure, and in a type theory with many constructions this may scale badly. Owen Lynch 2025 2 28 https://forest.topos.site/ocl-0072/ https://forest.topos.site/ocl-0072 /ocl-0072/ The 3-theory of dependent type theories () Owen Lynch 2025 2 28 https://forest.topos.site/ocl-007T/ https://forest.topos.site/ocl-007T /ocl-007T/ Judgment structure of Just as we did for simple type theory, we begin by reviewing the judgment structure of dependent type theory. The important difference between simple type theory and dependent type theory is that in simple type theory “contexts” were a derived notion; a context was merely a list of types. In dependent type theory, context is a primitive notion. It will turn out that there is still some sense in which a context is a list of types, but it will take a bit of time for us to see why that is. Owen Lynch 2025 3 11 https://forest.topos.site/ocl-009D/ https://forest.topos.site/ocl-009D /ocl-009D/ Example judgments for table JudgmentPronunciation is a context In context , is a type In context , and are judgmentally equal types In context , is a term of type In context , and are judgmentally equal terms of type We then have some structural rules. First of all, we have rules which allow us to produce contexts in the first place. Owen Lynch 2025 3 11 https://forest.topos.site/ocl-009E/ https://forest.topos.site/ocl-009E /ocl-009E/ Context formation rule rule says that there is an empty context, and that given a type judgment in a context, we may extend that context by a free variable in that type. But how can we use this extended context? First off, we have the variable rule. Owen Lynch 2025 3 11 https://forest.topos.site/ocl-009F/ https://forest.topos.site/ocl-009F /ocl-009F/ The variable rule for rule The variable rule simple says that we can use this postulated element of . We then have weakening. Owen Lynch 2025 3 11 https://forest.topos.site/ocl-009H/ https://forest.topos.site/ocl-009H /ocl-009H/ Weakening for rule Weakening says that anything we could derive in , we can still derive in . We then have substitution. Substitutions in dependent type theory are similar to the substitutions in definition , but trickier because substituting into terms can change types. In order to handle this, we inductively define substitutions in the following way. Owen Lynch 2025 3 11 https://forest.topos.site/ocl-009G/ https://forest.topos.site/ocl-009G /ocl-009G/ Dependent substitution definition A substitution from a context to a context is defined by considering the ways in which could be formed. In the case that , the empty context, then there is precisely one substitution into . Note that this makes into the terminal object of the category of contexts and substitutions. In the case that , then a substitution from to consists of a pair of a substitution , along with a term , where refers to the action of on the type in context to product a type in context . Of course, this operation must also be defined. This is generally done mutually recursively with the definition of substitution, but in order to do this we must know all the type formers, which we won't know until we fix a 1-theory and a 2-theory. Thus, in general, if is a context with free variables, a substitution into will consist of terms in context , of appropriate types. Substitutions act on both terms and types, so if we have , and , then . Owen Lynch 2025 2 28 https://forest.topos.site/ocl-007U/ https://forest.topos.site/ocl-007U /ocl-007U/ 1-theories in There is a surprising amount of power in just the basic setup for dependent type theory as given in § . That is, without adding any type formers for dependent records, dependent functions, etc. (e.g., 2-theories) we can still do many non-trivial things with 1-theories, analogous to how the basic setup for simple type theory afforded algebraic theories as its 1-theories. The classical name for 1-theories in is generalized algebraic theories Reference . All algebraic theories are also generalized algebraic theories; the canonical example of a generalized algebraic theory that is not an algebraic theory is the generalized algebraic theory of categories. 2025 2 13 https://forest.topos.site/ocl-006L/ https://forest.topos.site/ocl-006L /ocl-006L/ Categories as a generalized algebraic theory example The theory of categories is given by postulating the following judgments in dependent type theory; as discussed in § such a postulation is equivalently a generalized algebraic theory. Owen Lynch 2025 2 28 https://forest.topos.site/ocl-007V/ https://forest.topos.site/ocl-007V /ocl-007V/ Categorical semantics for One popular categorical semantics for is given by natural models, as introduced in Reference or Reference .Unfortunately, Reference ends at hyperdoctrines and does not go on to dependent type theory, but a similarly rigorous account of the semantics of dependent type theory may be found in Reference .We define natural model in the following definition, but note that the definition of natural model contains a concept (representable natural transformation) which we have not yet defined; we will define it after starting to give the correspondence between type theory and natural models so that the motivation for the definition is clear.Owen Lynch2025311https://forest.topos.site/ocl-009I/https://forest.topos.site/ocl-009I/ocl-009I/Natural modeldefinitionA natural model consists of a category , two presheaves , and a representable natural transformation .The connection between natural models and dependent type theory can be summarized in the following table.Owen Lynch2025311https://forest.topos.site/ocl-009J/https://forest.topos.site/ocl-009J/ocl-009J/Correspondence between type theory and natural modelstable Type theoryNatural model is an object of is a substitution is a morphism in and + naturality of Notice that the big thing missing from table is context formation, as in rule . This is addressed by the representability condition on , as defined in definition .2025213https://forest.topos.site/ocl-006J/https://forest.topos.site/ocl-006J/ocl-006J/Representable natural transformationdefinitionLet be a category, with and . Then is representable if for any object and any element , the pullback of the following diagram is a representable presheaf (recall that we identify with ). udmj30}{} \newcommand\yo{\!\text{\usefont{U}{min}{m}{n}\symbol{'207}}\!} \DeclareUnicodeCharacter{3088}{\yo} \usepackage{tikz, tikz-cd, mathtools, amssymb, stmaryrd,xcolor} \usetikzlibrary{matrix,arrows} \usetikzlibrary{backgrounds,fit,positioning,calc,shapes} \usetikzlibrary{decorations.pathreplacing} \usetikzlibrary{decorations.pathmorphing} \usetikzlibrary{decorations.markings} % `tikz-cd` is necessary to draw commutative diagrams. \RequirePackage{tikz-cd} % `amssymb` is necessary for `\lrcorner` and `\ulcorner`. \RequirePackage{amssymb} % `calc` is necessary to draw curved arrows. \usetikzlibrary{calc} % `pathmorphing` is necessary to draw squiggly arrows. \usetikzlibrary{decorations.pathmorphing} % `spath3` is necessary to draw shortened edges. \usetikzlibrary{spath3} % A TikZ style for curved arrows of a fixed height, due to AndréC. \tikzset{curve/.style={settings={#1},to path={(\tikztostart) .. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) .. (\tikztotarget)\tikztonodes}}, settings/.code={\tikzset{quiver/.cd,#1} \def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}}, quiver/.cd,pos/.initial=0.35,height/.initial=0} % A TikZ style for shortening paths without the poor behaviour of `shorten <' and `shorten >'. \tikzset{between/.style n args={2}{/tikz/spath/at end path construction={ \tikzset{spath/split at keep middle={current}{#1}{#2}} }}} % TikZ arrowhead/tail styles. \tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}} \tikzset{2tail/.code={\pgfsetarrowsstart{Implies[reversed]}}} \tikzset{2tail reversed/.code={\pgfsetarrowsstart{Implies}}} % TikZ arrow styles. \tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}} \newcommand{\triplecolon}{% \mathrel{\vbox{\baselineskip=2pt \hbox{.}\hbox{.}\hbox{.}}}% } \DeclareUnicodeCharacter{2AF6}{\triplecolon} \usepackage{mathpartir} ]]> To interpret representability in the context of natural models, let be a context with , and consider a diagram of the form: udmj30}{} \newcommand\yo{\!\text{\usefont{U}{min}{m}{n}\symbol{'207}}\!} \DeclareUnicodeCharacter{3088}{\yo} \usepackage{tikz, tikz-cd, mathtools, amssymb, stmaryrd,xcolor} \usetikzlibrary{matrix,arrows} \usetikzlibrary{backgrounds,fit,positioning,calc,shapes} \usetikzlibrary{decorations.pathreplacing} \usetikzlibrary{decorations.pathmorphing} \usetikzlibrary{decorations.markings} % `tikz-cd` is necessary to draw commutative diagrams. \RequirePackage{tikz-cd} % `amssymb` is necessary for `\lrcorner` and `\ulcorner`. \RequirePackage{amssymb} % `calc` is necessary to draw curved arrows. \usetikzlibrary{calc} % `pathmorphing` is necessary to draw squiggly arrows. \usetikzlibrary{decorations.pathmorphing} % `spath3` is necessary to draw shortened edges. \usetikzlibrary{spath3} % A TikZ style for curved arrows of a fixed height, due to AndréC. \tikzset{curve/.style={settings={#1},to path={(\tikztostart) .. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) .. (\tikztotarget)\tikztonodes}}, settings/.code={\tikzset{quiver/.cd,#1} \def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}}, quiver/.cd,pos/.initial=0.35,height/.initial=0} % A TikZ style for shortening paths without the poor behaviour of `shorten <' and `shorten >'. \tikzset{between/.style n args={2}{/tikz/spath/at end path construction={ \tikzset{spath/split at keep middle={current}{#1}{#2}} }}} % TikZ arrowhead/tail styles. \tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}} \tikzset{2tail/.code={\pgfsetarrowsstart{Implies[reversed]}}} \tikzset{2tail reversed/.code={\pgfsetarrowsstart{Implies}}} % TikZ arrow styles. \tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}} \newcommand{\triplecolon}{% \mathrel{\vbox{\baselineskip=2pt \hbox{.}\hbox{.}\hbox{.}}}% } \DeclareUnicodeCharacter{2AF6}{\triplecolon} \usepackage{mathpartir} ]]> Note that is, by the yoneda lemma, identified with a natural transformation out of . Then representability says that the apex of the pullback is representable by another object of , which we name . udmj30}{} \newcommand\yo{\!\text{\usefont{U}{min}{m}{n}\symbol{'207}}\!} \DeclareUnicodeCharacter{3088}{\yo} \usepackage{tikz, tikz-cd, mathtools, amssymb, stmaryrd,xcolor} \usetikzlibrary{matrix,arrows} \usetikzlibrary{backgrounds,fit,positioning,calc,shapes} \usetikzlibrary{decorations.pathreplacing} \usetikzlibrary{decorations.pathmorphing} \usetikzlibrary{decorations.markings} % `tikz-cd` is necessary to draw commutative diagrams. \RequirePackage{tikz-cd} % `amssymb` is necessary for `\lrcorner` and `\ulcorner`. \RequirePackage{amssymb} % `calc` is necessary to draw curved arrows. \usetikzlibrary{calc} % `pathmorphing` is necessary to draw squiggly arrows. \usetikzlibrary{decorations.pathmorphing} % `spath3` is necessary to draw shortened edges. \usetikzlibrary{spath3} % A TikZ style for curved arrows of a fixed height, due to AndréC. \tikzset{curve/.style={settings={#1},to path={(\tikztostart) .. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) .. (\tikztotarget)\tikztonodes}}, settings/.code={\tikzset{quiver/.cd,#1} \def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}}, quiver/.cd,pos/.initial=0.35,height/.initial=0} % A TikZ style for shortening paths without the poor behaviour of `shorten <' and `shorten >'. \tikzset{between/.style n args={2}{/tikz/spath/at end path construction={ \tikzset{spath/split at keep middle={current}{#1}{#2}} }}} % TikZ arrowhead/tail styles. \tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}} \tikzset{2tail/.code={\pgfsetarrowsstart{Implies[reversed]}}} \tikzset{2tail reversed/.code={\pgfsetarrowsstart{Implies}}} % TikZ arrow styles. \tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}} \newcommand{\triplecolon}{% \mathrel{\vbox{\baselineskip=2pt \hbox{.}\hbox{.}\hbox{.}}}% } \DeclareUnicodeCharacter{2AF6}{\triplecolon} \usepackage{mathpartir} ]]> This pullback diagram ingeniously interprets several type-theoretic rules at once.The object represents the context extension of by . The action of on types and terms gives us weakening. The morphism represents the variable rule; we have a term of type in context Additionally, if we consider the universal property of pullback, it will tell us the unique way to form a substitution into . udmj30}{} \newcommand\yo{\!\text{\usefont{U}{min}{m}{n}\symbol{'207}}\!} \DeclareUnicodeCharacter{3088}{\yo} \usepackage{tikz, tikz-cd, mathtools, amssymb, stmaryrd,xcolor} \usetikzlibrary{matrix,arrows} \usetikzlibrary{backgrounds,fit,positioning,calc,shapes} \usetikzlibrary{decorations.pathreplacing} \usetikzlibrary{decorations.pathmorphing} \usetikzlibrary{decorations.markings} % `tikz-cd` is necessary to draw commutative diagrams. \RequirePackage{tikz-cd} % `amssymb` is necessary for `\lrcorner` and `\ulcorner`. \RequirePackage{amssymb} % `calc` is necessary to draw curved arrows. \usetikzlibrary{calc} % `pathmorphing` is necessary to draw squiggly arrows. \usetikzlibrary{decorations.pathmorphing} % `spath3` is necessary to draw shortened edges. \usetikzlibrary{spath3} % A TikZ style for curved arrows of a fixed height, due to AndréC. \tikzset{curve/.style={settings={#1},to path={(\tikztostart) .. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) .. (\tikztotarget)\tikztonodes}}, settings/.code={\tikzset{quiver/.cd,#1} \def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}}, quiver/.cd,pos/.initial=0.35,height/.initial=0} % A TikZ style for shortening paths without the poor behaviour of `shorten <' and `shorten >'. \tikzset{between/.style n args={2}{/tikz/spath/at end path construction={ \tikzset{spath/split at keep middle={current}{#1}{#2}} }}} % TikZ arrowhead/tail styles. \tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}} \tikzset{2tail/.code={\pgfsetarrowsstart{Implies[reversed]}}} \tikzset{2tail reversed/.code={\pgfsetarrowsstart{Implies}}} % TikZ arrow styles. \tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}} \newcommand{\triplecolon}{% \mathrel{\vbox{\baselineskip=2pt \hbox{.}\hbox{.}\hbox{.}}}% } \DeclareUnicodeCharacter{2AF6}{\triplecolon} \usepackage{mathpartir} ]]> This diagram says that if we have a substitution and a term of type (that is, the action of on the type ), then we can form a substitution into , and moreover all substitutions into are produced in this manner. This is in accordance with the definition of substitution into an extended context that we gave in definition .Owen Lynch2025311https://forest.topos.site/ocl-009K/https://forest.topos.site/ocl-009K/ocl-009K/Additional conditions on natural modelsremarkThere are two additional conditions one might wish to put on a natural model. The first condition is that has a terminal object, which models the empty context. The second condition is that every object in is formed by repeated context extension from the terminal object. This is known as a “democratic” model. Owen Lynch 2025 2 28 https://forest.topos.site/ocl-007W/ https://forest.topos.site/ocl-007W /ocl-007W/ 2-theories in and their semantics In this section, we will go over some of the inference rules one can add to and their semantics from the natural models perspective. Note that combining § and § gets you most of the way to Martin-Löf type theory. Owen Lynch 2025 2 28 https://forest.topos.site/ocl-007X/ https://forest.topos.site/ocl-007X /ocl-007X/ Sigma types Sigma types are also known as dependent sums. They are called sigma types because the mathematical notation for disjoint union uses a capital sigma: .We start with the inference rules. These are presented in a different style than § , because writing out dependent sigma types in the style of § is somewhat annoying and in a structural type theory (a type theory with no restrictions on variable use), the two presentations are equivalent.Owen Lynch2025311https://forest.topos.site/ocl-009L/https://forest.topos.site/ocl-009L/ocl-009L/Formation for sigma typesrule Owen Lynch2025311https://forest.topos.site/ocl-009M/https://forest.topos.site/ocl-009M/ocl-009M/Introduction and elimination for sigma typesrule Owen Lynch2025311https://forest.topos.site/ocl-009N/https://forest.topos.site/ocl-009N/ocl-009N/Beta and eta for sigma typesrule These inference rules above correspond to the following structure on a natural model. Specifically, we say that a certain morphism is small if there exists a type with an isomorphism in the slice over , such that the following commutes udmj30}{} \newcommand\yo{\!\text{\usefont{U}{min}{m}{n}\symbol{'207}}\!} \DeclareUnicodeCharacter{3088}{\yo} \usepackage{tikz, tikz-cd, mathtools, amssymb, stmaryrd,xcolor} \usetikzlibrary{matrix,arrows} \usetikzlibrary{backgrounds,fit,positioning,calc,shapes} \usetikzlibrary{decorations.pathreplacing} \usetikzlibrary{decorations.pathmorphing} \usetikzlibrary{decorations.markings} % `tikz-cd` is necessary to draw commutative diagrams. \RequirePackage{tikz-cd} % `amssymb` is necessary for `\lrcorner` and `\ulcorner`. \RequirePackage{amssymb} % `calc` is necessary to draw curved arrows. \usetikzlibrary{calc} % `pathmorphing` is necessary to draw squiggly arrows. \usetikzlibrary{decorations.pathmorphing} % `spath3` is necessary to draw shortened edges. \usetikzlibrary{spath3} % A TikZ style for curved arrows of a fixed height, due to AndréC. \tikzset{curve/.style={settings={#1},to path={(\tikztostart) .. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) .. (\tikztotarget)\tikztonodes}}, settings/.code={\tikzset{quiver/.cd,#1} \def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}}, quiver/.cd,pos/.initial=0.35,height/.initial=0} % A TikZ style for shortening paths without the poor behaviour of `shorten <' and `shorten >'. \tikzset{between/.style n args={2}{/tikz/spath/at end path construction={ \tikzset{spath/split at keep middle={current}{#1}{#2}} }}} % TikZ arrowhead/tail styles. \tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}} \tikzset{2tail/.code={\pgfsetarrowsstart{Implies[reversed]}}} \tikzset{2tail reversed/.code={\pgfsetarrowsstart{Implies}}} % TikZ arrow styles. \tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}} \newcommand{\triplecolon}{% \mathrel{\vbox{\baselineskip=2pt \hbox{.}\hbox{.}\hbox{.}}}% } \DeclareUnicodeCharacter{2AF6}{\triplecolon} \usepackage{mathpartir} ]]> Then a natural model has sigma types if all morphisms are small. Specifically, we have an isomorphism udmj30}{} \newcommand\yo{\!\text{\usefont{U}{min}{m}{n}\symbol{'207}}\!} \DeclareUnicodeCharacter{3088}{\yo} \usepackage{tikz, tikz-cd, mathtools, amssymb, stmaryrd,xcolor} \usetikzlibrary{matrix,arrows} \usetikzlibrary{backgrounds,fit,positioning,calc,shapes} \usetikzlibrary{decorations.pathreplacing} \usetikzlibrary{decorations.pathmorphing} \usetikzlibrary{decorations.markings} % `tikz-cd` is necessary to draw commutative diagrams. \RequirePackage{tikz-cd} % `amssymb` is necessary for `\lrcorner` and `\ulcorner`. \RequirePackage{amssymb} % `calc` is necessary to draw curved arrows. \usetikzlibrary{calc} % `pathmorphing` is necessary to draw squiggly arrows. \usetikzlibrary{decorations.pathmorphing} % `spath3` is necessary to draw shortened edges. \usetikzlibrary{spath3} % A TikZ style for curved arrows of a fixed height, due to AndréC. \tikzset{curve/.style={settings={#1},to path={(\tikztostart) .. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) .. (\tikztotarget)\tikztonodes}}, settings/.code={\tikzset{quiver/.cd,#1} \def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}}, quiver/.cd,pos/.initial=0.35,height/.initial=0} % A TikZ style for shortening paths without the poor behaviour of `shorten <' and `shorten >'. \tikzset{between/.style n args={2}{/tikz/spath/at end path construction={ \tikzset{spath/split at keep middle={current}{#1}{#2}} }}} % TikZ arrowhead/tail styles. \tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}} \tikzset{2tail/.code={\pgfsetarrowsstart{Implies[reversed]}}} \tikzset{2tail reversed/.code={\pgfsetarrowsstart{Implies}}} % TikZ arrow styles. \tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}} \newcommand{\triplecolon}{% \mathrel{\vbox{\baselineskip=2pt \hbox{.}\hbox{.}\hbox{.}}}% } \DeclareUnicodeCharacter{2AF6}{\triplecolon} \usepackage{mathpartir} ]]> More generally, a natural model has sigma types if all composites of small morphisms are small. Owen Lynch 2025 2 28 https://forest.topos.site/ocl-007Y/ https://forest.topos.site/ocl-007Y /ocl-007Y/ Sigma types via polynomial functors In this section, we give an alternative presentation of the semantics for § , which introduces some categorical machinery that we will want to use later on. This draws on material from Reference , as well as Reference . Recall that the category of presheaves on a small category is a topos, and so in specific it is a locally cartesian closed category. Thus, for any morphism of presheaves , there is a polynomial functor defined in the internal language by and defined externally by where and are the unique morphisms to the terminal presheaf. We are particularly interested in for a natural model; we will be able to use this endofunctor to interpret the rules of inference for sigma types and pi types. Why this works is that, morally speaking and working internal to , the polynomial looks like where is the internal version of the display map . is short for “element”; is the type of elements of . This gives an intuition for things like the composite, that is As a sigma type (which is a sigma type in the internal logic of presheaves on , not yet a sigma type in the type theory) shows up in the exponent for this composite, it is no surprise that this composite can be used to define sigma types in the type theory. Specifically, the existence of sigma types is equivalent to having a cartesian morphism Owen Lynch 2025 3 12 https://forest.topos.site/ocl-009R/ https://forest.topos.site/ocl-009R /ocl-009R/ Cartesian morphism of polynomial functors definition Given polynomial functors and where and are type families, then a cartesian morphism from to consists of a pair , where Unwrapping definition in the case of and , we get a pair , where We can identify with the formation rule for sigma types, and with the introduction, elimination, beta, and eta rules, which form the four parts of an equivalence as usual. It turns out that (modulo some complications around the difference between equality and isomorphism), if we also give a unit type via a cartesian morphism , then is in fact a cartesian monad (a monoid in the category of polynomial functors and cartesian morphisms with composition as the monoidal product). The left and right unit laws for this monad witness that, internal to the type theory and the associativity witnesses that (again internally) There are a variety of approaches to handling that these are isomorphisms and not equalities; in Reference Awodey and Newstead handle this with pseudomonads, and in Reference , Aberlé and Spivak handle this by taking their metatheory to be homotopy type theory rather than set theory. Owen Lynch 2025 2 28 https://forest.topos.site/ocl-007Z/ https://forest.topos.site/ocl-007Z /ocl-007Z/ Dependent records A useful consequence of working with the universe as a polynomial functor is that the -ary generalization of sigma types, e.g. dependent records, becomes quite straightforwards to state. To do this, we first need to introduce the concept of the free polynomial monad on a polynomial functor. Owen Lynch 2025 3 12 https://forest.topos.site/ocl-009S/ https://forest.topos.site/ocl-009S /ocl-009S/ The free polynomial monad on a polynomial functor definition Given any locally cartesian closed category (or, more generally, a category with finite limits and a chosen class of exponentiable maps), there is a category of polynomial monads , which are monoids in the category of polynomial functors on . There is a forgetful functor . Depending on the category , there may or may not be a left adjoint to this forgetful functor; for the existence of this left adjoint may be proved via transfinite induction, see Reference for details. However, for a specific polynomial , we may ask if there is a free polynomial monad on , which is equivalent to asking if the slice category has an initial object; if the left adjoint existed, this is where it would have to send . We will take this (an initial object of ) to be our definition of the free polynomial monad on , and call this . In “good” cases (for instance, polynomial functors on set with finite degrees), the free polynomial monad on a polynomial functor can be compuuted as the colimit of where , and , being the identity polynomial. Intuitively, this colimit is something like Thus, a cartesian map gives a “record type” for every arity simultaneously (classical sigma types are given by ), and if we furthermore assume that this is an algebra for the free monad monad we get analogous conditions to the assumption that was a monad in § . Note: perhaps even when the free monad is not computed by that specific colimit, we in fact want to use that specific colimit? Is that specific colimit still a monad, even if it is not the free monad monad? Owen Lynch 2025 2 28 https://forest.topos.site/ocl-0080/ https://forest.topos.site/ocl-0080 /ocl-0080/ Pi types The rules for pi types are analogous to § .Owen Lynch2025311https://forest.topos.site/ocl-009O/https://forest.topos.site/ocl-009O/ocl-009O/Formation for pi typesrule Owen Lynch2025311https://forest.topos.site/ocl-009P/https://forest.topos.site/ocl-009P/ocl-009P/Introduction and elimination for pi typesrule Owen Lynch2025311https://forest.topos.site/ocl-009Q/https://forest.topos.site/ocl-009Q/ocl-009Q/Beta and eta for pi typesrule Following Reference , this corresponds to the existence of a pullback square udmj30}{} \newcommand\yo{\!\text{\usefont{U}{min}{m}{n}\symbol{'207}}\!} \DeclareUnicodeCharacter{3088}{\yo} \usepackage{tikz, tikz-cd, mathtools, amssymb, stmaryrd,xcolor} \usetikzlibrary{matrix,arrows} \usetikzlibrary{backgrounds,fit,positioning,calc,shapes} \usetikzlibrary{decorations.pathreplacing} \usetikzlibrary{decorations.pathmorphing} \usetikzlibrary{decorations.markings} % `tikz-cd` is necessary to draw commutative diagrams. \RequirePackage{tikz-cd} % `amssymb` is necessary for `\lrcorner` and `\ulcorner`. \RequirePackage{amssymb} % `calc` is necessary to draw curved arrows. \usetikzlibrary{calc} % `pathmorphing` is necessary to draw squiggly arrows. \usetikzlibrary{decorations.pathmorphing} % `spath3` is necessary to draw shortened edges. \usetikzlibrary{spath3} % A TikZ style for curved arrows of a fixed height, due to AndréC. \tikzset{curve/.style={settings={#1},to path={(\tikztostart) .. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) .. (\tikztotarget)\tikztonodes}}, settings/.code={\tikzset{quiver/.cd,#1} \def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}}, quiver/.cd,pos/.initial=0.35,height/.initial=0} % A TikZ style for shortening paths without the poor behaviour of `shorten <' and `shorten >'. \tikzset{between/.style n args={2}{/tikz/spath/at end path construction={ \tikzset{spath/split at keep middle={current}{#1}{#2}} }}} % TikZ arrowhead/tail styles. \tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}} \tikzset{2tail/.code={\pgfsetarrowsstart{Implies[reversed]}}} \tikzset{2tail reversed/.code={\pgfsetarrowsstart{Implies}}} % TikZ arrow styles. \tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}} \newcommand{\triplecolon}{% \mathrel{\vbox{\baselineskip=2pt \hbox{.}\hbox{.}\hbox{.}}}% } \DeclareUnicodeCharacter{2AF6}{\triplecolon} \usepackage{mathpartir} ]]> Let us work out what that means, by working internally. An element of is a type with another type depending on it, that is . The morphism takes this setup to a new type , which we may identify with . An element of is a type with a term of some type depending on it, that is , and the projection downwards forgets that term. The morphism takes this setup to , which is a term of (by commutativity of the square). Then the fact that the square is a pullback gives the elimination, beta, and eta laws.We can think about this pullback square in a different way, by considering as itself a polynomial functor. In Reference , this polynomial functor is called . Then the pullback square is equivalent to a cartesian morphism from to . Owen Lynch 2025 2 28 https://forest.topos.site/ocl-0081/ https://forest.topos.site/ocl-0081 /ocl-0081/ Extensional equality types Equality types are a tricky business in type theory, because each of the two main approaches (intensional and extensional) have major drawbacks. Intensional equality types complicate the use of equality types internally (which leads to so-called “transport hell”), but extensional equality types make full derivation reconstruction from terms undecidable.From a purely logical viewpoint however, where we study the structure of derivation trees not the algorithmics of reconstructing derivations trees from terms, there is no problem with extensional equality types. Moreover, as we will see later on, there are partial derivation reconstruction algorithms for type theory with extensional equality types which are nevertheless quite usable.Without further ado, we present the rules for extensional equality types.Owen Lynch2025312https://forest.topos.site/ocl-009T/https://forest.topos.site/ocl-009T/ocl-009T/Equality formationrule We use to distinguish from judgmental equality, which uses , following the use of == in typical programming languages to check equality.Owen Lynch2025312https://forest.topos.site/ocl-009U/https://forest.topos.site/ocl-009U/ocl-009U/Equality introduction and eliminationrule The introduction rule might look slightly strange, because normally is a constructor applied to an argument, but we present the rule in this way because it corresponds closely to how one would check extensional equality in a bidirectional type checker; when one checks against an equality type, one does a conversion check between the two sides of that equality.Owen Lynch2025312https://forest.topos.site/ocl-009V/https://forest.topos.site/ocl-009V/ocl-009V/Equality beta and etaruleReally, we only need the eta rule, which states that the equality type is judgmentally contractible. The beta rule is implicit in the assumption that judgmental equality is already contractible. If we were working in a homotopy type-theoretic metatheory, where this was not the case, then would depend on the specific metatheoretic equality we chose, and we would have a beta rule which said that eliminating from gave back the same metatheoretic equality; such a perspective is explored in Reference .Equality types are interpreted by the following pullback square, which may also be thought of as a cartesian morphism of polynomial functors udmj30}{} \newcommand\yo{\!\text{\usefont{U}{min}{m}{n}\symbol{'207}}\!} \DeclareUnicodeCharacter{3088}{\yo} \usepackage{tikz, tikz-cd, mathtools, amssymb, stmaryrd,xcolor} \usetikzlibrary{matrix,arrows} \usetikzlibrary{backgrounds,fit,positioning,calc,shapes} \usetikzlibrary{decorations.pathreplacing} \usetikzlibrary{decorations.pathmorphing} \usetikzlibrary{decorations.markings} % `tikz-cd` is necessary to draw commutative diagrams. \RequirePackage{tikz-cd} % `amssymb` is necessary for `\lrcorner` and `\ulcorner`. \RequirePackage{amssymb} % `calc` is necessary to draw curved arrows. \usetikzlibrary{calc} % `pathmorphing` is necessary to draw squiggly arrows. \usetikzlibrary{decorations.pathmorphing} % `spath3` is necessary to draw shortened edges. \usetikzlibrary{spath3} % A TikZ style for curved arrows of a fixed height, due to AndréC. \tikzset{curve/.style={settings={#1},to path={(\tikztostart) .. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) .. (\tikztotarget)\tikztonodes}}, settings/.code={\tikzset{quiver/.cd,#1} \def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}}, quiver/.cd,pos/.initial=0.35,height/.initial=0} % A TikZ style for shortening paths without the poor behaviour of `shorten <' and `shorten >'. \tikzset{between/.style n args={2}{/tikz/spath/at end path construction={ \tikzset{spath/split at keep middle={current}{#1}{#2}} }}} % TikZ arrowhead/tail styles. \tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}} \tikzset{2tail/.code={\pgfsetarrowsstart{Implies[reversed]}}} \tikzset{2tail reversed/.code={\pgfsetarrowsstart{Implies}}} % TikZ arrow styles. \tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}} \newcommand{\triplecolon}{% \mathrel{\vbox{\baselineskip=2pt \hbox{.}\hbox{.}\hbox{.}}}% } \DeclareUnicodeCharacter{2AF6}{\triplecolon} \usepackage{mathpartir} ]]> This says that for any pair of terms of the same type, there is a type of equalities between them, and that type has a single element precisely in the case that the two terms are equal (that is, are in the image of the diagonal).Note that just like in § , we can assume a cartesian morphism of polynomial functors that is equivalent to the above pullback square. Owen Lynch 2025 3 12 https://forest.topos.site/ocl-009W/ https://forest.topos.site/ocl-009W /ocl-009W/ Finite limits and essentially algebraic theories If we combine the theories of sigma types and equality types, we can write down a type for any finite limit. For instance, the pullback of udmj30}{} \newcommand\yo{\!\text{\usefont{U}{min}{m}{n}\symbol{'207}}\!} \DeclareUnicodeCharacter{3088}{\yo} \usepackage{tikz, tikz-cd, mathtools, amssymb, stmaryrd,xcolor} \usetikzlibrary{matrix,arrows} \usetikzlibrary{backgrounds,fit,positioning,calc,shapes} \usetikzlibrary{decorations.pathreplacing} \usetikzlibrary{decorations.pathmorphing} \usetikzlibrary{decorations.markings} % `tikz-cd` is necessary to draw commutative diagrams. \RequirePackage{tikz-cd} % `amssymb` is necessary for `\lrcorner` and `\ulcorner`. \RequirePackage{amssymb} % `calc` is necessary to draw curved arrows. \usetikzlibrary{calc} % `pathmorphing` is necessary to draw squiggly arrows. \usetikzlibrary{decorations.pathmorphing} % `spath3` is necessary to draw shortened edges. \usetikzlibrary{spath3} % A TikZ style for curved arrows of a fixed height, due to AndréC. \tikzset{curve/.style={settings={#1},to path={(\tikztostart) .. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) .. (\tikztotarget)\tikztonodes}}, settings/.code={\tikzset{quiver/.cd,#1} \def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}}, quiver/.cd,pos/.initial=0.35,height/.initial=0} % A TikZ style for shortening paths without the poor behaviour of `shorten <' and `shorten >'. \tikzset{between/.style n args={2}{/tikz/spath/at end path construction={ \tikzset{spath/split at keep middle={current}{#1}{#2}} }}} % TikZ arrowhead/tail styles. \tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}} \tikzset{2tail/.code={\pgfsetarrowsstart{Implies[reversed]}}} \tikzset{2tail reversed/.code={\pgfsetarrowsstart{Implies}}} % TikZ arrow styles. \tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}} \newcommand{\triplecolon}{% \mathrel{\vbox{\baselineskip=2pt \hbox{.}\hbox{.}\hbox{.}}}% } \DeclareUnicodeCharacter{2AF6}{\triplecolon} \usepackage{mathpartir} ]]> may be written as .More generally, if we only have equality types, then we may write down a context for any finite limit (we can only internalize contexts to types if we have sigma types).Essentially algebraic theories are 1-theories in the 2-theory of equality types where all of the postulated primitive types are given in the empty context. For instance, we could have an essentially algebraic theory for categories with: Thus, general 1-theories in the 2-theory of equality types are a common generalization of generalized algebraic theories and essentially algebraic theories. Adding sigma types is a matter of convenience (it does not change the power of the theory), but as they are not terribly hard to implement or use, it seems natural to also have them.Thus, we call equality types + sigma types the 2-theory of finite limits. Later, we will build a type theory for talking about 1-theories in this particular 2-theory. Owen Lynch 2025 3 17 https://forest.topos.site/ocl-00BH/ https://forest.topos.site/ocl-00BH /ocl-00BH/ Non-strict semantics via display map structures Natural models are very convenient, because they faithfully interpret the strictness of substitutions. However, when discussing semantics, it is sometimes desirable to consider less-strict models, so that we can define certain operations via universal properties without needing to choose representatives for pullbacks, etc. One mathematical structure which can serve this purpose is that of a clan. Owen Lynch 2025 3 17 https://forest.topos.site/ocl-00BI/ https://forest.topos.site/ocl-00BI /ocl-00BI/ Clan definition A clan is a category equipped with a terminal object and a subclass of morphisms called display maps or fibrations, such that Every isomorphism is a display map For every object, the unique map to the terminal object is a display map Display maps are closed under pullback against arbitrary other morphisms Display maps are closed under composition The name clan is due to Reference , but the concept goes back to Reference , where clans were called “categories with display maps”. For our purposes, we want a much more lightweight notion, which is just a category equipped with a class of maps stable under pullback. We call this a display category. Given a natural model, one may construct a display category structure on where the display maps are those that are isomorphic to for some . If the natural model has sigma types, then display maps are closed under composition, and if the natural model is additionally democratic with a terminal object, then terminal projections are display maps, and gains a clan structure. We can then reformulate 2-theories in terms of postulating that certain maps defined by universal properties exist and are display maps. For instance, equality types are interpreted by asking that be a display map. The intuition is that this should be isomorphic to . Owen Lynch 2025 2 28 https://forest.topos.site/ocl-0073/ https://forest.topos.site/ocl-0073 /ocl-0073/ The 3-theory of two-level dependent type theories () Type theories that are explicitly called “two-level” have been studied for about a decade now, and used for a variety of purposes, from their original application to formulating “crisp” equality in homotopy type theory, found in Reference , to recent applications in staged metaprogramming in Reference and Reference . Owen Lynch 2025 3 12 https://forest.topos.site/ocl-00A2/ https://forest.topos.site/ocl-00A2 /ocl-00A2/ 2LTT is -level type theory remark If one carefully reads Reference , one will see that in fact there are levels, as universes in Martin-Löf type theory require levels in order for the type theory to be consistent. However, the first levels look the same as one another, and the second levels also all look the same as one another, so there are only two “meaningful” levels. However, the basic idea of two-level type theory is significantly older than a decade. Specifically, one can see classical type theories such as parametric simply typed lambda calculus and the type theory for first-order logic presented in Reference as two-level type theories. In parametric simply typed lambda calculus, the two levels are type variables and term variables, and in first-order logic the two levels are term variables and proposition variables (though, typically in first-order logic we leave the proposition variables implicit because propositions are proof-irrelevant). Owen Lynch 2025 3 12 https://forest.topos.site/ocl-009X/ https://forest.topos.site/ocl-009X /ocl-009X/ Second-order logic as three-level type theory remark One is tempted to try to formulate second-order logic (type variables, term variables, and proposition variables) as a three-level type theory. We will not pursue this in the current paper. The basic idea of a two-level type theory is to have “inner” and “outer” types. Considering the inner types and the outer types separately, they may or may not be dependent type theories, but inner types are typically allowed to depend on outer types. In this section, we will only consider two-level type theories where both inner and outer types are dependent; we might call these dependent-dependent two-level type theories. This follows the definition of two-level type theory in Reference . We will leave to future work the definition of 3-theories for dependent-simple (as in Reference ) and simple-simple (as in first order logic) two-level type theories. Owen Lynch 2025 2 28 https://forest.topos.site/ocl-0082/ https://forest.topos.site/ocl-0082 /ocl-0082/ Judgment structure of In this section, we review the judgment structure for the 3-theory of (dependent) two-level type theory. As mentioned before, this can be seen as a specific case of the general theory of dependent type theory worked out in Reference . Owen Lynch 2025 3 12 https://forest.topos.site/ocl-00A0/ https://forest.topos.site/ocl-00A0 /ocl-00A0/ Example judgments for table JudgmentPronunciation is a context In context , is an outer type In context , and are judgmentally equal outer types In context , is an term of outer type In context , are judgmentally equal terms of outer type In context , is an inner type In context , and are judgmentally equal inner types In context , is an term of inner type In context , are judgmentally equal terms of inner type We can then extend the context by both inner and outer types, so we have: Owen Lynch 2025 3 12 https://forest.topos.site/ocl-009Y/ https://forest.topos.site/ocl-009Y /ocl-009Y/ Outer context extension and variable rule rule Owen Lynch 2025 3 12 https://forest.topos.site/ocl-009Z/ https://forest.topos.site/ocl-009Z /ocl-009Z/ Inner context extension and variable rule rule We also have weakening for both types of context extension. Note that as of yet, there are no rules which explicitly make inner types and outer types interact, or break the symmetry between inner and outer types. However, because there is only one type of context, inner types may depend on outer types and vice versa. 2025 2 28 https://forest.topos.site/ocl-0083/ https://forest.topos.site/ocl-0083 /ocl-0083/ Categorical semantics for The categorical semantics for are a very simple extension of . Specifically, a model for just consists of a category along with two representable natural transformations of presheaves on , and . The judgment structure of § then translates to statements about this pair of natural transformations in precisely the same way that dependent type theory translates to statements about a single natural transformation. Owen Lynch 2025 2 28 https://forest.topos.site/ocl-0084/ https://forest.topos.site/ocl-0084 /ocl-0084/ 2-theories in and their semantics Owen Lynch 2025 2 28 https://forest.topos.site/ocl-0085/ https://forest.topos.site/ocl-0085 /ocl-0085/ Single-level 2-theories All of the 2-theories from § may be imported at either the “inner” or “outer” level. So we may speak of having outer sigma types, inner sigma types, outer pi type, or inner pi types. These are 2-theories that purely involve either outer or inner types. An example for one of these 2-theories is in example . Owen Lynch 2025 3 12 https://forest.topos.site/ocl-00A3/ https://forest.topos.site/ocl-00A3 /ocl-00A3/ Outer pi types example Owen Lynch 2025 3 12 https://forest.topos.site/ocl-00A4/ https://forest.topos.site/ocl-00A4 /ocl-00A4/ Formation for outer pi types rule Owen Lynch 2025 3 12 https://forest.topos.site/ocl-00A5/ https://forest.topos.site/ocl-00A5 /ocl-00A5/ Introduction and elimination for outer pi types rule Owen Lynch 2025 3 13 https://forest.topos.site/ocl-00A7/ https://forest.topos.site/ocl-00A7 /ocl-00A7/ Beta and eta for outer pi types rule Then the semantics for these rules are given by a cartesian morphism , just as in § . We trust that the reader could supply similar definitions for outer and inner versions for the rest of the 2-theories in § . Owen Lynch 2025 2 28 https://forest.topos.site/ocl-0086/ https://forest.topos.site/ocl-0086 /ocl-0086/ Multi-level 2-theories The interesting 2-theories in two-level type theory are those which mix the levels. Owen Lynch 2025 3 12 https://forest.topos.site/ocl-00A1/ https://forest.topos.site/ocl-00A1 /ocl-00A1/ Inclusion of inner types into outer types This 2-theory breaks the symmetry between inner and outer types, by injecting inner types into outer types. Such a 2-theory might reflect an intended semantics where outer types are somehow “larger” than inner types.For instance, in Agda there is such a inclusion from universe level 0 into universe level 1.Owen Lynch2025313https://forest.topos.site/ocl-00A8/https://forest.topos.site/ocl-00A8/ocl-00A8/Formation for inclusion of inner into outerrule Owen Lynch2025313https://forest.topos.site/ocl-00A9/https://forest.topos.site/ocl-00A9/ocl-00A9/Introduction and elimination for inclusion of inner into outerrule Owen Lynch2025313https://forest.topos.site/ocl-00AA/https://forest.topos.site/ocl-00AA/ocl-00AA/Beta and eta for inclusion of inner into outerrule The semantics for this are a cartesian morphism , or equivalently a pullback square udmj30}{} \newcommand\yo{\!\text{\usefont{U}{min}{m}{n}\symbol{'207}}\!} \DeclareUnicodeCharacter{3088}{\yo} \usepackage{tikz, tikz-cd, mathtools, amssymb, stmaryrd,xcolor} \usetikzlibrary{matrix,arrows} \usetikzlibrary{backgrounds,fit,positioning,calc,shapes} \usetikzlibrary{decorations.pathreplacing} \usetikzlibrary{decorations.pathmorphing} \usetikzlibrary{decorations.markings} % `tikz-cd` is necessary to draw commutative diagrams. \RequirePackage{tikz-cd} % `amssymb` is necessary for `\lrcorner` and `\ulcorner`. \RequirePackage{amssymb} % `calc` is necessary to draw curved arrows. \usetikzlibrary{calc} % `pathmorphing` is necessary to draw squiggly arrows. \usetikzlibrary{decorations.pathmorphing} % `spath3` is necessary to draw shortened edges. \usetikzlibrary{spath3} % A TikZ style for curved arrows of a fixed height, due to AndréC. \tikzset{curve/.style={settings={#1},to path={(\tikztostart) .. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) .. (\tikztotarget)\tikztonodes}}, settings/.code={\tikzset{quiver/.cd,#1} \def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}}, quiver/.cd,pos/.initial=0.35,height/.initial=0} % A TikZ style for shortening paths without the poor behaviour of `shorten <' and `shorten >'. \tikzset{between/.style n args={2}{/tikz/spath/at end path construction={ \tikzset{spath/split at keep middle={current}{#1}{#2}} }}} % TikZ arrowhead/tail styles. \tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}} \tikzset{2tail/.code={\pgfsetarrowsstart{Implies[reversed]}}} \tikzset{2tail reversed/.code={\pgfsetarrowsstart{Implies}}} % TikZ arrow styles. \tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}} \newcommand{\triplecolon}{% \mathrel{\vbox{\baselineskip=2pt \hbox{.}\hbox{.}\hbox{.}}}% } \DeclareUnicodeCharacter{2AF6}{\triplecolon} \usepackage{mathpartir} ]]> This pullback square says that the terms of an inner type are in bijection with the terms of the outer type . Owen Lynch 2025 3 13 https://forest.topos.site/ocl-00AB/ https://forest.topos.site/ocl-00AB /ocl-00AB/ Inner-inner-outer pi types If functions are somehow “too large” to be inner types (as would be the case, for instance, if inner types were supposed to model finite-dimensional smooth manifolds, or inner types were supposed to be statically-sized types in a systems language), it is never the less still possible to have an outer type which plays the role of a pi type for inner types. We call these “inner-inner-outer” pi types, because the domain is an inner type, the codomain is an inner type, but the pi type itself in an outer type. What we previously called “inner pi types” in § would now be called inner-inner-inner pi types. Note that we do not bother to make up different notation for all of the various pi types (inner-inner-inner, inner-inner-outer, inner-outer-outer, etc.), as a given 2-theory there is likely to not contain more than two of them, one with an inner domain and the other with an outer domain. If we end up wanting more, we will have to come up with notation. Owen Lynch 2025 3 13 https://forest.topos.site/ocl-00AC/ https://forest.topos.site/ocl-00AC /ocl-00AC/ Formation for inner-inner-outer pi types rule Owen Lynch 2025 3 13 https://forest.topos.site/ocl-00AD/ https://forest.topos.site/ocl-00AD /ocl-00AD/ Introduction and elimination for inner-inner-outer pi types rule Owen Lynch 2025 3 13 https://forest.topos.site/ocl-00AE/ https://forest.topos.site/ocl-00AE /ocl-00AE/ Beta and eta for inner-inner-outer pi types rule The semantics for inner-inner-outer pi types are a cartesian morphism . Owen Lynch 2025 3 13 https://forest.topos.site/ocl-00AF/ https://forest.topos.site/ocl-00AF /ocl-00AF/ Inner-outer-outer pi types At this point, it should be entirely routine to come up with the definition of inner-outer-outer pi types, and these are modeled by a cartesian morphism , and any other variation is similar. Owen Lynch 2025 3 13 https://forest.topos.site/ocl-00AG/ https://forest.topos.site/ocl-00AG /ocl-00AG/ Inner universe as outer type It is well-known that having a type of all types leads to inconsitency. Classically, having “universes” is done by having a -type of -types. In this section, we give the rules for having an outer type of inner types.Owen Lynch2025313https://forest.topos.site/ocl-00AH/https://forest.topos.site/ocl-00AH/ocl-00AH/Formation for inner universerule Owen Lynch2025313https://forest.topos.site/ocl-00AI/https://forest.topos.site/ocl-00AI/ocl-00AI/Introduction and elimination for inner universerule Owen Lynch2025313https://forest.topos.site/ocl-00AJ/https://forest.topos.site/ocl-00AJ/ocl-00AJ/Beta and eta for inner universerule In practice, we may elide the and the , so our formation rule would look like The semantics for this are a pullback square udmj30}{} \newcommand\yo{\!\text{\usefont{U}{min}{m}{n}\symbol{'207}}\!} \DeclareUnicodeCharacter{3088}{\yo} \usepackage{tikz, tikz-cd, mathtools, amssymb, stmaryrd,xcolor} \usetikzlibrary{matrix,arrows} \usetikzlibrary{backgrounds,fit,positioning,calc,shapes} \usetikzlibrary{decorations.pathreplacing} \usetikzlibrary{decorations.pathmorphing} \usetikzlibrary{decorations.markings} % `tikz-cd` is necessary to draw commutative diagrams. \RequirePackage{tikz-cd} % `amssymb` is necessary for `\lrcorner` and `\ulcorner`. \RequirePackage{amssymb} % `calc` is necessary to draw curved arrows. \usetikzlibrary{calc} % `pathmorphing` is necessary to draw squiggly arrows. \usetikzlibrary{decorations.pathmorphing} % `spath3` is necessary to draw shortened edges. \usetikzlibrary{spath3} % A TikZ style for curved arrows of a fixed height, due to AndréC. \tikzset{curve/.style={settings={#1},to path={(\tikztostart) .. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) .. (\tikztotarget)\tikztonodes}}, settings/.code={\tikzset{quiver/.cd,#1} \def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}}, quiver/.cd,pos/.initial=0.35,height/.initial=0} % A TikZ style for shortening paths without the poor behaviour of `shorten <' and `shorten >'. \tikzset{between/.style n args={2}{/tikz/spath/at end path construction={ \tikzset{spath/split at keep middle={current}{#1}{#2}} }}} % TikZ arrowhead/tail styles. \tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}} \tikzset{2tail/.code={\pgfsetarrowsstart{Implies[reversed]}}} \tikzset{2tail reversed/.code={\pgfsetarrowsstart{Implies}}} % TikZ arrow styles. \tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}} \newcommand{\triplecolon}{% \mathrel{\vbox{\baselineskip=2pt \hbox{.}\hbox{.}\hbox{.}}}% } \DeclareUnicodeCharacter{2AF6}{\triplecolon} \usepackage{mathpartir} ]]> Equivalently, in the language of polynomials, this is a cartesian morphism . Owen Lynch 2025 3 13 https://forest.topos.site/ocl-00AK/ https://forest.topos.site/ocl-00AK /ocl-00AK/ Inner-outer equality types In the world of generalized algebraic theories, there is a distinction between “free model” and “finitely presented model”. For instance, the free models of the theory of commutative rings are the polynomial rings , while the finitely presented models are quotients of polynomial rings . Often it is the case that deciding equality between two terms in a free model is significantly easier than deciding equality between two terms in a finitely presented model; sometimes it can even be undecidable in the finitely presented case, which happens with the theory of groups. This distinction was introduced to us in conversation with Nathan Corbyn.When we simply import equality types into the inner level, then the contexts that we can write down with only inner types include equalities. Thus, these contexts correspond to finitely-presented models. In this 2-theory, we internalize the equality of inner terms as an outer type, which allows us to still handle equalities type theoretically, but while maintaining the property that a “purely inner” context extension may not introduce any more equalities.We end up choosing to still use “inner-inner” equality types in our implementation, because they are well-handled by e-graphs, but in a different algorithmic setting we imagine the inner-outer equality types being useful for controlling where we expect equalities to happen.Owen Lynch2025313https://forest.topos.site/ocl-00AL/https://forest.topos.site/ocl-00AL/ocl-00AL/Formation for inner-outer equality typesrule Owen Lynch2025313https://forest.topos.site/ocl-00AM/https://forest.topos.site/ocl-00AM/ocl-00AM/Introduction and elimination for inner-outer equality typesrule Owen Lynch2025313https://forest.topos.site/ocl-00AN/https://forest.topos.site/ocl-00AN/ocl-00AN/Beta and eta for inner-outer equality typesrule Just like in § , there is no beta rule because we already assume that judgmental equality is contractible.The semantics for inner-outer equality types is the existence of the following pullback square. udmj30}{} \newcommand\yo{\!\text{\usefont{U}{min}{m}{n}\symbol{'207}}\!} \DeclareUnicodeCharacter{3088}{\yo} \usepackage{tikz, tikz-cd, mathtools, amssymb, stmaryrd,xcolor} \usetikzlibrary{matrix,arrows} \usetikzlibrary{backgrounds,fit,positioning,calc,shapes} \usetikzlibrary{decorations.pathreplacing} \usetikzlibrary{decorations.pathmorphing} \usetikzlibrary{decorations.markings} % `tikz-cd` is necessary to draw commutative diagrams. \RequirePackage{tikz-cd} % `amssymb` is necessary for `\lrcorner` and `\ulcorner`. \RequirePackage{amssymb} % `calc` is necessary to draw curved arrows. \usetikzlibrary{calc} % `pathmorphing` is necessary to draw squiggly arrows. \usetikzlibrary{decorations.pathmorphing} % `spath3` is necessary to draw shortened edges. \usetikzlibrary{spath3} % A TikZ style for curved arrows of a fixed height, due to AndréC. \tikzset{curve/.style={settings={#1},to path={(\tikztostart) .. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) .. (\tikztotarget)\tikztonodes}}, settings/.code={\tikzset{quiver/.cd,#1} \def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}}, quiver/.cd,pos/.initial=0.35,height/.initial=0} % A TikZ style for shortening paths without the poor behaviour of `shorten <' and `shorten >'. \tikzset{between/.style n args={2}{/tikz/spath/at end path construction={ \tikzset{spath/split at keep middle={current}{#1}{#2}} }}} % TikZ arrowhead/tail styles. \tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}} \tikzset{2tail/.code={\pgfsetarrowsstart{Implies[reversed]}}} \tikzset{2tail reversed/.code={\pgfsetarrowsstart{Implies}}} % TikZ arrow styles. \tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}} \newcommand{\triplecolon}{% \mathrel{\vbox{\baselineskip=2pt \hbox{.}\hbox{.}\hbox{.}}}% } \DeclareUnicodeCharacter{2AF6}{\triplecolon} \usepackage{mathpartir} ]]> Owen Lynch 2025 3 13 https://forest.topos.site/ocl-00AO/ https://forest.topos.site/ocl-00AO /ocl-00AO/ Element Model Type Theory as a 2-theory The type theory we have implemented to accompany this paper we call “Element Model Type Theory”. This is because it is a two-level type theory, where: The inner terms are called elements The outer terms are called models The inner types are called types The outer types are called theories The intended semantics for EMTT is that general contexts (involving inner and outer types) correspond to finite limit theories, and the category of purely-inner context extensions of a fixed context is the category of contexts for the finite limit theory presented by that fixed context. We discuss precisely how this works in § . With the machinery that we have developed for describing 2-theories in two-level type theory, we can succinctly describe EMTT as being the composite of the following 2-theories. Inclusion of inner types into outer types, § Inner universe as outer type, § Inner-inner-inner sigma types, § Outer-outer-outer sigma types, § Inner-outer-outer pi types, § Inner-inner equality types, § Owen Lynch 2025 2 28 https://forest.topos.site/ocl-0076/ https://forest.topos.site/ocl-0076 /ocl-0076/ EMTT: an implementation of finite limit theories We gave the official type theory for EMTT in § , where we showed that it was one of a large family of two-level type theories which could be built out of the basic 2-theories in two-level type theory that we gave. In this section we go into more depth about EMTT in particular. We start in § by showing off a variety of examples of EMTT code that actually type-checks, which also displays the various uses to which EMTT can be put. We then give the entire type theory for EMTT again in § , using syntax more similar to the actual syntax we use in the implementation, as a reference. In § , we give a formal account of the way in which outer types in EMTT are theories. Finally, in § and § we discuss some algorithmic aspects of the elaborator for EMTT, which is a modification of Coquand's algorithm for elaboration via normalization-by-evaluation to support two-level type theory and a limited form of extensional equality. Owen Lynch 2025 2 28 https://forest.topos.site/ocl-007I/ https://forest.topos.site/ocl-007I /ocl-007I/ An introduction to EMTT by examples In this section, we give an overview of the implemented version of EMTT. In § we have attempted to present two-level type theory in generality with maximum clarity, and thus we stuck to familiar syntax and binary versions of type formers (e.g. sigma types instead of dependent records, single-argument pi types). However, in the actual implementation we have used a slightly non-standard syntax, for a variety of reasons including ease of implementation. Owen Lynch 2025 3 13 https://forest.topos.site/ocl-00AP/ https://forest.topos.site/ocl-00AP /ocl-00AP/ The theory of graphs example We will present the theory of graphs in two ways. The first way is in “algebraic theory” style, where E is a non-dependent type and we have functions src and tgt. V; tgt: [e: E] -> V; };]]> The first part, ThAlgGraph: @theory, says that ThAlgGraph will refer to a derivation of a theory (outer type) judgment in the empty context (the empty context is indicated by the lack of square brackets after ThAlgGraph). The second part after the equals sign is the syntax for a dependent record with four fields (which we might call an outer sigma type). Each of these fields has its own theory (outer type). For instance, the theory for V is @type, which is our name for the inner universe that we called before. The theory for src is [e: E] -> V, which is an inner-outer-outer pi type, or as we call it in EMTT, a pi theory. Note that there are two implicit coercions going on to interpret V as a theory (which it needs to be in order to be the codomain of a pi theory). First, there is the coercion from V as a model (outer term) of the theory (outer type) @type to V as an type (inner type); we would write this coercion as using the notation of § . Then there is the coercion from V as a type (inner type) to V as a theory (outer type); we would write this as using the notation of § . Thus, in the notation we had before, the full pi theory would be given as . The second presentation we have for the theory of graphs is the following. @type; };]]> The first part of this, ThDepGraph: @theory, is just as before but with a different name. But in the body, instead of having two functions out of E, E is a pi theory with codomain @type, or in other words a type dependent on two elements of V. We can then convert between graphs in each style with the following code. The first line, Dep2Alg[G: ThDepGraph]: ThAlgGraph says that Dep2Alg refers to a derivation of a model of the theory ThAlgGraph in the context of a model G of the theory ThDepGraph. Then the body of the Dep2Alg declaration uses the introduction rule for dependent record theories to produce a model of ThAlgGraph given by assigning each field to a model of the appropriate theory. For instance, in the line V = G.V, we assign the field V to the model G.V of the theory @type, which is the correct theory because that is the theory that we declared the field V to be of in ThAlgGraph. And G.V is a model of the theory @type because of the elimination rule for dependent record theories allows us to do a field projection from G (a model of ThDepGraph). In the next part, where we assign the field E, we use an inner sigma type, or as we say in EMTT, a dependent record type (as opposed to theory). This implicitly uses the coercion from derivations of the type judgment to models of the theory @type, which we called in § . This dependent type contains two vertices and an edge between them. Finally, we can define the src and tgt functions by projecting out of the record type that we assigned to E. In Alg2Dep, the only somewhat new part is the definition for E. Here, we define a model of the pi theory [src: V, tgt: V] -> @type via a lambda abstraction [src, tgt] ↦ ... and then a dependent record type. The dependent record type has one field of type , and then two fields which store proofs that the source and target of the first field are src and tgt respectively, which use equality types. We leave the latter two fields unnamed, because we will not need to use them explicitly (we learn more about how this works in § ). Owen Lynch 2025 3 13 https://forest.topos.site/ocl-00AQ/ https://forest.topos.site/ocl-00AQ /ocl-00AQ/ The theory of rings, compositionally example In this example, we show how to build up the theory of rings compositionally. This is quite similar to the way that rings would be defined in a full dependent type theory, but notice how it works very naturally with the type/theory distinction and does not require a full dependent type theory. We start with the theory of a monoid structure on a type. t; unit: t; lident: [x: t] -> op[unit, x] == x; rident: [x: t] -> op[x, unit] == x; assoc: [x: t, y: t, z: t] -> op[op[x, y], z] == op[x, op[y, z]]; };]]> Again, this binds ThMonoidOn to a derivation of a theory in the context of a model t of the theory @type. The body of this theory is a dependent record theory with five fields, which respectively model: The monoid operation The unit The left identity law for the unit The right identity law for the unit The associativity law for the monoid operation All of the theories of these fields are pi theories, with the exception of unit which uses the implicit coercion from types to theories to turn t into a theory. We can then layer the theory for an abelian group on top of this. { elt: t; _: m.op[x, elt] == m.unit; }; comm: [x: t, y: t] -> m.op[x, y] == m.op[y, x]; };]]> This shows off in multiple ways how it is useful to have a real type theory when forming finite limit theories. For instance, we see that a field does not have to be a type constructor, term constructor, or axiom, it can also be a previously defined theory. Also, we see that we can specify the codomain of inv to be the type of inverses of x (specified as a dependent record type). Then a ring consists of an abelian group and a monoid on the same type, along with a distributive law between them. times.op[x, plus.m.op[y, z]] == plus.m.op[times.op[x, y], times.op[x, z]]; };]]> Ideally, we would have some support for “opening” a dependent record so that its fields were in scope, possibly renaming them in the process, so that we could write x * (y + z) == (x * y) + (x * z) instead of the actual code for dist, but this syntax at least makes it quite clear what is going on. We can finish by producing the theory of a ring, rather than a ring on a type: Owen Lynch 2025 3 13 https://forest.topos.site/ocl-00AR/ https://forest.topos.site/ocl-00AR /ocl-00AR/ Lens-based systems theory example We can do a fair bit of lens-based systems theory in EMTT, following chapter 1 of Reference . The following definitions could be instead given in Agda or Lean, but doing them in EMTT instead has certain advantages. First of all, the base and fiber in an arena are types not theories. This means that we don't have to worry about universes or function types showing up in the state spaces of our dynamical systems. In fact, in base EMTT the only type that one can write down in the empty context is the unit type. However, if we gave ourselves a primitive ring object , then types that we could write down in the empty context correspond to sub-objects of specified by algebraic equations, which are finite-dimensional geometric objects appropriate for serving as the state space of a dynamical system. If we went even simpler, and only gave ourselves a primitive type with no operations , then types we could write down in the empty context correspond to finite sets, and then lenses correspond to wiring diagrams. The point is, the EMTT setup gives us the flexibility to narrowly restrict what a type is, while still allowing abstraction in the form of theories. Without further ado, we present the theories for lens-based system theory, starting with the theory of a dependent arena. @type; };]]> We can then give a definition of lens between two arenas, which is given by forward and backwards maps. B.base; bwd: [x: A.base, y: B.fiber[fwd[x]]] -> A.fiber[x]; };]]> We can use these to give a definition of lens composition. We can write down systems if we give a definition of tangent bundle. For now we use the “discrete tangent” (which is appropriate for modeling discrete-time systems). Then a system on an arena can be given as Such a system is a dependent Moore machine with interface A. Thus, such a system is already “open” in one way. But another way in which a system could be open is for the system have “holes” into which one is expected to plug other systems. This is the case for a wiring diagram, for instance. Such an “incomplete” system may be expressed as a “system in the context of other systems”, such as the following (where A, B, C are some fixed arenas): Filling in the ... directly is slightly painful, but the point is that this type theory has a place for such “higher-order” systems, the syntax for which could be derived from either a DSL or an actual graphical wiring diagram editor. Owen Lynch 2025 2 28 https://forest.topos.site/ocl-007J/ https://forest.topos.site/ocl-007J /ocl-007J/ Type theory of EMTT Owen Lynch 2025 1 31 https://forest.topos.site/ocl-005V/ https://forest.topos.site/ocl-005V /ocl-005V/ Rules of EMTT Type is a theory. Types are theories. Pi theories. Sigma theories. Sigma types. Equality types. Owen Lynch 2025 3 17 https://forest.topos.site/ocl-00BG/ https://forest.topos.site/ocl-00BG /ocl-00BG/ A model for EMTT in lex categories Lex is a shortening of “left exact”, which how people in homological algebra say “finite limit-preserving”. It happens that the word “lex” is much shorter than “finite limit-preserving”, so it has been taken up by the community at large. We say “lex category” to mean a category with all finite limits, and “lex functor” to mean a functor which preserves all finite limits. In this section, we discuss a model for EMTT with category of contexts given by . Immediately, there are problems with this, because is a 2-category, and it may be that some of our constructions only work up to equivalence rather than up to isomorphism so we may not simply work in the 1-skeleton. We conjecture that there exists a 2-equivalent category to in which the constructions that we do are all defined up to the correct level of strictness, but we do not pursue the development of this 2-category. One thing to note is that in order to be slightly less confusing about duals, we will work in and consider copresheaves of types, terms, etc. rather than working in and using presheaves. Owen Lynch 2025 3 19 https://forest.topos.site/ocl-00BJ/ https://forest.topos.site/ocl-00BJ /ocl-00BJ/ Contexts interpretation In order to have semantics in , we must identify contexts with lex categories, and substitutions with lex functors. The intution for this is that a context is sent to the category of inner extensions of ; that is, an object is a inner type telescope . We will make this more precise later. Owen Lynch 2025 3 19 https://forest.topos.site/ocl-00BK/ https://forest.topos.site/ocl-00BK /ocl-00BK/ Types (inner types) interpretation As EMTT has inner sigma types, an inner type telescope (e.g., context extension comprised only of inner types, as in interpretation ) may be identified with a type in context , and as we are working loosely, we will do this without further comment, so means that is an object of . Then lex functors act on inner types covariantly, as required. Owen Lynch 2025 3 19 https://forest.topos.site/ocl-00BL/ https://forest.topos.site/ocl-00BL /ocl-00BL/ Elements (inner terms) interpretation A element is interpreted as a global section . Owen Lynch 2025 3 19 https://forest.topos.site/ocl-00BM/ https://forest.topos.site/ocl-00BM /ocl-00BM/ Theories (outer types) interpretation If we are to be consistent then, a context extension must be interpreted as a lex functor. In the case that is comprised solely of inner types, then this lex functor is etalé. For general context extensions, we will eventually identify them with a certain presentation of lex functors (see interpretation ), but for now we can simply think of them as general lex functors. In other words, we interpret theories in a context as lex functors out of . Given a substitution and an theory in context , the action of is defined by pushout: udmj30}{} \newcommand\yo{\!\text{\usefont{U}{min}{m}{n}\symbol{'207}}\!} \DeclareUnicodeCharacter{3088}{\yo} \usepackage{tikz, tikz-cd, mathtools, amssymb, stmaryrd,xcolor} \usetikzlibrary{matrix,arrows} \usetikzlibrary{backgrounds,fit,positioning,calc,shapes} \usetikzlibrary{decorations.pathreplacing} \usetikzlibrary{decorations.pathmorphing} \usetikzlibrary{decorations.markings} % `tikz-cd` is necessary to draw commutative diagrams. \RequirePackage{tikz-cd} % `amssymb` is necessary for `\lrcorner` and `\ulcorner`. \RequirePackage{amssymb} % `calc` is necessary to draw curved arrows. \usetikzlibrary{calc} % `pathmorphing` is necessary to draw squiggly arrows. \usetikzlibrary{decorations.pathmorphing} % `spath3` is necessary to draw shortened edges. \usetikzlibrary{spath3} % A TikZ style for curved arrows of a fixed height, due to AndréC. \tikzset{curve/.style={settings={#1},to path={(\tikztostart) .. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) .. (\tikztotarget)\tikztonodes}}, settings/.code={\tikzset{quiver/.cd,#1} \def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}}, quiver/.cd,pos/.initial=0.35,height/.initial=0} % A TikZ style for shortening paths without the poor behaviour of `shorten <' and `shorten >'. \tikzset{between/.style n args={2}{/tikz/spath/at end path construction={ \tikzset{spath/split at keep middle={current}{#1}{#2}} }}} % TikZ arrowhead/tail styles. \tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}} \tikzset{2tail/.code={\pgfsetarrowsstart{Implies[reversed]}}} \tikzset{2tail reversed/.code={\pgfsetarrowsstart{Implies}}} % TikZ arrow styles. \tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}} \newcommand{\triplecolon}{% \mathrel{\vbox{\baselineskip=2pt \hbox{.}\hbox{.}\hbox{.}}}% } \DeclareUnicodeCharacter{2AF6}{\triplecolon} \usepackage{mathpartir} ]]> Of course, now the action of substitutions on outer types is by no means strict, but we will ignore that for now. Owen Lynch 2025 3 19 https://forest.topos.site/ocl-00BN/ https://forest.topos.site/ocl-00BN /ocl-00BN/ Models interpretation If is a theory in context , then a model is interpreted as a section: udmj30}{} \newcommand\yo{\!\text{\usefont{U}{min}{m}{n}\symbol{'207}}\!} \DeclareUnicodeCharacter{3088}{\yo} \usepackage{tikz, tikz-cd, mathtools, amssymb, stmaryrd,xcolor} \usetikzlibrary{matrix,arrows} \usetikzlibrary{backgrounds,fit,positioning,calc,shapes} \usetikzlibrary{decorations.pathreplacing} \usetikzlibrary{decorations.pathmorphing} \usetikzlibrary{decorations.markings} % `tikz-cd` is necessary to draw commutative diagrams. \RequirePackage{tikz-cd} % `amssymb` is necessary for `\lrcorner` and `\ulcorner`. \RequirePackage{amssymb} % `calc` is necessary to draw curved arrows. \usetikzlibrary{calc} % `pathmorphing` is necessary to draw squiggly arrows. \usetikzlibrary{decorations.pathmorphing} % `spath3` is necessary to draw shortened edges. \usetikzlibrary{spath3} % A TikZ style for curved arrows of a fixed height, due to AndréC. \tikzset{curve/.style={settings={#1},to path={(\tikztostart) .. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) .. (\tikztotarget)\tikztonodes}}, settings/.code={\tikzset{quiver/.cd,#1} \def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}}, quiver/.cd,pos/.initial=0.35,height/.initial=0} % A TikZ style for shortening paths without the poor behaviour of `shorten <' and `shorten >'. \tikzset{between/.style n args={2}{/tikz/spath/at end path construction={ \tikzset{spath/split at keep middle={current}{#1}{#2}} }}} % TikZ arrowhead/tail styles. \tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}} \tikzset{2tail/.code={\pgfsetarrowsstart{Implies[reversed]}}} \tikzset{2tail reversed/.code={\pgfsetarrowsstart{Implies}}} % TikZ arrow styles. \tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}} \newcommand{\triplecolon}{% \mathrel{\vbox{\baselineskip=2pt \hbox{.}\hbox{.}\hbox{.}}}% } \DeclareUnicodeCharacter{2AF6}{\triplecolon} \usepackage{mathpartir} ]]> Specifically, a model is a functor such that As substitutions act on theories by pushout, the universal product of pushout gives them an action on models. We will now discuss how the various 2-theories are interpreted. Owen Lynch 2025 3 19 https://forest.topos.site/ocl-00BO/ https://forest.topos.site/ocl-00BO /ocl-00BO/ Inclusion of inner types into outer types (§ ) interpretation Given an inner type of context (that is, an object of the lex category ), we interpret the outer type as the lex functor defined by .In order for this to satisfy the inference rules § , we need to show that for any object of a lex category , sections are in bijection with morphisms . What we will actually show is that isomorphism classes of sections are in bijection with morphisms ; we will not worry about this distinction now.Going in one direction, given a morphism , we may produce a functor via udmj30}{} \newcommand\yo{\!\text{\usefont{U}{min}{m}{n}\symbol{'207}}\!} \DeclareUnicodeCharacter{3088}{\yo} \usepackage{tikz, tikz-cd, mathtools, amssymb, stmaryrd,xcolor} \usetikzlibrary{matrix,arrows} \usetikzlibrary{backgrounds,fit,positioning,calc,shapes} \usetikzlibrary{decorations.pathreplacing} \usetikzlibrary{decorations.pathmorphing} \usetikzlibrary{decorations.markings} % `tikz-cd` is necessary to draw commutative diagrams. \RequirePackage{tikz-cd} % `amssymb` is necessary for `\lrcorner` and `\ulcorner`. \RequirePackage{amssymb} % `calc` is necessary to draw curved arrows. \usetikzlibrary{calc} % `pathmorphing` is necessary to draw squiggly arrows. \usetikzlibrary{decorations.pathmorphing} % `spath3` is necessary to draw shortened edges. \usetikzlibrary{spath3} % A TikZ style for curved arrows of a fixed height, due to AndréC. \tikzset{curve/.style={settings={#1},to path={(\tikztostart) .. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) .. (\tikztotarget)\tikztonodes}}, settings/.code={\tikzset{quiver/.cd,#1} \def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}}, quiver/.cd,pos/.initial=0.35,height/.initial=0} % A TikZ style for shortening paths without the poor behaviour of `shorten <' and `shorten >'. \tikzset{between/.style n args={2}{/tikz/spath/at end path construction={ \tikzset{spath/split at keep middle={current}{#1}{#2}} }}} % TikZ arrowhead/tail styles. \tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}} \tikzset{2tail/.code={\pgfsetarrowsstart{Implies[reversed]}}} \tikzset{2tail reversed/.code={\pgfsetarrowsstart{Implies}}} % TikZ arrow styles. \tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}} \newcommand{\triplecolon}{% \mathrel{\vbox{\baselineskip=2pt \hbox{.}\hbox{.}\hbox{.}}}% } \DeclareUnicodeCharacter{2AF6}{\triplecolon} \usepackage{mathpartir} ]]>=14pt, maps to, from=0, to=1] \end {tikzcd} ]]> This is a section, because for any , we have udmj30}{} \newcommand\yo{\!\text{\usefont{U}{min}{m}{n}\symbol{'207}}\!} \DeclareUnicodeCharacter{3088}{\yo} \usepackage{tikz, tikz-cd, mathtools, amssymb, stmaryrd,xcolor} \usetikzlibrary{matrix,arrows} \usetikzlibrary{backgrounds,fit,positioning,calc,shapes} \usetikzlibrary{decorations.pathreplacing} \usetikzlibrary{decorations.pathmorphing} \usetikzlibrary{decorations.markings} % `tikz-cd` is necessary to draw commutative diagrams. \RequirePackage{tikz-cd} % `amssymb` is necessary for `\lrcorner` and `\ulcorner`. \RequirePackage{amssymb} % `calc` is necessary to draw curved arrows. \usetikzlibrary{calc} % `pathmorphing` is necessary to draw squiggly arrows. \usetikzlibrary{decorations.pathmorphing} % `spath3` is necessary to draw shortened edges. \usetikzlibrary{spath3} % A TikZ style for curved arrows of a fixed height, due to AndréC. \tikzset{curve/.style={settings={#1},to path={(\tikztostart) .. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) .. (\tikztotarget)\tikztonodes}}, settings/.code={\tikzset{quiver/.cd,#1} \def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}}, quiver/.cd,pos/.initial=0.35,height/.initial=0} % A TikZ style for shortening paths without the poor behaviour of `shorten <' and `shorten >'. \tikzset{between/.style n args={2}{/tikz/spath/at end path construction={ \tikzset{spath/split at keep middle={current}{#1}{#2}} }}} % TikZ arrowhead/tail styles. \tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}} \tikzset{2tail/.code={\pgfsetarrowsstart{Implies[reversed]}}} \tikzset{2tail reversed/.code={\pgfsetarrowsstart{Implies}}} % TikZ arrow styles. \tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}} \newcommand{\triplecolon}{% \mathrel{\vbox{\baselineskip=2pt \hbox{.}\hbox{.}\hbox{.}}}% } \DeclareUnicodeCharacter{2AF6}{\triplecolon} \usepackage{mathpartir} ]]>=15pt, maps to, from=0, to=1] \end {tikzcd} ]]> In the other direction, if we have a section , then we may apply to udmj30}{} \newcommand\yo{\!\text{\usefont{U}{min}{m}{n}\symbol{'207}}\!} \DeclareUnicodeCharacter{3088}{\yo} \usepackage{tikz, tikz-cd, mathtools, amssymb, stmaryrd,xcolor} \usetikzlibrary{matrix,arrows} \usetikzlibrary{backgrounds,fit,positioning,calc,shapes} \usetikzlibrary{decorations.pathreplacing} \usetikzlibrary{decorations.pathmorphing} \usetikzlibrary{decorations.markings} % `tikz-cd` is necessary to draw commutative diagrams. \RequirePackage{tikz-cd} % `amssymb` is necessary for `\lrcorner` and `\ulcorner`. \RequirePackage{amssymb} % `calc` is necessary to draw curved arrows. \usetikzlibrary{calc} % `pathmorphing` is necessary to draw squiggly arrows. \usetikzlibrary{decorations.pathmorphing} % `spath3` is necessary to draw shortened edges. \usetikzlibrary{spath3} % A TikZ style for curved arrows of a fixed height, due to AndréC. \tikzset{curve/.style={settings={#1},to path={(\tikztostart) .. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) .. (\tikztotarget)\tikztonodes}}, settings/.code={\tikzset{quiver/.cd,#1} \def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}}, quiver/.cd,pos/.initial=0.35,height/.initial=0} % A TikZ style for shortening paths without the poor behaviour of `shorten <' and `shorten >'. \tikzset{between/.style n args={2}{/tikz/spath/at end path construction={ \tikzset{spath/split at keep middle={current}{#1}{#2}} }}} % TikZ arrowhead/tail styles. \tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}} \tikzset{2tail/.code={\pgfsetarrowsstart{Implies[reversed]}}} \tikzset{2tail reversed/.code={\pgfsetarrowsstart{Implies}}} % TikZ arrow styles. \tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}} \newcommand{\triplecolon}{% \mathrel{\vbox{\baselineskip=2pt \hbox{.}\hbox{.}\hbox{.}}}% } \DeclareUnicodeCharacter{2AF6}{\triplecolon} \usepackage{mathpartir} ]]> which produces a morphism in . One may easily check that these two operations are inverses. Owen Lynch 2025 3 19 https://forest.topos.site/ocl-00BP/ https://forest.topos.site/ocl-00BP /ocl-00BP/ Inner universe as outer type § interpretation The universe theory is interpreted as the free lex category on a single object, which is . This works because the category of lex functors is isomorphic to itself, and so the category of sections of is likewise isomorphic to . Owen Lynch 2025 3 19 https://forest.topos.site/ocl-00BQ/ https://forest.topos.site/ocl-00BQ /ocl-00BQ/ Sigma types (inner sigma types) § interpretation A type in context is identified with an object of . Thus, we may simply forget the projection to to form an object of ; this object we identify with . It is not hard to show that morphisms may be identified with pairs of morphisms in and morphisms udmj30}{} \newcommand\yo{\!\text{\usefont{U}{min}{m}{n}\symbol{'207}}\!} \DeclareUnicodeCharacter{3088}{\yo} \usepackage{tikz, tikz-cd, mathtools, amssymb, stmaryrd,xcolor} \usetikzlibrary{matrix,arrows} \usetikzlibrary{backgrounds,fit,positioning,calc,shapes} \usetikzlibrary{decorations.pathreplacing} \usetikzlibrary{decorations.pathmorphing} \usetikzlibrary{decorations.markings} % `tikz-cd` is necessary to draw commutative diagrams. \RequirePackage{tikz-cd} % `amssymb` is necessary for `\lrcorner` and `\ulcorner`. \RequirePackage{amssymb} % `calc` is necessary to draw curved arrows. \usetikzlibrary{calc} % `pathmorphing` is necessary to draw squiggly arrows. \usetikzlibrary{decorations.pathmorphing} % `spath3` is necessary to draw shortened edges. \usetikzlibrary{spath3} % A TikZ style for curved arrows of a fixed height, due to AndréC. \tikzset{curve/.style={settings={#1},to path={(\tikztostart) .. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) .. (\tikztotarget)\tikztonodes}}, settings/.code={\tikzset{quiver/.cd,#1} \def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}}, quiver/.cd,pos/.initial=0.35,height/.initial=0} % A TikZ style for shortening paths without the poor behaviour of `shorten <' and `shorten >'. \tikzset{between/.style n args={2}{/tikz/spath/at end path construction={ \tikzset{spath/split at keep middle={current}{#1}{#2}} }}} % TikZ arrowhead/tail styles. \tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}} \tikzset{2tail/.code={\pgfsetarrowsstart{Implies[reversed]}}} \tikzset{2tail reversed/.code={\pgfsetarrowsstart{Implies}}} % TikZ arrow styles. \tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}} \newcommand{\triplecolon}{% \mathrel{\vbox{\baselineskip=2pt \hbox{.}\hbox{.}\hbox{.}}}% } \DeclareUnicodeCharacter{2AF6}{\triplecolon} \usepackage{mathpartir} ]]> in . Owen Lynch 2025 3 19 https://forest.topos.site/ocl-00BR/ https://forest.topos.site/ocl-00BR /ocl-00BR/ Sigma theories (outer sigma types) § interpretation As we have identified theories with their display maps , a sigma theory is simply the composite . Owen Lynch 2025 3 19 https://forest.topos.site/ocl-00BS/ https://forest.topos.site/ocl-00BS /ocl-00BS/ Equality types (inner equality types) § interpretation In order to interpret equality types, we need for every object in to give an object of . The diagonal works perfectly for this purpose. The only remaining 2-theory to interpret is that of pi theories (inner-outer-outer pi types). Unfortunately, the existence of pi theories requires a much more sophisticated argument than the preceding 2-theories, which will require the development of some non-trivial theory. We begin with the following lemma. Owen Lynch 2025 3 19 https://forest.topos.site/ocl-00BT/ https://forest.topos.site/ocl-00BT /ocl-00BT/ Dependent function types out of function types lemma It is well-known that locally cartesian closed categories interpret (in some sense) dependent type theory with pi types. However, if we inspect the definition of locally cartesian closed categories, we see that it says only that each slice is cartesian closed, which means that slices have function types rather than pi types. How does one get from function types to pi types?This is easiest to understand type theoretically. The idea is that we can identify elements of a pi type with those elements of the function type that are sections of the projection . Specifically, can be identified with the pullback udmj30}{} \newcommand\yo{\!\text{\usefont{U}{min}{m}{n}\symbol{'207}}\!} \DeclareUnicodeCharacter{3088}{\yo} \usepackage{tikz, tikz-cd, mathtools, amssymb, stmaryrd,xcolor} \usetikzlibrary{matrix,arrows} \usetikzlibrary{backgrounds,fit,positioning,calc,shapes} \usetikzlibrary{decorations.pathreplacing} \usetikzlibrary{decorations.pathmorphing} \usetikzlibrary{decorations.markings} % `tikz-cd` is necessary to draw commutative diagrams. \RequirePackage{tikz-cd} % `amssymb` is necessary for `\lrcorner` and `\ulcorner`. \RequirePackage{amssymb} % `calc` is necessary to draw curved arrows. \usetikzlibrary{calc} % `pathmorphing` is necessary to draw squiggly arrows. \usetikzlibrary{decorations.pathmorphing} % `spath3` is necessary to draw shortened edges. \usetikzlibrary{spath3} % A TikZ style for curved arrows of a fixed height, due to AndréC. \tikzset{curve/.style={settings={#1},to path={(\tikztostart) .. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) .. (\tikztotarget)\tikztonodes}}, settings/.code={\tikzset{quiver/.cd,#1} \def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}}, quiver/.cd,pos/.initial=0.35,height/.initial=0} % A TikZ style for shortening paths without the poor behaviour of `shorten <' and `shorten >'. \tikzset{between/.style n args={2}{/tikz/spath/at end path construction={ \tikzset{spath/split at keep middle={current}{#1}{#2}} }}} % TikZ arrowhead/tail styles. \tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}} \tikzset{2tail/.code={\pgfsetarrowsstart{Implies[reversed]}}} \tikzset{2tail reversed/.code={\pgfsetarrowsstart{Implies}}} % TikZ arrow styles. \tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}} \newcommand{\triplecolon}{% \mathrel{\vbox{\baselineskip=2pt \hbox{.}\hbox{.}\hbox{.}}}% } \DeclareUnicodeCharacter{2AF6}{\triplecolon} \usepackage{mathpartir} ]]> Thus, to establish the existence of pi theories, we must show that for any object of a lex category , is an exponentiable object of . The proof that is an exponentiable object is a modification of Theorem B4.3.1 of Reference . This shows that an -topos is exponentiable under certain conditions, and proves this by observing that is the classifying topos for some geometric theory and working explicitly with that geometric theory. As we are in the setting of lex categories, we must modify this proof. Specifically, rather than using geometric theories, we will use finite limit sketches. We will give a relatively self-contained account of sketches, but the reader may also refer to Reference , Reference , or Section 4 of Reference . Owen Lynch 2025 3 14 https://forest.topos.site/ocl-00AS/ https://forest.topos.site/ocl-00AS /ocl-00AS/ Graph definition A graph is a functor from the small category to . A finite graph is a functor from the same category to . Let be the category of all graphs, and be the full subcategory of finite graphs. Owen Lynch 2025 3 17 https://forest.topos.site/ocl-00BE/ https://forest.topos.site/ocl-00BE /ocl-00BE/ Free category on a graph definition There is a forgetful functor from categories to graphs; the free category on a graph is given by the left adjoint to this functor. We call morphisms in the free category on a graph paths in that graph. Owen Lynch 2025 3 17 https://forest.topos.site/ocl-00BD/ https://forest.topos.site/ocl-00BD /ocl-00BD/ Graph with equated paths definition A parallel path pair in a graph consists of a pair of paths in with the same start and end vertex. A graph with equated paths consists of a graph along with a subset of parallel path pairs called the equated paths. For short, we call this an EP-graph. There is a category of EP-graphs, where the objects are category presentations and the morphisms are graph homomorphisms which send equated paths to equated paths. There is a forgetful functor from to which sends a category to its underlying graph equipped with the subset of parallel path pairs where the composite of equals the composite of . This forgetful functor has a left adjoint, which sends a graph with equated paths to a quotient of the free category on given by identifying the paths in . Owen Lynch 2025 3 14 https://forest.topos.site/ocl-00AT/ https://forest.topos.site/ocl-00AT /ocl-00AT/ Diagram definition A diagram in a graph is an object of . Owen Lynch 2025 3 14 https://forest.topos.site/ocl-00AU/ https://forest.topos.site/ocl-00AU /ocl-00AU/ Cone definition Given a finite graph , let be the graph defined by Thus, is an endofunctor on . Let a cone on a graph be an object of . Owen Lynch 2025 3 14 https://forest.topos.site/ocl-00AW/ https://forest.topos.site/ocl-00AW /ocl-00AW/ Sketch definition A sketch consists of an EP-graph along with a subset of isomorphism classes of cones on , which we call “postulated limits”. A sketch morphism from to consists of an EP-graph morphism that sends postulated limits to postulated limits. Let be the category of sketches and sketch morphisms. In a more general context, some might call sketches “finite limit sketches”, but as we only consider finite limit sketches, we will simply drop the “finite limit” prefix. Owen Lynch 2025 3 14 https://forest.topos.site/ocl-00AV/ https://forest.topos.site/ocl-00AV /ocl-00AV/ The induced sketch on a category definition Given any category , there is an induced finite limit sketch, where the graph is the underlying graph of , the diagrams are the commuting diagrams, and the cones are the limit cones. Owen Lynch 2025 3 14 https://forest.topos.site/ocl-00B0/ https://forest.topos.site/ocl-00B0 /ocl-00B0/ Realization of a sketch definition There is a forgetful functor from to , which factors through definition and the forgetful functor . This forgetful functor has a left adjoint . For a sketch , we define its realization to be the composite , and denote it by . Owen Lynch 2025 3 17 https://forest.topos.site/ocl-00BF/ https://forest.topos.site/ocl-00BF /ocl-00BF/ Graphs, EP-graphs, sketches, and finitely complete categories remark There is a sequence of adjoint functors that we will use heavily for the rest of this section; we leave it to the reader to construct these adjoints. udmj30}{} \newcommand\yo{\!\text{\usefont{U}{min}{m}{n}\symbol{'207}}\!} \DeclareUnicodeCharacter{3088}{\yo} \usepackage{tikz, tikz-cd, mathtools, amssymb, stmaryrd,xcolor} \usetikzlibrary{matrix,arrows} \usetikzlibrary{backgrounds,fit,positioning,calc,shapes} \usetikzlibrary{decorations.pathreplacing} \usetikzlibrary{decorations.pathmorphing} \usetikzlibrary{decorations.markings} % `tikz-cd` is necessary to draw commutative diagrams. \RequirePackage{tikz-cd} % `amssymb` is necessary for `\lrcorner` and `\ulcorner`. \RequirePackage{amssymb} % `calc` is necessary to draw curved arrows. \usetikzlibrary{calc} % `pathmorphing` is necessary to draw squiggly arrows. \usetikzlibrary{decorations.pathmorphing} % `spath3` is necessary to draw shortened edges. \usetikzlibrary{spath3} % A TikZ style for curved arrows of a fixed height, due to AndréC. \tikzset{curve/.style={settings={#1},to path={(\tikztostart) .. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) .. (\tikztotarget)\tikztonodes}}, settings/.code={\tikzset{quiver/.cd,#1} \def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}}, quiver/.cd,pos/.initial=0.35,height/.initial=0} % A TikZ style for shortening paths without the poor behaviour of `shorten <' and `shorten >'. \tikzset{between/.style n args={2}{/tikz/spath/at end path construction={ \tikzset{spath/split at keep middle={current}{#1}{#2}} }}} % TikZ arrowhead/tail styles. \tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}} \tikzset{2tail/.code={\pgfsetarrowsstart{Implies[reversed]}}} \tikzset{2tail reversed/.code={\pgfsetarrowsstart{Implies}}} % TikZ arrow styles. \tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}} \newcommand{\triplecolon}{% \mathrel{\vbox{\baselineskip=2pt \hbox{.}\hbox{.}\hbox{.}}}% } \DeclareUnicodeCharacter{2AF6}{\triplecolon} \usepackage{mathpartir} ]]> Owen Lynch 2025 3 14 https://forest.topos.site/ocl-00AX/ https://forest.topos.site/ocl-00AX /ocl-00AX/ Pushouts in the category of sketches construction In this construction, we compute the pushout of a span of sketches. First of all, note that the forgetful functor from sketches to graphs admits a further right adjoint, which sends a graph to the sketch where all parallel pairs are equated and all cones are postulated as limits. Thus, the forgetful functor preserves colimits as well as limits, so the underlying graph of a pushout is the pushout of the underlying graphs. Knowing this, it is then not difficult to show that the equated pairs and postulated limits in the pushout are the union of the induced equated pairs and postulated limits that must exist by the fact that the injections are sketch morphisms. Owen Lynch 2025 3 14 https://forest.topos.site/ocl-00AZ/ https://forest.topos.site/ocl-00AZ /ocl-00AZ/ Sketch complex definition In this definition we will define a sketch complex, which is a sketch built up inductively in a specific way, analogous to a CW-complex in topology.Consider the following four classes of sketch inclusions, which we call generating sketch inclusions.The vertex generator, which is the sketch inclusion from the empty sketch to the singleton sketch. The edge generator, which is sketch inclusion from the two-element sketch to the walking arrow. For any , consider the graph built of a length path and a length path, with their source and targets identified. Then the equation generator for is the sketch inclusion from the free sketch on that graph to the sketch on that graph where the two paths are equated. For any finite graph , cone generator on is the sketch inclusion from the free sketch on to the sketch with underlying graph where the identity is a cone.Then a sketch complex is a sequence , where each morphism is given as a pushout against one of the generating sketch inclusions. udmj30}{} \newcommand\yo{\!\text{\usefont{U}{min}{m}{n}\symbol{'207}}\!} \DeclareUnicodeCharacter{3088}{\yo} \usepackage{tikz, tikz-cd, mathtools, amssymb, stmaryrd,xcolor} \usetikzlibrary{matrix,arrows} \usetikzlibrary{backgrounds,fit,positioning,calc,shapes} \usetikzlibrary{decorations.pathreplacing} \usetikzlibrary{decorations.pathmorphing} \usetikzlibrary{decorations.markings} % `tikz-cd` is necessary to draw commutative diagrams. \RequirePackage{tikz-cd} % `amssymb` is necessary for `\lrcorner` and `\ulcorner`. \RequirePackage{amssymb} % `calc` is necessary to draw curved arrows. \usetikzlibrary{calc} % `pathmorphing` is necessary to draw squiggly arrows. \usetikzlibrary{decorations.pathmorphing} % `spath3` is necessary to draw shortened edges. \usetikzlibrary{spath3} % A TikZ style for curved arrows of a fixed height, due to AndréC. \tikzset{curve/.style={settings={#1},to path={(\tikztostart) .. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) .. (\tikztotarget)\tikztonodes}}, settings/.code={\tikzset{quiver/.cd,#1} \def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}}, quiver/.cd,pos/.initial=0.35,height/.initial=0} % A TikZ style for shortening paths without the poor behaviour of `shorten <' and `shorten >'. \tikzset{between/.style n args={2}{/tikz/spath/at end path construction={ \tikzset{spath/split at keep middle={current}{#1}{#2}} }}} % TikZ arrowhead/tail styles. \tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}} \tikzset{2tail/.code={\pgfsetarrowsstart{Implies[reversed]}}} \tikzset{2tail reversed/.code={\pgfsetarrowsstart{Implies}}} % TikZ arrow styles. \tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}} \newcommand{\triplecolon}{% \mathrel{\vbox{\baselineskip=2pt \hbox{.}\hbox{.}\hbox{.}}}% } \DeclareUnicodeCharacter{2AF6}{\triplecolon} \usepackage{mathpartir} ]]> The sketch presented by a sketch complex is simply the last sketch, which we denote as . Owen Lynch 2025 3 14 https://forest.topos.site/ocl-00B2/ https://forest.topos.site/ocl-00B2 /ocl-00B2/ Complex extensions definition A complex extension of a sketch complex is another sketch complex with for . Note that complex extensions induce monomorphisms in the category of sketches. Often we will be lazy and say that a morphism of sketches is a presented extension; this means that there exists a presentation of and a presentation of such that the morphism is a presented extension. It is not hard to show that this is equivalent to being a mono. Owen Lynch 2025 3 19 https://forest.topos.site/ocl-00BW/ https://forest.topos.site/ocl-00BW /ocl-00BW/ Finitely presented lex categories definition A lex category is finitely presented if it is the realization of a finite sketch. Note that the category of finite sketches and Kleisli morphisms for realization is equivalent to the category of finitely presented lex categories. Owen Lynch 2025 3 19 https://forest.topos.site/ocl-00BV/ https://forest.topos.site/ocl-00BV /ocl-00BV/ All Kleisli morphisms of sketches are equivalent to complex extensions theorem Given a Kleisli morphism for between sketche complexes we can produce a sketch extension of such that and are isomorphic as objects of the coslice category under . The idea here is similar in spirit to cylinder objects in topology. We first construct the sketch , which is a sketch extension of . Then, we identify the vertices in with their images in , which can be added to via finitely many cones, and we identify the edges in with their images in , which similarly may be added to by finitely many equated paths. We are done. Owen Lynch 2025 3 19 https://forest.topos.site/ocl-00BU/ https://forest.topos.site/ocl-00BU /ocl-00BU/ Theories are complex extensions interpretation Before, we identified theories with general lex functors out of contexts. As long as we are willing to restrict to lex categories presented by finite sketches, then theorem says that it is not a significant restriction to assume that theories correspond to complex extensions. If we want to work with general lex categories, then we must be slightly more careful. We say that a morphism of lex categories is finite if it can be presented by a finite sequence of pushouts against the generating sketch inclusions of definition , in , however, rather than . Then we interpret theories as finite morphisms out of the context. Everything essentially then works in the same way as when we assumed all lex categories were presented by finite sketches (in which case all morphisms are bounded), so we make the assumption that all lex categories are presented by finite sketches in the remainder of the paper. Owen Lynch 2025 3 19 https://forest.topos.site/ocl-00BX/ https://forest.topos.site/ocl-00BX /ocl-00BX/ Etale objects of are exponentiable theorem First, recale that an etale object of corresponds to the lex functor for an object of . We can prove that this is exponentiable in two ways; one by an explicit construction using complex extensions, and one that follows more closely to Johnstone's proof in B4.3.1 of Reference . We start with the more explicit construction. Owen Lynch 2025 3 19 https://forest.topos.site/ocl-00BZ/ https://forest.topos.site/ocl-00BZ /ocl-00BZ/ proof Given a complex extension and an object of , we wish to produce a new complex extension such that for any extension , there is a bijection udmj30}{} \newcommand\yo{\!\text{\usefont{U}{min}{m}{n}\symbol{'207}}\!} \DeclareUnicodeCharacter{3088}{\yo} \usepackage{tikz, tikz-cd, mathtools, amssymb, stmaryrd,xcolor} \usetikzlibrary{matrix,arrows} \usetikzlibrary{backgrounds,fit,positioning,calc,shapes} \usetikzlibrary{decorations.pathreplacing} \usetikzlibrary{decorations.pathmorphing} \usetikzlibrary{decorations.markings} % `tikz-cd` is necessary to draw commutative diagrams. \RequirePackage{tikz-cd} % `amssymb` is necessary for `\lrcorner` and `\ulcorner`. \RequirePackage{amssymb} % `calc` is necessary to draw curved arrows. \usetikzlibrary{calc} % `pathmorphing` is necessary to draw squiggly arrows. \usetikzlibrary{decorations.pathmorphing} % `spath3` is necessary to draw shortened edges. \usetikzlibrary{spath3} % A TikZ style for curved arrows of a fixed height, due to AndréC. \tikzset{curve/.style={settings={#1},to path={(\tikztostart) .. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) .. (\tikztotarget)\tikztonodes}}, settings/.code={\tikzset{quiver/.cd,#1} \def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}}, quiver/.cd,pos/.initial=0.35,height/.initial=0} % A TikZ style for shortening paths without the poor behaviour of `shorten <' and `shorten >'. \tikzset{between/.style n args={2}{/tikz/spath/at end path construction={ \tikzset{spath/split at keep middle={current}{#1}{#2}} }}} % TikZ arrowhead/tail styles. \tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}} \tikzset{2tail/.code={\pgfsetarrowsstart{Implies[reversed]}}} \tikzset{2tail reversed/.code={\pgfsetarrowsstart{Implies}}} % TikZ arrow styles. \tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}} \newcommand{\triplecolon}{% \mathrel{\vbox{\baselineskip=2pt \hbox{.}\hbox{.}\hbox{.}}}% } \DeclareUnicodeCharacter{2AF6}{\triplecolon} \usepackage{mathpartir} ]]> Here we identify with its image in lex categories under .We construct by carefully considering what a morphism over consists of.Specifically:For every vertex that adds to , we must pick out an object of and a morphism into . For every edge that adds to , we must pick out a triangle over in Such that:Cones in over the diagram shape are sent to cones in over the diagram shape . Equated paths in are sent to equated paths in (no change)This can read directly into the construction of .That is, for each vertex that adds to , we add a vertex to along with an edge from that object to (which without loss of generality we may assume is already in ).Then for each vertex in , let be if is in , and otherwise; there is always a canonical map .For each edge that adds to from to , then add an edge and an equated path making the following commute: udmj30}{} \newcommand\yo{\!\text{\usefont{U}{min}{m}{n}\symbol{'207}}\!} \DeclareUnicodeCharacter{3088}{\yo} \usepackage{tikz, tikz-cd, mathtools, amssymb, stmaryrd,xcolor} \usetikzlibrary{matrix,arrows} \usetikzlibrary{backgrounds,fit,positioning,calc,shapes} \usetikzlibrary{decorations.pathreplacing} \usetikzlibrary{decorations.pathmorphing} \usetikzlibrary{decorations.markings} % `tikz-cd` is necessary to draw commutative diagrams. \RequirePackage{tikz-cd} % `amssymb` is necessary for `\lrcorner` and `\ulcorner`. \RequirePackage{amssymb} % `calc` is necessary to draw curved arrows. \usetikzlibrary{calc} % `pathmorphing` is necessary to draw squiggly arrows. \usetikzlibrary{decorations.pathmorphing} % `spath3` is necessary to draw shortened edges. \usetikzlibrary{spath3} % A TikZ style for curved arrows of a fixed height, due to AndréC. \tikzset{curve/.style={settings={#1},to path={(\tikztostart) .. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) .. (\tikztotarget)\tikztonodes}}, settings/.code={\tikzset{quiver/.cd,#1} \def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}}, quiver/.cd,pos/.initial=0.35,height/.initial=0} % A TikZ style for shortening paths without the poor behaviour of `shorten <' and `shorten >'. \tikzset{between/.style n args={2}{/tikz/spath/at end path construction={ \tikzset{spath/split at keep middle={current}{#1}{#2}} }}} % TikZ arrowhead/tail styles. \tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}} \tikzset{2tail/.code={\pgfsetarrowsstart{Implies[reversed]}}} \tikzset{2tail reversed/.code={\pgfsetarrowsstart{Implies}}} % TikZ arrow styles. \tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}} \newcommand{\triplecolon}{% \mathrel{\vbox{\baselineskip=2pt \hbox{.}\hbox{.}\hbox{.}}}% } \DeclareUnicodeCharacter{2AF6}{\triplecolon} \usepackage{mathpartir} ]]> For each cone that adds to of diagram shape , add a cone of diagram shape by adding in all of the canonical maps for every vertex in the original diagram.Finally, for each equated path that adds to , add the corresponding equated path with vertices replaced by and edges replaced by .By the discussion earlier, one can see that a morphism from to over is equivalent to a morphism from itno , and we are done. Owen Lynch 2025 3 19 https://forest.topos.site/ocl-00C0/ https://forest.topos.site/ocl-00C0 /ocl-00C0/ proof This proof more closely follows B4.3.1 in Johnstone. The idea is the following. We first show given a lex category and an object , is exponentiable if and only if there exists the specific exponential object exists, where is the object classifier over . We will then show that in the case , then this specific exponential does exist. Now, for the first part, the only if direction is trivial, so the important direction is the if. Suppose that exists, and let be another lex category over . Then we assume that corresponds to a complex extension of , and work inductively over the elements added to . Specifically, suppose that we have an exponential object , and that is a one-step extension of . Then is derived from by a pushout along one of the generating sketch inclusions. We consider each of the generating sketch inclusions separately. In the case of the vertex generator, then . As exponentials commute with limits (and coproduct is product in the opposite category), we have . In the case of the edge generator, then we can compute as the coinserter of udmj30}{} \newcommand\yo{\!\text{\usefont{U}{min}{m}{n}\symbol{'207}}\!} \DeclareUnicodeCharacter{3088}{\yo} \usepackage{tikz, tikz-cd, mathtools, amssymb, stmaryrd,xcolor} \usetikzlibrary{matrix,arrows} \usetikzlibrary{backgrounds,fit,positioning,calc,shapes} \usetikzlibrary{decorations.pathreplacing} \usetikzlibrary{decorations.pathmorphing} \usetikzlibrary{decorations.markings} % `tikz-cd` is necessary to draw commutative diagrams. \RequirePackage{tikz-cd} % `amssymb` is necessary for `\lrcorner` and `\ulcorner`. \RequirePackage{amssymb} % `calc` is necessary to draw curved arrows. \usetikzlibrary{calc} % `pathmorphing` is necessary to draw squiggly arrows. \usetikzlibrary{decorations.pathmorphing} % `spath3` is necessary to draw shortened edges. \usetikzlibrary{spath3} % A TikZ style for curved arrows of a fixed height, due to AndréC. \tikzset{curve/.style={settings={#1},to path={(\tikztostart) .. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) .. (\tikztotarget)\tikztonodes}}, settings/.code={\tikzset{quiver/.cd,#1} \def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}}, quiver/.cd,pos/.initial=0.35,height/.initial=0} % A TikZ style for shortening paths without the poor behaviour of `shorten <' and `shorten >'. \tikzset{between/.style n args={2}{/tikz/spath/at end path construction={ \tikzset{spath/split at keep middle={current}{#1}{#2}} }}} % TikZ arrowhead/tail styles. \tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}} \tikzset{2tail/.code={\pgfsetarrowsstart{Implies[reversed]}}} \tikzset{2tail reversed/.code={\pgfsetarrowsstart{Implies}}} % TikZ arrow styles. \tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}} \newcommand{\triplecolon}{% \mathrel{\vbox{\baselineskip=2pt \hbox{.}\hbox{.}\hbox{.}}}% } \DeclareUnicodeCharacter{2AF6}{\triplecolon} \usepackage{mathpartir} ]]> where and pick out the source and target of an edge. Thus, again as exponentials commute with limits, is given by the coinserter of udmj30}{} \newcommand\yo{\!\text{\usefont{U}{min}{m}{n}\symbol{'207}}\!} \DeclareUnicodeCharacter{3088}{\yo} \usepackage{tikz, tikz-cd, mathtools, amssymb, stmaryrd,xcolor} \usetikzlibrary{matrix,arrows} \usetikzlibrary{backgrounds,fit,positioning,calc,shapes} \usetikzlibrary{decorations.pathreplacing} \usetikzlibrary{decorations.pathmorphing} \usetikzlibrary{decorations.markings} % `tikz-cd` is necessary to draw commutative diagrams. \RequirePackage{tikz-cd} % `amssymb` is necessary for `\lrcorner` and `\ulcorner`. \RequirePackage{amssymb} % `calc` is necessary to draw curved arrows. \usetikzlibrary{calc} % `pathmorphing` is necessary to draw squiggly arrows. \usetikzlibrary{decorations.pathmorphing} % `spath3` is necessary to draw shortened edges. \usetikzlibrary{spath3} % A TikZ style for curved arrows of a fixed height, due to AndréC. \tikzset{curve/.style={settings={#1},to path={(\tikztostart) .. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) .. (\tikztotarget)\tikztonodes}}, settings/.code={\tikzset{quiver/.cd,#1} \def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}}, quiver/.cd,pos/.initial=0.35,height/.initial=0} % A TikZ style for shortening paths without the poor behaviour of `shorten <' and `shorten >'. \tikzset{between/.style n args={2}{/tikz/spath/at end path construction={ \tikzset{spath/split at keep middle={current}{#1}{#2}} }}} % TikZ arrowhead/tail styles. \tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}} \tikzset{2tail/.code={\pgfsetarrowsstart{Implies[reversed]}}} \tikzset{2tail reversed/.code={\pgfsetarrowsstart{Implies}}} % TikZ arrow styles. \tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}} \newcommand{\triplecolon}{% \mathrel{\vbox{\baselineskip=2pt \hbox{.}\hbox{.}\hbox{.}}}% } \DeclareUnicodeCharacter{2AF6}{\triplecolon} \usepackage{mathpartir} ]]> Adding a cone may be seen as making the canonical morphism into the limit of a diagram an isomorphism, which is an inverter, thus the same argument as before obtains. Finally, adding an equated path corresponds to an equifier. This concludes the first part. For the second part, we need to show that exists. But this is just the theory of an object with a morphism into , which can be seen as a special case of the reasoning in proof , so we are done. This concludes the technical exposition of the interpretation into lex categories and lex functors. It may be worthwhile to the reader to work out pi theories in some simple cases. For instance, show that if and , then the sketch for is precisely the sketch for with an edge inserted between and (and and added as cones if they don't already exist). 2025 2 28 https://forest.topos.site/ocl-007H/ https://forest.topos.site/ocl-007H /ocl-007H/ Adapting Coquand's algorithm to the two-level setting Of necessity, this section is more in the style of “developer notes” than it is a full exposition. We assume familiarity with the basic algorithm for bidirectional elaboration with normalization by evaluation, tutorials for which can be found in Reference or Reference , and the original reference for which is Reference . This is likely not terribly different from the implementation of 2ltt in Reference , as we are heavily influenced by Kovács' other type theory implementations, but we have not read carefully that implementation to give a careful contrast. The basic setup for Coquand's algorithm is something like the following. TmStx -> TmVal eval_tp : Env -> TpStx -> TpVal -- elaboration tp : RawStx -> Ctx -> Maybe (TpStx, TpVal) syn : RawStx -> Ctx -> Maybe (TmStx, TmVal, TpVal) chk : RawStx -> Ctx -> TpVal -> Maybe (TmStx, TmVal)]]> Notice that we return TmVal and TpVal from tp, syn and chk, unlike the typical bidirectional elaboration setup; this corresponds to evaluating at the same time as elaborating. In theory, it would be most efficient to do this by returning a lazy value, in practice because we are in Rust we do not do this. Even though we evaluate at the same time as elaboration, we also need a separate evaluator, because we may re-evaluate typechecked syntax in different environments at other points in time. To make this into an elaborator for two-level type theory, we simply double everything. EltStx -> EltVal eval_model : Env -> ModelStx -> ModelVal eval_type : Env -> TypeStx -> TypeVal eval_theory : Env -> TheoryStx -> TheoryVal type_ : RawStx -> Ctx -> Maybe (TypeStx, TypeVal) theory : RawStx -> Ctx -> Maybe (TheoryStx, TheoryVal) syn_elt : RawStx -> Ctx -> Maybe (EltStx, EltVal, TypeVal) chk_elt : RawStx -> Ctx -> TypeVal -> Maybe (EltStx, EltVal) syn_model : RawStx -> Ctx -> Maybe (ModelStx, ModelVal, TheoryVal) chk_model : RawStx -> Ctx -> TheoryVal -> Maybe (ModelStx, ModelVal)]]> Then we adapt various 2-theories into constructors for the various -Val types. For instance to handle § , we have an Elt constructor for ModelVal, which allows promotion of an element to a model, and a corresponding Type constructor for TheoryVal, which allows promotion of a type to a theory. This is what permits our definition of Ctx which only consists of models; we can always produce a model from an element. Similarly, we have constructors for record types, record theories, their elements and models, pi theories and lambdas, etc. Just as normal in normalization-by-evaluation, we have neutrals; the difference here is that we now have element neutrals and model neutrals. There is not much else special here, except for what we discuss in § . 2025 2 28 https://forest.topos.site/ocl-007G/ https://forest.topos.site/ocl-007G /ocl-007G/ Integrating e-graphs into normalization-by-evaluation EMTT has two interesting features. The first is the two-level type theory, which we have discussed extensively. The second is the use of e-graphs to implement partial reconstruction of derivation trees in extensive type theory.E-graphs are a data structure used to store a congruence relation over terms. We use the excellent egg implementation Reference , and we encourage reading that paper to get a better introduction to e-graphs as a concept and as a data structure.The key thing to understand here is precisely what feature of a typical type theory implementation we are forgoing in order to handle the fact that general extensive type theory is undecidable. We are forgoing full derivation reconstruction from term syntax. This seems like a bad thing. However, in practice this is already something that is given up in intensional type theory, because type annotations are required at certain points in order to make derivation reconstruction decidable. We claim that our approach to extensive type theory is analogous; sometimes one must bring certain equalities to the type checker's attention so that it may use them later on.For instance, consider the following proofs of some lemmas about rings t := R.plus.op; zero : t := R.zero; neg : [x:t] -> t := R.neg; `* : [x: t, y: t] -> t := R.mul.op; one : t := R.one; neg_is_unique : [x: t, y: t, eq: x + y == zero] -> y == neg[x]; mul_zero_is_zero: [x: t] -> x * zero == zero; negation_via_mul_neg_one: [x: t] -> neg[one] * x == neg[x]; }; LemmasImpl[t: @type, R: RingOn[t]]: Lemmas[t, R] = { neg_is_unique = [x, y, _] ↦ { nx = neg[x]; R.plus.assoc[nx, x, y]; R.plus.unit[nx]; R.plus.unit[y]; R.plus.comm[nx, zero]; R.plus.comm[y, zero]; R.plus.isinv[x]; R.plus.comm[x, nx]; @refl }; mul_zero_is_zero = [x] ↦ { R.plus.unit[zero]; R.dist[x, zero, zero]; R.plus.assoc[x * zero, x * zero, neg[x * zero]]; R.plus.isinv[x * zero]; R.plus.unit[x * zero]; @refl }; negation_via_mul_neg_one = [x] ↦ { R.mul.unit[x]; R.mul.comm[x, neg[one]]; R.dist[x, one, neg[one]]; R.plus.isinv[one]; mul_zero_is_zero[x]; neg_is_unique[x, neg[one] * x, @refl]; @refl }; };]]>In these lemmas, we cite a bunch of ring axioms (using the block/let syntax, where, for instance, R.plus.assoc[nx, x, y] is shorthand for _ = R.plus.assoc[nx, x, y]) in order to bring the corresponding equalities into the e-graph. Then type-checking @refl does a conversion check for the two sides of the equality we are trying to prove.If we insert right before @refl, then we can visualize the state of the e-graph before the conversion check, and it looks like the following: It is somewhat hard to understand what is going on in the e-graph because the pretty-printing/layout is not great, but you can see that in the dotted box containing the y node, we also have .inv with child x. This says that conversion checking neg[x] = R.plus.inv[x] with y will succeed. There are also some other nodes in that same dotted box, which represent the fact that y + zero == y and zero + y == y.The thing to note here is that conversion checks are not magical. The work happens beforehand in let-binding the relevant equations that are needed to make an equivalent program that does type-check. Currently, this is done manually, but it is not hard to imagine a tactic engine which kept applying axioms and theorems until the desired equality appeared in the e-graph; this tactic engine would implement what is known as egraph saturation in the e-graph literature.Conveniently, we only have equality types for types, and we don't have pi types (only pi theories). So one of the reasons why e-graphs aren't used in conversion checking (namely, they totally fail at handling closure) does not apply for us. This is another benefit of the two-level setup.We now discuss the specifics of how the e-graph shows up in elaboration. As mentioned before, the e-graph stores element neutrals. Neutrals in normalization by evaluation are introduced to give values for function arguments that we otherwise know nothing about. So, for instance, when type checking the body of [x, y] ↦ b, we do so in an environment where x and y are bound to neutrals.Neutrals block computation. For instance, if f is a neutral model of a pi theory, then for any value of x, f[x] is a neutral. Similarly, if r is a neutral element of a record type with a field a, then r.a is a neutral.In EMTT, we store element neutrals in an e-graph. So if f is a neutral model of a pi theory with type codomain, then when we make f[x] (which is a neutral element), we add a new e-node the the e-graph with (more or less) head given by f and arguments given by x. Then when we bring an equality into scope (for instance, while type checking the body of a function of type [x: R, y: R, e: x*x + y*y == 1] -> R), we identify the two sides of e in the e-graph.There are some subtleties around making this work correctly. For instance, if r is a neutral of record type, then we immediately eta-expand r, which adds r.a, r.b, etc. to the e-graph, and then replaces r with { a = r.a; b = r.b; ... } (and it does this recursively, so if r.b is of record type, it also gets expanded).In fact, we can think of “adding an equality to the e-graph” as a form of eta-expansion for equality types, where we replace e : a = b with @refl after identifying a and b in the e-graph. Technically, a and b may not be e-ids, they may be themselves either records or @refl. In the case of @refl, they are already the same, so we need not do anything; in the case of records, we recursively identify their fields.The other subtlety is that after we bring an equality into scope while type checking a function (e.g. by adding a neutral for one of that function's arguments), and we finish type checking that function, we need to “remove” that equality from scope. This is not something supported by e-graphs, so instead what we do is we wrap the e-graph in a reference-counted pointer and use Rust's support for copy-on-write with reference-counted pointers. Before we type-check a function we save a clone of the reference-counted pointer, and this will ensure that the next modification to the e-graph will copy it rather than mutating it in-place. Once we've finished type-checking the function, we can go back to the old e-graph.Overall, e-graphs do not change the core normalization by evaluation algorithm drastically. We are unsure how e-graphs will scale to larger proofs, or whether a good UI can be made for e-graph guided proofs, but the initial results are promising and show that there are viable approaches to extensive type theory via e-graphs. 2025 2 28 https://forest.topos.site/ocl-0077/ https://forest.topos.site/ocl-0077 /ocl-0077/ Directions for future research 2025 2 28 https://forest.topos.site/ocl-007E/ https://forest.topos.site/ocl-007E /ocl-007E/ Observational homomorphism theories and initial models Given a theory in EMTT, it is not hard to write down a theory of homomorphisms between two models of that theory. For instance, if we have the theory for monoids: t; zero: t; assoc: [x: t, y: t, z: t] -> op[x, op[y, z]] == op[op[x, y], z]; unit: [x: t] -> op[x, zero] == x; }]]>we can write down the corresponding theory for a monoid homomorphism N.t; op: [x: M.t, y: M.t] -> t[M.op[x, y]] == N.op[t[x], t[y]]; zero: t[M.zero] == N.zero; assoc: [x: M.t, y: M.t, z: M.t] -> %ap[t, op, zero, M.assoc[x, y, z]] == N.assoc[t[x], t[y], t[z]]; unit: [x: M.t] -> %ap[t, op, zero, assoc, M.unit[x]] == N.unit[t[x]]; }]]>We use some pseudo-code in the above, where produces an equality N.op[t[x], N.op[t[y], t[z]]] == N.op[N.op[t[x], t[y]], t[z]] by using M.assoc and t, op, zero. Of course, because equality types are contractible, assoc and unit are redundant, but we keep them in for completeness.Any mathematician would have no trouble taking the definition of a @theory and producing a definition of homomorphism for that theory. So the natural question to ask is whether we can automate this process?In Reference , Altenkirch, McBride and Swierstra construct “observational type theory”, in which the equality type between two elements of a type is defined by induction on the structure of . For instance, if is a record type, then is definitionally a record of equalities.A recent research project has been higher observational type theory. In the original observational type theory, equality types were always propositions. However, in order to handle homotopy type theory, this is relaxed in higher observational type theory. The benefit of this is that the univalence axiom, which identifies equalities between two types with isomorphisms between them, can be definitionally true.We propose to do something morally quite similar; an “observational homomorphism theory”, which computes based on the structure of a theory, so that we could have @Hom[Monoid, M, N] = MonoidHom[M, N]. We expect that we might be able to skirt much of the difficulty of higher observational type theory in doing this, because we don't have a universe of theories. Thus, everything can remain strictly 2-categorical, corresponding to semantics in where a homomorphism is a natural transformation between two models, seen as sections of the display map for the theory. Homomorphisms between elements of types are propositions, and likewise homomorphisms between homomorphisms themselves are also propositions.Then building on top of functionality for observational homomorphisms, we propose to add the ability to take initial models of theories.To understand why this is desirable, consider the following example. @type; }; TwoPath[G: Gr] : [x: G.V, z: G.V] -> @type = [x, z] ↦ { y: G.V; e1: G.E[x,y]; e2: G.E[y,z]; }; Joined[G: Gr] : @type = { x: G.V; z: G.V; p1: TwoPath[G][x,z]; p2: TwoPath[G][z,x]; p1.y == p2.y; }; Dump[G: Gr, g: Joined[G]]: {} = { %dump "joined.svg"; {} };]]>We include the Dump model in order to show the state of the e-graph when we have introduced G: Gr and g: Joined[G]: We can see that there are three vertices (g.x, g.y, and g.p1.y = g.p2.y) and four edges (g.p1.e1, g.p1.e2, g.p2.e1, g.p2.e2), which looks like: udmj30}{} \newcommand\yo{\!\text{\usefont{U}{min}{m}{n}\symbol{'207}}\!} \DeclareUnicodeCharacter{3088}{\yo} \usepackage{tikz, tikz-cd, mathtools, amssymb, stmaryrd,xcolor} \usetikzlibrary{matrix,arrows} \usetikzlibrary{backgrounds,fit,positioning,calc,shapes} \usetikzlibrary{decorations.pathreplacing} \usetikzlibrary{decorations.pathmorphing} \usetikzlibrary{decorations.markings} % `tikz-cd` is necessary to draw commutative diagrams. \RequirePackage{tikz-cd} % `amssymb` is necessary for `\lrcorner` and `\ulcorner`. \RequirePackage{amssymb} % `calc` is necessary to draw curved arrows. \usetikzlibrary{calc} % `pathmorphing` is necessary to draw squiggly arrows. \usetikzlibrary{decorations.pathmorphing} % `spath3` is necessary to draw shortened edges. \usetikzlibrary{spath3} % A TikZ style for curved arrows of a fixed height, due to AndréC. \tikzset{curve/.style={settings={#1},to path={(\tikztostart) .. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) .. (\tikztotarget)\tikztonodes}}, settings/.code={\tikzset{quiver/.cd,#1} \def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}}, quiver/.cd,pos/.initial=0.35,height/.initial=0} % A TikZ style for shortening paths without the poor behaviour of `shorten <' and `shorten >'. \tikzset{between/.style n args={2}{/tikz/spath/at end path construction={ \tikzset{spath/split at keep middle={current}{#1}{#2}} }}} % TikZ arrowhead/tail styles. \tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}} \tikzset{2tail/.code={\pgfsetarrowsstart{Implies[reversed]}}} \tikzset{2tail reversed/.code={\pgfsetarrowsstart{Implies}}} % TikZ arrow styles. \tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}} \newcommand{\triplecolon}{% \mathrel{\vbox{\baselineskip=2pt \hbox{.}\hbox{.}\hbox{.}}}% } \DeclareUnicodeCharacter{2AF6}{\triplecolon} \usepackage{mathpartir} ]]> If we consider the theory {G: Gr, g: Joined[G]}, this graph, along with its canonical element of Joined[G], is precisely the initial model, which we denote as @init[{G: Gr; g: Joined[G];}]. As a consequence, homomorphisms from @init[{G: Gr; g: Joined[G];}].G into another graph H are in bijection with elements of Joined[H]. To see why this is true, if we have an element h of Joined[H], then we may form the model {G = H; g = h;} of {G: Gr, g: Joined[G]}, there is then a unique homomorphism f : @Hom[{G: Gr, g: Joined[G]}, @init[{G: Gr; g: Joined[G]}], {G = H; g = h;}], and we may take f.G : @Hom[Gr, @init[{G: Gr; g: Joined[G]}].G, H].More generally, a judgment Q[G: Gr]: @type may be seen as a conjunctive query, and (due to an observation by David Dalrymple), the initial model of {G: Gr; q: Q[G];} is the initial object of the category of “graphs equipped with a result of the conjunctive query”. In database theory, this is known as the “natural model”, which may be found in the relational case as early as Reference .Another application of initial models is that although we only have records and pi theories in EMTT, the ability to ask for initial models gives us coproducts and inductive types as well! For instance, we can make binary coproducts via: apex; inr: [y: s] -> apex; }; Either[t: @type, s: @type]: @type = @init[Cocone[t, s]].apex;]]>Now, we can show that any theory in the empty context has an initial model, but this is not necessarily true in an arbitrary context. We conjecture that a theory in a context has an initial model if the theory only postulates elements of types that the theory introduces. For instance, in context A: @type, the theory { x: A; } does not have an initial model. But the theory { B: @type; f: [x: A] -> B; } does have an initial model, namely { B = A; f[x] = x; }. We expect that this check will not be so hard to implement, so that @init[T] will fail at compile time if T tries to introduce an element of an already-existing type.This conjecture is supported by the fact that the category of sections of a lex functor has an initial object if and only if is fully faithful.If a facility for taking initial models can be successfully added to EMTT, then we will witness in a single system the well-known connection between initial models of generalized algebraic theories and quotient inductive-inductive types as given in Reference .Of course, this facility will complicate the semantics of EMTT. This is because as we now have non-trivial models of @type in the empty context, we can no longer give semantics in .Fortunately, we can identify with a sub-2-category of the category of topoi, by sending a lex category to the category of presheaves on it. This is not a full sub-2-category, and we conjecture that by taking more general classes of morphisms here we may be able to interpret initial models successfully; we leave the details of this to future work. 2025 2 28 https://forest.topos.site/ocl-007F/ https://forest.topos.site/ocl-007F /ocl-007F/ Composition patterns for open systems In example , we touched on using EMTT to do lens-based systems theory. In this section, we connect EMTT to span/cospan-based systems theory, and specifically to the kind of systems that CatColab works with.One of the more basic “systems theories” in catcolab is that of causal loop diagrams. We can write down this theory as: @type; # negative edges N: [x: V, y: V] -> @type; };]]>Then we should be able to present models of CausalLoop by using the initial model trick from § . For instance, here is a causal loop diagram for a very basic infection model, where we have a population of infected people, a population of susceptible people, and an infection process. Susceptible people and infected people both increase the rate of infection, and infection decreases the population of susceptible people while increasing the population of infected people.Notice that this looks precisely like a CatColab notebook; each line is a cell that declares a vertex, positive edge, or negative edge!The initial model of {M: CausalLoop; si: SI[M];} has underlying causal loop diagram that looks like: udmj30}{} \newcommand\yo{\!\text{\usefont{U}{min}{m}{n}\symbol{'207}}\!} \DeclareUnicodeCharacter{3088}{\yo} \usepackage{tikz, tikz-cd, mathtools, amssymb, stmaryrd,xcolor} \usetikzlibrary{matrix,arrows} \usetikzlibrary{backgrounds,fit,positioning,calc,shapes} \usetikzlibrary{decorations.pathreplacing} \usetikzlibrary{decorations.pathmorphing} \usetikzlibrary{decorations.markings} % `tikz-cd` is necessary to draw commutative diagrams. \RequirePackage{tikz-cd} % `amssymb` is necessary for `\lrcorner` and `\ulcorner`. \RequirePackage{amssymb} % `calc` is necessary to draw curved arrows. \usetikzlibrary{calc} % `pathmorphing` is necessary to draw squiggly arrows. \usetikzlibrary{decorations.pathmorphing} % `spath3` is necessary to draw shortened edges. \usetikzlibrary{spath3} % A TikZ style for curved arrows of a fixed height, due to AndréC. \tikzset{curve/.style={settings={#1},to path={(\tikztostart) .. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) .. (\tikztotarget)\tikztonodes}}, settings/.code={\tikzset{quiver/.cd,#1} \def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}}, quiver/.cd,pos/.initial=0.35,height/.initial=0} % A TikZ style for shortening paths without the poor behaviour of `shorten <' and `shorten >'. \tikzset{between/.style n args={2}{/tikz/spath/at end path construction={ \tikzset{spath/split at keep middle={current}{#1}{#2}} }}} % TikZ arrowhead/tail styles. \tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}} \tikzset{2tail/.code={\pgfsetarrowsstart{Implies[reversed]}}} \tikzset{2tail reversed/.code={\pgfsetarrowsstart{Implies}}} % TikZ arrow styles. \tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}} \newcommand{\triplecolon}{% \mathrel{\vbox{\baselineskip=2pt \hbox{.}\hbox{.}\hbox{.}}}% } \DeclareUnicodeCharacter{2AF6}{\triplecolon} \usepackage{mathpartir} ]]> where we put positive edges in blue and negative edges in red, which is precisely what we expect.However, with EMTT, when we produce a derivation of D[M: CausalLoop]: @type we are not restricted to making each field in the record a primitive type. We can also use other, previously defined types. For instance, if we want a infection model with two diseases on the same population of susceptible people, we can do the following.This would be visualized by: udmj30}{} \newcommand\yo{\!\text{\usefont{U}{min}{m}{n}\symbol{'207}}\!} \DeclareUnicodeCharacter{3088}{\yo} \usepackage{tikz, tikz-cd, mathtools, amssymb, stmaryrd,xcolor} \usetikzlibrary{matrix,arrows} \usetikzlibrary{backgrounds,fit,positioning,calc,shapes} \usetikzlibrary{decorations.pathreplacing} \usetikzlibrary{decorations.pathmorphing} \usetikzlibrary{decorations.markings} % `tikz-cd` is necessary to draw commutative diagrams. \RequirePackage{tikz-cd} % `amssymb` is necessary for `\lrcorner` and `\ulcorner`. \RequirePackage{amssymb} % `calc` is necessary to draw curved arrows. \usetikzlibrary{calc} % `pathmorphing` is necessary to draw squiggly arrows. \usetikzlibrary{decorations.pathmorphing} % `spath3` is necessary to draw shortened edges. \usetikzlibrary{spath3} % A TikZ style for curved arrows of a fixed height, due to AndréC. \tikzset{curve/.style={settings={#1},to path={(\tikztostart) .. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) .. (\tikztotarget)\tikztonodes}}, settings/.code={\tikzset{quiver/.cd,#1} \def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}}, quiver/.cd,pos/.initial=0.35,height/.initial=0} % A TikZ style for shortening paths without the poor behaviour of `shorten <' and `shorten >'. \tikzset{between/.style n args={2}{/tikz/spath/at end path construction={ \tikzset{spath/split at keep middle={current}{#1}{#2}} }}} % TikZ arrowhead/tail styles. \tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}} \tikzset{2tail/.code={\pgfsetarrowsstart{Implies[reversed]}}} \tikzset{2tail reversed/.code={\pgfsetarrowsstart{Implies}}} % TikZ arrow styles. \tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}} \newcommand{\triplecolon}{% \mathrel{\vbox{\baselineskip=2pt \hbox{.}\hbox{.}\hbox{.}}}% } \DeclareUnicodeCharacter{2AF6}{\triplecolon} \usepackage{mathpartir} ]]> And one can imagine iterating this indefinitely to produce causal loop diagrams of greater and greater complexity.But that is not all we can do with EMTT. We can also express a composition pattern of causal loop diagrams, without having specific causal loop diagrams to compose.For instance, we might express the previous composite abstractly as @type]: @type = { s: M.V; first: X[s]; second: X[s]; }; SI2[M: CausalLoop]: @type = Two[M, [s] ↦ { si: SI[M]; si.susceptible == s; }];]]>We can think of X: [s: M.V] -> @type as a causal loop diagram that exposes a single vertex as its interface. The fact that this vertex has been “exposed” is what allows us to join together two causal lopp diagrams in Two.Under the hood, this is all essentially just colimits of causal loop diagrams. But the framework of EMTT provides a solution to the problem of naming in iterated colimits, by using the x.y.z syntax that programmers are familiar with.One final thing to note is that the ability to take initial models means that a derivation of SI[M: CausalLoop]: @type can no longer be identified with a conjunctive query on causal loop diagrams, as there are many types in the empty context now. So we may want to carefully restrict where initial models are allowed to be used, so that we can prove the metatheorem that a derivation of SI[M: CausalLoop]: @type is in fact a conjunctive query (as it is in EMTT without initial models). 2025 2 28 https://forest.topos.site/ocl-007K/ https://forest.topos.site/ocl-007K /ocl-007K/ Hyperdoctrines, refinement types, abstract interpretation, and egglog E-graphs support a very general form of analysis, where each e-class is annotated with an element of a meet-semilattice. When e-classes are merged, their corresponding annotations are meet-ed.This has been used to compute interval bounds on arithmetic operators. For instance, if we know that and , then we can derive that , and if we know that where , then we have . Such analyses often come under the name “abstract interpretation”; e-graphs are one tool for abstract interpretation but by no means the only one.More generally, if are unary predicate symbols, then we may consider the meet-semilattice of conjunctions of the . This would allow us to track whether certain propositions (like “ is positive” held of e-classes in an e-graph).This could allow for a kind of “extensional propositional reasoning”, where just as we store equations in the e-graph, we also store propositions. So we could have something like: @prop; neg: [x: t] -> @prop; zero: t; posneg_is_zero: [x: t, pos[x], neg[x]] -> x == zero; example1: [x: t, y: t, x == y, pos[x], neg[y]]: y == zero := [x,y,_,_,_] ↦ { posneg_is_zero[x, @it_is_known, @it_is_known]; @refl }; };]]>where @it_is_known is a constructor like @refl, which typechecks at a proposition if that proposition is true according to the analysis data stored in the e-graph.This would correspond to typing rules Again, this makes derivation reconstruction undecidable, but we can get partial derivation reconstruction in a similar way to how we already deal with equality.We could analyze the addition of propositions to EMTT as modeling some kind of hyperdoctrine over types, as expressed type-theoretically in Chapter 4 of Reference .Then the ability to take dependent records that involve propositions would be akin to refinement types as expressed in Reference ; in this paper they even say explicitly:We can think of the refinement type inference algorithm as performing abstract interpretation over a programmer-specified finite lattice of refinements of each ML type.Finally, the language that corresponds to the most basic setup for a hyperdoctrine, with no forall or exists quantifiers, is datalog. We would express a basic datalog program (taken from the wikipedia article) in the following way in (prop-enhanced) EMTT: @prop; ancestor: [x: person, y: person] -> @prop; parent_is_ancestor: [x: person, y: person, parent[x, y]] -> ancestor[x, y]; ancestor_transitive: [x: person, y: person, z: person, parent[x, y], ancestor[y, z]] -> ancestor[x,z]; xerces: person; brooke: person; damocles: person; _: parent[xerces, brooke]; _: parent[brooke, damocles]; }]]>Recent research has shown that the bottom-up evaluation model for datalog may be productively combined with equality saturation of an e-graph; the result is a language called egglog Reference . We propose that EMTT+props could form a type-theoretic interface for egglog, in the same way that base EMTT forms a type-theoretic interface for e-graphs themselves. 2025 2 28 https://forest.topos.site/ocl-007L/ https://forest.topos.site/ocl-007L /ocl-007L/ Extensions to 1ML-style module systems One of the original inspirations for EMTT was 1ML Reference . In 1ML, the observation that “modules are just big record types” is taken seriously, and the heavyweight syntactic distinction in typical ML implementations between records and modules is eliminated, to be replaced with a semantic distinction between “big types” and “little types”. The semantics for 1ML are given in the original paper by elaboration to System F. We propose that a 1ML-esque system should be understood under the general heading of two-level type theory, and given semantics in this manner from the start. Specifically, the “theories” in EMTT could serve as a module system for a real programming language (just as the module systems for ML were originally inspired by algebraic theories). In this vein, elements of a “pi theory” might be seen as a module which depended upon some kind of runtime data. To understand what this means, we give an example. In OCaml, one can write down a module signature for graphs in the following way. v val tgt : e -> v end]]> However, this is only appropriate for graphs which can be specified at compile time. In Rust, there is a trait system instead of a module system, and trait implementations get to use a “self” parameters which can hold runtime data. bool; fn has_edge(&self, e: &Self::E) -> bool; fn src(&self, e: &Self::E) -> Self::V; fn tgt(&self, e: &Self::E) -> Self::V; }]]> We can then implement this trait using a data structure, as in the following: , edges: HashSet, src: HashMap, tgt: HashMap, } impl Graph for FinGraph { type V = Vertex; type E = Edge; fn has_vertex(&self, v: &Vertex) -> bool { self.vertices.contains(v) } fn has_edge(&self, e: &Edge) -> bool { self.edges.contains(e) } fn src(&self, e: &Edge) -> Vertex { *self.src.get(e).unwrap() } fn tgt(&self, e: &Edge) -> Vertex { *self.tgt.get(e).unwrap() } }]]> We could replicate this in OCaml with something like v -> bool val has_edge : self -> e -> bool val src : self -> e -> v val tgt : self -> e -> v end]]> But this is less idiomatic than it is in Rust, because in Rust if G implements Graph, then we can use G.src(e), etc., whereas in OCaml one must do GraphImpl.src G e. In a language with an EMTT-inspired module system, using pi theories we can get the best of both worlds: use the original OCaml-style presentation of the signature for graphs, and then have Rust-style implementations using runtime data: v; tgt: [x: e] -> v; }; FinGraph: @type = ...; FinGraphImplGraph: [self: FinGraph] -> Graph = ...;]]> And indeed the semantics for pi theories in sketches, which essentially “adds an extra argument to each function and type constructor in the theory”, is precisely the translation between the first and second presentations of the theory of graphs (modulo the fact that we must simulate a self-dependent type in Rust by a fixed type along with self-dependent predicate). This would codify in the type system a common pattern that is found in both CatColab and GATlab.jl for implementations of theories. We hope in future work to understand precisely how this could work in a setting where we want to compile to high-performance code (more monomorphized than OCaml, but still with a garbage collector unlike Rust). References András Kovács 2026 https://forest.topos.site/kovacs-2026-elaborationzoo/ https://forest.topos.site/kovacs-2026-elaborationzoo /kovacs-2026-elaborationzoo/ elaboration-zoo Reference https://github.com/AndrasKovacs/elaboration-zoo Michael Lambert Evan Patterson 2024 https://forest.topos.site/lambert-2024-cartesian/ https://forest.topos.site/lambert-2024-cartesian /lambert-2024-cartesian/ Cartesian double theories: A double-categorical framework for categorical doctrines Reference 10.1016/j.aim.2024.109630 András Kovács 2024 https://forest.topos.site/kovács-2024-closurefree/ https://forest.topos.site/kovács-2024-closurefree /kovács-2024-closurefree/ Closure-Free Functional Programming in a Two-Level Type Theory Reference 10.1145/3674648 Tobias Fritz 2024 https://forest.topos.site/fritz-2024-differential/ https://forest.topos.site/fritz-2024-differential /fritz-2024-differential/ Differential geometry and general relativity with algebraifolds Reference 10.1016/j.geomphys.2024.105327 Owen Lynch Kris Brown James Fairbanks Evan Patterson 2024 https://forest.topos.site/lynch-2024-gatlab/ https://forest.topos.site/lynch-2024-gatlab /lynch-2024-gatlab/ GATlab: Modeling and Programming with Generalized Algebraic Theories Reference 10.46298/entics.14666 Sophie Libkind David I. Spivak 2024 https://forest.topos.site/libkind-2024-pattern/ https://forest.topos.site/libkind-2024-pattern /libkind-2024-pattern/ Pattern runs on matter: The free monad monad as a module over the cofree comonad comonad Reference 10.48550/ARXIV.2404.16321 C. B. Aberlé David I. Spivak 2024 https://forest.topos.site/aberlé-2024-polynomial/ https://forest.topos.site/aberlé-2024-polynomial /aberlé-2024-polynomial/ Polynomial Universes and Dependent Types Reference 10.48550/ARXIV.2409.19176 Taichi Uemura 2023 https://forest.topos.site/uemura-2023-general/ https://forest.topos.site/uemura-2023-general /uemura-2023-general/ A general framework for the semantics of type theory Reference 10.1017/s0960129523000208 Yihong Zhang Yisu Remy Wang Oliver Flatt David Cao Philip Zucker Eli Rosenthal Zachary Tatlock Max Willsey 2023 https://forest.topos.site/zhang-2023-better/ https://forest.topos.site/zhang-2023-better /zhang-2023-better/ Better Together: Unifying Datalog and Equality Saturation Reference 10.1145/3591239 Danil Annenkov Paolo Capriotti Nicolai Kraus Christian Sattler 2023 https://forest.topos.site/annenkov-2023-twolevel/ https://forest.topos.site/annenkov-2023-twolevel /annenkov-2023-twolevel/ Two-level type theory and applications Reference 10.1017/s0960129523000130 András Kovács 2022 https://forest.topos.site/kovács-2022-staged/ https://forest.topos.site/kovács-2022-staged /kovács-2022-staged/ Staged compilation with two-level type theory Reference 10.1145/3547641 András Kovács 2022 https://forest.topos.site/kovács-2022-type/ https://forest.topos.site/kovács-2022-type /kovács-2022-type/ Type-Theoretic Signatures for Algebraic Theories and Inductive Types Reference https://andraskovacs.github.io/pdfs/phdthesis_compact.pdf @phdthesis{kovács-2022-type, title = {Type-Theoretic Signatures for Algebraic Theories and Inductive Types}, author = {Kovács, András}, school = {Eötvös Loránd University}, year = {2022} } Hoang Kim Nguyen Taichi Uemura 2022 https://forest.topos.site/nguyen-2022-inftytype/ https://forest.topos.site/nguyen-2022-inftytype /nguyen-2022-inftytype/ -type theories Reference 10.48550/ARXIV.2205.00798 Clive Newstead 2021 https://forest.topos.site/newstead-2021-algebraic/ https://forest.topos.site/newstead-2021-algebraic /newstead-2021-algebraic/ Algebraic models of dependent type theory Reference 10.48550/ARXIV.2103.06155 Max Willsey Chandrakana Nandi Yisu Remy Wang Oliver Flatt Zachary Tatlock Pavel Panchekha 2021 https://forest.topos.site/willsey-2021-egg/ https://forest.topos.site/willsey-2021-egg /willsey-2021-egg/ egg: Fast and extensible equality saturation Reference 10.1145/3434304 Jet Nestruev 2020 https://forest.topos.site/nestruev-2020-smooth/ https://forest.topos.site/nestruev-2020-smooth /nestruev-2020-smooth/ Smooth Manifolds and Observables Reference 10.1007/978-3-030-45650-4 David Thrane Christiansen 2018 https://forest.topos.site/christiansen-2018-checking/ https://forest.topos.site/christiansen-2018-checking /christiansen-2018-checking/ Checking Dependent Types with Normalization by Evaluation: A Tutorial Reference https://davidchristiansen.dk/tutorials/nbe/ Steve Awodey Clive Newstead 2018 https://forest.topos.site/awodey-2018-polynomial/ https://forest.topos.site/awodey-2018-polynomial /awodey-2018-polynomial/ Polynomial pseudomonads and dependent type theory Reference 10.48550/ARXIV.1802.00997 Thorsten Altenkirch Paolo Capriotti Gabe Dijkstra Nicolai Kraus Fredrik Nordvall Forsberg 2018 https://forest.topos.site/altenkirch-2018-quotient/ https://forest.topos.site/altenkirch-2018-quotient /altenkirch-2018-quotient/ Quotient Inductive-Inductive Types Reference 10.1007/978-3-319-89366-2_16 Mike Shulman 2018 https://forest.topos.site/shulman-2018-type/ https://forest.topos.site/shulman-2018-type /shulman-2018-type/ Type 2-theories Reference https://www.math.uwo.ca/faculty/kapulkin/seminars/hottestfiles/Shulman-2018-04-12-HoTTEST.pdf Andre Joyal 2017 https://forest.topos.site/joyal-2017-notes/ https://forest.topos.site/joyal-2017-notes /joyal-2017-notes/ Notes on Clans and Tribes Reference 10.48550/ARXIV.1710.10238 Michael A. Shulman 2016 https://forest.topos.site/shulman-2016-catlog/ https://forest.topos.site/shulman-2016-catlog /shulman-2016-catlog/ Categorical logic from a categorical point of view Reference https://mikeshulman.github.io/catlog/catlog.pdf Steve Awodey 2016 https://forest.topos.site/awodey-2016-natural/ https://forest.topos.site/awodey-2016-natural /awodey-2016-natural/ Natural models of homotopy type theory Reference 10.1017/s0960129516000268 Andreas Rossberg 2015 https://forest.topos.site/rossberg-2015-ml/ https://forest.topos.site/rossberg-2015-ml /rossberg-2015-ml/ 1ML – core and modules united (F-ing first-class modules) Reference 10.1145/2858949.2784738 Stephen Lack 2009 https://forest.topos.site/lack-2009-categories/ https://forest.topos.site/lack-2009-categories /lack-2009-categories/ A 2-Categories Companion Reference 10.1007/978-1-4419-1524-5_4 Oleksandr Manzyuk 2009 https://forest.topos.site/manzyuk-2009-closed/ https://forest.topos.site/manzyuk-2009-closed /manzyuk-2009-closed/ Closed categories vs. closed multicategories Reference http://www.tac.mta.ca/tac/volumes/26/5/26-05.pdf Thorsten Altenkirch Conor McBride Wouter Swierstra 2007 https://forest.topos.site/altenkirch-2007-observational/ https://forest.topos.site/altenkirch-2007-observational /altenkirch-2007-observational/ Observational equality, now! Reference 10.1145/1292597.1292608 Tom Leinster 2004 https://forest.topos.site/leinster-2004-higher/ https://forest.topos.site/leinster-2004-higher /leinster-2004-higher/ Higher Operads, Higher Categories Reference 10.1017/cbo9780511525896 Peter T Johnstone 2002 https://forest.topos.site/johnstone-2002-sketches/ https://forest.topos.site/johnstone-2002-sketches /johnstone-2002-sketches/ Sketches of an Elephant A Topos Theory Compendium Reference 10.1093/oso/9780198515982.001.0001 Noson S. Yanofsky 2000 https://forest.topos.site/yanofsky-2000-coherence/ https://forest.topos.site/yanofsky-2000-coherence /yanofsky-2000-coherence/ Coherence, Homotopy and 2-Theories Reference 10.48550/ARXIV.MATH/0007033 Michael Barr 1999 https://forest.topos.site/barr-1999-notes/ https://forest.topos.site/barr-1999-notes /barr-1999-notes/ Notes on sketches Reference https://www.math.mcgill.ca/barr/papers/sketch.pdf J. Adamek M. Hubert J. Rosicky 1999 https://forest.topos.site/adamek-1999-essentially/ https://forest.topos.site/adamek-1999-essentially /adamek-1999-essentially/ On essentially algebraic theorries and their generalizations Reference 10.1007/s000120050111 Thierry Coquand 1996 https://forest.topos.site/coquand-1996-algorithm/ https://forest.topos.site/coquand-1996-algorithm /coquand-1996-algorithm/ An algorithm for type-checking dependent types Reference 10.1016/0167-6423(95)00021-6 J. Adamek J. Rosicky 1994 https://forest.topos.site/adamek-1994-locally/ https://forest.topos.site/adamek-1994-locally /adamek-1994-locally/ Locally Presentable and Accessible Categories Reference 10.1017/cbo9780511600579 Tim Freeman Frank Pfenning 1991 https://forest.topos.site/freeman-1991-refinement/ https://forest.topos.site/freeman-1991-refinement /freeman-1991-refinement/ Refinement types for ML Reference 10.1145/113445.113468 John W. Gray 1989 https://forest.topos.site/gray-1989-category/ https://forest.topos.site/gray-1989-category /gray-1989-category/ The category of sketches as a model for algebraic semantics Reference 10.1090/conm/092/1003198 John Cartmell 1986 https://forest.topos.site/cartmell-1986-generalised/ https://forest.topos.site/cartmell-1986-generalised /cartmell-1986-generalised/ Generalised algebraic theories and contextual categories Reference 10.1016/0168-0072(86)90053-9 Joachim Lambek Phil Scott 1986 https://forest.topos.site/lambek-1986-introduction/ https://forest.topos.site/lambek-1986-introduction /lambek-1986-introduction/ Introduction to higher-order categorical logic Reference Paul Taylor 1986 https://forest.topos.site/taylor-1986-recursive/ https://forest.topos.site/taylor-1986-recursive /taylor-1986-recursive/ Recursive Domains, Indexed Category Theory and Polymorphism Reference https://ncatlab.org/nlab/files/Taylor-IndexedCategoryTheory.pdf Anders Kock Gonzalo E. Reyes 1977 https://forest.topos.site/kock-1977-doctrines/ https://forest.topos.site/kock-1977-doctrines /kock-1977-doctrines/ Doctrines in Categorical Logic Reference 10.1016/s0049-237x(08)71104-2 Ashok K. Chandra Philip M. Merlin 1977 https://forest.topos.site/chandra-1977-optimal/ https://forest.topos.site/chandra-1977-optimal /chandra-1977-optimal/ Optimal implementation of conjunctive queries in relational data bases Reference 10.1145/800105.803397 F. William Lawvere 1969 https://forest.topos.site/lawvere-1969-ordinal/ https://forest.topos.site/lawvere-1969-ordinal /lawvere-1969-ordinal/ Ordinal sums and equational doctrines Reference 10.1007/bfb0083085 https://github.com/mattearnshaw/lawvere/blob/master/pdfs/1969-ordinal-sums-and-equational-doctrines.pdf F. William Lawvere 1963 https://forest.topos.site/lawvere-1963-functorial/ https://forest.topos.site/lawvere-1963-functorial /lawvere-1963-functorial/ Functorial Semantics of Algebraic Theories and Some Algebraic Problems in the context of Functorial Semantics of Algebraic Theories Reference http://www.tac.mta.ca/tac/reprints/articles/5/tr5abs.html David Jaz Myers https://forest.topos.site/myers-2021-book/ https://forest.topos.site/myers-2021-book /myers-2021-book/ Categorical Systems Theory Reference http://davidjaz.com/Papers/DynamicalBook.pdf Ohad Kammar Robert Wright https://forest.topos.site/kammar-2024-firstclass/ https://forest.topos.site/kammar-2024-firstclass /kammar-2024-firstclass/ First-class Algebraic Presentations with Elaborator Reflection Reference https://icfp24.sigplan.org/details/tyde-2024-papers/5/First-class-Algebraic-Presentations-with-Elaborator-Reflection-Extended-Abstract- Michael Barr https://forest.topos.site/charles-wells https://forest.topos.site/barr-2005-toposes/ https://forest.topos.site/barr-2005-toposes /barr-2005-toposes/ Toposes, Triples and Theories Reference http://www.tac.mta.ca/tac/reprints/articles/12/tr12.pdf Context Backlinks Related Contributions