\documentclass[../Main.tex]{subfiles}
\begin{document}
\section{Categorical Semantics}
We will need some basics knowledge categorical semantics for type theory. A bit old, but still good
instructive read can be found here\cite{jacobsCategoricalLogicType1999}. We will recap categories with
families as we will encounter them later more often.

\subsection{Category with Families}
A category with families\cite{dybjerInternalTypeTheory2003, castellanCategoriesFamiliesUnityped2020a, hofmannSyntaxSemanticsDependent} consists of a category of contexts and context substitutions. And an assignment
of context to (semantical) types, which then gets interpreted as the possible types in that context. And a second assignment of types in
a context to (semantical) terms of that type. These have to fulfill some rules, so that they actually behave like contexts, types and terms.
We follow Dybjer in the way we organize this data. First we define the category \(\Fam\).

\begin{definition}
	\(\Fam\) is the category which has as objects \((I,\{A\}_{i ∈ I})\), where \(I\) is a set and \(\{A_i\}_{i ∈ I}\) is
	a family of sets indexed by \(I\). A morphism of \(\Fam\), \(f \colon (I,\{A_i\}_{i ∈ I}) → (J, \{B_j\}_{j ∈ J})\)
  consists of a tuple \((f,\{f_i\}_{i ∈ I})\). Where \(f\) is a function \(I → J\) and \(f_i\) is a function
  \(A_i → B_{f(i)}\).
\end{definition}

% TODO this typesets ugly and we want to make this the definition and the definition a remark
% If we do this we need to change the technicallities in the next definition accordingly
\begin{remark}
	Alternatively this is just the category \(\mathcal{S}et^→\)
\end{remark}



% call elements of C contexts
% pi_1 is not great
\begin{definition}[Category with Families (CwF)\index{category!with families}\index{CwF}]
	A category with families, consists of a category \(\C\) with terminal obeject, and a functor \(T \colon \C^{op} → \Fam\).
	Before we continue the definition we will introduce some very helpful notation.
	Let \(Γ\) and \(Δ\) be objects of \(\C\) and \(σ \colon Δ → Γ \). We call
	\begin{itemize}
		\item \(\Ty(Γ) \coloneqq π_1 ( T (Γ))\), the types in context \(Γ\).
		\item whenever \(A ∈ \Ty(Γ)\), \(\Tm(Γ, A) \coloneqq (π_2 (T (Γ)))_A\), the terms of type \(A\) in context \(Γ\).
		\item \(A[σ] \coloneqq π_1 (T (σ))(A) ∈ \Ty(Δ)\) the substitution of \(A\) along \(σ\).
		\item whenever \(t ∈ \Tm(Γ, A)\), \(t[σ] \coloneqq (π_2 (T(σ)))_A(t) ∈ \Tm(Δ, A[σ])\) the substitution
		of \(t\) along \(σ\).
	\end{itemize}
	For a CwF we require a context comprehension operation, that assigns to every context \(Γ ∈ \C\) and type
	\(A ∈ \Ty(Γ)\), a context
	\(Γ.A ∈ \C\), a morphism \(\p^1_{Γ.A} \colon Γ.A → Γ\) and a term \(\p^2_{Γ.A} ∈ \Tm(Γ.A,A[p^1_{Γ.A}])\), such that
	for every substitution \(γ \colon Δ → Γ \) and every term \(t ∈ \Tm(Δ,A[γ])\) there exists a unique substitution
	\(⟨ γ,t ⟩ \colon Δ → Γ.A \), which fulfills the conditions
	\(\p^1_{Γ.A} ∘ ⟨γ,t⟩ = γ\) and \(\p^2_{Γ.A}[⟨γ,t⟩] = t\).
\end{definition}

\begin{remark}
	Some literature does not require the existance of a terminal object. We decided to require it, because for all
	our purposes we will need it anyway.
\end{remark}

\begin{remark}
For the initiated, in other ways of building models for dependent type theory, that are based on some form of
slice categories (i.e.: categories with attributes). The morphism \(\p^1_{Γ.A}\) and the term \(\p^2_{Γ.A}\) correspond to the
first and second projection from the
dependent product \(Γ.A\). And the condition imposed on them correspond to the corresponding universal property.
\end{remark}

% TODO how do sections and Terms relate
% TODO fix semantic bla naming conventions above

\subsubsection{Semantics}
We assume a fixed CwF in the background.

How the above naming conventions suggest we want to interpret contexts as semantic contexts, types as semantic
types and terms as semantic terms. So we define a partial interpretation function \( ⟦-⟧ \) mapping contexts
to semantic contexts, types in contex \(Γ\) to \( \Ty(⟦Γ⟧) \) and terms of type \(A\) of in contex \( Γ \) to
to \( \Tm(⟦Γ⟧,⟦A⟧) \). We will continue this section with defining that function. We will see that for various
typetheoretic construction we need to pose additional conditions on our CwF. We will develop them along the way.

First the contexts:

\begin{itemize}
	\item \( ⟦\diamond⟧ ≔ ⊤\)
	\item \(⟦Γ,x : A⟧ ≔ ⟦Γ⟧.⟦Γ⊢A⟧ \)
\end{itemize}

Now we talk about types and their terms. Before we jump into type constructors, we see how we deal with assumptions.

\begin{itemize}
  \item \( ⟦Γ,x:A⊢x:A⟧ ≔ \p^2_{⟦Γ,x:A⟧} \)
  \item \( ⟦Γ,x:A,Δ,y:B⊢x:A⟧ ≔ ⟦Γ,x:A,Δ⊢x:A⟧[\p^1_{⟦Γ,x:A,Δ,y:B⟧}] \)
\end{itemize}

Now we are ready to dive into the Semantics of various different types.
\end{document}
