concept-dag.tex

\RequirePackage{luatex85}
\documentclass[margin=5mm]{standalone}
\usepackage{varwidth}
\usepackage{tikz}
\usetikzlibrary{positioning}
\usetikzlibrary{graphdrawing,graphs}
\usegdlibrary{trees}  % tree layout
\usegdlibrary{layered}% layered layout
\usegdlibrary{force}  % spring layout
\newcommand{\node}[2]{\begin{varwidth}{#1}\centering #2\end{varwidth}}
\usepackage{xcolor}
\begin{document}
\begin{tikzpicture}[rounded corners]
  % \graph[spring electrical layout, nodes=draw, node distance=2cm, electric charge=5] 
  % \graph[spring layout, nodes=draw, node distance=10cm, convergence tolerance=0.000001, cooling factor=0.2] 
  % \graph[layered layout, nodes={draw, text width=3.0cm, align=flush center}, level distance=1.3cm, node distance=3cm]
  \graph
  [layered layout,
  nodes={draw, align=flush center},
  level distance=1.3cm,
  sibling distance=3.2cm,
  nope/.style={color=white, fill=gray}
  ]
  {
    "\node{3cm}{Homotopy Type Theory}" -- {
      "\node{2cm}{Homotopy}"[nope] -- {
        "\node{2cm}{Category theory}"[color=white, fill=yellow, sibling distance=2.8cm],
        "\node{3cm}{Loop spaces}"[nope],
        "\node{3cm}{Globular sets}"[sibling distance=0.5cm, nope] -- {
          "\node{3cm}{Presheafs}"[sibling distance=0.5cm, nope]
        },
        ""[sibling distance=0cm] -- {
        ""[sibling distance=0cm] -- {
        "\node{3cm}{Fibration}"[sibling distance=0.5cm] -- {
          "\node{3cm}{Homotopy lifting property}"[nope],
          "\node{3cm}{Fiber bundle}"[nope] -- {
            "\node{3cm}{Covering space}"[color=white, fill=yellow, sibling distance=2.8cm]
          }
        },
        },
        },
        ""[sibling distance=0cm] -- {
          "\node{3cm}{Weak $\infty$-groupoid}"[nope] -- {
            "\node{3cm}{Fundamental groupoid}"[color=white, fill=yellow],
            ""[sibling distance=0cm] -- {
            ""[sibling distance=0cm] -- {
            "\node{3cm}{$\infty$-categories}"[nope] -- {
              "\node{3cm}{Whiskering}"[nope],
              "\node{3cm}{Vertical composition}"[nope],
              "\node{3cm}{Horizontal composition}"[nope],
            }
            }
            }
          },
        },
        ""[sibling distance=0cm] -- {
        ""[sibling distance=0cm] -- {
        "\node{3cm}{Quillin model categories}"[nope] --[bend right=20] {
          ""[sibling distance=0cm] -- {
            "\node{2.2cm}{Grothendieck, Serre, Kan fibrations}"[nope],
          },
          "\node{3cm}{Weak factorization systems}"[nope] -- {
            "\node{3cm}{Lifting properties}"[nope]
          },
        },
        },
        },
      },
      "\node{3cm}{Univalent Type Theory}" -- {
        "\node{2cm}{Univalence Axiom}"[color=white, fill=green] -- {
          "\node{2cm}{Weak equivalences}"[color=white, fill=green],
        },
        ""[sibling distance=0cm] -- {
          "\node{3cm}{Per Martin-L\"of's}"[color=white,fill=green] --[bend right=5] {
            ""[sibling distance=2.2cm] -- {
              "\node{3cm}{Equality}"[color=white, fill=green] -- {
                "\node{3cm}{Propositional vs syntactic}"[color=white, fill=green],
                "\node{3cm}{Extensional vs intentional}"[color=white, fill=green],
                "\node{3cm}{(Higher) equality types}"[color=white, fill=green]
              },
            },
          },
          "\node{3cm}{Per Martin-L\"of's}"[color=white,fill=green] -- {
            "\node{3cm}{Dependent sum}"[color=white, fill=green] -- {
              "\node{3cm}{Dependent function}"[color=white, fill=green],
            },
            "\node{3cm}{Classical type theory}"[color=white,fill=green] -- {
              "\node{3cm}{1\textsuperscript{st} order and predicate logic}"[color=white, fill=green],
              "\node{3cm}{System F}"[color=white, fill=green] -- {
                "\node{3cm}{(G)ADTs}"[color=white, fill=green]
              },
            },
            ""[sibling distance=0cm] -- {
            ""[sibling distance=0cm] -- {
              "\node{3cm}{(Co)inductive types}"[color=white,fill=green] -- {
                "\node{3cm}{$F$-(co)algebras}"[color=white, fill=yellow],
                "\node{3cm}{W-types}"[color=white, fill=yellow],
                "\node{3cm}{M-types}"[color=white, fill=yellow]
              }
            }
            }
          }
        },
        "\node{2cm}{Grothendieck Universes}"[color=white, fill=green],
      },
      "\node{3cm}{Univalent Type Theory}" --[bend left=10] {
        "\node{3cm}{$h$-levels}"[color=white, fill=green] -- {
          "\node{3cm}{homotopy $n$-types}"[color=white, fill=yellow]
        },
        "\node{3cm}{Higher inductive types}",
      },
      "\node{2cm}{Homotopy}"[color=white, fill=gray] --[bend left=0] "\node{2cm}{Weak equivalences}"[color=white, fill=green],
    },
  };
\end{tikzpicture}
\end{document}