\documentclass[../Main.tex]{subfiles}
\begin{document}
\section{Cubical Type Theory}
This section is mainly to give the reader which is not acquainted with cubical type theory
some guidance and intuition. The reader that already is well-versed in this regard might
skip this section. We still expect the reader to be familiar with some form of univalent
type theory. For a more technical complete presentation we point at \cite{ABCHFL} and \cite{cavalloUnifyingCubicalModels2020}.
We think about this in terms of categorical semantics, so we expect the reader to have
basic idea about this. For the basic ideas there is the quite old \cite{jacobsCategoricalLogicType1999}. % TODO find categorical semantics references
We also recall some translation between intuition and technical treatments of types those elements and similar things.
We also want to mention that cubical type theory isn't one type theory, but a zoo of related variances of the same idea.
Usually there is already a model in mind, and we allow our type theory to talk about some features of those.
We will briefly talk about this in this section for a more technical treatment take a look at \cite{cavalloUnifyingCubicalModels2020}
Our presentation follows \cite{ABCHFL}. We state formation rules and describe the intended interpretation and leave
out the syntactical rules that captures the behavior that the interpretation captures, as we think that would
not add to further intuition. For the Cartesian case these can be found in \cite{ABCHFL} and for the deMorgan case in \cite{CCHM}.


\subsection{types and universes}
As our type theory features a universe of small types we get a technical very nice
way of interpreting types. We will interpret our universe as a certain fibrant
map \(p_U: E → U\). We can then define a type in context \(Γ\) as a map
\(Γ → U\). From a topological intuition we  want to think about types as
fibrant small maps into \(Γ\). The way to translate between these way is by taking
a pullback.
\begin{equation*}
	\begin{tikzcd}
		{Γ.A} \arrow[r] \arrow[d] \pb & E \arrow[d,"p_U"] \\
		Γ \arrow[r,"A"] & U
	\end{tikzcd}
\end{equation*}
Of course this means that there have to exist the right amount of morphisms
from \(Γ → U\), but this is the property that makes our universe a universe.
Of course this translation can't be expected to be one to one as pullbacks
are only defined up to isomorphism. One way to deal with this to make a
choice of pullbacks (calling these display maps) and require that every small fibrant map is isomorphic
to one of those display maps. This has further problems though. For example is
substitution functorial on the nose, but if we were to go for display maps this
corresponds to building another pullback along a map between contexts. So we
would need to make our choice of display maps that these choice of pullbacks
gets functorial on the nose. On the other hand working with maps into \(U\)
has technical benefits. Substitution becomes precomposition, which
is functorial on the nose and we get smallness for free. This does
not directly reflect our topological intuition though. So when we talk about
intuition we talk about fibrant maps into the context, but on the technical side
we work with maps into the universe.

We shortly recall how terms of types are treated in this way.
A term \(a\) of type \(A\) in context \(Γ\), becomes a map
we call also \(a\) from \(Γ\) to \(E\) such that the following
triangle commutes.
\begin{equation*}
	\begin{tikzcd}
		 & E \arrow[d,"p_U"] \\
		Γ \arrow[ru,"a"] \arrow[r,"A"] & U
	\end{tikzcd}
\end{equation*}
This translates directly to the expected splits of the display map
\begin{equation*}
	\begin{tikzcd}
		Γ \arrow[rrd, bend left,"a"] \arrow[ddr, bend right,"\id"] \arrow [rd,dashed] & & \\
		  & Γ.A \arrow[r] \arrow[d] \pb & E \arrow[d,"p_U"] \\
		  & Γ \arrow[r, "A"] & U
	\end{tikzcd}
\end{equation*}

\subsection{Liftings}
As with HoTT in cubical type theory, we want a type theory that satisfies the univalence axiom. But other than
HoTT, cubical type theory is allowed to talk rather directly about liftings of trivial cofibrations along fibrations.


\subsubsection{interval, dimensions and cubes}
Cubical type theory has a rather direct way talking about paths. We allow the type theory to talk about the
underlying interval object. We will use the symbol \(\I\) here.  This might be a bit unintuitive because
these are not necessarily Kan. To not get tangled up in this problem we split our context in two. The first half only containing
variables of the interval and later half types as we are used to. Or in other words every context has the form
\(Φ;Γ\), where \(Φ\) has the form  \(i:\I,j:\I,\dots\), and \(Γ\) is allowed to depend on \(Φ\). We often
think of the elements of \(Φ\) as dimensions.
As in cubical type theory the interval object is usually representable and the underlying category is closed under products the
interpretation of \(Φ\) is some higher dimensional representable cube. To see that this makes sense we can think about the case
where \(Γ\) is empty and we have a closed type \(\cdot ⊢ A\). Then a term
\(Φ ⊢ a:A\) corresponds to a section of the display map
\begin{equation*}
	\begin{tikzcd}
		Φ.A \arrow[d] \arrow[r] \pb & A \arrow[d] \arrow[r] \pb & E \arrow[d,"p_U"]\\
		Φ \arrow[r] \arrow[u,dashed,"a", bend left] & * \arrow[r,"A"] & U
	\end{tikzcd}
\end{equation*}
and thus also to a map \(Φ → A\). As \(Φ\) is some representable cube it is isomorphic to some \(\Yo c\)
and so this map corresponds by yoneda to an element of \(A(c)\).
In other words we might think about the elements of \(Φ\) as intervals (with start- and endpoint) in different
directions.
One might express this by including the following new kind of judgment. 
\[
Φ ⊢ r:\I \face
\]
and the following rules
\[
\begin{prooftree}
	\infer0{Φ ⊢ 0 : \I \face}
\end{prooftree}
\quad \quad
\begin{prooftree}
	\infer0{Φ ⊢ 1 : \I \face}
\end{prooftree}
\quad \quad
\begin{prooftree}
	\infer0[$r ∈ Φ$]{Φ ⊢ r : \I \face}
\end{prooftree}
\]

\subsubsection{cofibrations}
Models of cubical type theory are usually cofibrantly generated, and these generating maps have representable
codomain. This is done by restricting our first context half by some form of dimension formulas. So our context gets
a third part \(Φ;ϕ;Γ\). The exact details depend on the model in question. Following the presentation in
in \cite{ABCHFL} we introduce an additional kind of judgments, of the form
\begin{equation*}
	Φ ⊢ α \cofib \quad \textrm{and} \quad Φ ⊢ ϕ \formula
\end{equation*}
Our \(ϕ\) will consist of a list of such \(α\), and we think of this as one formula by conjunction of this list.
This is expressed by the following rules
%
%TODO alignment
\begin{equation*}
	\begin{prooftree}
		\hypo{\vphantom{Φ ϕ \formula}}
		\infer1{Φ ⊢ \cdot \formula \vphantom{ϕ,}}
	\end{prooftree}
	\quad \quad
	\begin{prooftree}
		\hypo{Φ ⊢ ϕ \formula}
		\hypo{Φ ⊢ α \cofib}
		\infer2{Φ ­⊢ ϕ,α \formula}
	\end{prooftree}
\end{equation*} %
%
But about what kind of subobjects do we want to talk? The first that comes to mind are faces, which
get syntactically represented by the following rule.
\begin{equation*}
	\begin{prooftree}
		\hypo{Φ ⊢ r:\I \face}
		\hypo{Φ ⊢ r':\I \face}
		\infer2{Φ ⊢ r = r' \cofib}
	\end{prooftree}
\end{equation*}
Our interpretation will naturally get to be objects in \(\mathbf{Sub}(Φ)\).
For example \(Φ ⊢ r = 1\), means that \(r ∈ Φ\) and we can write \(Φ\) as \(Ψ,r:\I\) and the judgment gets
interpreted as the face inclusion \(⟨\id,1/r⟩:Ψ → Φ\). If we have \(Φ  ⊢ r = r'\), we can write \(Φ\) as
\(Ψ,r':\I,r:\I\) and our interpretation becomes the diagonal \(⟨\id,r'/r⟩\). \(Φ⊢ r = r\)
as the identity and \(Φ⊢0=1\) as the inclusion of the empty subobject. Cubical variants disagree which
face inclusions should be allowed. The \cite{CCHM} model does not include the diagonal case, while in
the Cartesian model \cite{ABCHFL} the inclusion of these are important to get fillings from compositions.

We are also allowed to glue these together. For example we might want the right and the top face of a square.
We can do this using the \(∨\) operation.
\begin{equation*}
	\begin{prooftree}
		\hypo{Φ⊢α \cofib}
		\hypo{Φ⊢β \cofib}
		\infer2{Φ⊢ α∨β \cofib}
	\end{prooftree}
\end{equation*}
We will interpret as the coproduct in \(\mathbf{Sub}(Φ)\), or spelled out as the pushout of a their pullback.
The geometrical intuition might be we glue the two subobjects together,
along their intersection. Or as a diagram
\begin{equation}
	\begin{tikzcd}
		P \arrow[r] \arrow[d] \pb \pu & A \arrow[d] \arrow[rdd,"α", hook , bend left] & \\
		B \arrow[rrd, "β", hook, bend right ] \arrow[r] & A∨B \arrow[rd, "α∨β", dashed, hook] & \\
		& & Φ
	\end{tikzcd}
\end{equation}
where the outer square is a pullback and the inner square is a pushout.

We also have a third operation, that will take an important role in the development of
getting a constructive model for univalence. Namely \(∀\), like the name suggest
it will get interpreted as the right adjoint of the pullback functor between
subobject categories. We add the following rule
\begin{equation}
	\begin{prooftree}
		\hypo{Φ,i:\I ⊢ α \cofib }
		\infer1{Φ⊢∀i:\I.α \cofib}
	\end{prooftree}
\end{equation}
Geometrically this might be envisioned by only keeping faces that are defined across the
entirety of that dimension, and then projecting the dimension away.


\subsubsection{path types}
As one might expect usual topology cubical type theory treats path types like
maps from interval. They are also used to model identity types. But as they
are maps from the interval we can actually evaluate them.
\begin{equation*}
	\begin{prooftree}
		\hypo{Φ;ϕ;Γ ⊢ A}
		\hypo{Φ;ϕ;Γ ⊢ t : A}
		\hypo{Φ;ϕ;Γ ⊢ u : A}
		\infer3{Φ;ϕ;Γ ⊢ \Path{A}{t}{u}}
	\end{prooftree}
\end{equation*}
Which you can think of as the paths from \(t\) to \(u\) in \(A\), or as the
ways \(t\) and \(u\) are identifiable. As we want to think about paths as maps
from the interval, get rules similar to that of function types.
\begin{equation*}
	\begin{prooftree}
	\hypo{Φ;ϕ;Γ ⊢A}
	\hypo{Φ,i:\I;ϕ;Γ ⊢t:A}
	\infer2{Φ;ϕ;Γ ⊢⟨i⟩ t : \Path{A}{t(i/0)}{t(i/1)}}
	\end{prooftree}
\end{equation*}
Of course we can also evaluate them
\begin{equation*}
	\begin{prooftree}
		\hypo{Φ;ϕ;Γ ⊢p : \Path{A}{t}{u}}
		\hypo{Φ ⊢ r : \I}
		\infer2{Φ;ϕ;Γ ⊢ p\,r:A}
	\end{prooftree}
\end{equation*}
with the usual (\(η\)) and (\(β\)) rules as well as \(p\,0 \equiv t\) and \(p\,1 \equiv u\).

\subsubsection{terms of intervals}
In general there are more terms of the interval as we allowed in the construction of \(ϕ\) above.
Which are allowed is usually closely tied to the site of the underlying model. For example in the
\cite{CCHM} model the underlying cite is the Lawvere theory of deMorgan algebras, and the terms
of the interval in that are also the terms of a deMorgan algebra. We want to shortly study them
and give some names and intuition to them. We will mostly talk about the \cite{CCHM} model, as the
Cartesian case has a lot less morphisms in its site.

Unraveling the definition of a Lawvere theory, we get that the site of the \cite{CCHM} consists of
a skeleton of finite sets and a morphism from \(A\) to \(B\) is a function from \(B\) to the free
deMorgan algebra generated by \(A\). As the yoneda embedding is fully faithfull this also holds
for the subcategory of representables. A term in some dimensional context \(Φ\) of type \I becomes
a map from \(Φ → \I\), and as this a map from \(\I^n → \I\). These correspond to a term of a deMorgan
algebra with \(n\) variables. We will write for this judgments of the form
\begin{equation*}
	Φ ⊢ t : \I
\end{equation*}
We can think of a type in a context with \(n\) dimension variables as an \(n\)-cube
of types. And a term as an \(n\)-cube in the total space of the type, going across the fibers.
Depending on the map in the site, or equivalently map between the representables, we get terms
of cubes that we can plug into our types.

For example if we have a line of types, we can look
at it as a degenerate square of types. These can be done in multiple ways. The obvious one is
through weakening. Or syntactically going from \(r:\I;; ⊢ A\) to \(r:\I,r':\I;; ⊢ A\). Which gives
us a square of types that is constant in the direction of \(r'\). In usual topology there are more
ways to get degenerate a square from a line, for example we might want that the right and the
top face are given line and the left and bottom face is constant. These kind of degeneracies are
usually called connections and exist in some models. In the \cite{CCHM} model this specific
degeneracy corresponds to the meet (\(∧\)). Or syntactically more explicit, if we have
a line of types \(r:\I⊢A\) we can get a degenerate square of types \(r:\I,r':\I⊢A(r/r∧r')\).
In point set topology we could think about this as taking the infimum of \(r\) and \(r'\).
Of course there is also the dual connection, which is also present in \cite{CCHM}. There
is also a model with only one of the two connections studied in \cite{cavalloRelativeEleganceCartesian2022}
These degeneracies allow to reconstruct fillings from compositions. The Cartesian model
does not have connections, there we will use diagonal cofibrations to get fillings from
compositions.
% TODO image of connections.

In the \cite{CCHM} model we are also allowed to reverse dimensions. This corresponds
to the inversion/negation of the deMorgan algebra. These kind of maps are often called reversals.

The last map we want to mention here, are diagonals. These correspond syntactically to the diagonals
\(r:\I;; ⊢ (r,r) : \I^2\). The reason to mention them is that the \cite{BCH} model does not feature those
in the site. It gets away with this by using a different monoidal structure, so the judgment above has
an interpretation, it is just different then one might initially think.

\subsubsection{compositions and fillings}
The first thing we need to talk about a filling, is a filling problem.
\begin{equation*}
\begin{tikzcd}
	\Ob \arrow[d,hook] \arrow[r] & □;;Γ.A \arrow[d] \\
	□ \arrow[r] \arrow[ur, dashed, "\mfill"] & □;;Γ
\end{tikzcd}
\end{equation*}
A syntactic representation of the figuratively drawn problem above might be represented by
witnessing the following rule.
\todo{should I also include the judgmental equalities that say that a filling is actually a filling of that problem?}
\begin{equation*}
	\begin{prooftree}
		\hypo{z: \I ,z':\I ;;Γ ⊢ A \type }
		\hypo{z: \I ,z': \I ;z{=}0 ∨ z{=}1 ∨ z'{=}0;Γ⊢ t : A}
		\infer2{z: \I ,z': \I ;;Γ⊢ \mfill (t) : A}
	\end{prooftree}
\end{equation*}

Allowing this in its obvious generalization runs directly into problems, as that would allow
liftings against arbitrary cofibrations, and not only trivial ones. To get around this problem
we reformulate our syntactic representation. To do this we split the problem data into two
parts. The first part is the base, that is not allowed to talk about the dimension we want to
fill, but completely defined in all other dimensions, and a part that is allowed to talk about the dimension we want to fill in,
but must be attached to the base and agree with it.
\begin{equation*}
	\begin{prooftree}
		\hypo{z:\I,z':\I;;Γ &⊢ A \type}
		\infer[no rule]1{z:\I;;Γ &⊢ b: A(0/z')}
		\infer[no rule]1{z:\I &⊢ z{=}0 ∨ z{=}1 \formula}
		\infer[no rule]1{z:\I;z':\I;z{=}0 ∨ z{=}1;Γ &⊢ t : A}
		\infer[no rule]1{z:\I;z{=}0 ∨ z{=}1;Γ &⊢ t(0/z') \equiv b : A(0/z')}
		\infer1{z:\I;z':\I;;&⊢ \mfill^{z':0}(b,t) : A}
	\end{prooftree}
\end{equation*}
That these describe trivial cofibrations is justified by the fact, that our model structures are cylindrical.
Or in other words the pushout product with the inclusions of the cylinder object sends cofibrations to
trivial cofibrations. The term \(t\) is often called the tube of the lifting problem and \(b\) either the
cap or the base.
If we abstract our example away we get
\todo{get a better variable convention for dimension going}
\begin{equation*}
	\begin{prooftree}
		\hypo{Φ,z:\I;;Γ &⊢ A \type}
		\infer[no rule]1{Φ&⊢r: \I}
		\infer[no rule]1{Φ;;Γ &⊢ b: A(r/z)}
		\infer[no rule]1{Φ &⊢ ϕ \formula}
		\infer[no rule]1{Φ;z:\I;ϕ;Γ &⊢ t : A}
		\infer[no rule]1{Φ;ϕ;Γ &⊢ t(r/z) \equiv b : A(r/z)}
		\infer1{Φ;z:\I;;Γ&⊢ \mfill^{r}(b,t) : A}
	\end{prooftree}
\end{equation*}
Or written as the intended commuting diagram
\begin{equation*}
	\begin{tikzcd}
		Φ,z:\I;ϕ ∨ Φ\arrow[r,"{[b,t]}"] \arrow[d, hook, "{(ϕ,z) ∨ (r/z)}"'] & Φ,z:\I;;Γ.A \arrow[d] \\
		Φ,z:\I \arrow[r] \arrow[ur,"{\mfill(b,t)}", dashed] & Φ,z:\I;;Γ
	\end{tikzcd}
\end{equation*}
From a syntactical point of view that rule is not so great, as in the
conclusion there is an explicit free variable \(r'\), and it is not
at all clear how one would substitute a term for \(r'\) into our filling term.
The usual way of dealing with this problem is by making \(r'\) a term appearing
in the conditions of the rule.
\begin{equation*}
	\begin{prooftree}
		\hypo{Φ,z:\I;;Γ &⊢ A \type}
		\infer[no rule]1{Φ&⊢r: \I}
		\infer[no rule]1{Φ&⊢r':\I}
		\infer[no rule]1{Φ;;Γ &⊢ b: A(r/z)}
		\infer[no rule]1{Φ &⊢ ϕ \formula}
		\infer[no rule]1{Φ;z:\I;ϕ;Γ &⊢ t : A}
		\infer[no rule]1{Φ;ϕ;Γ &⊢ t(r/z) \equiv b : A(r/z)}
		\infer1{Φ;;Γ&⊢ \comp_A^{z:r→r'}(b,t) : A(r'/z)}
	\end{prooftree}
\end{equation*}
\todo{include the coherence rules here? because they are less obvious}
These are usually called compositions, and correspond to a face of the filling.
If we translate this back to the world of commutative diagrams we get\footcite[p.431]{ABCHFL}:
\begin{equation*}
	\begin{tikzcd}
		Φ;ϕ ∨ Φ;r{=}r' \arrow[d,"{ϕ ∨ r{=}r'}"'] \arrow[r] & Φ,z:\I;ϕ ∨ Φ\arrow[r,"{[t,b]}"] \arrow[d, hook, "{(ϕ,z) ∨ (r/z)}"] & Φ,z:\I;;Γ.A \arrow[d] \\
		Φ \arrow[r,"{(\id,r'/z)}"'] \arrow[rru, dashed,"{\comp_A^{z:r→r}(b,t)}"] & Φ,z:\I \arrow[r] & Φ,z:\I;;Γ
	\end{tikzcd}
\end{equation*}
Different variants allow different terms for \(r'\) and \(z\). On one extreme the
\cite{CCHM} model only allows composition from 0 to 1. Which is in the presence of
reversals and connections is not really a strong restriction. In the Cartesian model
we need to be less restrictive to.

In general it is not clear that can recover fillings from compositions. So it
is our job to make that possible. In the presence of at least one connection this
is not to difficult, and we can define
\begin{equation*}
	Φ,i:\I;;Γ⊢\mfill_A^z(b,t) ≔ \comp_{A(i/i∧j)}^{a→b}(b,t(i∧j/i)) : A
\end{equation*}\todo{make this technical correct}
\todo{agree on a way to write substitution, why is this not uniform across literature?}
\todo{make hand drawn picture for this}

This doesn't work in the Cartesian setting though, as we don't have any connections. Here
we can use the fact that we allowed diagonals in our filling problems. And define
\begin{equation*}
	Φ,z:\I;;Γ ⊢ \mfill_A^{z:r}(b,t) ≔ \comp_A^{z':r→z}(b,t) : A
\end{equation*}
where \(z'\) does not appear in \(Φ\).
\todo{make hand drawn picture for this}

\begin{equation}
	\begin{prooftree}
		\hypo{Φ ⊢ Γ \mathbf{ctx}}
		\hypo{Φ,i:\I;Γ⊢ A \mathbf{type}}
		\hypo{Φ;Γ⊢A}
		\infer3{b}
	\end{prooftree}
\end{equation}

We also allow a special kind of lambda abstraction
for these kind of variables (note that real lambda abstraction is only allowed for types).
\begin{equation}
	\begin{prooftree}
		\hypo{Φ,i:\I;Γ⊢t:A}
		\infer1{Φ;Γ⊢⟨i⟩t : A^{\I}}
	\end{prooftree}
\end{equation}



\end{document}
