Merge remote-tracking branch 'upstream/master' into update-blueprint

GroupoidModel/TypeTheory.lean

@@ -8,15 +8,15 @@ mutual
 inductive TyExpr where
   | univ
   | el (A : Expr)
-  | pi (ty A : TyExpr)
+  | pi (A B : TyExpr)
   deriving Repr
 
 inductive Expr where
   /-- A de Bruijn index. -/
   | bvar (n : Nat)
   | app (f a : Expr)
   | lam (ty : TyExpr) (val : Expr)
-  | pi (ty A : Expr)
+  | pi (A B : Expr)
   deriving Repr
 end
 
@@ -130,6 +130,12 @@ variable {Ctx : Type u} [SmallCategory Ctx] [HasTerminal Ctx] [M : NaturalModel
 
 def wU : y(Γ) ⟶ M.Ty := yoneda.map (terminal.from Γ) ≫ U
 
+@[simp]
+theorem comp_wU (Δ Γ : Ctx) (f : y(Δ) ⟶ y(Γ)) : f ≫ wU = wU := by
+  aesop (add norm wU)
+
+/-- `CtxStack Γ` witnesses that the semantic context `Γ`
+is built by successive context extension operations. -/
 inductive CtxStack : Ctx → Type u where
   | nil : CtxStack (⊤_ Ctx)
   | cons {Γ} (A : y(Γ) ⟶ Ty) : CtxStack Γ → CtxStack (M.ext Γ A)
@@ -352,7 +358,7 @@ theorem ofTerm_correct_tp {Γ A} (H : HasType Γ e A) {Γ'} (hΓ : Γ' ∈ ofCtx
 theorem ofType_correct {Γ A} (H : IsType Γ A) {Γ'} (hΓ : Γ' ∈ ofCtx (Ctx := Ctx) Γ) :
     (ofType Γ' A).Dom := ofTerm_ofType_correct.2 H hΓ
 
-def foo : Type → Type := fun x : Type => x
+section Examples
 
 def Typed (Γ A) := { e // HasType Γ e A }
 
@@ -371,3 +377,5 @@ theorem toModel_type {A} (e : Typed [] A) : toModel e ≫ tp = toModelType (Ctx
   ofTerm_correct_tp (Ctx := Ctx) e.2 ⟨trivial, rfl⟩
 
 example : y(⊤_ _) ⟶ M.Tm := toModel foo._hott
+
+end Examples

blueprint/src/groupoid_model.tex

@@ -17,7 +17,8 @@ \subsection{Classifying display maps}
   We denote the category of small categories as $\cat$ and the large categories as $\Cat$.
   We denote the category of small groupoids as $\grpd$. %% and the large groupoids as $\GRPD$.
 
-  We are primarily working in the category of large presheaves indexed by small groupoids,
+  We are primarily working in the category of large presheaves indexed by
+  the (large, locally small) category of small groupoids,
   which we will denote by
   \[ \Pshgrpd = [\grpd^{\op}, \Set]\]
 
@@ -1599,3 +1600,69 @@ \subsection{Identity types}
   \end{align*}
 \end{proof}
 
+\subsection{Universe of Discrete Groupoids}
+In this section we assume \textit{three} different universe sizes,
+which we will distinguish by all lowercase (small), capitalized first letter (large),
+and all-caps (extra large), respectively.
+For example, the three categories of sets will be nested as follows
+\[ \set \hookrightarrow \Set \hookrightarrow \SET \]
+We shift all of our previous work up by one universe level,
+so that we are working in the category $\PSH{\Grpd}$ of extra large
+presheaves, indexed by the
+(extra large, locally large)
+category of large groupoids.
+We would then have $\Type = [-, \Grpd]$ and $\Term = [-, \ptGrpd]$.
+
+\medskip
+
+\begin{defn}[Universe of discrete groupoids]
+  Let $\U$ be the (large) groupoid of small sets,
+  i.e. let $\U$ have $\set$ as its objects
+  and morphisms between two small sets as all the bijections between them.
+  This gives us $\ulcorner \U \urcorner : \terminal \to \Type$.
+
+  Then we define $\El : \yo \U \to \Type$ by defining $\El : \U \to \Grpd$
+  as the inclusion - any small set can be regarded as a large discrete groupoid.
+  % https://q.uiver.app/#q=WzAsMyxbMCwwLCJcXFUiXSxbMSwwLCJcXGdycGQiXSxbMSwxLCJcXEdycGQiXSxbMCwxLCIiLDAseyJzdHlsZSI6eyJ0YWlsIjp7Im5hbWUiOiJob29rIiwic2lkZSI6InRvcCJ9fX1dLFsxLDIsIiIsMCx7InN0eWxlIjp7InRhaWwiOnsibmFtZSI6Imhvb2siLCJzaWRlIjoidG9wIn19fV0sWzAsMiwiXFxFbCIsMix7InN0eWxlIjp7InRhaWwiOnsibmFtZSI6Imhvb2siLCJzaWRlIjoidG9wIn19fV1d
+  \[\begin{tikzcd}
+    \U & \grpd \\
+    & \Grpd
+    \arrow[hook, from=1-1, to=1-2]
+    \arrow["\El"', hook, from=1-1, to=2-2]
+    \arrow[hook, from=1-2, to=2-2]
+  \end{tikzcd}\]
+
+  Then we take $\pi := \disp{\El}$, giving us
+% https://q.uiver.app/#q=WzAsNCxbMCwxLCJcXFUiXSxbMSwxLCJcXFR5cGUiXSxbMSwwLCJcXFRlcm0iXSxbMCwwLCJcXEUiXSxbMCwxLCJcXEVsIiwyXSxbMiwxLCJcXHRwIl0sWzMsMCwiXFxwaSIsMl0sWzMsMl0sWzMsMSwiIiwxLHsic3R5bGUiOnsibmFtZSI6ImNvcm5lciJ9fV1d
+\[\begin{tikzcd}
+	\E & \Term \\
+	\U & \Type
+	\arrow[from=1-1, to=1-2]
+	\arrow["\pi"', from=1-1, to=2-1]
+	\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2]
+	\arrow["\tp", from=1-2, to=2-2]
+	\arrow["\El"', from=2-1, to=2-2]
+\end{tikzcd}\]
+
+  We can compute the groupoid $E$ as that with
+  objects that are pairs $(X,x)$ where $x \in X \in \set$,
+  and morphisms
+  \[ E((X,x), (Y,y)) = \{f : X \to Y \st f \, x = y \}\]
+  Then $\pi : E \to U$ is the forgetful functor $(X,x) \mapsto X$.
+\end{defn}
+
+\medskip
+
+Showing that this universe is closed under $\Pi, \Si, \Id$ formation
+depends on how we formalize $\set \hookrightarrow \Set$.
+In both cases we need to check that discreteness is preserved by
+the type formers, which is straightforward.
+If we are working with sets and cardinality,
+i.e. taking $\set = \Set_{<\la} \subset \Set_{< \kappa} = \Set$
+for some inaccessible cardinals $\la < \kappa$,
+then it is straightforward to check that the type formers
+do not make ``larger'' types.
+If we are working with type theoretic universes with a lift
+operation $\mathsf{ULift} : \set \to \Set$ then
+it may \textit{not} be true that $\mathsf{ULift}$ commutes with
+our type formers.

blueprint/src/macros/common.tex

@@ -49,28 +49,31 @@
 \newcommand{\tcat}{\mathbf}
 \newcommand{\id}{\mathsf{id}}
 \newcommand{\psh}[1]{\mathbf{Psh}(#1)} %% consider renaming to \Psh
+\newcommand{\PSH}[1]{\mathbf{PSH}(#1)}
 \newcommand{\yo}{\mathsf{y}}
 \newcommand{\pshC}{\psh{\catC}}
 \newcommand{\Arr}{\mathsf{Arr}}
+\newcommand{\CartArr}{\mathsf{CartArr}}
 \newcommand{\unit}{\, \mathsf{unit} \, }
 \newcommand{\counit}{\, \mathsf{counit} \, }
 \newcommand{\terminal}{\bullet}
 \newcommand{\Two}{\bullet+\bullet}
 
 \newcommand{\set}{\tcat{set}}
 \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{\Grpd}{\tcat{Grpd}}
 \newcommand{\ptgrpd}{\tcat{grpd}_\bullet}
-% \newcommand{\ptGrpd}{\tcat{Grpd}_\bullet}
+\newcommand{\ptGrpd}{\tcat{Grpd}_\bullet}
 \newcommand{\Pshgrpd}{\mathbf{Psh}(\grpd)}
 \newcommand{\PshCat}{\mathbf{Psh}(\Cat)}
 
-\newcommand{\Poly}[1]{\mathsf{Poly}_{#1}}
+\newcommand{\Poly}[1]{P_{#1}}
 \newcommand{\Star}[1]{{#1}^{\star}}
 
 \newcommand{\Type}{\mathsf{Ty}}
@@ -85,6 +88,7 @@
 \newcommand{\pair}{\mathsf{pair}}
 \newcommand{\Id}{\mathsf{Id}}
 \newcommand{\refl}{\mathsf{refl}}
+\newcommand{\J}{\mathsf{J}}
 \newcommand{\fst}{\mathsf{fst}}
 \newcommand{\snd}{\mathsf{snd}}
 \newcommand{\ev}[2]{\mathsf{ev}_{#1} \, #2}