Start a page on categories with representable maps

]]>added pointer to

- Paul Taylor, §4.3.2 in:
*Recursive Domains, Indexed Category Theory and Polymorphism*, Cambridge (1983-7) [pdf]

simplified natural models by adding the adjoint characterization of representability, and making clear that the representable profunctor description is part of the comparison to CwFs.

]]>am taking the liberty of renaming this entry from

“categorical model of dependent types”

to the more canonical

“categorical semantics of dependent type theory”

]]>added the following chunk of references, copied over from *relation between category theory and type thory*:

The model of dependent type theory with dependent product types/dependent function types in locally cartesian closed categories was first made explicit in

- {#Seely} R. A. G. Seely,
*Locally cartesian closed categories and type theory*, Math. Proc. Camb. Phil. Soc.**95**(1984) 33-48 [doi:10.1017/S0305004100061284, pdf]

The problem with strict substitution compared to weak pullback in this argument was discussed and fixed in

{#Curien} Pierre-Louis Curien,

*Substitution up to isomorphism*, Fundamenta Informaticae,**19**1-2 (1993) 51-86 [doi:10.5555/175469.175471] and: Diagrammes**23**(1990) 43-66 [numdam:DIA_1990__23__43_0]{#Hofmann} Martin Hofmann,

*On the interpretation of type theory in locally cartesian closed categories*, in*Computer Science Logic. CSL 1994*, Lecture Notes in Computer Science**933**(1994) 427–441 [doi:10.1007/BFb0022273]

but in the process the equivalence of categories was lost. This was finally all rectified in

- {#ClairambaultDybjer} Pierre Clairambault, Peter Dybjer,
*The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories*, in*Typed lambda calculi and applications*, Lecture Notes in Comput. Sci.**6690**Springer (2011) [arXiv:1112.3456, doi:10.1007/978-3-642-21691-6_10]

and

- {#CurienGarnerHofmann} Pierre-Louis Curien, Richard Garner, Martin Hofmann,
*Revisiting the categorical interpretation of dependent type theory*, Theoretical Computer Science**546**21 (2014) 99-119 [doi:10.1016/j.tcs.2014.03.003, CurienGarnerHofmann.pdf:file]

]]>

added pointer to:

- Daniel Gratzer, Jonathan Sterling,
*Syntactic categories for dependent type theory: sketching and adequacy*[arXiv:2012.10783]

Deleted the sub-section header “References – Another overview” that was silently introduced in June 2022 (see #44 above), having now dealt with all its items.

The only reference in that June edit which was not a duplicate or a broken link was to Jacobs’ textbook (and that was literally given just as “Jacobs’ textbook” ).

]]>deleted the (ill-formed) duplicates of the following references that were silently introduced in June 2022 (see #44 above):

André Joyal,

*Notes on Clans and Tribes*[arXiv:1710.10238]Steve Awodey,

*Natural models of homotopy type theory*, Mathematical Structures in Computer Science,**28**2 (2016) 241-286 [arXiv:1406.3219, doi:10.1017/S0960129516000268]

Polished up this couple of reference items and deleted their duplication that was silently introduced in June 2022 (see #44 above):

Peter Dybjer,

*Internal type theory*, Types for proofs and programs (Torino, 1995), Lecture Notes in Comput. Sci.**1158**Springer (1996) 120-134 [doi:10.1007/3-540-61780-9_66, pdf, MR1474535]Bart Jacobs,

*Comprehension categories and the semantics of type dependency*, Theoret. Comput. Sci.**107**2 (1993) 169-207 [MR1201808, doi:10.1016/0304-3975(93)90169-T]

Deleted the following pointers also introduced in that June edit, all of which are dead (if anyone has working links, let’s add them in):

http://uf-ias-2012.wikispaces.com/file/view/cwf1.pdf/373011668/cwf1.pdf

http://uf-ias-2012.wikispaces.com/file/view/notesTT.pdf/370624132/notesTT.pdf

http://uf-ias-2012.wikispaces.com/file/view/substitution.pdf/418826938/substitution.pdf

http://uf-ias-2012.wikispaces.com/file/view/CGH-Glynn-anniv-2013.pdf/418828064/CGH-Glynn-anniv-2013.pdf

(all of these look like ill-formed URLs, but even applying the evident fixes does not make them work)

]]>added pointer to the following item (which was hinted at as “Bart Jacobs’ book” in the silent edit from June 2022):

- Bart Jacobs,
*Categorical Logic and Type Theory*, Studies in Logic and the Foundations of Mathematics**141**, Elsevier (1998) [ISBN:978-0-444-50170-7, pdf]

polished up these two bibitems and deleted their duplication that was silently introduced in June 2022 (see #44 above)

Eugenio Moggi,

*A category-theoretic account of program modules*, Math. Structures Comput. Sci.**1**1 (1991) 103-139 [MR1108806 , doi:10.1017/S0960129500000074]Andrew M. Pitts,

*Categorical logic*, in*Handbook of Logic in Computer Science***5**Oxford Univ. Press (2000) 39-128 [doi:10.1093/oso/9780198537816.003.0002, pdf, MR1859470]

On Cartmell’s article: I deleted pointer to

https://github.com/peterlefanulumsdaine/cartmell-thesis

since I can’t spot a human-readable file hosted on that page.

If anyone has a pointer to the intended pdf, let’s add it.

(But notice that I have added the doi, using which the original article may be viewed directly here )

]]>polished up these two bibitems and deleted their duplication that was silently introduced in June 2022 (see #44 above):

John Cartmell,

*Generalised algebraic theories and contextual categories*, Annals of Pure and Applied Logic Volume 32, 1986, Pages 209-243 (doi:10.1016/0168-0072(86)90053-9)Thomas Streicher,

*Semantics of type theory – Correctness, completeness and independence results*, Progress in Theoretical Computer Science, Birkhäuser (1991) [ISBN:0-8176-3594-7, doi:10.1007/978-1-4612-0433-6, MR1134134 ]

Just a heads-up that in rev 57 on June 9 a user signing as “Anonymous” had dropped code with no less than 9 sub-section headers into the References-section, the top line of the new material announcing it as “Another overview”.

I guess this block of source code was blindly copy-and-pasted from the HoTT wiki. It’s not as long as the 9 subsection headers suggest, since many of them consist of nothing but one or two bib-items.

Maybe somebody who cares about this entry might find the energy to remove this “Another overview”-subsection hierarchy and instead merge the bibitems into the previously existing list?

]]>Have fixed and completed the publication data for:

- Steve Awodey,
*Natural models of homotopy type theory*, Mathematical Structures in Computer Science,**28**2 (2016) 241-286 $[$arXiv:1406.3219, doi:10.1017/S0960129516000268$]$

and cross-linked with *natural models of homotopy type theory*

Added

- Benedikt Ahrens, Jacopo Emmenegger, Paige Randall North, Egbert Rijke,
*B-systems and C-systems are equivalent*(arXiv:2111.09948)

Typo (extra “of”)

Anonymous

]]>Added the reference

- Clive Newstead,
*Algebraic models of dependent type theory*(arXiv:2103.06155)

Thanks for adding this! I’ve only glanced at it, but it looks like a very nice addition.

]]>Add example: The big model in the category of lcc categories.

This got quite long, and it overwhelms the examples section somewhat. Let me know if it should be shortened/moved somewhere else.

]]>Also added a note and citation that the contextual core of a CwA is a right adjoint.

]]>This page still contained a claim from its original version in 2012 that the *right* adjoint splitting was better for type theory. I updated it to the modern-as-of-2014 view that the left adjoint splitting is better.

Not that that article in #34 is explicitly about dependent types, but this page is a redirect for ’comprehension category’, and is the only place as yet to add it.

At some point it would be good to get back to whatever it is that connects Paul-André et al.’s work on refinement (glimpsed at times in the article) with Mike et al.’s work on modality.

]]>Added a reference for comprehension categories

- Paul-André Melliès, Nicolas Rolland,
*Comprehension and quotient structures in the language of 2-categories*, (arXiv:2005.10015)

]]>Our main purpose and achievement in this paper is to exhibit the 2-categorical structures secretly at work in the 1-categorical approach to comprehension structures traditionally found in categorical logic.