diff --git a/.gitignore b/.gitignore index d80cf81..bbc7ace 100644 --- 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 deleted file mode 100644 index e69de29..0000000 diff --git a/blueprint/print/print.pdf b/blueprint/print/print.pdf deleted file mode 100644 index ad544c9..0000000 Binary files a/blueprint/print/print.pdf and /dev/null differ diff --git a/blueprint/src/chapter/all.tex b/blueprint/src/chapter/all.tex new file mode 100644 index 0000000..ce103a2 --- /dev/null +++ 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 b/blueprint/src/chapter/groupoid_model.tex similarity index 99% rename from blueprint/src/groupoid_model.tex rename to blueprint/src/chapter/groupoid_model.tex index a87885f..32eb312 100644 --- a/blueprint/src/groupoid_model.tex +++ b/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 b/blueprint/src/chapter/natural_model.tex similarity index 100% rename from blueprint/src/natural_model.tex rename to blueprint/src/chapter/natural_model.tex diff --git a/blueprint/src/polynomial.tex b/blueprint/src/chapter/polynomial.tex similarity index 99% rename from blueprint/src/polynomial.tex rename to blueprint/src/chapter/polynomial.tex index 992b752..1e99cbe 100644 --- a/blueprint/src/polynomial.tex +++ b/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 index b10e339..df9761e 100644 --- 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 deleted file mode 100644 index 1c2c3a4..0000000 --- a/blueprint/src/web.bbl +++ /dev/null @@ -1,28 +0,0 @@ -\begin{thebibliography}{Awo23} - -\bibitem[Awo17]{awodey2017naturalmodelshomotopytype} -Steve Awodey. -\newblock Natural models of homotopy type theory, 2017. - -\bibitem[Awo23]{awodey2023hofmannstreicheruniverses} -Steve Awodey. -\newblock On hofmann-streicher universes, 2023. - -\bibitem[Hof95]{streicher1995ExtensionalConceptsInIntensionalTypeTheory} -Martin Hofmann. -\newblock Extensional concepts in intensional type theory, 1995. - -\bibitem[HS98]{hofmannstreicher1996} -Martin Hofmann and Thomas Streicher. -\newblock The groupoid interpretation of type theory. -\newblock In {\em Twenty-five years of constructive type theory ({V}enice, - 1995)}, volume~36 of {\em Oxford Logic Guides}, pages 83--111. Oxford Univ. - Press, New York, 1998. - -\bibitem[Joy]{joyalnlabmodelstructuresoncat} -André Joyal. -\newblock Model structures on cat. -\newblock - \url{https://ncatlab.org/joyalscatlab/published/Model+structures+on+Cat}. - -\end{thebibliography} diff --git a/blueprint/src/web.tex b/blueprint/src/web.tex index 435a933..29167ae 100644 --- 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 new file mode 100644 index 0000000..dea36d3 --- /dev/null +++ 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 + ]; + }; + }); +}