0

Nice looking proof by Vene

I found this very nice looking way to display equational proofs. It is used by Vene Vermo several times in his papers and I am wondering how to recreate it. When selecting things in the pdf I found that the vertical bars are lots of separate characters, I have no other clues.

  • 2
    Welcome to TeX.SE. Please edit your posting to show us what you've tried so far and to note where you're experiencing difficulties. – Mico Oct 12 at 10:05
3

It can be obtained with two nested align(ed)at environments:

    \documentclass[french]{article}

    \usepackage[utf8]{inputenc}
    \usepackage[T1]{fontenc}
    \usepackage{empheq, stmaryrd}
\DeclareMathOperator{\id}{id}
\DeclareMathOperator{\In}{in}
\DeclareMathOperator{\fst}{fst}
\DeclareMathOperator{\snd}{snd}
\DeclarePairedDelimiter\innerp\langle\rangle
\newcommand\sfF{\mathsf{F}}

    \begin{document}

 \begin{empheq}[left = {\empheqlbrack}]{alignat* = 2}
 &{} \triangleright{} & \enspace &f \circ\In = \varphi\circ\sfF\innerp{f, \id}\\[-2ex]
 \cline{2-4}\noalign{\vskip-0.5ex}
 & & & f \\
  & = & &\quad\text{-- pairing --} \\
 & & & \fst\circ \innerp{f, \id} \\
 & = & &\quad\text{-- cata-\textsc{Charn} --} \\
& \hphantom{{}={}} & &\hskip 0.75em \left[%
 \begin{alignedat}{2}
 & & & \innerp{f, \id}\circ \In \\
 & = & \quad & \quad\text{-- pairing --} \\
 & & & \innerp{f\circ\In, \In} \\
 & = & & \quad\text{-- $\sfF$ functor --} \\
 & & & \innerp{f\circ\In, \In\circ\sfF\id} \\
 & = & & \quad\text{-- pairing --} \\
 & & & \innerp[\big]{f\circ\In, \In\circ\sfF(\snd\circ\innerp{f, \id})} \\
 & = & & \quad\text{-- $\triangleleft, \mathsf{F}$ functor --} \\
 & & & \innerp[\big]{\varphi\circ\sfF\innerp{f, \id}, \In\circ\sfF\:\snd\circ\sfF\:\innerp{f, \id}} \\
 & = & & \quad\text{-- pairing --} \\
 & & & \innerp{\varphi, \In\circ\sfF\:\snd}\circ\sfF\:\innerp{f, \id}
 \end{alignedat}\right. \\[1ex]
  & & & \fst\circ\llparenthesis\innerp{\varphi, \In\circ\sfF\snd}\rrparenthesis
    \end{empheq}

    \end{document} 

enter image description here

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.