Merge branch 'sinhp:master' into master

GroupoidModel/Outline.md

@@ -42,7 +42,7 @@ We will need at least the following:
   -/
 
   /-
-# 3. HoTT 0
+# 3. HoTT_0
 No idea how to do this in practice!
 But it would be nice if the user could:
 - interact with types, terms, and type families, rather than
@@ -56,7 +56,7 @@ But it would be nice if the user could:
 
 /-
 # Targets
-Here are some things that should be doable in HoTT 0:
+Here are some things that should be doable in HoTT_0:
 - HoTT Book real numbers and cumulative hierarchy,
 - univalent set theory,
 - structure identity principle for general algebraic structures,

blueprint/print/.gitignore

@@ -0,0 +1,9 @@
+*.synctex.gz
+*.out
+*.log
+*.fdb_latexmk
+*.blg
+*.bbl
+*.fls
+*.aux
+*.auctex-auto

blueprint/src/.gitignore

@@ -0,0 +1,9 @@
+*.synctex.gz
+*.out
+*.log
+*.fdb_latexmk
+*.blg
+*.bbl
+*.fls
+*.aux
+*.auctex-auto

blueprint/src/macros/common.tex

@@ -9,10 +9,99 @@
 % (this is what the [theorem] arguments mean) and never resets it.
 % If you want for instance to number them within chapters then you can add
 % [chapter] at the end of the next line.
-\newtheorem{theorem}{Theorem}
-\newtheorem{proposition}[theorem]{Proposition}
+
+%%%%%%% THEOREMS %%%%%%%%%
+\newtheorem{theorem}{Theorem}[section]
+\newtheorem*{theorem*}{Theorem}
+\newtheorem{prop}[theorem]{Proposition}
+\newtheorem{obs}[theorem]{Observation}
 \newtheorem{lemma}[theorem]{Lemma}
-\newtheorem{corollary}[theorem]{Corollary}
+\newtheorem{cor}[theorem]{Corollary}
+\newtheorem{applemma}{Lemma}[section]
 
 \theoremstyle{definition}
-\newtheorem{definition}[theorem]{Definition}
+\newtheorem{defn}[theorem]{Definition}
+
+\theoremstyle{remark}
+\newtheorem{rmk}[theorem]{Remark}
+\newtheorem*{eg}{Example}
+\newtheorem{ex}{Exercise}
+\newtheorem*{remark*}{Remark}
+\newtheorem*{remarks*}{Remarks}
+\newtheorem*{notation*}{Notation}
+\newtheorem*{convention*}{Convention}
+
+\newenvironment{comment}{\begin{quote} \em Comment. }{\end{quote}}
+
+%%%%%%% SYMBOLS %%%%%%%%%
+
+\newcommand{\defeq}{=_{\mathrm{def}}}
+\newcommand{\iso}{\cong}
+\newcommand{\equi}{\simeq}
+\newcommand{\retequi}{\unlhd}
+\newcommand{\op}{\mathrm{op}}
+\newcommand{\Id}{\mathrm{Id}}
+\newcommand{\Nat}{\mathbb{N}}
+\newcommand{\co}{\colon}
+\newcommand{\st}{\,|\,}
+
+% \newcommand{\cat}{\mathbb}
+\newcommand{\catC}{\mathbb{C}}
+\newcommand{\tcat}{\mathbf}
+\newcommand{\id}{\mathsf{id}}
+\newcommand{\psh}[1]{\mathbf{Psh}(#1)} %% consider renaming to \Psh
+\newcommand{\yo}{\mathsf{y}}
+\newcommand{\pshC}{\psh{\catC}}
+\newcommand{\Type}{\mathsf{Ty}}
+\newcommand{\Term}{\mathsf{Tm}}
+\newcommand{\tp}{\mathsf{tp}}
+\newcommand{\disp}[1]{\mathsf{disp}_{#1}}
+\newcommand{\var}{\mathsf{var}}
+\newcommand{\Prop}{\mathsf{Prop}}
+\newcommand{\U}{\mathsf{U}}
+\newcommand{\E}{\mathsf{E}}
+\newcommand{\El}{\mathsf{El}}
+\newcommand{\Poly}[1]{\mathsf{Poly}_{#1}}
+\newcommand{\pair}{\mathsf{pair}}
+\newcommand{\fst}{\mathsf{fst}}
+\newcommand{\ev}[2]{\mathsf{ev}_{#1} \, #2}
+\newcommand{\counit}{\mathsf{counit}}
+
+\newcommand{\Fib}{\mathsf{Fib}}
+\newcommand{\lift}[2]{\mathsf{lift} \, #1 \, #2}
+\newcommand{\fiber}{\mathsf{fiber}}
+\newcommand{\terminal}{\bullet}
+\newcommand{\Two}{\bullet+\bullet}
+\newcommand{\Interval}{\mathbb{I}}
+
+\newcommand{\set}{\tcat{set}}
+\newcommand{\Set}{\tcat{Set}}
+\newcommand{\cat}{\tcat{cat}}
+\newcommand{\ptcat}{\tcat{cat}_\bullet}
+\newcommand{\Cat}{\tcat{Cat}}
+\newcommand{\ptCat}{\tcat{Cat}_\bullet}
+\newcommand{\grpd}{\tcat{grpd}}
+% \newcommand{\Grpd}{\tcat{Grpd}}
+\newcommand{\ptgrpd}{\tcat{grpd}_\bullet}
+% \newcommand{\ptGrpd}{\tcat{Grpd}_\bullet}
+\newcommand{\Pshgrpd}{\mathbf{Psh}(\grpd)}
+\newcommand{\PshCat}{\mathbf{Psh}(\Cat)}
+
+% % Greek
+\newcommand{\al}{\alpha}
+\newcommand{\be}{\beta}
+\newcommand{\ga}{\gamma}
+\newcommand{\de}{\delta}
+\newcommand{\ep}{\varepsilon}
+\newcommand{\io}{\iota}
+\newcommand{\ka}{\kappa}
+\newcommand{\la}{\lambda}
+\newcommand{\om}{\omega}
+\newcommand{\si}{\sigma}
+
+\newcommand{\Ga}{\Gamma}
+\newcommand{\De}{\Delta}
+\newcommand{\Th}{\Theta}
+\newcommand{\La}{\Lambda}
+\newcommand{\Si}{\Sigma}
+\newcommand{\Om}{\Omega}