diff --git a/flake.lock b/flake.lock index 664ba68e..0d43e408 100644 --- a/flake.lock +++ b/flake.lock @@ -1,5 +1,26 @@ { "nodes": { + "bib2forester": { + "inputs": { + "flake-utils": "flake-utils", + "nixpkgs": [ + "nixpkgs" + ] + }, + "locked": { + "lastModified": 1782480966, + "narHash": "sha256-GwnoDQZ7Atb8EFrDKheM0pGRSQR9POcLglqDd/5FeJ4=", + "owner": "olynch", + "repo": "bib2forester", + "rev": "1099ec2f432c37b689870002e76f20c45c3a529e", + "type": "github" + }, + "original": { + "owner": "olynch", + "repo": "bib2forester", + "type": "github" + } + }, "flake-utils": { "inputs": { "systems": "systems" @@ -18,6 +39,24 @@ "type": "github" } }, + "flake-utils_2": { + "inputs": { + "systems": "systems_2" + }, + "locked": { + "lastModified": 1731533236, + "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "flake-utils", + "type": "github" + } + }, "nixpkgs": { "locked": { "lastModified": 1780145889, @@ -52,7 +91,8 @@ }, "root": { "inputs": { - "flake-utils": "flake-utils", + "bib2forester": "bib2forester", + "flake-utils": "flake-utils_2", "nixpkgs": "nixpkgs", "rust-overlay": "rust-overlay" } @@ -89,6 +129,21 @@ "repo": "default", "type": "github" } + }, + "systems_2": { + "locked": { + "lastModified": 1681028828, + "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", + "owner": "nix-systems", + "repo": "default", + "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", + "type": "github" + }, + "original": { + "owner": "nix-systems", + "repo": "default", + "type": "github" + } } }, "root": "root", diff --git a/flake.nix b/flake.nix index f6a52aa4..764e47e8 100644 --- a/flake.nix +++ b/flake.nix @@ -3,12 +3,17 @@ nixpkgs.url = "github:NixOS/nixpkgs/nixos-26.05"; flake-utils.url = "github:numtide/flake-utils"; rust-overlay.url = "github:oxalica/rust-overlay"; + bib2forester = { + url = "github:olynch/bib2forester"; + inputs.nixpkgs.follows = "nixpkgs"; + }; }; outputs = inputs@{ self, nixpkgs, rust-overlay, + bib2forester, ... }: inputs.flake-utils.lib.eachSystem [ "x86_64-linux" ] ( @@ -171,6 +176,7 @@ devShells.default = pkgs.mkShell { name = "coln"; buildInputs = with pkgs; [ + bib2forester.packages."${system}".default cabal-install cabal2nix coln-manual-dev diff --git a/manual/templates/plain.tree b/manual/templates/plain.tree new file mode 100644 index 00000000..a29ce570 --- /dev/null +++ b/manual/templates/plain.tree @@ -0,0 +1 @@ +\import{prelude} diff --git a/manual/theme/forester.js b/manual/theme/forester.js index 9c8b046c..a7e1b019 100644 --- a/manual/theme/forester.js +++ b/manual/theme/forester.js @@ -685,7 +685,7 @@ l0,-`+(t+144)+`c-2,-159.3,-10,-310.7,-24,-454c-53.3,-528,-210,-949.7, |[ \r ]+ ?)[ \r ]*`,Yr="[\u0300-\u036F]",G1=new RegExp(Yr+"+$"),K1="("+Bi+"+)|"+(V1+"|")+"([!-\\[\\]-\u2027\u202A-\uD7FF\uF900-\uFFFF]"+(Yr+"*")+"|[\uD800-\uDBFF][\uDC00-\uDFFF]"+(Yr+"*")+"|\\\\verb\\*([^]).*?\\4|\\\\verb([^*a-zA-Z]).*?\\5"+("|"+U1)+("|"+F1+")"),Zt=class{constructor(e,t){this.input=void 0,this.settings=void 0,this.tokenRegex=void 0,this.catcodes=void 0,this.input=e,this.settings=t,this.tokenRegex=new RegExp(K1,"g"),this.catcodes={"%":14,"~":13}}setCatcode(e,t){this.catcodes[e]=t}lex(){var e=this.input,t=this.tokenRegex.lastIndex;if(t===e.length)return new C0("EOF",new A0(this,t,t));var a=this.tokenRegex.exec(e);if(a===null||a.index!==t)throw new T("Unexpected character: '"+e[t]+"'",new C0(e[t],new A0(this,t,t+1)));var n=a[6]||a[3]||(a[2]?"\\ ":" ");if(this.catcodes[n]===14){var i=e.indexOf(` `,this.tokenRegex.lastIndex);return i===-1?(this.tokenRegex.lastIndex=e.length,this.settings.reportNonstrict("commentAtEnd","% comment has no terminating newline; LaTeX would fail because of commenting the end of math mode (e.g. $)")):this.tokenRegex.lastIndex=i+1,this.lex()}return new C0(n,new A0(this,t,this.tokenRegex.lastIndex))}},Xr=class{constructor(e,t){e===void 0&&(e={}),t===void 0&&(t={}),this.current=void 0,this.builtins=void 0,this.undefStack=void 0,this.current=t,this.builtins=e,this.undefStack=[]}beginGroup(){this.undefStack.push({})}endGroup(){if(this.undefStack.length===0)throw new T("Unbalanced namespace destruction: attempt to pop global namespace; please report this as a bug");var e=this.undefStack.pop();for(var t in e)e.hasOwnProperty(t)&&(e[t]==null?delete this.current[t]:this.current[t]=e[t])}endGroups(){for(;this.undefStack.length>0;)this.endGroup()}has(e){return this.current.hasOwnProperty(e)||this.builtins.hasOwnProperty(e)}get(e){return this.current.hasOwnProperty(e)?this.current[e]:this.builtins[e]}set(e,t,a){if(a===void 0&&(a=!1),a){for(var n=0;n0&&(this.undefStack[this.undefStack.length-1][e]=t)}else{var i=this.undefStack[this.undefStack.length-1];i&&!i.hasOwnProperty(e)&&(i[e]=this.current[e])}t==null?delete this.current[e]:this.current[e]=t}},W1=bi;d("\\noexpand",function(r){var e=r.popToken();return r.isExpandable(e.text)&&(e.noexpand=!0,e.treatAsRelax=!0),{tokens:[e],numArgs:0}});d("\\expandafter",function(r){var e=r.popToken();return r.expandOnce(!0),{tokens:[e],numArgs:0}});d("\\@firstoftwo",function(r){var e=r.consumeArgs(2);return{tokens:e[0],numArgs:0}});d("\\@secondoftwo",function(r){var e=r.consumeArgs(2);return{tokens:e[1],numArgs:0}});d("\\@ifnextchar",function(r){var e=r.consumeArgs(3);r.consumeSpaces();var t=r.future();return e[0].length===1&&e[0][0].text===t.text?{tokens:e[1],numArgs:0}:{tokens:e[2],numArgs:0}});d("\\@ifstar","\\@ifnextchar *{\\@firstoftwo{#1}}");d("\\TextOrMath",function(r){var e=r.consumeArgs(2);return r.mode==="text"?{tokens:e[0],numArgs:0}:{tokens:e[1],numArgs:0}});var qn={0:0,1:1,2:2,3:3,4:4,5:5,6:6,7:7,8:8,9:9,a:10,A:10,b:11,B:11,c:12,C:12,d:13,D:13,e:14,E:14,f:15,F:15};d("\\char",function(r){var e=r.popToken(),t,a="";if(e.text==="'")t=8,e=r.popToken();else if(e.text==='"')t=16,e=r.popToken();else if(e.text==="`")if(e=r.popToken(),e.text[0]==="\\")a=e.text.charCodeAt(1);else{if(e.text==="EOF")throw new T("\\char` missing argument");a=e.text.charCodeAt(0)}else t=10;if(t){if(a=qn[e.text],a==null||a>=t)throw new T("Invalid base-"+t+" digit "+e.text);for(var n;(n=qn[r.future().text])!=null&&n{var a=r.consumeArg().tokens;if(a.length!==1)throw new T("\\newcommand's first argument must be a macro name");var n=a[0].text,i=r.isDefined(n);if(i&&!e)throw new T("\\newcommand{"+n+"} attempting to redefine "+(n+"; use \\renewcommand"));if(!i&&!t)throw new T("\\renewcommand{"+n+"} when command "+n+" does not yet exist; use \\newcommand");var l=0;if(a=r.consumeArg().tokens,a.length===1&&a[0].text==="["){for(var u="",h=r.expandNextToken();h.text!=="]"&&h.text!=="EOF";)u+=h.text,h=r.expandNextToken();if(!u.match(/^\s*[0-9]+\s*$/))throw new T("Invalid number of arguments: "+u);l=parseInt(u),a=r.consumeArg().tokens}return r.macros.set(n,{tokens:a,numArgs:l}),""};d("\\newcommand",r=>da(r,!1,!0));d("\\renewcommand",r=>da(r,!0,!1));d("\\providecommand",r=>da(r,!0,!0));d("\\message",r=>{var e=r.consumeArgs(1)[0];return console.log(e.reverse().map(t=>t.text).join("")),""});d("\\errmessage",r=>{var e=r.consumeArgs(1)[0];return console.error(e.reverse().map(t=>t.text).join("")),""});d("\\show",r=>{var e=r.popToken(),t=e.text;return console.log(e,r.macros.get(t),se[t],K.math[t],K.text[t]),""});d("\\bgroup","{");d("\\egroup","}");d("~","\\nobreakspace");d("\\lq","`");d("\\rq","'");d("\\aa","\\r a");d("\\AA","\\r A");d("\\textcopyright","\\html@mathml{\\textcircled{c}}{\\char`\xA9}");d("\\copyright","\\TextOrMath{\\textcopyright}{\\text{\\textcopyright}}");d("\\textregistered","\\html@mathml{\\textcircled{\\scriptsize R}}{\\char`\xAE}");d("\u212C","\\mathscr{B}");d("\u2130","\\mathscr{E}");d("\u2131","\\mathscr{F}");d("\u210B","\\mathscr{H}");d("\u2110","\\mathscr{I}");d("\u2112","\\mathscr{L}");d("\u2133","\\mathscr{M}");d("\u211B","\\mathscr{R}");d("\u212D","\\mathfrak{C}");d("\u210C","\\mathfrak{H}");d("\u2128","\\mathfrak{Z}");d("\\Bbbk","\\Bbb{k}");d("\xB7","\\cdotp");d("\\llap","\\mathllap{\\textrm{#1}}");d("\\rlap","\\mathrlap{\\textrm{#1}}");d("\\clap","\\mathclap{\\textrm{#1}}");d("\\mathstrut","\\vphantom{(}");d("\\underbar","\\underline{\\text{#1}}");d("\\not",'\\html@mathml{\\mathrel{\\mathrlap\\@not}}{\\char"338}');d("\\neq","\\html@mathml{\\mathrel{\\not=}}{\\mathrel{\\char`\u2260}}");d("\\ne","\\neq");d("\u2260","\\neq");d("\\notin","\\html@mathml{\\mathrel{{\\in}\\mathllap{/\\mskip1mu}}}{\\mathrel{\\char`\u2209}}");d("\u2209","\\notin");d("\u2258","\\html@mathml{\\mathrel{=\\kern{-1em}\\raisebox{0.4em}{$\\scriptsize\\frown$}}}{\\mathrel{\\char`\u2258}}");d("\u2259","\\html@mathml{\\stackrel{\\tiny\\wedge}{=}}{\\mathrel{\\char`\u2258}}");d("\u225A","\\html@mathml{\\stackrel{\\tiny\\vee}{=}}{\\mathrel{\\char`\u225A}}");d("\u225B","\\html@mathml{\\stackrel{\\scriptsize\\star}{=}}{\\mathrel{\\char`\u225B}}");d("\u225D","\\html@mathml{\\stackrel{\\tiny\\mathrm{def}}{=}}{\\mathrel{\\char`\u225D}}");d("\u225E","\\html@mathml{\\stackrel{\\tiny\\mathrm{m}}{=}}{\\mathrel{\\char`\u225E}}");d("\u225F","\\html@mathml{\\stackrel{\\tiny?}{=}}{\\mathrel{\\char`\u225F}}");d("\u27C2","\\perp");d("\u203C","\\mathclose{!\\mkern-0.8mu!}");d("\u220C","\\notni");d("\u231C","\\ulcorner");d("\u231D","\\urcorner");d("\u231E","\\llcorner");d("\u231F","\\lrcorner");d("\xA9","\\copyright");d("\xAE","\\textregistered");d("\uFE0F","\\textregistered");d("\\ulcorner",'\\html@mathml{\\@ulcorner}{\\mathop{\\char"231c}}');d("\\urcorner",'\\html@mathml{\\@urcorner}{\\mathop{\\char"231d}}');d("\\llcorner",'\\html@mathml{\\@llcorner}{\\mathop{\\char"231e}}');d("\\lrcorner",'\\html@mathml{\\@lrcorner}{\\mathop{\\char"231f}}');d("\\vdots","\\mathord{\\varvdots\\rule{0pt}{15pt}}");d("\u22EE","\\vdots");d("\\varGamma","\\mathit{\\Gamma}");d("\\varDelta","\\mathit{\\Delta}");d("\\varTheta","\\mathit{\\Theta}");d("\\varLambda","\\mathit{\\Lambda}");d("\\varXi","\\mathit{\\Xi}");d("\\varPi","\\mathit{\\Pi}");d("\\varSigma","\\mathit{\\Sigma}");d("\\varUpsilon","\\mathit{\\Upsilon}");d("\\varPhi","\\mathit{\\Phi}");d("\\varPsi","\\mathit{\\Psi}");d("\\varOmega","\\mathit{\\Omega}");d("\\substack","\\begin{subarray}{c}#1\\end{subarray}");d("\\colon","\\nobreak\\mskip2mu\\mathpunct{}\\mathchoice{\\mkern-3mu}{\\mkern-3mu}{}{}{:}\\mskip6mu\\relax");d("\\boxed","\\fbox{$\\displaystyle{#1}$}");d("\\iff","\\DOTSB\\;\\Longleftrightarrow\\;");d("\\implies","\\DOTSB\\;\\Longrightarrow\\;");d("\\impliedby","\\DOTSB\\;\\Longleftarrow\\;");var Hn={",":"\\dotsc","\\not":"\\dotsb","+":"\\dotsb","=":"\\dotsb","<":"\\dotsb",">":"\\dotsb","-":"\\dotsb","*":"\\dotsb",":":"\\dotsb","\\DOTSB":"\\dotsb","\\coprod":"\\dotsb","\\bigvee":"\\dotsb","\\bigwedge":"\\dotsb","\\biguplus":"\\dotsb","\\bigcap":"\\dotsb","\\bigcup":"\\dotsb","\\prod":"\\dotsb","\\sum":"\\dotsb","\\bigotimes":"\\dotsb","\\bigoplus":"\\dotsb","\\bigodot":"\\dotsb","\\bigsqcup":"\\dotsb","\\And":"\\dotsb","\\longrightarrow":"\\dotsb","\\Longrightarrow":"\\dotsb","\\longleftarrow":"\\dotsb","\\Longleftarrow":"\\dotsb","\\longleftrightarrow":"\\dotsb","\\Longleftrightarrow":"\\dotsb","\\mapsto":"\\dotsb","\\longmapsto":"\\dotsb","\\hookrightarrow":"\\dotsb","\\doteq":"\\dotsb","\\mathbin":"\\dotsb","\\mathrel":"\\dotsb","\\relbar":"\\dotsb","\\Relbar":"\\dotsb","\\xrightarrow":"\\dotsb","\\xleftarrow":"\\dotsb","\\DOTSI":"\\dotsi","\\int":"\\dotsi","\\oint":"\\dotsi","\\iint":"\\dotsi","\\iiint":"\\dotsi","\\iiiint":"\\dotsi","\\idotsint":"\\dotsi","\\DOTSX":"\\dotsx"};d("\\dots",function(r){var e="\\dotso",t=r.expandAfterFuture().text;return t in Hn?e=Hn[t]:(t.slice(0,4)==="\\not"||t in K.math&&$.contains(["bin","rel"],K.math[t].group))&&(e="\\dotsb"),e});var ma={")":!0,"]":!0,"\\rbrack":!0,"\\}":!0,"\\rbrace":!0,"\\rangle":!0,"\\rceil":!0,"\\rfloor":!0,"\\rgroup":!0,"\\rmoustache":!0,"\\right":!0,"\\bigr":!0,"\\biggr":!0,"\\Bigr":!0,"\\Biggr":!0,$:!0,";":!0,".":!0,",":!0};d("\\dotso",function(r){var e=r.future().text;return e in ma?"\\ldots\\,":"\\ldots"});d("\\dotsc",function(r){var e=r.future().text;return e in ma&&e!==","?"\\ldots\\,":"\\ldots"});d("\\cdots",function(r){var e=r.future().text;return e in ma?"\\@cdots\\,":"\\@cdots"});d("\\dotsb","\\cdots");d("\\dotsm","\\cdots");d("\\dotsi","\\!\\cdots");d("\\dotsx","\\ldots\\,");d("\\DOTSI","\\relax");d("\\DOTSB","\\relax");d("\\DOTSX","\\relax");d("\\tmspace","\\TextOrMath{\\kern#1#3}{\\mskip#1#2}\\relax");d("\\,","\\tmspace+{3mu}{.1667em}");d("\\thinspace","\\,");d("\\>","\\mskip{4mu}");d("\\:","\\tmspace+{4mu}{.2222em}");d("\\medspace","\\:");d("\\;","\\tmspace+{5mu}{.2777em}");d("\\thickspace","\\;");d("\\!","\\tmspace-{3mu}{.1667em}");d("\\negthinspace","\\!");d("\\negmedspace","\\tmspace-{4mu}{.2222em}");d("\\negthickspace","\\tmspace-{5mu}{.277em}");d("\\enspace","\\kern.5em ");d("\\enskip","\\hskip.5em\\relax");d("\\quad","\\hskip1em\\relax");d("\\qquad","\\hskip2em\\relax");d("\\tag","\\@ifstar\\tag@literal\\tag@paren");d("\\tag@paren","\\tag@literal{({#1})}");d("\\tag@literal",r=>{if(r.macros.get("\\df@tag"))throw new T("Multiple \\tag");return"\\gdef\\df@tag{\\text{#1}}"});d("\\bmod","\\mathchoice{\\mskip1mu}{\\mskip1mu}{\\mskip5mu}{\\mskip5mu}\\mathbin{\\rm mod}\\mathchoice{\\mskip1mu}{\\mskip1mu}{\\mskip5mu}{\\mskip5mu}");d("\\pod","\\allowbreak\\mathchoice{\\mkern18mu}{\\mkern8mu}{\\mkern8mu}{\\mkern8mu}(#1)");d("\\pmod","\\pod{{\\rm mod}\\mkern6mu#1}");d("\\mod","\\allowbreak\\mathchoice{\\mkern18mu}{\\mkern12mu}{\\mkern12mu}{\\mkern12mu}{\\rm mod}\\,\\,#1");d("\\newline","\\\\\\relax");d("\\TeX","\\textrm{\\html@mathml{T\\kern-.1667em\\raisebox{-.5ex}{E}\\kern-.125emX}{TeX}}");var Di=z(_0["Main-Regular"]["T".charCodeAt(0)][1]-.7*_0["Main-Regular"]["A".charCodeAt(0)][1]);d("\\LaTeX","\\textrm{\\html@mathml{"+("L\\kern-.36em\\raisebox{"+Di+"}{\\scriptstyle A}")+"\\kern-.15em\\TeX}{LaTeX}}");d("\\KaTeX","\\textrm{\\html@mathml{"+("K\\kern-.17em\\raisebox{"+Di+"}{\\scriptstyle A}")+"\\kern-.15em\\TeX}{KaTeX}}");d("\\hspace","\\@ifstar\\@hspacer\\@hspace");d("\\@hspace","\\hskip #1\\relax");d("\\@hspacer","\\rule{0pt}{0pt}\\hskip #1\\relax");d("\\ordinarycolon",":");d("\\vcentcolon","\\mathrel{\\mathop\\ordinarycolon}");d("\\dblcolon",'\\html@mathml{\\mathrel{\\vcentcolon\\mathrel{\\mkern-.9mu}\\vcentcolon}}{\\mathop{\\char"2237}}');d("\\coloneqq",'\\html@mathml{\\mathrel{\\vcentcolon\\mathrel{\\mkern-1.2mu}=}}{\\mathop{\\char"2254}}');d("\\Coloneqq",'\\html@mathml{\\mathrel{\\dblcolon\\mathrel{\\mkern-1.2mu}=}}{\\mathop{\\char"2237\\char"3d}}');d("\\coloneq",'\\html@mathml{\\mathrel{\\vcentcolon\\mathrel{\\mkern-1.2mu}\\mathrel{-}}}{\\mathop{\\char"3a\\char"2212}}');d("\\Coloneq",'\\html@mathml{\\mathrel{\\dblcolon\\mathrel{\\mkern-1.2mu}\\mathrel{-}}}{\\mathop{\\char"2237\\char"2212}}');d("\\eqqcolon",'\\html@mathml{\\mathrel{=\\mathrel{\\mkern-1.2mu}\\vcentcolon}}{\\mathop{\\char"2255}}');d("\\Eqqcolon",'\\html@mathml{\\mathrel{=\\mathrel{\\mkern-1.2mu}\\dblcolon}}{\\mathop{\\char"3d\\char"2237}}');d("\\eqcolon",'\\html@mathml{\\mathrel{\\mathrel{-}\\mathrel{\\mkern-1.2mu}\\vcentcolon}}{\\mathop{\\char"2239}}');d("\\Eqcolon",'\\html@mathml{\\mathrel{\\mathrel{-}\\mathrel{\\mkern-1.2mu}\\dblcolon}}{\\mathop{\\char"2212\\char"2237}}');d("\\colonapprox",'\\html@mathml{\\mathrel{\\vcentcolon\\mathrel{\\mkern-1.2mu}\\approx}}{\\mathop{\\char"3a\\char"2248}}');d("\\Colonapprox",'\\html@mathml{\\mathrel{\\dblcolon\\mathrel{\\mkern-1.2mu}\\approx}}{\\mathop{\\char"2237\\char"2248}}');d("\\colonsim",'\\html@mathml{\\mathrel{\\vcentcolon\\mathrel{\\mkern-1.2mu}\\sim}}{\\mathop{\\char"3a\\char"223c}}');d("\\Colonsim",'\\html@mathml{\\mathrel{\\dblcolon\\mathrel{\\mkern-1.2mu}\\sim}}{\\mathop{\\char"2237\\char"223c}}');d("\u2237","\\dblcolon");d("\u2239","\\eqcolon");d("\u2254","\\coloneqq");d("\u2255","\\eqqcolon");d("\u2A74","\\Coloneqq");d("\\ratio","\\vcentcolon");d("\\coloncolon","\\dblcolon");d("\\colonequals","\\coloneqq");d("\\coloncolonequals","\\Coloneqq");d("\\equalscolon","\\eqqcolon");d("\\equalscoloncolon","\\Eqqcolon");d("\\colonminus","\\coloneq");d("\\coloncolonminus","\\Coloneq");d("\\minuscolon","\\eqcolon");d("\\minuscoloncolon","\\Eqcolon");d("\\coloncolonapprox","\\Colonapprox");d("\\coloncolonsim","\\Colonsim");d("\\simcolon","\\mathrel{\\sim\\mathrel{\\mkern-1.2mu}\\vcentcolon}");d("\\simcoloncolon","\\mathrel{\\sim\\mathrel{\\mkern-1.2mu}\\dblcolon}");d("\\approxcolon","\\mathrel{\\approx\\mathrel{\\mkern-1.2mu}\\vcentcolon}");d("\\approxcoloncolon","\\mathrel{\\approx\\mathrel{\\mkern-1.2mu}\\dblcolon}");d("\\notni","\\html@mathml{\\not\\ni}{\\mathrel{\\char`\u220C}}");d("\\limsup","\\DOTSB\\operatorname*{lim\\,sup}");d("\\liminf","\\DOTSB\\operatorname*{lim\\,inf}");d("\\injlim","\\DOTSB\\operatorname*{inj\\,lim}");d("\\projlim","\\DOTSB\\operatorname*{proj\\,lim}");d("\\varlimsup","\\DOTSB\\operatorname*{\\overline{lim}}");d("\\varliminf","\\DOTSB\\operatorname*{\\underline{lim}}");d("\\varinjlim","\\DOTSB\\operatorname*{\\underrightarrow{lim}}");d("\\varprojlim","\\DOTSB\\operatorname*{\\underleftarrow{lim}}");d("\\gvertneqq","\\html@mathml{\\@gvertneqq}{\u2269}");d("\\lvertneqq","\\html@mathml{\\@lvertneqq}{\u2268}");d("\\ngeqq","\\html@mathml{\\@ngeqq}{\u2271}");d("\\ngeqslant","\\html@mathml{\\@ngeqslant}{\u2271}");d("\\nleqq","\\html@mathml{\\@nleqq}{\u2270}");d("\\nleqslant","\\html@mathml{\\@nleqslant}{\u2270}");d("\\nshortmid","\\html@mathml{\\@nshortmid}{\u2224}");d("\\nshortparallel","\\html@mathml{\\@nshortparallel}{\u2226}");d("\\nsubseteqq","\\html@mathml{\\@nsubseteqq}{\u2288}");d("\\nsupseteqq","\\html@mathml{\\@nsupseteqq}{\u2289}");d("\\varsubsetneq","\\html@mathml{\\@varsubsetneq}{\u228A}");d("\\varsubsetneqq","\\html@mathml{\\@varsubsetneqq}{\u2ACB}");d("\\varsupsetneq","\\html@mathml{\\@varsupsetneq}{\u228B}");d("\\varsupsetneqq","\\html@mathml{\\@varsupsetneqq}{\u2ACC}");d("\\imath","\\html@mathml{\\@imath}{\u0131}");d("\\jmath","\\html@mathml{\\@jmath}{\u0237}");d("\\llbracket","\\html@mathml{\\mathopen{[\\mkern-3.2mu[}}{\\mathopen{\\char`\u27E6}}");d("\\rrbracket","\\html@mathml{\\mathclose{]\\mkern-3.2mu]}}{\\mathclose{\\char`\u27E7}}");d("\u27E6","\\llbracket");d("\u27E7","\\rrbracket");d("\\lBrace","\\html@mathml{\\mathopen{\\{\\mkern-3.2mu[}}{\\mathopen{\\char`\u2983}}");d("\\rBrace","\\html@mathml{\\mathclose{]\\mkern-3.2mu\\}}}{\\mathclose{\\char`\u2984}}");d("\u2983","\\lBrace");d("\u2984","\\rBrace");d("\\minuso","\\mathbin{\\html@mathml{{\\mathrlap{\\mathchoice{\\kern{0.145em}}{\\kern{0.145em}}{\\kern{0.1015em}}{\\kern{0.0725em}}\\circ}{-}}}{\\char`\u29B5}}");d("\u29B5","\\minuso");d("\\darr","\\downarrow");d("\\dArr","\\Downarrow");d("\\Darr","\\Downarrow");d("\\lang","\\langle");d("\\rang","\\rangle");d("\\uarr","\\uparrow");d("\\uArr","\\Uparrow");d("\\Uarr","\\Uparrow");d("\\N","\\mathbb{N}");d("\\R","\\mathbb{R}");d("\\Z","\\mathbb{Z}");d("\\alef","\\aleph");d("\\alefsym","\\aleph");d("\\Alpha","\\mathrm{A}");d("\\Beta","\\mathrm{B}");d("\\bull","\\bullet");d("\\Chi","\\mathrm{X}");d("\\clubs","\\clubsuit");d("\\cnums","\\mathbb{C}");d("\\Complex","\\mathbb{C}");d("\\Dagger","\\ddagger");d("\\diamonds","\\diamondsuit");d("\\empty","\\emptyset");d("\\Epsilon","\\mathrm{E}");d("\\Eta","\\mathrm{H}");d("\\exist","\\exists");d("\\harr","\\leftrightarrow");d("\\hArr","\\Leftrightarrow");d("\\Harr","\\Leftrightarrow");d("\\hearts","\\heartsuit");d("\\image","\\Im");d("\\infin","\\infty");d("\\Iota","\\mathrm{I}");d("\\isin","\\in");d("\\Kappa","\\mathrm{K}");d("\\larr","\\leftarrow");d("\\lArr","\\Leftarrow");d("\\Larr","\\Leftarrow");d("\\lrarr","\\leftrightarrow");d("\\lrArr","\\Leftrightarrow");d("\\Lrarr","\\Leftrightarrow");d("\\Mu","\\mathrm{M}");d("\\natnums","\\mathbb{N}");d("\\Nu","\\mathrm{N}");d("\\Omicron","\\mathrm{O}");d("\\plusmn","\\pm");d("\\rarr","\\rightarrow");d("\\rArr","\\Rightarrow");d("\\Rarr","\\Rightarrow");d("\\real","\\Re");d("\\reals","\\mathbb{R}");d("\\Reals","\\mathbb{R}");d("\\Rho","\\mathrm{P}");d("\\sdot","\\cdot");d("\\sect","\\S");d("\\spades","\\spadesuit");d("\\sub","\\subset");d("\\sube","\\subseteq");d("\\supe","\\supseteq");d("\\Tau","\\mathrm{T}");d("\\thetasym","\\vartheta");d("\\weierp","\\wp");d("\\Zeta","\\mathrm{Z}");d("\\argmin","\\DOTSB\\operatorname*{arg\\,min}");d("\\argmax","\\DOTSB\\operatorname*{arg\\,max}");d("\\plim","\\DOTSB\\mathop{\\operatorname{plim}}\\limits");d("\\bra","\\mathinner{\\langle{#1}|}");d("\\ket","\\mathinner{|{#1}\\rangle}");d("\\braket","\\mathinner{\\langle{#1}\\rangle}");d("\\Bra","\\left\\langle#1\\right|");d("\\Ket","\\left|#1\\right\\rangle");var $i=r=>e=>{var t=e.consumeArg().tokens,a=e.consumeArg().tokens,n=e.consumeArg().tokens,i=e.consumeArg().tokens,l=e.macros.get("|"),u=e.macros.get("\\|");e.macros.beginGroup();var h=g=>b=>{r&&(b.macros.set("|",l),n.length&&b.macros.set("\\|",u));var x=g;if(!g&&n.length){var k=b.future();k.text==="|"&&(b.popToken(),x=!0)}return{tokens:x?n:a,numArgs:0}};e.macros.set("|",h(!1)),n.length&&e.macros.set("\\|",h(!0));var m=e.consumeArg().tokens,v=e.expandTokens([...i,...m,...t]);return e.macros.endGroup(),{tokens:v.reverse(),numArgs:0}};d("\\bra@ket",$i(!1));d("\\bra@set",$i(!0));d("\\Braket","\\bra@ket{\\left\\langle}{\\,\\middle\\vert\\,}{\\,\\middle\\vert\\,}{\\right\\rangle}");d("\\Set","\\bra@set{\\left\\{\\:}{\\;\\middle\\vert\\;}{\\;\\middle\\Vert\\;}{\\:\\right\\}}");d("\\set","\\bra@set{\\{\\,}{\\mid}{}{\\,\\}}");d("\\angln","{\\angl n}");d("\\blue","\\textcolor{##6495ed}{#1}");d("\\orange","\\textcolor{##ffa500}{#1}");d("\\pink","\\textcolor{##ff00af}{#1}");d("\\red","\\textcolor{##df0030}{#1}");d("\\green","\\textcolor{##28ae7b}{#1}");d("\\gray","\\textcolor{gray}{#1}");d("\\purple","\\textcolor{##9d38bd}{#1}");d("\\blueA","\\textcolor{##ccfaff}{#1}");d("\\blueB","\\textcolor{##80f6ff}{#1}");d("\\blueC","\\textcolor{##63d9ea}{#1}");d("\\blueD","\\textcolor{##11accd}{#1}");d("\\blueE","\\textcolor{##0c7f99}{#1}");d("\\tealA","\\textcolor{##94fff5}{#1}");d("\\tealB","\\textcolor{##26edd5}{#1}");d("\\tealC","\\textcolor{##01d1c1}{#1}");d("\\tealD","\\textcolor{##01a995}{#1}");d("\\tealE","\\textcolor{##208170}{#1}");d("\\greenA","\\textcolor{##b6ffb0}{#1}");d("\\greenB","\\textcolor{##8af281}{#1}");d("\\greenC","\\textcolor{##74cf70}{#1}");d("\\greenD","\\textcolor{##1fab54}{#1}");d("\\greenE","\\textcolor{##0d923f}{#1}");d("\\goldA","\\textcolor{##ffd0a9}{#1}");d("\\goldB","\\textcolor{##ffbb71}{#1}");d("\\goldC","\\textcolor{##ff9c39}{#1}");d("\\goldD","\\textcolor{##e07d10}{#1}");d("\\goldE","\\textcolor{##a75a05}{#1}");d("\\redA","\\textcolor{##fca9a9}{#1}");d("\\redB","\\textcolor{##ff8482}{#1}");d("\\redC","\\textcolor{##f9685d}{#1}");d("\\redD","\\textcolor{##e84d39}{#1}");d("\\redE","\\textcolor{##bc2612}{#1}");d("\\maroonA","\\textcolor{##ffbde0}{#1}");d("\\maroonB","\\textcolor{##ff92c6}{#1}");d("\\maroonC","\\textcolor{##ed5fa6}{#1}");d("\\maroonD","\\textcolor{##ca337c}{#1}");d("\\maroonE","\\textcolor{##9e034e}{#1}");d("\\purpleA","\\textcolor{##ddd7ff}{#1}");d("\\purpleB","\\textcolor{##c6b9fc}{#1}");d("\\purpleC","\\textcolor{##aa87ff}{#1}");d("\\purpleD","\\textcolor{##7854ab}{#1}");d("\\purpleE","\\textcolor{##543b78}{#1}");d("\\mintA","\\textcolor{##f5f9e8}{#1}");d("\\mintB","\\textcolor{##edf2df}{#1}");d("\\mintC","\\textcolor{##e0e5cc}{#1}");d("\\grayA","\\textcolor{##f6f7f7}{#1}");d("\\grayB","\\textcolor{##f0f1f2}{#1}");d("\\grayC","\\textcolor{##e3e5e6}{#1}");d("\\grayD","\\textcolor{##d6d8da}{#1}");d("\\grayE","\\textcolor{##babec2}{#1}");d("\\grayF","\\textcolor{##888d93}{#1}");d("\\grayG","\\textcolor{##626569}{#1}");d("\\grayH","\\textcolor{##3b3e40}{#1}");d("\\grayI","\\textcolor{##21242c}{#1}");d("\\kaBlue","\\textcolor{##314453}{#1}");d("\\kaGreen","\\textcolor{##71B307}{#1}");var Ni={"^":!0,_:!0,"\\limits":!0,"\\nolimits":!0},Zr=class{constructor(e,t,a){this.settings=void 0,this.expansionCount=void 0,this.lexer=void 0,this.macros=void 0,this.stack=void 0,this.mode=void 0,this.settings=t,this.expansionCount=0,this.feed(e),this.macros=new Xr(W1,t.macros),this.mode=a,this.stack=[]}feed(e){this.lexer=new Zt(e,this.settings)}switchMode(e){this.mode=e}beginGroup(){this.macros.beginGroup()}endGroup(){this.macros.endGroup()}endGroups(){this.macros.endGroups()}future(){return this.stack.length===0&&this.pushToken(this.lexer.lex()),this.stack[this.stack.length-1]}popToken(){return this.future(),this.stack.pop()}pushToken(e){this.stack.push(e)}pushTokens(e){this.stack.push(...e)}scanArgument(e){var t,a,n;if(e){if(this.consumeSpaces(),this.future().text!=="[")return null;t=this.popToken(),{tokens:n,end:a}=this.consumeArg(["]"])}else({tokens:n,start:t,end:a}=this.consumeArg());return this.pushToken(new C0("EOF",a.loc)),this.pushTokens(n),t.range(a,"")}consumeSpaces(){for(;;){var e=this.future();if(e.text===" ")this.stack.pop();else break}}consumeArg(e){var t=[],a=e&&e.length>0;a||this.consumeSpaces();var n=this.future(),i,l=0,u=0;do{if(i=this.popToken(),t.push(i),i.text==="{")++l;else if(i.text==="}"){if(--l,l===-1)throw new T("Extra }",i)}else if(i.text==="EOF")throw new T("Unexpected end of input in a macro argument, expected '"+(e&&a?e[u]:"}")+"'",i);if(e&&a)if((l===0||l===1&&e[u]==="{")&&i.text===e[u]){if(++u,u===e.length){t.splice(-u,u);break}}else u=0}while(l!==0||a);return n.text==="{"&&t[t.length-1].text==="}"&&(t.pop(),t.shift()),t.reverse(),{tokens:t,start:n,end:i}}consumeArgs(e,t){if(t){if(t.length!==e+1)throw new T("The length of delimiters doesn't match the number of args!");for(var a=t[0],n=0;nthis.settings.maxExpand)throw new T("Too many expansions: infinite loop or need to increase maxExpand setting")}expandOnce(e){var t=this.popToken(),a=t.text,n=t.noexpand?null:this._getExpansion(a);if(n==null||e&&n.unexpandable){if(e&&n==null&&a[0]==="\\"&&!this.isDefined(a))throw new T("Undefined control sequence: "+a);return this.pushToken(t),!1}this.countExpansion(1);var i=n.tokens,l=this.consumeArgs(n.numArgs,n.delimiters);if(n.numArgs){i=i.slice();for(var u=i.length-1;u>=0;--u){var h=i[u];if(h.text==="#"){if(u===0)throw new T("Incomplete placeholder at end of macro body",h);if(h=i[--u],h.text==="#")i.splice(u+1,1);else if(/^[1-9]$/.test(h.text))i.splice(u,2,...l[+h.text-1]);else throw new T("Not a valid argument number",h)}}}return this.pushTokens(i),i.length}expandAfterFuture(){return this.expandOnce(),this.future()}expandNextToken(){for(;;)if(this.expandOnce()===!1){var e=this.stack.pop();return e.treatAsRelax&&(e.text="\\relax"),e}throw new Error}expandMacro(e){return this.macros.has(e)?this.expandTokens([new C0(e)]):void 0}expandTokens(e){var t=[],a=this.stack.length;for(this.pushTokens(e);this.stack.length>a;)if(this.expandOnce(!0)===!1){var n=this.stack.pop();n.treatAsRelax&&(n.noexpand=!1,n.treatAsRelax=!1),t.push(n)}return this.countExpansion(t.length),t}expandMacroAsText(e){var t=this.expandMacro(e);return t&&t.map(a=>a.text).join("")}_getExpansion(e){var t=this.macros.get(e);if(t==null)return t;if(e.length===1){var a=this.lexer.catcodes[e];if(a!=null&&a!==13)return}var n=typeof t=="function"?t(this):t;if(typeof n=="string"){var i=0;if(n.indexOf("#")!==-1)for(var l=n.replace(/##/g,"");l.indexOf("#"+(i+1))!==-1;)++i;for(var u=new Zt(n,this.settings),h=[],m=u.lex();m.text!=="EOF";)h.push(m),m=u.lex();h.reverse();var v={tokens:h,numArgs:i};return v}return n}isDefined(e){return this.macros.has(e)||se.hasOwnProperty(e)||K.math.hasOwnProperty(e)||K.text.hasOwnProperty(e)||Ni.hasOwnProperty(e)}isExpandable(e){var t=this.macros.get(e);return t!=null?typeof t=="string"||typeof t=="function"||!t.unexpandable:se.hasOwnProperty(e)&&!se[e].primitive}},In=/^[₊₋₌₍₎₀₁₂₃₄₅₆₇₈₉ₐₑₕᵢⱼₖₗₘₙₒₚᵣₛₜᵤᵥₓᵦᵧᵨᵩᵪ]/,jt=Object.freeze({"\u208A":"+","\u208B":"-","\u208C":"=","\u208D":"(","\u208E":")","\u2080":"0","\u2081":"1","\u2082":"2","\u2083":"3","\u2084":"4","\u2085":"5","\u2086":"6","\u2087":"7","\u2088":"8","\u2089":"9","\u2090":"a","\u2091":"e","\u2095":"h","\u1D62":"i","\u2C7C":"j","\u2096":"k","\u2097":"l","\u2098":"m","\u2099":"n","\u2092":"o","\u209A":"p","\u1D63":"r","\u209B":"s","\u209C":"t","\u1D64":"u","\u1D65":"v","\u2093":"x","\u1D66":"\u03B2","\u1D67":"\u03B3","\u1D68":"\u03C1","\u1D69":"\u03D5","\u1D6A":"\u03C7","\u207A":"+","\u207B":"-","\u207C":"=","\u207D":"(","\u207E":")","\u2070":"0","\xB9":"1","\xB2":"2","\xB3":"3","\u2074":"4","\u2075":"5","\u2076":"6","\u2077":"7","\u2078":"8","\u2079":"9","\u1D2C":"A","\u1D2E":"B","\u1D30":"D","\u1D31":"E","\u1D33":"G","\u1D34":"H","\u1D35":"I","\u1D36":"J","\u1D37":"K","\u1D38":"L","\u1D39":"M","\u1D3A":"N","\u1D3C":"O","\u1D3E":"P","\u1D3F":"R","\u1D40":"T","\u1D41":"U","\u2C7D":"V","\u1D42":"W","\u1D43":"a","\u1D47":"b","\u1D9C":"c","\u1D48":"d","\u1D49":"e","\u1DA0":"f","\u1D4D":"g",\u02B0:"h","\u2071":"i",\u02B2:"j","\u1D4F":"k",\u02E1:"l","\u1D50":"m",\u207F:"n","\u1D52":"o","\u1D56":"p",\u02B3:"r",\u02E2:"s","\u1D57":"t","\u1D58":"u","\u1D5B":"v",\u02B7:"w",\u02E3:"x",\u02B8:"y","\u1DBB":"z","\u1D5D":"\u03B2","\u1D5E":"\u03B3","\u1D5F":"\u03B4","\u1D60":"\u03D5","\u1D61":"\u03C7","\u1DBF":"\u03B8"}),Ir={"\u0301":{text:"\\'",math:"\\acute"},"\u0300":{text:"\\`",math:"\\grave"},"\u0308":{text:'\\"',math:"\\ddot"},"\u0303":{text:"\\~",math:"\\tilde"},"\u0304":{text:"\\=",math:"\\bar"},"\u0306":{text:"\\u",math:"\\breve"},"\u030C":{text:"\\v",math:"\\check"},"\u0302":{text:"\\^",math:"\\hat"},"\u0307":{text:"\\.",math:"\\dot"},"\u030A":{text:"\\r",math:"\\mathring"},"\u030B":{text:"\\H"},"\u0327":{text:"\\c"}},Pn={\u00E1:"a\u0301",\u00E0:"a\u0300",\u00E4:"a\u0308",\u01DF:"a\u0308\u0304",\u00E3:"a\u0303",\u0101:"a\u0304",\u0103:"a\u0306",\u1EAF:"a\u0306\u0301",\u1EB1:"a\u0306\u0300",\u1EB5:"a\u0306\u0303",\u01CE:"a\u030C",\u00E2:"a\u0302",\u1EA5:"a\u0302\u0301",\u1EA7:"a\u0302\u0300",\u1EAB:"a\u0302\u0303",\u0227:"a\u0307",\u01E1:"a\u0307\u0304",\u00E5:"a\u030A",\u01FB:"a\u030A\u0301",\u1E03:"b\u0307",\u0107:"c\u0301",\u1E09:"c\u0327\u0301",\u010D:"c\u030C",\u0109:"c\u0302",\u010B:"c\u0307",\u00E7:"c\u0327",\u010F:"d\u030C",\u1E0B:"d\u0307",\u1E11:"d\u0327",\u00E9:"e\u0301",\u00E8:"e\u0300",\u00EB:"e\u0308",\u1EBD:"e\u0303",\u0113:"e\u0304",\u1E17:"e\u0304\u0301",\u1E15:"e\u0304\u0300",\u0115:"e\u0306",\u1E1D:"e\u0327\u0306",\u011B:"e\u030C",\u00EA:"e\u0302",\u1EBF:"e\u0302\u0301",\u1EC1:"e\u0302\u0300",\u1EC5:"e\u0302\u0303",\u0117:"e\u0307",\u0229:"e\u0327",\u1E1F:"f\u0307",\u01F5:"g\u0301",\u1E21:"g\u0304",\u011F:"g\u0306",\u01E7:"g\u030C",\u011D:"g\u0302",\u0121:"g\u0307",\u0123:"g\u0327",\u1E27:"h\u0308",\u021F:"h\u030C",\u0125:"h\u0302",\u1E23:"h\u0307",\u1E29:"h\u0327",\u00ED:"i\u0301",\u00EC:"i\u0300",\u00EF:"i\u0308",\u1E2F:"i\u0308\u0301",\u0129:"i\u0303",\u012B:"i\u0304",\u012D:"i\u0306",\u01D0:"i\u030C",\u00EE:"i\u0302",\u01F0:"j\u030C",\u0135:"j\u0302",\u1E31:"k\u0301",\u01E9:"k\u030C",\u0137:"k\u0327",\u013A:"l\u0301",\u013E:"l\u030C",\u013C:"l\u0327",\u1E3F:"m\u0301",\u1E41:"m\u0307",\u0144:"n\u0301",\u01F9:"n\u0300",\u00F1:"n\u0303",\u0148:"n\u030C",\u1E45:"n\u0307",\u0146:"n\u0327",\u00F3:"o\u0301",\u00F2:"o\u0300",\u00F6:"o\u0308",\u022B:"o\u0308\u0304",\u00F5:"o\u0303",\u1E4D:"o\u0303\u0301",\u1E4F:"o\u0303\u0308",\u022D:"o\u0303\u0304",\u014D:"o\u0304",\u1E53:"o\u0304\u0301",\u1E51:"o\u0304\u0300",\u014F:"o\u0306",\u01D2:"o\u030C",\u00F4:"o\u0302",\u1ED1:"o\u0302\u0301",\u1ED3:"o\u0302\u0300",\u1ED7:"o\u0302\u0303",\u022F:"o\u0307",\u0231:"o\u0307\u0304",\u0151:"o\u030B",\u1E55:"p\u0301",\u1E57:"p\u0307",\u0155:"r\u0301",\u0159:"r\u030C",\u1E59:"r\u0307",\u0157:"r\u0327",\u015B:"s\u0301",\u1E65:"s\u0301\u0307",\u0161:"s\u030C",\u1E67:"s\u030C\u0307",\u015D:"s\u0302",\u1E61:"s\u0307",\u015F:"s\u0327",\u1E97:"t\u0308",\u0165:"t\u030C",\u1E6B:"t\u0307",\u0163:"t\u0327",\u00FA:"u\u0301",\u00F9:"u\u0300",\u00FC:"u\u0308",\u01D8:"u\u0308\u0301",\u01DC:"u\u0308\u0300",\u01D6:"u\u0308\u0304",\u01DA:"u\u0308\u030C",\u0169:"u\u0303",\u1E79:"u\u0303\u0301",\u016B:"u\u0304",\u1E7B:"u\u0304\u0308",\u016D:"u\u0306",\u01D4:"u\u030C",\u00FB:"u\u0302",\u016F:"u\u030A",\u0171:"u\u030B",\u1E7D:"v\u0303",\u1E83:"w\u0301",\u1E81:"w\u0300",\u1E85:"w\u0308",\u0175:"w\u0302",\u1E87:"w\u0307",\u1E98:"w\u030A",\u1E8D:"x\u0308",\u1E8B:"x\u0307",\u00FD:"y\u0301",\u1EF3:"y\u0300",\u00FF:"y\u0308",\u1EF9:"y\u0303",\u0233:"y\u0304",\u0177:"y\u0302",\u1E8F:"y\u0307",\u1E99:"y\u030A",\u017A:"z\u0301",\u017E:"z\u030C",\u1E91:"z\u0302",\u017C:"z\u0307",\u00C1:"A\u0301",\u00C0:"A\u0300",\u00C4:"A\u0308",\u01DE:"A\u0308\u0304",\u00C3:"A\u0303",\u0100:"A\u0304",\u0102:"A\u0306",\u1EAE:"A\u0306\u0301",\u1EB0:"A\u0306\u0300",\u1EB4:"A\u0306\u0303",\u01CD:"A\u030C",\u00C2:"A\u0302",\u1EA4:"A\u0302\u0301",\u1EA6:"A\u0302\u0300",\u1EAA:"A\u0302\u0303",\u0226:"A\u0307",\u01E0:"A\u0307\u0304",\u00C5:"A\u030A",\u01FA:"A\u030A\u0301",\u1E02:"B\u0307",\u0106:"C\u0301",\u1E08:"C\u0327\u0301",\u010C:"C\u030C",\u0108:"C\u0302",\u010A:"C\u0307",\u00C7:"C\u0327",\u010E:"D\u030C",\u1E0A:"D\u0307",\u1E10:"D\u0327",\u00C9:"E\u0301",\u00C8:"E\u0300",\u00CB:"E\u0308",\u1EBC:"E\u0303",\u0112:"E\u0304",\u1E16:"E\u0304\u0301",\u1E14:"E\u0304\u0300",\u0114:"E\u0306",\u1E1C:"E\u0327\u0306",\u011A:"E\u030C",\u00CA:"E\u0302",\u1EBE:"E\u0302\u0301",\u1EC0:"E\u0302\u0300",\u1EC4:"E\u0302\u0303",\u0116:"E\u0307",\u0228:"E\u0327",\u1E1E:"F\u0307",\u01F4:"G\u0301",\u1E20:"G\u0304",\u011E:"G\u0306",\u01E6:"G\u030C",\u011C:"G\u0302",\u0120:"G\u0307",\u0122:"G\u0327",\u1E26:"H\u0308",\u021E:"H\u030C",\u0124:"H\u0302",\u1E22:"H\u0307",\u1E28:"H\u0327",\u00CD:"I\u0301",\u00CC:"I\u0300",\u00CF:"I\u0308",\u1E2E:"I\u0308\u0301",\u0128:"I\u0303",\u012A:"I\u0304",\u012C:"I\u0306",\u01CF:"I\u030C",\u00CE:"I\u0302",\u0130:"I\u0307",\u0134:"J\u0302",\u1E30:"K\u0301",\u01E8:"K\u030C",\u0136:"K\u0327",\u0139:"L\u0301",\u013D:"L\u030C",\u013B:"L\u0327",\u1E3E:"M\u0301",\u1E40:"M\u0307",\u0143:"N\u0301",\u01F8:"N\u0300",\u00D1:"N\u0303",\u0147:"N\u030C",\u1E44:"N\u0307",\u0145:"N\u0327",\u00D3:"O\u0301",\u00D2:"O\u0300",\u00D6:"O\u0308",\u022A:"O\u0308\u0304",\u00D5:"O\u0303",\u1E4C:"O\u0303\u0301",\u1E4E:"O\u0303\u0308",\u022C:"O\u0303\u0304",\u014C:"O\u0304",\u1E52:"O\u0304\u0301",\u1E50:"O\u0304\u0300",\u014E:"O\u0306",\u01D1:"O\u030C",\u00D4:"O\u0302",\u1ED0:"O\u0302\u0301",\u1ED2:"O\u0302\u0300",\u1ED6:"O\u0302\u0303",\u022E:"O\u0307",\u0230:"O\u0307\u0304",\u0150:"O\u030B",\u1E54:"P\u0301",\u1E56:"P\u0307",\u0154:"R\u0301",\u0158:"R\u030C",\u1E58:"R\u0307",\u0156:"R\u0327",\u015A:"S\u0301",\u1E64:"S\u0301\u0307",\u0160:"S\u030C",\u1E66:"S\u030C\u0307",\u015C:"S\u0302",\u1E60:"S\u0307",\u015E:"S\u0327",\u0164:"T\u030C",\u1E6A:"T\u0307",\u0162:"T\u0327",\u00DA:"U\u0301",\u00D9:"U\u0300",\u00DC:"U\u0308",\u01D7:"U\u0308\u0301",\u01DB:"U\u0308\u0300",\u01D5:"U\u0308\u0304",\u01D9:"U\u0308\u030C",\u0168:"U\u0303",\u1E78:"U\u0303\u0301",\u016A:"U\u0304",\u1E7A:"U\u0304\u0308",\u016C:"U\u0306",\u01D3:"U\u030C",\u00DB:"U\u0302",\u016E:"U\u030A",\u0170:"U\u030B",\u1E7C:"V\u0303",\u1E82:"W\u0301",\u1E80:"W\u0300",\u1E84:"W\u0308",\u0174:"W\u0302",\u1E86:"W\u0307",\u1E8C:"X\u0308",\u1E8A:"X\u0307",\u00DD:"Y\u0301",\u1EF2:"Y\u0300",\u0178:"Y\u0308",\u1EF8:"Y\u0303",\u0232:"Y\u0304",\u0176:"Y\u0302",\u1E8E:"Y\u0307",\u0179:"Z\u0301",\u017D:"Z\u030C",\u1E90:"Z\u0302",\u017B:"Z\u0307",\u03AC:"\u03B1\u0301",\u1F70:"\u03B1\u0300",\u1FB1:"\u03B1\u0304",\u1FB0:"\u03B1\u0306",\u03AD:"\u03B5\u0301",\u1F72:"\u03B5\u0300",\u03AE:"\u03B7\u0301",\u1F74:"\u03B7\u0300",\u03AF:"\u03B9\u0301",\u1F76:"\u03B9\u0300",\u03CA:"\u03B9\u0308",\u0390:"\u03B9\u0308\u0301",\u1FD2:"\u03B9\u0308\u0300",\u1FD1:"\u03B9\u0304",\u1FD0:"\u03B9\u0306",\u03CC:"\u03BF\u0301",\u1F78:"\u03BF\u0300",\u03CD:"\u03C5\u0301",\u1F7A:"\u03C5\u0300",\u03CB:"\u03C5\u0308",\u03B0:"\u03C5\u0308\u0301",\u1FE2:"\u03C5\u0308\u0300",\u1FE1:"\u03C5\u0304",\u1FE0:"\u03C5\u0306",\u03CE:"\u03C9\u0301",\u1F7C:"\u03C9\u0300",\u038E:"\u03A5\u0301",\u1FEA:"\u03A5\u0300",\u03AB:"\u03A5\u0308",\u1FE9:"\u03A5\u0304",\u1FE8:"\u03A5\u0306",\u038F:"\u03A9\u0301",\u1FFA:"\u03A9\u0300"},Jt=class r{constructor(e,t){this.mode=void 0,this.gullet=void 0,this.settings=void 0,this.leftrightDepth=void 0,this.nextToken=void 0,this.mode="math",this.gullet=new Zr(e,t,this.mode),this.settings=t,this.leftrightDepth=0}expect(e,t){if(t===void 0&&(t=!0),this.fetch().text!==e)throw new T("Expected '"+e+"', got '"+this.fetch().text+"'",this.fetch());t&&this.consume()}consume(){this.nextToken=null}fetch(){return this.nextToken==null&&(this.nextToken=this.gullet.expandNextToken()),this.nextToken}switchMode(e){this.mode=e,this.gullet.switchMode(e)}parse(){this.settings.globalGroup||this.gullet.beginGroup(),this.settings.colorIsTextColor&&this.gullet.macros.set("\\color","\\textcolor");try{var e=this.parseExpression(!1);return this.expect("EOF"),this.settings.globalGroup||this.gullet.endGroup(),e}finally{this.gullet.endGroups()}}subparse(e){var t=this.nextToken;this.consume(),this.gullet.pushToken(new C0("}")),this.gullet.pushTokens(e);var a=this.parseExpression(!1);return this.expect("}"),this.nextToken=t,a}parseExpression(e,t){for(var a=[];;){this.mode==="math"&&this.consumeSpaces();var n=this.fetch();if(r.endOfExpression.indexOf(n.text)!==-1||t&&n.text===t||e&&se[n.text]&&se[n.text].infix)break;var i=this.parseAtom(t);if(i){if(i.type==="internal")continue}else break;a.push(i)}return this.mode==="text"&&this.formLigatures(a),this.handleInfixNodes(a)}handleInfixNodes(e){for(var t=-1,a,n=0;n=0&&this.settings.reportNonstrict("unicodeTextInMathMode",'Latin-1/Unicode text character "'+t[0]+'" used in math mode',e);var u=K[this.mode][t].group,h=A0.range(e),m;if(Is.hasOwnProperty(u)){var v=u;m={type:"atom",mode:this.mode,family:v,loc:h,text:t}}else m={type:u,mode:this.mode,loc:h,text:t};l=m}else if(t.charCodeAt(0)>=128)this.settings.strict&&(jn(t.charCodeAt(0))?this.mode==="math"&&this.settings.reportNonstrict("unicodeTextInMathMode",'Unicode text character "'+t[0]+'" used in math mode',e):this.settings.reportNonstrict("unknownSymbol",'Unrecognized Unicode character "'+t[0]+'"'+(" ("+t.charCodeAt(0)+")"),e)),l={type:"textord",mode:"text",loc:A0.range(e),text:t};else return null;if(this.consume(),i)for(var g=0;gQ1(m.left)).join("|")+")");a=e.search(i),a!==-1;){a>0&&(n.push({type:"text",data:e.slice(0,a)}),e=e.slice(a));var l=t.findIndex(m=>e.startsWith(m.left));if(a=J1(t[l].right,e,t[l].left.length),a===-1)break;var u=e.slice(0,a+t[l].right.length),h=el.test(u)?u:e.slice(t[l].left.length,a);n.push({type:"math",data:h,rawData:u,display:t[l].display}),e=e.slice(a+t[l].right.length)}return e!==""&&n.push({type:"text",data:e}),n},rl=function(e,t){var a=tl(e,t.delimiters);if(a.length===1&&a[0].type==="text")return null;for(var n=document.createDocumentFragment(),i=0;iv.indexOf(" "+b+" ")===-1);g&&r(n,t)}()}},_i=function(e,t){if(!e)throw new Error("No element provided to render");var a={};for(var n in t)t.hasOwnProperty(n)&&(a[n]=t[n]);a.delimiters=a.delimiters||[{left:"$$",right:"$$",display:!0},{left:"\\(",right:"\\)",display:!1},{left:"\\begin{equation}",right:"\\end{equation}",display:!0},{left:"\\begin{align}",right:"\\end{align}",display:!0},{left:"\\begin{alignat}",right:"\\end{alignat}",display:!0},{left:"\\begin{gather}",right:"\\end{gather}",display:!0},{left:"\\begin{CD}",right:"\\end{CD}",display:!0},{left:"\\[",right:"\\]",display:!0}],a.ignoredTags=a.ignoredTags||["script","noscript","style","textarea","pre","code","option"],a.ignoredClasses=a.ignoredClasses||[],a.errorCallback=a.errorCallback||console.error,a.macros=a.macros||{},al(e,a)};function nl(r,e){return r.reduce(([t,a],n)=>e(n)?[[...t,n],a]:[t,[...a,n]],[[],[]])}window.addEventListener("load",r=>{_i(document.body);let e=l=>{for(;l!=null;)l.nodeName=="DETAILS"&&(l.open=!0),l=l.parentNode},t=l=>{if(l.target.tagName==="A")return;let h=l.target.closest("span[data-target]").getAttribute("data-target"),m=document.querySelector(h);e(m),window.location=h};[...document.querySelectorAll("[data-target^='#']")].forEach(l=>l.addEventListener("click",t));let a=document.querySelector("ninja-keys"),i=`${document.querySelector("html").getAttribute("data-base-url")}forest.json`;fetch(i).then(l=>l.json()).then(l=>{let u=[],h='',m='';window.sourcePath&&u.push({id:"edit",title:"Edit current tree in Visual Studio Code",section:"Commands",hotkey:"cmd+e",icon:h,handler:()=>{window.location.href=`vscode://file/${window.sourcePath}`}});let v=k=>k.tags?k.tags.includes("top"):!1,g=(k,A,C)=>{let R=`${k.taxon?k.title?`${k.taxon}. ${k.title}`:k.taxon:k.title?k.title:"Untitled"} [${k.uri}]`;u.push({id:k.uri,title:R,section:A,icon:C,handler:()=>{window.location.href=k.route}})},[b,x]=nl(l,v);b.forEach(k=>g(k,"Top Trees",m)),x.forEach(k=>g(k,"All Trees",null)),a.data=u})});var il=2e3,st;function qi(){st=new EventSource("/refresh"),st.onmessage=function(r){r.data=="refresh"?(st.close(),location.reload()):console.log(r.data)},st.onerror=function(r){st.close(),setTimeout(qi,il)}}qi();})(); + please report what input caused this bug`);return a=a.slice(1,-1),{type:"verb",mode:"text",body:a,star:n}}Pn.hasOwnProperty(t[0])&&!K[this.mode][t[0]]&&(this.settings.strict&&this.mode==="math"&&this.settings.reportNonstrict("unicodeTextInMathMode",'Accented Unicode text character "'+t[0]+'" used in math mode',e),t=Pn[t[0]]+t.slice(1));var i=G1.exec(t);i&&(t=t.substring(0,i.index),t==="i"?t="\u0131":t==="j"&&(t="\u0237"));var l;if(K[this.mode][t]){this.settings.strict&&this.mode==="math"&&Fr.indexOf(t)>=0&&this.settings.reportNonstrict("unicodeTextInMathMode",'Latin-1/Unicode text character "'+t[0]+'" used in math mode',e);var u=K[this.mode][t].group,h=A0.range(e),m;if(Is.hasOwnProperty(u)){var v=u;m={type:"atom",mode:this.mode,family:v,loc:h,text:t}}else m={type:u,mode:this.mode,loc:h,text:t};l=m}else if(t.charCodeAt(0)>=128)this.settings.strict&&(jn(t.charCodeAt(0))?this.mode==="math"&&this.settings.reportNonstrict("unicodeTextInMathMode",'Unicode text character "'+t[0]+'" used in math mode',e):this.settings.reportNonstrict("unknownSymbol",'Unrecognized Unicode character "'+t[0]+'"'+(" ("+t.charCodeAt(0)+")"),e)),l={type:"textord",mode:"text",loc:A0.range(e),text:t};else return null;if(this.consume(),i)for(var g=0;gQ1(m.left)).join("|")+")");a=e.search(i),a!==-1;){a>0&&(n.push({type:"text",data:e.slice(0,a)}),e=e.slice(a));var l=t.findIndex(m=>e.startsWith(m.left));if(a=J1(t[l].right,e,t[l].left.length),a===-1)break;var u=e.slice(0,a+t[l].right.length),h=el.test(u)?u:e.slice(t[l].left.length,a);n.push({type:"math",data:h,rawData:u,display:t[l].display}),e=e.slice(a+t[l].right.length)}return e!==""&&n.push({type:"text",data:e}),n},rl=function(e,t){var a=tl(e,t.delimiters);if(a.length===1&&a[0].type==="text")return null;for(var n=document.createDocumentFragment(),i=0;iv.indexOf(" "+b+" ")===-1);g&&r(n,t)}()}},_i=function(e,t){if(!e)throw new Error("No element provided to render");var a={};for(var n in t)t.hasOwnProperty(n)&&(a[n]=t[n]);a.delimiters=a.delimiters||[{left:"$$",right:"$$",display:!0},{left:"\\(",right:"\\)",display:!1},{left:"\\begin{equation}",right:"\\end{equation}",display:!0},{left:"\\begin{align}",right:"\\end{align}",display:!0},{left:"\\begin{alignat}",right:"\\end{alignat}",display:!0},{left:"\\begin{gather}",right:"\\end{gather}",display:!0},{left:"\\begin{CD}",right:"\\end{CD}",display:!0},{left:"\\[",right:"\\]",display:!0}],a.ignoredTags=a.ignoredTags||["script","noscript","style","textarea","pre","code","option"],a.ignoredClasses=a.ignoredClasses||[],a.errorCallback=a.errorCallback||console.error,a.macros=a.macros||{},al(e,a)};function nl(r,e){return r.reduce(([t,a],n)=>e(n)?[[...t,n],a]:[t,[...a,n]],[[],[]])}window.addEventListener("load",r=>{_i(document.body,{fleqn:!0});let e=l=>{for(;l!=null;)l.nodeName=="DETAILS"&&(l.open=!0),l=l.parentNode},t=l=>{if(l.target.tagName==="A")return;let h=l.target.closest("span[data-target]").getAttribute("data-target"),m=document.querySelector(h);e(m),window.location=h};[...document.querySelectorAll("[data-target^='#']")].forEach(l=>l.addEventListener("click",t));let a=document.querySelector("ninja-keys"),i=`${document.querySelector("html").getAttribute("data-base-url")}forest.json`;fetch(i).then(l=>l.json()).then(l=>{let u=[],h='',m='';window.sourcePath&&u.push({id:"edit",title:"Edit current tree in Visual Studio Code",section:"Commands",hotkey:"cmd+e",icon:h,handler:()=>{window.location.href=`vscode://file/${window.sourcePath}`}});let v=k=>k.tags?k.tags.includes("top"):!1,g=(k,A,C)=>{let R=`${k.taxon?k.title?`${k.taxon}. ${k.title}`:k.taxon:k.title?k.title:"Untitled"} [${k.uri}]`;u.push({id:k.uri,title:R,section:A,icon:C,handler:()=>{window.location.href=k.route}})},[b,x]=nl(l,v);b.forEach(k=>g(k,"Top Trees",m)),x.forEach(k=>g(k,"All Trees",null)),a.data=u})});var il=2e3,st;function qi(){st=new EventSource("/refresh"),st.onmessage=function(r){r.data=="refresh"?(st.close(),location.reload()):console.log(r.data)},st.onerror=function(r){st.close(),setTimeout(qi,il)}}qi();})(); /*! Bundled license information: @lit/reactive-element/css-tag.js: diff --git a/manual/theme/javascript-source/forester.js b/manual/theme/javascript-source/forester.js index c99e90a6..a27a8ea7 100644 --- a/manual/theme/javascript-source/forester.js +++ b/manual/theme/javascript-source/forester.js @@ -10,7 +10,7 @@ function partition(array, isValid) { } window.addEventListener("load", (event) => { - autoRenderMath(document.body) + autoRenderMath(document.body, { fleqn: true }) const openAllDetailsAbove = elt => { while (elt != null) { diff --git a/manual/theme/style.css b/manual/theme/style.css index a2d4c4e3..8b818807 100644 --- a/manual/theme/style.css +++ b/manual/theme/style.css @@ -85,10 +85,15 @@ h6 { margin-bottom: 0; } -h5, -h6, p { margin-top: 0; + margin-bottom: 0; +} + +section.block > details { + > :not(:first-child)+* { + margin-top: 1rem; + } } h1, @@ -263,6 +268,12 @@ section .block[data-taxon] details>summary>header>h1 { font-size: 12pt; } +section .block[data-taxon] { + border-left-style: solid; + border-width: 2px; + border-radius: 0px; +} + span.taxon { color: #444; font-weight: bolder; @@ -298,7 +309,8 @@ section.block>details { section.block>details[open] { - margin-bottom: 1em; + /* border-right: 1px; */ + margin-bottom: 0; } diff --git a/manual/trees/0001.tree b/manual/trees/0001.tree index 38184706..520c6463 100644 --- a/manual/trees/0001.tree +++ b/manual/trees/0001.tree @@ -1,7 +1,5 @@ \title{Coln manual} -\p{Coln is a database with an expressive language for schemas, queries, and migrations. This document forms the manual for Coln.} - \transclude{002H} \transclude{0002} \transclude{000K} diff --git a/manual/trees/0028.tree b/manual/trees/0028.tree index 9b648bc3..3f9abe86 100644 --- a/manual/trees/0028.tree +++ b/manual/trees/0028.tree @@ -16,7 +16,7 @@ \p{The reason type theory may be usefully applied to propositional logic because all of the connectives of propositional logic (and, or, not, forall, exists, etc.) satisfy universal properties; this is the same as the reason why type theory may be applied to any other area.} -\p{The way that type theory may be applied to a particular area is via the development of \em{a particular} type theory. Confusion between type theory as a subject and the concept of \em{a type theory} as a mathematical object is an unfortunate side effect of the nomenclature, because “ breaks with the convention that in group theory, we study groups, in field theory we study fields, or in category theory we study categories.} +\p{The way that type theory may be applied to a particular area is via the development of \em{a particular} type theory. Confusion between type theory as a subject and the concept of \em{a type theory} as a mathematical object is an unfortunate side effect of the nomenclature, because the use of “type theory” to describe the field breaks with the convention that in group theory, we study groups, in field theory we study fields, or in category theory we study categories. However, in type theory, we study type theories.} \p{A particular type theory is merely a syntactic formalization of some collection of universal properties, consisting of a collection of \em{rules} by which we judge that a certain piece of syntax is \em{well-typed}. The beauty of universal properties is that each universal property is quite self-contained, so a type theory may be designed by systematically observing which universal properties the objects of interest support, and then adding the standard type-theoretic rules for those universal properties to one's type theory.} diff --git a/manual/trees/002A.tree b/manual/trees/002A.tree index ed3c99ba..2ca950d7 100644 --- a/manual/trees/002A.tree +++ b/manual/trees/002A.tree @@ -7,20 +7,10 @@ \p{Following the principles of this manual, this is \em{not} a mathematical paper; there will be a more formal account of this type theory, but that is in progress. Rather, this is a conceptual account that makes reference to mathematics.} -\p{In [The Elephant](johnstone-2002-sketches), Johnstone makes the following definitions for “theory”; we call this an \em{elephant theory} in order to distinguish it from other notions of theory we might consider.} +\transclude{002M} -\transclude{002C} +\transclude{002N} -\transclude{002E} - -\transclude{002F} - -\transclude{002D} - -\transclude{002G} - -\transclude{002I} - -\p{The remainder of this section is simply an investigation of what type formers are supported in #{\ms{ElTh}}.} +\transclude{002S} \transclude{002J} diff --git a/manual/trees/002D.tree b/manual/trees/002D.tree index 573fc285..40798388 100644 --- a/manual/trees/002D.tree +++ b/manual/trees/002D.tree @@ -2,14 +2,6 @@ \taxon{Definition} \import{prelude} -\p{\defcase{Geometric theories} may be consicely defined as the elephant theories built up via a sequence of [product-inserter-equifier limits](pie-limit) starting from the object classifier.} - -\p{We expand this to give more intuition.} - -\p{If #{T} is a theory, a \defcase{simple functional extension} of #{T} is another theory #{T'} given as the \em{inserter} of two geometric constructs #{F,G \colon T \to \bb{O}}. Intuitively, #{T'} is the theory given by freely adding a new morphism between the “objects” #{F} and #{G}.} - -\p{If #{T} is a theory, a \defcase{simple equational extension} of #{T} is another theory #{T'} given as the \em{equifier} of two indexed natural transformations #{\alpha, \beta \colon F \Rightarrow G}, where #{F} and #{G} are geometric constructs. Intuitively, #{T'} is the theory given by adding a new equality between morphisms of “objects”.} - -\p{A \defcase{geometric theory} is a theory built up by a finite sequence #{T_0,\ldots,T_n} of simple functional extensions and simple equational extensions starting from #{T_0 = \bb{O}^m} for some finite #{m}.} +\p{A \defcase{geometric theory} is an elephant theory built up by a finite sequence #{T_0,\ldots,T_n} of [simple functional extensions](002K) and [simple equational extensions](002L) starting from #{T_0 = \bb{O}^m} for some finite #{m}.} \p{(See [Elephant](johnstone-2002-sketches) Definition 4.2.7, note that Johnstone gives a slightly different definition, using \em{simple geometric quotients} in place of simple equational extensions, which use inverters instead of equifiers. The name “simple equational extension” is not known to us to be previously used, but it follows the schema of “simple functional extension.”)} diff --git a/manual/trees/002I.tree b/manual/trees/002I.tree index 52503dc9..5cda7e57 100644 --- a/manual/trees/002I.tree +++ b/manual/trees/002I.tree @@ -6,10 +6,10 @@ \p{Intuitively, #{\ms{Ty}(\Gamma)} is “elephant theories relative to #{\Gamma}.” This is because #{\groth \Gamma} is the category of topoi equipped with a model of #{\Gamma}; if #{\Gamma} were a geometric theory then #{\groth \Gamma} would be equivalent to #{\ms{BTop}/\mc{S}[\Gamma]}.} -\p{Then define #{\ms{Tm} \colon (\groth \ms{Ty})\op \to \ms{Set}} by letting #{\ms{Tm}(\Gamma, A)} be the set of \em{sections} of #{A}. A section #{a} is a natural assignment of #{a(\mc{E}, M) \colon A(\mc{E}, M)} for #{(\mc{E},M) \in \groth \Gamma}.} +\p{Then define #{\ms{Tm} \colon (\groth \ms{Ty})\op \to \ms{SET}} by letting #{\ms{Tm}(\Gamma, A)} be the set of \em{sections} of #{A}. A section #{a} is a natural assignment of #{a(\mc{E}, M) \colon A(\mc{E}, M)} for #{(\mc{E},M) \in \groth \Gamma}.} \p{Context extension is given in the following way. Suppose that #{\Gamma \colon (\ms{BTop}/\mc{S})\op \to \ms{Cat}} is a context and #{A \colon \ms{Ty}(\Gamma)}. Then #{\Gamma \ext A \colon (\ms{BTop}/\mc{S})\op \to \ms{Cat}} is defined by #{(\Gamma \ext A)(\mc{E}) = (M \colon \Gamma(\mc{E})) \times A(\mc{E},M)}.} -\p{Then finally we have weakening and the variable rule given by the first and second projections out of #{\Gamma \ext A}.} +\p{Weakening and the variable rule are by the first and second projections out of #{\Gamma \ext A}.} \p{Note that even though topoi and elephant theories are non-trivially 2-categorical, #{(\ms{ElTh},\ms{Ty},\ms{Tm})} forms nevertheless a strict (albeit quite large) category with families.} diff --git a/manual/trees/002J.tree b/manual/trees/002J.tree index 9eb59ccb..d2bc659d 100644 --- a/manual/trees/002J.tree +++ b/manual/trees/002J.tree @@ -1 +1,6 @@ -\date{2026-05-27T09:54:56Z} +\import{prelude} +\title{Type formers} + +\p{One of the nice things about categorical semantics is that once we have fixed the basic structure (the category with families), the type theory essentially writes itself, in the sense that we may just look through various standard type formers and ask whether or not the semantics has the relevant universal property or not.} + +\transclude{002V} diff --git a/manual/trees/002K.tree b/manual/trees/002K.tree new file mode 100644 index 00000000..ee89c2f7 --- /dev/null +++ b/manual/trees/002K.tree @@ -0,0 +1,5 @@ +\title{Simple functional extension} +\taxon{Definition} +\import{prelude} + +\p{If #{T} is a theory, a \defcase{simple functional extension} of #{T} is another theory #{T'} given as the \em{inserter} of two geometric constructs #{F,G \colon T \to \bb{O}}. Intuitively, #{T'} is the theory given by freely adding a new morphism between the “objects” #{F} and #{G}.} diff --git a/manual/trees/002L.tree b/manual/trees/002L.tree new file mode 100644 index 00000000..fd8a811c --- /dev/null +++ b/manual/trees/002L.tree @@ -0,0 +1,5 @@ +\title{Simple equational extension} +\import{prelude} +\taxon{Definition} + +\p{If #{T} is a theory, a \defcase{simple equational extension} of #{T} is another theory #{T'} given as the \em{equifier} of two indexed natural transformations #{\alpha, \beta \colon F \Rightarrow G}, where #{F} and #{G} are geometric constructs. Intuitively, #{T'} is the theory given by adding a new equality between morphisms of “objects”.} diff --git a/manual/trees/002M.tree b/manual/trees/002M.tree new file mode 100644 index 00000000..d6d861ee --- /dev/null +++ b/manual/trees/002M.tree @@ -0,0 +1,17 @@ +\title{A refresher on geometric theories} + +\p{In this section, we briefly review the approach to geometric theories followed in [The Elephant](johnstone-2002-sketches).} + +\transclude{002C} + +\transclude{002E} + +\transclude{002F} + +\transclude{002K} + +\transclude{002L} + +\transclude{002D} + +\transclude{002G} diff --git a/manual/trees/002N.tree b/manual/trees/002N.tree new file mode 100644 index 00000000..255b34bd --- /dev/null +++ b/manual/trees/002N.tree @@ -0,0 +1,15 @@ +\title{Types and terms} +\import{prelude} + +\p{In this section, we build a [category with families](cwf) #{\mb{E}} out of elephant theories, which gives the semantics of types and terms in our type theory.} + +\p{Categories with families have many parts; we build up the structure in sections. We follow [Kovacs](kovacs-2022-typetheoretic) in presenting a category with families as a model of a GAT. As we give the semantics for each part of the GAT, we write out the relevant part of the signature with a \check next to it to signify that that part of the GAT is defined.} + +\transclude{002O} + +\transclude{002P} + +\transclude{002Q} + +\transclude{002R} + diff --git a/manual/trees/002O.tree b/manual/trees/002O.tree new file mode 100644 index 00000000..1f3d096e --- /dev/null +++ b/manual/trees/002O.tree @@ -0,0 +1,13 @@ +\import{prelude} +\title{Category structure of #{\mb{E}}} + +\p{The category for #{\mb{E}} is just the category of [elephant theories](002C), where the morphisms are 2-natural transformations.} + +##{\begin{align*} +&\ms{Con} \colon \ms{Type} \quad \check \\ +&\ms{Sub} \colon \ms{Con} \to \ms{Con} \to \ms{Type} \quad \check +\end{align*}} + +\p{We omit some parts of the GAT signature; for instance here we omit the parts which declare that #{\ms{Con}} and #{\ms{Sub}} form a category. We refer to this category overall as #{\bb{C}_{\mb{E}}}.} + +\p{This category has a terminal object given by the functor constant at #{1}, the terminal category; we refer to this by #{\cdot} in light of its role as the empty context.} diff --git a/manual/trees/002P.tree b/manual/trees/002P.tree new file mode 100644 index 00000000..ff3916ac --- /dev/null +++ b/manual/trees/002P.tree @@ -0,0 +1,14 @@ +\import{prelude} +\title{Types in #{\mb{E}}} + +\p{Given a context #{\Gamma}, a type in #{\Gamma} is a 2-functor #{A \colon \left(\groth \Gamma\right)\op \to \ms{CAT}}.} + +##{\ms{Ty} \colon \ms{Con} \to \ms{Type} \quad \check} + +\p{Note that #{\ms{Ty}\,\cdot} is again just the type of elephant theories.} + +\p{In general, #{\groth \Gamma} is the 2-category of topoi equipped with a model of #{\Gamma}. In the case that #{\Gamma} is a geometric theory, this is equivalent to elephant theories where #{\ms{BTop}/\ms{S}} is replaced with the #{\ms{BTop}/\ms{S}[\Gamma]}, where #{\ms{S}[\Gamma]} is the classifying topos for #{\Gamma}. Thus, #{\ms{Ty}\,\Gamma} can be thought of as the collection of elephant theories relative to #{\Gamma}.} + +\p{It is not hard to see that #{\ms{Ty}} forms a presheaf over #{\bb{C}_{\mb{E}}} because we can apply the Grothendieck construction to the 2-natural transformation #{\gamma \colon \Delta \To \Gamma} to get #{\groth \gamma \colon \groth \Delta \to \groth \Gamma}, and then precomposition with #{\groth \gamma} gives us the required map from #{\ms{Ty}\,\Gamma} to #{\ms{Ty}\,\Delta}.} + +##{{-}[-] \colon \{\Delta\;\Gamma \colon \ms{Con}\} \to \ms{Ty}\,\Gamma \to (\ms{Sub}\,\Delta\,\Gamma) \to \ms{Ty}\,\Delta \quad \check} diff --git a/manual/trees/002Q.tree b/manual/trees/002Q.tree new file mode 100644 index 00000000..093b7541 --- /dev/null +++ b/manual/trees/002Q.tree @@ -0,0 +1,19 @@ +\import{prelude} +\title{Terms in #{\mb{E}}} + +\p{Given a context #{\Gamma} and a type #{A \colon \left(\groth \Gamma\right)\op \to \ms{CAT}}, a term #{a} of type #{A} is a 2-section of #{A}.} + +##{\ms{Tm} \colon (\Gamma \colon \ms{Con}) \to \ms{Ty}\,\Gamma \to \ms{Type} \quad \check} + +\p{The categorical way to define “2-section” would be as a strict 2-functor #{a \colon \groth \Gamma \to \groth A} that is a strict section of the projection. A more type-theoretic way to define “2-section” would be to say a 2-section is a map #{a \colon \left((\mc{E},M) \colon \groth \Gamma\right) \to A(\mc{E},M)} such that #{a(\mc{E},M)} is 2-functorial in #{\mc{E}} and #{M}.} + +\p{Given #{\gamma \colon \Delta \To \Gamma}, we may define #{a[\gamma] \colon \ms{Tm}\,\Delta\,(A[\gamma])} by} + +##{a[\gamma]\,\left((\mc{E}, M) \colon \groth \Delta \right) = a(\mc{E}, \gamma_{\mc{E}}(M)) \colon ({A[\gamma]}(\mc{E}, M) = A(\mc{E}, \gamma_{\mc{E}}(M)))} + +\p{This turns #{\ms{Tm}} into an indexed presheaf over #{\ms{Ty}}.} + +##{\begin{align*} + &{-}[-] \colon \{\Delta\;\Gamma \colon \ms{Con}\} \to \{A \colon \ms{Ty}\,\Gamma\} \to \\ + &\quad \ms{Tm}\,\Gamma\,A \to (\gamma \colon \Delta \To \Gamma) \to \ms{Tm}\,\Delta\,(A[\gamma]) \quad \check +\end{align*}} diff --git a/manual/trees/002R.tree b/manual/trees/002R.tree new file mode 100644 index 00000000..e870de19 --- /dev/null +++ b/manual/trees/002R.tree @@ -0,0 +1,28 @@ +\import{prelude} +\title{Context extension in #{\mb{E}}} + +\p{Given a context #{\Gamma} and type #{A}, we define the context extension #{\Gamma \ext A} by} + +##{(\Gamma \ext A)(\mc{E} \colon \ms{BTop}/\mc{S}) = (M \colon \Gamma(\mc{E})) \times A(\mc{E},M)} + +\p{extended suitably to produce a category, and to be 2-functorial.} + +##{{-}\ext{-} \colon (\Gamma \colon \ms{Con}) \to \ms{Ty}\,\Gamma \to \ms{Con} \quad \check} + +\p{We then have the weakening substitution given by first projection and the variable rule given by second projection.} + +##{\begin{align*} +&\ms{p} \colon \{\Gamma \colon \ms{Con}\} \to \{A \colon \ms{Ty}\,\Gamma\} \to (\Gamma \ext A \To \Gamma) \quad \check \\ +&\ms{q} \colon \{\Gamma \colon \ms{Con}\} \to \{A \colon \ms{Ty}\,\Gamma\} \to \ms{Tm}\,(\Gamma \ext A)\,(A[\ms{p}]) \quad \check +\end{align*}} + +\p{Finally, context comprehension is defined by pairing.} + +##{\begin{align*} + &({-},{-}) \colon \{\Delta\;\Gamma \colon \ms{Con}\} \to \{A \colon \ms{Ty}\,\Gamma\} \to \\ + &\quad (\gamma \colon \Delta \To \Gamma) \to \ms{Tm}\,\Delta\,(A[\gamma]) \to (\Delta \To \Gamma \ext A) \quad \check +\end{align*}} + +\p{Weakening/variable and context comprehension then can be used to form an isomorphism:} + +##{(\Delta \Rightarrow \Gamma \ext A) \cong (\gamma \colon \Delta \Rightarrow \Gamma) \times \ms{Tm}\,\Delta\,(A[\gamma]) \quad \check} diff --git a/manual/trees/002S.tree b/manual/trees/002S.tree new file mode 100644 index 00000000..9cbed470 --- /dev/null +++ b/manual/trees/002S.tree @@ -0,0 +1,12 @@ +\title{Levels and universes} +\import{prelude} + +\p{The basic structure of types and terms works for general elephant theories, but we are most concerned with geometric theories. To handle this, we introduce judgments inspired by the approach to levels and universes introduced by Jon Sterling in [[sterling-2025-fuss-free]].} + +\p{Note that Jon uses this for levels in MLTT, where the type theory “at each level” is essentially the same. However, in our use of levels, different rules in the type theory will only apply at certain levels.} + +\transclude{002U} + +\transclude{002T} + +\transclude{002W} diff --git a/manual/trees/002T.tree b/manual/trees/002T.tree new file mode 100644 index 00000000..e795f146 --- /dev/null +++ b/manual/trees/002T.tree @@ -0,0 +1,16 @@ +\title{Geometric theories} +\import{prelude} + +\p{We introduce a judgment on types capturing when an elephant theory is a geometric theory. Confusingly enough, in Coln we call these types \defcase{theories}; general types (elephant theories) are called top-level types.} + +##{\ms{IsTheory} \colon \{\Gamma \colon \ms{Con}\} \to \ms{Ty}\,\Gamma \to \ms{Prop}} + +\p{A proof of #{\ms{IsTheory}\,A} is a construction of #{A} as a sequence of simple functional and simple equational extensions of the object classifier, establishing it as a [geometric theory](002D). As #{\ms{IsTheory}\,A} is a proposition, we propositionally truncate the type of such constructions.} + +##{\ms{IsTheory} \colon \{\Gamma \colon \ms{Con}\} \to \ms{Ty}\,\Gamma \to \ms{Prop} \quad \check} + +\p{We can then internalize this into a universe. The universe #{\ms{Theory} \colon \ms{Ty}\,\cdot} sends a topos #{\mc{E}} to the category of geometric theories #{A \colon \ms{BTop}/\mc{E} \to \ms{CAT}}.} + +##{\ms{Tm}\,\Gamma\,\ms{Theory} \cong (A \colon \ms{Ty}\,\Gamma) \times \ms{IsTheory}\,A \quad \check} + +\p{This is the shakiest part of the semantics for this type theory; it may be that non-strictness or size issues make this universe infeasible. However, this can be fixed by moving to a two-level type theory. “Presheaves over elephant theories” seems a bit absurd though, so hopefully this can work out as is.} diff --git a/manual/trees/002U.tree b/manual/trees/002U.tree new file mode 100644 index 00000000..b4f0a338 --- /dev/null +++ b/manual/trees/002U.tree @@ -0,0 +1,16 @@ +\title{Sets} +\import{prelude} + +\p{We introduce a judgment on types capturing when an elephant theory is a [geometric construct](002F). We call such types \defcase{sets}.} + +##{\ms{IsSet} \colon \{\Gamma \colon \ms{Con}\} \to \ms{Ty}\,\Gamma \to \ms{Prop}} + +\p{A proof of #{\ms{IsSet}\,A} for #{A \colon \ms{Ty}\,\Gamma} is a natural choice of objects #{((\mc{E},M) \colon \groth \Gamma) \mapsto (X_{A}(\mc{E},M) \colon \mc{E})} such that #{A(\mc{E},M) \cong \mc{E}(1, X_{A}(\mc{E},M))}.} + +##{\ms{IsSet} \colon \{\Gamma \colon \ms{Con}\} \to \ms{Ty}\,\Gamma \to \ms{Prop} \quad \check} + +\p{We then have a universe #{\ms{Set}} which is given by the \em{weak} object classifier, which sends a topos #{\mc{E}} to the category of representable presheaves on #{\ms{Sh}(\mc{E})}. This is equivalent to the object classifier, but we use it because it makes the isomorphism below work out.} + +##{\ms{Tm}\,\Gamma\,\ms{Set} \cong (A \colon \ms{Ty}\,\Gamma) \times \ms{IsSet}\,A \quad \check} + +\p{In the above isomorphism, we call the right-to-left direction \defcase{encoding} and the left-to-right direction \defcase{decoding}.} diff --git a/manual/trees/002V.tree b/manual/trees/002V.tree new file mode 100644 index 00000000..be58c3b8 --- /dev/null +++ b/manual/trees/002V.tree @@ -0,0 +1,22 @@ +\title{Record types} +\import{prelude} + +\p{In the Coln implementation, we have general #{n}-ary record types with named fields. However, for the sake of simplicity, here we only cover binary dependent records, also known as #{\Sigma}-types.} + +##{\begin{align*} + &\Sigma \colon \{\Gamma \colon \ms{Con}\} \to (A \colon \ms{Ty}\,\Gamma) \to (\ms{Ty}\,(\Gamma \ext A)) \to \ms{Ty}\,\Gamma \\ + &\ms{Tm}\,\Gamma\,(\Sigma\,A\,B) \cong (a \colon \ms{Tm}\,\Gamma\,A) \times \ms{Tm}\,\Gamma\,(B[(1_\Gamma, a)]) +\end{align*}} + +\p{This is fairly straightforward to give semantics to. Fix some elephant theory #{\Gamma}, and let #{A \colon (\groth \Gamma)\op \to \ms{CAT}}, #{B \colon (\groth \Gamma \ext A)\op \to \ms{CAT}}. Then #{(\Sigma\,A\,B) \colon (\groth \Gamma)\op \to \ms{CAT}} may be defined by} + +##{(\Sigma\,A\,B)(\mc{E},M) = (a \colon A(\mc{E},M)) \times B(\mc{E},(M,a))} + +\p{It is straightforward to then interpret the projections, etc.} + +##{\begin{align*} + &\Sigma \colon \{\Gamma \colon \ms{Con}\} \to (A \colon \ms{Ty}\,\Gamma) \to (\ms{Ty}\,(\Gamma \ext A)) \to \ms{Ty}\,\Gamma \quad \check \\ + &\ms{Tm}\,\Gamma\,(\Sigma\,A\,B) \cong (a \colon \ms{Tm}\,\Gamma\,A) \times \ms{Tm}\,\Gamma\,(B[(1_\Gamma, a)]) \quad \check +\end{align*}} + +\p{Slightly less trivial to verify is that #{\Sigma} preserves the levels of its constituent types.} diff --git a/manual/trees/002W.tree b/manual/trees/002W.tree new file mode 100644 index 00000000..338425aa --- /dev/null +++ b/manual/trees/002W.tree @@ -0,0 +1,12 @@ +\title{Sets are geometric theories} +\import{prelude} + +\p{Any [set](002U) is a [geometric theory](002T), in the sense that we have.} + +##{\ms{SetImpliesTheory} \colon \{\Gamma \colon \ms{Con}\} \to \{A \colon \ms{Ty}\,\Gamma\} \to \ms{IsSet}\,A \to \ms{IsTheory}\,A} + +\p{This is because #{\ms{IsSet}\,A} implies that #{A} is represented by a 2-natural transformation #{X_A} into the object classifier, and thus #{A} is a simple functional extension of the empty theory given by postulating a morphism #{1 \to X_A}. In other words, #{A} is really “the theory of a global element of #{X_A}”.} + +##{\ms{SetImpliesTheory} \colon \{\Gamma \colon \ms{Con}\} \to \{A \colon \ms{Ty}\,\Gamma\} \to \ms{IsSet}\,A \to \ms{IsTheory}\,A \quad \check} + +\p{One can use #{\ms{SetImpliesTheory}} along with the encoding and decoding functions for #{\ms{Set}} and #{\ms{Theory}} in order to make a function #{\ms{Tm}\,\Gamma\,\ms{Set} \to \ms{Tm}\,\Gamma\,\ms{Theory}}. The advantage of #{\ms{SetImpliesTheory}} over directly postulating this function is that the way we have set things up, promotion from #{\ms{Set}} to #{\ms{Theory}} automatically commutes with coding/decoding.} diff --git a/manual/trees/glossary/cwf.tree b/manual/trees/glossary/cwf.tree new file mode 100644 index 00000000..7cbaf17a --- /dev/null +++ b/manual/trees/glossary/cwf.tree @@ -0,0 +1,4 @@ +\title{Category with Families} +\taxon{Term} + +\p{See: the [nlab page on categorical semantics of dependent type theory](https://ncatlab.org/nlab/show/categorical+semantics+of+dependent+type+theory#categories_with_families).} diff --git a/manual/trees/people/ambrus-kaposi.tree b/manual/trees/people/ambrus-kaposi.tree new file mode 100644 index 00000000..e3f68935 --- /dev/null +++ b/manual/trees/people/ambrus-kaposi.tree @@ -0,0 +1,2 @@ +\title{Ambrus Kaposi} +\taxon{person} \ No newline at end of file diff --git a/manual/trees/people/szumi-xie.tree b/manual/trees/people/szumi-xie.tree new file mode 100644 index 00000000..8d3a23b9 --- /dev/null +++ b/manual/trees/people/szumi-xie.tree @@ -0,0 +1,2 @@ +\title{Szumi Xie} +\taxon{person} \ No newline at end of file diff --git a/manual/trees/prelude.tree b/manual/trees/prelude.tree index 88f9bb2d..2fa7351b 100644 --- a/manual/trees/prelude.tree +++ b/manual/trees/prelude.tree @@ -14,8 +14,13 @@ \def\kw[x]{\strong{\x}} \def\ms[t]{\mathsf{\t}} +\def\mb[t]{\mathbf{\t}} \def\mc[t]{\mathcal{\t}} \def\bb[t]{\mathbb{\t}} \def\op{^\mathrm{op}} -\def\groth{\int} +\def\groth{{\textstyle\int}} \def\ext{\triangleright} + +\def\check{✅} + +\def\To{\Rightarrow} diff --git a/manual/trees/references/kaposi-2024-secondorder.tree b/manual/trees/references/kaposi-2024-secondorder.tree new file mode 100644 index 00000000..0e2817e9 --- /dev/null +++ b/manual/trees/references/kaposi-2024-secondorder.tree @@ -0,0 +1,22 @@ +\title{Second-Order Generalised Algebraic Theories: Signatures and First-Order Semantics} +\author{ambrus-kaposi} +\author{szumi-xie} +\date{2024} +\taxon{reference} +\meta{doi}{10.4230/LIPICS.FSCD.2024.10} +\meta{bibtex}{\verb>>| +@inproceedings{kaposi-2024-secondorder, + doi = {10.4230/LIPICS.FSCD.2024.10}, + url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.10}, + author = {Kaposi, Ambrus and Xie, Szumi}, + keywords = {Type theory, universal algebra, inductive types, quotient inductive types, higher-order abstract syntax, logical framework, Theory of computation → Type theory}, + language = {en}, + title = {Second-Order Generalised Algebraic Theories: Signatures and First-Order Semantics}, + journal = {LIPIcs, Volume 299, FSCD 2024}, + volume = {299}, + pages = {10:1-10:24}, + publisher = {Schloss Dagstuhl – Leibniz-Zentrum für Informatik}, + year = {2024}, + copyright = {Creative Commons Attribution 4.0 International license} +} +>>} \ No newline at end of file diff --git a/manual/trees/references/sterling-2025-fuss-free.tree b/manual/trees/references/sterling-2025-fuss-free.tree new file mode 100644 index 00000000..6c8e3497 --- /dev/null +++ b/manual/trees/references/sterling-2025-fuss-free.tree @@ -0,0 +1,4 @@ +\title{Fuss-free universe hierarchies} +\author{jon-sterling} +\taxon{Reference} +\meta{external}{https://www.jonmsterling.com/01HX/}