\documentclass[../Main.tex]{subfiles}
\begin{document}

% TODO add references
% TODO assume that we have seen lambda calculus
\section{Dependent Type Theory}
To talk about Cubical Type Theory we must first talk about what dependent type theory is.
We will first talk about syntax and in the next section about the formal semantics. Of course
we will discuss what we want the syntax to mean in this section, but the technical encodings of
those are for the next section.

What do we mean when we say \emph{dependent} type theory? We want

%TODO good example what dependent types are
% 1.) Numbers from 1 to x (with x : N)
% 2.) lists of length x
% 3.) Lukas fragen
%

We will go forward having different kind of judgements
\begin{itemize}
	\item \(Γ ctx\), for \(Γ\) is a well-formed context
	\item \(Γ ⊢ A type \) , for A is a well-formed type in context \(Γ\)
	\item \(Γ ⊢ t : A \), for \( t \) is a well-formed term of type \(A\) in context \(Γ\)
\end{itemize}

We also assume a countable set of variable \(V\) and a bijection \(f \colon ℕ → V\). We write
\(v_n \coloneqq f(n)\). For better readability we will take the freedom to use \(x,y,z,\dots\)
for variables.

\subsubsection{Contexts}
As in some non-dependent typed logic (like the typed lambda calculus),
we need contexts to track what type free variables have. But here types might depend on the previous
declared variables. We define a context inductively. So first the empty context is a context.

\begin{itemize}
\item \begin{prooftree}
	\infer0{\diamond ctx}
\end{prooftree}
\end{itemize}
And we can extend already valid contexts, by types in that context.
\begin{itemize}
	\item \begin{prooftree}
		\hypo{Γ ctx}
		\hypo{Γ ⊢ A type}
		\infer2{Γ,x : A ctx}
	\end{prooftree}
\end{itemize}

\subsubsection{Types}
Here we will no go through the types that we will use in our typetheory, except for equality types.
That will be handled later in the section about Cubical Type Theory. Let us begin with (dependent) function types.
These work almost the same as in the normal lambda calculus, the only difference is that we allow the output type
to depend on the value of the input.

\begin{itemize}
	\item \begin{prooftree}

	\end{prooftree}
\end{itemize}

\end{document}
