nerf/thesis
1
0
Fork 0
generated from nerf/texTemplate
Code Issues Pull requests Projects Releases Packages Wiki Activity

before adjunction proof

Browse source
This commit is contained in:
Dennis Frieberg 2024-07-28 23:34:21 +02:00
parent 9bf50e4353
commit 0ef95e1735
Signed by: nerf
GPG key ID: 42DED0E2D8F04FB6
24 changed files with 3394 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
.editorconfig Normal file
View file

@ -0,0 +1,6 @@
root = true
[*]
end_of_line = lf
charset = utf-8
indent_style = tab

8
.gitignore vendored
View file

@ -45,6 +45,11 @@
# latexrun
latex.out/
.cache/
.local/
.texlive2022/
.lesshst
## Auxiliary and intermediate files from other packages:
# algorithms
*.alg
@ -303,3 +308,6 @@ TSWLatexianTemp*
# Nix buid output
/result
# language correction
.aspell.*

25
flake.lock Normal file
View file

@ -0,0 +1,25 @@
{
"nodes": {
"nixpkgs": {
"locked": {
"lastModified": 1694343207,
"narHash": "sha256-jWi7OwFxU5Owi4k2JmiL1sa/OuBCQtpaAesuj5LXC8w=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "78058d810644f5ed276804ce7ea9e82d92bee293",
"type": "github"
},
"original": {
"id": "nixpkgs",
"type": "indirect"
}
},
"root": {
"inputs": {
"nixpkgs": "nixpkgs"
}
}
},
"root": "root",
"version": 7
}

30
flake.nix
View file

@ -30,19 +30,22 @@
let
pkgs = nixpkgsFor.${system};
# LaTex package dependencies
latexdeps = {inherit (pkgs.texlive) scheme-small;};
latexdeps = {inherit (pkgs.texlive) scheme-full;};
latex = pkgs.texlive.combine latexdeps;
latexrun = pkgs.latexrun;
in {
default = pkgs.stdenvNoCC.mkDerivation {
name = "output.pdf";
buildInputs = [latex latexrun pkgs.biber];
buildInputs = [latex latexrun pkgs.biber pkgs.inkscape];
src = self;
buildPhase = ''
latexrun -o output.pdf src/Main.tex
HOME=.
cd src
latexrun --latex-cmd lualatex --bibtex-cmd biber --latex-args '\-shell-escape' -o output.pdf Main.tex
'';
installPhase = ''
mkdir -p $out
env > $out/env
cp output.pdf $out/output.pdf
'';
};
@ -57,7 +60,7 @@
kakoune =
let
texlab = pkgs.texlab;
latexTmpDir = "src/latex.out/";
latexTmpDir = "latex.out/";
myKakoune =
let
# this could also be done by generating toml with the
@ -67,20 +70,20 @@
text = ''
[language.latex]
filetypes = ["latex"]
roots = [".git"]
roots = [".git", "Main.tex"]
command = "texlab"
# args = ["-vvvv", "--log-file", "/tmp/texlabLog"]
args = ["-vvvv", "--log-file", "/tmp/texlabLog"]
settings_section = "texlab"
[language.latex.settings.texlab.build]
onSave = true
auxDirectory = "${latexTmpDir}"
executable = "latexrun"
args = ["--bibtex-cmd", "biber", "--latex-args", "'-synctex=1'","%f"]
args = ["--latex-cmd", "lualatex", "--bibtex-cmd", "biber", "--latex-args", "'-shell-escape -synctex=1'","%f"]
# args = ["--latex-cmd", "lualatex", "--bibtex-cmd", "biber", "%f"]
forwardSearchAfter = true
[language.latex.settings.texlab.forwardSearch]
executable = "zathura"
args = ["--synctex-forward", "%l:1:%f", "%p"]
[language.latex.settings.texlab]
auxDirectory = "${latexTmpDir}"
'';
};
config = pkgs.writeTextFile (rec {
@ -89,9 +92,9 @@
text = ''
colorscheme solarized-dark
set global tabstop 2
set global indentwidth 2
# eval %sh{kak-lsp --kakoune --session $kak_session -c ${kak-lsp-config} --log /tmp/kak-lspLog -vvvv}
eval %sh{kak-lsp --kakoune --session $kak_session -c ${kak-lsp-config}}
set global indentwidth 0
eval %sh{kak-lsp --kakoune --session $kak_session -c ${kak-lsp-config} --log /tmp/kak-lspLog -vvvv}
# eval %sh{kak-lsp --kakoune --session $kak_session -c ${kak-lsp-config}}
hook global WinSetOption filetype=(latex) %{
lsp-auto-hover-enable
lsp-enable-window
@ -111,7 +114,10 @@
# TODO only try to start the kakoune session if no session with that
# name exists
shellHook = ''
HOME=.
# unset LANG # This is a very stupid idea but lualatex GRMBLFX!!! # argh this brakes kakoune unicode!!!
alias ..="cd .."
cd src
mkdir -p ${latexTmpDir}
export KAKOUNE_CONFIG_DIR="/dev/null/"
kak -d -s ${name} &

1
src/.bash_history Normal file
View file

@ -0,0 +1 @@
vim

143
src/Main.tex
View file

@ -1,4 +1,143 @@
\documentclass{scrartcl}
\documentclass[DIV=calc,draft=true]{scrartcl}
\usepackage{microtype}
\usepackage{amsthm} %theorems
\usepackage{mathtools} %coloneqq and other stuff
\usepackage{amssymb}
%\usepackage[colon=literal]{unicode-math-luatex} %unicode in mathmode does conflict amssymb maybe sometimes use this line if you want
% that : behaves like \colon
\usepackage{unicode-math-luatex}
\usepackage{imakeidx} %make index possible
% \makeindex[columns=3, title=Alphabetical Index]
\usepackage{graphicx}
\usepackage{dsfont}
\usepackage{hyperref}
\usepackage{tikz}
\usetikzlibrary{cd}
\usepackage{faktor}
\usepackage{polyglossia}
\setdefaultlanguage[variant=us]{english}
\usepackage[style=alphabetic]{biblatex}
\usepackage{ebproof}
\usepackage{xspace}
\usepackage[obeyDraft]{todonotes}
\usepackage{subfiles}
\usepackage[plain]{fancyref}
\usepackage{cleveref}
% \usepackage{mathabx}
\usepackage{pdftexcmds} % pdftex primitves for lualatex
\makeatletter % make the primitives available for svg
\let\pdfstrcmp\pdf@strcmp
\let\pdffilemoddate\pdf@filemoddate
\makeatother
\usepackage{svg}
\addbibresource{resource.bib}
\theoremstyle{definition}
\newtheorem{theorem}{Theorem}[subsection]
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{example}[theorem]{Example}
\newtheorem{proposition}[theorem]{Proposition}
\theoremstyle{remark}
\newtheorem*{remark}{Remark}
\newcommand*{\fancyrefthmlabelprefix}{thm}
\newcommand*{\fancyreflemlabelprefix}{lem}
\newcommand*{\fancyrefcorlabelprefix}{cor}
\newcommand*{\fancyrefproplabelprefix}{prop}
\newcommand*{\fancyrefexlabelprefix}{ex}
\newcommand*{\fancyrefremlabelprefix}{rem}
\newcommand*{\fancyrefdeflabelprefix}{def}
% This is a dirty hack, we should go via \fref...name commands intstead
\frefformat{plain}{\fancyrefthmlabelprefix}{theorem #1}
\Frefformat{plain}{\fancyrefthmlabelprefix}{Theorem #1}
\frefformat{plain}{\fancyreflemlabelprefix}{lemma #1}
\Frefformat{plain}{\fancyreflemlabelprefix}{Lemma #1}
\frefformat{plain}{\fancyrefcorlabelprefix}{corollary #1}
\Frefformat{plain}{\fancyrefcorlabelprefix}{Corollary #1}
\frefformat{plain}{\fancyrefproplabelprefix}{proposition #1}
\Frefformat{plain}{\fancyrefproplabelprefix}{Proposition #1}
\frefformat{plain}{\fancyrefexlabelprefix}{example #1}
\Frefformat{plain}{\fancyrefexlabelprefix}{Example #1}
\frefformat{plain}{\fancyrefremlabelprefix}{remark #1}
\Frefformat{plain}{\fancyrefremlabelprefix}{Remark #1}
\frefformat{plain}{\fancyrefdeflabelprefix}{definition #1}
\Frefformat{plain}{\fancyrefdeflabelprefix}{Definition #1}
\newenvironment{eqcd*}[1][]{\begin{equation*}\begin{tikzcd}[#1]}{\end{tikzcd}\end{equation*}\ignorespacesafterend}
\newenvironment{eqcd}[1][]{\begin{equation}\begin{tikzcd}[#1]}{\end{tikzcd}\end{equation}\ignorespacesafterend}
\DeclareMathOperator{\Ty}{Ty}
\DeclareMathOperator{\Tm}{Tm}
\DeclareMathOperator{\Obj}{Obj}
\DeclareMathOperator{\im}{im}
\DeclareMathOperator{\TFib}{TFib}
\DeclareMathOperator{\colim}{colim}
\DeclareMathOperator{\Yo}{\mathbf{y}}
\newcommand{\Fam}{\mathcal{F}\mathrm{am}}
\newcommand{\Id}{\textsf{Id}}
\newcommand{\id}{\textsf{id}}
\newcommand{\Cat}[1]{\ensuremath{\mathcal{#1}}\xspace}
\newcommand{\A}{\Cat{A}}
\newcommand{\B}{\Cat{B}}
\newcommand{\C}{\Cat{C}}
\newcommand{\D}{\Cat{D}}
\newcommand{\E}{\Cat{E}}
\newcommand{\I}{\ensuremath{\mathds{I}}\xspace}
\newcommand{\J}{\Cat{J}}
\newcommand{\T}{\ensuremath{\mathrm{T}}\xspace}
\newcommand{\Hom}{\mathrm{Hom}}
\newcommand{\type}{\, \mathsf{type}}
\newcommand{\cofib}{\, \mathsf{cofib}}
\newcommand{\formula}{\, \mathsf{formula}}
\newcommand{\face}{\, \mathsf{face}}
\newcommand{\mfill}{\mathsf{fill}}
\newcommand{\comp}{\mathsf{comp}}
\newcommand{\Path}[3]{\mathsf{Path}\,#1\,#2\,#3}
\newcommand{\p}{\textrm{p}}
\newcommand{\Set}{\ensuremath{\mathbf{Set}}\xspace}
\newcommand{\skl}{\mathrm{skl}}
\newcommand{\op}{\mathsf{op}}
\renewcommand{\d}{\mathsf{d}}
\renewcommand{\i}{\textsf{i}}
\renewcommand{\t}{\mathsf{t}}
\newcommand{\⊗}{\mathbin{\hat{⊗}}}
\newcommand{\×}{\mathbin{\hat{×}}}
\newcommand{\□}{\ensuremath{\hat{□}}\xspace}
\newcommand{\Δ}{\ensuremath{\hat{Δ}}\xspace}
\newcommand{\dCube}{\ensuremath{□_{∧∨}}\xspace}
\newcommand{\dcSet}{\ensuremath{\widehat{\dCube}}\xspace}
\newcommand{\FL}{\ensuremath{\textbf{FL}}\xspace}
\newcommand{\M}{\Cat{M}}
\newcommand{\arr}[1]{#1^{→}}
\newcommand{\FinSetOp}{\ensuremath{{\mathbf{FinSet}\rlap{\raisebox{0.75ex}{\rotatebox{90}{*}}}\raisebox{-0.3ex}{\rotatebox{90}{*}}}^\mathsf{op}}\xspace}
\newcommand{\FinSet}{\ensuremath{{\mathbf{FinSet}\rlap{\raisebox{0.75ex}{\rotatebox{90}{*}}}\raisebox{-0.3ex}{\rotatebox{90}{*}}}}\xspace}
% \newcommand{\Yo}{\mathbf{y}}
%
\newcommand{\pb}{\arrow[dr,phantom,very near start, "\lrcorner"]}
\newcommand{\pu}{\arrow[dr,phantom,very near end, "\ulcorner"]}
\newcommand{\Ob}[1][0.66em]{\begin{tikzpicture}[y=#1,x=#1]
\draw[line join=round] (0,1) -- (0,0) -- (1,0) -- (1,1);
\end{tikzpicture}
}
% \AtBeginDocument{\DeclareMathSymbol{→}{\mathbin}{symbols}{"21}} % I don't know why this does not work
\title{A uniform equivariant model for cubical Type Theory}
\author{Dennis Frieberg}
\date{\today}
\begin{document}
Hallo Welt!
\maketitle
\tableofcontents
\subfile{Preliminaries/Preliminaries}
\subfile{main/Mainpart}
\listoftodos
\printindex
\printbibliography
\end{document}

89
src/Preliminaries/Categorical_Semantics.tex Normal file
View file

@ -0,0 +1,89 @@
\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}

373
src/Preliminaries/Cubical_Set.tex Normal file
View file

@ -0,0 +1,373 @@
\documentclass[../Main.tex]{subfiles}
\begin{document}
\section{Cubical Sets}
\subsection{Category of Cubes}
%TODO auto correct
%TODO proof read
%TODO Dedekind cubes
%TODO connections
The first question we need to answer, what site to consider. In the simplicial world there is more
or less a consesus, what exactly the site should be. In the cubical world there are multiple models
with slightly different sites. Our main protagonist will be the cartesian model, but we will also
need to introduce the Dedekind model, as it will appear in an argument later. For a comperative
analysis we direct the reader to \cite{cavalloUnifyingCubicalModels2016} and \cite{ABCHFL}.
\subsubsection{Cartesian cubes}
The most uniform description is probably in form of Lawvere theories,
but our site has a more direct description \cite{mathematicalsciencesresearchinstitutemsriEquivariantUniformKan2020}.
\begin{definition}
Let \(\mathrm{FinSet}\) be the category whose objects are the subsets of \(ℕ\), of the form \(\{0,..,n\}\), for some
\(n ∈ ℕ\), and as morphisms functions between them.
\end{definition}
\begin{remark}
Up to equivalence this is the category of finite sets. Choosing a skeleton will circumvent later size issues, but
for convenience we will pretend that these are finite sets and not always reindex our sets to have an initial segment
of \(ℕ\).
\end{remark}
\begin{definition}\label{def:cartCubeSet}
Let \( □ ≔ {\mathrm{FinSet}\rlap{\raisebox{0.75ex}{\rotatebox{90}{*}}}\raisebox{-0.3ex}{\rotatebox{90}{*}}}^\mathsf{op}\)
the opposite category of double-pointed finite sets.
\end{definition}
An alternative definition would be
\begin{definition}\label{def:cartCubeTheory}
Let \(□\) be the Lawvere-theory of the type theory with a single type \I, and
two constants \(⊥ : \I\) and \(⊤ : \I\).
\end{definition}
\begin{remark}
As in light of \fref{def:cartCubeSet} and \fref{def:cartCubeTheory} we sometimes talk about morphisms
as functions \(X + 2 → Y + 2\) preserving both points in \(2\) or equivalently ordinary functions \(X → Y+2\).
\end{remark}
We will now spend some time exploring, why this might be viewed as the cube category.
We write \(\{⊥|a,b,c|⊤\}\) for double pointed finite sets, where \(⊥\) and \(⊤\) are the
two distunguished points. A cube of dimension \(n\) is now interpreted as such a set
with \(n+2\) (\(n\) without the distinguished points) many elements. We think of these
as dimension variables. We could for example think about the zero dimensional cube
(a point) \(\{⊥|⊤\}\) and the 2 dimensional cube (a square) \(\{⊥|a,b|⊤\}\).
How many maps do we expect from the line, into the point? Exactly one. And this is
also exactly what we get, a fitting map in \( \FinSetOp \) corresponds to a function
\(\{⊥|⊤\} → \{⊥|a,b|⊤\}\) preserving \(⊥\) and \(⊤\), this is already unique.
In the other direction we have four maps. These encode the corners. For example the corner “\((⊥,⊥)\)”
gets encode by sending \(a\) and \(b\) to \(⊥\).
Lets increase the dimensions a bit and look at the maps from a 1 dimensional cube (a line segment)
\(\{⊥|x|⊤\}\}\) into the square. These correspond to functions from \(\{a,b\} → \{⊥,x,⊤\}\). We
can think of this as a dimensional description of a line in a square. We have 2 dimensions in which
the line can move \(a\) and \(b\). And in this two dimennsions the line can either be constant (sending
this dimension to \(⊥\) or \(⊤\), or can advance along its dimension (sending the dimension to \(x\)).
So we get the degenerate corner points (as lines), by sending both of \(a\) and \(b\) to \(⊥\) or \(⊤\).
We get the for sides of the square by sending one of \(a\) or \(b\) to \(⊥\) or \(⊤\). The two sides
that run along the dimension \(a\) send \(a\) to \(x\).
One function is left, sending both \(a\) and \(b\) to \(x\). This is the line that advances in both
dimensions. Or in other words the diagonal.
\begin{remark}
Our cube category is closed under taking products. This differs from the simplicial case. This will turn out to be very handy and
important later.
\end{remark}
As we will need some of these element througout the document again we will give them names.
\begin{definition}[Notation for cubes]\label{def:cubeNotation}
We call:
\begin{itemize}
\item \([0] ≔ \{⊥|⊤\}\)
\item \([1] ≔ \{⊥|x|⊤\}\)
\item \(\deg(x) ≔ |x| - 2\)
\item \(\mathrm{d}_k ­­: [0] → [1]\) with \(k ∈ \{⊤,⊥\}\), be the map given by the function that sends \(x \mapsto k\)
\end{itemize}
\end{definition}
\begin{figure}
\centering
\includesvg[inkscapearea=nocrop,inkscapedpi=500]{figures/square_example_picture.svg}
\caption{A square with some lines maped into it}
\todo[inline]{fix 0 to \(⊥\) and same for 1}
\end{figure}
Also while \(□\) is not a strict Reedy-category (as \(Δ\) is) it is almost, namely an Eilenberg-Zilber category.
So most of Reedy theory from the simplicial case can be salvaged. This will play an integral part in the
prove that our model structure on \□ is equivalent to spaces.
\begin{definition}[generalized Reedy-category] %TODO add cite nlab
A \emph{generalized Reedy category} is a category \C together with two
wide subcategories \(\C_+\) and \(\C_-\) and a function \(d:\mathrm{ob}(\C) → α\) called \emph{degree},
for some ordinal \(α\), such that
\begin{enumerate}
\item every non-isomorphism in \(\C_+\) raises degree,
\item every non-isomorphism in \(\C_-\) lowers degree,
\item every isomorphism in \C preserves degree,
\item \(\C_+ ∩ \C_-\) is the core of \C
\item every morphism factors as a mapn in \(\C_-\) followed by a map in \(\C_+\), uniquely up
to isomorphism
\item if \(f ∈ \C_-\) and \(θ\) is an isomorphism such that \(θf = f\), then \(θ = \id\)
\end{enumerate}
\end{definition}
Which will be an important concept later, but in our special case we can do even better
\begin{definition}[Eilenberg-Zilber category] %TODO add cite nlab
An \emph{Eilenberg-Zilber category} or short \emph{EZ-category} is a small category \C
equipped with a function \(d:\mathrm{ob}(\C)→ℕ\) such that
\begin{enumerate}
\item For \(f : x → y\) a morphism of \C: \label{EZ:1}
\begin{enumerate}
\item If \(f\) is an isomorphism, then \(d(x) = d(y)\).
\item If \(f\) is a noninvertible monomorphism, then \(d(x) < d(y)\).
\item If \(f\) is a noninvertible split epimorphism, then \(d(x) > d(y)\).
\end{enumerate}
\item Every morphism factors as a split epimorphism followed by a monomorphism. \label{EZ:2}
\item Every pair of split epimorphisms in \C has an absolute pushout. \label{EZ:3}
\end{enumerate}
\end{definition}
\begin{remark}
Cleary every EZ-category is a generalized Reedy category
\end{remark}
\begin{theorem}\label{thm:CisEZ}
\(□\) together with \(\deg\) is an EZ-category
\end{theorem}
Before we give a proof we will give a technical lemma about absolute pushouts of split epis.
\begin{lemma}\label{absolutePushout} %TODO cite nlab absolute pushout
Let
\begin{equation*}
\begin{tikzcd}
A \arrow[r, two heads, "b"'] \arrow[d, two heads, "c"] & B \arrow[l,bend right, dashed, "b'"'] \arrow[d, two heads, "d_1"'] \\
C \arrow[r, "d_2"] \arrow[u,bend left, dashed,"c'"] & D \arrow[u, bend right, dashed,"d_1'"']
\end{tikzcd}
\end{equation*}
be a diagram in a category \C of split epis such that, \(bc' = d_1'd_2\). Then it is already a pushout square.
\end{lemma}
\begin{proof}
We look at an arbitrary cocone
\begin{equation*}
\begin{tikzcd}
A \arrow[r, two heads, "b"] \arrow[d, two heads, "c"] & B \arrow[d, "e_1"] \\
C \arrow[r, "e_2"] & E
\end{tikzcd}
\end{equation*}
We can compose this square with \((c',d_1')\) yielding
\begin{equation*}
\begin{tikzcd}
C \arrow[d,"c'"] \arrow[r, "d_2"] \arrow[dd,bend right, "\id"'] & D \arrow[d,"d_1'"] \\
A \arrow[r, two heads, "b"] \arrow[d, two heads, "c"] & B \arrow[d, "e_1"] \\
C \arrow[r, "e_2"] & E
\end{tikzcd}
\end{equation*}
We get our candidate map from \(e_1d_1' : D → E\). We need to show that it commuts with \(e_1\) and \(d_1\) as well as
\(e_2\) and \(d_2\). The second case \(e_1d_1'd_2 = e_2\) is directly obvious from the diagram.
To check that \(e_1d_1'd_1 = e_1\) it is enough to check that \(be_1d_1'd_1 = be_1\), as \(b\) is epic. Which is a
straight forward diagramm chase, if one adds all the undrawn arrwos to the diagram above. Since \(d_1\), are epic \(e_1d'_1\) is unique in fulfilling already one of the two conditions.
\end{proof}
\begin{remark}
As we see in the proof, we don't need \(b\) to be split, but our application needs the split, as split epis are
preserved by pushouts and general epis are not.
\end{remark}
\begin{remark}
As split epis and commutativity is preserved by all functors, pushouts of this form are absolute pushouts.
\end{remark}
As we will use the following statement multiple times in the proof we put it into its own lemma.
\begin{lemma} \label{EZ:split}
Every epi in \(□\) splits. Or dually every mono in \(\FinSet\) has a retraction.
This can be constructed in a way that for a mono \(f\) in \(\FinSet\) the corresponding contraction
sends everything not in the image of \(f\) to \(⊥\).
\end{lemma}
\begin{proof}
Let \(f\) be an epi in \(□\). It is thus a monomorphism in \(\FinSet\). We construct a retraction
\(g\) (that will be a split in \(□\)). Let \(g(x)\) by the unique pre image of \(f\) if it is not empty. If it is empty we choose
any element (for example \(⊥\)). It is trivial to verify that this is a retraction. And as \(f\) needs to
preserve the destinguished points, \(g\) does to.
\end{proof}
\begin{proof}[Proof of theorem \ref{thm:CisEZ}]
Property \ref{EZ:1} follows from basic facts about surjectivity and injectivity between finite sets.
Property \ref{EZ:2} needs us to find a (epi,mono) factorization in \(\FinSet\). This factorization
can be obtained in the same way one would obtain it \(\Set\), by factoring an morphism through its image.
It is straight forward to verify, that the distinguished points are preserved by those maps. And the
that the epi (in \(□\)) splits follows from \ref{EZ:split}.
For property \ref{EZ:3}, we only need find a pushout and splits of the form described in \ref{absolutePushout}.
So let \(c : A → C\) and \(b : A → B\) spilt epis. We will do this by
constructing the dual digram in \(\FinSet\). We will keep the names for the morphisms. As pullbacks over non-empty diagrams
work in \(\FinSet\) like in \(\Set\) we can construct a pullback. Now we must construct the
dotted arrows that satisfy the dual properties of lemma \ref{absolutePushout}.
\begin{equation*}
\begin{tikzcd}
D \arrow[r, tail ,"b^*c"] \arrow[d,tail, "c^*b"] \pb & B \arrow[d,tail, "b"'] \\
C \arrow[r,tail,"c"] \arrow[u,dashed, two heads, "(c^*b)'", bend left] & A \arrow[l, bend left,dashed, two heads, "c'"] \arrow[u,bend right,dashed,two heads ,"b'"']
\end{tikzcd}
\end{equation*}
Let \(c'\), \(b'\) and \((c\*b)'\) be retractions of \(c\), \(b\) and \(c^*b\) that sends everything that is not in
their image to \(0\).
We will show the required commutativity by case distinction
Let \(x ∈ C\). Note that \(x ∈ \im c^*b\) if and only if \(c(x) ∈ \im b\) as this is a pullback diagram. Thus it is
immediatly clear that if \(x\) is not contained in \(\im c^*b\) that \((b^*c)(c^*b)'(x) = 0 = b'c(x)\). Let us turn to
the case that \(x ∈ \im c^*b \). As restricted to those \(x\) the map \(c^*b\) is surjective it suffices to check
\( b'c(c^*b) = (b^*c)(c^*b)'(c^*b) \).
\begin{equation*}
(b^*c) = b'b(b^*c) = b'c(c^*b) = (b^*c)(c^*b)'(c^*b) = (b^*c)
\end{equation*}
Thus the corresponding diagram in \(□\) fulfills the requirements of lemma \ref{absolutePushout}, and is thus
an absolute pushout square.
\end{proof}
Next we start looking at the presheaf topos on our cube category \(\hat{□}\).
We will recall some important concepts, and give some construtcion, that we will
use later. Also we introduce some notation.
\begin{definition}[Notation for Cubical Sets]\label{def:notationCubeSets}
We fix the following notations for Cartesian cubical sets:
\begin{itemize}
\item \(* ≔ \Yo{[0]}\)
\item \(\I ≔ \Yo{[1]}\)
\item \(δ_k ­≔ \Yo \mathrm{d}_k\)
\end{itemize}
\end{definition}
\subsubsection{Dedekind cubes}
We will also encounter the so called Dedekind cubes. There are also multiple ways to look at them. We will present
multiple definitions, but skip the equivalence proofs as they don't bear much inside into the subject.
\begin{definition}\leavevmode
\begin{itemize}
\item Let \FL be the category of finite lattices and monotone maps.
\item Let \(𝟚\) be the finite lattice \(⊥ ≤ ⊤\).
\end{itemize}
\end{definition}
\begin{definition}\label{def:dedCubeLat}
The category \(□_{∧∨}\) is the full subcategory of \FL, restricted to objects of the form \(𝟚^n\) with \(n ∈ ℕ\).
\end{definition}
\begin{definition}\label{def:dedCubeTheory}
The category \(□_{∧∨}\) is the Lawvere-theory of the theory of lattices.
\end{definition}
Unraveling this definition gives us a quite similar description to our description of Cartesian cubes.
Let \(F\) be the functor that assigns to a set its free lattice. We have then as objects
natural numbers (or up to equivalence finite sets). And again we will write elements of these as lower
roman letters instead of natural numbers to keep the confusion between sets and their elements minimal.
A morphism \(m → n\) is a function
from \(n → F(m)\). This adds a few more degeneracy maps, but the general geometric intuition stays the
same. The elments of of an object are dimensions, and maps do give us for every dimension in the target
a term, that describes the behaiviour of our domain in that particular direction. If we look at an
example again one might ask what the difference is, between the new degeneracies map from a square
to the interval in comparison to the old one. We can view these as degenrate squares where we map the top
and right (or bottom and left) side along the interval and the other to sides to \(⊥\) (or \(⊤\)).
This wasn't possible before and will make a drastic difference once we start considiring filling and
composition problems.
\begin{figure}
\missingfigure{draw pictures for this}
\caption{A squre degenrated with a connection. The upper and right side are equal while the left and bottom side is degenrated to point.}
\end{figure}
\todo{add figure for \(2→2\) degeneracy map}
\begin{proposition}
The Dedekind cubes are an EZ-category
\end{proposition}
\begin{proof}[Proof sketch:]
This can be proven by an analog argument as \fref{thm:CisEZ}
\end{proof}
If it is clear from the context we will use the notation from \fref{def:cubeNotation} and \fref{def:notationCubeSets} for
the anologous objects of the Dedekind cubes.
\todo{think about if I want to write down the proof}
% We want to recall universes though, as they will become important later again.
% As a warm-up lets consider \(\Set\), as the presheaves over the singleton category.
% We now want to classify all small sets indexed by some set. This is relatively easy, we take the set
% of all small sets, lets call it \(U\) and the set of all elements of all small sets \(E ≔ ∐_{u ∈ U} u\)
% together with the map \(p_U : E → U\) sending each element back to the set where it came from
% \(p_U(s,x) ≔ s\). Another way to express \(E\) would be in term of pointed samll sets, so could
% equivalently define \(E ≔ \Set_{κ}^{*}\). So how do we recover a collection of small sets from this? We just take
% from our potential index set \(α : X → U\) to U. We can then get a pullback.
% \begin{equation}
% \begin{tikzcd}
% A \arrow[d,"α^{*}p_u"] \arrow[r] \arrow[dr,phantom, "\lrcorner", very near start] & E \arrow[d,"p_U"] \\
% X \arrow[r,"α"] & U
% \end{tikzcd}
% \end{equation}
% And get small sets indexed by \(X\) by sending \(x \mapsto α^{*}p_u^{-1}(x)\). But can we get all those maps
% as pullbacks? Indeed we can, given such a map \(p\) we define \(α(x) ≔ p^{-1}(x)\). Or in more categorical
% terms we are \(α\) sends \(x\) to the collection of \(a\) such that the following diagram commutes.
% \begin{equation}
% \begin{tikzcd}
% \Yo{*} \arrow[r,"a", dashed] \arrow[d,"\id"] & A \arrow[d,"p"] \\
% \Yo{*} \arrow[r,"x"] & X
% \end{tikzcd}
% \end{equation}
%
% Now let us get back to an arbitrary presheaf category. Let \(\C\) be a category, that we will use as
% our site from here on.
% We first need to make percise what our analogon for
% small set, and collection for small indexed sets is.
%
% \begin{definition} %TODO cite to awodeyKripkeJoyalForcingType2021 Definition 1.1 ? % TODO fix newline shit
% \begin{enumerate}
% \item A presheaf is called small if all its values are small
% \item A map of presheaves \(p : A → X \) is small if for every \(x : \Yo c → X \) the
% presheaf \(A_x\) obtained by the pullback
% \begin{equation*}
% \begin{tikzcd}
% A_x \arrow[r] \arrow[d] \arrow[dr, phantom, "\lrcorner", very near start] & A \arrow[d,"p"] \\
% \Yo c \arrow[r,"x"] & X
% \end{tikzcd}
% \end{equation*}
% is small.
% \end{enumerate}
% \end{definition}
%
% We want now to mimic the set case, so let us first look at, how \(α\) would look, if we just do
% the straight forward generalization.
% \begin{equation*}
% \begin{tikzcd}
% \Yo d \arrow[r,dashed, "a"] \arrow[d,"\Yo f"] & A \arrow[d,"p"] \\
% \Yo c \arrow[r,"x"] & X
% \end{tikzcd}
% \end{equation*}
% Notice that we gained an additional dependency, that this diagram depends on, namely \(f\).
% This makes \(α(x)\) a (small) presheaf on \(\C / c \). And gives rise to the follwing definition:
%
% \begin{equation}
% U(c) ≔ \Obj [ (\C / c)^{\op},\Set_{κ}]
% \end{equation}
% The action on \(U(f)\) for \(f : d → c \) in \(\C\) is given by precomposition with the induced functor
% \( \C / d → \C / c \). And similiar to the \(\Set\) case we can define:
% \begin{equation}
% E(c) ≔ \Obj [ (\C / c)^{\op},\Set^{*}_{κ}]
% \end{equation}
% and let the forgetfull functor \(\Set^{*} → \Set\) induce \(p_U : E → U\).
%
%
% There are lots of equivalent descriptions of the suboject classifier \(Ω\), we want to recall one quite similiar to our universe
% definition. We call \(\mathbf{2}\) the category of the well-ordering with two elements \( 0 ≤ 1 \).
%
% \begin{definition}
% We define
% \begin{equation*}
% Ω(c) ≔ \Obj[(\C / c)^{\op},\mathbf{2}]
% \end{equation*}
% The natural transformation \(\t: * → Ω\) is given by the presheaves that have constant value 1. We call
% \(\t\) a \emph{suboject classifier} ttt
% \end{definition}
\end{document}

395
src/Preliminaries/Cubical_Type_Theory.tex Normal file
View file

@ -0,0 +1,395 @@
\documentclass[../Main.tex]{subfiles}
\begin{document}
\section{Cubical Type Theory}
This section is mainly to give the reader which is not aquainted 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 similiar 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 syntactial rules that captures the behaviour 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 univese 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 isomorph
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
correpsonds 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 typetheory to talk about the
underlying inteval 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 isomomorhpic 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 thoery 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 judgements, of the form
\begin{equation*}
Φ ⊢ α \cofib \quad \textrm{and} \quad Φ ⊢ ϕ \formula
\end{equation*}
Our \(ϕ\) will constist 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 exmaple \(Φ ⊢ 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 exmaple 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 intution 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. Nameliy \(∀\), 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 arcoss 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 similiar 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.
Unravelling the definition of a lawvere theory, we get that the site of the \cite{CCHM} consists of
a skelleton 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 ist 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 judgements 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 fibres.
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 gooing 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
degenracy corresponds to the meet (\(∧\)). Or syntactically more explicit, if we have
a line of types \(r:\I⊢A\) we can get a degenarete square of types \(r:\I,r':\I⊢A(r/r∧r')\).
In point set topology we could think about ths 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 algbera. 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 judgemental 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 completly 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 syntactial 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 extrem 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 litrature?}
\todo{make handrawn 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 handrawn 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}

62
src/Preliminaries/Dependent_Type_Theory.tex Normal file
View file

@ -0,0 +1,62 @@
\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}

51
src/Preliminaries/Leibniz_Construction.tex Normal file
View file

@ -0,0 +1,51 @@
\documentclass[../Main.tex]{subfiles}
\begin{document}
\section{Leibniz Construction}
We will see use a well know construction in homotopy theory, to
elegantly construct a lot of interesting objects, the Leibniz construction.
This section will recall the definition establish some facts and give some examples.
There are multiple
We start be giving the definition
\begin{definition}[Leibniz Construction]
Let \(\A\), \(\B\) and \(\C\) be categories and \(\C\) has finite pushouts. Let \(⊗ : \A × \B → \C \) be a bifunctor.
Then we define \(\hat{⊗} : \arr{\A} × \arr{\B} → \arr{\C}\) to defined as follows. Given \(f : A → A' \) in \(\A\) and
\( g : B → B' \) in \(\B\), then \( f \hat{⊗} g \) is defined as in the following diagram.\\
\begin{equation*}
\begin{tikzcd}
A ⊗ B \arrow[r, "f ⊗ \id"] \arrow[d, "\id ⊗ g"] \arrow[dr, phantom, "\ulcorner", very near end] & A' ⊗ \mathrlap{B} \phantom{A'} \arrow[ddr, bend left, "\id ⊗ g"] \arrow[d] & \\
\phantom{B'} \mathllap{A} ⊗ B' \arrow[drr, bend right, "f ⊗ \id"] \arrow[r] & A ⊗ B' ∐\limits_{A ⊗ B} A' ⊗ B \arrow[dr, dashed ,"f \hat{⊗} g"] & \\
& & A' ⊗ B'
\end{tikzcd}
\end{equation*}
\end{definition}
When the bifunctor is the cartesian product functor, this construction is also known as the \emph{pushout-product}.
Now we will give some examples, some of them instructive and some that will appear later again.
\begin{example}
Let \(\C\) be your favourite category of spaces, \( × \) the cartesian product and \(f = g\) be the
inclusion of the point into the start of the interval. Then the pushout-product \(f \hat{×} g \) is the inclusion of
two adjacents sides of a square, into that square.
\end{example}
Or a bit more general
\begin{example}\label{Leibniz:Ex:OpenBox}
Let \(\C\) be your favourite category of spaces, \( × \) the cartesian poduct. Let \(f\) be the
inclusion of one endpoint into the interval. Let \(g : ∂\I^n → \I^n \) be the boundary inclusion into
the \(n\)-cube. Then \(f \hat{×} \) is the filling of an \(n\) dimensional open box.
\end{example}
\begin{example}
Let \(\C\) be your favourite category of spaces, and \( @ : \C^{\C} × \C → \C \) defined as
\( F @ x ≔ F(x)\) the functor application functor. Let \(\I ⊗ (−)\) be a functorial cylinder and \(i_0\).
be one of the inclusions \( i_0 : \Id → \I ⊗ (−) \) and \( ∂X → X \) be the boundery inclusion of \(X\).
Then \( i_0 \hat{@} (∂X → X) \) is the filling of a cylinder with one base surface of shape \(X\).
\end{example}
As we will come across this example multiple times it will get some special syntax.
\begin{definition}
\end{definition}
% TODO Left adjoint
\end{document}

8
src/Preliminaries/Model_Categories.tex Normal file
View file

@ -0,0 +1,8 @@
\documentclass[Preliminaries.tex]{subfiles}
\begin{document}
\section{Model Categories}
We will need some basic knowledge about model categories. A nice introduction can be found in the
nlab\cite{IntroductionHomotopyTheory}. A more feature complete reference is this book by Hirschhorn\cite{hirschhornModelCategoriesTheir2009}
\end{document}

417
src/Preliminaries/Model_Structure.tex Normal file
View file

@ -0,0 +1,417 @@
\documentclass[../Main.tex]{subfiles}
\begin{document}
\section{Model structure}\label{modelStructure}
% TODO restructure lifting with respect to category
% awfs
% Then cubical sets
\subsection{Cartesian Cubes}
We now presenting our, main star, the equivariant model structure on cubical sets.
We will give a description of the two involved factorization systems and then follow
an argument from \cite{cavalloRelativeEleganceCartesian2022}, to show that it is indeed
a model structure. The modelstructure as well as the presentation is taken from
\cite{mathematicalsciencesresearchinstitutemsriEquivariantUniformKan2020}. This
equivariant model structure is also know as the ACCRS model structure.
% reference for uniform fibrations CCHM and
The “usual” model structure on this cube category is not equivalent to spaces, as shown
by Buchholtz. %TODO find citation
If we build the qutoient by swapping the dimensions of a square, the resulting space is not
contractable, while in spaces it is. The idea is to correct this defect, by making the embedding
of the point a trivial cofibration. This is archived by forcing an extra property onto
the fibrations.
\begin{equation*}
\begin{tikzcd}[column sep=large]
* \arrow[r,"\id"] \arrow[d,tail,"f"] & * \arrow[d,tail,"σf"'] \arrow[r] & * \arrow[d,tail] \arrow[r,"β"] & X \arrow[d,"f"] \\
\I^2 \arrow[r,"σ"', shift right=0.5ex] \arrow[r,"\id", shift left=0.5ex] \arrow[urrr, dashed, ,near end, "{j(αe,β)}"'] & \I^2 \arrow[urr, dashed, "{j(αeσ,β)}"] \arrow[r, "e"] & Q \arrow[r,"α"] & Y
\end{tikzcd}
\end{equation*} % Fix twist of suboject
Here \(e\) is the coequilizer map. The hope would be, that
the coequilizer, would now present a lift for the right most lifting problem. But in general that
does not hold, the lifts have neither to commute with \(σ\) nor with \(\id\). The path forward
will be to restrict the fibrations to have the desired property.
%
\subsubsection{Weak factorization systems}
If we force additional properties on our lifting problems, one might rightfully
ask if these indeed induce a weak factorization system (wfs). It is also unclear if
there are induced factorizations at all. The good news is, there is a refined version
of the small object argument \ref{smallObject}, that will help us out. This works on
the back of algebraic weak factorization systems. We don't need the whole theory and
get by with the following definitiont.
\begin{definition}\label{def:rightMaps}
Let \J be category and \(J : \J → \M^→\) be a functor. Then an object \(f\) in
\(\M^→\) is a \emph{right \(J\)-map} if for every object \(i\) in \J, and for every
lifting problem
\begin{equation*}
\begin{tikzcd}[column sep=large]
L \arrow[r,"α"] \arrow[d, "Ji"'] & X \arrow[d,"f"] \\
M \arrow[r,"β"] \arrow[ur, dashed,"{j(α,β)}"] & Y
\end{tikzcd}
\end{equation*}
there is a specified lift \(j(α,β)\), such that for every \((a,b) : k → i\) in \J, the diagram
\begin{equation*}
\begin{tikzcd}[column sep=huge]
L' \arrow[r,"a"] \arrow[d,"Jk"'] & L \arrow[r,"α"] \arrow[d,"Ji"] & X \arrow[d,"f"] \\
M' \arrow[urr, dashed, near start, "{j(αa,βb)}"] \arrow[r,"b"] & M \arrow[ur, dashed, "{j(α,β)}"'] \arrow[r,"β"] & Y
\end{tikzcd}
\end{equation*}
commutes.
\end{definition}
\begin{remark}
If we start with a set \J and make it into a discret category, then we will get our old definition
of right lifting map, with an additional choice function for lifts. Which exists anyway if we
are ready to believe in strong enough choice principles.
\end{remark}
After we defined a class of right maps by those lifting problems, it is not clear that these
will yield a wfs.
To get those we invoke a refinment of Quillens small object argument, namely
Garners small object argument \cite{garnerUnderstandingSmallObject2009}. This has the additional benefit of producing
algebraic weak factorization systems (awfs). For a quick reference see
\cite{riehlMadetoOrderWeakFactorization2015a}, and for an extensive tour \cite{riehlAlgebraicModelStructures2011}, or
\cite{bourkeAlgebraicWeakFactorisation2016,bourkeAlgebraicWeakFactorisation2016a}. The main takeaway for
us is the following theorem \cite[][Theorem 2.28]{riehlAlgebraicModelStructures2011}
\begin{theorem}[Garner]\label{smallObject}
Let \(\M\) be a cocomplete category satisfying either of the following conditions.
\begin{itemize}
\item[(\ast)] Every \(X ∈ \M\) is \(α_X\)-presentable for some regular cardinal \(α_X\).
\item[(\dagger)] Every \(X ∈ \M\) is \(α_X\)-bounded with respect to some proper, well-copowered
orthogonal factorization system on \(\M\), for some regular cardinal \(α_X\).
\end{itemize}
Let \( J : \mathcal{J} → \M^→\) be a category over \(\M^→\), with \(\mathcal{J}\) small. Then the free awfs on \(\mathcal{J}\) exists
and is algebraically-free on \(\mathcal{J}\).
\end{theorem}
Without going to much into the size issues, every locally presentable categoy satisfies \((\ast)\). And as \(\□\) is a presheaf
category over a countable category, it is locally presentable. Also by beeing a presheaf category makes it automatically cocomplete.
We also won't clarify all the consequences that getting an awfs instead of a wfs, brings with it. For us the important
thing is, that every awfs has an underlying wfs. The free part of that statement unsures that this construction preserves
the right lifting class.
Now we need to formulate our definitions in a way that agrees with this conditions of this theorem.
\subsubsection{Cofibrations and trivial fibrations}
The short way of specifying this weak factorization system, is by saying
the cofibrations are the monomorphisms. Another, longer way, but for the further development more
enlightening is by formulating this as uniform lifting properties.
The condition to have uniform lifts, comes from \cite{CCHM} and generalized in \cite{gambinoFrobeniusConditionRight2017} . This requirement is motivated to have
constructive interpretation of Cubical type theory. As we don't focus on the typetheoretic interpretation, but on the model structure we won't
explore this further.
\begin{definition}
Let \(\mathcal{M}\) be a pullback stable class of morphisms.
A map \(f\) has the \emph{uniform right lifting property} against a \(\mathcal{M}\), if for every \(m ∈ \mathcal{M}\)
every lifting problem of the form
\begin{equation*}
\begin{tikzcd}[column sep=large]
A \arrow[r,"α"] \arrow[d,"m"'] & X \arrow[d,"f"] \\
B \arrow[r,"β"] \arrow[ur, dashed, "{j(α,β)}"] & Y
\end{tikzcd}
\end{equation*}
has a specified solution, such that for every pullback square the following diagram with the specified
lifts commute.
\begin{equation*}
\begin{tikzcd}[column sep=large]
C \arrow[r,"a"] \arrow[d,"m'"] \pb & A \arrow[r, "α"] \arrow[d, "m"] & X \arrow[d,"f"] \\
D \arrow[r,"b"'] \arrow[urr,dashed,"{j(αa,βb)}"] & B \arrow[ur, dashed, "{j(α,β)}"'] \arrow[r,"β"'] & Y
\end{tikzcd}
\end{equation*}
\end{definition}
\begin{definition}
A \emph{generating cofibration} is a monomorphism into a cube \(c : C ↣ \I^n\)
\end{definition}
\begin{definition}
A \emph{uniform trivial fibration} is a map with the uniform right lifting property against the generating cofibrations.
\end{definition}
Alternatively a definition more in line with our discussion above
\begin{definition}
The category of \emph{uniform generating cofibrations} has as object monomorphisms into a cube \(C ↣ I^n\) of arbitraty dimension, and
as morphism cartesian squares between those.
\end{definition}
\begin{definition}
A \emph{uniform trivial cofibration} is a right map with respect to the inclusion functor from the category of uniform generation cofibrations
into \(\□^→\)
\end{definition}
% TODO show equivalence in a rigorous way.
\subsubsection{Trivial cofibrations and fibrations}
As we sketced above, the strategy will be to make more maps trivial cofibrations. This is done
by making it harder to be a fibration. Before we give the definition in full generality, we
need to adress which coequilizer we talk about percisely.
Of course doing this only in the 2 dimensional case is not enough. For this we need to say what
the “swap” maps are. What these should do is permutating the dimensions. So let \(Σ_k\) be the symmetric group
on \(k\) elements. For every \(σ' ∈ Σ_k\), we get a map from \( σ : \I^k → \I^k \), by \(⟨π_{σ'(1)}, … , π_{σ'(k)}⟩\),
where \(π_l : \I^k → \I \) is the \(l\)-th projection. Also if we have a subcube \(f : \I^n \rightarrowtail \I^k\),
we get a pullback square of the following form
\begin{equation*}
\begin{tikzcd}
\I^n \arrow[r,"\id"] \arrow[d,tail,"f"] \pb & \I^n \arrow[d,tail, "σf"] \\
\I^k \arrow[r,"σ"] & \I^k
\end{tikzcd}
\end{equation*}
whose right arrow we call \(σf\).
%
Now we desrcibe our generating trivial cofibrations. We remeber example \ref{Leibniz:Ex:OpenBox}. We would
like to do the same here, but a bit more general.
Instead we are going for boxfillings in the context of a cube. The definition of those will be very similiar
we will just work in the slice over a cube \(I^k\). We do the Pushout-product in the slice, and
forget the slice to get a map in \(\□\).
\begin{equation*}
\begin{tikzcd}
\left(\faktor{\□}{\I^k} \right) ^{→} × \left(\faktor{\□}{\I^k}\right)^{→} \arrow[r,"\hat{×}_{\I^k}"] & \left(\faktor{\□}{\I^k}\right)^→ \arrow[r,"\textrm{forget}"] & \□^→
\end{tikzcd}
\end{equation*}
What do we change by working in the slice?
For intuiton let us first look at the case
with a one dimensional context. The point in in this context ist the terminal object in \(\faktor{\□}{\I}\).
The interval in this cube category could be described as the pullback, of the interval in \(\□ = \faktor{\□}{\I^0}\)
along the unique map \(\I → \I^0\), or in simpler words it is the left projection \(π_l : \I × \I → \I\).
Let us now look what maps we have from the point into the interval \(\id_\I → π_l \). We get the two
endpoint maps we expected, as \(⟨\id, 0⟩ \) and \(⟨\id, 1⟩\), but in this context we get an additional map,
namely \(⟨\id, \id⟩\). If we would forget the context again (aka beeing in the slice), this is the diagonal of the square. From
a type theoretic perspective this is realy not surprising. Here it amounts to the question, how many different terms
of type \(\I\) can be produced. In an empty context the answer is two.
\begin{align*}
⊢ 0 : \I && ⊢ 1 : \I
\end{align*}
But in the context of \(\I\), the answer is three.
\begin{align*}
i:\I ⊢ 0 : \I && i:\I ⊢ 1 : \I && i:\I ⊢ i : \I
\end{align*}
Like the type theory suggest we can think of this, as an generic element of the interval. That this
element is different from both closed points, is what differentiates the interval from the
coproduct of two points. In the typetheoretic world we want something that is called a composition structure, and these
should also work
along those diagonals, this amounts to be able to have be able to have a cube filling property along those diagonals,
or in other words we want them to be trivial cofibrations too. The earliest mention of the idea the I am aware of is
this short note \cite{coquandVariationCubicalSets2014}, for a discussion see for example \cite{angiuliSyntaxModelsCartesian2021}.
The generalization of the boundary inclusion is straight forward. We just take any cube over \(\I^k\)
\(ζ : \I^n → \I^k\) and a monomorphism \(c : C → \I^n\), this also induces an object in the slice by composition.
Notice that we did not require that \( n ≥ k\).
If we pack all of this into a definiton we get.
\begin{definition}
Let \(ζ : \I^n → \I^k\) be a cube over \(\I^k\) and \(c : C → \I^n\) monic. A map of the form
\begin{equation*}
\begin{tikzcd}
C \arrow[r,"c", tail] \arrow[dr] & \I^n \arrow[d,"ζ"] \arrow[dr,phantom, "\hat{×}_{\I^k}"] & \I^k \arrow[d,"\id"] \arrow[r,"{⟨\id,l⟩}"] & \I^k × \I^m \arrow[dl,"π_l"] \\
& \I^k & \I^k &
\end{tikzcd}
\end{equation*}
is called \emph{generating trivial cofibration}, as a map in \(\□\) with signature \(B_{c,ζ,l} \rightarrowtail \I^m × \I^n\).
\end{definition}
\begin{figure}
\centering
\includesvg[inkscapearea=nocrop,inkscapedpi=500,width=15cm]{figures/trivial_cofibration.svg}
\caption{An example construction of a trivial cofibration}
\end{figure}
We now want to define our fibrations as the uniform equivariant right lifting maps. To do this we need to define what this
actually means. Uniformity wants a choice of lifts that agree with pullback squares between (trivial) cofibrations. %TODO move the uniformity section upwards
\begin{equation*}
\begin{tikzcd}[column sep=large]
A \arrow[r, "a"] \arrow[d, tail] \arrow[dr, phantom, very near start, "\lrcorner"] & B \arrow[d, tail] \arrow[r,"x"] & X \arrow[d, two heads] \\
\I^k \arrow[r,"b"] \arrow[rru, dashed, "{j(xa,yb)}"] & \I^n \arrow[r,"y"] \arrow[ru, dashed, "{j(x,y)}"'] & Y
\end{tikzcd}
\end{equation*}
The uniformity condition wants that the triangle containing both chosen lifts commutes, or as an equation \(j(x,y)b = j(ax,yb)\).
We now need to combine the uniformity and the equivariance condition. As the pushout-product is functorial it is enough to
describe these conditions between the building blocks of our trivial cofibration and apply the pushout-product again.
Again we will do this in a slice and forget the slice afterwards.
\begin{equation*}
\left(
\begin{tikzcd}[column sep = normal]
D \arrow[r,"a"] \arrow[d, tail, "∂"] \pb & C \arrow[d,tail,"c"] &[-20pt] \\
\I^m \arrow[r,"α"] & \I^n \arrow[dr, "ζ"] & \\[-15pt]
& & \I^k
\end{tikzcd}
\right)
\hat{×}_{\I^k}
\left(
\begin{tikzcd}
\I^k \arrow[d,"{⟨\id,l⟩}"] \arrow[r,"\id"] & \I^k \arrow[d,"{⟨\id,σl⟩}"] &[-30pt] \\
\I^k × \I^l \arrow[r,"\id × σ"] & \I^k × \I^l \arrow[dr,"π_l"] & \\[-15pt]
& & \I^k
\end{tikzcd}
\right)
\end{equation*}
Notice that we understand the vertical morphisms as objects of \(\□^→\) and the horizontal ones as morphism in \(\□^→\).
Also notice, that the left diagramm is a square for which we use in our uniformity condition and the right one captures
equivariance. And notice that the pushout-product of the columns yield trivial cofibrations. We will denote the resulting
commutative square as
\begin{equation}\label{devilSquare}
\begin{tikzcd}[column sep=large]
B_{∂,ζα,l} \arrow[r,"{⟨α,a×σ⟩}"] \arrow[d, tail] & B_{c,ζ,σl} \arrow[d, tail] \\
\I^m × \I^l \arrow[r, "α×σ"] & \I^n × \I^l
\end{tikzcd}
\end{equation}
Now we can finaly give the definition of uniform equivariant fibrations.
\begin{definition}
The category of \emph{generating uniform equivariant trivial cofibrations} has as object
generating cofibrations and as morphism squares of the shape defined in \ref{devilSquare}
above.
\end{definition}
\begin{definition}
A \emph{uniform equivariant fibration} is right map with respect to the inclusion functor of the category of generating
uniform equivariant trivial cofibrations into \(\□^→\).
\end{definition}
We will show that this is a modelstructure by using the theory of premodel structures
\cites[section 3]{cavalloRelativeEleganceCartesian2022}[section 3]{solution}{sattlerCYLINDRICALMODELSTRUCTURES}.
\todo{if there is time (there probably won't be) include the premodel theory and explain}
This machinery gives us a nice condition to check if we are actually dealing with a modelstructure.
\begin{theorem}[{\cite[theorem 3.3.5]{cavalloRelativeEleganceCartesian2022}}]\label{thm:premodelIsModel}
Let \(M\) be a cylindrical premodel category in which
\begin{enumerate}
\item all objects are cofibrant;
\item the fibration extension property is satisfied.
\end{enumerate}
Then the premodel structure on \(M\) defines a model structure.
\end{theorem}
For this all to make sense we need to talk about what a \emph{cylindrical premodel} structure is, and what the
\emph{fibration extension property} is.
We will postpone to show that this is indeed a model structure with a univalent universe. First we will give a description
for a model structure on the Dedekind cubes.
\subsection{Dedekind Cubes}
We will also need a description of the model structure on the Dedekind cubes. It is similar in construction, we just
don't need explicit equivariance. It turns out that in the presence of connections we get equivariance for free
\cite[Remark 4.2.26]{cavalloRelativeEleganceCartesian2022}. While the argument that this modelstructure indeed is a
model structure constructing univalent universes is somewhat easier, as we can extract it from an internal description
in the presheaf topos, by using strategies from \cite{LOPS}. As we only need this model structure for a later argument
we will not present all the arguments here.
Characterizing cofibrations and trivial fibrations will done as above.
\begin{definition}
A \emph{generating cofibration} is a monomorphism into a cube \(c : C ↣ \I^n\)
\end{definition}
\begin{definition}
A \emph{uniform trivial fibration} is a map with the uniform right lifting property against the generating cofibrations
\end{definition}
It will be usefull for our later development, to give a characterization in the internal language of the presheaf topos
\(\□_{∧∨}\). For more details on the interpretation of the internal semantics of cubical sets see \cite{awodeyKripkeJoyalForcingType2021}.
For the this style of modeling cubical type thoery inside of topoi see \cite{ortonAxiomsModellingCubical2018}.
We will first give the characterization, then try to give some intuition why it makes sense and afterwards give a prove.
\begin{equation}\label{eq:TFib}
\TFib A ≔ Π_{φ:Ω}Π_{f:[φ] → A} Σ_{a:A} Π_{α: [φ]} v(α) = a
\end{equation}
\missingfigure{draw a tfib explanation}
So assume we have a type \(A\) in some context \(Γ\). For the discussion we will identify types with their
respecting display maps, to keep the notational overhead low.
In this context the display map of \([φ]\) is monomorphism into \(Γ\), or
in other words a subterminal in \(\faktor{\□}{Γ}\). The term \(f : [φ] → A\) corresponds to a map from \([φ]\)
to \(A\). As this is a subterminal we could view it as a partial element of \(A\), or under the analogy to spaces we can
think of \(A\)
like a bundle over \(Γ\), we specify an element in only some fibers of \(A\). The \(a\) now corresponds to a full element
of \(A\) that agrees with the partial element, where it is defined. So giving an element of the type
\(\TFib A\) is like giving an operation that can fill partial elements. Or formulated as a lifting problem:
\begin{equation}
\begin{tikzcd}
{[φ]} \arrow[r,"f"] \arrow[d,tail] & A \arrow[d] \\
Γ \arrow[r,"\id"] \arrow[ru,dashed,"a"'] & Γ
\end{tikzcd}
\end{equation}
%
It is an opration that given \([φ]\) and \(f\) returns an \(a\) and a wittness that the upper triangle commutes.
The lower one commuts automatically by the virtue of \(a\) beeing a term of type \(A\). Notice that uniformity
does not appear explicitly in this description, but happens automatically as pullback squares are the
interpretation of substitutions, and the type thoeretic rules around substitution already imply a uniform
choice of our lifts.
\todo{give a proof or get rid of the claim that we do}
We can also give an anolog description of fibrations. As we do not need to think about equivariance the descriptions
gets a bit less involved but stays basically the same.
\begin{definition}
Let \(c : C ↣ \I^n\) be monic a \emph{generating trivial cofibration} is a map of the form
\( c \× δ_k\)
\end{definition}
\begin{definition}
A \emph{uniform fibration} is a uniform right lifting map against generating trivial cofibrations.
\end{definition}
\begin{proposition}[{\cite[Remark 4.2.26]{cavalloRelativeEleganceCartesian2022}}]\label{prop:dedekindEquivariant}
The uniform fibrations of \(□_{∧∨}\) are equivariant.
\end{proposition}
% % \subsubsubsection{Internal description}
% For our further development we also want an internal description of our fibrations. This turns out to be more tricky then
% the trivial fibration variant for multiple reasons. The first is, that trivial cofibrations are harder to describe then
% cofibrations. We also have an additional condition namely equivariance.
% We also want a universe in the cubical type theory, that corresponds to a fibrant univers of fibrations in \(\□\).
%
% First we need to discuss, how type theory talks about lifting problems.
%
% We will do this the other way round. We first describe our fibrant universe and then get the rest for free. We will
% do this in a way following \cite{LOPS}. The first important obesrvation will be that our functorial cylinder not only
% has a right adjoint, but an even further right adjoint. Or in other words our interval is tiny.
% This can be seen with ease, we can describe the cylinder path space adjunction by a functor on \(□\). Namely the
% product with \([1]\). One checks easaly that \(((−) × [1])_!\) is isomporhic to the product with \(\I\) in \(\□\).
% Like in any presheaf topos we get an induced adjoint triple. This situation is very common to variants of cubical
% sets. In contrast to simplicial sets where this does not happen.
% \begin{equation}
% ((−) × [1])_! ⊣ ((−) × [1])^* ⊣ ((−) × [1])_*
% \end{equation}
% \begin{proposition}
% We have that
% \begin{equation*}
% (−)^\I \cong ((−) × [1])^*
% \end{equation*}
% \end{proposition}
% \begin{proof}
% Let \(A\) be a cubical Set. Because \(□\) is closed under products we get
% by yoneda and the definition of exponentials the following natural isomorphism.
% \begin{equation*}
% A^\I_n \cong \□(\I^n,A^\I) \cong \□(\I^n × \I, A) \cong A([1]^n × [1]) = ((−) × [1])^*(A)_n
% \end{equation*}
% And thus an isomorphism between the given functors.
% \end{proof}
%
% \begin{definition}
% We write \(\sqrt{\phantom{−}} ­≔ ((−)×[1])_* \) for the rightmost adjoint of this adjunction
% triple.
% \end{definition}
\end{document}

19
src/Preliminaries/Preliminaries.tex Normal file
View file

@ -0,0 +1,19 @@
\documentclass[../Main.tex]{subfiles}
\begin{document}
% \chapter{Preliminaries}
\section{Category Theory}
We already assume some basic notions of category theory. For the completly unitiated there are good
references for example \cite{maclaneCategoriesWorkingMathematician1978} or \cite{awodeyCategoryTheory2006}.
We will also assume some familarities with presheave categories \cite{maclaneSheavesGeometryLogic1994}.
But we will revisit some branches of category theory that we will encouter later.
% \subfile{Model_Categories}
\subfile{Leibniz_Construction}
\subfile{Cubical_Set}
\subfile{Model_Structure}
% \subfile{Reedy_Categories}
% \subfile{Dependent_Type_Theory}
% \subfile{Categorical_Semantics}
\end{document}

4
src/Preliminaries/Reedy_Categories.tex Normal file
View file

@ -0,0 +1,4 @@
\documentclass[Preliminaries.tex]{subfiles}
\begin{document}
\end{document}

4
src/Preliminaries/figures/square_example_picture.svg Normal file
View file

File diff suppressed because one or more lines are too long
Side by side

After

Width:  |  Height:  |  Size: 1.2 MiB

4
src/Preliminaries/figures/trivial_cofibration.svg Normal file
View file

File diff suppressed because one or more lines are too long
Side by side

After

Width:  |  Height:  |  Size: 3 MiB

1
src/Preliminaries/resource.bib Symbolic link
View file

@ -0,0 +1 @@
../resource.bib

671
src/main/Equivalence.tex Normal file
View file

@ -0,0 +1,671 @@
\documentclass[../Main.tex]{subfiles}
\begin{document}
\section{Equivalence to spaces}\todo{do I need to explain idempotent completions?}
For this section we fix the following notation. We write \(n\) for a set with cardinality \(n\),
and identify \(2\) with the set \(\{⊥,⊤\}\). Wen write \([n]\) for the well ordered sets
\(\{0,…,n\}\).
We would love to compare the model categories on \(\□\) and \(\Δ\). For this we want at least
an adjoint pair between those. If we somehow could get a functor on the site level, we could
get an adjoint triple. But there is no immediate obvious functor to do the job.
The usual trick would be to go look at the idempotent completions of these categories. These
have usually more objects and are sometimes more suitable as the codomain of a functor, while
the presheaf category stays the same (up to equivalence).
For example the idempotent completion of \dCube is the category \FL of finite lattices and
monotone maps \cites{streicherSimplicialSetsCubical2021}{sattlerIdempotentCompletionCubes2019}.
So we have automatically \(\widehat{\FL} = \dcSet\),
and there is an obvious inclusion \(i: Δ → \FL\). Sadly for us \(□\) is already idempotent complete.
To get around this issue we can embed \(j: □ → \dCube → \FL\), and get into the following situation.
\begin{equation*}
\begin{tikzcd}[column sep=large]
\□ \arrow[from=r,"j^*"{description,name=i}] & \widehat{\FL} %
\arrow[from=l,bend left=50,"j_!"{above,name=ish}] \arrow[from=l,bend right=50, "j_*"{below,name=ist}] %
\arrow[from=r,bend right=50, "i_!"{above,name=jsh}] \arrow[from=r,bend left=50,"i_*"{below,name=jst}] %
& \Δ \arrow[from=l,"i^*"{description,name=j}]
\arrow[phantom,from=i,to=ish,"{\rotatebox{270}{\(⊣\)}}"]
\arrow[phantom,from=ist,to=i,"{\rotatebox{270}{\(⊣\)}}"]
\arrow[phantom,from=j,to=jsh,"{\rotatebox{270}{\(⊣\)}}"]
\arrow[phantom,from=jst,to=j,"{\rotatebox{270}{\(⊣\)}}"]
\end{tikzcd}
\end{equation*}
We can define \(j\) also explicitly like this:
\begin{definition}
Let \(𝟚\) the finite order \(⊥ ≤ ⊤\), if it is convenient we will identify this with the order \(0 ≤ 1\).
\end{definition} \todo{move this somewhere sane}
\begin{definition}\label{def:j}
Let \(j : □ → \FL\) the functor given by the following data:
\begin{itemize}
\item On objects: \(f(\{⊥|x_1…x_n|⊤\}) ­≔ 𝟚^n\) \todo{use \(⊥⊤\) notation in introduction chapter}
\item On morphisms: \(j(f)(g)(x) ≔ \begin{cases}g(f(x)) & f(x) \notin 𝟚 \\ f(x) & f(x) ∈ 𝟚\end{cases}\)
\end{itemize}
\end{definition}
In \cite{rhielVid} it is claimed that \(i^*j_!\) is the triangulation functor and \(j^*i_!\) a
left Quillen homotpoy inverse. In the mean time Reid Barton observed in an yet unpublished paper,
\todo{how to cite this? claimed in \cite{solution}}
that this triangulation can be described by a single functor on the level of sites \(Δ → □\). One
could now establish Quillen equivalence using this functor, for details see \cite[sec. 6]{solution}.
We are going to verify the original argument. To give an overview of the necessary steps:
\begin{enumerate}
\item Show that \(i_!\) and \(i^*\) are left Quillen. \label{step1}
\item Show that \(j_!\) and \(j^*\) are left Quillen. \label{step2}
\item[*] Conclude that all 4 preserve weak equivalences.
\item Show that \(i_! j^*\) and \(j_! i^*\) descend to inverses of the Homotopy Categories.
\end{enumerate}
Before we jump into the formal proofs we like to get some intuition for the four functors of interest.
To make sense of this all we need to understand what happens with \FL. \FL has the luxury as containing
both \(Δ\) as the well orderings and \dCube as \(𝟚^n\). As \FL is the idempotent completion of \dCube,
we also now that a presheaf on \FL, is completly determined by its behavior on \dCube. The two functors
\(i^*\) and \(j^*\) are just the restrictions, but also \(i_!\) and \(j_!\) are geometrically not so
difficult to understand. On the elements in the image of \(i\) (or \(j\)) they agree with the original definition.
Let \(F ∈ \Δ\), then \(F(x) = i_!(F)(i(x))\). The interesting question is what does \(i_!\) define
on cubes and \(j_!\) on simplicials. \(j_!\) will basically triangulate the cube (see \fref{prop:triangulation}),
while \(i_!\) will add just cubes that are degenerated to simplicials.
To understand \(i^*\) a bit better we might take a look how things that are defined on \(𝟚^n\) extend to simplicials.
For this we need to exhibit \([n]\), as a retract of \(𝟚^n\). For this we define two maps.
\begin{definition}
Let
\begin{itemize}
\item \(r: 𝟚^n → [n]\) be the monotone function \(r(f) = Σ_{x ∈ n}f(x)\)
\item \(i: [n] → 𝟚^n\) be the monotone function \(i(x)(y) = \begin{cases} ⊤ & y < x \\ ⊥ & \text{otherwise} \end{cases}\)
\end{itemize}
\end{definition}
We can see directly that this is a split retract pair and thus gives rise to an idempotent \(e = ir : 𝟚^n → 𝟚^n\).
And by general abstract nonesens we get that \(r\) is an absolute coequilizer map of \(e\) and \(\id\). As well as \(i\)
is an aboslute equilizer of \(e\) and \(\id\). So for a presheaf
\(F\) on \FL, we can compute \(F([n])\) as the equilizer from \(F(e)\) and \(F(\id)\), or the coequilizer of \(F(e)\) and \(F(\id)\).
\begin{proposition}\label{prop:i_!Nothing}
\(i_!Δ^n\) agrees with \(\Yo [n]\).
\end{proposition}
\begin{proof}
\begin{equation*}
\Hom_{\FL}(i_!Δ^n,B) = \Hom_{\Δ}(Δ^n,i^*B) = B(i([n])) = B([n]) = \Hom_{\FL}(\Yo [n], B)
\end{equation*}
And by uniqueness of adjoints the claim follows.
\end{proof}
\begin{proposition}\label{prop:j_!Nothing}
\(j_!(\I^n) = \Yo 𝟚^n\)
\end{proposition} \todo{move to a sane place}
\begin{proof}
We have that \(\Hom(j_!(\I^n),B) = \Hom(\I^n,j^*(B))\). And we get
\begin{equation}
\Hom(\Yo 𝟚^n, B) = B(𝟚^n) = B(j(n)) = \Hom(\I^n,j^*B)
\end{equation}
thus by uniqueness of adjoints we have, that \(j_!(\I^n) = \Yo 𝟚^n\).
\end{proof}
Let us start with step 1. We need to show that \(i_!\) and \(i^*\) preserve cofibrations (or
in other words monomorphisms), \(i^*\) preservers fibrations and trivial cofibrations. The hard
part will be to show that \(i_!\) preserves monomorphisms and we will do it last.
\begin{proposition}
\(i^*\) preserves monomorphisms.
\end{proposition}
\begin{proof}
Given a monomorphism \(f\) in \(\Δ\). As being monic can be tested component wise we need
to show that \((i^*f)_x\) is monic, for an arbitrary \(x∈□\). This is just \(f_{(ix)}\) which is monic by assumption.
\end{proof}
\begin{proposition}
\(i^*\) preserves trivial cofibrations \todo{maybe equivalently \(i_*\) preserves fibrations}
\end{proposition}
\begin{proof}
Sketch:
generation trivial cofibrations are pushout product of mono and endpoint inclusion into the interval.
left and right adjoint functor (like \(i_*\) preserve these) pushout product with mono and interval
are also trivial cofibrations in \Δ.
\end{proof}
We get now to the difficult part of step \ref{step1}. The argument we are going to follow is due to Sattler
and involves the Reedy Structure of \(Δ\). We are going through the whole argument here, as it is a good preparation
for \(j_!\) in step \ref{step2}.
\begin{proposition}[{\cite[prop. 3.3]{sattlerIdempotentCompletionCubes2019}}]
\(i_!\) preserves monomorphisms.
\end{proposition}
Following \cite{sattlerIdempotentCompletionCubes2019} we are first going to prove two technical lemma.
Note that a repetition of this argument is also good to check if we actually need an elegant Reedy structure
or if we can do with just an Eilenberg-Zilber category.
\begin{lemma}[{\cite[lem 3.4]{sattlerIdempotentCompletionCubes2019}}]\label{lem:idemLemma3.4}
Let \C be an Eilenberg-Zilber category. Assume \C as pullbacks along face maps.
The functor \(\colim : \hat{\C} → \Set\) preserves monomorphisms.
\end{lemma}
\begin{remark}
The original source has as an extra condition that these pullbacks preserve face and degeneracy maps. We
don't need this by making use of the fact that degeneracies split.
\end{remark}
For this proof we will make some use of the equivalence between presheaves and discrete Grothendieck fibrations.
This has the benefit of exhibiting our monomorphism, as a Grothendieck fibration. We also can lift the
Eilenberg-Zilber structure from our site, a notion that is hard to express with presheaves.
\begin{lemma}\label{lem:liftEZFib}
Let \(\C\) be an Eilenberg-Zilber category, and \(\p : Q → \C\) a discrete Grothendieck fibration.
Then we can lift the Eilenberg-Zilber structure to \(Q\).
\end{lemma}
The hard part of the proof will be the lifting of absolute pushouts. In general pushouts don't need to
lift, as the fibre above the pushout in the base category might be empty. If we had a split pushout like in
lemma \ref{absolutePushout}, we could lift the splits to solve that problem. Sadly not all absolute pushouts
are of this form, but something a bit weaker is true. The first appearance of this observation seems to be
in \cite{pareAbsoluteColimits1971}.
\begin{lemma}\label{lem:absPushChar}
A commutative square
\begin{eqcd*}
A \arrow[r, "p" ] \arrow[d, "q" ] & B \arrow[d, "m"] \\
C \arrow[r, "n"] & P
\end{eqcd*}
is an absolute pushout diagram if and only if there exists
\begin{enumerate}
\item A section \(u : P → B\) of \(m\).
\item Morphisms \(r_1…r_k : B → A \) and \(s_1…s_k : B → A\) for some \( k ≥ 1\), such that \(ps_1 = \id_B\),
\(qs_i = qr_i\) for all \(i\), \(pr_i = ps_{i+1}\) for all \(i < k\), and \(pr_k = um\).
\item Morphisms \(t_1…t_{l+1} : C → A\) and \(v_1…v_l : C → A\) for some \(l ≥ 0\), such that \(qt_1 = \id_C\),
\(pt_i = pv_i\) for all \(i < l\), \(qv_i = qt_{i+1}\) for all \(i ≤ l\), and \(pt_{l+1} = un\).
\end{enumerate}
or the symmetric situation where \(B\) and \(C\) are interchanged.
\end{lemma}
\begin{proof}
Let us assume first we have given all the data above (and WLOG \(B\) and \(C\) are not interchanged), and let
\begin{eqcd*}
A \arrow[r, "p" ] \arrow[d, "q" ] & B \arrow[d, "b"] \\
C \arrow[r, "c"] & X
\end{eqcd*}
a commutative square. We now need to find a \(x : P → X\), that witnesses \(P\) as a pushout.
Since \(m\) splits, \(x\) will be unique automatically. We define \(x ≔ bu\). We now need to check
if it makes the both evident triangles commute. We do this by chasing though all the data we have been given.
\begin{equation*}
xm = bum = bqr_k = cqr_k = cqs_k = bps_k = bqr_{k-1} = … = bps_1 = b
\end{equation*}
and
\begin{equation*}
xn = bun = bpt_{l+1} = cqt_{l+1} = cqv_l = bpv_l = bpt_l = … = cqt_1 = c
\end{equation*}
Now let us assume the given square is an absolute pushout. Now we need to construct all the date from above.
To get the desired split \(u\), we will apply the \(hom(P,−)\) functor and get a pushout square in \(\Set\).
\begin{eqcd*}
\hom(P,A) \arrow[r, "p"] \arrow[d, "q"] \pu & \hom(P,B) \arrow[d, "m"] \\
\hom(P,C) \arrow[r, "n"] & \hom(P,P)
\end{eqcd*}
That means we have a surjection from \(\hom(P,B) + \hom(P,C) → \hom(P,P)\).
A preimage of \(\id_P\) under this surjection is a morphism \(u\) for that either \(mu = \id_P\)
or \(nu = \id_P\) holds. We assume WLOG the first case.
To get \(r_1…r_k\) and \(s_1…s_k\) that relate \(\id_B\) and \(um\), we look at the image under the
\(\hom(B,−)\) functor.
\begin{eqcd*}
\hom(B,A) \arrow[r, "p"] \arrow[d, "q"] \pu & \hom(B,B) \arrow[d, "m"] \\
\hom(B,C) \arrow[r, "n"] & \hom(B,P)
\end{eqcd*}
We know that \(um\) and \(\id_B\), are getting sent to the same map in \(\hom(B,P)\), because
\(mum = m = m\id_B\).
We can now construct a sequence of maps in \(\hom(B,A)\) if we alternate between taking preimages of images
under \(p\) and \(q\). Lets call the preimages along \(p\) \(s_i\), and the preimages along \(q\) \(r_i\).
This procedure immediately guarantees the equations
\begin{align*}
qs_i = qr_i & & pr_i = ps_{i+1} \text{.}
\end{align*}
If we start the procedure with \(\id_B\) in \(\hom(B,B)\), we also get \(ps_1 = \id_B\). Because \(\id_B\) and
\(um\) get sent to the same element along \(m\) there exists a \(k\) and a choice of \(r_i\) and \(s_i\) such that
\(pr_k = um\).
The maps for condition three, can be constructed with the same technique after applying the \(\hom(C,−)\) functor.
The index shift comes from the fact that \(\id_C ∈ \hom(C,C)\) and \(un ∈ \hom(C,B)\) are in opposite corners
of the resulting diagram.
\end{proof}
To be able to lift this structure make sure we can lift commuting triangles first.
\begin{lemma}\label{lem:gfibliftcommute}
Let \(F : Q → \C\) be a discrete Grothendieck fibration, \(f: A → B\) be a morphism in \(Q\), and
\(g : C → F(B)\) and \(h : F(A) → C\) such that \(gh = F(f)\). We can lift \(g\) and \(h\) to form
a commutative diagram in \(Q\).
\begin{eqcd*}[column sep=small]
A \arrow[rr,"f"] \arrow[dr, dashed, "h'"'] & & B \\[-10pt]
& C' \arrow[ur,"g'"', dashed]& \\
F(A) \arrow[rr,"F(f)"] \arrow[dr, "h"'] & & F(B) \\[-10pt]
& C \arrow[ur, "g"'] &
\end{eqcd*}
\end{lemma}
\begin{remark}
It also suffices to just give an object \(B\) and a commutative diagram in \C.
\end{remark}
\begin{proof}
That we can get lifts \(g'\) and \(h'\) follows directly from the definition of discrete Grothendieck fibration.
We only need to argue that the domain of \(h'\) is indeed \(A\) and that the diagram commutes. As \(f\) and \(g'h'\) are lifts
of \(F(f) = gh\), we get \(f = g'h'\) by the uniqueness of lifts.
\end{proof}
\begin{proof}[Proof of Lemma \ref{lem:liftEZFib}]
First we need to define a degree function \(\d : \Obj Q → ℕ\). Let \(\d'\) be the degree function from
\C, we then define \(\d ≔ \d' \p\). The next thing to do is to show that isomorphisms preserve degree, split epis
lower degree and noninvertible monomorphisms increase degree. For that it suffices to show that \(p\) preserves
these. Isomorphisms and split epis are preserved by every functor, so only noninvertible monomorphisms remain.
We will establish this in two steps, first showing mono preservation and then reflection of inverses.
Given some monomorphism \(f : A ↣B\) in \(Q\) and two morphisms \(g,h : C → \p(A)\) in \C, such that \(\p(f)h = \p(f)g \)
We can lift \(g\) and \(h\) to \(g' : C' → A\) and \(h' : C' → A\). By lemma \ref{lem:gfibliftcommute} we have \(fg' = fh'\) and
thus \(g' = h'\). We get directly \( g = \p(g') = \p(h') = h\) and thus \(\p(f)\) is monic.
Assume we have a map \(f\) in \(Q\) such that \(\p(f)\) has a (one sided) inverse. By lemma \ref{lem:gfibliftcommute} the lift
of that (one sided) inverse, is also a (one sided) inverse of \(f\).
This fact also helps us directly in the next step. We need to show that every morphism factors into a split epi followed by
a monomorphism. We can lift a factorization by lemma \ref{lem:gfibliftcommute}, and as one sided inverses are preserved by lifting
\(\p\) reflects split epis. So we only need to show that monos are preserved by liftings. Let \(f : A → B\) be a morphism
in \(Q\), such that \(\p(f)\) is monic and let \(g,h : C → A\) such that \(fg = fh\). Because \(p(f)\) is monic \(\p(g) = \p(h)\),
and thus \(g\) and \(h\) are liftings of the same morphism. As liftings are unique \(g = h\) and \(f\) monic.
As a last step we must establish that a span of split epis has an absolute pushout. So let \(f: A → B \) and \(g : A → C\) be spilt
epimorphisms in \(Q\). As these are preserved by functors \(\p(f)\) and \(\p(g)\) are split epis too. So there is an absolute pushout
of \(\p(f)\) and \(\p(g)\). By lemma \ref{lem:absPushChar}, we can extend this square, by all the extra morphisms that characterize
the absolute pushout. We first lift the split established by 1 in lemma \ref{lem:absPushChar}, to get our candidate pushout.
Lifting the rest of the data, and checking that the required equalities still hold is a tedious but straight forward repeated
application of lemma \ref{lem:liftEZFib}. Afterwards we can apply lemma \ref{lem:absPushChar} again to verify that we indeed got
an absolute pushout in \(Q\).
\end{proof}
\begin{remark}
With the exact same argument we can lift elegant Reedy structures. We don't even need to to check the mono preservation,
we can just define face maps to be lifts of face maps. Even though not explicit in the definition degeneracies in elegant
reedy categories are split epimorphisms. We took the extra effort here to see if this step would be a problem in the cubical
case.
\end{remark}
\begin{lemma}\label{lem:liftPullbacks}
Let \(F : Q → \C\) be a discrete Grothendieck fibration. Given as span in \(Q\) and a pullback of the image of the
span in \C. Then there exists a lift of that pullback completing the original span to a pullback square.
\end{lemma}
\begin{proof}
Let \(p : A → C\) and \(q : B → C\) be a span in \(Q\), such that its image under \(F\) completes to a pullback
square. We can lift this square to a commuting square in \(Q\), by lemma \ref{lem:gfibliftcommute}.
We now need to check that this again a pullback square.
\begin{eqcd*}[column sep=tiny, row sep=small]
X \arrow[dd, bend right, "x"' ] \arrow[rrrd, bend left=15, "y"] \arrow[dr, dashed] & & & \\
& P' \arrow[rr,"p'"] \arrow[dl,"q'"'] & & A \arrow[dl,"f"] \\
B \arrow[rr,"g"'] & & C & \\[30pt]
F(X) \arrow[dd, bend right, "F(x)"'] \arrow[rrrd, bend left=15, "F(y)"] \arrow[dr, dashed] & & & \\
& P \arrow[rr,"p"] \arrow[dl,"q"'] \pb & & F(A) \arrow[dl,"F(f)"] \\
F(B) \arrow[rr, "F(g)"'] & & F(C) &
\end{eqcd*}
So let us take any cospan \((x,y)\) that completes the span \((f,g)\) to a commuting square in \(Q\).
We can map this to \C via \(F\) and get a universal map witnessing that the square in \C is indeed a pullback.
We can lift this map uniquely to \(P'\) along \(F\), and by lemma \ref{lem:gfibliftcommute} this lift makes the
diagram commute.
\end{proof}
We will also need another technical property of discrete Grothendieck fibrations and Eilenberg-Zilber categories.
\begin{lemma}\label{lem:bifib}
Let \(F : P ↣ \C\) be a a monic discrete Grothendieck fibration, and \C be an Eilenberg-Zilber (or elegant Reedy) category. Then
\(F\) as opcartesian lifts of degeneracy maps. \todo{check if we introduced “degeneracy” and “face” as words in the definition}
\end{lemma}
\begin{proof}
So let \(A\) be an object in P and \(f : F(A) → B\) be a degeneracy in \C i.e. a split epi.
We can then lift the split to \(A\), and get a morphism \(g : B' → A\) where \(B'\) is the unique object
above \(B\). We can now lift \(f\), to \(B'\) and get a morphism \(f': A → B'\) above \(f\). Verifying that
\(f'\) has the required universal property is a straight forward repeated application of lemma \ref{lem:gfibliftcommute}.
\end{proof}
\begin{proof}[Proof of Lemma \ref{lem:idemLemma3.4}]
Let \(f : P' ↣ Q'\) be a monomorphism in \(\hat{\C}\). This gives equivalently rise to a monomorphism \(F\)
of discrete Grothendieck fibrations via the category of elements. \todo{do I need to explain this?}
We define \(P ­≔ \int P'\), \(Q ≔ \int Q'\) and \(F ≔ \int f\).
\begin{equation*}
\begin{tikzcd}[column sep=tiny, row sep=small]
P \arrow[rr,"F",tail] \arrow[rd] & & Q \arrow[ld] \\
& \C &
\end{tikzcd}
\end{equation*}
That \(\colim\) sends \(f\) to a monomorphism,
can equivalently stated that \(F\) is monic on connected components. That follows directly from the explicit construction
of colimits in \(\Set\). Also \(F\) gets to be a discrete Grothendieck fibration on its own. We can lift the Eilenberg-Zilber
structure to \(Q\) by lemma \ref{lem:liftEZFib}. Also \(F\) is a bifibration if restricted to the degeneracy maps by lemma \ref{lem:bifib}.
\todo{We don't need this (and the lemma) anymore}
So now let S and T be be objects of \(P\) such that \(F(S)\) and \(F(T)\) lie in the same connected component of \(Q\).
This means there is a zigzag connecting \(F(S)\) and \(F(T)\). We can normalize this to a span. To see this we are going
to show how to turn a cospan into a span of morphisms. So let \( f : D → B\) and \( g : E → B \) be a cospan. Because of the Eilenberg-Zilber
structure we can factor those into a degeneracy followed by a face map. Lets call them \(f_d\), \(f_f\), \(g_d\) and \(g_f\).
\todo{lift the pullback property}
\begin{eqcd*}[column sep=small]
D \arrow[dr, two heads, "f_d"] & & P \arrow [dr, tail] \arrow[dl, tail] \arrow[dd, phantom,very near start, "\rotatebox{-45}{\(\lrcorner\)}"]& & E \arrow[dl, two heads, "g_d"'] \\
{} & • \arrow[dr, tail, "f_f"] \arrow[lu, bend left] & & • \arrow[dl,tail, "g_f"'] \arrow[ru, bend right] & \\
{} & & B & &
\end{eqcd*}
We can then construct the pullback \(P\) along \(f_f\) and \(g_f\), and the resulting maps concated with the splits of \(f_d\) and \(g_d\)
are a span over \(D\) and \(E\). This means \(F(S)\) and \(F(T)\) are connected by a span of morphisms. Because \(F\) is injective
on objects we can lift this span to a span from \(S\) to \(T\) and thus \(S\) and \(T\) are in the same connected component.
\end{proof}
Before we continue to follow \cite{sattlerIdempotentCompletionCubes2019}, we need yet another lemma about lifting elegant Reedy
structures. Sadly this does not work well for Eilenberg-Zilber categories. So we need to find a way around this later.
\begin{lemma}\label{liftReedyToComma}
Let \A be an elegant Reedy category, \(i : \A → \B \) a functor and \(B ∈ \B \) an object in \B. We can lift
the elegant Reedy structure along \(p : B ↓ i → \A \), where \(p\) is the evident projection from the comma
category. \todo{fill the gaps}
\end{lemma}
\begin{proof}
First we need to define a degree function \(\d: \Obj (\B) → ℕ\), let \(\d'\) be the degree function from the elegant Reedy structure
we can then define \(\d ≔ \d'p\). We define the degeneracies and faces, as being degeneracies and faces under \(p\).
Here we would already get a problem with EZ-categories as we might have maps that are monic in \(B ↓ i\), but not in \B.
As a next step we need to construct desired factorization into a degeneracy and a face map. So we take
a map \(f\) in \(B ↓ i\) and factor it as a map in \A into \(f = f_f f_d\). If we try to lift the factorization
we end up with the following diagram.
\begin{eqcd*}
{} & B \arrow[dl, "ϕ"'] \arrow[dr, "ϕ'"] & \\
i(A) \arrow[rr,"i(f)", near start] \arrow[dr, "i(f_d)"'] & & i(A') \\
{} & i(X) \arrow[ur, "i(f_f)"'] \arrow[from=uu, crossing over, "i(f_d)ϕ", near start] &
\end{eqcd*}
It remains to show that the front right triangle commutes.
\begin{equation*}
i(f_f)(i(f_d)ϕ) = (i(f_f)i(f_d))ϕ= i(f_f f_d) ϕ = i(f) ϕ = ϕ'
\end{equation*}
% Is there an error here? The split makes a problem right?
It is then tedious, but straight forward to check one of the equivalent elegance axioms.
\end{proof}
\begin{lemma}\label{commaPullback}
Let \(i : \A → \B\) be a functor, and \(B\) an object of \(\B\), and let \(p : B ↓ i → A \) be the projection map. A
span in \(B ↓ i\) has a pullback, if the span has a pullback in \B, and the pullback square lies in the image of \(i\).
\end{lemma}
\begin{remark}
Usually this situation is given, if \A has pullbacks along a class of maps and \(i\) preserves them.
\end{remark}
\begin{proof}
So consider a span of maps in \(B ↓ i\). That fulfills the conditions of this lemma.
If we unravel this, we get the following diagram
\begin{eqcd*}
{} & B \arrow[rdd, "ϕ'", bend left] \arrow[ldd, "ϕ"', bend right] & \\
{} & & \\
i(X) \arrow[rd, "i(f)"] & & i(Y) \arrow[ld, "i(g)"'] \\
{} & i(Z) &
\end{eqcd*}
By assumption we have pullbacks of \(i(f)\) and \(i(g)\) in \B, that lies in the image of \(i\). So we
can complete the diagram
\begin{eqcd*}
{} & B \arrow[rdd, "ϕ'", bend left] \arrow[ldd, "ϕ"', bend right] \arrow[d,dashed, "{⟨ϕ,ϕ'⟩}"] & \\
{} & i(P) \arrow[ld] \arrow[rd] & \\
i(X) \arrow[rd, "i(f)"] & & i(Y) \arrow[ld, "i(g)"'] \\
{} & i(Z) &
\end{eqcd*}
and exhibit \(i(P)\) as an object in \(B ↓ i\) by the universal map of the pullback.
\end{proof}
\begin{lemma}[{\cite[lemma 3.5]{sattlerIdempotentCompletionCubes2019}}]\label{lem:idemLemma3.5}
Let \A be an elegant Reedy category and \(i : \A → \B\) a functor. Assume that \A has pullbacks along face maps whenever the
cospan under consideration lies in the image of the projection \(B ↓ i → \A\) for some \(B ∈ \B\), and that \(i\) preserves these pullbacks.
Then the left Kan extension \(i_! : \hat{\A} → \hat{\B}\) preserves monomorphisms.
\end{lemma}
\begin{remark}
The original source also requires that these pullbacks preserve face and degeneracy maps. We get around this by making use of the fact
that degeneracies are split in lemma \ref{lem:liftEZFib}
\end{remark}
\begin{proof}
We only need to show that \(i_!\) preserves monomorphisms component wise, giving us a functor from \(\hat{\A} → \Set\) for every
object in \( B ∈\B\). This functor can be written as \todo{argue why stacks project 00VC}
\begin{eqcd*}
\hat{\A} \arrow[r,"p^*"] & \widehat{B ↓ i} \arrow[r,"\colim"] & \Set
\end{eqcd*}
where \(p : B ↓ i → \A\) is the projection.
This is the usual construction of \(i_!\) in this setting, see for example \cite{stacks00VC}.
It is trivial that \(p^*\) preserves monomorphisms, so we only need to check that \(\colim\) does.
We want to apply lemma \ref{lem:idemLemma3.4}
We can lift the elegant Reedy structure from \A to \( B ↓ i \) along \(p\) by lemma \ref{liftReedyToComma}.
And as the face maps in \(B↓i\) are defined as maps that \(p\) sends to face maps in \A. We can lift the
required pullbacks to \(B↓i\) by lemma \ref{commaPullback}.
\end{proof}
\begin{proposition}[{\cite[proposition 3.3]{sattlerIdempotentCompletionCubes2019}}]\label{idemProp3.3}
\(i_! : \hat{Δ} → \widehat{□_{∧∨}}\) preserves monomorphisms.
\end{proposition}
\begin{proof}
We want to verify the conditions for lemma \ref{lem:idemLemma3.5}. Our first observation is, that \(Δ\). Dos not have arbitrary
pullbacks of face maps. Intuitively speaking we have only the non empty ones. So let us unpack the condition that
we only need pullbacks if the cospan of face maps lies in the image of the projection \(B ↓ i → Δ\) for some \(B\).
That means there is a \(B ∈ \FL\) such that
\begin{eqcd*}
{} & B \arrow[rd] \arrow[ld] & \\
i(X) \arrow[rd, "i(f_f)"] & & i(Y) \arrow[ld, "i(g_f)"'] \\
{} & i(Z) &
\end{eqcd*}
As the face maps in \(Δ\) are monic we can identify \(X\) and \(Y\) with their respective image in \(Z\). As \FL does not
contain the empty poset, they share at least a point, and the pullback is given by \(\im f_f ∩ \im g_f\). A quick calculation
shows that this is also a pullback in \FL and thus we can apply lemma \ref{lem:idemLemma3.5}
\end{proof}
\subsection{Step 2}
We are now going to show that \(j^*\) and \(j_!\) are left Quillen. As expected the hard part will be again to show that
\(j_!\) preserves monomorphisms.
So let us start with \(j^*\) again.
\begin{proposition}
\(j^*\) preserves monomorphisms.
\end{proposition}
\begin{proof}
t \todo{trivial}
\end{proof}
\begin{proposition}
\(j^*\) preserves trivial cofibration
\end{proposition}
\begin{proof}
t \todo{same as \(i^*\)}
\end{proof}
\begin{proposition}
\(j^*\) preserves fibrations (bäh)
\end{proposition}
\begin{proof}
t \todo{do i really need todo this?}
\end{proof}
We want to recap the general proof idea, that \(i_!\) preserved monos. We can test being a monomorphism component wise and can write the
left Kan extension evaluated at a point as some mono preserving functor followed by a colimit.
That the colimit preserves monomorphisms is equivalent to a condition of connected on the categories
of elements. As we can only lift morphisms backwards along discrete Grothendieck fibrations, but we are faced
with zigzags. To remedy this we want to lift a strong enough pullback property to turn these zigzags into spans.
This strategy will be the same \(j_!\). Sadly we couldn't get arbitrary Eilenberg-Zilber structures to lift, so
we will need a slightly different attack point.
We first observe that \(□\) has a lot more pullbacks then \(Δ\). While \(Δ\) has only “non empty” pullbacks of face maps
\(□\) has all “non empty" pullbacks. This elevates us from the necessity to lift the Eilenberg-Zilber structure to \(B ↓ i\).
We can get by with the following lemma.
\begin{lemma}\label{lem:pullbackMono}
Let \(i: \A → \B\) be a functor, such that for all \(B ∈ \B\), spans in the image of the projection \(p: B ↓ i\) have pullbacks
in \B, and these pullbacks are in the image of \(i\). Then \(i_!\) preserves monomorphisms.
\end{lemma}
To show this we replace lemma \ref{lem:idemLemma3.4} with the following simpler lemma.
\begin{lemma}\label{lem:colimPullbackMono}
Let \C be a category. Assume \C has pullbacks, then the functor \(\colim : \hat{\C} → \Set\) preserves monomorphisms.
\end{lemma}
\begin{proof}
Again let \(f\) be a monomorphism in \(\hat{\C}\). This is equivalently a monomorphism \(F: P → Q\) of discrete Grothendieck fibrations
over \C. We need to show that \(F\) is injective on connected components. We can lift the pullbacks to \(Q\) by lemma \ref{lem:liftPullbacks}.
Let now \(S\) and \(T\) be in \(Q\) such that \(F(S)\) and \(F(T)\) are connected by a zigzag. We can turn this zigzag into a span, by
taking pullbacks of cospans. Because \(F\) is monic it is injective on object and we can lift this span to a span in \(P\) and thus
\(S\) and \(T\) are in the same connected component.
\end{proof}
\begin{proof}[Proof of lemma \ref{lem:pullbackMono}]
As in lemma \ref{lem:idemLemma3.5}, we check that \(i_!\) preserves monos component wise. We write \(i_!(B)\) again as
\begin{eqcd*}
\hat{\A} \arrow[r, "p^*"] & \widehat{B ↓ i} \arrow[r, "\colim"] & \Set
\end{eqcd*}
where \(p : B ↓ i → A\) is the projection map. We need to show that \(B ↓ i\) has pullbacks, but that is an immediate
consequence of lemma \ref{commaPullback}.
\end{proof}
And we arrive at the conclusion we wanted to get to:
\begin{proposition}
\(j_! : \widehat{\FL} → \□\) preserves monomorphisms.
\end{proposition}
\begin{proof}
For this proof we will identify \(2 = \{⊥,⊤\}\).
We want to fulfill the conditions of \fref{lem:pullbackMono}. To check these conditions we check that equalizer and products
with the desired conditions exist. Products are a straight forward calculation so we go forward to the equalizer case.
To check this we will look at a diagram of the following form.
\begin{eqcd*}[column sep=small]
{} & B \arrow[ld] \arrow[rd] & \\
𝟚^n \arrow[rr, "j(f)", shift left] \arrow[rr, "j(g)"', shift right] & & 𝟚^m
\end{eqcd*}
where we identify \(f\) and \(g\) with functions \(m → n + 2\).
We note that equalizer, if they exist in \FL, are constructed the same way as in \Set.
If we apply this to our diagram we can see, that this construction can't create something empty,
as both maps needs to preserve elements from \(B\).
We would like to complete the diagram in the following way
%\begin{eqcd*}[column sep=large]
\begin{equation*}
\begin{tikzcd}[column sep=large]
{} & B \arrow[dl] \arrow[d] \arrow[dr] & {} \\
𝟚^l \arrow[r,"j(e)"] & 𝟚^n \arrow[r,"j(f)", shift left] \arrow[r,"j(g)"',shift right] & 𝟚^m
\end{tikzcd}
\end{equation*}
So we need to find finite set \(l\) and a map \(e : n → l + 2\). We will construct those by
effectively constructing the coequilizer in \FinSet. So we take the quotient \(\faktor{n+2}{~}\)
where \(~\) is the equivalence relation generated by the relation of having a joint preimage under
\(f\) and \(g\). We will now argue that our equalizer would be empty if this quotient identifies
\(⊤\) and \(⊥\).
We assume that indeed the relation identifies \(⊥\) and \(⊤\), let \(h ∈ 𝟚^n\) such that \(j(f)(h) = j(g)(h)\).
Because \(⊥\) and \(⊤\) are being identified, there exists two finite sequence of elements \(x_i\) and \(y_i\) in \(m\), such that
there exists a \(k\) and
(WLOG) \(f(x_1) = ⊥\), \(g(x_i) = f(y_i)\), \(g(y_i) = f(x_{i+1})\) and \(g(y_k) = ⊤\).
Plugging that into the definition of \(j\) we get
\begin{align*}
⊥ = j(f)(h)(x_1) &= j(g)(h)(x_1) = j(f)(h)(y_1) \\ &= j(g)(h)(y_1) = j(f)(h)(x_2) = … = j(g)(h)(y_k) = ⊤
\end{align*}
which is a contradiction and thus \(⊤\) and \(⊥\) are not identified.
For \(e : n → l + 2\) we take the evident quotient map restricted to \(n\).
While we now have our candidate, we still need to show that this is actually a pushout in \FL. As \FL is well pointed
it suffices to check global elements, which again are just elements in the set theoretic sense.
As \(fe = ge\) by construction and \(j\) is a functor we get \(j(f)j(e) = j(g)j(e)\).
Again let \(h ∈ 𝟚^n\) such that \(j(f)(h) = j(g)(h)\). We can then define
\begin{align*}
h': l → 𝟚 & & h'(x) ≔ h(z) & & z ∈ e^{-1}(x)
\end{align*}
For this definition to make sense we need to argue that the choice of \(z\) does not matter.
So let \(z\) and \(z'\) be both element of \(e^{-1}(x)\). Like above that means there are
two sequences \(x_i\) and \(y_i\) like above, just that \(f(x_1) = z\) and \(g(y_k) = z'\), instead
of \(⊥\) and \(⊤\).
And like above we get
\begin{align*}
h(z) = j(f)(h)(x_1) &= j(g)(h)(x_1) = j(f)(h)(y_1) \\ &= j(g)(h)(y_1) = j(f)(h)(x_2) = … = j(g)(h)(y_k) = h(z')
\end{align*}
We also need that the map \(j(e)\) is monic, but this follows directly from the fact, that \(e\) in \FinSet is epic.
We only need to produce a map \(B → 𝟚^l\), that commutes. We get this map directly, because we have shown that
this diagram is an equalizer in \FL.
This means we fulfill the conditions of \fref{lem:pullbackMono} and thus \(j_!\) preserves monomorphisms.
\end{proof}
\subsection{Step *}
By Ken Browns lemma we now that left Quillen functors preserve weak equivalences between cofibrant objects.
In our setting every object is cofibrant, so all for functors preserve weak equivalences. Thus all for functors
descend to functors of the underlying homotpoy categories.
\subsection{Step 3}
For \(i_!j^*\) and \(i^*j_!\) to be a potential quillen equivalence, they need to adjoint. So we continue by showing that.
To do that we first verify the claim that \(i^*j_!\) is indeed the triangulation functor.
\begin{definition}\label{def:triangulation}
Let \(t: □ → \Δ\) be the functor that sends \([1]^n \mapsto (Δ^1)^n\). The \emph{triangulation functor \(\T\)}
is the left Kan extension of \(t\) along yoneda.
\begin{eqcd*}
□ \arrow[r,"t"] \arrow[d,"\Yo"] & \Δ \\
\□ \arrow[ru,"\T"] &
\end{eqcd*}
\end{definition}
\begin{proposition}\label{prop:triangulation}
The functor \(i^*j_!\) is the triangulation functor.
\end{proposition}
\begin{proof}
As \T is the unique cocontinues functor that extends product preserving functor from □ to \Δ that sends the interval
to the interval, we only need to show these conditions. \(i^*j_!\) is cocontinues as it is the composition of two left
adjoints. We need to show that this functor is product preserving on representables. But by and
\begin{equation*}
j_!(\I^n × \I^m) = j_!(\I^{n+m}) = \Yo 𝟚^{n+m} = \Yo 𝟚^n × \Yo 𝟚^m = j_!(\I^n) × j_!(\I^m)
\end{equation*}
and \(i^*\) is a right adjoint we get this property immediatly. We also need to show that \(i^*j_!\) preserves the interval.
We already know this for \(j_!\). So the question ist if \(i^*\) preserves the interval. We now that \(i^*(\I)(x) =
\Hom_{\dCube}(\Yo [1],i(x))\). As \(i\) is fully faithful the claim follows.
\end{proof}
The main insight from that this adjunction tells us, is that simplicials can't see connections. Or in other word degenerating
a simplex along a connection is the same as degenrating it along a projection. While this is relatively easy to see from
an intuitive standpoint it is a bit tedious to actually show.
\begin{lemma}\label{lem:trianglesDon'tSeeConnections}
We have the following natural bijection
\begin{equation*}
\Hom_{\□}(j^*i_!(Δ^n),\I^m) = \Hom_{\Δ}(Δ^n,i^*j_!(\I^m))
\end{equation*}
\end{lemma}
\begin{proof}
Using that \(j_!\) and \(i_!\) preserve representables by \cref{prop:i_!Nothing,prop:j_!Nothing} , using the yoneda lemma on the right and expand the definition
on the left we get the following.
\begin{equation*}
\Hom_{\□}(\Hom_{\FL}(j(-),[n]),\Hom_□(-,m)) = \Hom_{\FL}([n],𝟚^m)
\end{equation*}
So given a natural transformation \(η : \Hom_{\FL}(j(-),[n]) → \Hom_□(-,n)\), we define \(f: [n] → 𝟚^m\). For this we identify
an element \(x\) of a finite lattice \(Y\) with the monotone map \(x : 𝟚^0 → Y\) sending the one point to \(x\). If we plug
such an \(x\) into \(η_0\), we get a map \(η_0(x) : 0 → m\) in \□, or in other words a function \(m → 2\), which we
can identify with an element of \(𝟚^m\). Monotonicity is witnessed by \(η_1\). Translating \(f\) back to a function
\(η_0\) bijectively is trivial, we only need to show that \(η_0\) already determines all of \(η\). So assume we have
\(η_l\) already defined, we want to define \(η_{l+1}\). We only need to care about non degenerated cells, as these are
already forced by the lower data. For these non degenrate cases there is at most one candidate aligning with the face maps
to lower data. Using monotonicity of \(f\) we can see that these align correctly, and thus we ge a unique \(η\) given \(f\).
\end{proof}
\todo{compute the last part, but that would be at least 3 lemmas and a 2 pages}
\todo{is it true at all? It has to be else everything else is wrong too. But can i map a triangle into a square?
on the right side for sure}
\begin{proposition}\label{prop:adjoints}
\(j^*i_!\) is left adjoint to \(i^*j_!\)
\end{proposition}
\begin{proof}
As we already know that the left adjoint is cocontinuous, we only need to check this for representables in the
left component.
\begin{equation*}
\Hom_{\□}(j^*i_!(Δ^n),B) = \Hom_{\Δ}(Δ^n,i^*j_!(B))
\end{equation*}
We can decomposition \(B\) into a cubical cell complex \cref{??}, a morphism from \(j^*i_!
\end{proof}
\todo{somehow handle that we can get a cell decomposition of \(B\) (cite something?)}
From here on we follow the argument from \cite[§6.2]{solution}.
What we still need to show is that the unit and couint of the adjunction \(i_!j^* ⊣ i^*j_!\) are valued
in weak equivalences.
For this we need a technical Lemma about Eilenberg-Zilber categories. But to make sense of its claim we first need
to introduce a technicality. If we have a category \A and presheafs on it. Then the automorphism group of some
\(a ∈ \A\) acts on \(\Yo a\,b\) by composition. This kind of acting is natural in the sense that \(\Yo a f\) is an
\(\mathrm{Aut}(a)\) equivariant map. Thus we can say \(\mathrm{Aut}(a)\) acts on \(\Yo a\). And thus we can also
quotient \(\Yo a\) by subgroups of \(\mathrm{Aut}(a)\).
\begin{lemma}[{\cites[§5]{riehlTheoryPracticeReedy2014}[lemma 6.2.13]{solution}}]\label{lem:Eilenberg-ZilberMonosCreated}
Let \A be an Eilenberg-Zilber category. Then the monomorphism in \(\hat{\A}\) are generated under
coproduct, pushout, sequential composition, and right cancelation under monomorphisms by the maps
\(­­∅ → \faktor{\Yo a}{H}\) valued in the quotient of a representable presheaf at some \(a ∈ \A\) by an arbitrary
subgroup \(H\) of its automorphism group.
\end{lemma}
\todo{if there is time (lol) proof and explain the theory behind this}
\end{document}

5
src/main/Mainpart.tex Normal file
View file

@ -0,0 +1,5 @@
\documentclass[../Main.tex]{subfiles}
\begin{document}
\subfile{Model_Structure_Argument}
\end{document}

163
src/main/Model_Structure_Argument.tex Normal file
View file

@ -0,0 +1,163 @@
\documentclass[../Main.tex]{subfiles}
\begin{document}
\section{Name TODO}
This arguments from this section follows very closely/This section recalls \cite[section 3]{cavalloRelativeEleganceCartesian2022}, which is
itself a refinment of \cite{sattlerEquivalenceExtensionProperty2017}. We focus a bit more on the arguments that we actually need
and leave out some remarks about the overall theory.
and establishes a nice critereon for a premodel structure beeing a model structure. This excerpt is mainly included in this document
to be more selfcontained.
\begin{definition}[{\cite[Def. 3.1.1]{cavalloRelativeEleganceCartesian2022} \cite[Def. 2.1.23]{bartonModel2CategoryEnriched2019}}]
Let \(\M\) be a finitely complete and cocomplete category. A \emph{premodel structure} on \(\M\) constist of two
weak factorization system \((C,F_t)\) called cofibrations and trivial fibrations and \((C_t,F)\) called
trivial cofibrations and fibrations on \(\M\) such that \(C_t ⊂ C\) and \(F_t ⊂ F\).
\end{definition}
The data that is missig for a real model structure is the set of weak equivalences \(W\) such that \(C,W,F\) gets to
be a model structure. In the case of a model structure \(W\) would already be determined by the other two classes,
giving us an obvious candidate for \(W\)
\begin{definition}[{\cite[Def. 3.1.3]{cavalloRelativeEleganceCartesian2022}}]
A morphism in a premodle structure is a \emph{weak equivalence} if it factors as a trivial cofibration followed
by a trivial fibration. We will call this class \(W(C,F)\).
\end{definition}
One might rightfully ask, what can stop this of beeing a model structure. The good news is, it is only the 2-out-of-3 property.
The other conditions can be shown quite easely
\begin{lemma}[retract argument]\label{retractArgument}\index{retract Argument}
Consider a composite morphism \(f : X \overset{i}{→} A \overset{p}{→} Y\)
Then the following holds
\begin{itemize}
\item If \(f\) has the left lifting property against \(p\), then \(f\) is a rectract of \(i\).
\item If \(f\) has the riht lifting property against \(i\), then \(f\) is a retract of \(p\).
\end{itemize}
\end{lemma}
\begin{proof}
We prove the first statement, the other second one is dual.
We can write the decomposition of \(f\) like in the following square and get a lift \(l\) against \(p\).
\begin{equation*}
\begin{tikzcd}
X \arrow[r,"i"] \arrow[d,"f"] & A \arrow[d,"p"] \\
Y \arrow[r,"\id"] \arrow[ur, dashed, "l"] & Y
\end{tikzcd}
\end{equation*}
Now we can realize \(f\) as a retract as follows.
\begin{equation*}
\begin{tikzcd}
X \arrow[r,"\id"] \arrow[d,"f"] & X \arrow[r,"\id"] \arrow[d,"i"] & X \arrow[d,"f"] \\
Y \arrow[r,"l"] \arrow[rr, bend right, "\id"'] & A \arrow[r, "p"] & Y
\end{tikzcd}
\end{equation*}
\end{proof}
\begin{proposition}[{\cite[Def. 3.1.5]{cavalloRelativeEleganceCartesian2022}}]
\(C_t = C ∩ W(C,F)\) and \(F_t = F ∩ W(C,F)\)
\end{proposition}
\begin{proof}
We are proving the case for trivial cofibrations the other part is analog.
Let \(g ∈ C ∩ W(C,F)\), then \(g\) factors into a trivial cofibration \(c\) followd be a trivial fibration \(f\).
As \(g\) is also a cofibration, \(g\) has the left lifting property against \(f\) and by lemma \ref{retractArgument}
is a retract of the trivial cofibration \(c\). As those are closed under retracts \(g\) is a trivial cofibration too.
The other direction follows from the fact that classes defined by lifting propertys always contain identities.
\end{proof}
We now start to reduce the problem of checking 2-out-of-3. It turns out we do not need to check all possible maps.
\begin{definition}[{\cite[Def. 3.1.7]{cavalloRelativeEleganceCartesian2022}}]
Given a wide subcategory \(\A ⊆ \E\) of a category \(\E\), we say \(\A\) has left cancellation in \(\E\) (or among maps in \(\E\)) when for every
composable pair \(g\), \(f\) in \(\E\), if \(gf\) and \(g\) are in \(\A\) then \(f\) is in \(\A\). Dually, \(\A\) has right cancellation in \(\E\)
when for all \(g\), \(f\) with \(gf\), \(f ∈ \A\), we have \(g ∈ \A\).
\end{definition}
\begin{theorem}[{\cite[Thm 3.1.8]{cavalloRelativeEleganceCartesian2022}}]
\(W(C,F)\) satisfies 2-out-of-3 exactly if the following hold:
\begin{enumerate}
\item[(A)] trivial cofibrations have right cancellation among cofibrations and trivial fibrations have left cancellation among fibrations;
\item[(B)] every (cofibration, trivial fibration) factorization or (trivial cofibration, fibration) factorization of a weak equivalence is
a (trivial cofibration, trival fibration) factorization;
\item[(C)] every composite of a trivial fibration followed by a trivial cofibration is a weak equivalence.
\end{enumerate}
\end{theorem}
\begin{proof}
Assume \(W(C,F)\) satisfies 2-out-of-3. Let us start with (A), let \(g\) and \(f\) be cofibrations such that \(gf\) and \(g\) are trivial.
then by 2-out-of-3 \(f\) is a trivial map too. (The second half of (A) follows in the same way)
Let us investigate (B). Let \(k\) be a weak equivalence, and \(fg\) be a factorization into a trivial cofibration \(g\) followed by a
fibration \(f\). Then by 2-out-of-3 \(f\) is a weak equivalence two. (The second half of (B) is analog)
(C) follows even more directly from 2-out-of-3.
Let us now assume A-C, and let \(g : Y → Z\) and \(f : X → Y\). We can then factor f into a cofibration followed by a trivial fibration
and \(g\) into a trivial cofibraiton followed by a fibration.
\begin{equation*}
\begin{tikzcd}
X \arrow[dr, "f"] \arrow[r, tail] & U \arrow[r, tail, "\sim"] \arrow[d,two heads, "\sim"] & W \arrow[d,two heads,"\sim"] \\
& Y \arrow[dr, "g"] \arrow[r,tail,"\sim"] & V \arrow[d,two heads] \\
& & Z
\end{tikzcd}
\end{equation*}
The maps from and to \(W\) can be obtained by factorizing the composition \(U \overset{\sim}{→} Y \overset{\sim}{→} V\) again and using (B).
Now let us suppose \(f\) and \(g\) are weak equivalences, by (B) the maps from \(X → U\) and \(V → Z\) become weak equivalences too.
Thus the the composition of \(gf\) is a weak equivalence, witnessed by the upper and right side of the diagram.
Now let us assume that \(f\) and \(gf\) are weak equivalences. By (B) the map \(X → U\) gets to be a trivial cofibration again.
Thus the composite \(X → W\) is a trivial cofibration and again by (B) the composite map \(W → Z\) gets to be a trivial fibration,
as these to composites factor \(gf\). By (A) this makes the map \(V → Z\) a trivial fibration. This establishes that \(g\)
factors as a trivial cofibration by a trivial fibration and hence \(g\) is a weak equivalence.
The proof for \(g\) and \(gf\) beeing weak equivalences is dual.
\end{proof}
Now we move on and make use of extra structure that (for example) cubical models exhibit. An adjoint functorial cylinder.
\begin{definition}[{\cite[Def. 3.2.1]{cavalloRelativeEleganceCartesian2022}}]\index{functiorial cylinder}
A \emph{functorial cylinder} on a category \E is a functor \(\I⊗(−): \E → \E \) equipped with \emph{endpoint} and \emph{contraction}
transformations fitting in a diagram as shown:
\begin{equation*}
\begin{tikzcd}[column sep=large, row sep=large]
\Id \arrow[r, dashed, "δ_0⊗(−)"] \arrow[dr, "\id"] & \I⊗(−) \arrow[d,dashed,"ε⊗(−)" description] & \Id \arrow[l,dashed, "δ_1⊗(−)"'] \arrow[dl,"\id"'] \\
& \Id &
\end{tikzcd}
\end{equation*}
An \emph{adjoint functorial cylinder} is a functorial cylinder such that \(\I ⊗ (−) \) is a left adjoint.
The dual notion is called a \emph{functorial path object} consisting of a functor \(\I ⊘ (−)\) and natural
transformation \(δ_k ⊘ (−)\) and \(ε ⊘ (−)\).
\end{definition}
\begin{definition}[{\cite[Def. 3.2.2]{cavalloRelativeEleganceCartesian2022}}]
Given a functiorial cylinder in a cocomplete category, we have a induced \emph{boundary} transformation
\( ∂ ⊗ X ≔ [δ_0 ⊗ X, δ_1 ⊗ X] : X ⊔ X → \I ⊗ X \).
\end{definition}
\begin{definition}[{\cite[Def. 3.2.4]{cavalloRelativeEleganceCartesian2022}}]
Write \(@ : [\E,\Cat{F}] × \E → \Cat{F}\) for the application bifunctor definde by \(F @ X ≔ F(X)\).
Given a category \E with a functorial cylinder and \(f ∈ \E^→\), we abbreviate \((δ_k ⊗ (−)) \hat{@} f : \E^→ → \E^→\)
as \(δ_k\⊗f\). We likewise write \(ε \⊗ f\) for Leibniz application of the contraction. We write \(δ_k \hat{⊘}(−)\) and
\(ε \hat{⊘}(−)\) for the dual operations associated to a functorial path object.
\end{definition}
\begin{definition}[{\cite[Def. 3.2.5]{cavalloRelativeEleganceCartesian2022}}]\index{cylindrical premodel structure}
A \emph{cylindrical premodel structure} on a category \E consists of a premodel structure and adjoint functorial cylinder on
\E that are compatible in the following sense:
\begin{itemize}
\item \(∂ \⊗ (−)\) preserves cofibrations and trivial cofibrations;
\item \(δ_k\⊗(−)\) sends cofibrations to trivial cofibrations for \(k ∈ \{0,1\}\).
\end{itemize}
\end{definition}
TODO Move this to the part about the cube category
\begin{theorem}
\□ has an adjoint functorial cylinder given by \(\I × (-)\) making the premodel structure giving by the weak factorization system
in section \ref{modelStructure}, a cylindrical model structure
\end{theorem}
\begin{proof}
As \□ is a presheaf category and as such cartesian closed, we get \(\I × (−) ⊣ (−)^{\I}\). We also have
\(δ_k⊗(−) ≔ δ_k × (−)\) and \(ε⊗(−) ≔ ε × (−)\). As the cofibrations are just the monomorphisms, it is clear
that \(∂\⊗(−)\) preserves cofibrations.
TODO write out rest (see note cylinder)
\end{proof}
In a cylindrical modelcategory we can
%AFH compositions
%com : (s : I) → (A s)[φ |-> f * s] fst(com r) = fst x_0
%CCHM composition
%com : ( A ε)[φ |-> f * ε]
% see CMS20 (Unifying Cubical Models of Univalent type theory
\end{document}

1
src/main/resource.bib Symbolic link
View file

@ -0,0 +1 @@
../resource.bib

927
src/resource.bib Normal file
View file

@ -0,0 +1,927 @@
@article{ABCHFL,
title = {Syntax and Models of {{Cartesian}} Cubical Type Theory},
author = {Angiuli, Carlo and Brunerie, Guillaume and Coquand, Thierry and Harper, Robert and Hou (Favonia), Kuen-Bang and Licata, Daniel R.},
date = {2021-04},
journaltitle = {Mathematical Structures in Computer Science},
volume = {31},
number = {4},
pages = {424--468},
publisher = {Cambridge University Press},
issn = {0960-1295, 1469-8072},
doi = {10.1017/S0960129521000347},
url = {https://www.cambridge.org/core/journals/mathematical-structures-in-computer-science/article/syntax-and-models-of-cartesian-cubical-type-theory/01B9E98DF997F0861E4BA13A34B72A7D},
urldate = {2023-04-21},
abstract = {We present a cubical type theory based on the Cartesian cube category (faces, degeneracies, symmetries, diagonals, but no connections or reversal) with univalent universes, each containing Π, Σ, path, identity, natural number, boolean, suspension, and glue (equivalence extension) types. The type theory includes a syntactic description of a uniform Kan operation, along with judgmental equality rules defining the Kan operation on each type. The Kan operation uses both a different set of generating trivial cofibrations and a different set of generating cofibrations than the Cohen, Coquand, Huber, and Mörtberg (CCHM) model. Next, we describe a constructive model of this type theory in Cartesian cubical sets. We give a mechanized proof, using Agda as the internal language of cubical sets in the style introduced by Orton and Pitts, that glue, Π, Σ, path, identity, boolean, natural number, suspension types, and the universe itself are Kan in this model, and that the universe is univalent. An advantage of this formal approach is that our construction can also be interpreted in a range of other models, including cubical sets on the connections cube category and the De Morgan cube category, as used in the CCHM model, and bicubical sets, as used in directed type theory.},
langid = {english},
keywords = {ABCHFL,cubical type theory,homotopy type theory,Type theory},
file = {/home/nerf/Zotero/storage/2MPEKIEC/Angiuli et al. - 2021 - Syntax and models of Cartesian cubical type theory.pdf}
}
@inproceedings{angiuliCartesianCubicalComputational2018,
title = {Cartesian {{Cubical Computational Type Theory}}: {{Constructive Reasoning}} with {{Paths}} and {{Equalities}}},
shorttitle = {Cartesian {{Cubical Computational Type Theory}}},
booktitle = {{{DROPS-IDN}}/v2/Document/10.4230/{{LIPIcs}}.{{CSL}}.2018.6},
author = {Angiuli, Carlo and Hou (Favonia), Kuen-Bang and Harper, Robert},
date = {2018},
publisher = {Schloss Dagstuhl – Leibniz-Zentrum für Informatik},
doi = {10.4230/LIPIcs.CSL.2018.6},
url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.6},
urldate = {2024-04-28},
abstract = {We present a dependent type theory organized around a Cartesian notion of cubes (with faces, degeneracies, and diagonals), supporting both fibrant and non-fibrant types. The fibrant fragment validates Voevodsky's univalence axiom and includes a circle type, while the non-fibrant fragment includes exact (strict) equality types satisfying equality reflection. Our type theory is defined by a semantics in cubical partial equivalence relations, and is the first two-level type theory to satisfy the canonicity property: all closed terms of boolean type evaluate to either true or false.},
eventtitle = {27th {{EACSL Annual Conference}} on {{Computer Science Logic}} ({{CSL}} 2018)},
langid = {english},
file = {/home/nerf/Zotero/storage/XTZNK2WW/Angiuli et al. - 2018 - Cartesian Cubical Computational Type Theory Const.pdf}
}
@book{awodeyCategoryTheory2006,
title = {Category {{Theory}}},
author = {Awodey, Steve},
date = {2006-05-25},
publisher = {Oxford University Press},
doi = {10.1093/acprof:oso/9780198568612.001.0001},
url = {https://doi.org/10.1093/acprof:oso/9780198568612.001.0001},
urldate = {2023-09-12},
abstract = {This book is a text and reference book on Category Theory, a branch of abstract algebra. The book contains clear definitions of the essential concepts, which are illuminated with numerous accessible examples. It provides full proofs of all the important propositions and theorems, and aims to make the basic ideas, theorems, and methods of Category Theory understandable. Although it assumes few mathematical pre-requisites, the standard of mathematical rigour is not compromised. The material covered includes the standard core of categories; functors; natural transformations; equivalence; limits and colimits; functor categories; representables; Yoneda's lemma; adjoints; and monads. An extra topic of cartesian closed categories and the lambda-calculus is also provided.},
isbn = {978-0-19-856861-2}
}
@online{awodeyHofmannStreicherUniverses2023,
title = {On {{Hofmann-Streicher}} Universes},
author = {Awodey, Steve},
date = {2023-07-11},
eprint = {2205.10917},
eprinttype = {arXiv},
eprintclass = {math},
doi = {10.48550/arXiv.2205.10917},
url = {http://arxiv.org/abs/2205.10917},
urldate = {2024-07-05},
abstract = {We have another look at the construction by Hofmann and Streicher of a universe \$(U,\{\textbackslash mathsf\{E\}l\})\$ for the interpretation of Martin-L\textbackslash "of type theory in a presheaf category \$\textbackslash psh\{\textbackslash C\}\$. It turns out that \$(U,\{\textbackslash mathsf\{E\}l\})\$ can be described as the \textbackslash emph\{categorical nerve\} of the classifier \$\textbackslash dot\{\textbackslash Set\}\textasciicircum\{\textbackslash mathsf\{op\}\} \textbackslash to \textbackslash op\{\textbackslash Set\}\$ for discrete fibrations in \$\textbackslash Cat\$, where the nerve functor is right adjoint to the so-called ``Grothendieck construction'' taking a presheaf \$P : \textbackslash op\{\textbackslash C\}\textbackslash to\textbackslash Set\$ to its category of elements \$\textbackslash int\_\textbackslash C P\$. We also consider change of base for such universes, as well as universes of structured families, such as fibrations.},
pubstate = {prepublished},
keywords = {Mathematics - Category Theory,Mathematics - Logic},
file = {/home/nerf/Zotero/storage/NIIL8ZAK/Awodey - 2023 - On Hofmann-Streicher universes.pdf;/home/nerf/Zotero/storage/J3DQ66DM/2205.html}
}
@online{awodeyKripkeJoyalForcingType2021,
title = {Kripke-{{Joyal}} Forcing for Type Theory and Uniform Fibrations},
author = {Awodey, S. and Gambino, N. and Hazratpour, S.},
date = {2021-10-27},
eprint = {2110.14576},
eprinttype = {arXiv},
eprintclass = {math},
doi = {10.48550/arXiv.2110.14576},
url = {http://arxiv.org/abs/2110.14576},
urldate = {2024-02-21},
abstract = {We introduce a new method for precisely relating certain kinds of algebraic structures in a presheaf category and judgements of its internal type theory. The method provides a systematic way to organise complex diagrammatic reasoning and generalises the well-known Kripke-Joyal forcing for logic. As an application, we prove several properties of algebraic weak factorisation systems considered in Homotopy Type Theory.},
pubstate = {prepublished},
keywords = {03G30 03B38 18F20 18N45,Mathematics - Category Theory,Mathematics - Logic},
file = {/home/nerf/Zotero/storage/NNQITW4X/Awodey et al. - 2021 - Kripke-Joyal forcing for type theory and uniform f.pdf;/home/nerf/Zotero/storage/M3MTFM97/2110.html}
}
@article{awodeyQuillenModelStructures,
title = {Quillen Model Structures on Cubical Sets},
author = {Awodey, Steve},
pages = {31},
langid = {english},
file = {/home/nerf/Zotero/storage/79HSXCBI/Awodey - Quillen model structures on cubical sets.pdf}
}
@incollection{balchinBisimplicialSets2021,
title = {Bisimplicial {{Sets}}},
booktitle = {A {{Handbook}} of {{Model Categories}}},
author = {Balchin, Scott},
editor = {Balchin, Scott},
date = {2021},
pages = {205--215},
publisher = {Springer International Publishing},
location = {Cham},
doi = {10.1007/978-3-030-75035-0_12},
url = {https://doi.org/10.1007/978-3-030-75035-0_12},
urldate = {2024-04-10},
abstract = {The category of bisimplicial sets is the functor category \$\$\textbackslash mathbf\{Set\} \textasciicircum\{(\textbackslash varDelta \textasciicircum\{op\} \textbackslash times \textbackslash varDelta \textasciicircum\{op\})\}\$\$Set(Δop×Δop), which we denote \$\$\textbackslash mathbf\{ssSet\} \$\$ssSet. Equivalently, \$\$\textbackslash mathbf\{ssSet\} \$\$ssSetis the category of simplicial objects in simplicial sets, i.e., \$\$\textbackslash mathbf\{ssSet\} \textbackslash cong \textbackslash mathbf\{sSet\} \textasciicircum\{\textbackslash varDelta \textasciicircum\{op\}\}\$\$ssSet≅sSetΔop. Under this identification, one could equally call a bisimplicial set a simplicial space.},
isbn = {978-3-030-75035-0},
langid = {english},
file = {/home/nerf/Zotero/storage/3LJ3IU2J/Balchin - 2021 - Bisimplicial Sets.pdf}
}
@article{bartonModel2CategoryEnriched2019,
title = {A {{Model}} 2-{{Category}} of {{Enriched Combinatorial Premodel Categories}}},
author = {Barton, Reid William},
date = {2019-09-10},
issn = {4201-3127},
url = {https://dash.harvard.edu/handle/1/42013127},
urldate = {2024-04-28},
abstract = {Quillen equivalences induce equivalences of homotopy theories and therefore form a natural choice for the "weak equivalences" between model categories. In [21], Hovey asked whether the 2-category Mod of model categories has a "model 2-category structure" with these weak equivalences. We give an example showing that Mod does not have pullbacks, so cannot be a model 2-category. We can try to repair this lack of limits by generalizing the notion of model category. The lack of limits in Mod is due to the two-out-of-three axiom, so we define a premodel category to be a complete and cocomplete category equipped with two nested weak factorization systems. Combinatorial premodel categories form a 2-category CPM with excellent algebraic properties: CPM has all limits and colimits and is equipped with a tensor product (representing Quillen bifunctors) which is adjoint to an internal Hom. The homotopy theory of a model category depends in an essential way on the weak equivalences, so it does not extend directly to premodel categories. We build a substitute homotopy theory under an additional axiom on the premodel category, which holds automatically for a premodel category enriched in a monoidal model category V. The 2-category of combinatorial V-premodel categories VCPM is simply the 2-category of modules over the monoid object V, so VCPM inherits the algebraic structure of CPM. We construct a model 2-category structure on VCPM for V a tractable symmetric monoidal model category, by adapting Szumiło's construction of a fibration category of cofibration categories [35]. For set-theoretic reasons, constructing factorizations for this model 2-category structure requires a technical variant of the small object argument which relies on an analysis of the rank of combinatoriality of a premodel category.},
langid = {english},
annotation = {Accepted: 2019-12-11T10:06:35Z},
file = {/home/nerf/Zotero/storage/ALJR3L7T/Barton - 2019 - A Model 2-Category of Enriched Combinatorial Premo.pdf}
}
@article{bergerExtensionNotionReedy2011,
title = {On an Extension of the Notion of {{Reedy}} Category},
author = {Berger, Clemens and Moerdijk, Ieke},
date = {2011-12},
journaltitle = {Mathematische Zeitschrift},
shortjournal = {Math. Z.},
volume = {269},
number = {3-4},
eprint = {0809.3341},
eprinttype = {arXiv},
pages = {977--1004},
issn = {0025-5874, 1432-1823},
doi = {10.1007/s00209-010-0770-x},
url = {http://arxiv.org/abs/0809.3341},
urldate = {2022-04-26},
abstract = {We extend the classical notion of a Reedy category so as to allow non-trivial automorphisms. Our extension includes many important examples occuring in topology such as Segal's category Gamma, or the total category of a crossed simplicial group such as Connes' cyclic category Lambda. For any generalized Reedy category R and any cofibrantly generated model category E, the functor category E\textasciicircum R is shown to carry a canonical model structure of Reedy type.},
keywords = {18G55 55U35 (Primary) 18G30 20N99 (Secondary),absolute pushouts,Eilenberg-Zilber Category,Mathematics - Algebraic Topology,Mathematics - Category Theory},
file = {/home/nerf/Zotero/storage/9CXJYQ22/Berger and Moerdijk - 2011 - On an extension of the notion of Reedy category.pdf;/home/nerf/Zotero/storage/E9DB6IW2/0809.html}
}
@inproceedings{bezemModelTypeTheory2014,
title = {A {{Model}} of {{Type Theory}} in {{Cubical Sets}}},
author = {Bezem, Marc and Coquand, Thierry and Huber, Simon},
namea = {Herbstritt, Marc},
nameatype = {collaborator},
date = {2014},
pages = {22 pages},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH, Wadern/Saarbruecken, Germany},
doi = {10.4230/LIPICS.TYPES.2013.107},
url = {http://drops.dagstuhl.de/opus/volltexte/2014/4628/},
urldate = {2023-08-28},
abstract = {We present a model of type theory with dependent product, sum, and identity, in cubical sets. We describe a universe and explain how to transform an equivalence between two types into an equality. We also explain how to model propositional truncation and the circle. While not expressed internally in type theory, the model is expressed in a constructive metalogic. Thus it is a step towards a computational interpretation of Voevodsky's Univalence Axiom.},
langid = {english},
keywords = {000 Computer science knowledge general works,Computer Science},
file = {/home/nerf/Zotero/storage/4KKXST7S/Bezem et al. - A model of type theory in cubical sets.pdf}
}
@article{borceuxCauchyCompletionCategory1986,
title = {Cauchy completion in category theory},
author = {Borceux, Francis and Dejean, Dominique},
date = {1986},
journaltitle = {Cahiers de Topologie et Géométrie Différentielle Catégoriques},
volume = {27},
number = {2},
pages = {133--146},
url = {http://www.numdam.org/item/?id=CTGDC_1986__27_2_133_0},
urldate = {2022-08-31},
langid = {french},
file = {/home/nerf/Zotero/storage/K5TFJMSJ/Borceux and Dejean - 1986 - Cauchy completion in category theory.pdf;/home/nerf/Zotero/storage/VQ499FFR/item.html}
}
@article{bourkeAlgebraicWeakFactorisation2016,
title = {Algebraic Weak Factorisation Systems {{I}}: Accessible {{AWFS}}},
shorttitle = {Algebraic Weak Factorisation Systems {{I}}},
author = {Bourke, John and Garner, Richard},
date = {2016-01},
journaltitle = {Journal of Pure and Applied Algebra},
shortjournal = {Journal of Pure and Applied Algebra},
volume = {220},
number = {1},
eprint = {1412.6559},
eprinttype = {arXiv},
pages = {108--147},
issn = {00224049},
doi = {10.1016/j.jpaa.2015.06.002},
url = {http://arxiv.org/abs/1412.6559},
urldate = {2022-04-26},
abstract = {Algebraic weak factorisation systems (AWFS) refine weak factorisation systems by requiring that the assignations sending a map to its first and second factors should underlie an interacting comonad--monad pair on the arrow category. We provide a comprehensive treatment of the basic theory of AWFS---drawing on work of previous authors---and complete the theory with two main new results. The first provides a characterisation of AWFS and their morphisms in terms of their double categories of left or right maps. The second concerns a notion of cofibrant generation of an AWFS by a small double category; it states that, over a locally presentable base, any small double category cofibrantly generates an AWFS, and that the AWFS so arising are precisely those with accessible monad and comonad. Besides the general theory, numerous applications of AWFS are developed, emphasising particularly those aspects which go beyond the non-algebraic situation.},
keywords = {18A32 55U35,Mathematics - Algebraic Topology,Mathematics - Category Theory},
file = {/home/nerf/Zotero/storage/NSWFIVRX/Bourke and Garner - 2016 - Algebraic weak factorisation systems I accessible.pdf;/home/nerf/Zotero/storage/EHWCEUH2/1412.html}
}
@article{bourkeAlgebraicWeakFactorisation2016a,
title = {Algebraic Weak Factorisation Systems {{II}}: Categories of Weak Maps},
shorttitle = {Algebraic Weak Factorisation Systems {{II}}},
author = {Bourke, John and Garner, Richard},
date = {2016-01},
journaltitle = {Journal of Pure and Applied Algebra},
shortjournal = {Journal of Pure and Applied Algebra},
volume = {220},
number = {1},
eprint = {1412.6560},
eprinttype = {arXiv},
pages = {148--174},
issn = {00224049},
doi = {10.1016/j.jpaa.2015.06.003},
url = {http://arxiv.org/abs/1412.6560},
urldate = {2022-04-26},
abstract = {We investigate the categories of weak maps associated to an algebraic weak factorisation system (AWFS) in the sense of Grandis-Tholen. For any AWFS on a category with an initial object, cofibrant replacement forms a comonad, and the category of (left) weak maps associated to the AWFS is by definition the Kleisli category of this comonad. We exhibit categories of weak maps as a kind of "homotopy category", that freely adjoins a section for every "acyclic fibration" (=right map) of the AWFS; and using this characterisation, we give an alternate description of categories of weak maps in terms of spans with left leg an acyclic fibration. We moreover show that the 2-functor sending each AWFS on a suitable category to its cofibrant replacement comonad has a fully faithful right adjoint: so exhibiting the theory of comonads, and dually of monads, as incorporated into the theory of AWFS. We also describe various applications of the general theory: to the generalised sketches of Kinoshita-Power-Takeyama, to the two-dimensional monad theory of Blackwell-Kelly-Power, and to the theory of dg-categories.},
keywords = {18A32 55U35,Mathematics - Algebraic Topology,Mathematics - Category Theory},
file = {/home/nerf/Zotero/storage/PY6J3T45/Bourke and Garner - 2016 - Algebraic weak factorisation systems II categorie.pdf;/home/nerf/Zotero/storage/5R23IT8L/1412.html}
}
@online{castellanCategoriesFamiliesUnityped2020a,
title = {Categories with {{Families}}: {{Unityped}}, {{Simply Typed}}, and {{Dependently Typed}}},
shorttitle = {Categories with {{Families}}},
author = {Castellan, Simon and Clairambault, Pierre and Dybjer, Peter},
date = {2020-07-07},
eprint = {1904.00827},
eprinttype = {arXiv},
eprintclass = {cs},
doi = {10.48550/arXiv.1904.00827},
url = {http://arxiv.org/abs/1904.00827},
urldate = {2023-03-11},
abstract = {We show how the categorical logic of untyped, simply typed and dependently typed lambda calculus can be structured around the notion of category with family (cwf). To this end we introduce subcategories of simply typed cwfs (scwfs), where types do not depend on variables, and unityped cwfs (ucwfs), where there is only one type. We prove several equivalence and biequivalence theorems between cwf-based notions and basic notions of categorical logic, such as cartesian operads, Lawvere theories, categories with finite products and limits, cartesian closed categories, and locally cartesian closed categories. Some of these theorems depend on the restrictions of contextuality (in the sense of Cartmell) or democracy (used by Clairambault and Dybjer for their biequivalence theorems). Some theorems are equivalences between notions with strict preservation of chosen structure. Others are biequivalences between notions where properties are only preserved up to isomorphism. In addition to this we discuss various constructions of initial ucwfs, scwfs, and cwfs with extra structure.},
pubstate = {prepublished},
keywords = {Computer Science - Logic in Computer Science},
file = {/home/nerf/Zotero/storage/D6MP7U8C/Castellan et al. - 2020 - Categories with Families Unityped, Simply Typed, .pdf;/home/nerf/Zotero/storage/9E9C3MVL/1904.html}
}
@online{cavalloRelativeEleganceCartesian2022,
title = {Relative Elegance and Cartesian Cubes with One Connection},
author = {Cavallo, Evan and Sattler, Christian},
date = {2022-11-27},
eprint = {2211.14801},
eprinttype = {arXiv},
eprintclass = {math},
doi = {10.48550/arXiv.2211.14801},
url = {http://arxiv.org/abs/2211.14801},
urldate = {2022-12-16},
abstract = {We establish a Quillen equivalence between the Kan-Quillen model structure and a model structure, derived from a model of a cubical type theory, on the category of cartesian cubical sets with one connection. We thereby identify a second model structure which both constructively models homotopy type theory and presents infinity-groupoids, the first known example being the equivariant cartesian model of Awodey-Cavallo-Coquand-Riehl-Sattler.},
pubstate = {prepublished},
keywords = {Mathematics - Algebraic Topology,Mathematics - Category Theory},
file = {/home/nerf/Zotero/storage/GH8VCM2Q/Cavallo and Sattler - 2022 - Relative elegance and cartesian cubes with one con.pdf;/home/nerf/Zotero/storage/75FUEPL2/2211.html}
}
@article{cavalloUnifyingCubicalModels2016,
title = {Unifying {{Cubical Models}} of {{Univalent Type Theory}}},
author = {Cavallo, Evan and Mörtberg, Anders and Swan, Andrew W},
date = {2016},
langid = {english},
file = {/home/nerf/Zotero/storage/UDTLUHWA/Cavallo et al. - 2016 - Unifying Cubical Models of Univalent Type Theory.pdf}
}
@inproceedings{cavalloUnifyingCubicalModels2020,
title = {Unifying {{Cubical Models}} of {{Univalent Type Theory}}},
booktitle = {28th {{EACSL Annual Conference}} on {{Computer Science Logic}} ({{CSL}} 2020)},
author = {Cavallo, Evan and Mörtberg, Anders and Swan, Andrew W.},
editor = {Fernández, Maribel and Muscholl, Anca},
date = {2020},
series = {Leibniz {{International Proceedings}} in {{Informatics}} ({{LIPIcs}})},
volume = {152},
pages = {14:1--14:17},
publisher = {Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik},
location = {Dagstuhl, Germany},
issn = {1868-8969},
doi = {10.4230/LIPIcs.CSL.2020.14},
url = {https://drops.dagstuhl.de/opus/volltexte/2020/11657},
urldate = {2023-08-23},
isbn = {978-3-95977-132-0},
keywords = {Cubical Set Models,Cubical Type Theory,examples composition structures,Homotopy Type Theory,Univalent Foundations},
file = {/home/nerf/Zotero/storage/HMQ4GBI5/Cavallo et al. - 2020 - Unifying Cubical Models of Univalent Type Theory.pdf;/home/nerf/Zotero/storage/K2D9KNGG/11657.html}
}
@online{CCHM,
title = {Cubical {{Type Theory}}: A Constructive Interpretation of the Univalence Axiom},
shorttitle = {Cubical {{Type Theory}}},
author = {Cohen, Cyril and Coquand, Thierry and Huber, Simon and Mörtberg, Anders},
date = {2016-11-07},
eprint = {1611.02108},
eprinttype = {arXiv},
eprintclass = {cs, math},
doi = {10.48550/arXiv.1611.02108},
url = {http://arxiv.org/abs/1611.02108},
urldate = {2024-03-29},
abstract = {This paper presents a type theory in which it is possible to directly manipulate \$n\$-dimensional cubes (points, lines, squares, cubes, etc.) based on an interpretation of dependent type theory in a cubical set model. This enables new ways to reason about identity types, for instance, function extensionality is directly provable in the system. Further, Voevodsky's univalence axiom is provable in this system. We also explain an extension with some higher inductive types like the circle and propositional truncation. Finally we provide semantics for this cubical type theory in a constructive meta-theory.},
pubstate = {prepublished},
shorthand = {CCHM},
keywords = {CCHM,Computer Science - Logic in Computer Science,de Morgan,F.3.2,F.4.1,Mathematics - Logic},
file = {/home/nerf/Zotero/storage/IPGDN2AH/Cohen et al. - 2016 - Cubical Type Theory a constructive interpretation.pdf;/home/nerf/Zotero/storage/3Q8F527E/1611.html}
}
@unpublished{coquandConstructiveSheafModels2020,
title = {Constructive Sheaf Models of Type Theory},
author = {Coquand, Thierry and Ruch, Fabian and Sattler, Christian},
date = {2020-07-08},
eprint = {1912.10407},
eprinttype = {arXiv},
eprintclass = {math},
url = {http://arxiv.org/abs/1912.10407},
urldate = {2022-04-25},
abstract = {We generalise sheaf models of intuitionistic logic to univalent type theory over a small category with a Grothendieck topology. We use in a crucial way that we have constructive models of univalence, that can then be relativized to any presheaf models, and these sheaf models are obtained by localisation for a left exact modality. We provide first an abstract notion of descent data which can be thought of as a higher version of the notion of prenucleus on frames, from which can be generated a nucleus (left exact modality) by transfinite iteration. We then provide several examples.},
keywords = {Mathematics - Logic},
file = {/home/nerf/Zotero/storage/BM86P38T/Coquand et al. - 2020 - Constructive sheaf models of type theory.pdf;/home/nerf/Zotero/storage/VIMEBY7W/1912.html}
}
@online{coquandVariationCubicalSets2014,
title = {Variation on {{Cubical Sets}}},
author = {Coquand, Thierry},
date = {2014},
url = {https://www.cse.chalmers.se/~coquand/diag.pdf},
urldate = {2024-04-30},
file = {/home/nerf/Zotero/storage/HQBY2TZY/diag.pdf}
}
@online{dohertyCubicalModelsInfty2020,
title = {Cubical Models of \$(\textbackslash infty, 1)\$-Categories},
author = {Doherty, Brandon and Kapulkin, Chris and Lindsey, Zachery and Sattler, Christian},
date = {2020-05-11},
url = {https://arxiv.org/abs/2005.04853v3},
urldate = {2023-08-23},
abstract = {We construct a model structure on the category of cubical sets with connections whose cofibrations are the monomorphisms and whose fibrant objects are defined by the right lifting property with respect to inner open boxes, the cubical analogue of inner horns. We show that this model structure is Quillen equivalent to the Joyal model structure on simplicial sets via the triangulation functor. As an application, we show that cubical quasicategories admit a convenient notion of a mapping space, which we use to characterize the weak equivalences between fibrant objects in our model structure as DK-equivalences.},
langid = {english},
organization = {arXiv.org},
file = {/home/nerf/Zotero/storage/6F6WV5U3/Doherty et al. - 2020 - Cubical models of $(infty, 1)$-categories.pdf}
}
@inproceedings{dybjerInternalTypeTheory2003,
title = {Internal {{Type Theory}}},
author = {Dybjer, Peter},
date = {2003-06-23},
doi = {10.1007/3-540-61780-9_66},
abstract = {We introduce categories with families as a new notion of model for a basic framework of dependent types. This notion is close to ordinary syntax and yet has a clean categorical description. We also present categories with families as a generalized algebraic theory. Then we define categories with families formally in Martin-Lof's intensional intuitionistic type theory. Finally, we discuss the coherence problem for these internal categories with families.},
isbn = {978-3-540-61780-8},
keywords = {CwF,Families},
file = {/home/nerf/Zotero/storage/MKQRDD7X/Dybjer - 2003 - Internal Type Theory.pdf}
}
@unpublished{gambinoConstructiveKanQuillenModel2021,
title = {The Constructive {{Kan-Quillen}} Model Structure: Two New Proofs},
shorttitle = {The Constructive {{Kan-Quillen}} Model Structure},
author = {Gambino, Nicola and Sattler, Christian and Szumiło, Karol},
date = {2021-11-22},
eprint = {1907.05394},
eprinttype = {arXiv},
eprintclass = {math},
url = {http://arxiv.org/abs/1907.05394},
urldate = {2022-04-29},
abstract = {We present two new proofs of Simon Henry's result that the category of simplicial sets admits a constructive counterpart of the classical Kan-Quillen model structure. Our proofs are entirely self-contained and avoid complex combinatorial arguments on anodyne extensions. We also give new constructive proofs of the left and right properness of the model structure.},
keywords = {Mathematics - Algebraic Topology,Mathematics - Category Theory},
file = {/home/nerf/Zotero/storage/G66J48KN/Gambino et al. - 2021 - The constructive Kan-Quillen model structure two .pdf;/home/nerf/Zotero/storage/IQ2BSHPM/1907.html}
}
@unpublished{gambinoEffectiveModelStructure2021,
title = {The Effective Model Structure and \$\textbackslash infty\$-Groupoid Objects},
author = {Gambino, Nicola and Henry, Simon and Sattler, Christian and Szumiło, Karol},
date = {2021-03-10},
eprint = {2102.06146},
eprinttype = {arXiv},
eprintclass = {math},
url = {http://arxiv.org/abs/2102.06146},
urldate = {2022-04-25},
abstract = {For a category \$\textbackslash mathcal E\$ with finite limits and well-behaved countable coproducts, we construct a model structure, called the effective model structure, on the category of simplicial objects in \$\textbackslash mathcal E\$, generalising the Kan--Quillen model structure on simplicial sets. We then prove that the effective model structure is left and right proper and satisfies descent in the sense of Rezk. As a consequence, we obtain that the associated \$\textbackslash infty\$-category has finite limits, colimits satisfying descent, and is locally Cartesian closed when \$\textbackslash mathcal E\$ is, but is not a higher topos in general. We also characterise the \$\textbackslash infty\$-category presented by the effective model structure, showing that it is the full sub-category of presheaves on \$\textbackslash mathcal E\$ spanned by Kan complexes in \$\textbackslash mathcal E\$, a result that suggests a close analogy with the theory of exact completions.},
keywords = {18N40 (primary) 18N60 55U10,Mathematics - Algebraic Topology,Mathematics - Category Theory},
file = {/home/nerf/Zotero/storage/QVGLME2U/Gambino et al. - 2021 - The effective model structure and $infty$-groupoi.pdf;/home/nerf/Zotero/storage/2YSZT8KA/2102.html}
}
@article{gambinoFrobeniusConditionRight2017,
title = {The {{Frobenius Condition}}, {{Right Properness}}, and {{Uniform Fibrations}}},
author = {Gambino, Nicola and Sattler, Christian},
date = {2017-12},
journaltitle = {Journal of Pure and Applied Algebra},
shortjournal = {Journal of Pure and Applied Algebra},
volume = {221},
number = {12},
eprint = {1510.00669},
eprinttype = {arXiv},
pages = {3027--3068},
issn = {00224049},
doi = {10.1016/j.jpaa.2017.02.013},
url = {http://arxiv.org/abs/1510.00669},
urldate = {2022-04-29},
abstract = {We develop further the theory of weak factorization systems and algebraic weak factorization systems. In particular, we give a method for constructing (algebraic) weak factorization systems whose right maps can be thought of as (uniform) fibrations and that satisfy the (functorial) Frobenius condition. As applications, we obtain a new proof that the Quillen model structure for Kan complexes is right proper, avoiding entirely the use of topological realization and minimal fibrations, and we solve an open problem in the study of Voevodsky's simplicial model of type theory, proving a constructive version of the preservation of Kan fibrations by pushforward along Kan fibrations. Our results also subsume and extend work by Coquand and others on cubical sets.},
keywords = {Mathematics - Algebraic Topology,Mathematics - Category Theory,Mathematics - Logic,Unknown Paper?},
file = {/home/nerf/Zotero/storage/SVIAPJW5/Gambino and Sattler - 2017 - The Frobenius Condition, Right Properness, and Uni.pdf;/home/nerf/Zotero/storage/DTMPA7ZW/1510.html;/home/nerf/Zotero/storage/NLPL6A6T/1510.html}
}
@article{garnerUnderstandingSmallObject2009,
title = {Understanding the Small Object Argument},
author = {Garner, Richard},
date = {2009-06},
journaltitle = {Applied Categorical Structures},
shortjournal = {Appl Categor Struct},
volume = {17},
number = {3},
eprint = {0712.0724},
eprinttype = {arXiv},
pages = {247--285},
issn = {0927-2852, 1572-9095},
doi = {10.1007/s10485-008-9137-4},
url = {http://arxiv.org/abs/0712.0724},
urldate = {2022-04-26},
abstract = {The small object argument is a transfinite construction which, starting from a set of maps in a category, generates a weak factorisation system on that category. As useful as it is, the small object argument has some problematic aspects: it possesses no universal property; it does not converge; and it does not seem to be related to other transfinite constructions occurring in categorical algebra. In this paper, we give an "algebraic" refinement of the small object argument, cast in terms of Grandis and Tholen's natural weak factorisation systems, which rectifies each of these three deficiencies.},
keywords = {18A32 55U35,18C10,55U35,Algebraic model structures,Mathematics - Algebraic Topology,Mathematics - Category Theory,Small object argument,Weak factorisation system},
file = {/home/nerf/Zotero/storage/7UVP29D5/Garner - 2009 - Understanding the Small Object Argument.pdf;/home/nerf/Zotero/storage/9V4MZU3G/Garner - 2009 - Understanding the small object argument.pdf;/home/nerf/Zotero/storage/8TPNVUAK/0712.html}
}
@article{grandisNaturalWeakFactorization2006,
title = {Natural Weak Factorization Systems},
author = {Grandis, Marco and Tholen, Walter},
date = {2006-01-01},
journaltitle = {Archivum Mathematicum},
shortjournal = {Archivum Mathematicum},
volume = {42},
abstract = {In order to facilitate a natural choice for morphisms created by the (left or right) lifting property as used in the definition of weak factorization systems, the notion of natural weak factorization system in the category K is introduced, as a pair (comonad, monad) over K 2 . The link with existing notions in terms of morphism classes is given via the respective Eilenberg–Moore categories.},
file = {/home/nerf/Zotero/storage/PKDDLPTE/Grandis and Tholen - 2006 - Natural weak factorization systems.pdf}
}
@online{gratzerStrictUniversesGrothendieck2022,
title = {Strict Universes for {{Grothendieck}} Topoi},
author = {Gratzer, Daniel and Shulman, Michael and Sterling, Jonathan},
date = {2022-03-15},
eprint = {2202.12012},
eprinttype = {arXiv},
eprintclass = {cs, math},
doi = {10.48550/arXiv.2202.12012},
url = {http://arxiv.org/abs/2202.12012},
urldate = {2022-08-31},
abstract = {Hofmann and Streicher famously showed how to lift Grothendieck universes into presheaf topoi, and Streicher has extended their result to the case of sheaf topoi by sheafification. In parallel, van den Berg and Moerdijk have shown in the context of algebraic set theory that similar constructions continue to apply even in weaker metatheories. Unfortunately, sheafification seems not to preserve an important realignment property enjoyed by the presheaf universes that plays a critical role in models of univalent type theory as well as synthetic Tait computability, a recent technique to establish syntactic properties of type theories and programming languages. In the context of multiple universes, the realignment property also implies a coherent choice of codes for connectives at each universe level, thereby interpreting the cumulativity laws present in popular formulations of Martin-L\textbackslash "of type theory. We observe that a slight adjustment to an argument of Shulman constructs a cumulative universe hierarchy satisfying the realignment property at every level in any Grothendieck topos. Hence one has direct-style interpretations of Martin-L\textbackslash "of type theory with cumulative universes into all Grothendieck topoi. A further implication is to extend the reach of recent synthetic methods in the semantics of cubical type theory and the syntactic metatheory of type theory and programming languages to all Grothendieck topoi.},
pubstate = {prepublished},
keywords = {Computer Science - Logic in Computer Science,Mathematics - Category Theory,Mathematics - Logic},
file = {/home/nerf/Zotero/storage/IREIT5EI/Gratzer et al. - 2022 - Strict universes for Grothendieck topoi.pdf;/home/nerf/Zotero/storage/QZ4LQ95R/2202.html}
}
@book{hirschhornModelCategoriesTheir2009,
title = {Model {{Categories}} and {{Their Localizations}}},
author = {Hirschhorn, Philip},
date = {2009-08-24},
series = {Mathematical {{Surveys}} and {{Monographs}}},
volume = {99},
publisher = {American Mathematical Society},
issn = {0076-5376, 2331-7159},
doi = {10.1090/surv/099},
url = {https://www.ams.org/surv/099},
urldate = {2023-09-12},
abstract = {Advancing research. Creating connections.},
isbn = {978-0-8218-4917-0 978-1-4704-1326-2},
langid = {english}
}
@article{hofmannDoctorPhilosophyUniversity,
title = {Doctor of {{Philosophy University}} of {{Edinburgh}} 1995},
author = {Hofmann, Martin},
langid = {english},
file = {/home/nerf/Zotero/storage/VKM9TK2D/Hofmann - Doctor of Philosophy University of Edinburgh 1995.pdf}
}
@article{hofmannSyntaxSemanticsDependent,
title = {Syntax and {{Semantics}} of {{Dependent Types}}},
author = {Hofmann, Martin},
langid = {english},
keywords = {CwF,Families,Presheaf model},
file = {/home/nerf/Zotero/storage/NY2W23FP/Hofmann - Syntax and Semantics of Dependent Types.pdf}
}
@online{hoveyModelCategories2007,
title = {Model {{Categories}}},
author = {Hovey, Mark},
date = {2007-10-17},
series = {Mathematical {{Surveys}} and {{Monographs}}},
volume = {63},
publisher = {American Mathematical Society},
issn = {0076-5376, 2331-7159},
doi = {10.1090/surv/063},
url = {https://www.ams.org/surv/063},
urldate = {2024-04-28},
abstract = {Advancing research. Creating connections.},
isbn = {9780821843611 9781470412906},
langid = {english},
organization = {American Mathematical Society}
}
@online{IntroductionHomotopyTheory,
title = {Introduction to {{Homotopy Theory}} in {{nLab}}},
url = {https://ncatlab.org/nlab/show/Introduction+to+Homotopy+Theory},
urldate = {2023-09-12},
file = {/home/nerf/Zotero/storage/77QL5DY8/Introduction+to+Homotopy+Theory.html}
}
@unpublished{isaacsonSymmetricCubicalSets2009,
title = {Symmetric {{Cubical Sets}}},
author = {Isaacson, Samuel B.},
date = {2009-10-26},
eprint = {0910.4948},
eprinttype = {arXiv},
eprintclass = {math},
url = {http://arxiv.org/abs/0910.4948},
urldate = {2022-04-26},
abstract = {We introduce a new cubical model for homotopy types. More precisely, we'll define a category Qs with the following features: Qs is a PROP containing the classical box category as a subcategory, the category Qs-Set of presheaves of sets on Qs models the homotopy category, and combinatorial symmetric monoidal model categories with cofibrant unit all have homotopically well behaved Qs-Set enrichments.},
keywords = {55u35,Mathematics - Algebraic Topology,Mathematics - Category Theory},
file = {/home/nerf/Zotero/storage/QGG5W5Q5/Isaacson - 2009 - Symmetric Cubical Sets.pdf;/home/nerf/Zotero/storage/ZN3NRQN4/0910.html}
}
@book{jacobsCategoricalLogicType1999,
title = {Categorical Logic and Type Theory},
author = {Jacobs, Bart},
date = {1999},
series = {Studies in Logic and the Foundations of Mathematics},
edition = {1st ed},
number = {v. 141},
publisher = {Elsevier Science},
location = {Amsterdam ; New York},
isbn = {978-0-444-50170-7},
langid = {english},
pagetotal = {760},
keywords = {Categories (Mathematics),Type theory},
file = {/home/nerf/Zotero/storage/BKE5ASHQ/Jacobs - 1999 - Categorical logic and type theory.pdf}
}
@inbook{lawvereAlgebraicProblemsContext1968,
title = {Some Algebraic Problems in the Context of Functorial Semantics of Algebraic Theories},
booktitle = {Reports of the {{Midwest Category Seminar II}}},
author = {Lawvere, F. William},
editor = {MacLane, S.},
date = {1968},
volume = {61},
pages = {41--61},
publisher = {Springer Berlin Heidelberg},
location = {Berlin, Heidelberg},
doi = {10.1007/BFb0077116},
url = {http://link.springer.com/10.1007/BFb0077116},
urldate = {2023-11-13},
bookauthor = {André, M. and Buchsbaum, D. A. and Dubuc, E. and Knighten, R. L. and Lawvere, F. W.},
isbn = {978-3-540-04231-0 978-3-540-35863-3},
langid = {english},
file = {/home/nerf/Zotero/storage/QMR75KQ6/Lawvere - 1968 - Some algebraic problems in the context of functori.pdf}
}
@article{lawvereFUNCTORIALSEMANTICSALGEBRAIC1963,
title = {{{FUNCTORIAL SEMANTICS OF ALGEBRAIC THEORIES}}},
author = {Lawvere, F. William},
date = {1963-11},
journaltitle = {Proceedings of the National Academy of Sciences},
shortjournal = {Proc. Natl. Acad. Sci. U.S.A.},
volume = {50},
number = {5},
pages = {869--872},
issn = {0027-8424, 1091-6490},
doi = {10.1073/pnas.50.5.869},
url = {https://pnas.org/doi/full/10.1073/pnas.50.5.869},
urldate = {2023-11-13},
langid = {english},
file = {/home/nerf/Zotero/storage/ECTRWE4B/Lawvere - 1963 - FUNCTORIAL SEMANTICS OF ALGEBRAIC THEORIES.pdf}
}
@unpublished{LOPS,
title = {Internal {{Universes}} in {{Models}} of {{Homotopy Type Theory}}},
author = {Licata, Daniel R. and Orton, Ian and Pitts, Andrew M. and Spitters, Bas},
date = {2018},
eprint = {1801.07664},
eprinttype = {arXiv},
eprintclass = {cs},
pages = {17 pages},
doi = {10.4230/LIPIcs.FSCD.2018.22},
url = {http://arxiv.org/abs/1801.07664},
urldate = {2022-05-11},
abstract = {We begin by recalling the essentially global character of universes in various models of homotopy type theory, which prevents a straightforward axiomatization of their properties using the internal language of the presheaf toposes from which these model are constructed. We get around this problem by extending the internal language with a modal operator for expressing properties of global elements. In this setting we show how to construct a universe that classifies the Cohen-Coquand-Huber-M\textbackslash "ortberg (CCHM) notion of fibration from their cubical sets model, starting from the assumption that the interval is tiny - a property that the interval in cubical sets does indeed have. This leads to an elementary axiomatization of that and related models of homotopy type theory within what we call crisp type theory.},
shorthand = {LOPS},
version = {2},
keywords = {Computer Science - Logic in Computer Science,F.3.2,F.4.1,LOPS,Tiny},
file = {/home/nerf/Zotero/storage/58IRMAVX/Licata et al. - 2018 - Internal Universes in Models of Homotopy Type Theo.pdf;/home/nerf/Zotero/storage/9H5DEUV7/1801.html}
}
@book{maclaneCategoriesWorkingMathematician1978,
title = {Categories for the {{Working Mathematician}}},
author = {Mac Lane, Saunders},
date = {1978},
series = {Graduate {{Texts}} in {{Mathematics}}},
volume = {5},
publisher = {Springer},
location = {New York, NY},
doi = {10.1007/978-1-4757-4721-8},
url = {http://link.springer.com/10.1007/978-1-4757-4721-8},
urldate = {2023-09-12},
isbn = {978-1-4419-3123-8 978-1-4757-4721-8},
keywords = {addition,Adjoint functor,algebra,Morphism,theorem},
file = {/home/nerf/Zotero/storage/LCQ4M4Q8/Mac Lane - 1978 - Categories for the Working Mathematician.pdf}
}
@book{maclaneSheavesGeometryLogic1994,
title = {Sheaves in {{Geometry}} and {{Logic}}: {{A First Introduction}} to {{Topos Theory}}},
shorttitle = {Sheaves in {{Geometry}} and {{Logic}}},
author = {Mac Lane, Saunders and Moerdijk, Ieke},
date = {1994},
series = {Universitext},
publisher = {Springer},
location = {New York, NY},
doi = {10.1007/978-1-4612-0927-0},
url = {https://link.springer.com/10.1007/978-1-4612-0927-0},
urldate = {2023-09-12},
isbn = {978-0-387-97710-2 978-1-4612-0927-0},
langid = {english},
keywords = {Algebraic structure,Boolean algebra,Division,forcing,Heyting algebra,set,set theory},
file = {/home/nerf/Zotero/storage/W58HYMXM/Mac Lane and Moerdijk - 1994 - Sheaves in Geometry and Logic A First Introductio.pdf}
}
@online{NCategoryCafe,
title = {The N-{{Category Café}}},
url = {https://golem.ph.utexas.edu/category/2015/06/what_is_a_reedy_category.html},
urldate = {2024-04-10},
langid = {english},
file = {/home/nerf/Zotero/storage/FG4SPDSM/what_is_a_reedy_category.html}
}
@unpublished{ortonAxiomsModellingCubical2018,
title = {Axioms for {{Modelling Cubical Type Theory}} in a {{Topos}}},
author = {Orton, Ian and Pitts, Andrew M.},
date = {2018-12-08},
eprint = {1712.04864},
eprinttype = {arXiv},
eprintclass = {cs},
doi = {10.23638/LMCS-14(4:23)2018},
url = {http://arxiv.org/abs/1712.04864},
urldate = {2022-05-11},
abstract = {The homotopical approach to intensional type theory views proofs of equality as paths. We explore what is required of an object \$I\$ in a topos to give such a path-based model of type theory in which paths are just functions with domain \$I\$. Cohen, Coquand, Huber and M\textbackslash "ortberg give such a model using a particular category of presheaves. We investigate the extent to which their model construction can be expressed in the internal type theory of any topos and identify a collection of quite weak axioms for this purpose. This clarifies the definition and properties of the notion of uniform Kan filling that lies at the heart of their constructive interpretation of Voevodsky's univalence axiom. (This paper is a revised and expanded version of a paper of the same name that appeared in the proceedings of the 25th EACSL Annual Conference on Computer Science Logic, CSL 2016.)},
keywords = {Computer Science - Logic in Computer Science,F.4.1},
file = {/home/nerf/Zotero/storage/IPQSVWQ9/Orton and Pitts - 2018 - Axioms for Modelling Cubical Type Theory in a Topo.pdf;/home/nerf/Zotero/storage/KRK2SGUB/1712.html}
}
@book{quillenHomotopicalAlgebra1967,
title = {Homotopical {{Algebra}}},
author = {Quillen, Daniel G.},
editor = {Dold, A. and Eckmann, B.},
editortype = {redactor},
date = {1967},
series = {Lecture {{Notes}} in {{Mathematics}}},
volume = {43},
publisher = {Springer},
location = {Berlin, Heidelberg},
doi = {10.1007/BFb0097438},
url = {http://link.springer.com/10.1007/BFb0097438},
urldate = {2022-04-27},
isbn = {978-3-540-03914-3 978-3-540-35523-6},
keywords = {algebra,homotopical algebra,Homotopie,homotopy,homotopy theory,Quillen},
file = {/home/nerf/Zotero/storage/JG33WVEZ/Quillen - 1967 - Homotopical Algebra.pdf}
}
@unpublished{riehlAlgebraicModelStructures2011,
title = {Algebraic Model Structures},
author = {Riehl, Emily},
date = {2011-03-11},
eprint = {0910.2733},
eprinttype = {arXiv},
eprintclass = {math},
url = {http://arxiv.org/abs/0910.2733},
urldate = {2022-04-26},
abstract = {We define a new notion of an algebraic model structure, in which the cofibrations and fibrations are retracts of coalgebras for comonads and algebras for monads, and prove "algebraic" analogs of classical results. Using a modified version of Quillen's small object argument, we show that every cofibrantly generated model structure in the usual sense underlies a cofibrantly generated algebraic model structure. We show how to pass a cofibrantly generated algebraic model structure across an adjunction, and we characterize the algebraic Quillen adjunction that results. We prove that pointwise natural weak factorization systems on diagram categories are cofibrantly generated if the original ones are, and we give an algebraic generalization of the projective model structure. Finally, we prove that certain fundamental comparison maps present in any cofibrantly generated model category are cofibrations when the cofibrations are monomorphisms, a conclusion that does not seem to be provable in the classical, non-algebraic, theory.},
keywords = {55U35 18A32,Mathematics - Algebraic Topology,Mathematics - Category Theory},
file = {/home/nerf/Zotero/storage/7748DLXS/Riehl - 2011 - Algebraic model structures.pdf;/home/nerf/Zotero/storage/5TLYJVHI/0910.html}
}
@book{riehlCategoricalHomotopyTheory2014,
title = {Categorical {{Homotopy Theory}}},
author = {Riehl, Emily},
date = {2014},
series = {New {{Mathematical Monographs}}},
publisher = {Cambridge University Press},
location = {Cambridge},
doi = {10.1017/CBO9781107261457},
url = {https://www.cambridge.org/core/books/categorical-homotopy-theory/556C7A200B521E61466BB7763C49DDA4},
urldate = {2023-07-07},
abstract = {This book develops abstract homotopy theory from the categorical perspective with a particular focus on examples. Part I discusses two competing perspectives by which one typically first encounters homotopy (co)limits: either as derived functors definable when the appropriate diagram categories admit a compatible model structure, or through particular formulae that give the right notion in certain examples. Emily Riehl unifies these seemingly rival perspectives and demonstrates that model structures on diagram categories are irrelevant. Homotopy (co)limits are explained to be a special case of weighted (co)limits, a foundational topic in enriched category theory. In Part II, Riehl further examines this topic, separating categorical arguments from homotopical ones. Part III treats the most ubiquitous axiomatic framework for homotopy theory - Quillen's model categories. Here, Riehl simplifies familiar model categorical lemmas and definitions by focusing on weak factorization systems. Part IV introduces quasi-categories and homotopy coherence.},
isbn = {978-1-107-04845-4},
file = {/home/nerf/Zotero/storage/NEXTFSKD/Riehl - Categorical homotopy theory.pdf;/home/nerf/Zotero/storage/IJYSYMC6/556C7A200B521E61466BB7763C49DDA4.html}
}
@article{riehlCategoryTheoryContext,
title = {Category Theory in Context},
author = {Riehl, Emily},
langid = {english},
file = {/home/nerf/Zotero/storage/4WNNYCP7/Riehl - Category theory in context.pdf}
}
@article{riehlINDUCTIVEPRESENTATIONSGENERALIZED,
title = {{{INDUCTIVE PRESENTATIONS OF GENERALIZED REEDY CATEGORIES}}},
author = {Riehl, Emily},
abstract = {This note explores the algebraic perspective on the notion of generalized Reedy category introduced by Berger and Moerdijk [BM08]. The aim is to unify inductive arguments by means of a canonical presentation of the hom bifunctor as a “generalized cell complex.” This is analogous to the weighted (co)limits approach to strict Reedy category theory presented in [RV14], which inspired this work. These presentations are used to prove that various functors associated to categories of Reedy-indexed diagrams are “derived” preserving pointwise weak equivalences between appropriately fibrant or cofibrant diagrams.},
langid = {english},
file = {/home/nerf/Zotero/storage/2CCAMCEM/Riehl - INDUCTIVE PRESENTATIONS OF GENERALIZED REEDY CATEG.pdf}
}
@article{riehlINDUCTIVEPRESENTATIONSGENERALIZEDa,
title = {{{INDUCTIVE PRESENTATIONS OF GENERALIZED REEDY CATEGORIES}}},
author = {Riehl, Emily},
abstract = {This note explores the algebraic perspective on the notion of generalized Reedy category introduced by Berger and Moerdijk [BM08]. The aim is to unify inductive arguments by means of a canonical presentation of the hom bifunctor as a “generalized cell complex.” This is analogous to the weighted (co)limits approach to strict Reedy category theory presented in [RV14], which inspired this work. These presentations are used to prove that various functors associated to categories of Reedy-indexed diagrams are “derived” preserving pointwise weak equivalences between appropriately fibrant or cofibrant diagrams.},
langid = {english},
file = {/home/nerf/Zotero/storage/6G7N6N5U/Riehl - INDUCTIVE PRESENTATIONS OF GENERALIZED REEDY CATEG.pdf}
}
@incollection{riehlMadetoOrderWeakFactorization2015a,
title = {Made-to-{{Order Weak Factorization Systems}}},
booktitle = {Extended {{Abstracts Fall}} 2013},
author = {Riehl, Emily},
editor = {González, Maria Del Mar and Yang, Paul C. and Gambino, Nicola and Kock, Joachim},
date = {2015},
pages = {87--92},
publisher = {Springer International Publishing},
location = {Cham},
doi = {10.1007/978-3-319-21284-5_17},
url = {https://link.springer.com/10.1007/978-3-319-21284-5_17},
urldate = {2024-04-15},
isbn = {978-3-319-21283-8 978-3-319-21284-5},
langid = {english},
file = {/home/nerf/Zotero/storage/PN8KT9LC/Riehl - 2015 - Made-to-Order Weak Factorization Systems.pdf}
}
@online{riehlTheoryPracticeReedy2014,
title = {The Theory and Practice of {{Reedy}} Categories},
author = {Riehl, Emily and Verity, Dominic},
date = {2014-06-03},
eprint = {1304.6871},
eprinttype = {arXiv},
eprintclass = {math},
doi = {10.48550/arXiv.1304.6871},
url = {http://arxiv.org/abs/1304.6871},
urldate = {2024-04-07},
abstract = {The goal of this paper is to demystify the role played by the Reedy category axioms in homotopy theory. With no assumed prerequisites beyond a healthy appetite for category theoretic arguments, we present streamlined proofs of a number of useful technical results, which are well known to folklore but difficult to find in the literature. While the results presented here are not new, our approach to their proofs is somewhat novel. Specifically, we reduce the much of the hard work involved to simpler computations involving weighted colimits and Leibniz (pushout-product) constructions. The general theory is developed in parallel with examples, which we use to prove that familiar formulae for homotopy limits and colimits indeed have the desired properties.},
pubstate = {prepublished},
keywords = {55U35 18G30 18D10,Mathematics - Algebraic Topology,Mathematics - Category Theory},
file = {/home/nerf/Zotero/storage/ME8UH6X7/Riehl and Verity - 2014 - The theory and practice of Reedy categories.pdf;/home/nerf/Zotero/storage/TU3Y2293/1304.html}
}
@article{riehlTOPOSSEMANTICSHOMOTOPY,
title = {{{ON THE}} ∞-{{TOPOS SEMANTICS OF HOMOTOPY TYPE THEORY}}},
author = {Riehl, Emily},
pages = {37},
abstract = {Many introductions to homotopy type theory and the univalence axiom neglect to explain what any of it means, glossing over the semantics of this new formal system in traditional set-based foundations. This series of talks will attempt to survey the state of the art, first presenting Voevodsky’s simplicial model of univalent foundations and then touring Shulman’s vast generalization, which provides an interpretation of homotopy type theory with strict univalent universes in any ∞-topos. As we will explain, this achievement was the product of a community effort to abstract and streamline the original arguments as well as develop new lines of reasoning.},
langid = {english},
file = {/home/nerf/Zotero/storage/UA9ZRJ5Y/Riehl - ON THE ∞-TOPOS SEMANTICS OF HOMOTOPY TYPE THEORY.pdf}
}
@online{riehlTypeTheorySynthetic2023,
title = {A Type Theory for Synthetic \$\textbackslash infty\$-Categories},
author = {Riehl, Emily and Shulman, Michael},
date = {2023-06-08},
eprint = {1705.07442},
eprinttype = {arXiv},
eprintclass = {math},
doi = {10.48550/arXiv.1705.07442},
url = {http://arxiv.org/abs/1705.07442},
urldate = {2024-05-30},
abstract = {We propose foundations for a synthetic theory of \$(\textbackslash infty,1)\$-categories within homotopy type theory. We axiomatize a directed interval type, then define higher simplices from it and use them to probe the internal categorical structures of arbitrary types. We define Segal types, in which binary composites exist uniquely up to homotopy; this automatically ensures composition is coherently associative and unital at all dimensions. We define Rezk types, in which the categorical isomorphisms are additionally equivalent to the type-theoretic identities - a "local univalence" condition. And we define covariant fibrations, which are type families varying functorially over a Segal type, and prove a "dependent Yoneda lemma" that can be viewed as a directed form of the usual elimination rule for identity types. We conclude by studying homotopically correct adjunctions between Segal types, and showing that for a functor between Rezk types to have an adjoint is a mere proposition. To make the bookkeeping in such proofs manageable, we use a three-layered type theory with shapes, whose contexts are extended by polytopes within directed cubes, which can be abstracted over using "extension types" that generalize the path-types of cubical type theory. In an appendix, we describe the motivating semantics in the Reedy model structure on bisimplicial sets, in which our Segal and Rezk types correspond to Segal spaces and complete Segal spaces.},
pubstate = {prepublished},
keywords = {03G30 18G55 55U40,Mathematics - Category Theory,Mathematics - Logic},
file = {/home/nerf/Zotero/storage/6MQM9TWA/Riehl and Shulman - 2023 - A type theory for synthetic $infty$-categories.pdf;/home/nerf/Zotero/storage/H3UW42V3/1705.html}
}
@video{riehlVid,
entrysubtype = {video},
title = {The {{Equivariant Uniform Kan Fibration Model}} of {{Cubical Homotopy Type Theory}} - {{YouTube}}},
editor = {Riehl, Emily},
editortype = {director},
date = {2020-05-26},
url = {https://www.youtube.com/watch?v=A8tEwxM7uxE},
urldate = {2022-06-19},
abstract = {Dr Emily Riehl Johns Hopkins University},
file = {/home/nerf/Zotero/storage/SYCCCLDV/watch.html}
}
@online{rileyTypeTheoryTiny2024,
title = {A {{Type Theory}} with a {{Tiny Object}}},
author = {Riley, Mitchell},
date = {2024-03-04},
eprint = {2403.01939},
eprinttype = {arXiv},
eprintclass = {cs, math},
doi = {10.48550/arXiv.2403.01939},
url = {http://arxiv.org/abs/2403.01939},
urldate = {2024-03-12},
abstract = {We present an extension of Martin-L\textbackslash "of Type Theory that contains a tiny object; a type for which there is a right adjoint to the formation of function types as well as the expected left adjoint. We demonstrate the practicality of this type theory by proving various properties related to tininess internally and suggest a few potential applications.},
pubstate = {prepublished},
keywords = {Computer Science - Programming Languages,Mathematics - Category Theory,Mathematics - Logic},
file = {/home/nerf/Zotero/storage/DM45P9J4/Riley - 2024 - A Type Theory with a Tiny Object.pdf;/home/nerf/Zotero/storage/8KAP7SMU/2403.html}
}
@article{sattlerCYLINDRICALMODELSTRUCTURES,
title = {{{CYLINDRICAL MODEL STRUCTURES}}},
author = {Sattler, Christian},
url = {https://www.cse.chalmers.se/~sattler/docs/interval-model-structure.pdf},
langid = {english},
file = {/home/nerf/Zotero/storage/G9NTWNAY/Sattler - CYLINDRICAL MODEL STRUCTURES.pdf}
}
@online{sattlerEquivalenceExtensionProperty2017,
title = {The {{Equivalence Extension Property}} and {{Model Structures}}},
author = {Sattler, Christian},
date = {2017-04-23},
url = {https://arxiv.org/abs/1704.06911v4},
urldate = {2023-08-23},
abstract = {We give an elementary construction of a certain class of model structures. In particular, we rederive the Kan model structure on simplicial sets without the use of topological spaces, minimal complexes, or any concrete model of fibrant replacement such as Kan's Ex\textasciicircum infinity functor. Our argument makes crucial use of the glueing construction developed by Cohen et al. in the specific setting of certain cubical sets.},
langid = {english},
pubstate = {prepublished},
keywords = {Mathematics - Algebraic Topology,Mathematics - Category Theory,Mathematics - Logic,The unknown Paper?},
file = {/home/nerf/Zotero/storage/GFLT3HLU/Sattler - 2017 - The Equivalence Extension Property and Model Struc.pdf;/home/nerf/Zotero/storage/FDPHZXNP/1704.html;/home/nerf/Zotero/storage/SEADD4R7/1704.html}
}
@online{sattlerIdempotentCompletionCubes2019,
title = {Idempotent Completion of Cubes in Posets},
author = {Sattler, Christian},
date = {2019-03-08},
eprint = {1805.04126},
eprinttype = {arXiv},
eprintclass = {math},
doi = {10.48550/arXiv.1805.04126},
url = {http://arxiv.org/abs/1805.04126},
urldate = {2023-08-23},
abstract = {This note concerns the category \$\textbackslash Box\$ of cartesian cubes with connections, equivalently the full subcategory of posets on objects \$[1]\textasciicircum n\$ with \$n \textbackslash geq 0\$. We show that the idempotent completion of \$\textbackslash Box\$ consists of finite complete posets. It follows that cubical sets, ie presheaves over \$\textbackslash Box\$, are equivalent to presheaves over finite complete posets. This yields an alternative exposition of a result by Kapulkin and Voevodsky that simplicial sets form a subtopos of cubical sets.},
pubstate = {prepublished},
keywords = {Mathematics - Category Theory},
file = {/home/nerf/Zotero/storage/SYH7C9JV/Sattler - 2019 - Idempotent completion of cubes in posets.pdf;/home/nerf/Zotero/storage/9ZN8RBCZ/1805.html}
}
@online{shulmanAllInftyToposes2019,
title = {All \$(\textbackslash infty,1)\$-Toposes Have Strict Univalent Universes},
author = {Shulman, Michael},
date = {2019-04-26},
eprint = {1904.07004},
eprinttype = {arXiv},
eprintclass = {math},
doi = {10.48550/arXiv.1904.07004},
url = {http://arxiv.org/abs/1904.07004},
urldate = {2024-07-23},
abstract = {We prove the conjecture that any Grothendieck \$(\textbackslash infty,1)\$-topos can be presented by a Quillen model category that interprets homotopy type theory with strict univalent universes. Thus, homotopy type theory can be used as a formal language for reasoning internally to \$(\textbackslash infty,1)\$-toposes, just as higher-order logic is used for 1-toposes. As part of the proof, we give a new, more explicit, characterization of the fibrations in injective model structures on presheaf categories. In particular, we show that they generalize the coflexible algebras of 2-monad theory.},
pubstate = {prepublished},
keywords = {Mathematics - Algebraic Topology,Mathematics - Category Theory},
file = {/home/nerf/Zotero/storage/STEZIS8H/Shulman - 2019 - All $(infty,1)$-toposes have strict univalent uni.pdf;/home/nerf/Zotero/storage/XZQ93HPD/1904.html}
}
@article{shulmanREEDYCATEGORIESTHEIR,
title = {{{REEDY CATEGORIES AND THEIR GENERALIZATIONS}}},
author = {Shulman, Michael},
abstract = {We observe that the Reedy model structure on a diagram category can be constructed by iterating an operation of “bigluing” model structures along a pair of functors and a natural transformation. This yields a new explanation of the definition of Reedy categories: they are almost exactly those small categories for which the category of diagrams and its model structure can be constructed by iterated bigluing. It also gives a consistent way to produce generalizations of Reedy categories, including the generalized Reedy categories of Cisinski and Berger–Moerdijk and the enriched Reedy categories of Angeltveit, but also new versions such as a combined notion of “enriched generalized Reedy category”.},
langid = {english},
file = {/home/nerf/Zotero/storage/BMRJ6NMU/Shulman - REEDY CATEGORIES AND THEIR GENERALIZATIONS.pdf}
}
@online{solution,
title = {The Equivariant Model Structure on Cartesian Cubical Sets},
author = {Awodey, Steve and Cavallo, Evan and Coquand, Thierry and Riehl, Emily and Sattler, Christian},
date = {2024-06-26},
eprint = {2406.18497},
eprinttype = {arXiv},
eprintclass = {cs, math},
doi = {10.48550/arXiv.2406.18497},
url = {http://arxiv.org/abs/2406.18497},
urldate = {2024-07-03},
abstract = {We develop a constructive model of homotopy type theory in a Quillen model category that classically presents the usual homotopy theory of spaces. Our model is based on presheaves over the cartesian cube category, a well-behaved Eilenberg-Zilber category. The key innovation is an additional equivariance condition in the specification of the cubical Kan fibrations, which can be described as the pullback of an interval-based class of uniform fibrations in the category of symmetric sequences of cubical sets. The main technical results in the development of our model have been formalized in a computer proof assistant.},
pubstate = {prepublished},
shorthand = {ACCRS},
keywords = {Computer Science - Logic in Computer Science,Mathematics - Algebraic Topology,Mathematics - Logic},
file = {/home/nerf/Zotero/storage/AKJBUSV6/Awodey et al. - 2024 - The equivariant model structure on cartesian cubic.pdf;/home/nerf/Zotero/storage/ZD7WA4UC/2406.html}
}
@inreference{stacks00VC,
title = {The {{Stacks}} Project},
author = {The \{Stacks project authors\}},
url = {https://stacks.math.columbia.edu/tag/00VC}
}
@book{streicherSemanticsTypeTheory1991,
title = {Semantics of {{Type Theory}}},
author = {Streicher, Thomas},
date = {1991},
publisher = {Birkhäuser Boston},
location = {Boston, MA},
doi = {10.1007/978-1-4612-0433-6},
url = {http://link.springer.com/10.1007/978-1-4612-0433-6},
urldate = {2023-09-02},
isbn = {978-1-4612-6757-7 978-1-4612-0433-6},
langid = {english},
file = {/home/nerf/Zotero/storage/ALA3AMGY/Streicher - 1991 - Semantics of Type Theory.pdf}
}
@article{streicherSimplicialSetsCubical2021,
title = {Simplicial Sets inside Cubical Sets},
author = {Streicher, Thomas and Weinberger, Jonathan},
date = {2021-03-15},
journaltitle = {Theory and Applications of Categories},
volume = {37},
number = {10},
pages = {276--286},
url = {http://www.tac.mta.ca/tac/volumes/37/10/37-10abs.html},
urldate = {2024-05-02},
file = {/home/nerf/Zotero/storage/DSG2FX6B/Streicher and Weinberger - 2021 - Simplicial sets inside cubical sets.pdf}
}
@incollection{streicherUNIVERSESTOPOSES2005,
title = {{{UNIVERSES IN TOPOSES}}},
booktitle = {From {{Sets}} and {{Types}} to {{Topology}} and {{Analysis}}},
author = {Streicher, Thomas},
editor = {Crosilla, Laura and Schuster, Peter},
date = {2005-10-06},
edition = {1},
pages = {78--90},
publisher = {Oxford University PressOxford},
doi = {10.1093/acprof:oso/9780198566519.003.0005},
url = {https://academic.oup.com/book/5354/chapter/148144921},
urldate = {2023-11-14},
abstract = {We discuss a notion of universe in toposes which from a logical point of view gives rise to an extension of Higher Order Intuitionistic Arithmetic (HAH) that allows one to construct families of types in such a universe by structural recursion and to quantify over such families. Further, we show that (hierarchies of) such universes do exist in all sheaf and realizability toposes but neither in the free topos nor in the Vω+ω model of Zermelo set theory.},
isbn = {978-0-19-856651-9 978-0-19-171392-7},
langid = {english},
file = {/home/nerf/Zotero/storage/CB5TH6EV/Streicher - 2005 - UNIVERSES IN TOPOSES.pdf}
}
@online{swanDefinableNondefinableNotions2022,
title = {Definable and {{Non-definable Notions}} of {{Structure}}},
author = {Swan, Andrew W.},
date = {2022-06-27},
eprint = {2206.13643},
eprinttype = {arXiv},
eprintclass = {cs, math},
doi = {10.48550/arXiv.2206.13643},
url = {http://arxiv.org/abs/2206.13643},
urldate = {2024-03-11},
abstract = {Definability is a key notion in the theory of Grothendieck fibrations that characterises when an external property of objects can be accessed from within the internal logic of the base of a fibration. In this paper we consider a generalisation of definability from properties of objects to structures on objects, introduced by Shulman under the name local representability. We first develop some general theory and show how to recover existing notions due to B\textbackslash '\{e\}nabou and Johnstone as special cases. We give several examples of definable and non definable notions o structure, focusing on algebraic weak factorisation systems, which can be naturally viewed as notions of structure on codomain fibrations. Regarding definability, we give a sufficient criterion for cofibrantly generated awfs's to be definable, generalising a construction of the universe for cubical sets, but also including some very different looking examples that do not satisfy tininess in the internal sense, that exponential functors have a right adjoint. Our examples of non definability include the identification of logical principles holding for the interval objects in simplicial sets and Bezem-Coquand-Huber cubical sets that suffice to show a certain definition of Kan fibration is not definable.},
pubstate = {prepublished},
keywords = {03G30 18N40,Computer Science - Logic in Computer Science,Mathematics - Category Theory,Mathematics - Logic},
file = {/home/nerf/Zotero/storage/CJRDB5DU/Swan - 2022 - Definable and Non-definable Notions of Structure.pdf;/home/nerf/Zotero/storage/DS7C3TKZ/2206.html}
}

1
src/result Symbolic link
View file

@ -0,0 +1 @@
/nix/store/vi5k8nsgp9knk76bri7p6nr1la5fa4mn-output.pdf