search

AlgebraicJulia / Catlab.jl

A framework for applied category theory in the Julia language
https://www.algebraicjulia.org
MIT License
604 stars 56 forks source link

LaTeX pretty-printing of GATs #243

Open epatters opened 3 years ago

epatters commented 3 years ago

Pretty-print GATs as LaTeX in both of the following styles:

  1. Cartmell-style linear notation

    image

  2. natural-deduction-style tree notation

    image

The examples above depict the theory of monoids and are taken from Sterling's paper Algebraic type theory and universe hierarchies.

The first style is similar to the syntax of our @theory macro and should be easily ported to MathJax/KaTeX, while the second style is harder to typeset but beloved by type theorists.

jpfairbanks commented 3 years ago

Oh yeah that Cartmell style should be easy from our @theory syntax. It is beautiful that we are able to use Julia metaprogramming to create embed this DSL into Julia. The type theorist notation is definitely harder to typeset especially with those colored boxes which make for nice figures in papers.