Skip to content

Commit

Permalink
deploy: bb4e6b8
Browse files Browse the repository at this point in the history
  • Loading branch information
@jonsterling
jonsterling committed Nov 18, 2024
1 parent 37fa737 commit d204ba4
Show file tree
Hide file tree
Showing 1,651 changed files with 41,433 additions and 41,433 deletions.
4 changes: 2 additions & 2 deletions abchfl-2021.xml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -101,15 +101,15 @@ href="cchm-2017.xml"
title="Cubical type theory: a constructive interpretation of the univalence axiom"
addr="cchm-2017"
type="local">theory</fr:link></fr:strong> that reorganizes the higher-dimensional structure discussed by considering all the points, lines, squares, cubes, hypercubes, and so-on that one can draw in a given type. The computational interpretation of the new cubical type theory can be split into two different conjectures:</fr:p><fr:tree
show-metadata="false"><fr:frontmatter><fr:authors /><fr:date><fr:year>2023</fr:year><fr:month>1</fr:month><fr:day>19</fr:day></fr:date><fr:anchor>7375</fr:anchor><fr:addr
show-metadata="false"><fr:frontmatter><fr:authors /><fr:date><fr:year>2023</fr:year><fr:month>1</fr:month><fr:day>19</fr:day></fr:date><fr:anchor>7347</fr:anchor><fr:addr
type="user">jms-000S</fr:addr><fr:route>jms-000S.xml</fr:route><fr:title
text="Cubical canonicity">Cubical canonicity</fr:title><fr:taxon>Conjecture</fr:taxon></fr:frontmatter><fr:mainmatter><fr:p>For any closed term <fr:tex
display="inline"><![CDATA[\cdot \vdash N:\mathsf {nat}]]></fr:tex> of cubical type theory, there exists a unique natural number <fr:tex
display="inline"><![CDATA[n\in \mathbb {N}]]></fr:tex> such that <fr:tex
display="inline"><![CDATA[\cdot \vdash N\equiv \bar {n}:\mathsf {nat}]]></fr:tex> where <fr:tex
display="inline"><![CDATA[\bar {n}]]></fr:tex> is the encoding of the number <fr:tex
display="inline"><![CDATA[n]]></fr:tex> as a term in the type theory.</fr:p></fr:mainmatter></fr:tree><fr:tree
show-metadata="false"><fr:frontmatter><fr:authors /><fr:date><fr:year>2023</fr:year><fr:month>1</fr:month><fr:day>19</fr:day></fr:date><fr:anchor>7376</fr:anchor><fr:addr
show-metadata="false"><fr:frontmatter><fr:authors /><fr:date><fr:year>2023</fr:year><fr:month>1</fr:month><fr:day>19</fr:day></fr:date><fr:anchor>7348</fr:anchor><fr:addr
type="user">jms-000T</fr:addr><fr:route>jms-000T.xml</fr:route><fr:title
text="Decidability of cubical type theory">Decidability of cubical type theory</fr:title><fr:taxon>Conjecture</fr:taxon></fr:frontmatter><fr:mainmatter><fr:p>The assertions <fr:tex
display="inline"><![CDATA[\Gamma \vdash {A}\ \textit {type}]]></fr:tex>, <fr:tex
Expand Down
14 changes: 7 additions & 7 deletions abigailpribisova.xml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
<?xml-stylesheet type="text/xsl" href="default.xsl"?>
<fr:tree
xmlns:fr="http://www.jonmsterling.com/jms-005P.xml"
root="false"><fr:frontmatter><fr:authors /><fr:anchor>7945</fr:anchor><fr:addr
root="false"><fr:frontmatter><fr:authors /><fr:anchor>7976</fr:anchor><fr:addr
type="user">abigailpribisova</fr:addr><fr:route>abigailpribisova.xml</fr:route><fr:title
text="Abigail Pribisova">Abigail Pribisova</fr:title><fr:meta
name="position">MPhil Student</fr:meta><fr:meta
Expand All @@ -12,24 +12,24 @@ title="University of Cambridge"
addr="ucam"
type="local">University of Cambridge</fr:link></fr:meta></fr:frontmatter><fr:mainmatter /><fr:backmatter><fr:tree
show-metadata="false"
hidden-when-empty="true"><fr:frontmatter><fr:anchor>7939</fr:anchor><fr:title
hidden-when-empty="true"><fr:frontmatter><fr:anchor>7970</fr:anchor><fr:title
text="References">References</fr:title></fr:frontmatter><fr:mainmatter /></fr:tree><fr:tree
show-metadata="false"
hidden-when-empty="true"><fr:frontmatter><fr:anchor>7940</fr:anchor><fr:title
hidden-when-empty="true"><fr:frontmatter><fr:anchor>7971</fr:anchor><fr:title
text="Context">Context</fr:title></fr:frontmatter><fr:mainmatter /></fr:tree><fr:tree
show-metadata="false"
hidden-when-empty="true"><fr:frontmatter><fr:anchor>7941</fr:anchor><fr:title
hidden-when-empty="true"><fr:frontmatter><fr:anchor>7972</fr:anchor><fr:title
text="Backlinks">Backlinks</fr:title></fr:frontmatter><fr:mainmatter /></fr:tree><fr:tree
show-metadata="false"
hidden-when-empty="true"><fr:frontmatter><fr:anchor>7943</fr:anchor><fr:title
hidden-when-empty="true"><fr:frontmatter><fr:anchor>7974</fr:anchor><fr:title
text="Related">Related</fr:title></fr:frontmatter><fr:mainmatter><fr:tree
show-metadata="true"
expanded="false"
toc="false"
numbered="false"><fr:frontmatter><fr:authors /><fr:anchor>7942</fr:anchor><fr:addr
numbered="false"><fr:frontmatter><fr:authors /><fr:anchor>7973</fr:anchor><fr:addr
type="user">ucam</fr:addr><fr:route>ucam.xml</fr:route><fr:title
text="University of Cambridge">University of Cambridge</fr:title><fr:taxon>Institution</fr:taxon><fr:meta
name="external">https://www.cam.ac.uk/</fr:meta></fr:frontmatter><fr:mainmatter /></fr:tree></fr:mainmatter></fr:tree><fr:tree
show-metadata="false"
hidden-when-empty="true"><fr:frontmatter><fr:anchor>7944</fr:anchor><fr:title
hidden-when-empty="true"><fr:frontmatter><fr:anchor>7975</fr:anchor><fr:title
text="Contributions">Contributions</fr:title></fr:frontmatter><fr:mainmatter /></fr:tree></fr:backmatter></fr:tree>
4 changes: 2 additions & 2 deletions acmz-2021.xml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -109,15 +109,15 @@ href="cchm-2017.xml"
title="Cubical type theory: a constructive interpretation of the univalence axiom"
addr="cchm-2017"
type="local">theory</fr:link></fr:strong> that reorganizes the higher-dimensional structure discussed by considering all the points, lines, squares, cubes, hypercubes, and so-on that one can draw in a given type. The computational interpretation of the new cubical type theory can be split into two different conjectures:</fr:p><fr:tree
show-metadata="false"><fr:frontmatter><fr:authors /><fr:date><fr:year>2023</fr:year><fr:month>1</fr:month><fr:day>19</fr:day></fr:date><fr:anchor>7375</fr:anchor><fr:addr
show-metadata="false"><fr:frontmatter><fr:authors /><fr:date><fr:year>2023</fr:year><fr:month>1</fr:month><fr:day>19</fr:day></fr:date><fr:anchor>7347</fr:anchor><fr:addr
type="user">jms-000S</fr:addr><fr:route>jms-000S.xml</fr:route><fr:title
text="Cubical canonicity">Cubical canonicity</fr:title><fr:taxon>Conjecture</fr:taxon></fr:frontmatter><fr:mainmatter><fr:p>For any closed term <fr:tex
display="inline"><![CDATA[\cdot \vdash N:\mathsf {nat}]]></fr:tex> of cubical type theory, there exists a unique natural number <fr:tex
display="inline"><![CDATA[n\in \mathbb {N}]]></fr:tex> such that <fr:tex
display="inline"><![CDATA[\cdot \vdash N\equiv \bar {n}:\mathsf {nat}]]></fr:tex> where <fr:tex
display="inline"><![CDATA[\bar {n}]]></fr:tex> is the encoding of the number <fr:tex
display="inline"><![CDATA[n]]></fr:tex> as a term in the type theory.</fr:p></fr:mainmatter></fr:tree><fr:tree
show-metadata="false"><fr:frontmatter><fr:authors /><fr:date><fr:year>2023</fr:year><fr:month>1</fr:month><fr:day>19</fr:day></fr:date><fr:anchor>7376</fr:anchor><fr:addr
show-metadata="false"><fr:frontmatter><fr:authors /><fr:date><fr:year>2023</fr:year><fr:month>1</fr:month><fr:day>19</fr:day></fr:date><fr:anchor>7348</fr:anchor><fr:addr
type="user">jms-000T</fr:addr><fr:route>jms-000T.xml</fr:route><fr:title
text="Decidability of cubical type theory">Decidability of cubical type theory</fr:title><fr:taxon>Conjecture</fr:taxon></fr:frontmatter><fr:mainmatter><fr:p>The assertions <fr:tex
display="inline"><![CDATA[\Gamma \vdash {A}\ \textit {type}]]></fr:tex>, <fr:tex
Expand Down
14 changes: 7 additions & 7 deletions act-2022.xml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,20 +2,20 @@
<?xml-stylesheet type="text/xsl" href="default.xsl"?>
<fr:tree
xmlns:fr="http://www.jonmsterling.com/jms-005P.xml"
root="false"><fr:frontmatter><fr:authors /><fr:date><fr:year>2022</fr:year><fr:month>7</fr:month></fr:date><fr:anchor>19627</fr:anchor><fr:addr
root="false"><fr:frontmatter><fr:authors /><fr:date><fr:year>2022</fr:year><fr:month>7</fr:month></fr:date><fr:anchor>19628</fr:anchor><fr:addr
type="user">act-2022</fr:addr><fr:route>act-2022.xml</fr:route><fr:title
text="ACT ’22: International Conference on Applied Category Theory"><fr:em>ACT ’22</fr:em>: International Conference on Applied Category Theory</fr:title><fr:taxon>Conference</fr:taxon><fr:meta
name="external">https://msp.cis.strath.ac.uk/act2022/</fr:meta></fr:frontmatter><fr:mainmatter><fr:p><fr:link
href="https://www.appliedcategorytheory.org/"
type="external">Applied category theory</fr:link> is a topic of interest for a growing community of researchers, interested in studying many different kinds of systems using category-theoretic tools. These systems are found across computer science, mathematics, and physics, as well as in social science, linguistics, cognition, and neuroscience. The background and experience of our members is as varied as the systems being studied. The goal of Applied Category Theory is to bring researchers in the field together, disseminate the latest results, and facilitate further development of the field.</fr:p></fr:mainmatter><fr:backmatter><fr:tree
show-metadata="false"
hidden-when-empty="true"><fr:frontmatter><fr:anchor>19621</fr:anchor><fr:title
hidden-when-empty="true"><fr:frontmatter><fr:anchor>19622</fr:anchor><fr:title
text="References">References</fr:title></fr:frontmatter><fr:mainmatter /></fr:tree><fr:tree
show-metadata="false"
hidden-when-empty="true"><fr:frontmatter><fr:anchor>19622</fr:anchor><fr:title
hidden-when-empty="true"><fr:frontmatter><fr:anchor>19623</fr:anchor><fr:title
text="Context">Context</fr:title></fr:frontmatter><fr:mainmatter /></fr:tree><fr:tree
show-metadata="false"
hidden-when-empty="true"><fr:frontmatter><fr:anchor>19624</fr:anchor><fr:title
hidden-when-empty="true"><fr:frontmatter><fr:anchor>19625</fr:anchor><fr:title
text="Backlinks">Backlinks</fr:title></fr:frontmatter><fr:mainmatter><fr:tree
show-metadata="true"
expanded="false"
Expand All @@ -24,7 +24,7 @@ numbered="false"><fr:frontmatter><fr:authors><fr:author><fr:link
href="jonmsterling.xml"
title="Jon Sterling"
addr="jonmsterling"
type="local">Jon Sterling</fr:link></fr:author></fr:authors><fr:date><fr:year>2023</fr:year><fr:month>10</fr:month><fr:day>12</fr:day></fr:date><fr:anchor>19623</fr:anchor><fr:addr
type="local">Jon Sterling</fr:link></fr:author></fr:authors><fr:date><fr:year>2023</fr:year><fr:month>10</fr:month><fr:day>12</fr:day></fr:date><fr:anchor>19624</fr:anchor><fr:addr
type="user">jms-00AF</fr:addr><fr:route>jms-00AF.xml</fr:route><fr:title
text="Conference program committees">Conference program committees</fr:title></fr:frontmatter><fr:mainmatter><fr:ol><fr:li><fr:link
href="oopsla-2024-25.xml"
Expand All @@ -47,8 +47,8 @@ title="ACT ’22: International Conference on Applied Category Theory"
addr="act-2022"
type="local"><fr:em>ACT ’22</fr:em>: International Conference on Applied Category Theory</fr:link></fr:li></fr:ol></fr:mainmatter></fr:tree></fr:mainmatter></fr:tree><fr:tree
show-metadata="false"
hidden-when-empty="true"><fr:frontmatter><fr:anchor>19625</fr:anchor><fr:title
hidden-when-empty="true"><fr:frontmatter><fr:anchor>19626</fr:anchor><fr:title
text="Related">Related</fr:title></fr:frontmatter><fr:mainmatter /></fr:tree><fr:tree
show-metadata="false"
hidden-when-empty="true"><fr:frontmatter><fr:anchor>19626</fr:anchor><fr:title
hidden-when-empty="true"><fr:frontmatter><fr:anchor>19627</fr:anchor><fr:title
text="Contributions">Contributions</fr:title></fr:frontmatter><fr:mainmatter /></fr:tree></fr:backmatter></fr:tree>
Loading

0 comments on commit d204ba4

Please sign in to comment.