paper: fix bugs in msc, get title/author/abstract in paper

Author: artagnon

Diff for: paper/msc.cls

@@ -1167,18 +1167,6 @@
 
 \def\aopfoot#1{\gdef\@aopfoot{#1}}\aopfoot{}
 
-\def\ps@myplain{\let\@mkboth\@gobbletwo%
-   \def\@evenfoot{\vbox to 2.7pt{\vspace*{-27.5pt}%
-            \hbox to \textwidth{\psplainfootfont\@cpr\hfill}}}%
-   \def\@oddfoot{\vbox to 2.7pt{\vspace*{-27.5pt}%
-            \hbox to \textwidth{\psplainfootfont\@cpr\hfill}}}%
-   \def\@evenhead{\hbox to 322.5pt{\vbox{\vspace*{6.5pt}%
-               {\psplainfont\global\copoddheadtrue{\itshape\@journaltitle} (\@jnlDoiYr),\if@issue\ \textbf{\@volno},\ pp.\else\fi\ \first@page--\last@page}\vskip2pt%\ \textbf{\@volumeno}
-               {\psplainfont\doitext\@doi}}}\vbox to 13.5pt{\includegraphics{cup_logo.eps}}}
-   \def\@oddhead{\hbox to 322.5pt{\vbox{\vspace*{6.5pt}%
-               {\psplainfont\global\copoddheadtrue{\itshape\@journaltitle} (\@jnlDoiYr),\if@issue\ \textbf{\@volno},\ pp.\else\fi\ \first@page--\last@page}\vskip2pt%\ \textbf{\@volumeno}
-               {\psplainfont\doitext\@doi}}}\vbox to 13.5pt{\includegraphics{cup_logo.eps}}}}%
-
 \let\save@clearpage\clearpage
 \let\save@outputpage\@outputpage
 
@@ -1338,8 +1326,8 @@
 %
 \def\auand{\unskip\unskip\unskip\comma\nobreakspace{}\unskip\unskip\unskip}%
 \def\aurunand{\unskip\unskip\unskip\comma}%
-\def\aulastand{\ and\nobreakspace{}\unskip\unskip\unskip}%
-\def\auandname{and\nobreakspace{}\unskip\unskip\unskip}%
+\def\aulastand{\ and}%
+\def\auandname{\ and\ }%
 
 \renewcommand{\author}[2][]{%
    \gdef\au@data{yes}%
@@ -1357,11 +1345,11 @@
       \ignorespaces\csname author0\endcsname%
    \else%
       \ifnum\authorcount=2%
-         \ignorespaces\csname author0\endcsname\if@twoauthors\else\comma\ \fi \auandname \csname author1\endcsname%
+         \ignorespaces\csname author0\endcsname \auandname \csname author1\endcsname%
       \else%
          \@whilenum\tempcount<\tempauthorcount%
          \do{%\vskip8pt
-            \csname author\the\tempcount\endcsname\comma\ %
+            \csname author\the\tempcount\endcsname\ %
             \global\advance\tempcount1}%
          \aulastand \csname author\the\tempcount\endcsname\unskip%
       \fi%
@@ -1467,7 +1455,6 @@
    %  \def\@makefnmark{\rlap{\@textsuperscript{\scriptsize\@thefnmark}}}%
    %   \long\def\@makefntext##1{##1}%
    \@maketitle%
-   \thispagestyle{myplain}%
    \endgroup
    %  \renewcommand\thefootnote{}%
    \ifx\@aopfoot\@empty%
@@ -2145,6 +2132,7 @@
                \fi
             \fi
          \fi}
+
    \fi}
 %
 \def\endenumerate{\@topsepadd\csname belowlistskip\romannumeral\the\@enumdepth\endcsname\endlist}%
@@ -2421,6 +2409,7 @@
             \fi\fi
          \leftmargin\csname leftmargin\romannumeral\the\@itemdepth\endcsname
          \def\makelabel##1{\hss\llap{##1}}}
+
    \fi}%
 %
 \def\enditemize{%
@@ -2452,6 +2441,7 @@
             \fi\fi
          \leftmargin\csname leftmargin\romannumeral\the\@itemdepth\endcsname
          \def\makelabel##1{\hss\llap{##1}}}
+
    \fi}%
 %
 \def\enddescription{\endlist}
@@ -3414,6 +3404,7 @@
    \else
       \def\draftnote{\vbox to 0pt{\vskip-12pt}}%
       \def\Qauthor#1{\marginpar{{\raggedright\footnotesize\bf #1\endgraf}}}
+
    \fi
    \let\qtoa\Qauthor
    %%%%%%%%%%%%%%%%%%%% Character count  %%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -3757,6 +3748,7 @@
    \else
       \vadjust{\vbox to 0pt{%
                \vskip-7.5pt\@@question{#1}\vskip7.5pt}}
+
    \fi}
 %
 \def\QtoAuthor#1{\@question{{\bf Author:\ #1}}}
@@ -3898,6 +3890,7 @@
 \ifpuretex
 \else
    \newcommand\emptyfloatpage{\thisfloatpagestyle{rotatepage}}
+
 \fi
 
 
@@ -3913,6 +3906,7 @@
                \else%%
                   %\hbox to\hsize{\hss\box\@tempboxa\hss}%%
                   \Set@LT@caption{#1}{#2}{\centering#3}
+
                \fi%%
                \endgraf%
                \vskip\belowcaptionskip%

Diff for: paper/paper.tex

@@ -184,14 +184,14 @@
 \begin{abstract}
   Constructions such as semi-simplicial and semi-cubical sets can be defined in the ``usual way'' as presheaves over respectively, the semi-simplex or semi-cube category, which we call \emph{fibered} definitions, but also defined like in e.g. \cite{voevodsky12} or in \cite{herbelin15}, as a dependently-typed construction, which we call \emph{indexed}.
 
-  On another side, it is known that semi-simplicial and semi-cubical sets are related to iterated Reynolds's parametricity, respectively in its unary and binary variants\dots
+  It is known that semi-simplicial and semi-cubical sets are related to iterated Reynolds's parametricity, respectively in its unary and binary variants\dots
 
   We exploit this correspondence to develop a uniform indexed definition of both augmented semi-simplicial and semi-cubical sets, which is additionally fully formalized in Coq's dependent type theory. Beside the interest in the construction itself, we expect it to eventually serve as models of type theory preserving more definitional equalities than presheaf models do.
 \end{abstract}
 \begin{keywords}
   simplicial set, cubical set, coq, formalization, HoTT
 \end{keywords}
-% \maketitle
+\maketitle
 
 \section{Introduction}
 \subsection*{Fibered vs indexed presentation of semi-simplicial and semi-cubical sets}
@@ -214,8 +214,8 @@ \subsection*{Fibered vs indexed presentation of semi-simplicial and semi-cubical
 up to cubical faces identities. In it, $X_1$ can be seen as a family over $X_0 \times X_0$ presented in a fibered form, $X_2$ can be seen as a family of $X_1 \times X_1 \times X_1 \times X_1$, and so on. This suggests an alternative indexed presentation of the same presheaf as a stratified sequence of families indexed on elements of families of lower rank, taking into account the coherence conditions to prevent duplications. Formulated in type theory, it takes the form:
 
 \begin{align*}
-  X_0 & :              & \U                                                                                           \\
-  X_1 & :              & X_0 \times X_0 \rightarrow \U                                                           \\
+  X_0 & :              & \U                                                                            \\
+  X_1 & :              & X_0 \times X_0 \rightarrow \U                                                 \\
   X_2 & : \Pi a b c d. & X_1(a)(b) \times X_1(a)(c) \times X_1 (b)(d) \times X_1 (c)(d) \rightarrow \U \\
   \ldots
 \end{align*}
@@ -465,8 +465,8 @@ \section{Type theory}
 \section{Relating to parametricity\label{sec:rel-param}}
 Let us recall from the introduction, the form taken by the indexed presentation of a semi-cubical set:
 \begin{align*}
-  X_0 & :              & \U                                                                                           \\
-  X_1 & :              & X_0 \times X_0 \rightarrow \U                                                           \\
+  X_0 & :              & \U                                                                            \\
+  X_1 & :              & X_0 \times X_0 \rightarrow \U                                                 \\
   X_2 & : \Pi a b c d. & X_1(a)(b) \times X_1(a)(c) \times X_1 (b)(d) \times X_1 (c)(d) \rightarrow \U \\
   \ldots
 \end{align*}