AlgebraicJulia/Catlab.jl

LaTeX pretty-printing of GATs

Open

#243 opened on Aug 24, 2020

View on GitHub
 (1 comment) (0 reactions) (1 assignee)Julia (706 stars) (68 forks)batch import
GATsenhancementgood first issue

Description

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

  1. Cartmell-style linear notation

  2. natural-deduction-style tree notation

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.

Contributor guide

Tech stack
None
Domain
documentationtooling
Issue type
feature
DifficultyEstimated implementation difficulty for a new contributor, from 1 for very small changes to 5 for expert-level work.
3
Estimated timeA rough time range for an experienced contributor to investigate, implement, test, and prepare a pull request.
1-2 days
Activity statusHow available the issue appears right now: fresh, active, stale, blocked, or waiting on maintainer input.
stale
ClarityHow clearly the issue explains the expected change, acceptance criteria, and next step.
clear
Prerequisites
Familiarity with JuliaUnderstanding of GATsKnowledge of LaTeX formatting
Newbie friendlinessA 1-100 score estimating how approachable this issue is for first-time contributors.
35
Research direction
Examine existing LaTeX output in Catlab.jl for similar constructs (e.g., theories). Study the referenced paper's notation for GATs. Implement first the Cartmell style linear notation by adapting the `@theory` macro's syntax, then tackle the natural deduction tree notation, possibly using existing tree formatting utilities. Consider leveraging MathJax/KaTeX for rendering.