Merge branch 'master' of github.com:mikeshulman/basictex

all.bib

@@ -16819,11 +16819,24 @@ @Book{martinlof:itt
   publisher = 	 {Bibliopolis},
   year = 	 1984}
 
-@Article{escardo-xu:brouwer-ch,
-  author = 	 {Mart{\'\i}n Escard{\'o} and Chuangjie Xu},
-  title = 	 {The inconsistency of a {Brouwerian} continuity principle with the {Curry}--{Howard} interpretation},
-  journal = 	 {Typed Lambda Calculi and Applications},
-  year = 	 2015}
+@InProceedings{escardo-xu:brouwer-ch,
+  author =	{Mart{\'i}n H{\"o}tzel Escard{\'o} and Chuangjie Xu},
+  title =	{{The Inconsistency of a Brouwerian Continuity Principle with the Curry–Howard Interpretation}},
+  booktitle =	{13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
+  pages =	{153--164},
+  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
+  ISBN =	{978-3-939897-87-3},
+  ISSN =	{1868-8969},
+  year =	{2015},
+  volume =	{38},
+  editor =	{Thorsten Altenkirch},
+  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
+  address =	{Dagstuhl, Germany},
+  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5161},
+  URN =		{urn:nbn:de:0030-drops-51618},
+  doi =		{10.4230/LIPIcs.TLCA.2015.153},
+  annote =	{Keywords: Dependent type, intensional Martin-L{\"o}f type theory, Curry-Howard interpretation, constructive mathematics, Brouwerian continuity axioms, anonymous exi}
+}
 
 @Book{beeson:fcm,
   author = 	 {Beeson, M.},
@@ -23829,6 +23842,13 @@ @Article{oliva:dialectica-ll
   number =    2,
   pages =     {269--290}}
 
+@Misc{baldwin:scaffolds,
+  author =    {John T. Baldwin},
+  title =     {Category Theory and Model Theory: Symbiotic Scaffolds},
+  howpublished = {Talk at JMM 2022, AMS Special Session on ``Competing Foundations for Mathematics: How Do We Choose?''},
+  year =      2022,
+  note =      {\url{http://homepages.math.uic.edu/~jbaldwin/pub/ams2022slidesf.pdf}}}
+
 @PhdThesis{uemura:thesis,
   author =       {Taichi Uemura},
   title =        {Abstract and concrete type theories},
@@ -23967,3 +23987,14 @@ @article{ca:pattern-matching
 numpages = {30},
 keywords = {Agda, Copatterns, Dependent pattern matching, Dependent types}
 }
+
+@article{shulman:lcm,
+  title={Affine logic for constructive mathematics},
+  volume={28},
+  DOI={10.1017/bsl.2022.28},
+  number={3},
+  journal={The Bulletin of Symbolic Logic},
+  publisher={Cambridge University Press},
+  author={Shulman, Michael},
+  year={2022},
+  pages={327--386}}

decls.tex

@@ -553,6 +553,8 @@
 \newif\ifhyperref
 \@ifpackageloaded{hyperref}{\hyperreftrue}{\hyperreffalse}
 \iftac
+% TODO: In TAC style, \currthmtype isn't getting set by the theorem environments.  They need to be a \your@thing *followed* by a \gdef\currthmtype{#2}.
+
   %% In the TAC style, all theorems are actually subsections.  So
   %% the hyperref \autoref doesn't work and we have to use our own code
   %% in any case.  We also have to hook into the \state macros instead
@@ -566,9 +568,9 @@
   \let\@defthm\newtheorem
   \def\switchtotheoremrm{\let\@defthm\newtheoremrm}
   \def\defthm#1#2#3{\@defthm{#1}{#2}} % Ignore the third argument (for cleveref only)
-  % The following allows us to use \cref for sections and figures too,
-  % as if it were cleveref.  (But not for subsections, and also not for
-  % multiple references at once.)
+  % The following allows us to use \cref for sections, subsections,
+  % and figures too, as if it were cleveref.  (But not for multiple
+  % references at once.)
   \let\your@section\section
   \def\section{\gdef\currthmtype{section}\your@section}
   \let\your@subsection\subsection