feat: fix web blueprint (#27)

* feat: fix web blueprint * feat: link Lean declarations in blueprint * chore: remove pdf
sinhp · Nov 14, 2024 · 69744a3 · 69744a3
1 parent 8d6ab9b
commit 69744a3
Show file tree

Hide file tree

Showing 11 changed files with 48 additions and 68 deletions.
diff --git a/.gitignore b/.gitignore
@@ -4,16 +4,14 @@
 .lake/*
 .cache/*
 ## Blueprint
-/blueprint/print/print.log
-/blueprint/web/
-/blueprint/src/print.pdf
-/blueprint/src/web.paux
-/blueprint/src/web.pdf
-/blueprint/src/web.bbl
-/blueprint/print/
+blueprint/web/
+blueprint/print/
+blueprint/src/print.pdf
+blueprint/lean_decls
 ## Docs
 docs/_includes/sorries.md
 ## TeX
+*.paux
 *.aux
 *.lof
 *.log

diff --git a/blueprint/lean_decls b/blueprint/lean_decls
diff --git a/blueprint/print/print.pdf b/blueprint/print/print.pdf
diff --git a/blueprint/src/chapter/all.tex b/blueprint/src/chapter/all.tex
@@ -0,0 +1,21 @@
+% This file collects all the blueprint chapters.
+% It is not supposed to be built standalone:
+% see web.tex and print.tex instead.
+
+\title{Groupoid Model of HoTT in Lean 4}
+\author{Authors}
+
+\begin{document}
+\maketitle
+
+\section{Natural Models}
+\input{chapter/natural_model}
+\section{The Groupoid Model}
+\input{chapter/groupoid_model}
+\section{Polynomial Endofunctors}
+\input{chapter/polynomial}
+
+\bibliography{refs.bib}{}
+\bibliographystyle{alpha}
+
+\end{document}
diff --git a/blueprint/src/groupoid_model.tex → blueprint/src/chapter/groupoid_model.tex b/blueprint/src/groupoid_model.tex → blueprint/src/chapter/groupoid_model.tex
@@ -29,6 +29,7 @@ \subsection{Classifying display maps}
 \medskip
 
 \begin{defn}[Pointed]
+  \lean{CategoryTheory.PCat} \leanok
   We will take the category of pointed small categories $\ptcat$
   to have objects as pairs $(\catC \in \cat, c \in \catC)$
   and morphisms as pairs

diff --git a/blueprint/src/natural_model.tex → blueprint/src/chapter/natural_model.tex b/blueprint/src/natural_model.tex → blueprint/src/chapter/natural_model.tex
diff --git a/blueprint/src/polynomial.tex → blueprint/src/chapter/polynomial.tex b/blueprint/src/polynomial.tex → blueprint/src/chapter/polynomial.tex
@@ -5,7 +5,7 @@
 \medskip
 
 \begin{defn}[Polynomial endofunctor]
-  \label{polynomial_endofunctor}
+  \label{polynomial_endofunctor} \lean{UvPoly} \leanok
   Let $\catC$ be a locally Cartesian closed category
   (in our case, presheaves on the category of contexts).
   This means for each morphism $t : B \to A$ we have an adjoint triple
@@ -39,7 +39,7 @@
 \medskip
 
 \begin{prop}[Characterising property of Polynomial Endofunctors]
-  \label{polynomial_endofunctor_property}
+  \label{polynomial_endofunctor_property} \lean{UvPoly.equiv} \leanok
   The data of a map into the polynomial applied to an object in $\catC$
 % https://q.uiver.app/#q=WzAsMixbMCwwLCJcXEdhIl0sWzEsMCwiXFxQb2x5e3R9IFkiXSxbMCwxXV0=
 \[\begin{tikzcd}
@@ -780,4 +780,3 @@
   Then we simply unfold the computation for each of $\Poly{\kappa}$
   and $\Star{\rho}$.
 \end{proof}
-
diff --git a/blueprint/src/print.tex b/blueprint/src/print.tex
@@ -35,24 +35,4 @@
 \input{macros/common}
 \input{macros/print}
 
-\title{A Groupoidal Natural Model of HoTT in Lean 4}
-\author{Sina Hazratpour, Joseph Hua}
-
-\begin{document}
-\maketitle
-
-\section{Natural Models}
-\input{natural_model}
-
-\section{The Groupoid Model}
-\input{groupoid_model}
-
-\section{Polynomial Endofunctors}
-\input{polynomial}
-
-
-\bibliography{refs.bib}{}
-\bibliographystyle{alpha}
-
-
-\end{document}
+\input{chapter/all}
diff --git a/blueprint/src/web.bbl b/blueprint/src/web.bbl
diff --git a/blueprint/src/web.tex b/blueprint/src/web.tex
@@ -8,8 +8,7 @@
 
 \usepackage{amssymb, amsthm, amsmath}
 \usepackage{hyperref}
-\usepackage[showmore, dep_graph]{blueprint}
-
+\usepackage[showmore, dep_graph,thms=defn+prop+lemma+cor]{blueprint}
 
 \input{macros/common}
 \input{macros/web}
@@ -18,10 +17,4 @@
 \github{https://github.com/sinhp/groupoid_model_in_lean4}
 \dochome{https://sinhp.github.io/groupoid_model_in_lean4/docs}
 
-\title{Groupoid Model of HoTT in Lean 4}
-\author{Authors}
-
-\begin{document}
-\maketitle
-% \input{content}
-\end{document}
+\input{chapter/all}
diff --git a/flake.nix b/flake.nix
@@ -0,0 +1,16 @@
+{
+  outputs = { self, nixpkgs, flake-utils }:
+    flake-utils.lib.eachDefaultSystem (system: let
+      pkgs = nixpkgs.legacyPackages.${system};
+    in {
+      devShells.default = pkgs.mkShell {
+        packages = with pkgs; [ 
+          bashInteractive
+          typst
+          texlive.combined.scheme-full
+          python3
+          graphviz
+        ];
+      };
+    });
+}