Merge branch 'dev'

This commit is contained in:
Frederik Hanghøj Iversen 2018-05-08 18:35:45 +02:00
commit a181cfb63e
54 changed files with 5031 additions and 1928 deletions

1
.gitignore vendored
View file

@ -1 +0,0 @@
references/

View file

@ -1,21 +1,12 @@
Backlog
=======
Prove postulates in `Cat.Wishlist`:
* `ntypeCommulative : n ≤ m → HasLevel ⟨ n ⟩₋₂ A → HasLevel ⟨ m ⟩₋₂ A`
Prove that these two formulations of univalence are equivalent:
∀ A B → isEquiv (A ≡ B) (A ≅ B) (id-to-iso A B)
∀ A → isContr (Σ[ X ∈ Object ] A ≅ X)
Prove univalence for the category of
* the opposite category
* functors and natural transformations
Prove:
* `isProp (Product ...)`
* `isProp (HasProducts ...)`
In AreInverses, dont use the "point-free" version. I.e.:
`∀ x → f x ≡ g x` rather than `f ≡ g`
Ideas for future work
---------------------

View file

@ -1,6 +1,32 @@
Changelog
Change log
=========
Version 1.5.0
-------------
Prove postulates in `Cat.Wishlist`:
* `ntypeCommulative : n ≤ m → HasLevel ⟨ n ⟩₋₂ A → HasLevel ⟨ m ⟩₋₂ A`
Prove that these two formulations of univalence are equivalent:
∀ A B → isEquiv (A ≡ B) (A ≅ B) (id-to-iso A B)
∀ A → isContr (Σ[ X ∈ Object ] A ≅ X)
Prove univalence for the category of...
* the opposite category
* sets
* "pair" category
Finish the proof that products are propositional:
* `isProp (Product ...)`
* `isProp (HasProducts ...)`
Remove --allow-unsolved-metas pragma from various files
Also renamed a lot of different projections. E.g. arrow-composition, etc..
Version 1.4.1
-------------
Defines a module to work with equivalence providing a way to go between
@ -29,12 +55,12 @@ Adds an "equality principle" for categories and monads.
Prove that `IsMonad` is a mere proposition.
Provides the yoneda embedding without relying on the existence of a category of
categories. This is acheived by providing some of the data needed to make a ccc
categories. This is achieved by providing some of the data needed to make a ccc
out of the category of categories without actually having such a category.
Renames functors object map and arrow map to `omap` and `fmap`.
Prove that kleisli- and monoidal- monads are equivalent!
Prove that Kleisli- and monoidal- monads are equivalent!
[WIP] Started working on the proofs for univalence for the category of sets and
the category of functors.
@ -42,7 +68,7 @@ the category of functors.
Version 1.3.0
-------------
Removed unused modules and streamlined things more: All specific categories are
in the namespace `Cat.Categories`.
in the name space `Cat.Categories`.
Lemmas about categories are now in the appropriate record e.g. `IsCategory`.
Also changed how category reexports stuff.
@ -53,7 +79,7 @@ Rename Opposite to opposite
Add documentation in Category-module
Formulation of monads in two ways; the "monoidal-" and "kleisli-" form.
Formulation of monads in two ways; the "monoidal-" and "Kleisli-" form.
WIP: Equivalence of these two formulations

View file

@ -6,3 +6,4 @@
*.pdf
*.bbl
*.blg
*.toc

7
doc/BACKLOG.md Normal file
View file

@ -0,0 +1,7 @@
Talk about structure of library:
===
What can I say about reusability?
Misc
====

View file

@ -3,17 +3,21 @@
# Originally from : http://tex.stackexchange.com/a/40759
#
# Change only the variable below to the name of the main tex file.
PROJNAME=proposal
PROJNAME=univalent-categories
MAIN=main.tex
# You want latexmk to *always* run, because make does not have all the info.
# Also, include non-file targets in .PHONY so they are run regardless of any
# file of the given name existing.
.PHONY: $(PROJNAME).pdf all clean
.PHONY: $(PROJNAME).pdf all clean preview
# The first rule in a Makefile is the one executed by default ("make"). It
# should always be the "all" rule, so that "make" and "make all" are identical.
all: $(PROJNAME).pdf
preview: $(MAIN)
latexmk -pvc -jobname=$(PROJNAME) -pdf -xelatex $<
# CUSTOM BUILD RULES
# In case you didn't know, '$@' is a variable holding the name of the target,
@ -36,8 +40,8 @@ all: $(PROJNAME).pdf
# -interactive=nonstopmode keeps the pdflatex backend from stopping at a
# missing file reference and interactively asking you for an alternative.
$(PROJNAME).pdf: $(PROJNAME).tex
latexmk -pdf -pdflatex="pdflatex -interactive=nonstopmode" -use-make $<
$(PROJNAME).pdf: $(MAIN)
latexmk -jobname=$(PROJNAME) -pdf -xelatex -use-make $<
cleanall:
latexmk -C

37
doc/appendix.tex Normal file
View file

@ -0,0 +1,37 @@
\lstset{basicstyle=\footnotesize\ttfamily,breaklines=true,breakpages=true}
\def\fileps
{ ../src/Cat.agda
, ../src/Cat/Categories/Cat.agda
, ../src/Cat/Categories/Cube.agda
, ../src/Cat/Categories/CwF.agda
, ../src/Cat/Categories/Fam.agda
, ../src/Cat/Categories/Free.agda
, ../src/Cat/Categories/Fun.agda
, ../src/Cat/Categories/Rel.agda
, ../src/Cat/Categories/Sets.agda
, ../src/Cat/Category.agda
, ../src/Cat/Category/CartesianClosed.agda
, ../src/Cat/Category/Exponential.agda
, ../src/Cat/Category/Functor.agda
, ../src/Cat/Category/Monad.agda
, ../src/Cat/Category/Monad/Kleisli.agda
, ../src/Cat/Category/Monad/Monoidal.agda
, ../src/Cat/Category/Monad/Voevodsky.agda
, ../src/Cat/Category/Monoid.agda
, ../src/Cat/Category/NaturalTransformation.agda
, ../src/Cat/Category/Product.agda
, ../src/Cat/Category/Yoneda.agda
, ../src/Cat/Equivalence.agda
, ../src/Cat/Prelude.agda
}
\foreach \filep in \fileps {
\chapter{\filep}
%% \begin{figure}[htpb]
\lstinputlisting{\filep}
%% \caption{Source code for \texttt{\filep}}
%% \label{fig:\filep}
%% \end{figure}
}
%% \lstset{framextopmargin=50pt}
%% \lstinputlisting{../../src/Cat.agda}

135
doc/chalmerstitle.sty Normal file
View file

@ -0,0 +1,135 @@
% Requires: hypperref
\ProvidesPackage{chalmerstitle}
%% \RequirePackage{kvoptions}
%% \SetupKeyvalOptions{
%% family=ct,
%% prefix=ct@
%% }
%% \DeclareStringOption{authoremail}
%% \DeclareStringOption{supervisor}
%% \DeclareStringOption{supervisoremail}
%% \DeclareStringOption{supervisordepartment}
%% \DeclareStringOption{cosupervisor}
%% \DeclareStringOption{cosupervisoremail}
%% \DeclareStringOption{cosupervisordepartment}
%% \DeclareStringOption{examiner}
%% \DeclareStringOption{examineremail}
%% \DeclareStringOption{examinerdepartment}
%% \DeclareStringOption{institution}
%% \DeclareStringOption{department}
%% \DeclareStringOption{researchgroup}
%% \DeclareStringOption{subtitle}
%% \ProcessKeyvalOptions*
\newcommand*{\authoremail}[1]{\gdef\@authoremail{#1}}
\newcommand*{\supervisor}[1]{\gdef\@supervisor{#1}}
\newcommand*{\supervisoremail}[1]{\gdef\@supervisoremail{#1}}
\newcommand*{\supervisordepartment}[1]{\gdef\@supervisordepartment{#1}}
\newcommand*{\cosupervisor}[1]{\gdef\@cosupervisor{#1}}
\newcommand*{\cosupervisoremail}[1]{\gdef\@cosupervisoremail{#1}}
\newcommand*{\cosupervisordepartment}[1]{\gdef\@cosupervisordepartment{#1}}
\newcommand*{\examiner}[1]{\gdef\@examiner{#1}}
\newcommand*{\examineremail}[1]{\gdef\@examineremail{#1}}
\newcommand*{\examinerdepartment}[1]{\gdef\@examinerdepartment{#1}}
\newcommand*{\institution}[1]{\gdef\@institution{#1}}
\newcommand*{\department}[1]{\gdef\@department{#1}}
\newcommand*{\researchgroup}[1]{\gdef\@researchgroup{#1}}
\newcommand*{\subtitle}[1]{\gdef\@subtitle{#1}}
%% FRONTMATTER
\newcommand*{\myfrontmatter}{%
\newgeometry{top=3cm, bottom=3cm,left=2.25 cm, right=2.25cm}
\begingroup
\thispagestyle{empty}
{\Huge\@title}\\[.5cm]
{\Large A formalization of category theory in Cubical Agda}\\[2.5cm]
\begin{center}
\includegraphics[width=\linewidth,keepaspectratio]{isomorphism.png}
\end{center}
% Cover text
\vfill
%% \renewcommand{\familydefault}{\sfdefault} \normalfont % Set cover page font
{\Large\@author}\\[.5cm]
Master's thesis in Computer Science
\endgroup
%% \end{titlepage}
% BACK OF COVER PAGE (BLANK PAGE)
\newpage
%% \newgeometry{a4paper} % Temporarily change margins
%% \restoregeometry
\thispagestyle{empty}
\null
}
\renewcommand*{\maketitle}{%
\begin{titlepage}
% TITLE PAGE
\newpage
\thispagestyle{empty}
\begin{center}
\textsc{\LARGE Master's thesis \the\year}\\[4cm] % Report number is currently not in use
\textbf{\LARGE \@title} \\[1cm]
{\large \@subtitle}\\[1cm]
{\large \@author}
\vfill
\centering
\includegraphics[width=0.2\pdfpagewidth]{logo_eng.pdf}
\vspace{5mm}
\textsc{Department of Computer Science and Engineering}\\
\textsc{{\@researchgroup}}\\
%Name of research group (if applicable)\\
\textsc{\@institution} \\
\textsc{Gothenburg, Sweden \the\year}\\
\end{center}
% IMPRINT PAGE (BACK OF TITLE PAGE)
\newpage
\thispagestyle{plain}
\textit{\@title}\\
\@subtitle\\
\copyright\ \the\year ~ \textsc{\@author}
\vspace{4.5cm}
\setlength{\parskip}{0.5cm}
\textbf{Author:}\\
\@author\\
\href{mailto:\@authoremail>}{\texttt{<\@authoremail>}}
\textbf{Supervisor:}\\
\@supervisor\\
\href{mailto:\@supervisoremail>}{\texttt{<\@supervisoremail>}}\\
\@supervisordepartment
\textbf{Co-supervisor:}\\
\@cosupervisor\\
\href{mailto:\@cosupervisoremail>}{\texttt{<\@cosupervisoremail>}}\\
\@cosupervisordepartment
\textbf{Examiner:}\\
\@examiner\\
\href{mailto:\@examineremail>}{\texttt{<\@examineremail>}}\\
\@examinerdepartment
\vfill
Master's Thesis \the\year\\ % Report number currently not in use
\@department\\
%Division of Division name\\
%Name of research group (if applicable)\\
\@institution\\
SE-412 96 Gothenburg\\
Telephone +46 31 772 1000 \setlength{\parskip}{0.5cm}\\
% Caption for cover page figure if used, possibly with reference to further information in the report
%% Cover: Wind visualization constructed in Matlab showing a surface of constant wind speed along with streamlines of the flow. \setlength{\parskip}{0.5cm}
%Printed by [Name of printing company]\\
Gothenburg, Sweden \the\year
\restoregeometry
\end{titlepage}}

3
doc/conclusion.tex Normal file
View file

@ -0,0 +1,3 @@
\chapter{Conclusion}
\TODO{\ldots}

286
doc/cubical.tex Normal file
View file

@ -0,0 +1,286 @@
\chapter{Cubical Agda}
\section{Propositional equality}
In Agda judgmental equality is a feature of the type-system. It's a property of
types that can be checked by computational means. In the example from the
introduction $n + 0$ can be judged to be equal to $n$ simply by expanding the
definition of $+$.
Propositional equality on the other hand is defined within the language itself.
Cubical Agda extends the underlying type system (\TODO{Cite someone smarter than
me with a good resource on this}) but introduces a data-type within the
languages.
Exceprts of the source code relevant to this section can be found in appendix
\ref{sec:app-cubical}.
\subsection{The equality type}
The usual notion of judgmental equality says that given a type $A \tp \MCU$ and
two points of $A$; $a_0, a_1 \tp A$ we can form the type:
%
\begin{align}
a_0 \equiv a_1 \tp \MCU
\end{align}
%
In Agda this is defined as an inductive data-type with the single constructor:
%
\begin{align}
\refl \tp a \equiv a
\end{align}
%
For any $a \tp A$.
There also exist a related notion of \emph{heterogeneous} equality where allows
for equating points of different types. In this case given two types $A, B \tp
\MCU$ and two points $a \tp A$, $b \tp B$ we can construct the type:
%
\begin{align}
a \cong b \tp \MCU
\end{align}
%
This is likewise defined as an inductive data-type with a single constructors:
%
\begin{align}
\refl \tp a \cong a
\end{align}
%
In Cubical Agda these two notions are paralleled with homogeneous- and
heterogeneous paths respectively.
%
\subsection{The path type}
In Cubical Agda judgmental equality is encapsulated with the type:
%
$$
\Path \tp (P \tp I → \MCU) → P\ 0 → P\ 1 → \MCU
$$
%
$I$ is a special data-type (\TODO{that also has special computational properties
AFAIK}) called the index set. $I$ can be thought of simply as the interval on
the real numbers from $0$ to $1$. $P$ is a family of types over the index set
$I$. I will sometimes refer to $P$ as the ``path-space'' of some path $p \tp
\Path\ P\ a\ b$. By this token $P\ 0$ then corresponds to the type at the
left-endpoint and $P\ 1$ as the type at the right-endpoint. The type is called
$\Path$ because it is connected with paths in homotopy theory. The intuition
behind this is that $\Path$ describes paths in $\MCU$ -- i.e. between types. For
a path $p$ for the point $p\ i$ the index $i$ describes how far along the path
one has moved. An inhabitant of $\Path\ P\ a_0\ a_1$ is a (dependent-)
function, $p$, from the index-space to the path-space:
%
$$
p \tp I \to P\ i
$$
%
Which must satisfy being judgmentally equal to $a_0$ (respectively $a_1$) at the
endpoints. I.e.:
%
\begin{align*}
p\ 0 & = a_0 \\
p\ 1 & = a_1
\end{align*}
%
The notion of ``homogeneous equalities'' can be recovered by not letting the
path-space $P$ depend on it's argument:
%
$$
a_0 \equiv a_1 \defeq \Path\ (\lambda i \to A)\ a_0\ a_1
$$
%
For $A \tp \MCU$, $a_0, a_1 \tp A$. I will generally prefer to use the notation
$a_0 \equiv a_1$ when talking about non-dependent paths and use the notation
$\Path\ (\lambda i \to A)\ a_0\ a_1$ when the path-space is of particular
interest.
With this definition we can also recover reflexivity. That is, for any $A \tp
\MCU$ and $a \tp A$:
%
\begin{equation}
\begin{aligned}
\refl & \tp \Path (\lambda i \to A)\ a\ a \\
\refl & \defeq \lambda i \to a
\end{aligned}
\end{equation}
%
Or, in other terms; reflexivity is the path in $A$ that is $a$ at the left
endpoint as well as at the right endpoint. It is inhabited by the path which
stays constantly at $a$ at any index $i$.
Paths have some other important properties, but they are not the focus of this
thesis. \TODO{Refer the reader somewhere for more info.}
%
\section{Homotopy levels}
In ITT all equality proofs are identical (in a closed context). This means that,
in some sense, any two inhabitants of $a \equiv b$ are ``equally good'' -- they
don't have any interesting structure. This is referred to as uniqueness of
identity proofs. Unfortunately this is orthogonal to univalence that only makes
sense in the absence of UIP.
In homotopy type theory we have a hierarchy of types based on their ``internal
structure''. At the bottom of this hierarchy we have the set of contractible
types:
%
\begin{equation}
\begin{aligned}
%% \begin{split}
& \isContr && \tp \MCU \to \MCU \\
& \isContr\ A && \defeq \sum_{c \tp A} \prod_{a \tp A} a \equiv c
%% \end{split}
\end{aligned}
\end{equation}
%
The first component of $\isContr\ A$ is called ``the center of contraction''.
Under the propositions-as-types interpretation of type-theory $\isContr\ A$ can
be thought of as ``the true proposition $A$''. It is a theorem that if a type is
contractible, then it is isomorphic to the unit-type $\top$.
The next step in the hierarchy is the set of mere propositions:
%
\begin{equation}
\begin{aligned}
& \isProp && \tp \MCU \to \MCU \\
& \isProp\ A && \defeq \prod_{a_0, a_1 \tp A} a_0 \equiv a_1
\end{aligned}
\end{equation}
%
$\isProp\ A$ can be thought of as the set of true and false propositions. It is
a result that if a mere proposition $A$ is inhabited, then so is it
contractible. If it is not inhabited it is equivalent to the empty-type (or
false proposition).\TODO{Cite!!}
I will refer to a type $A \tp \MCU$ as a \emph{mere} proposition if I want to
stress that we have $\isProp\ A$.
Then comes the set of homotopical sets:
%
\begin{equation}
\begin{aligned}
& \isSet && \tp \MCU \to \MCU \\
& \isSet\ A && \defeq \prod_{a_0, a_1 \tp A} \isProp\ (a_0 \equiv a_1)
\end{aligned}
\end{equation}
%
At this point it should be noted that the term ``set'' is somewhat conflated;
there is the notion of sets from set-theory, in Agda types are denoted
\texttt{Set}. I will use it consistently to refer to a type $A$ as a set exactly
if $\isSet\ A$ is inhabited.
The next step in the hierarchy is, as the reader might've guessed, the type:
%
\begin{equation}
\begin{aligned}
& \isGroupoid && \tp \MCU \to \MCU \\
& \isGroupoid\ A && \defeq \prod_{a_0, a_1 \tp A} \isSet\ (a_0 \equiv a_1)
\end{aligned}
\end{equation}
%
And so it continues. In fact we can generalize this family of types by indexing
them with a natural number. For historical reasons, though, the bottom of the
hierarchy, the contractible types, is said to be a \nomen{-2-type}, propositions
are \nomen{-1-types}, (homotopical) sets are \nomen{0-types} and so on\ldots
Just as with paths, homotopical sets are not at the center of focus for this
thesis. But I mention here some properties that will be relevant for this
exposition:
Proposition: Homotopy levels are cumulative. That is, if $A \tp \MCU$ has
homotopy level $n$ then so does it have $n + 1$.
Let $\left\Vert A \right\Vert = n$ denote that the level of $A$ is $n$.
Proposition: For any homotopic level $n$ this is a mere proposition.
%
\section{A few lemmas}
Rather than getting into the nitty-gritty details of Agda I venture to take a
more ``combinator-based'' approach. That is, I will use theorems about paths
already that have already been formalized. Specifically the results come from
the Agda library \texttt{cubical} (\TODO{Cite}). I have used a handful of
results from this library as well as contributed a few lemmas myself.\footnote{The module \texttt{Cat.Prelude} lists the upstream dependencies. As well my contribution to \texttt{cubical} can be found in the git logs \TODO{Cite}.}
These theorems are all purely related to homotopy theory and cubical Agda and as
such not specific to the formalization of Category Theory. I will present a few
of these theorems here, as they will be used later in chapter
\ref{ch:implementation} throughout.
\subsection{Path induction}
\label{sec:pathJ}
The induction principle for paths intuitively gives us a way to reason about a
type-family indexed by a path by only considering if said path is $\refl$ (the
``base-case''). For \emph{based path induction}, that equality is \emph{based}
at some element $a \tp A$.
Let a type $A \tp \MCU$ and an element of the type $a \tp A$ be given. $a$ is said to be the base of the induction. Given a family of types:
%
$$
P \tp \prod_{a' \tp A} \prod_{p \tp a ≡ a'} \MCU
$$
%
And an inhabitant of $P$ at $\refl$:
%
$$
p \tp P\ a\ \refl
$$
%
We have the function:
%
$$
\pathJ\ P\ p \tp \prod_{a' \tp A} \prod_{p \tp a ≡ a'} P\ a\ p
$$
%
\subsection{Paths over propositions}
\label{sec:lemPropF}
Another very useful combinator is $\lemPropF$:
To `promote' this to a dependent path we can use another useful combinator;
$\lemPropF$. Given a type $A \tp \MCU$ and a type family on $A$; $P \tp A \to
\MCU$. Let $\var{propP} \tp \prod_{x \tp A} \isProp\ (P\ x)$ be the proof that
$P$ is a mere proposition for all elements of $A$. Furthermore say we have a
path between some two elements in $A$; $p \tp a_0 \equiv a_1$ then we can built
a heterogeneous path between any two elements of $p_0 \tp P\ a_0$ and $p_1 \tp
P\ a_1$:
%
$$
\lemPropF\ \var{propP}\ p \defeq \Path\ (\lambda\; i \mto P\ (p\ i))\ p_0\ p_1
$$
%
This is quite a mouthful. So let me try to show how this is a very general and
useful result.
Often when proving equalities between elements of some dependent types
$\lemPropF$ can be used to boil this complexity down to showing that the
dependent parts of the type are mere propositions. For instance, saw we have a type:
%
$$
T \defeq \sum_{a \tp A} P\ a
$$
%
For some proposition $P \tp A \to \MCU$. If we want to prove $t_0 \equiv t_1$
for two elements $t_0, t_1 \tp T$ then this will be a pair of paths:
%
%
\begin{align*}
p \tp & \fst\ t_0 \equiv \fst\ t_1 \\
& \Path\ (\lambda i \to P\ (p\ i))\ \snd\ t_0 \equiv \snd\ t_1
\end{align*}
%
Here $\lemPropF$ directly allow us to prove the latter of these:
%
$$
\lemPropF\ \var{propP}\ p
\tp \Path\ (\lambda i \to P\ (p\ i))\ \snd\ t_0 \equiv \snd\ t_1
$$
%
\subsection{Functions over propositions}
\label{sec:propPi}
$\prod$-types preserve propositionality when the co-domain is always a
proposition.
%
$$
\mathit{propPi} \tp \left(\prod_{a \tp A} \isProp\ (P\ a)\right) \to \isProp\ \left(\prod_{a \tp A} P\ a\right)
$$
\subsection{Pairs over propositions}
\label{sec:propSig}
%
$\sum$-types preserve propositionality whenever it's first component is a
proposition, and it's second component is a proposition for all points of in the
left type.
%
$$
\mathit{propSig} \tp \isProp\ A \to \left(\prod_{a \tp A} \isProp\ (P\ a)\right) \to \isProp\ \left(\sum_{a \tp A} P\ a\right)
$$

74
doc/discussion.tex Normal file
View file

@ -0,0 +1,74 @@
\chapter{Perspectives}
\section{Discussion}
In the previous chapter the practical aspects of proving things in Cubical Agda
were highlighted. I also demonstrated the usefulness of separating ``laws'' from
``data''. One of the reasons for this is that dependencies within types can lead
to very complicated goals. One technique for alleviating this was to prove that
certain types are mere propositions.
\subsection{Computational properties}
Another aspect (\TODO{That I actually didn't highlight very well in the previous
chapter}) is the computational nature of paths. Say we have formalized this
common result about monads:
\TODO{Some equation\ldots}
By transporting this to the Kleisli formulation we get a result that we can use
to compute with. This is particularly useful because the Kleisli formulation
will be more familiar to programmers e.g. those coming from a background in
Haskell. Whereas the theory usually talks about monoidal monads.
\TODO{Mention that with postulates we cannot do this}
\subsection{Reusability of proofs}
The previous example also illustrate how univalence unifies two otherwise
disparate areas: The category-theoretic study of monads; and monads as in
functional programming. Univalence thus allows one to reuse proofs. You could
say that univalence gives the developer two proofs for the price of one.
The introduction (section \ref{sec:context}) mentioned an often
employed-technique for enabling extensional equalities is to use the
setoid-interpretation. Nowhere in this formalization has this been necessary,
$\Path$ has been used globally in the project as propositional equality. One
interesting place where this becomes apparent is in interfacing with the Agda
standard library. Multiple definitions in the Agda standard library have been
designed with the setoid-interpretation in mind. E.g. the notion of ``unique
existential'' is indexed by a relation that should play the role of
propositional equality. Likewise for equivalence relations, they are indexed,
not only by the actual equivalence relation, but also by another relation that
serve as propositional equality.
%% Unfortunately we cannot use the definition of equivalences found in the
%% standard library to do equational reasoning directly. The reason for this is
%% that the equivalence relation defined there must be a homogenous relation,
%% but paths are heterogeneous relations.
In the formalization at present a significant amount of energy has been put
towards proving things that would not have been needed in classical Agda. The
proofs that some given type is a proposition were provided as a strategy to
simplify some otherwise very complicated proofs (e.g.
\ref{eq:proof-prop-IsPreCategory} and \label{eq:productPath}). Often these
proofs would not be this complicated. If the J-rule holds definitionally the
proof-assistant can help simplify these goals considerably. The lack of the
J-rule has a significant impact on the complexity of these kinds of proofs.
\TODO{Universe levels.}
\section{Future work}
\subsection{Agda \texttt{Prop}}
Jesper Cockx' work extending the universe-level-laws for Agda and the
\texttt{Prop}-type.
\subsection{Compiling Cubical Agda}
\label{sec:compiling-cubical-agda}
Compilation of program written in Cubical Agda is currently not supported. One
issue here is that the backends does not provide an implementation for the
cubical primitives (such as the path-type). This means that even though the
path-type gives us a computational interpretation of functional extensionality,
univalence, transport, etc., we do not have a way of actually using this to
compile our programs that use these primitives. It would be interesting to see
practical applications of this. The path between monads that this library
exposes could provide one particularly interesting case-study.
\subsection{Higher inductive types}
This library has not explored the usefulness of higher inductive types in the
context of Category Theory.

72
doc/feedback.txt Normal file
View file

@ -0,0 +1,72 @@
Andrea Vezzosi <vezzosi@chalmers.se> Tue, Apr 24, 2018 at 2:02 PM
To: Frederik Hanghøj Iversen <fhi.1990@gmail.com>
Cc: Thierry Coquand <coquand@chalmers.se>
On Tue, Apr 24, 2018 at 12:57 PM, Frederik Hanghøj Iversen
<fhi.1990@gmail.com> wrote:
> I've written the first few sections about my implementation. I was wondering
> if you could have a quick look at it. You don't need to read it
> word-for-word but I would like some indication from you if this is the sort
> of thing you would like to see in the final report.
Yes! I would say this very much fits the bill of what the main part of
the report should be, then you could have a discussion section where
you might put some analysis of the pros and cons of cubical, design
choices you made, and your experience overall.
I wonder if there should be some short introduction to Cubical Type
Theory before this chapter, so you can introduce the Path type by
itself and show some simple proof with it. e.g. how to get function
extensionality.
You mention a few "combinators" like propPi and lemPropF, you might
want to call them just lemmas, so it's clearer that these can be
proven in --cubical.
>
> I refer you specifically to "Chapter 2 - Implementation" on p. 6.
>
> In this chapter I plan to additionally include some text about the proof we
> did that products are mere propositions and the proof about the two
> equivalent notions of a monad.
I've read the chapter up until 2.3 and skimmed the rest for now, but I
accumulated some editing suggestions I copy here.
Remember to look for things like these when you proof-read the rest :)
You should be careful to properly introduce things before you use
them, like IsPreCategory (I'd prefer if it took the raw category as
argument btw) and its fields isIdentity, isAssociative, .. come up a
bit out of the blue from the end of page 8.
Maybe the easiest is to show the definition of IsPreCategory.
Maybe give a type for propIsIdentity and mention the other prop* are similar.
Also the notation "isIdentity_a" to apply projections is a bit unusual
so it needs to be introduced as well.
To be fair it would be simpler to stick to function application
(though I see that it would introduce more parentheses),
"The situation is a bit more complicated when we have a dependent
type" could be more clear by being more specific:
"The situation is a bit more complicated when the type of a field
depends on a previous field"
Here too it might be more concrete if you also give the code for IsCategory.
In Path ( λ i → Univalent_{p i} ) isPreCategory_a isPreCategory_b
I suggest parentheses around (p i), but also you should be consistent
on whether you want to call the proof "p" or "p_{isPreCategory}",
finally i'm guessing the two fields should be "isUnivalent" rather
than "isPreCategory".
You can cite the book on the specific definition of isEquiv,
"contractible fibers" in section 4.4, the grad lemma is also from
somewhere but I don't remember off-hand.
You have not defined what you mean by _\~=_ and isomorphism.
Cheers,
Andrea
[Quoted text hidden]

View file

@ -1,4 +1,4 @@
\section{Halftime report}
\chapter{Halftime report}
I've written this as an appendix because 1) the aim of the thesis changed
drastically from the planning report/proposal 2) partly I'm not sure how to
structure my thesis.
@ -8,7 +8,7 @@ unclear to me at this point what I should have in the final report. Here I will
describe what I have managed to formalize so far and what outstanding challenges
I'm facing.
\subsection{Implementation overview}
\section{Implementation overview}
The overall structure of my project is as follows:
\begin{itemize}
@ -50,7 +50,7 @@ creating a function embodying the ``equality principle'' for a given record. In
the case of monads, to prove two categories propositionally equal it enough to
provide a proof that their data is equal.
\subsubsection{Categories}
\subsection{Categories}
Defines the basic notion of a category. This definition closely follows that of
[HoTT]: That is, the standard definition of a category (data; objects, arrows,
composition and identity, laws; preservation of identity and composition) plus
@ -69,30 +69,30 @@ shown that univalence holds for such a construction)
I also show that taking the opposite is an involution.
\subsubsection{Functors}
\subsection{Functors}
Defines the notion of a functor - also split up into data and laws.
Propositionality for being a functor.
Composition of functors and the identity functor.
\subsubsection{Products}
\subsection{Products}
Definition of what it means for an object to be a product in a given category.
Definition of what it means for a category to have all products.
\WIP Prove propositionality for being a product and having products.
\WIP{} Prove propositionality for being a product and having products.
\subsubsection{Exponentials}
\subsection{Exponentials}
Definition of what it means to be an exponential object.
Definition of what it means for a category to have all exponential objects.
\subsubsection{Cartesian closed categories}
\subsection{Cartesian closed categories}
Definition of what it means for a category to be cartesian closed; namely that
it has all products and all exponentials.
\subsubsection{Natural transformations}
\subsection{Natural transformations}
Definition of transformations\footnote{Maybe this is a name I made up for a
family of morphisms} and the naturality condition for these.
@ -101,18 +101,18 @@ principle. Proof that natural transformations are homotopic sets.
The identity natural transformation.
\subsubsection{Yoneda embedding}
\subsection{Yoneda embedding}
The yoneda embedding is typically presented in terms of the category of
categories (cf. Awodey) \emph however this is not stricly needed - all we need
is what would be the exponential object in that category - this happens to be
functors and so this is how we define the yoneda embedding.
\subsubsection{Monads}
\subsection{Monads}
Defines an equivalence between these two formulations of a monad:
\subsubsubsection{Monoidal monads}
\subsubsection{Monoidal monads}
Defines the standard monoidal representation of a monad:
@ -121,7 +121,7 @@ and some laws about these natural transformations.
Propositionality proofs and equality principle is provided.
\subsubsubsection{Kleisli monads}
\subsubsection{Kleisli monads}
A presentation of monads perhaps more familiar to a functional programer:
@ -130,28 +130,48 @@ some laws about these maps.
Propositionality proofs and equality principle is provided.
\subsubsubsection{Voevodsky's construction}
\subsubsection{Voevodsky's construction}
Provides construction 2.3 as presented in an unpublished paper by the late
Vladimir Voevodsky. This construction is similiar to the equivalence provided
for the two preceding formulations
Provides construction 2.3 as presented in an unpublished paper by Vladimir
Voevodsky. This construction is similiar to the equivalence provided for the two
preceding formulations
\footnote{ TODO: I would like to include in the thesis some motivation for why
this construction is particularly interesting.}
\subsubsection{Homotopy sets}
\subsection{Homotopy sets}
The typical category of sets where the objects are modelled by an Agda set
(henceforth ``type'') at a given level is not a valid category in this cubical
settings, we need to restrict the types to be those that are homotopy sets. Thus the objects of this category are:
(henceforth ``$\Type$'') at a given level is not a valid category in this cubical
settings, we need to restrict the types to be those that are homotopy sets. Thus
the objects of this category are:
%
$$\Set_\ell \defeq \sum_{A \tp \MCU_\ell} \isSet\ A$$
$$\hSet_\ell \defeq \sum_{A \tp \MCU_\ell} \isSet\ A$$
%
\WIP{} I'm still missing a few details for the proof that this category is
univalent. Indeed this doesn't not follow immediately from
The definition of univalence for categories I have defined is:
%
$$\mathit{univalence} \tp (A \cong B) \simeq (A \simeq B)$$
$$\isEquiv\ (\hA \equiv \hB)\ (\hA \cong \hB)\ \idToIso$$
%
since $A$ and $B$ are of type $\MCU \neq \Set$.
\subsubsection{Categories}
Where $\hA and \hB$ denote objects in the category. Note that this is stronger
than
%
$$(\hA \equiv \hB) \simeq (\hA \cong \hB)$$
%
Because we require that the equivalence is constructed from the witness to:
%
$$\id \comp f \equiv f \x f \comp \id \equiv f$$
%
And indeed univalence does not follow immediately from univalence for types:
%
$$(A \equiv B) \simeq (A \simeq B)$$
%
Because $A\ B \tp \Type$ whereas $\hA\ \hB \tp \hSet$.
For this reason I have shown that this category satisfies the following
equivalent formulation of being univalent:
%
$$\prod_{A \tp hSet} \isContr \left( \sum_{X \tp hSet} A \cong X \right)$$
%
But I have not shown that it is indeed equivalent to my former definition.
\subsection{Categories}
Note that this category does in fact not exist. In stead I provide the
definition of the ``raw'' category as well as some of the laws.
@ -162,16 +182,78 @@ These lemmas can be used to provide the actual exponential object in a context
where we have a witness to this being a category. This is useful if this library
is later extended to talk about higher categories.
\subsubsection{Functors}
\subsection{Functors}
The category of functors and natural transformations. An immediate corrolary is
the set of presheaf categories.
\WIP{} I have not shown that the category of functors is univalent.
\subsubsection{Relations}
The category of relations. \WIP I have not shown that this category is
\subsection{Relations}
The category of relations. \WIP{} I have not shown that this category is
univalent. Not sure I intend to do so either.
\subsubsection{Free category}
The free category of a category. \WIP I have not shown that this category is
\subsection{Free category}
The free category of a category. \WIP{} I have not shown that this category is
univalent.
\section{Current Challenges}
Besides the items marked \WIP{} above I still feel a bit unsure about what to
include in my report. Most of my work so far has been specifically about
developing this library. Some ideas:
%
\begin{itemize}
\item
Modularity properties
\item
Compare with setoid-approach to solve similiar problems.
\item
How to structure an implementation to best deal with types that have no
structure (propositions) and those that do (sets and everything above)
\end{itemize}
%
\section{Ideas for future developments}
\subsection{Higher categories}
I only have a notion of (1-)categories. Perhaps it would be nice to also
formalize higher categories.
\subsection{Hierarchy of concepts related to monads}
In Haskell the type-class Monad sits in a hierarchy atop the notion of a functor
and applicative functors. There's probably a similiar notion in the
category-theoretic approach to developing this.
As I have already defined monads from these two perspectives, it would be
interesting to take this idea even further and actually show how monads are
related to applicative functors and functors. I'm not entirely sure how this
would look in Agda though.
\subsection{Use formulation on the standard library}
I also thought it would be interesting to use this library to show certain
properties about functors, applicative functors and monads used in the Agda
Standard library. So I went ahead and tried to show that agda's standard
library's notion of a functor (along with suitable laws) is equivalent to my
formulation (in the category of homotopic sets). I ran into two problems here,
however; the first one is that the standard library's notion of a functor is
indexed by the object map:
%
$$
\Functor \tp (\Type \to \Type) \to \Type
$$
%
Where $\Functor\ F$ has the member:
%
$$
\fmap \tp (A \to B) \to F A \to F B
$$
%
Whereas the object map in my definition is existentially quantified:
%
$$
\Functor \tp \Type
$$
%
And $\Functor$ has these members:
\begin{align*}
F & \tp \Type \to \Type \\
\fmap & \tp (A \to B) \to F A \to F B\}
\end{align*}
%

1325
doc/implementation.tex Normal file

File diff suppressed because it is too large Load diff

205
doc/introduction.tex Normal file
View file

@ -0,0 +1,205 @@
\chapter{Introduction}
Functional extensionality and univalence is not expressible in
\nomen{Intensional Martin Löf Type Theory} (ITT). This poses a severe limitation
on both i. what is \emph{provable} and ii. the \emph{re-usability} of proofs.
Recent developments have, however, resulted in \nomen{Cubical Type Theory} (CTT)
which permits a constructive proof of these two important notions.
Furthermore an extension has been implemented for the proof assistant Agda
(\cite{agda}, \cite{cubical-agda}) that allows us to work in such a ``cubical
setting''. This thesis will explore the usefulness of this extension in the
context of category theory.
%
\section{Motivating examples}
%
In the following two sections I present two examples that illustrate some
limitations inherent in ITT and -- by extension -- Agda.
%
\subsection{Functional extensionality}
Consider the functions:
%
\begin{multicols}{2}
\noindent
\begin{equation*}
f \defeq (n \tp \bN) \mapsto (0 + n \tp \bN)
\end{equation*}
\begin{equation*}
g \defeq (n \tp \bN) \mapsto (n + 0 \tp \bN)
\end{equation*}
\end{multicols}
%
$n + 0$ is \nomen{definitionally} equal to $n$, which we write as $n + 0 = n$.
This is also called \nomen{judgmental} equality. We call it definitional
equality because the \emph{equality} arises from the \emph{definition} of $+$
which is:
%
\newcommand{\suc}[1]{\mathit{suc}\ #1}
\begin{align*}
+ & \tp \bN \to \bN \to \bN \\
n + 0 & \defeq n \\
n + (\suc{m}) & \defeq \suc{(n + m)}
\end{align*}
%
Note that $0 + n$ is \emph{not} definitionally equal to $n$. $0 + n$ is in
normal form. I.e.; there is no rule for $+$ whose left-hand-side matches this
expression. We \emph{do}, however, have that they are \nomen{propositionally}
equal, which we write as $n + 0 \equiv n$. Propositional equality means that
there is a proof that exhibits this relation. Since equality is a transitive
relation we have that $n + 0 \equiv 0 + n$.
Unfortunately we don't have $f \equiv g$.\footnote{Actually showing this is
outside the scope of this text. Essentially it would involve giving a model
for our type theory that validates all our axioms but where $f \equiv g$ is
not true.} There is no way to construct a proof asserting the obvious
equivalence of $f$ and $g$ -- even though we can prove them equal for all
points. This is exactly the notion of equality of functions that we are
interested in; that they are equal for all inputs. We call this
\nomen{point-wise equality}, where the \emph{points} of a function refers
to it's arguments.
In the context of category theory functional extensionality is e.g. needed to
show that representable functors are indeed functors. The representable functor
for a category $\bC$ and a fixed object in $A \in \bC$ is defined to be:
%
\begin{align*}
\fmap \defeq X \mapsto \Hom_{\bC}(A, X)
\end{align*}
%
The proof obligation that this satisfies the identity law of functors
($\fmap\ \idFun \equiv \idFun$) thus becomes:
%
\begin{align*}
\Hom(A, \idFun_{\bX}) = (g \mapsto \idFun \comp g) \equiv \idFun_{\Sets}
\end{align*}
%
One needs functional extensionality to ``go under'' the function arrow and apply
the (left) identity law of the underlying category to prove $\idFun \comp g
\equiv g$ and thus close the goal.
%
\subsection{Equality of isomorphic types}
%
Let $\top$ denote the unit type -- a type with a single constructor. In the
propositions-as-types interpretation of type theory $\top$ is the proposition
that is always true. The type $A \x \top$ and $A$ has an element for each $a :
A$. So in a sense they have the same shape (Greek; \nomen{isomorphic}). The
second element of the pair does not add any ``interesting information''. It can
be useful to identify such types. In fact, it is quite commonplace in
mathematics. Say we look at a set $\{x \mid \phi\ x \land \psi\ x\}$ and somehow
conclude that $\psi\ x \equiv \top$ for all $x$. A mathematician would
immediately conclude $\{x \mid \phi\ x \land \psi\ x\} \equiv \{x \mid
\phi\ x\}$ without thinking twice. Unfortunately such an identification can not
be performed in ITT.
More specifically what we are interested in is a way of identifying
\nomen{equivalent} types. I will return to the definition of equivalence later
in section \ref{sec:equiv}, but for now it is sufficient to think of an
equivalence as a one-to-one correspondence. We write $A \simeq B$ to assert that
$A$ and $B$ are equivalent types. The principle of univalence says that:
%
$$\mathit{univalence} \tp (A \simeq B) \simeq (A \equiv B)$$
%
In particular this allows us to construct an equality from an equivalence
($\mathit{ua} \tp (A \simeq B) \to (A \equiv B)$) and vice-versa.
\section{Formalizing Category Theory}
%
The above examples serve to illustrate a limitation of ITT. One case where these
limitations are particularly prohibitive is in the study of Category Theory. At
a glance category theory can be described as ``the mathematical study of
(abstract) algebras of functions'' (\cite{awodey-2006}). By that token
functional extensionality is particularly useful for formulating Category
Theory. In Category theory it is also common to identify isomorphic structures
and univalence gives us a way to make this notion precise. In fact we can
formulate this requirement within our formulation of categories by requiring the
\emph{categories} themselves to be univalent as we shall see.
\section{Context}
\label{sec:context}
%
The idea of formalizing Category Theory in proof assistants is not new. There
are a multitude of these available online. Just as a first reference see this
question on Math Overflow: \cite{mo-formalizations}. Notably these
implementations of category theory in Agda:
%
\begin{itemize}
\item
\url{https://github.com/copumpkin/categories}
A formalization in Agda using the setoid approach
\item
\url{https://github.com/pcapriotti/agda-categories}
A formalization in Agda with univalence and functional extensionality as
postulates.
\item
\url{https://github.com/HoTT/HoTT/tree/master/theories/Categories}
A formalization in Coq in the homotopic setting
\item
\url{https://github.com/mortberg/cubicaltt}
A formalization in CubicalTT - a language designed for cubical-type-theory.
Formalizes many different things, but only a few concepts from category
theory.
\end{itemize}
%
The contribution of this thesis is to explore how working in a cubical setting
will make it possible to prove more things and to reuse proofs and to try and
compare some aspects of this formalization with the existing ones.\TODO{How can
I live up to this?}
There are alternative approaches to working in a cubical setting where one can
still have univalence and functional extensionality. One option is to postulate
these as axioms. This approach, however, has other shortcomings, e.g.; you lose
\nomen{canonicity} (\TODO{Pageno!} \cite{huber-2016}). Canonicity means that any
well-typed term evaluates to a \emph{canonical} form. For example for a closed
term $e \tp \bN$ it will be the case that $e$ reduces to $n$ applications of
$\mathit{suc}$ to $0$ for some $n$; $e = \mathit{suc}^n\ 0$. Without canonicity
terms in the language can get ``stuck'' -- meaning that they do not reduce to a
canonical form.
Another approach is to use the \emph{setoid interpretation} of type theory
(\cite{hofmann-1995,huber-2016}). With this approach one works with
\nomen{extensional sets} $(X, \sim)$, that is a type $X \tp \MCU$ and an
equivalence relation $\sim \tp X \to X \to \MCU$ on that type. Under the setoid
interpretation the equivalence relation serve as a sort of ``local''
propositional equality. This approach has other drawbacks; it does not satisfy
all propositional equalities of type theory (\TODO{Citation needed}), is
cumbersome to work with in practice (\cite[p. 4]{huber-2016}) and makes
equational proofs less reusable since equational proofs $a \sim_{X} b$ are
inherently `local' to the extensional set $(X , \sim)$.
\section{Conventions}
\TODO{Talk a bit about terminology. Find a good place to stuff this little
section.}
In the remainder of this paper I will use the term \nomen{Type} to describe --
well, types. Thereby diverging from the notation in Agda where the keyword
\texttt{Set} refers to types. \nomen{Set} on the other hand shall refer to the
homotopical notion of a set. I will also leave all universe levels implicit.
And I use the term \nomen{arrow} to refer to morphisms in a category, whereas
the terms morphism, map or function shall be reserved for talking about
type-theoretic functions; i.e. functions in Agda.
$\defeq$ will be used for introducing definitions. $=$ will be used to for
judgmental equality and $\equiv$ will be used for propositional equality.
All this is summarized in the following table:
\begin{center}
\begin{tabular}{ c c c }
Name & Agda & Notation \\
\hline
\nomen{Type} & \texttt{Set} & $\Type$ \\
\nomen{Set} & \texttt{Σ Set IsSet} & $\Set$ \\
Function, morphism, map & \texttt{A → B} & $A → B$ \\
Dependent- ditto & \texttt{(a : A) → B} & $_{a \tp A} B$ \\
\nomen{Arrow} & \texttt{Arrow A B} & $\Arrow\ A\ B$ \\
\nomen{Object} & \texttt{C.Object} & $̱ℂ.Object$ \\
Definition & \texttt{=} & $̱\defeq$ \\
Judgmental equality & \null & $̱=$ \\
Propositional equality & \null & $̱\equiv$
\end{tabular}
\end{center}

BIN
doc/isomorphism.png Normal file

Binary file not shown.

After

Width:  |  Height:  |  Size: 344 KiB

88
doc/macros.tex Normal file
View file

@ -0,0 +1,88 @@
\newcommand{\subsubsubsection}[1]{\textbf{#1}}
\newcommand{\WIP}{\textbf{WIP}}
\newcommand{\coloneqq}{\mathrel{\vcenter{\baselineskip0.5ex \lineskiplimit0pt
\hbox{\scriptsize.}\hbox{\scriptsize.}}}%
=}
\newcommand{\defeq}{\mathrel{\triangleq}}
%% Alternatively:
%% \newcommand{\defeq}{}
\newcommand{\bN}{\mathbb{N}}
\newcommand{\bC}{\mathbb{C}}
\newcommand{\bX}{\mathbb{X}}
% \newcommand{\to}{\rightarrow}
\newcommand{\mto}{\mapsto}
\newcommand{\UU}{\ensuremath{\mathcal{U}}\xspace}
\let\type\UU
\newcommand{\MCU}{\UU}
\newcommand{\nomen}[1]{\emph{#1}}
\newcommand{\todo}[1]{\textit{#1}}
\newcommand{\comp}{\circ}
\newcommand{\x}{\times}
\newcommand\inv[1]{#1\raisebox{1.15ex}{$\scriptscriptstyle-\!1$}}
\newcommand{\tp}{\mathrel{:}}
\newcommand{\Type}{\mathcal{U}}
\usepackage{graphicx}
\makeatletter
\newcommand{\shorteq}{%
\settowidth{\@tempdima}{-}% Width of hyphen
\resizebox{\@tempdima}{\height}{=}%
}
\makeatother
\newcommand{\var}[1]{\ensuremath{\mathit{#1}}}
\newcommand{\Hom}{\var{Hom}}
\newcommand{\fmap}{\var{fmap}}
\newcommand{\bind}{\var{bind}}
\newcommand{\join}{\var{join}}
\newcommand{\omap}{\var{omap}}
\newcommand{\pure}{\var{pure}}
\newcommand{\idFun}{\var{id}}
\newcommand{\Sets}{\var{Sets}}
\newcommand{\Set}{\var{Set}}
\newcommand{\hSet}{\var{hSet}}
\newcommand{\id}{\var{id}}
\newcommand{\isEquiv}{\var{isEquiv}}
\newcommand{\idToIso}{\var{idToIso}}
\newcommand{\isSet}{\var{isSet}}
\newcommand{\isContr}{\var{isContr}}
\newcommand{\isGroupoid}{\var{isGroupoid}}
\newcommand{\pathJ}{\var{pathJ}}
\newcommand\Object{\var{Object}}
\newcommand\Functor{\var{Functor}}
\newcommand\isProp{\var{isProp}}
\newcommand\propPi{\var{propPi}}
\newcommand\propSig{\var{propSig}}
\newcommand\PreCategory{\var{PreCategory}}
\newcommand\IsPreCategory{\var{IsPreCategory}}
\newcommand\isIdentity{\var{isIdentity}}
\newcommand\propIsIdentity{\var{propIsIdentity}}
\newcommand\IsCategory{\var{IsCategory}}
\newcommand\Gl{\var{\lambda}}
\newcommand\lemPropF{\var{lemPropF}}
\newcommand\isPreCategory{\var{isPreCategory}}
\newcommand\congruence{\var{cong}}
\newcommand\identity{\var{identity}}
\newcommand\isequiv{\var{isequiv}}
\newcommand\qinv{\var{qinv}}
\newcommand\fiber{\var{fiber}}
\newcommand\shuffle{\var{shuffle}}
\newcommand\Univalent{\var{Univalent}}
\newcommand\refl{\var{refl}}
\newcommand\isoToId{\var{isoToId}}
\newcommand\Isomorphism{\var{Isomorphism}}
\newcommand\rrr{\ggg}
\newcommand\fish{\mathrel{\wideoverbar{\rrr}}}
\newcommand\fst{\var{fst}}
\newcommand\snd{\var{snd}}
\newcommand\Path{\var{Path}}
\newcommand\Category{\var{Category}}
\newcommand\TODO[1]{TODO: \emph{#1}}
\newcommand*{\QED}{\hfill\ensuremath{\square}}%
\newcommand\uexists{\exists!}
\newcommand\Arrow{\var{Arrow}}
\newcommand\NTsym{\var{NT}}
\newcommand\NT[2]{\NTsym\ #1\ #2}
\newcommand\Endo[1]{\var{Endo}\ #1}
\newcommand\EndoR{\mathcal{R}}

76
doc/main.tex Normal file
View file

@ -0,0 +1,76 @@
\documentclass[a4paper]{report}
%% \documentclass[compact,a4paper]{article}
\input{packages.tex}
\input{macros.tex}
\title{Univalent Categories}
\author{Frederik Hanghøj Iversen}
%% \usepackage[
%% subtitle=foo,
%% author=Frederik Hanghøj Iversen,
%% authoremail=hanghj@student.chalmers.se,
%% newcommand=chalmers,=Chalmers University of Technology,
%% supervisor=Thierry Coquand,
%% supervisoremail=coquand@chalmers.se,
%% supervisordepartment=chalmers,
%% cosupervisor=Andrea Vezzosi,
%% cosupervisoremail=vezzosi@chalmers.se,
%% cosupervisordepartment=chalmers,
%% examiner=Andreas Abel,
%% examineremail=abela@chalmers.se,
%% examinerdepartment=chalmers,
%% institution=chalmers,
%% department=Department of Computer Science and Engineering,
%% researchgroup=Programming Logic Group
%% ]{chalmerstitle}
\usepackage{chalmerstitle}
\subtitle{A formalization of category theory in Cubical Agda}
\authoremail{hanghj@student.chalmers.se}
\newcommand{\chalmers}{Chalmers University of Technology}
\supervisor{Thierry Coquand}
\supervisoremail{coquand@chalmers.se}
\supervisordepartment{\chalmers}
\cosupervisor{Andrea Vezzosi}
\cosupervisoremail{vezzosi@chalmers.se}
\cosupervisordepartment{\chalmers}
\examiner{Andreas Abel}
\examineremail{abela@chalmers.se}
\examinerdepartment{\chalmers}
\institution{\chalmers}
\department{Department of Computer Science and Engineering}
\researchgroup{Programming Logic Group}
\bibliographystyle{plain}
%% \newtheorem{prop}{Proposition}
\makeatletter
\newcommand*{\rom}[1]{\expandafter\@slowroman\romannumeral #1@}
\makeatother
\begin{document}
\myfrontmatter
\pagenumbering{roman}
\maketitle
\addtocontents{toc}{\protect\thispagestyle{empty}}
\tableofcontents
\pagenumbering{arabic}
%
\input{introduction.tex}
\input{cubical.tex}
\input{implementation.tex}
\input{discussion.tex}
\input{conclusion.tex}
\nocite{cubical-demo}
\nocite{coquand-2013}
\bibliography{refs}
\begin{appendices}
\setcounter{page}{1}
\pagenumbering{roman}
\input{sources.tex}
%% \input{planning.tex}
%% \input{halftime.tex}
\end{appendices}
\end{document}

87
doc/packages.tex Normal file
View file

@ -0,0 +1,87 @@
\usepackage[utf8]{inputenc}
\usepackage{natbib}
\usepackage[
hidelinks,
pdfusetitle,
pdfsubject={category theory},
pdfkeywords={type theory, homotopy theory, category theory, agda}]
{hyperref}
\usepackage{graphicx}
\usepackage{parskip}
\usepackage{multicol}
\usepackage{amssymb,amsmath,amsthm,stmaryrd,mathrsfs,wasysym}
\usepackage[toc,page]{appendix}
\usepackage{xspace}
\usepackage[a4paper]{geometry}
% \setlength{\parskip}{10pt}
% \usepackage{tikz}
% \usetikzlibrary{arrows, decorations.markings}
% \usepackage{chngcntr}
% \counterwithout{figure}{section}
\numberwithin{equation}{section}
\usepackage{listings}
\usepackage{fancyvrb}
\usepackage{mathpazo}
\usepackage[scaled=0.95]{helvet}
\usepackage{courier}
\linespread{1.05} % Palatino looks better with this
\usepackage{lmodern}
\usepackage{enumerate}
\usepackage{verbatim}
\usepackage{fontspec}
\usepackage[light]{sourcecodepro}
%% \setmonofont{Latin Modern Mono}
%% \setmonofont[Mapping=tex-text]{FreeMono.otf}
%% \setmonofont{FreeMono.otf}
%% \pagestyle{fancyplain}
\setlength{\headheight}{15pt}
\renewcommand{\chaptermark}[1]{\markboth{\textsc{Chapter \thechapter. #1}}{}}
\renewcommand{\sectionmark}[1]{\markright{\textsc{\thesection\ #1}}}
% Allows for the use of unicode-letters:
\usepackage{unicode-math}
%% \RequirePackage{kvoptions}
\usepackage{pgffor}
\lstset
{basicstyle=\ttfamily
,columns=fullflexible
,breaklines=true
,inputencoding=utf8
,extendedchars=true
%% ,literate={á}{{\'a}}1 {ã}{{\~a}}1 {é}{{\'e}}1
}
\usepackage{newunicodechar}
%% \setmainfont{PT Serif}
\newfontfamily{\fallbackfont}{FreeMono.otf}[Scale=MatchLowercase]
%% \setmonofont[Mapping=tex-text]{FreeMono.otf}
\DeclareTextFontCommand{\textfallback}{\fallbackfont}
\newunicodechar{}{\textfallback{}}
\newunicodechar{}{\textfallback{}}
\newunicodechar{}{\textfallback{}}
\newunicodechar{}{\textfallback{}}
\newunicodechar{}{\textfallback{}}
\newunicodechar{}{\textfallback{}}
\newunicodechar{}{\textfallback{}}
\newunicodechar{}{\textfallback{}}
\newunicodechar{}{\textfallback{}}
\newunicodechar{}{\textfallback{}}
\newunicodechar{𝒜}{\textfallback{?}}
\newunicodechar{}{\textfallback{?}}
%% \newunicodechar{}{\textfallback{}}

View file

@ -1,4 +1,4 @@
\section{Planning report}
\chapter{Planning report}
%
I have already implemented multiple essential building blocks for a
formalization of core-category theory. These concepts include:

View file

@ -106,9 +106,15 @@
@MISC{mo-formalizations,
TITLE = {Formalizations of category theory in proof assistants},
AUTHOR = {Jason Gross},
HOWPUBLISHED = {MathOverflow},
NOTE = {Version: 2014-01-19},
year={2014},
EPRINT = {\url{https://mathoverflow.net/q/152497}},
URL = {https://mathoverflow.net/q/152497}
url = {https://mathoverflow.net/q/152497},
howpublished = {MathOverflow: \url{https://mathoverflow.net/q/152497}}
}
@Misc{UniMath,
author = {Voevodsky, Vladimir and Ahrens, Benedikt and Grayson, Daniel and others},
title = {{UniMath --- a computer-checked library of univalent mathematics}},
url = {https://github.com/UniMath/UniMath},
howpublished = {{available} at \url{https://github.com/UniMath/UniMath}}
}

428
doc/sources.tex Normal file
View file

@ -0,0 +1,428 @@
\chapter{Source code}
\label{ch:app-sources}
In the following a few of the definitions mentioned in the report are included.
The following is \emph{not} a verbatim copy of individual modules from the
implementation. Rather, this is a redacted and pre-formatted designed for
presentation purposes. It's provided here as a convenience. The actual sources
are the only authoritative source. Is something is not clear, please refer to
those.
\clearpage
\section{Cubical}
\label{sec:app-cubical}
\begin{figure}[h]
\begin{Verbatim}
postulate
PathP : ∀ {} (A : I → Set ) → A i0 → A i1 → Set
module _ {} {A : Set } where
__ : A → A → Set
__ {A = A} = PathP (λ _ → A)
refl : {x : A} → x ≡ x
refl {x = x} = λ _ → x
\end{Verbatim}
\caption{Excerpt from the cubical library. Definition of the path-type.}
\end{figure}
%
\begin{figure}[h]
\begin{Verbatim}
module _ { : Level} (A : Set ) where
isContr : Set
isContr = Σ[ x ∈ A ] (∀ y → x ≡ y)
isProp : Set
isProp = (x y : A) → x ≡ y
isSet : Set
isSet = (x y : A) → (p q : x ≡ y) → p ≡ q
isGrpd : Set
isGrpd = (x y : A) → (p q : x ≡ y) → (a b : p ≡ q) → a ≡ b
\end{Verbatim}
\caption{Excerpt from the cubical library. Definition of the first few
homotopy-levels.}
\end{figure}
%
\begin{figure}[h]
\begin{Verbatim}
module _ { '} {A : Set } {x : A}
(P : ∀ y → x ≡ y → Set ') (d : P x ((λ i → x))) where
pathJ : (y : A) → (p : x ≡ y) → P y p
pathJ _ p = transp (λ i → uncurry P (contrSingl p i)) d
\end{Verbatim}
\clearpage
\caption{Excerpt from the cubical library. Definition of based path-induction.}
\end{figure}
%
\begin{figure}[h]
\begin{Verbatim}
module _ { '} {A : Set } {B : A → Set '} where
propPi : (h : (x : A) → isProp (B x)) → isProp ((x : A) → B x)
propPi h f0 f1 = λ i → λ x → (h x (f0 x) (f1 x)) i
lemPropF : (P : (x : A) → isProp (B x)) {a0 a1 : A}
(p : a0 ≡ a1) {b0 : B a0} {b1 : B a1} → PathP (λ i → B (p i)) b0 b1
lemPropF P p {b0} {b1} = λ i → P (p i)
(primComp (λ j → B (p (i ∧ j)) ) (~ i) (λ _ → λ { (i = i0) → b0 }) b0)
(primComp (λ j → B (p (i ~ j)) ) (i) (λ _ → λ{ (i = i1) → b1 }) b1) i
lemSig : (pB : (x : A) → isProp (B x))
(u v : Σ A B) (p : fst u ≡ fst v) → u ≡ v
lemSig pB u v p = λ i → (p i) , ((lemPropF pB p) {snd u} {snd v} i)
propSig : (pA : isProp A) (pB : (x : A) → isProp (B x)) → isProp (Σ A B)
propSig pA pB t u = lemSig pB t u (pA (fst t) (fst u))
\end{Verbatim}
\caption{Excerpt from the cubical library. A few combinators.}
\end{figure}
\clearpage
\section{Categories}
\label{sec:app-categories}
\begin{figure}[h]
\begin{Verbatim}
record RawCategory (a b : Level) : Set (lsuc (a ⊔ b)) where
field
Object : Set a
Arrow : Object → Object → Set b
identity : {A : Object} → Arrow A A
_<<<_ : {A B C : Object} → Arrow B C → Arrow A B → Arrow A C
_>>>_ : {A B C : Object} → (Arrow A B) → (Arrow B C) → Arrow A C
f >>> g = g <<< f
IsAssociative : Set (a ⊔ b)
IsAssociative = ∀ {A B C D} {f : Arrow A B} {g : Arrow B C} {h : Arrow C D}
→ h <<< (g <<< f) ≡ (h <<< g) <<< f
IsIdentity : ({A : Object} → Arrow A A) → Set (a ⊔ b)
IsIdentity id = {A B : Object} {f : Arrow A B}
→ id <<< f ≡ f × f <<< id ≡ f
ArrowsAreSets : Set (a ⊔ b)
ArrowsAreSets = ∀ {A B : Object} → isSet (Arrow A B)
IsInverseOf : ∀ {A B} → (Arrow A B) → (Arrow B A) → Set b
IsInverseOf = λ f g → g <<< f ≡ identity × f <<< g ≡ identity
Isomorphism : ∀ {A B} → (f : Arrow A B) → Set b
Isomorphism {A} {B} f = Σ[ g ∈ Arrow B A ] IsInverseOf f g
__ : (A B : Object) → Set b
__ A B = Σ[ f ∈ Arrow A B ] (Isomorphism f)
IsTerminal : Object → Set (a ⊔ b)
IsTerminal T = {X : Object} → isContr (Arrow X T)
Terminal : Set (a ⊔ b)
Terminal = Σ Object IsTerminal
\end{Verbatim}
\caption{Excerpt from module \texttt{Cat.Category}. The definition of a category.}
\end{figure}
\clearpage
\begin{figure}[h]
\begin{Verbatim}
module Univalence (isIdentity : IsIdentity identity) where
idIso : (A : Object) → A ≊ A
idIso A = identity , identity , isIdentity
idToIso : (A B : Object) → A ≡ B → A ≊ B
idToIso A B eq = subst eq (idIso A)
Univalent : Set (a ⊔ b)
Univalent = {A B : Object} → isEquiv (A ≡ B) (A ≊ B) (idToIso A B)
\end{Verbatim}
\caption{Excerpt from module \texttt{Cat.Category}. Continued from previous. Definition of univalence.}
\end{figure}
\begin{figure}[h]
\begin{Verbatim}
module _ {a b : Level} ( : RawCategory a b) where
record IsPreCategory : Set (lsuc (a ⊔ b)) where
open RawCategory public
field
isAssociative : IsAssociative
isIdentity : IsIdentity identity
arrowsAreSets : ArrowsAreSets
open Univalence isIdentity public
record PreCategory : Set (lsuc (a ⊔ b)) where
field
isPreCategory : IsPreCategory
open IsPreCategory isPreCategory public
record IsCategory : Set (lsuc (a ⊔ b)) where
field
isPreCategory : IsPreCategory
open IsPreCategory isPreCategory public
field
univalent : Univalent
\end{Verbatim}
\caption{Excerpt from module \texttt{Cat.Category}. Records with inhabitants for
the laws defined in the previous listings.}
\end{figure}
\clearpage
\begin{figure}[h]
\begin{Verbatim}
module Opposite {a b : Level} where
module _ ( : Category a b) where
private
module _ where
module = Category
opRaw : RawCategory a b
RawCategory.Object opRaw = .Object
RawCategory.Arrow opRaw = flip .Arrow
RawCategory.identity opRaw = .identity
RawCategory._<<<_ opRaw = ._>>>_
open RawCategory opRaw
isPreCategory : IsPreCategory opRaw
IsPreCategory.isAssociative isPreCategory = sym .isAssociative
IsPreCategory.isIdentity isPreCategory = swap .isIdentity
IsPreCategory.arrowsAreSets isPreCategory = .arrowsAreSets
open IsPreCategory isPreCategory
----------------------------
-- NEXT LISTING GOES HERE --
----------------------------
isCategory : IsCategory opRaw
IsCategory.isPreCategory isCategory = isPreCategory
IsCategory.univalent isCategory
= univalenceFromIsomorphism (isoToId* , inv)
opposite : Category a b
Category.raw opposite = opRaw
Category.isCategory opposite = isCategory
module _ { : Category a b} where
open Category
private
rawInv : Category.raw (opposite (opposite )) ≡ raw
RawCategory.Object (rawInv _) = Object
RawCategory.Arrow (rawInv _) = Arrow
RawCategory.identity (rawInv _) = identity
RawCategory._<<<_ (rawInv _) = _<<<_
oppositeIsInvolution : opposite (opposite ) ≡
oppositeIsInvolution = Category≡ rawInv
\end{Verbatim}
\caption{Excerpt from module \texttt{Cat.Category}. Showing that the opposite
category is a category. Part of this listing has been cut out and placed in
the next listing.}
\end{figure}
\clearpage
For reasons of formatting the following listing is continued from the above with
fewer levels of indentation.
%
\begin{figure}[h]
\begin{Verbatim}
module _ {A B : .Object} where
open Σ (toIso _ _ (.univalent {A} {B}))
renaming (fst to idToIso* ; snd to inv*)
open AreInverses {f = .idToIso A B} {idToIso*} inv*
shuffle : A ≊ B → A .≊ B
shuffle (f , g , inv) = g , f , inv
shuffle~ : A .≊ B → A ≊ B
shuffle~ (f , g , inv) = g , f , inv
isoToId* : A ≊ B → A ≡ B
isoToId* = idToIso* ∘ shuffle
inv : AreInverses (idToIso A B) isoToId*
inv =
( funExt (λ x → begin
(isoToId* ∘ idToIso A B) x
≡⟨⟩
(idToIso* ∘ shuffle ∘ idToIso A B) x
≡⟨ cong (λ φ → φ x)
(cong (λ φ → idToIso* ∘ shuffle ∘ φ) (funExt (isoEq refl))) ⟩
(idToIso* ∘ shuffle ∘ shuffle~ ∘ .idToIso A B) x
≡⟨⟩
(idToIso* ∘ .idToIso A B) x
≡⟨ (λ i → verso-recto i x) ⟩
x ∎)
, funExt (λ x → begin
(idToIso A B ∘ idToIso* ∘ shuffle) x
≡⟨ cong (λ φ → φ x)
(cong (λ φ → φ ∘ idToIso* ∘ shuffle) (funExt (isoEq refl))) ⟩
(shuffle~ ∘ .idToIso A B ∘ idToIso* ∘ shuffle) x
≡⟨ cong (λ φ → φ x)
(cong (λ φ → shuffle~ ∘ φ ∘ shuffle) recto-verso) ⟩
(shuffle~ ∘ shuffle) x
≡⟨⟩
x ∎)
)
\end{Verbatim}
\caption{Excerpt from module \texttt{Cat.Category}. Proving univalence for the opposite category.}
\end{figure}
\clearpage
\section{Products}
\label{sec:app-products}
\begin{figure}[h]
\begin{Verbatim}
module _ {a b : Level} ( : Category a b) where
open Category
module _ (A B : Object) where
record RawProduct : Set (a ⊔ b) where
no-eta-equality
field
object : Object
fst : [ object , A ]
snd : [ object , B ]
record IsProduct (raw : RawProduct) : Set (a ⊔ b) where
open RawProduct raw public
field
ump : ∀ {X : Object} (f : [ X , A ]) (g : [ X , B ])
→ ∃![ f×g ] ( [ fst ∘ f×g ] ≡ f P.× [ snd ∘ f×g ] ≡ g)
record Product : Set (a ⊔ b) where
field
raw : RawProduct
isProduct : IsProduct raw
open IsProduct isProduct public
\end{Verbatim}
\caption{Excerpt from module \texttt{Cat.Category.Product}. Definition of products.}
\end{figure}
%
\begin{figure}[h]
\begin{Verbatim}
module _{a b : Level} { : Category a b}
(let module = Category ) {A* B* : .Object} where
module _ where
raw : RawCategory _ _
raw = record
{ Object = Σ[ X ∈ .Object ] .Arrow X A* × .Arrow X B*
; Arrow = λ{ (A , a0 , a1) (B , b0 , b1)
→ Σ[ f ∈ .Arrow A B ]
[ b0 ∘ f ] ≡ a0
× [ b1 ∘ f ] ≡ a1
}
; identity = λ{ {X , f , g}
.identity {X} , .rightIdentity , .rightIdentity
}
; _<<<_ = λ { {_ , a0 , a1} {_ , b0 , b1} {_ , c0 , c1}
(f , f0 , f1) (g , g0 , g1)
→ (f .<<< g)
, (begin
[ c0 ∘ [ f ∘ g ] ] ≡⟨ .isAssociative ⟩
[ [ c0 ∘ f ] ∘ g ] ≡⟨ cong (λ φ → [ φ ∘ g ]) f0 ⟩
[ b0 ∘ g ] ≡⟨ g0 ⟩
a0 ∎
)
, (begin
[ c1 ∘ [ f ∘ g ] ] ≡⟨ .isAssociative ⟩
[ [ c1 ∘ f ] ∘ g ] ≡⟨ cong (λ φ → [ φ ∘ g ]) f1 ⟩
[ b1 ∘ g ] ≡⟨ g1 ⟩
a1 ∎
)
}
}
\end{Verbatim}
\caption{Excerpt from module \texttt{Cat.Category.Product}. Definition of ``pair category''.}
\end{figure}
\clearpage
\section{Monads}
\label{sec:app-monads}
\begin{figure}[h]
\begin{Verbatim}
module Cat.Category.Monad.Kleisli
{a b : Level} ( : Category a b) where
record RawMonad : Set where
field
omap : Object → Object
pure : {X : Object} [ X , omap X ]
bind : {X Y : Object} [ X , omap Y ] → [ omap X , omap Y ]
fmap : ∀ {A B} [ A , B ] → [ omap A , omap B ]
fmap f = bind (pure <<< f)
_>=>_ : {A B C : Object}
[ A , omap B ] → [ B , omap C ] → [ A , omap C ]
f >=> g = f >>> (bind g)
join : {A : Object} [ omap (omap A) , omap A ]
join = bind identity
IsIdentity = {X : Object}
→ bind pure ≡ identity {omap X}
IsNatural = {X Y : Object} (f : [ X , omap Y ])
→ pure >=> f ≡ f
IsDistributive = {X Y Z : Object}
(g : [ Y , omap Z ]) (f : [ X , omap Y ])
→ (bind f) >>> (bind g) ≡ bind (f >=> g)
record IsMonad (raw : RawMonad) : Set where
open RawMonad raw public
field
isIdentity : IsIdentity
isNatural : IsNatural
isDistributive : IsDistributive
\end{Verbatim}
\caption{Excerpt from module \texttt{Cat.Category.Monad.Kleisli}. Definition of
Kleisli monads.}
\end{figure}
%
\begin{figure}[h]
\begin{Verbatim}
module Cat.Category.Monad.Monoidal
{a b : Level} ( : Category a b) where
private
= a ⊔ b
open Category using (Object ; Arrow ; identity ; _<<<_)
record RawMonad : Set where
field
R : EndoFunctor
pureNT : NaturalTransformation Functors.identity R
joinNT : NaturalTransformation F[ R ∘ R ] R
Romap = Functor.omap R
fmap = Functor.fmap R
pureT : Transformation Functors.identity R
pureT = fst pureNT
pure : {X : Object} [ X , Romap X ]
pure = pureT _
pureN : Natural Functors.identity R pureT
pureN = snd pureNT
joinT : Transformation F[ R ∘ R ] R
joinT = fst joinNT
join : {X : Object} [ Romap (Romap X) , Romap X ]
join = joinT _
joinN : Natural F[ R ∘ R ] R joinT
joinN = snd joinNT
bind : {X Y : Object} [ X , Romap Y ] → [ Romap X , Romap Y ]
bind {X} {Y} f = join <<< fmap f
IsAssociative : Set _
IsAssociative = {X : Object}
→ joinT X <<< fmap join ≡ join <<< join
IsInverse : Set _
IsInverse = {X : Object}
→ join <<< pure ≡ identity {Romap X}
× join <<< fmap pure ≡ identity {Romap X}
record IsMonad (raw : RawMonad) : Set where
open RawMonad raw public
field
isAssociative : IsAssociative
isInverse : IsInverse
\end{Verbatim}
\caption{Excerpt from module \texttt{Cat.Category.Monad.Monoidal}. Definition of
Monoidal monads.}
\end{figure}

@ -1 +1 @@
Subproject commit fbd8ba7ea84c4b643fd08797b4031b18a59f561d
Subproject commit 4493cf249a1648be2ad365fe94ece337bfbcb5d9

@ -1 +1 @@
Subproject commit 5b35333dbbd8fa523e478c1cfe60657321ca38fe
Subproject commit 4e5d43a9c75286b3a8750567d75a930674d7720d

View file

@ -1,22 +0,0 @@
Remove stuff about models of type theory
Add references to specific (noteable) implementaitons of category theory:
* Unimath
* cubicaltt
* https://github.com/pcapriotti/agda-categories
* https://github.com/copumpkin/categories
* ...
Talk about structure of library:
===
Propositional- and non-propositional stuff split up
Providing "equiality principles"
Provide overview of what has been proven.
What can I say about reusability?
Misc
====
Propositional content

View file

@ -1,56 +0,0 @@
% Requires: hypperref
\ProvidesPackage{chalmerstitle}
\newcommand*{\authoremail}[1]{\gdef\@authoremail{#1}}
\newcommand*{\supervisor}[1]{\gdef\@supervisor{#1}}
\newcommand*{\supervisoremail}[1]{\gdef\@supervisoremail{#1}}
\newcommand*{\cosupervisor}[1]{\gdef\@cosupervisor{#1}}
\newcommand*{\cosupervisoremail}[1]{\gdef\@cosupervisoremail{#1}}
\newcommand*{\institution}[1]{\gdef\@institution{#1}}
\renewcommand*{\maketitle}{%
\begin{titlepage}
\begin{center}
{\scshape\LARGE Master thesis project proposal\\}
\vspace{0.5cm}
{\LARGE\bfseries \@title\\}
\vspace{2cm}
{\Large \@author\\ \href{mailto:\@authoremail>}{\texttt{<\@authoremail>}} \\}
% \vspace{0.2cm}
%
% {\Large name and email adress of student 2\\}
\vspace{1.0cm}
{\large Supervisor: \@supervisor\\ \href{mailto:\@supervisoremail>}{\texttt{<\@supervisoremail>}}\\}
\vspace{0.2cm}
{\large Co-supervisor: \@cosupervisor\\ \href{mailto:\@cosupervisoremail>}{\texttt{<\@cosupervisoremail>}}\\}
\vspace{1.5cm}
{\large Relevant completed courses:\par}
{\itshape
Logic in Computer Science -- DAT060\\
Models of Computation -- TDA184\\
Research topic in Computer Science -- DAT235\\
Types for programs and proofs -- DAT140
}
\vfill
{\large \@institution\\\today\\}
\end{center}
\end{titlepage}
}

View file

@ -1,26 +0,0 @@
\newcommand{\coloneqq}{\mathrel{\vcenter{\baselineskip0.5ex \lineskiplimit0pt
\hbox{\scriptsize.}\hbox{\scriptsize.}}}%
=}
\newcommand{\defeq}{\coloneqq}
\newcommand{\bN}{\mathbb{N}}
\newcommand{\bC}{\mathbb{C}}
\newcommand{\bX}{\mathbb{X}}
% \newcommand{\to}{\rightarrow}
\newcommand{\mto}{\mapsto}
\newcommand{\UU}{\ensuremath{\mathcal{U}}\xspace}
\let\type\UU
\newcommand{\nomen}[1]{\emph{#1}}
\newcommand{\todo}[1]{\textit{#1}}
\newcommand{\comp}{\circ}
\newcommand{\x}{\times}
\newcommand{\Hom}{\mathit{Hom}}
\newcommand{\fmap}{\mathit{fmap}}
\newcommand{\idFun}{\mathit{id}}
\newcommand{\Sets}{\mathit{Sets}}
\newcommand{\Set}{\mathit{Set}}
\newcommand{\MCU}{\UU}
\newcommand{\isSet}{\mathit{isSet}}
\newcommand{\tp}{\;\mathord{:}\;}
\newcommand{\subsubsubsection}[1]{\textbf{#1}}
\newcommand{\WIP}[1]{\textbf{[WIP]}}

View file

@ -1,289 +0,0 @@
\documentclass{article}
\usepackage[utf8]{inputenc}
\usepackage{natbib}
\usepackage[hidelinks]{hyperref}
\usepackage{graphicx}
\usepackage{parskip}
\usepackage{multicol}
\usepackage{amsmath,amssymb}
\usepackage[toc,page]{appendix}
\usepackage{xspace}
% \setlength{\parskip}{10pt}
% \usepackage{tikz}
% \usetikzlibrary{arrows, decorations.markings}
% \usepackage{chngcntr}
% \counterwithout{figure}{section}
\usepackage{chalmerstitle}
\input{macros.tex}
\title{Category Theory and Cubical Type Theory}
\author{Frederik Hanghøj Iversen}
\authoremail{hanghj@student.chalmers.se}
\supervisor{Thierry Coquand}
\supervisoremail{coquand@chalmers.se}
\cosupervisor{Andrea Vezzosi}
\cosupervisoremail{vezzosi@chalmers.se}
\institution{Chalmers University of Technology}
\begin{document}
\maketitle
%
\section{Introduction}
%
Functional extensionality and univalence is not expressible in
\nomen{Intensional Martin Löf Type Theory} (ITT). This poses a severe limitation
on both 1) what is \emph{provable} and 2) the \emph{reusability} of proofs.
Recent developments have, however, resulted in \nomen{Cubical Type Theory} (CTT)
which permits a constructive proof of these two important notions.
Furthermore an extension has been implemented for the proof assistant Agda
(\cite{agda}) that allows us to work in such a ``cubical setting''. This project
will be concerned with exploring the usefulness of this extension. As a
case-study I will consider \nomen{category theory}. This will serve a dual
purpose: First off category theory is a field where the notion of functional
extensionality and univalence wil be particularly useful. Secondly, Category
Theory gives rise to a \nomen{model} for CTT.
The project will consist of two parts: The first part will be concerned with
formalizing concepts from category theory. The focus will be on formalizing
parts that will be useful in the second part of the project: Showing that
\nomen{Cubical Sets} give rise to a model of CTT.
%
\section{Problem}
%
In the following two subsections I present two examples that illustrate the
limitation inherent in ITT and by extension to the expressiveness of Agda.
%
\subsection{Functional extensionality}
Consider the functions:
%
\begin{multicols}{2}
$f \defeq (n : \bN) \mapsto (0 + n : \bN)$
$g \defeq (n : \bN) \mapsto (n + 0 : \bN)$
\end{multicols}
%
$n + 0$ is definitionally equal to $n$. We call this \nomen{definitional
equality} and write $n + 0 = n$ to assert this fact. We call it definitional
equality because the \emph{equality} arises from the \emph{definition} of $+$
which is:
%
\newcommand{\suc}[1]{\mathit{suc}\ #1}
\begin{align*}
+ & : \bN \to \bN \\
n + 0 & \defeq n \\
n + (\suc{m}) & \defeq \suc{(n + m)}
\end{align*}
%
Note that $0 + n$ is \emph{not} definitionally equal to $n$. $0 + n$ is in
normal form. I.e.; there is no rule for $+$ whose left-hand-side matches this
expression. We \emph{do}, however, have that they are \nomen{propositionally}
equal. We write $n + 0 \equiv n$ to assert this fact. Propositional equality
means that there is a proof that exhibits this relation. Since equality is a
transitive relation we have that $n + 0 \equiv 0 + n$.
Unfortunately we don't have $f \equiv g$.\footnote{Actually showing this is
outside the scope of this text. Essentially it would involve giving a model
for our type theory that validates all our axioms but where $f \equiv g$ is
not true.} There is no way to construct a proof asserting the obvious
equivalence of $f$ and $g$ -- even though we can prove them equal for all
points. This is exactly the notion of equality of functions that we are
interested in; that they are equal for all inputs. We call this
\nomen{pointwise equality}, where the \emph{points} of a function refers
to it's arguments.
In the context of category theory the principle of functional extensionality is
for instance useful in the context of showing that representable functors are
indeed functors. The representable functor for a category $\bC$ and a fixed
object in $A \in \bC$ is defined to be:
%
\begin{align*}
\fmap \defeq X \mapsto \Hom_{\bC}(A, X)
\end{align*}
%
The proof obligation that this satisfies the identity law of functors
($\fmap\ \idFun \equiv \idFun$) becomes:
%
\begin{align*}
\Hom(A, \idFun_{\bX}) = (g \mapsto \idFun \comp g) \equiv \idFun_{\Sets}
\end{align*}
%
One needs functional extensionality to ``go under'' the function arrow and apply
the (left) identity law of the underlying category to proove $\idFun \comp g
\equiv g$ and thus closing the above proof.
%
\iffalse
I also want to talk about:
\begin{itemize}
\item
Foundational systems
\item
Theory vs. metatheory
\item
Internal type theory
\end{itemize}
\fi
\subsection{Equality of isomorphic types}
%
Let $\top$ denote the unit type -- a type with a single constructor. In the
propositions-as-types interpretation of type theory $\top$ is the proposition
that is always true. The type $A \x \top$ and $A$ has an element for each $a :
A$. So in a sense they are the same. The second element of the pair does not add
any ``interesting information''. It can be useful to identify such types. In
fact, it is quite commonplace in mathematics. Say we look at a set $\{x \mid
\phi\ x \land \psi\ x\}$ and somehow conclude that $\psi\ x \equiv \top$ for all
$x$. A mathematician would immediately conclude $\{x \mid \phi\ x \land
\psi\ x\} \equiv \{x \mid \phi\ x\}$ without thinking twice. Unfortunately such
an identification can not be performed in ITT.
More specifically; what we are interested in is a way of identifying types that
are in a one-to-one correspondence. We say that such types are
\nomen{isomorphic} and write $A \cong B$ to assert this.
To prove two types isomorphic is to give an \nomen{isomorphism} between them.
That is, a function $f : A \to B$ with an inverse $f^{-1} : B \to A$, i.e.:
$f^{-1} \comp f \equiv id_A$. If such a function exist we say that $A$ and $B$
are isomorphic and write $A \cong B$.
Furthermore we want to \emph{identify} such isomorphic types. This, we get from
the principle of univalence:\footnote{It's often referred to as the univalence
axiom, but since it is not an axiom in this setting but rather a theorem I
refer to this just as a `principle'.}
%
$$(A \cong B) \cong (A \equiv B)$$
%
\subsection{Formalizing Category Theory}
%
The above examples serve to illustrate the limitation of Agda. One case where
these limitations are particularly prohibitive is in the study of Category
Theory. At a glance category theory can be described as ``the mathematical study
of (abstract) algebras of functions'' (\cite{awodey-2006}). So by that token
functional extensionality is particularly useful for formulating Category
Theory. In Category theory it is also common to identify isomorphic structures
and this is exactly what we get from univalence.
\subsection{Cubical model for Cubical Type Theory}
%
A model is a way of giving meaning to a formal system in a \emph{meta-theory}. A
typical example of a model is that of sets as models for predicate logic. Thus
set-theory becomes the meta-theory of the formal language of predicate logic.
In the context of a given type theory and restricting ourselves to
\emph{categorical} models a model will consist of mapping `things' from the
type-theory (types, terms, contexts, context morphisms) to `things' in the
meta-theory (objects, morphisms) in such a way that the axioms of the
type-theory (typing-rules) are validated in the meta-theory. In
\cite{dybjer-1995} the author describes a way of constructing such models for
dependent type theory called \emph{Categories with Families} (CwFs).
In \cite{bezem-2014} the authors devise a CwF for Cubical Type Theory. This
project will study and formalize this model. Note that I will \emph{not} aim to
formalize CTT itself and therefore also not give the formal translation between
the type theory and the meta-theory. Instead the translation will be accounted
for informally.
The project will formalize CwF's. It will also define what pieces of data are
needed for a model of CTT (without explicitly showing that it does in fact model
CTT). It will then show that a CwF gives rise to such a model. Furthermore I
will show that cubical sets are presheaf categories and that any presheaf
category is itself a CwF. This is the precise way by which the project aims to
provide a model of CTT. Note that this formalization specifcally does not
mention the language of CTT itself. Only be referencing this previous work do we
arrive at a model of CTT.
%
\section{Context}
%
In \cite{bezem-2014} a categorical model for cubical type theory is presented.
In \cite{cohen-2016} a type-theory where univalence is expressible is presented.
The categorical model in the previous reference serve as a model of this type
theory. So these two ideas are closely related. Cubical type theory arose out of
\nomen{Homotopy Type Theory} (\cite{hott-2013}) and is also of interest as a
foundation of mathematics (\cite{voevodsky-2011}).
An implementation of cubical type theory can be found as an extension to Agda.
This is due to \citeauthor{cubical-agda}. This, of course, will be central to
this thesis.
The idea of formalizing Category Theory in proof assistants is not a new
idea\footnote{There are a multitude of these available online. Just as first
reference see this question on Math Overflow: \cite{mo-formalizations}}. The
contribution of this thesis is to explore how working in a cubical setting will
make it possible to prove more things and to reuse proofs.
There are alternative approaches to working in a cubical setting where one can
still have univalence and functional extensionality. One option is to postulate
these as axioms. This approach, however, has other shortcomings, e.g.; you lose
\nomen{canonicity} (\cite{huber-2016}). Canonicity means that any well-type
term will (under evaluation) reduce to a \emph{canonical} form. For example for
an integer $e : \bN$ it will be the case that $e$ is definitionally equal to $n$
applications of $\mathit{suc}$ to $0$ for some $n$; $e = \mathit{suc}^n\ 0$.
Without canonicity terms in the language can get ``stuck'' when they are
evaluated.
Another approach is to use the \emph{setoid interpretation} of type theory
(\cite{hofmann-1995,huber-2016}). Types should additionally `carry around' an
equivalence relation that should serve as propositional equality. This approach
has other drawbacks; it does not satisfy all judgemental equalites of type
theory and is cumbersome to work with in practice (\cite[p. 4]{huber-2016}).
%
\section{Goals and Challenges}
%
In summary, the aim of the project is to:
%
\begin{itemize}
\item
Formalize Category Theory in Cubical Agda
\item
Formalize Cubical Sets in Agda
% \item
% Formalize Cubical Type Theory in Agda
\item
Show that Cubical Sets are a model for Cubical Type Theory
\end{itemize}
%
The formalization of category theory will focus on extracting the elements from
Category Theory that we need in the latter part of the project. In doing so I'll
be gaining experience with working with Cubical Agda. Equality proofs using
cubical Agda can be tricky, so working with that will be a challenge in itself.
Most of the proofs in the context of cubical models I will formalize are based
on previous work. Those proofs, however, are not formalized in a proof
assistant.
One particular challenge in this context is that in a cubical setting there can
be multiple distinct terms that inhabit a given equality proof.\footnote{This is
in contrast with ITT where one \emph{can} have \nomen{Uniqueness of identity proofs}
(\cite[p. 4]{huber-2016}).} This means that the choice for a given equality
proof can influence later proofs that refer back to said proof. This is new and
relatively unexplored territory.
Another challenge is that Category Theory is something that I only know the
basics of. So learning the necessary concepts from Category Theory will also be
a goal and a challenge in itself.
After this has been implemented it would also be possible to formalize Cubical
Type Theory and formally show that Cubical Sets are a model of this. I do not
intend to formally implement the language of dependent type theory in this
project.
The thesis shall conclude with a discussion about the benefits of Cubical Agda.
%
\bibliographystyle{plainnat}
\nocite{cubical-demo}
\nocite{coquand-2013}
\bibliography{refs}
\begin{appendices}
\input{planning.tex}
\input{halftime.tex}
\end{appendices}
\end{document}

1
report/.gitignore vendored
View file

@ -1 +0,0 @@
cat.pdf

View file

@ -1,40 +0,0 @@
PROJECT = cat
PDF = $(PROJECT).pdf
NOTES = $(PROJECT).md
preview: report
xdg-open $(PDF)
report: $(PDF)
$(PDF): $(NOTES)
pandoc $(NOTES) \
-o $(PDF) \
--latex-engine=xelatex \
--variable urlcolor=cyan \
-V papersize:a4 \
-V geometry:margin=1.5in \
--filter pandoc-citeproc
github: README.md
README.md: $(NOTES)
pandoc $(NOTES) \
-o README.md
run:
stack exec lab4
build:
stack build
dist: report
tar \
--transform "s/^/$(PROJECT)\//" \
-zcvf $(PROJECT).tar.gz \
$(SOURCE) \
LICENSE \
stack.yaml \
lab4.cabal \
Makefile \
$(PDF)

View file

@ -1,90 +0,0 @@
---
title: Formalizing category theory in Agda - Project description
date: May 27th 2017
author: Frederik Hanghøj Iversen `<hanghj@student.chalmers.se>`
bibliography: refs.bib
---
Background
==========
Functional extensionality gives rise to a notion of equality of functions not
present in intensional dependent type theory. A type-system called cubical
type-theory is outlined in [@cohen-2016] that recovers the computational
interprtation of the univalence theorem.
Keywords: The category of sets, limits, colimits, functors, natural
transformations, kleisly category, yoneda lemma, closed cartesian categories,
propositional logic.
<!--
"[...] These foundations promise to resolve several seemingly unconnected
problems-provide a support for categorical and higher categorical arguments
directly on the level of the language, make formalizations of usual mathematics
much more concise and much better adapted to the use with existing proof
assistants such as Coq [...]"
From "Univalent Foundations of Mathematics" by "Voevodsky".
-->
Aim
===
The aim of the project is two-fold. The first part of the project will be
concerned with formalizing some concepts from category theory in Agda's
type-system. This formalization should aim to incorporate definitions and
theorems that allow us to express the correpondence in the second part: Namely
showing the correpondence between well-typed terms in cubical type theory as
presented in Huber and Thierry's paper and with that of some concepts from Category Theory.
This latter part is not entirely clear for me yet, I know that all these are relevant keywords:
* The category, C, of names and substitutions
* Cubical Sets, i.e.: Functors from C to Set (the category of sets)
* Presheaves
* Fibers and fibrations
These are all formulated in the language of Category Theory. The purpose it to
show what they correspond to in the in Cubical Type Theory. As I understand it
at least the last buzzword on this list corresponds to Type Families.
I'm not sure how I'll go about expressing this in Agda. I suspect it might
be a matter of demostrating that these two formulations are isomorphic.
So far I have some experience with at least expressing some categorical
concepts in Agda using this new notion of equality. That is, equaility is in
some sense a continuuous path from a point of some type to another. So at the
moment, my understanding of cubical type theory is just that it has another
notion of equality but is otherwise pretty much the same.
Timeplan
========
The first part of the project will focus on studying and understanding the
foundations for this project namely; familiarizing myself with basic concepts
from category theory, understanding how cubical type theory gives rise to
expressing functional extensionality and the univalence theorem.
After I have understood these fundamental concepts I will use them in the
formalization of functors, applicative functors, monads, etc.. in Agda. This
should be done before the end of the first semester of the school-year
2017/2018.
At this point I will also have settled on a direction for the rest of the
project and developed a time-plan for the second phase of the project. But
cerainly it will involve applying the result of phase 1 in some context as
mentioned in [the project aim][aim].
Resources
=========
* Cubical demo by Andrea Vezossi: [@cubical-demo]
* Paper on cubical type theory [@cohen-2016]
* Book on homotopy type theory: [@hott-2013]
* Book on category theory: [@awodey-2006]
* Modal logic - Modal type theory,
see [ncatlab](https://ncatlab.org/nlab/show/modal+type+theory).
References
==========

View file

@ -1,42 +0,0 @@
@article{cohen-2016,
author = {Cyril Cohen and
Thierry Coquand and
Simon Huber and
Anders M{\"{o}}rtberg},
title =
{ Cubical Type Theory:
a constructive interpretation of the univalence axiom
},
journal = {CoRR},
volume = {abs/1611.02108},
year = {2016},
url = {http://arxiv.org/abs/1611.02108},
timestamp = {Thu, 01 Dec 2016 19:32:08 +0100},
biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/CohenCHM16},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@book{hott-2013,
author = {The {Univalent Foundations Program}},
title = {Homotopy Type Theory: Univalent Foundations of Mathematics},
publisher = {\url{https://homotopytypetheory.org/book}},
address = {Institute for Advanced Study},
year = 2013
}
@book{awodey-2006,
title={Category Theory},
author={Awodey, S.},
isbn={9780191513824},
series={Oxford Logic Guides},
url={https://books.google.se/books?id=IK\_sIDI2TCwC},
year={2006},
publisher={Ebsco Publishing}
}
@misc{cubical-demo,
author = {Andrea Vezzosi},
title = {Cubical Type Theory Demo},
year = {2017},
publisher = {GitHub},
journal = {GitHub repository},
howpublished = {\url{https://github.com/Saizan/cubical-demo}},
commit = {a51d5654c439111110d5b6df3605b0043b10b753}
}

View file

@ -3,42 +3,22 @@
module Cat.Categories.Cat where
open import Cat.Prelude renaming (proj₁ to fst ; proj₂ to snd)
open import Cat.Prelude renaming (fst to fst ; snd to snd)
open import Cat.Category
open import Cat.Category.Functor
open import Cat.Category.Product
open import Cat.Category.Exponential hiding (_×_ ; product)
open import Cat.Category.NaturalTransformation
import Cat.Category.NaturalTransformation
open import Cat.Categories.Fun
-- The category of categories
module _ ( ' : Level) where
private
module _ {𝔸 𝔹 𝔻 : Category '} {F : Functor 𝔸 𝔹} {G : Functor 𝔹 } {H : Functor 𝔻} where
assc : F[ H F[ G F ] ] F[ F[ H G ] F ]
assc = Functor≡ refl
module _ { 𝔻 : Category '} {F : Functor 𝔻} where
ident-r : F[ F identity ] F
ident-r = Functor≡ refl
ident-l : F[ identity F ] F
ident-l = Functor≡ refl
RawCat : RawCategory (lsuc ( ')) ( ')
RawCategory.Object RawCat = Category '
RawCategory.Arrow RawCat = Functor
RawCategory.𝟙 RawCat = identity
RawCategory._∘_ RawCat = F[_∘_]
private
open RawCategory RawCat
isAssociative : IsAssociative
isAssociative {f = F} {G} {H} = assc {F = F} {G = G} {H = H}
isIdentity : IsIdentity identity
isIdentity = ident-l , ident-r
RawCategory.identity RawCat = Functors.identity
RawCategory._<<<_ RawCat = F[_∘_]
-- NB! `ArrowsAreSets RawCat` is *not* provable. The type of functors,
-- however, form a groupoid! Therefore there is no (1-)category of
@ -68,51 +48,55 @@ module CatProduct { ' : Level} ( 𝔻 : Category ') where
Obj = .Object × 𝔻.Object
Arr : Obj Obj Set '
Arr (c , d) (c' , d') = [ c , c' ] × 𝔻 [ d , d' ]
𝟙 : {o : Obj} Arr o o
𝟙 = .𝟙 , 𝔻.𝟙
__ :
identity : {o : Obj} Arr o o
identity = .identity , 𝔻.identity
_<<<_ :
{a b c : Obj}
Arr b c
Arr a b
Arr a c
__ = λ { (bc∈C , bc∈D) (ab∈C , ab∈D) [ bc∈C ab∈C ] , 𝔻 [ bc∈D ab∈D ]}
_<<<_ = λ { (bc∈C , bc∈D) (ab∈C , ab∈D) [ bc∈C ab∈C ] , 𝔻 [ bc∈D ab∈D ]}
rawProduct : RawCategory '
RawCategory.Object rawProduct = Obj
RawCategory.Arrow rawProduct = Arr
RawCategory.𝟙 rawProduct = 𝟙
RawCategory._∘_ rawProduct = _∘_
RawCategory.identity rawProduct = identity
RawCategory._<<<_ rawProduct = _<<<_
open RawCategory rawProduct
arrowsAreSets : ArrowsAreSets
arrowsAreSets = setSig {sA = .arrowsAreSets} {sB = λ x 𝔻.arrowsAreSets}
isIdentity : IsIdentity 𝟙
isIdentity : IsIdentity identity
isIdentity
= Σ≡ (fst .isIdentity) (fst 𝔻.isIdentity)
, Σ≡ (snd .isIdentity) (snd 𝔻.isIdentity)
isPreCategory : IsPreCategory rawProduct
IsPreCategory.isAssociative isPreCategory = Σ≡ .isAssociative 𝔻.isAssociative
IsPreCategory.isIdentity isPreCategory = isIdentity
IsPreCategory.arrowsAreSets isPreCategory = arrowsAreSets
postulate univalent : Univalence.Univalent isIdentity
instance
isCategory : IsCategory rawProduct
IsCategory.isAssociative isCategory = Σ≡ .isAssociative 𝔻.isAssociative
IsCategory.isIdentity isCategory = isIdentity
IsCategory.arrowsAreSets isCategory = arrowsAreSets
IsCategory.isPreCategory isCategory = isPreCategory
IsCategory.univalent isCategory = univalent
object : Category '
Category.raw object = rawProduct
Category.isCategory object = isCategory
proj₁ : Functor object
proj₁ = record
fstF : Functor object
fstF = record
{ raw = record
{ omap = fst ; fmap = fst }
; isFunctor = record
{ isIdentity = refl ; isDistributive = refl }
}
proj₂ : Functor object 𝔻
proj₂ = record
sndF : Functor object 𝔻
sndF = record
{ raw = record
{ omap = snd ; fmap = snd }
; isFunctor = record
@ -136,17 +120,27 @@ module CatProduct { ' : Level} ( 𝔻 : Category ') where
open module x = Functor x₁
open module x = Functor x₂
isUniqL : F[ proj₁ x ] x₁
isUniqL : F[ fstF x ] x₁
isUniqL = Functor≡ refl
isUniqR : F[ proj₂ x ] x₂
isUniqR : F[ sndF x ] x₂
isUniqR = Functor≡ refl
isUniq : F[ proj₁ x ] x₁ × F[ proj₂ x ] x₂
isUniq : F[ fstF x ] x₁ × F[ sndF x ] x₂
isUniq = isUniqL , isUniqR
isProduct : ∃![ x ] (F[ proj₁ x ] x₁ × F[ proj₂ x ] x₂)
isProduct = x , isUniq
isProduct : ∃![ x ] (F[ fstF x ] x₁ × F[ sndF x ] x₂)
isProduct = x , isUniq , uq
where
module _ {y : Functor X object} (eq : F[ fstF y ] x₁ × F[ sndF y ] x₂) where
omapEq : Functor.omap x Functor.omap y
omapEq = {!!}
-- fmapEq : (λ i → {!{A B : ?} → Arrow A B → 𝔻 [ ? A , ? B ]!}) [ Functor.fmap x ≡ Functor.fmap y ]
-- fmapEq = {!!}
rawEq : Functor.raw x Functor.raw y
rawEq = {!!}
uq : x y
uq = Functor≡ rawEq
module _ { ' : Level} (unprovable : IsCategory (RawCat ')) where
private
@ -158,8 +152,8 @@ module _ { ' : Level} (unprovable : IsCategory (RawCat ')) where
rawProduct : RawProduct Cat 𝔻
RawProduct.object rawProduct = P.object
RawProduct.proj₁ rawProduct = P.proj₁
RawProduct.proj₂ rawProduct = P.proj₂
RawProduct.fst rawProduct = P.fstF
RawProduct.snd rawProduct = P.sndF
isProduct : IsProduct Cat _ _ rawProduct
IsProduct.ump isProduct = P.isProduct
@ -175,6 +169,9 @@ module _ { ' : Level} (unprovable : IsCategory (RawCat ')) where
-- | The category of categories have expoentntials - and because it has products
-- it is therefory also cartesian closed.
module CatExponential { : Level} ( 𝔻 : Category ) where
open Cat.Category.NaturalTransformation 𝔻
renaming (identity to identityNT)
using ()
private
module = Category
module 𝔻 = Category 𝔻
@ -189,8 +186,8 @@ module CatExponential { : Level} ( 𝔻 : Category ) where
object = Fun
module _ {dom cod : Functor 𝔻 × .Object} where
open Σ dom renaming (proj₁ to F ; proj₂ to A)
open Σ cod renaming (proj₁ to G ; proj₂ to B)
open Σ dom renaming (fst to F ; snd to A)
open Σ cod renaming (fst to G ; snd to B)
private
module F = Functor F
module G = Functor G
@ -207,23 +204,23 @@ module CatExponential { : Level} ( 𝔻 : Category ) where
open CatProduct renaming (object to _⊗_) using ()
module _ {c : Functor 𝔻 × .Object} where
open Σ c renaming (proj₁ to F ; proj₂ to C)
open Σ c renaming (fst to F ; snd to C)
ident : fmap {c} {c} (NT.identity F , .𝟙 {A = snd c}) 𝔻.𝟙
ident : fmap {c} {c} (identityNT F , .identity {A = snd c}) 𝔻.identity
ident = begin
fmap {c} {c} (Category.𝟙 (object ) {c}) ≡⟨⟩
fmap {c} {c} (idN F , .𝟙) ≡⟨⟩
𝔻 [ identityTrans F C F.fmap .𝟙 ] ≡⟨⟩
𝔻 [ 𝔻.𝟙 F.fmap .𝟙 ] ≡⟨ 𝔻.leftIdentity
F.fmap .𝟙 ≡⟨ F.isIdentity
𝔻.𝟙
fmap {c} {c} (Category.identity (object ) {c}) ≡⟨⟩
fmap {c} {c} (idN F , .identity) ≡⟨⟩
𝔻 [ identityTrans F C F.fmap .identity ] ≡⟨⟩
𝔻 [ 𝔻.identity F.fmap .identity ] ≡⟨ 𝔻.leftIdentity
F.fmap .identity ≡⟨ F.isIdentity
𝔻.identity
where
module F = Functor F
module _ {F×A G×B H×C : Functor 𝔻 × .Object} where
open Σ F×A renaming (proj₁ to F ; proj₂ to A)
open Σ G×B renaming (proj₁ to G ; proj₂ to B)
open Σ H×C renaming (proj₁ to H ; proj₂ to C)
open Σ F×A renaming (fst to F ; snd to A)
open Σ G×B renaming (fst to G ; snd to B)
open Σ H×C renaming (fst to H ; snd to C)
private
module F = Functor F
module G = Functor G
@ -232,14 +229,14 @@ module CatExponential { : Level} ( 𝔻 : Category ) where
module _
{θ×f : NaturalTransformation F G × [ A , B ]}
{η×g : NaturalTransformation G H × [ B , C ]} where
open Σ θ×f renaming (proj₁ to θNT ; proj₂ to f)
open Σ θNT renaming (proj₁ to θ ; proj₂ to θNat)
open Σ η×g renaming (proj₁ to ηNT ; proj₂ to g)
open Σ ηNT renaming (proj₁ to η ; proj₂ to ηNat)
open Σ θ×f renaming (fst to θNT ; snd to f)
open Σ θNT renaming (fst to θ ; snd to θNat)
open Σ η×g renaming (fst to ηNT ; snd to g)
open Σ ηNT renaming (fst to η ; snd to ηNat)
private
ηθNT : NaturalTransformation F H
ηθNT = NT[_∘_] {F} {G} {H} ηNT θNT
open Σ ηθNT renaming (proj₁ to ηθ ; proj₂ to ηθNat)
open Σ ηθNT renaming (fst to ηθ ; snd to ηθNat)
isDistributive :
𝔻 [ 𝔻 [ η C θ C ] F.fmap ( [ g f ] ) ]
@ -283,18 +280,18 @@ module CatExponential { : Level} ( 𝔻 : Category ) where
: Functor 𝔸 object Functor
Functor (𝔸 ) (object )
transpose : Functor 𝔸 object
eq : F[ eval (parallelProduct transpose (identity {C = })) ] F
eq : F[ eval (parallelProduct transpose (Functors.identity { = })) ] F
-- eq : F[ :eval: ∘ {!!} ] ≡ F
-- eq : Cat [ :eval: ∘ (HasProducts._|×|_ hasProducts transpose (𝟙 Cat {o = })) ] ≡ F
-- eq : Cat [ :eval: ∘ (HasProducts._|×|_ hasProducts transpose (identity Cat {o = })) ] ≡ F
-- eq' : (Cat [ :eval: ∘
-- (record { product = product } HasProducts.|×| transpose)
-- (𝟙 Cat)
-- (identity Cat)
-- ])
-- ≡ F
-- For some reason after `e8215b2c051062c6301abc9b3f6ec67106259758`
-- `catTranspose` makes Agda hang. catTranspose : ∃![ F~ ] (Cat [
-- :eval: (parallelProduct F~ (𝟙 Cat {o = }))] F) catTranspose =
-- :eval: (parallelProduct F~ (identity Cat {o = }))] F) catTranspose =
-- transpose , eq
-- We don't care about filling out the holes below since they are anyways hidden
@ -318,8 +315,8 @@ module _ ( : Level) (unprovable : IsCategory (RawCat )) where
exponent : Exponential Cat 𝔻
exponent = record
{ obj = CatExp.object
; eval = eval
; isExponential = isExponential
; eval = {!eval!}
; isExponential = {!isExponential!}
}
hasExponentials : HasExponentials Cat

View file

@ -7,7 +7,6 @@ open import Data.Bool hiding (T)
open import Data.Sum hiding ([_,_])
open import Data.Unit
open import Data.Empty
open import Function
open import Relation.Nullary
open import Relation.Nullary.Decidable
@ -19,7 +18,7 @@ open import Cat.Category.Functor
-- See section 6.8 in Huber's thesis for details on how to implement the
-- categorical version of CTT
open Category hiding (__)
open Category hiding (_<<<_)
open Functor
module _ { ' : Level} (Ns : Set ) where
@ -67,8 +66,8 @@ module _ { ' : Level} (Ns : Set ) where
Raw : RawCategory -- o (lsuc lzero ⊔ o)
Raw.Object Raw = FiniteDecidableSubset
Raw.Arrow Raw = Hom
Raw.𝟙 Raw {o} = inj₁ , λ { (i , ii) (j , jj) eq Σ≡ eq {!refl!} }
Raw.__ Raw = {!!}
Raw.identity Raw {o} = inj₁ , λ { (i , ii) (j , jj) eq Σ≡ eq {!refl!} }
Raw._<<<_ Raw = {!!}
postulate IsCategory : IsCategory Raw

View file

@ -25,21 +25,21 @@ module _ {a b : Level} where
private
module T = Functor T
Type : (Γ : .Object) Set a
Type Γ = proj₁ (proj₁ (T.omap Γ))
Type Γ = fst (fst (T.omap Γ))
module _ {Γ : .Object} {A : Type Γ} where
-- module _ {A B : Object } {γ : [ A , B ]} where
-- k : Σ (proj₁ (omap T B) → proj₁ (omap T A))
-- k : Σ (fst (omap T B) → fst (omap T A))
-- (λ f →
-- {x : proj₁ (omap T B)} →
-- proj₂ (omap T B) x → proj₂ (omap T A) (f x))
-- {x : fst (omap T B)} →
-- snd (omap T B) x → snd (omap T A) (f x))
-- k = T.fmap γ
-- k₁ : proj₁ (omap T B) → proj₁ (omap T A)
-- k₁ = proj₁ k
-- k₂ : ({x : proj₁ (omap T B)} →
-- proj₂ (omap T B) x → proj₂ (omap T A) (k₁ x))
-- k₂ = proj₂ k
-- k₁ : fst (omap T B) → fst (omap T A)
-- k₁ = fst k
-- k₂ : ({x : fst (omap T B)} →
-- snd (omap T B) x → snd (omap T A) (k₁ x))
-- k₂ = snd k
record ContextComprehension : Set (a b) where
field

View file

@ -2,62 +2,60 @@
module Cat.Categories.Fam where
open import Cat.Prelude
import Function
open import Cat.Category
module _ (a b : Level) where
private
Object = Σ[ hA hSet a ] (proj₁ hA hSet b)
Object = Σ[ hA hSet a ] (fst hA hSet b)
Arr : Object Object Set (a b)
Arr ((A , _) , B) ((A' , _) , B') = Σ[ f (A A') ] ({x : A} proj₁ (B x) proj₁ (B' (f x)))
𝟙 : {A : Object} Arr A A
proj₁ 𝟙 = λ x x
proj₂ 𝟙 = λ b b
__ : {a b c : Object} Arr b c Arr a b Arr a c
(g , g') (f , f') = g Function. f , g' Function. f'
Arr ((A , _) , B) ((A' , _) , B') = Σ[ f (A A') ] ({x : A} fst (B x) fst (B' (f x)))
identity : {A : Object} Arr A A
fst identity = λ x x
snd identity = λ b b
_<<<_ : {a b c : Object} Arr b c Arr a b Arr a c
(g , g') <<< (f , f') = g f , g' f'
RawFam : RawCategory (lsuc (a b)) (a b)
RawFam = record
{ Object = Object
; Arrow = Arr
; 𝟙 = λ { {A} 𝟙 {A = A}}
; __ = λ {a b c} __ {a} {b} {c}
; identity = λ { {A} identity {A = A}}
; _<<<_ = λ {a b c} _<<<_ {a} {b} {c}
}
open RawCategory RawFam hiding (Object ; 𝟙)
open RawCategory RawFam hiding (Object ; identity)
isAssociative : IsAssociative
isAssociative = Σ≡ refl refl
isIdentity : IsIdentity λ { {A} 𝟙 {A} }
isIdentity : IsIdentity λ { {A} identity {A} }
isIdentity = (Σ≡ refl refl) , Σ≡ refl refl
open import Cubical.NType.Properties
open import Cubical.Sigma
instance
isCategory : IsCategory RawFam
isCategory = record
{ isAssociative = λ {A} {B} {C} {D} {f} {g} {h} isAssociative {A} {B} {C} {D} {f} {g} {h}
; isIdentity = λ {A} {B} {f} isIdentity {A} {B} {f = f}
; arrowsAreSets = λ {
{((A , hA) , famA)}
{((B , hB) , famB)}
setSig
isPreCategory : IsPreCategory RawFam
IsPreCategory.isAssociative isPreCategory
{A} {B} {C} {D} {f} {g} {h} = isAssociative {A} {B} {C} {D} {f} {g} {h}
IsPreCategory.isIdentity isPreCategory
{A} {B} {f} = isIdentity {A} {B} {f = f}
IsPreCategory.arrowsAreSets isPreCategory
{(A , hA) , famA} {(B , hB) , famB}
= setSig
{sA = setPi λ _ hB}
{sB = λ f
let
helpr : isSet ((a : A) proj₁ (famA a) proj₁ (famB (f a)))
helpr = setPi λ a setPi λ _ proj₂ (famB (f a))
helpr : isSet ((a : A) fst (famA a) fst (famB (f a)))
helpr = setPi λ a setPi λ _ snd (famB (f a))
-- It's almost like above, but where the first argument is
-- implicit.
res : isSet ({a : A} proj₁ (famA a) proj₁ (famB (f a)))
res : isSet ({a : A} fst (famA a) fst (famB (f a)))
res = {!!}
in res
}
}
; univalent = {!!}
}
isCategory : IsCategory RawFam
IsCategory.isPreCategory isCategory = isPreCategory
IsCategory.univalent isCategory = {!!}
Fam : Category (lsuc (a b)) (a b)
Category.raw Fam = RawFam
Category.isCategory Fam = isCategory

View file

@ -1,4 +1,4 @@
{-# OPTIONS --allow-unsolved-metas #-}
{-# OPTIONS --allow-unsolved-metas --cubical #-}
module Cat.Categories.Free where
open import Cat.Prelude hiding (Path ; empty)
@ -29,8 +29,8 @@ module _ {a b : Level} ( : Category a b) where
RawFree : RawCategory a (a b)
RawCategory.Object RawFree = .Object
RawCategory.Arrow RawFree = Path .Arrow
RawCategory.𝟙 RawFree = empty
RawCategory.__ RawFree = concatenate
RawCategory.identity RawFree = empty
RawCategory._<<<_ RawFree = concatenate
open RawCategory RawFree
@ -52,7 +52,7 @@ module _ {a b : Level} ( : Category a b) where
ident-l : {A} {B} {p : Path .Arrow A B} concatenate empty p p
ident-l = refl
isIdentity : IsIdentity 𝟙
isIdentity : IsIdentity identity
isIdentity = ident-l , ident-r
open Univalence isIdentity
@ -61,16 +61,20 @@ module _ {a b : Level} ( : Category a b) where
arrowsAreSets : isSet (Path .Arrow A B)
arrowsAreSets a b p q = {!!}
eqv : isEquiv (A B) (A B) (Univalence.id-to-iso isIdentity A B)
isPreCategory : IsPreCategory RawFree
IsPreCategory.isAssociative isPreCategory {f = f} {g} {h} = isAssociative {r = f} {g} {h}
IsPreCategory.isIdentity isPreCategory = isIdentity
IsPreCategory.arrowsAreSets isPreCategory = arrowsAreSets
module _ {A B : .Object} where
eqv : isEquiv (A B) (A B) (Univalence.idToIso isIdentity A B)
eqv = {!!}
univalent : Univalent
univalent = eqv
isCategory : IsCategory RawFree
IsCategory.isAssociative isCategory {f = f} {g} {h} = isAssociative {r = f} {g} {h}
IsCategory.isIdentity isCategory = isIdentity
IsCategory.arrowsAreSets isCategory = arrowsAreSets
IsCategory.isPreCategory isCategory = isPreCategory
IsCategory.univalent isCategory = univalent
Free : Category _ _

View file

@ -1,181 +1,218 @@
{-# OPTIONS --allow-unsolved-metas --cubical #-}
{-# OPTIONS --allow-unsolved-metas --cubical --caching #-}
module Cat.Categories.Fun where
open import Cat.Prelude
open import Cat.Equivalence
open import Cat.Category
open import Cat.Category.Functor hiding (identity)
open import Cat.Category.NaturalTransformation
open import Cat.Category.Functor
import Cat.Category.NaturalTransformation
as NaturalTransformation
module Fun {c c' d d' : Level} ( : Category c c') (𝔻 : Category d d') where
module NT = NaturalTransformation 𝔻
open NT public
open NaturalTransformation 𝔻 public hiding (module Properties)
private
module = Category
module 𝔻 = Category 𝔻
private
module _ {A B C D : Functor 𝔻} {θ' : NaturalTransformation A B}
{η' : NaturalTransformation B C} {ζ' : NaturalTransformation C D} where
θ = proj₁ θ'
η = proj₁ η'
ζ = proj₁ ζ'
θNat = proj₂ θ'
ηNat = proj₂ η'
ζNat = proj₂ ζ'
L : NaturalTransformation A D
L = (NT[_∘_] {A} {C} {D} ζ' (NT[_∘_] {A} {B} {C} η' θ'))
R : NaturalTransformation A D
R = (NT[_∘_] {A} {B} {D} (NT[_∘_] {B} {C} {D} ζ' η') θ')
_g⊕f_ = NT[_∘_] {A} {B} {C}
_h⊕g_ = NT[_∘_] {B} {C} {D}
isAssociative : L R
isAssociative = lemSig (naturalIsProp {F = A} {D})
L R (funExt (λ x 𝔻.isAssociative))
private
module _ {A B : Functor 𝔻} {f : NaturalTransformation A B} where
allNatural = naturalIsProp {F = A} {B}
f' = proj₁ f
eq-r : C (𝔻 [ f' C identityTrans A C ]) f' C
eq-r C = begin
𝔻 [ f' C identityTrans A C ] ≡⟨⟩
𝔻 [ f' C 𝔻.𝟙 ] ≡⟨ 𝔻.rightIdentity
f' C
eq-l : C (𝔻 [ identityTrans B C f' C ]) f' C
eq-l C = 𝔻.leftIdentity
ident-r : (NT[_∘_] {A} {A} {B} f (NT.identity A)) f
ident-r = lemSig allNatural _ _ (funExt eq-r)
ident-l : (NT[_∘_] {A} {B} {B} (NT.identity B) f) f
ident-l = lemSig allNatural _ _ (funExt eq-l)
isIdentity
: (NT[_∘_] {A} {B} {B} (NT.identity B) f) f
× (NT[_∘_] {A} {A} {B} f (NT.identity A)) f
isIdentity = ident-l , ident-r
module _ where
-- Functor categories. Objects are functors, arrows are natural transformations.
RawFun : RawCategory (c c' d d') (c c' d')
RawFun = record
{ Object = Functor 𝔻
; Arrow = NaturalTransformation
; 𝟙 = λ {F} NT.identity F
; _∘_ = λ {F G H} NT[_∘_] {F} {G} {H}
}
raw : RawCategory (c c' d d') (c c' d')
RawCategory.Object raw = Functor 𝔻
RawCategory.Arrow raw = NaturalTransformation
RawCategory.identity raw {F} = identity F
RawCategory._<<<_ raw {F} {G} {H} = NT[_∘_] {F} {G} {H}
open RawCategory RawFun
open Univalence (λ {A} {B} {f} isIdentity {A} {B} {f})
module _ where
open RawCategory raw hiding (identity)
open NaturalTransformation.Properties 𝔻
isPreCategory : IsPreCategory raw
IsPreCategory.isAssociative isPreCategory {A} {B} {C} {D} = isAssociative {A} {B} {C} {D}
IsPreCategory.isIdentity isPreCategory {A} {B} = isIdentity {A} {B}
IsPreCategory.arrowsAreSets isPreCategory {F} {G} = naturalTransformationIsSet {F} {G}
open IsPreCategory isPreCategory hiding (identity)
module _ {F G : Functor 𝔻} (p : F G) where
private
module F = Functor F
module G = Functor G
p-omap : F.omap G.omap
p-omap = cong Functor.omap p
pp : {C : .Object} 𝔻 [ Functor.omap F C , Functor.omap F C ] 𝔻 [ Functor.omap F C , Functor.omap G C ]
pp {C} = cong (λ f 𝔻 [ Functor.omap F C , f C ]) p-omap
module _ {C : .Object} where
p* : F.omap C G.omap C
p* = cong (_$ C) p-omap
iso : F.omap C 𝔻.≊ G.omap C
iso = 𝔻.idToIso _ _ p*
open Σ iso renaming (fst to f→g) public
open Σ (snd iso) renaming (fst to g→f ; snd to inv) public
lem : coe (pp {C}) 𝔻.identity f→g
lem = trans (𝔻.9-1-9-right {b = Functor.omap F C} 𝔻.identity p*) 𝔻.rightIdentity
idToNatTrans : NaturalTransformation F G
idToNatTrans = (λ C coe pp 𝔻.identity) , λ f begin
coe pp 𝔻.identity 𝔻.<<< F.fmap f ≡⟨ cong (𝔻._<<< F.fmap f) lem
-- Just need to show that f→g is a natural transformation
-- I know that it has an inverse; g→f
f→g 𝔻.<<< F.fmap f ≡⟨ {!lem!}
G.fmap f 𝔻.<<< f→g ≡⟨ cong (G.fmap f 𝔻.<<<_) (sym lem)
G.fmap f 𝔻.<<< coe pp 𝔻.identity
module _ {A B : Functor 𝔻} where
module A = Functor A
module B = Functor B
module _ (p : A B) where
omapP : A.omap B.omap
omapP i = Functor.omap (p i)
coerceAB : {X} 𝔻 [ A.omap X , A.omap X ] 𝔻 [ A.omap X , B.omap X ]
coerceAB {X} = cong (λ φ 𝔻 [ A.omap X , φ X ]) omapP
-- The transformation will be the identity on 𝔻. Such an arrow has the
-- type `A.omap A → A.omap A`. Which we can coerce to have the type
-- `A.omap → B.omap` since `A` and `B` are equal.
coe𝟙 : Transformation A B
coe𝟙 X = coe coerceAB 𝔻.𝟙
module _ {a b : .Object} (f : [ a , b ]) where
nat' : 𝔻 [ coe𝟙 b A.fmap f ] 𝔻 [ B.fmap f coe𝟙 a ]
nat' = begin
(𝔻 [ coe𝟙 b A.fmap f ]) ≡⟨ {!!}
(𝔻 [ B.fmap f coe𝟙 a ])
transs : (i : I) Transformation A (p i)
transs = {!!}
natt : (i : I) Natural A (p i) {!!}
natt = {!!}
t : Natural A B coe𝟙
t = coe c (identityNatural A)
module _ (iso : A B) where
omapEq : A.omap B.omap
omapEq = funExt eq
where
c : Natural A A (identityTrans A) Natural A B coe𝟙
c = begin
Natural A A (identityTrans A) ≡⟨ (λ x {!natt ?!})
Natural A B coe𝟙
-- cong (λ φ → {!Natural A A (identityTrans A)!}) {!!}
module _ (C : .Object) where
f : 𝔻.Arrow (A.omap C) (B.omap C)
f = fst (fst iso) C
g : 𝔻.Arrow (B.omap C) (A.omap C)
g = fst (fst (snd iso)) C
inv : 𝔻.IsInverseOf f g
inv
= ( begin
g 𝔻.<<< f ≡⟨ cong (λ x fst x $ C) (fst (snd (snd iso)))
𝔻.identity
)
, ( begin
f 𝔻.<<< g ≡⟨ cong (λ x fst x $ C) (snd (snd (snd iso)))
𝔻.identity
)
isoC : A.omap C 𝔻.≊ B.omap C
isoC = f , g , inv
eq : A.omap C B.omap C
eq = 𝔻.isoToId isoC
k : Natural A A (identityTrans A) Natural A B coe𝟙
k n {a} {b} f = res
U : (F : .Object 𝔻.Object) Set _
U F = {A B : .Object} [ A , B ] 𝔻 [ F A , F B ]
module _
(omap : .Object 𝔻.Object)
(p : A.omap omap)
where
res : (𝔻 [ coe𝟙 b A.fmap f ]) (𝔻 [ B.fmap f coe𝟙 a ])
res = {!!}
nat : Natural A B coe𝟙
nat = nat'
fromEq : NaturalTransformation A B
fromEq = coe𝟙 , nat
module _ {A B : Functor 𝔻} where
obverse : A B A B
obverse p = res
D : Set _
D = ( fmap : U omap)
( let
raw-B : RawFunctor 𝔻
raw-B = record { omap = omap ; fmap = fmap }
)
(isF-B' : IsFunctor 𝔻 raw-B)
( let
B' : Functor 𝔻
B' = record { raw = raw-B ; isFunctor = isF-B' }
)
(iso' : A B') PathP (λ i U (p i)) A.fmap fmap
-- D : Set _
-- D = PathP (λ i → U (p i)) A.fmap fmap
-- eeq : (λ f → A.fmap f) ≡ fmap
-- eeq = funExtImp (λ A → funExtImp (λ B → funExt (λ f → isofmap {A} {B} f)))
-- where
-- module _ {X : .Object} {Y : .Object} (f : [ X , Y ]) where
-- isofmap : A.fmap f ≡ fmap f
-- isofmap = {!ap!}
d : D A.omap refl
d = res
where
ob : Arrow A B
ob = fromEq p
re : Arrow B A
re = fromEq (sym p)
vr : _∘_ {A = A} {B} {A} re ob 𝟙 {A}
vr = {!!}
rv : _∘_ {A = B} {A} {B} ob re 𝟙 {B}
rv = {!!}
isInverse : IsInverseOf {A} {B} ob re
isInverse = vr , rv
iso : Isomorphism {A} {B} ob
iso = re , isInverse
res : A B
res = ob , iso
module _
( fmap : U A.omap )
( let
raw-B : RawFunctor 𝔻
raw-B = record { omap = A.omap ; fmap = fmap }
)
( isF-B' : IsFunctor 𝔻 raw-B )
( let
B' : Functor 𝔻
B' = record { raw = raw-B ; isFunctor = isF-B' }
)
( iso' : A B' )
where
module _ {X Y : .Object} (f : [ X , Y ]) where
step : {!!} 𝔻.≊ {!!}
step = {!!}
resres : A.fmap {X} {Y} f fmap {X} {Y} f
resres = {!!}
res : PathP (λ i U A.omap) A.fmap fmap
res i {X} {Y} f = resres f i
reverse : A B A B
reverse iso = {!!}
fmapEq : PathP (λ i U (omapEq i)) A.fmap B.fmap
fmapEq = pathJ D d B.omap omapEq B.fmap B.isFunctor iso
ve-re : (y : A B) obverse (reverse y) y
ve-re = {!!}
rawEq : A.raw B.raw
rawEq i = record { omap = omapEq i ; fmap = fmapEq i }
re-ve : (x : A B) reverse (obverse x) x
re-ve = {!!}
private
f : (A B) (A B)
f p = idToNatTrans p , idToNatTrans (sym p) , NaturalTransformation≡ A A (funExt (λ C {!!})) , {!!}
g : (A B) (A B)
g = Functor≡ rawEq
inv : AreInverses f g
inv = {!funExt λ p → ?!} , {!!}
done : isEquiv (A B) (A B) (Univalence.id-to-iso (λ { {A} {B} isIdentity {A} {B}}) A B)
done = {!gradLemma obverse reverse ve-re re-ve!}
iso : (A B) (A B)
iso = f , g , inv
univ : (A B) (A B)
univ = fromIsomorphism _ _ iso
-- There used to be some work-in-progress on this theorem, please go back to
-- this point in time to see it:
--
-- commit 6b7d66b7fc936fe3674b2fd9fa790bd0e3fec12f
-- Author: Frederik Hanghøj Iversen <fhi.1990@gmail.com>
-- Date: Fri Apr 13 15:26:46 2018 +0200
univalent : Univalent
univalent = done
univalent = univalenceFrom≃ univ
instance
isCategory : IsCategory RawFun
isCategory = record
{ isAssociative = λ {A B C D} isAssociative {A} {B} {C} {D}
; isIdentity = λ {A B} isIdentity {A} {B}
; arrowsAreSets = λ {F} {G} naturalTransformationIsSet {F} {G}
; univalent = univalent
}
isCategory : IsCategory raw
IsCategory.isPreCategory isCategory = isPreCategory
IsCategory.univalent isCategory = univalent
Fun : Category (c c' d d') (c c' d')
Category.raw Fun = RawFun
Category.raw Fun = raw
Category.isCategory Fun = isCategory
module _ { ' : Level} ( : Category ') where
private
open import Cat.Categories.Sets
open NaturalTransformation (opposite ) (𝓢𝓮𝓽 ')
module K = Fun (opposite ) (𝓢𝓮𝓽 ')
module F = Category K.Fun
-- Restrict the functors to Presheafs.
rawPresh : RawCategory ( lsuc ') ( ')
rawPresh = record
raw : RawCategory ( lsuc ') ( ')
raw = record
{ Object = Presheaf
; Arrow = NaturalTransformation
; 𝟙 = λ {F} identity F
; __ = λ {F G H} NT[_∘_] {F = F} {G = G} {H = H}
; identity = λ {F} identity F
; _<<<_ = λ {F G H} NT[_∘_] {F = F} {G = G} {H = H}
}
instance
isCategory : IsCategory rawPresh
isCategory = Fun.isCategory _ _
Presh : Category ( lsuc ') ( ')
Category.raw Presh = rawPresh
Category.isCategory Presh = isCategory
-- isCategory : IsCategory raw
-- isCategory = record
-- { isAssociative =
-- λ{ {A} {B} {C} {D} {f} {g} {h}
-- → F.isAssociative {A} {B} {C} {D} {f} {g} {h}
-- }
-- ; isIdentity =
-- λ{ {A} {B} {f}
-- → F.isIdentity {A} {B} {f}
-- }
-- ; arrowsAreSets =
-- λ{ {A} {B}
-- → F.arrowsAreSets {A} {B}
-- }
-- ; univalent =
-- λ{ {A} {B}
-- → F.univalent {A} {B}
-- }
-- }
-- Presh : Category ( ⊔ lsuc ') (')
-- Category.raw Presh = raw
-- Category.isCategory Presh = isCategory

View file

@ -1,8 +1,7 @@
{-# OPTIONS --cubical --allow-unsolved-metas #-}
module Cat.Categories.Rel where
open import Cat.Prelude renaming (proj₁ to fst ; proj₂ to snd)
open import Function
open import Cat.Prelude hiding (Rel)
open import Cat.Category
@ -153,14 +152,15 @@ RawRel : RawCategory (lsuc lzero) (lsuc lzero)
RawRel = record
{ Object = Set
; Arrow = λ S R Subset (S × R)
; 𝟙 = λ {S} Diag S
; __ = λ {A B C} S R λ {( a , c ) Σ[ b B ] ( (a , b) R × (b , c) S )}
; identity = λ {S} Diag S
; _<<<_ = λ {A B C} S R λ {( a , c ) Σ[ b B ] ( (a , b) R × (b , c) S )}
}
RawIsCategoryRel : IsCategory RawRel
RawIsCategoryRel = record
{ isAssociative = funExt is-isAssociative
; isIdentity = funExt ident-l , funExt ident-r
; arrowsAreSets = {!!}
; univalent = {!!}
}
isPreCategory : IsPreCategory RawRel
IsPreCategory.isAssociative isPreCategory = funExt is-isAssociative
IsPreCategory.isIdentity isPreCategory = funExt ident-l , funExt ident-r
IsPreCategory.arrowsAreSets isPreCategory = {!!}
Rel : PreCategory RawRel
PreCategory.isPreCategory Rel = isPreCategory

View file

@ -1,23 +1,13 @@
-- | The category of homotopy sets
{-# OPTIONS --allow-unsolved-metas --cubical --caching #-}
{-# OPTIONS --cubical --caching #-}
module Cat.Categories.Sets where
open import Cat.Prelude hiding (_≃_)
import Data.Product
open import Function using (_∘_ ; _∘_)
open import Cubical.Univalence using (univalence ; con ; _≃_ ; idtoeqv ; ua)
open import Cat.Prelude as P
open import Cat.Category
open import Cat.Category.Functor
open import Cat.Category.Product
open import Cat.Wishlist
open import Cat.Equivalence as Eqv using (AreInverses ; module Equiv ; module NoEta)
open NoEta
module Equivalence = Equivalence
open import Cat.Equivalence
_⊙_ : {a b c : Level} {A : Set a} {B : Set b} {C : Set c} (A B) (B C) A C
eqA eqB = Equivalence.compose eqA eqB
@ -27,268 +17,46 @@ sym≃ = Equivalence.symmetry
infixl 10 _⊙_
module _ { : Level} {A : Set } {a : A} where
id-coe : coe refl a a
id-coe = begin
coe refl a ≡⟨⟩
pathJ (λ y x A) _ A refl ≡⟨ pathJprop {x = a} (λ y x A) _
_ ≡⟨ pathJprop {x = a} (λ y x A) _
a
module _ { : Level} {A B : Set } {a : A} where
inv-coe : (p : A B) coe (sym p) (coe p a) a
inv-coe p =
let
D : (y : Set ) _ y Set _
D _ q = coe (sym q) (coe q a) a
d : D A refl
d = begin
coe (sym refl) (coe refl a) ≡⟨⟩
coe refl (coe refl a) ≡⟨ id-coe
coe refl a ≡⟨ id-coe
a
in pathJ D d B p
inv-coe' : (p : B A) coe p (coe (sym p) a) a
inv-coe' p =
let
D : (y : Set ) _ y Set _
D _ q = coe (sym q) (coe q a) a
k : coe p (coe (sym p) a) a
k = pathJ D (trans id-coe id-coe) B (sym p)
in k
module _ ( : Level) where
private
SetsRaw : RawCategory (lsuc )
RawCategory.Object SetsRaw = hSet
RawCategory.Arrow SetsRaw (T , _) (U , _) = T U
RawCategory.𝟙 SetsRaw = Function.id
RawCategory.__ SetsRaw = Function._∘_
RawCategory.identity SetsRaw = idFun _
RawCategory._<<<_ SetsRaw = _∘_
open RawCategory SetsRaw hiding (_∘_)
module _ where
private
open RawCategory SetsRaw hiding (_<<<_)
isIdentity : IsIdentity Function.id
proj₁ isIdentity = funExt λ _ refl
proj₂ isIdentity = funExt λ _ refl
open Univalence (λ {A} {B} {f} isIdentity {A} {B} {f})
isIdentity : IsIdentity (idFun _)
fst isIdentity = funExt λ _ refl
snd isIdentity = funExt λ _ refl
arrowsAreSets : ArrowsAreSets
arrowsAreSets {B = (_ , s)} = setPi λ _ s
isIso = Eqv.Isomorphism
module _ {hA hB : hSet } where
open Σ hA renaming (proj₁ to A ; proj₂ to sA)
open Σ hB renaming (proj₁ to B ; proj₂ to sB)
lem1 : (f : A B) isSet A isSet B isProp (isIso f)
lem1 f sA sB = res
where
module _ (x y : isIso f) where
module x = Σ x renaming (proj₁ to inverse ; proj₂ to areInverses)
module y = Σ y renaming (proj₁ to inverse ; proj₂ to areInverses)
module xA = AreInverses x.areInverses
module yA = AreInverses y.areInverses
-- I had a lot of difficulty using the corresponding proof where
-- AreInverses is defined. This is sadly a bit anti-modular. The
-- reason for my troubles is probably related to the type of objects
-- being hSet's rather than sets.
p : {f} g isProp (AreInverses {A = A} {B} f g)
p {f} g xx yy i = record
{ verso-recto = ve-re
; recto-verso = re-ve
}
where
module xxA = AreInverses xx
module yyA = AreInverses yy
ve-re : g f Function.id
ve-re = arrowsAreSets {A = hA} {B = hA} _ _ xxA.verso-recto yyA.verso-recto i
re-ve : f g Function.id
re-ve = arrowsAreSets {A = hB} {B = hB} _ _ xxA.recto-verso yyA.recto-verso i
1eq : x.inverse y.inverse
1eq = begin
x.inverse ≡⟨⟩
x.inverse Function.id ≡⟨ cong (λ φ x.inverse φ) (sym yA.recto-verso)
x.inverse (f y.inverse) ≡⟨⟩
(x.inverse f) y.inverse ≡⟨ cong (λ φ φ y.inverse) xA.verso-recto
Function.id y.inverse ≡⟨⟩
y.inverse
2eq : (λ i AreInverses f (1eq i)) [ x.areInverses y.areInverses ]
2eq = lemPropF p 1eq
res : x y
res i = 1eq i , 2eq i
module _ {a b : Level} {A : Set a} {P : A Set b} where
lem2 : ((x : A) isProp (P x)) (p q : Σ A P)
(p q) (proj₁ p proj₁ q)
lem2 pA p q = fromIsomorphism iso
where
f : {p q} p q proj₁ p proj₁ q
f e i = proj₁ (e i)
g : {p q} proj₁ p proj₁ q p q
g {p} {q} = lemSig pA p q
ve-re : (e : p q) (g f) e e
ve-re = pathJ (\ q (e : p q) (g f) e e)
(\ i j p .proj₁ , propSet (pA (p .proj₁)) (p .proj₂) (p .proj₂) (λ i (g {p} {p} f) (λ i₁ p) i .proj₂) (λ i p .proj₂) i j ) q
re-ve : (e : proj₁ p proj₁ q) (f {p} {q} g {p} {q}) e e
re-ve e = refl
inv : AreInverses (f {p} {q}) (g {p} {q})
inv = record
{ verso-recto = funExt ve-re
; recto-verso = funExt re-ve
}
iso : (p q) Eqv.≅ (proj₁ p proj₁ q)
iso = f , g , inv
lem3 : {c} {Q : A Set (c b)}
((a : A) P a Q a) Σ A P Σ A Q
lem3 {Q = Q} eA = res
where
f : Σ A P Σ A Q
f (a , pA) = a , _≃_.eqv (eA a) pA
g : Σ A Q Σ A P
g (a , qA) = a , g' qA
where
k : Eqv.Isomorphism _
k = Equiv≃.toIso _ _ (_≃_.isEqv (eA a))
open Σ k renaming (proj₁ to g')
ve-re : (x : Σ A P) (g f) x x
ve-re x i = proj₁ x , eq i
where
eq : proj₂ ((g f) x) proj₂ x
eq = begin
proj₂ ((g f) x) ≡⟨⟩
proj₂ (g (f (a , pA))) ≡⟨⟩
g' (_≃_.eqv (eA a) pA) ≡⟨ lem
pA
where
open Σ x renaming (proj₁ to a ; proj₂ to pA)
k : Eqv.Isomorphism _
k = Equiv≃.toIso _ _ (_≃_.isEqv (eA a))
open Σ k renaming (proj₁ to g' ; proj₂ to inv)
module A = AreInverses inv
-- anti-funExt
lem : (g' (_≃_.eqv (eA a))) pA pA
lem i = A.verso-recto i pA
re-ve : (x : Σ A Q) (f g) x x
re-ve x i = proj₁ x , eq i
where
open Σ x renaming (proj₁ to a ; proj₂ to qA)
eq = begin
proj₂ ((f g) x) ≡⟨⟩
_≃_.eqv (eA a) (g' qA) ≡⟨ (λ i A.recto-verso i qA)
qA
where
k : Eqv.Isomorphism _
k = Equiv≃.toIso _ _ (_≃_.isEqv (eA a))
open Σ k renaming (proj₁ to g' ; proj₂ to inv)
module A = AreInverses inv
inv : AreInverses f g
inv = record
{ verso-recto = funExt ve-re
; recto-verso = funExt re-ve
}
iso : Σ A P Eqv.≅ Σ A Q
iso = f , g , inv
res : Σ A P Σ A Q
res = fromIsomorphism iso
module _ {a b : Level} {A : Set a} {B : Set b} where
lem4 : isSet A isSet B (f : A B)
isEquiv A B f isIso f
lem4 sA sB f =
let
obv : isEquiv A B f isIso f
obv = Equiv≃.toIso A B
inv : isIso f isEquiv A B f
inv = Equiv≃.fromIso A B
re-ve : (x : isEquiv A B f) (inv obv) x x
re-ve = Equiv≃.inverse-from-to-iso A B
ve-re : (x : isIso f) (obv inv) x x
ve-re = Equiv≃.inverse-to-from-iso A B sA sB
iso : isEquiv A B f Eqv.≅ isIso f
iso = obv , inv ,
record
{ verso-recto = funExt re-ve
; recto-verso = funExt ve-re
}
in fromIsomorphism iso
isPreCat : IsPreCategory SetsRaw
IsPreCategory.isAssociative isPreCat = refl
IsPreCategory.isIdentity isPreCat {A} {B} = isIdentity {A} {B}
IsPreCategory.arrowsAreSets isPreCat {A} {B} = arrowsAreSets {A} {B}
open IsPreCategory isPreCat
module _ {hA hB : Object} where
open Σ hA renaming (proj₁ to A ; proj₂ to sA)
open Σ hB renaming (proj₁ to B ; proj₂ to sB)
open Σ hA renaming (fst to A ; snd to sA)
open Σ hB renaming (fst to B ; snd to sB)
-- lem3 and the equivalence from lem4
step0 : Σ (A B) isIso Σ (A B) (isEquiv A B)
step0 = lem3 {c = lzero} (λ f sym≃ (lem4 sA sB f))
-- univalence
step1 : Σ (A B) (isEquiv A B) (A B)
step1 = hh h
where
h : (A B) (A B)
h = sym≃ (univalence {A = A} {B})
obv : Σ (A B) (isEquiv A B) A B
obv = Eqv.deEta
inv : A B Σ (A B) (isEquiv A B)
inv = Eqv.doEta
re-ve : (x : _) (inv obv) x x
re-ve x = refl
-- Because _≃_ does not have eta equality!
ve-re : (x : _) (obv inv) x x
ve-re (con eqv isEqv) i = con eqv isEqv
areInv : AreInverses obv inv
areInv = record { verso-recto = funExt re-ve ; recto-verso = funExt ve-re }
eqv : Σ (A B) (isEquiv A B) Eqv.≅ (A B)
eqv = obv , inv , areInv
hh : Σ (A B) (isEquiv A B) (A B)
hh = fromIsomorphism eqv
-- lem2 with propIsSet
step2 : (A B) (hA hB)
step2 = sym≃ (lem2 (λ A isSetIsProp) hA hB)
-- Go from an isomorphism on sets to an isomorphism on homotopic sets
trivial? : (hA hB) (A Eqv.≅ B)
trivial? = sym≃ (fromIsomorphism res)
where
fwd : Σ (A B) isIso hA hB
fwd (f , g , inv) = f , g , inv.toPair
where
module inv = AreInverses inv
bwd : hA hB Σ (A B) isIso
bwd (f , g , x , y) = f , g , record { verso-recto = x ; recto-verso = y }
res : Σ (A B) isIso Eqv.≅ (hA hB)
res = fwd , bwd , record { verso-recto = refl ; recto-verso = refl }
conclusion : (hA hB) (hA hB)
conclusion = trivial? step0 step1 step2
univ≃ : (hA hB) (hA hB)
univ≃ = trivial? step0 step1 step2
module _ (hA : Object) where
open Σ hA renaming (proj₁ to A)
eq1 : (Σ[ hB Object ] hA hB) (Σ[ hB Object ] hA hB)
eq1 = ua (lem3 (\ hB univ≃))
univalent[Contr] : isContr (Σ[ hB Object ] hA hB)
univalent[Contr] = subst {P = isContr} (sym eq1) tres
where
module _ (y : Σ[ hB Object ] hA hB) where
open Σ y renaming (proj₁ to hB ; proj₂ to hA≡hB)
qres : (hA , refl) (hB , hA≡hB)
qres = contrSingl hA≡hB
tres : isContr (Σ[ hB Object ] hA hB)
tres = (hA , refl) , qres
univ≃ : (hA hB) (hA hB)
univ≃
= equivSigProp (λ A isSetIsProp)
univalence
equivSig {P = isEquiv A B} {Q = TypeIsomorphism} (equiv≃iso sA sB)
univalent : Univalent
univalent = from[Contr] univalent[Contr]
univalent = univalenceFrom≃ univ≃
SetsIsCategory : IsCategory SetsRaw
IsCategory.isAssociative SetsIsCategory = refl
IsCategory.isIdentity SetsIsCategory {A} {B} = isIdentity {A} {B}
IsCategory.arrowsAreSets SetsIsCategory {A} {B} = arrowsAreSets {A} {B}
IsCategory.isPreCategory SetsIsCategory = isPreCat
IsCategory.univalent SetsIsCategory = univalent
𝓢𝓮𝓽 Sets : Category (lsuc )
@ -300,11 +68,10 @@ module _ { : Level} where
private
𝓢 = 𝓢𝓮𝓽
open Category 𝓢
open import Cubical.Sigma
module _ (hA hB : Object) where
open Σ hA renaming (proj₁ to A ; proj₂ to sA)
open Σ hB renaming (proj₁ to B ; proj₂ to sB)
open Σ hA renaming (fst to A ; snd to sA)
open Σ hB renaming (fst to B ; snd to sB)
private
productObject : Object
@ -315,20 +82,32 @@ module _ { : Level} where
_&&&_ x = f x , g x
module _ (hX : Object) where
open Σ hX renaming (proj₁ to X)
open Σ hX renaming (fst to X)
module _ (f : X A ) (g : X B) where
ump : proj₁ Function.∘′ (f &&& g) f × proj₂ Function.∘′ (f &&& g) g
proj₁ ump = refl
proj₂ ump = refl
ump : fst ∘′ (f &&& g) f × snd ∘′ (f &&& g) g
fst ump = refl
snd ump = refl
rawProduct : RawProduct 𝓢 hA hB
RawProduct.object rawProduct = productObject
RawProduct.proj₁ rawProduct = Data.Product.proj₁
RawProduct.proj₂ rawProduct = Data.Product.proj₂
RawProduct.fst rawProduct = fst
RawProduct.snd rawProduct = snd
isProduct : IsProduct 𝓢 _ _ rawProduct
IsProduct.ump isProduct {X = hX} f g
= (f &&& g) , ump hX f g
= f &&& g , ump hX f g , λ eq funExt (umpUniq eq)
where
open Σ hX renaming (fst to X) using ()
module _ {y : X A × B} (eq : fst ∘′ y f × snd ∘′ y g) (x : X) where
p1 : fst ((f &&& g) x) fst (y x)
p1 = begin
fst ((f &&& g) x) ≡⟨⟩
f x ≡⟨ (λ i sym (fst eq) i x)
fst (y x)
p2 : snd ((f &&& g) x) snd (y x)
p2 = λ i sym (snd eq) i x
umpUniq : (f &&& g) x y x
umpUniq i = p1 i , p2 i
product : Product 𝓢 hA hB
Product.raw product = rawProduct

View file

@ -12,8 +12,8 @@
--
-- Data
-- ----
-- 𝟙; the identity arrow
-- __; function composition
-- identity; the identity arrow
-- _<<<_; function composition
--
-- Laws
-- ----
@ -24,17 +24,15 @@
-- ------
--
-- Propositionality for all laws about the category.
{-# OPTIONS --allow-unsolved-metas --cubical #-}
{-# OPTIONS --cubical #-}
module Cat.Category where
open import Cat.Prelude
renaming
( proj₁ to fst
; proj₂ to snd
)
import Function
import Cat.Equivalence
open Cat.Equivalence public using () renaming (Isomorphism to TypeIsomorphism)
open Cat.Equivalence
hiding (preorder≅ ; Isomorphism)
------------------
-- * Categories --
@ -50,21 +48,23 @@ record RawCategory (a b : Level) : Set (lsuc (a ⊔ b)) where
field
Object : Set a
Arrow : Object Object Set b
𝟙 : {A : Object} Arrow A A
__ : {A B C : Object} Arrow B C Arrow A B Arrow A C
identity : {A : Object} Arrow A A
_<<<_ : {A B C : Object} Arrow B C Arrow A B Arrow A C
infixl 10 _∘_ _>>>_
-- infixr 8 _<<<_
-- infixl 8 _>>>_
infixl 10 _<<<_ _>>>_
-- | Operations on data
domain : { a b : Object } Arrow a b Object
domain {a = a} _ = a
domain : {a b : Object} Arrow a b Object
domain {a} _ = a
codomain : { a b : Object } Arrow a b Object
codomain : {a b : Object} Arrow a b Object
codomain {b = b} _ = b
_>>>_ : {A B C : Object} (Arrow A B) (Arrow B C) Arrow A C
f >>> g = g f
f >>> g = g <<< f
-- | Laws about the data
@ -72,30 +72,30 @@ record RawCategory (a b : Level) : Set (lsuc (a ⊔ b)) where
-- right-hand-side.
IsAssociative : Set (a b)
IsAssociative = {A B C D} {f : Arrow A B} {g : Arrow B C} {h : Arrow C D}
h (g f) (h g) f
h <<< (g <<< f) (h <<< g) <<< f
IsIdentity : ({A : Object} Arrow A A) Set (a b)
IsIdentity id = {A B : Object} {f : Arrow A B}
id f f × f id f
id <<< f f × f <<< id f
ArrowsAreSets : Set (a b)
ArrowsAreSets = {A B : Object} isSet (Arrow A B)
IsInverseOf : {A B} (Arrow A B) (Arrow B A) Set b
IsInverseOf = λ f g g f 𝟙 × f g 𝟙
IsInverseOf = λ f g g <<< f identity × f <<< g identity
Isomorphism : {A B} (f : Arrow A B) Set b
Isomorphism {A} {B} f = Σ[ g Arrow B A ] IsInverseOf f g
__ : (A B : Object) Set b
__ A B = Σ[ f Arrow A B ] (Isomorphism f)
__ : (A B : Object) Set b
__ A B = Σ[ f Arrow A B ] (Isomorphism f)
module _ {A B : Object} where
Epimorphism : {X : Object } (f : Arrow A B) Set b
Epimorphism {X} f = ( g₀ g₁ : Arrow B X ) g₀ f g₁ f g₀ g₁
Epimorphism {X} f = (g₀ g₁ : Arrow B X) g₀ <<< f g₁ <<< f g₀ g₁
Monomorphism : {X : Object} (f : Arrow A B) Set b
Monomorphism {X} f = ( g₀ g₁ : Arrow X A ) f g₀ f g₁ g₀ g₁
Monomorphism {X} f = (g₀ g₁ : Arrow X A) f <<< g₀ f <<< g₁ g₀ g₁
IsInitial : Object Set (a b)
IsInitial I = {X : Object} isContr (Arrow I X)
@ -110,56 +110,70 @@ record RawCategory (a b : Level) : Set (lsuc (a ⊔ b)) where
Terminal = Σ Object IsTerminal
-- | Univalence is indexed by a raw category as well as an identity proof.
module Univalence (isIdentity : IsIdentity 𝟙) where
module Univalence (isIdentity : IsIdentity identity) where
-- | The identity isomorphism
idIso : (A : Object) A A
idIso A = 𝟙 , (𝟙 , isIdentity)
idIso : (A : Object) A A
idIso A = identity , identity , isIdentity
-- | Extract an isomorphism from an equality
--
-- [HoTT §9.1.4]
id-to-iso : (A B : Object) A B A B
id-to-iso A B eq = transp (\ i A eq i) (idIso A)
idToIso : (A B : Object) A B A B
idToIso A B eq = subst eq (idIso A)
Univalent : Set (a b)
Univalent = {A B : Object} isEquiv (A B) (A B) (id-to-iso A B)
Univalent = {A B : Object} isEquiv (A B) (A B) (idToIso A B)
univalenceFromIsomorphism : {A B : Object}
TypeIsomorphism (idToIso A B) isEquiv (A B) (A B) (idToIso A B)
univalenceFromIsomorphism = fromIso _ _
-- A perhaps more readable version of univalence:
Univalent≃ = {A B : Object} (A B) (A B)
Univalent≃ = {A B : Object} (A B) (A B)
Univalent≅ = {A B : Object} (A B) (A B)
private
-- | Equivalent formulation of univalence.
Univalent[Contr] : Set _
Univalent[Contr] = A isContr (Σ[ X Object ] A X)
Univalent[Contr] = A isContr (Σ[ X Object ] A X)
-- From: Thierry Coquand <Thierry.Coquand@cse.gu.se>
-- Date: Wed, Mar 21, 2018 at 3:12 PM
--
-- This is not so straight-forward so you can assume it
postulate from[Contr] : Univalent[Contr] Univalent
from[Contr] : Univalent[Contr] Univalent
from[Contr] = ContrToUniv.lemma _ _
where
open import Cubical.Fiberwise
-- | The mere proposition of being a category.
--
-- Also defines a few lemmas:
--
-- iso-is-epi : Isomorphism f → Epimorphism {X = X} f
-- iso-is-mono : Isomorphism f → Monomorphism {X = X} f
--
-- Sans `univalent` this would be what is referred to as a pre-category in
-- [HoTT].
record IsCategory {a b : Level} ( : RawCategory a b) : Set (lsuc (a b)) where
univalenceFrom≃ : Univalent≃ Univalent
univalenceFrom≃ = from[Contr] step
where
module _ (f : Univalent≃) (A : Object) where
lem : Σ Object (A ≡_) Σ Object (A ≊_)
lem = equivSig λ _ f
aux : isContr (Σ Object (A ≡_))
aux = (A , refl) , (λ y contrSingl (snd y))
step : isContr (Σ Object (A ≊_))
step = equivPreservesNType {n = ⟨-2⟩} lem aux
univalenceFrom≅ : Univalent≅ Univalent
univalenceFrom≅ x = univalenceFrom≃ $ fromIsomorphism _ _ x
propUnivalent : isProp Univalent
propUnivalent a b i = propPi (λ iso propIsContr) a b i
module _ {a b : Level} ( : RawCategory a b) where
record IsPreCategory : Set (lsuc (a b)) where
open RawCategory public
field
isAssociative : IsAssociative
isIdentity : IsIdentity 𝟙
isIdentity : IsIdentity identity
arrowsAreSets : ArrowsAreSets
open Univalence isIdentity public
field
univalent : Univalent
leftIdentity : {A B : Object} {f : Arrow A B} 𝟙 f f
leftIdentity : {A B : Object} {f : Arrow A B} identity <<< f f
leftIdentity {A} {B} {f} = fst (isIdentity {A = A} {B} {f})
rightIdentity : {A B : Object} {f : Arrow A B} f 𝟙 f
rightIdentity : {A B : Object} {f : Arrow A B} f <<< identity f
rightIdentity {A} {B} {f} = snd (isIdentity {A = A} {B} {f})
------------
@ -171,78 +185,380 @@ record IsCategory {a b : Level} ( : RawCategory a b) : Set (lsuc
iso→epi : Isomorphism f Epimorphism {X = X} f
iso→epi (f- , left-inv , right-inv) g₀ g₁ eq = begin
g₀ ≡⟨ sym rightIdentity
g₀ 𝟙 ≡⟨ cong (_∘_ g₀) (sym right-inv)
g₀ (f f-) ≡⟨ isAssociative
(g₀ f) f- ≡⟨ cong (λ φ φ f-) eq
(g₁ f) f- ≡⟨ sym isAssociative
g₁ (f f-) ≡⟨ cong (_∘_ g₁) right-inv
g₁ 𝟙 ≡⟨ rightIdentity
g₀ <<< identity ≡⟨ cong (_<<<_ g₀) (sym right-inv)
g₀ <<< (f <<< f-) ≡⟨ isAssociative
(g₀ <<< f) <<< f- ≡⟨ cong (λ φ φ <<< f-) eq
(g₁ <<< f) <<< f- ≡⟨ sym isAssociative
g₁ <<< (f <<< f-) ≡⟨ cong (_<<<_ g₁) right-inv
g₁ <<< identity ≡⟨ rightIdentity
g₁
iso→mono : Isomorphism f Monomorphism {X = X} f
iso→mono (f- , left-inv , right-inv) g₀ g₁ eq =
begin
g₀ ≡⟨ sym leftIdentity
𝟙 g₀ ≡⟨ cong (λ φ φ g₀) (sym left-inv)
(f- f) g₀ ≡⟨ sym isAssociative
f- (f g₀) ≡⟨ cong (_∘_ f-) eq
f- (f g₁) ≡⟨ isAssociative
(f- f) g₁ ≡⟨ cong (λ φ φ g₁) left-inv
𝟙 g₁ ≡⟨ leftIdentity
identity <<< g₀ ≡⟨ cong (λ φ φ <<< g₀) (sym left-inv)
(f- <<< f) <<< g₀ ≡⟨ sym isAssociative
f- <<< (f <<< g₀) ≡⟨ cong (_<<<_ f-) eq
f- <<< (f <<< g₁) ≡⟨ isAssociative
(f- <<< f) <<< g₁ ≡⟨ cong (λ φ φ <<< g₁) left-inv
identity <<< g₁ ≡⟨ leftIdentity
g₁
iso→epi×mono : Isomorphism f Epimorphism {X = X} f × Monomorphism {X = X} f
iso→epi×mono iso = iso→epi iso , iso→mono iso
propIsAssociative : isProp IsAssociative
propIsAssociative = propPiImpl (λ _ propPiImpl (λ _ propPiImpl (λ _ propPiImpl (λ _ propPiImpl (λ _ propPiImpl (λ _ propPiImpl λ _ arrowsAreSets _ _))))))
propIsIdentity : {f : {A} Arrow A A} isProp (IsIdentity f)
propIsIdentity {id} = propPiImpl (λ _ propPiImpl λ _ propPiImpl (λ f
propSig (arrowsAreSets (id <<< f) f) λ _ arrowsAreSets (f <<< id) f))
propArrowIsSet : isProp ( {A B} isSet (Arrow A B))
propArrowIsSet = propPiImpl λ _ propPiImpl (λ _ isSetIsProp)
propIsInverseOf : {A B f g} isProp (IsInverseOf {A} {B} f g)
propIsInverseOf = propSig (arrowsAreSets _ _) (λ _ arrowsAreSets _ _)
module _ {A B : Object} where
propIsomorphism : (f : Arrow A B) isProp (Isomorphism f)
propIsomorphism f a@(g , η , ε) a'@(g' , η' , ε') =
lemSig (λ g propIsInverseOf) a a' geq
where
geq : g g'
geq = begin
g ≡⟨ sym rightIdentity
g <<< identity ≡⟨ cong (λ φ g <<< φ) (sym ε')
g <<< (f <<< g') ≡⟨ isAssociative
(g <<< f) <<< g' ≡⟨ cong (λ φ φ <<< g') η
identity <<< g' ≡⟨ leftIdentity
g'
isoEq : {a b : A B} fst a fst b a b
isoEq = lemSig propIsomorphism _ _
propIsInitial : I isProp (IsInitial I)
propIsInitial I x y i {X} = res X i
where
module _ (X : Object) where
open Σ (x {X}) renaming (fst to fx ; snd to cx)
open Σ (y {X}) renaming (fst to fy ; snd to cy)
fp : fx fy
fp = cx fy
prop : (x : Arrow I X) isProp ( f x f)
prop x = propPi (λ y arrowsAreSets x y)
cp : (λ i f fp i f) [ cx cy ]
cp = lemPropF prop fp
res : (fx , cx) (fy , cy)
res i = fp i , cp i
propIsTerminal : T isProp (IsTerminal T)
propIsTerminal T x y i {X} = res X i
where
module _ (X : Object) where
open Σ (x {X}) renaming (fst to fx ; snd to cx)
open Σ (y {X}) renaming (fst to fy ; snd to cy)
fp : fx fy
fp = cx fy
prop : (x : Arrow X T) isProp ( f x f)
prop x = propPi (λ y arrowsAreSets x y)
cp : (λ i f fp i f) [ cx cy ]
cp = lemPropF prop fp
res : (fx , cx) (fy , cy)
res i = fp i , cp i
module _ where
private
trans≊ : Transitive _≊_
trans≊ (f , f~ , f-inv) (g , g~ , g-inv)
= g <<< f
, f~ <<< g~
, ( begin
(f~ <<< g~) <<< (g <<< f) ≡⟨ isAssociative
(f~ <<< g~) <<< g <<< f ≡⟨ cong (λ φ φ <<< f) (sym isAssociative)
f~ <<< (g~ <<< g) <<< f ≡⟨ cong (λ φ f~ <<< φ <<< f) (fst g-inv)
f~ <<< identity <<< f ≡⟨ cong (λ φ φ <<< f) rightIdentity
f~ <<< f ≡⟨ fst f-inv
identity
)
, ( begin
g <<< f <<< (f~ <<< g~) ≡⟨ isAssociative
g <<< f <<< f~ <<< g~ ≡⟨ cong (λ φ φ <<< g~) (sym isAssociative)
g <<< (f <<< f~) <<< g~ ≡⟨ cong (λ φ g <<< φ <<< g~) (snd f-inv)
g <<< identity <<< g~ ≡⟨ cong (λ φ φ <<< g~) rightIdentity
g <<< g~ ≡⟨ snd g-inv
identity
)
isPreorder : IsPreorder _≊_
isPreorder = record { isEquivalence = equalityIsEquivalence ; reflexive = idToIso _ _ ; trans = trans≊ }
preorder≊ : Preorder _ _ _
preorder≊ = record { Carrier = Object ; _≈_ = _≡_ ; __ = _≊_ ; isPreorder = isPreorder }
record PreCategory : Set (lsuc (a b)) where
field
isPreCategory : IsPreCategory
open IsPreCategory isPreCategory public
-- Definition 9.6.1 in [HoTT]
record StrictCategory : Set (lsuc (a b)) where
field
preCategory : PreCategory
open PreCategory preCategory
field
objectsAreSets : isSet Object
record IsCategory : Set (lsuc (a b)) where
field
isPreCategory : IsPreCategory
open IsPreCategory isPreCategory public
field
univalent : Univalent
-- | The formulation of univalence expressed with _≃_ is trivially admissable -
-- just "forget" the equivalence.
univalent≃ : Univalent≃
univalent≃ = _ , univalent
module _ {A B : Object} where
private
iso : TypeIsomorphism (idToIso A B)
iso = toIso _ _ univalent
isoToId : (A B) (A B)
isoToId = fst iso
asTypeIso : TypeIsomorphism (idToIso A B)
asTypeIso = toIso _ _ univalent
-- FIXME Rename
inverse-from-to-iso' : AreInverses (idToIso A B) isoToId
inverse-from-to-iso' = snd iso
module _ {a b : Object} (f : Arrow a b) where
module _ {a' : Object} (p : a a') where
private
p~ : Arrow a' a
p~ = fst (snd (idToIso _ _ p))
D : a'' a a'' Set _
D a'' p' = coe (cong (λ x Arrow x b) p') f f <<< (fst (snd (idToIso _ _ p')))
9-1-9-left : coe (cong (λ x Arrow x b) p) f f <<< p~
9-1-9-left = pathJ D (begin
coe refl f ≡⟨ id-coe
f ≡⟨ sym rightIdentity
f <<< identity ≡⟨ cong (f <<<_) (sym subst-neutral)
f <<< _ ≡⟨⟩ _ ) a' p
module _ {b' : Object} (p : b b') where
private
p* : Arrow b b'
p* = fst (idToIso _ _ p)
D : b'' b b'' Set _
D b'' p' = coe (cong (λ x Arrow a x) p') f fst (idToIso _ _ p') <<< f
9-1-9-right : coe (cong (λ x Arrow a x) p) f p* <<< f
9-1-9-right = pathJ D (begin
coe refl f ≡⟨ id-coe
f ≡⟨ sym leftIdentity
identity <<< f ≡⟨ cong (_<<< f) (sym subst-neutral)
_ <<< f ) b' p
-- lemma 9.1.9 in hott
module _ {a a' b b' : Object}
(p : a a') (q : b b') (f : Arrow a b)
where
private
q* : Arrow b b'
q* = fst (idToIso _ _ q)
q~ : Arrow b' b
q~ = fst (snd (idToIso _ _ q))
p* : Arrow a a'
p* = fst (idToIso _ _ p)
p~ : Arrow a' a
p~ = fst (snd (idToIso _ _ p))
pq : Arrow a b Arrow a' b'
pq i = Arrow (p i) (q i)
U : b'' b b'' Set _
U b'' q' = coe (λ i Arrow a (q' i)) f fst (idToIso _ _ q') <<< f <<< (fst (snd (idToIso _ _ refl)))
u : coe (λ i Arrow a b) f fst (idToIso _ _ refl) <<< f <<< (fst (snd (idToIso _ _ refl)))
u = begin
coe refl f ≡⟨ id-coe
f ≡⟨ sym leftIdentity
identity <<< f ≡⟨ sym rightIdentity
identity <<< f <<< identity ≡⟨ cong (λ φ identity <<< f <<< φ) lem
identity <<< f <<< (fst (snd (idToIso _ _ refl))) ≡⟨ cong (λ φ φ <<< f <<< (fst (snd (idToIso _ _ refl)))) lem
fst (idToIso _ _ refl) <<< f <<< (fst (snd (idToIso _ _ refl)))
where
lem : {x} PathP (λ _ Arrow x x) identity (fst (idToIso x x refl))
lem = sym subst-neutral
D : a'' a a'' Set _
D a'' p' = coe (λ i Arrow (p' i) (q i)) f fst (idToIso b b' q) <<< f <<< (fst (snd (idToIso _ _ p')))
d : coe (λ i Arrow a (q i)) f fst (idToIso b b' q) <<< f <<< (fst (snd (idToIso _ _ refl)))
d = pathJ U u b' q
9-1-9 : coe pq f q* <<< f <<< p~
9-1-9 = pathJ D d a' p
9-1-9' : coe pq f <<< p* q* <<< f
9-1-9' = begin
coe pq f <<< p* ≡⟨ cong (_<<< p*) 9-1-9
q* <<< f <<< p~ <<< p* ≡⟨ sym isAssociative
q* <<< f <<< (p~ <<< p*) ≡⟨ cong (λ φ q* <<< f <<< φ) lem
q* <<< f <<< identity ≡⟨ rightIdentity
q* <<< f
where
lem : p~ <<< p* identity
lem = fst (snd (snd (idToIso _ _ p)))
module _ {A B X : Object} (iso : A B) where
private
p : A B
p = isoToId iso
p-dom : Arrow A X Arrow B X
p-dom = cong (λ x Arrow x X) p
p-cod : Arrow X A Arrow X B
p-cod = cong (λ x Arrow X x) p
lem : {A B} {x : A B} idToIso A B (isoToId x) x
lem {x = x} i = snd inverse-from-to-iso' i x
open Σ iso renaming (fst to ι) using ()
open Σ (snd iso) renaming (fst to ι~ ; snd to inv)
coe-dom : {f : Arrow A X} coe p-dom f f <<< ι~
coe-dom {f} = begin
coe p-dom f ≡⟨ 9-1-9-left f p
f <<< fst (snd (idToIso _ _ (isoToId iso))) ≡⟨⟩
f <<< fst (snd (idToIso _ _ p)) ≡⟨ cong (f <<<_) (cong (fst snd) lem)
f <<< ι~
coe-cod : {f : Arrow X A} coe p-cod f ι <<< f
coe-cod {f} = begin
coe p-cod f
≡⟨ 9-1-9-right f p
fst (idToIso _ _ p) <<< f
≡⟨ cong (λ φ φ <<< f) (cong fst lem)
ι <<< f
module _ {f : Arrow A X} {g : Arrow B X} (q : PathP (λ i p-dom i) f g) where
domain-twist : g f <<< ι~
domain-twist = begin
g ≡⟨ sym (coe-lem q)
coe p-dom f ≡⟨ coe-dom
f <<< ι~
-- This can probably also just be obtained from the above my taking the
-- symmetric isomorphism.
domain-twist-sym : f g <<< ι
domain-twist-sym = begin
f ≡⟨ sym rightIdentity
f <<< identity ≡⟨ cong (f <<<_) (sym (fst inv))
f <<< (ι~ <<< ι) ≡⟨ isAssociative
f <<< ι~ <<< ι ≡⟨ cong (_<<< ι) (sym domain-twist)
g <<< ι
-- | All projections are propositions.
module Propositionality where
propIsAssociative : isProp IsAssociative
propIsAssociative x y i = arrowsAreSets _ _ x y i
propIsIdentity : {f : {A} Arrow A A} isProp (IsIdentity f)
propIsIdentity a b i
= arrowsAreSets _ _ (fst a) (fst b) i
, arrowsAreSets _ _ (snd a) (snd b) i
propArrowIsSet : isProp ( {A B} isSet (Arrow A B))
propArrowIsSet a b i = isSetIsProp a b i
propIsInverseOf : {A B f g} isProp (IsInverseOf {A} {B} f g)
propIsInverseOf x y = λ i
let
h : fst x fst y
h = arrowsAreSets _ _ (fst x) (fst y)
hh : snd x snd y
hh = arrowsAreSets _ _ (snd x) (snd y)
in h i , hh i
module _ {A B : Object} {f : Arrow A B} where
isoIsProp : isProp (Isomorphism f)
isoIsProp a@(g , η , ε) a'@(g' , η' , ε') =
lemSig (λ g propIsInverseOf) a a' geq
-- | Terminal objects are propositional - a.k.a uniqueness of terminal
-- | objects.
--
-- Having two terminal objects induces an isomorphism between them - and
-- because of univalence this is equivalent to equality.
propTerminal : isProp Terminal
propTerminal Xt Yt = res
where
geq : g g'
geq = begin
g ≡⟨ sym rightIdentity
g 𝟙 ≡⟨ cong (λ φ g φ) (sym ε')
g (f g') ≡⟨ isAssociative
(g f) g' ≡⟨ cong (λ φ φ g') η
𝟙 g' ≡⟨ leftIdentity
g'
open Σ Xt renaming (fst to X ; snd to Xit)
open Σ Yt renaming (fst to Y ; snd to Yit)
open Σ (Xit {Y}) renaming (fst to Y→X) using ()
open Σ (Yit {X}) renaming (fst to X→Y) using ()
-- Need to show `left` and `right`, what we know is that the arrows are
-- unique. Well, I know that if I compose these two arrows they must give
-- the identity, since also the identity is the unique such arrow (by X
-- and Y both being terminal objects.)
Xprop : isProp (Arrow X X)
Xprop f g = trans (sym (snd Xit f)) (snd Xit g)
Yprop : isProp (Arrow Y Y)
Yprop f g = trans (sym (snd Yit f)) (snd Yit g)
left : Y→X <<< X→Y identity
left = Xprop _ _
right : X→Y <<< Y→X identity
right = Yprop _ _
iso : X Y
iso = X→Y , Y→X , left , right
p0 : X Y
p0 = isoToId iso
p1 : (λ i IsTerminal (p0 i)) [ Xit Yit ]
p1 = lemPropF propIsTerminal p0
res : Xt Yt
res i = p0 i , p1 i
propUnivalent : isProp Univalent
propUnivalent a b i = propPi (λ iso propIsContr) a b i
-- Merely the dual of the above statement.
propInitial : isProp Initial
propInitial Xi Yi = res
where
open Σ Xi renaming (fst to X ; snd to Xii)
open Σ Yi renaming (fst to Y ; snd to Yii)
open Σ (Xii {Y}) renaming (fst to Y→X) using ()
open Σ (Yii {X}) renaming (fst to X→Y) using ()
-- Need to show `left` and `right`, what we know is that the arrows are
-- unique. Well, I know that if I compose these two arrows they must give
-- the identity, since also the identity is the unique such arrow (by X
-- and Y both being terminal objects.)
Xprop : isProp (Arrow X X)
Xprop f g = trans (sym (snd Xii f)) (snd Xii g)
Yprop : isProp (Arrow Y Y)
Yprop f g = trans (sym (snd Yii f)) (snd Yii g)
left : Y→X <<< X→Y identity
left = Yprop _ _
right : X→Y <<< Y→X identity
right = Xprop _ _
iso : X Y
iso = Y→X , X→Y , right , left
res : Xi Yi
res = lemSig propIsInitial _ _ (isoToId iso)
groupoidObject : isGrpd Object
groupoidObject A B = res
where
open import Data.Nat using (_≤_ ; ≤′-refl ; ≤′-step)
setIso : x isSet (Isomorphism x)
setIso x = ntypeCumulative {n = 1} (≤′-step ≤′-refl) (propIsomorphism x)
step : isSet (A B)
step = setSig {sA = arrowsAreSets} {sB = setIso}
res : isSet (A B)
res = equivPreservesNType
{A = A B} {B = A B} {n = ⟨0⟩}
(Equivalence.symmetry (univalent≃ {A = A} {B}))
step
-- | Propositionality of being a category
module _ {a b : Level} ( : RawCategory a b) where
open RawCategory
open Univalence
private
module _ (x y : IsPreCategory ) where
module x = IsPreCategory x
module y = IsPreCategory y
-- In a few places I use the result of propositionality of the various
-- projections of `IsCategory` - Here I arbitrarily chose to use this
-- result from `x : IsCategory C`. I don't know which (if any) possibly
-- adverse effects this may have.
-- module Prop = X.Propositionality
propIsPreCategory : x y
IsPreCategory.isAssociative (propIsPreCategory i)
= x.propIsAssociative x.isAssociative y.isAssociative i
IsPreCategory.isIdentity (propIsPreCategory i)
= x.propIsIdentity x.isIdentity y.isIdentity i
IsPreCategory.arrowsAreSets (propIsPreCategory i)
= x.propArrowIsSet x.arrowsAreSets y.arrowsAreSets i
module _ (x y : IsCategory ) where
module X = IsCategory x
module Y = IsCategory y
@ -252,37 +568,38 @@ module _ {a b : Level} ( : RawCategory a b) where
-- adverse effects this may have.
module Prop = X.Propositionality
isIdentity : (λ _ IsIdentity 𝟙) [ X.isIdentity Y.isIdentity ]
isIdentity = Prop.propIsIdentity X.isIdentity Y.isIdentity
U : {a : IsIdentity 𝟙}
(λ _ IsIdentity 𝟙) [ X.isIdentity a ]
(b : Univalent a)
Set _
U eqwal univ =
(λ i Univalent (eqwal i))
[ X.univalent univ ]
P : (y : IsIdentity 𝟙)
(λ _ IsIdentity 𝟙) [ X.isIdentity y ] Set _
P y eq = (univ : Univalent y) U eq univ
p : (b' : Univalent X.isIdentity)
(λ _ Univalent X.isIdentity) [ X.univalent b' ]
p univ = Prop.propUnivalent X.univalent univ
helper : P Y.isIdentity isIdentity
helper = pathJ P p Y.isIdentity isIdentity
eqUni : U isIdentity Y.univalent
eqUni = helper Y.univalent
isIdentity= : (λ _ IsIdentity identity) [ X.isIdentity Y.isIdentity ]
isIdentity= = X.propIsIdentity X.isIdentity Y.isIdentity
isPreCategory= : X.isPreCategory Y.isPreCategory
isPreCategory= = propIsPreCategory X.isPreCategory Y.isPreCategory
private
p = cong IsPreCategory.isIdentity isPreCategory=
univalent= : (λ i Univalent (p i))
[ X.univalent Y.univalent ]
univalent= = lemPropF
{A = IsIdentity identity}
{B = Univalent}
propUnivalent
{a0 = X.isIdentity}
{a1 = Y.isIdentity}
p
done : x y
IsCategory.isAssociative (done i) = Prop.propIsAssociative X.isAssociative Y.isAssociative i
IsCategory.isIdentity (done i) = isIdentity i
IsCategory.arrowsAreSets (done i) = Prop.propArrowIsSet X.arrowsAreSets Y.arrowsAreSets i
IsCategory.univalent (done i) = eqUni i
IsCategory.isPreCategory (done i) = isPreCategory= i
IsCategory.univalent (done i) = univalent= i
propIsCategory : isProp (IsCategory )
propIsCategory = done
-- | Univalent categories
--
-- Just bundles up the data with witnesses inhabiting the propositions.
-- Question: Should I remove the type `Category`?
record Category (a b : Level) : Set (lsuc (a b)) where
field
raw : RawCategory a b
@ -300,13 +617,11 @@ module _ {a b : Level} { 𝔻 : Category a b} where
module _ (rawEq : .raw 𝔻.raw) where
private
isCategoryEq : (λ i IsCategory (rawEq i)) [ .isCategory 𝔻.isCategory ]
isCategoryEq = lemPropF propIsCategory rawEq
isCategoryEq = lemPropF {A = RawCategory _ _} {B = IsCategory} propIsCategory rawEq
Category≡ : 𝔻
Category≡ i = record
{ raw = rawEq i
; isCategory = isCategoryEq i
}
Category.raw (Category≡ i) = rawEq i
Category.isCategory (Category≡ i) = isCategoryEq i
-- | Syntax for arrows- and composition in a given category.
module _ {a b : Level} ( : Category a b) where
@ -315,7 +630,7 @@ module _ {a b : Level} ( : Category a b) where
_[_,_] = Arrow
_[_∘_] : {A B C : Object} (g : Arrow B C) (f : Arrow A B) Arrow A C
_[_∘_] = __
_[_∘_] = _<<<_
-- | The opposite category
--
@ -324,38 +639,66 @@ module _ {a b : Level} ( : Category a b) where
module Opposite {a b : Level} where
module _ ( : Category a b) where
private
module _ where
module = Category
opRaw : RawCategory a b
RawCategory.Object opRaw = .Object
RawCategory.Arrow opRaw = Function.flip .Arrow
RawCategory.𝟙 opRaw = .𝟙
RawCategory._∘_ opRaw = Function.flip ._∘_
RawCategory.Arrow opRaw = flip .Arrow
RawCategory.identity opRaw = .identity
RawCategory._<<<_ opRaw = ._>>>_
open RawCategory opRaw
isIdentity : IsIdentity 𝟙
isIdentity = swap .isIdentity
isPreCategory : IsPreCategory opRaw
IsPreCategory.isAssociative isPreCategory = sym .isAssociative
IsPreCategory.isIdentity isPreCategory = swap .isIdentity
IsPreCategory.arrowsAreSets isPreCategory = .arrowsAreSets
open Univalence isIdentity
open IsPreCategory isPreCategory
module _ {A B : .Object} where
univalent : isEquiv (A B) (A B)
(Univalence.id-to-iso (swap .isIdentity) A B)
fst (univalent iso) = flipFiber (fst (.univalent (flipIso iso)))
where
flipIso : A B B .≅ A
flipIso (f , f~ , iso) = f , f~ , swap iso
flipFiber
: fiber (.id-to-iso B A) (flipIso iso)
fiber ( id-to-iso A B) iso
flipFiber (eq , eqIso) = sym eq , {!!}
snd (univalent iso) = {!!}
open Σ (toIso _ _ (.univalent {A} {B}))
renaming (fst to idToIso* ; snd to inv*)
open AreInverses {f = .idToIso A B} {idToIso*} inv*
shuffle : A B A .≊ B
shuffle (f , g , inv) = g , f , inv
shuffle~ : A .≊ B A B
shuffle~ (f , g , inv) = g , f , inv
lem : (p : A B) idToIso A B p shuffle~ (.idToIso A B p)
lem p = isoEq refl
isoToId* : A B A B
isoToId* = idToIso* shuffle
inv : AreInverses (idToIso A B) isoToId*
inv =
( funExt (λ x begin
(isoToId* idToIso A B) x
≡⟨⟩
(idToIso* shuffle idToIso A B) x
≡⟨ cong (λ φ φ x) (cong (λ φ idToIso* shuffle φ) (funExt lem))
(idToIso* shuffle shuffle~ .idToIso A B) x
≡⟨⟩
(idToIso* .idToIso A B) x
≡⟨ (λ i verso-recto i x)
x )
, funExt (λ x begin
(idToIso A B idToIso* shuffle) x
≡⟨ cong (λ φ φ x) (cong (λ φ φ idToIso* shuffle) (funExt lem))
(shuffle~ .idToIso A B idToIso* shuffle) x
≡⟨ cong (λ φ φ x) (cong (λ φ shuffle~ φ shuffle) recto-verso)
(shuffle~ shuffle) x
≡⟨⟩
x )
)
isCategory : IsCategory opRaw
IsCategory.isAssociative isCategory = sym .isAssociative
IsCategory.isIdentity isCategory = isIdentity
IsCategory.arrowsAreSets isCategory = .arrowsAreSets
IsCategory.univalent isCategory = univalent
IsCategory.isPreCategory isCategory = isPreCategory
IsCategory.univalent isCategory
= univalenceFromIsomorphism (isoToId* , inv)
opposite : Category a b
Category.raw opposite = opRaw
@ -373,8 +716,8 @@ module Opposite {a b : Level} where
rawInv : Category.raw (opposite (opposite )) raw
RawCategory.Object (rawInv _) = Object
RawCategory.Arrow (rawInv _) = Arrow
RawCategory.𝟙 (rawInv _) = 𝟙
RawCategory._∘_ (rawInv _) = _∘_
RawCategory.identity (rawInv _) = identity
RawCategory._<<<_ (rawInv _) = _<<<_
oppositeIsInvolution : opposite (opposite )
oppositeIsInvolution = Category≡ rawInv

View file

@ -16,11 +16,11 @@ module _ { '} ( : Category ') {{hasProducts : HasProducts }}
field
uniq
: (A : Object) (f : [ A × B , C ])
∃![ f~ ] ( [ eval f~ |×| Category.𝟙 ] f)
∃![ f~ ] ( [ eval f~ |×| Category.identity ] f)
IsExponential : (Cᴮ : Object) [ Cᴮ × B , C ] Set ( ')
IsExponential Cᴮ eval = (A : Object) (f : [ A × B , C ])
∃![ f~ ] ( [ eval f~ |×| Category.𝟙 ] f)
∃![ f~ ] ( [ eval f~ |×| Category.identity ] f)
record Exponential : Set ( ') where
field
@ -30,7 +30,7 @@ module _ { '} ( : Category ') {{hasProducts : HasProducts }}
{{isExponential}} : IsExponential obj eval
transpose : (A : Object) [ A × B , C ] [ A , obj ]
transpose A f = proj₁ (isExponential A f)
transpose A f = fst (isExponential A f)
record HasExponentials { ' : Level} ( : Category ') {{_ : HasProducts }} : Set ( ') where
open Category

View file

@ -1,39 +1,37 @@
{-# OPTIONS --cubical #-}
module Cat.Category.Functor where
open import Agda.Primitive
open import Function
open import Cat.Prelude
open import Cubical
open import Cubical.NType.Properties using (lemPropF)
open import Cat.Category
open Category hiding (_∘_ ; raw ; IsIdentity)
module _ {c c' d d'}
( : Category c c')
(𝔻 : Category d d')
where
private
module = Category
module 𝔻 = Category 𝔻
= c c' d d'
𝓤 = Set
Omap = Object Object 𝔻
Omap = .Object 𝔻.Object
Fmap : Omap Set _
Fmap omap = {A B}
[ A , B ] 𝔻 [ omap A , omap B ]
record RawFunctor : 𝓤 where
field
omap : Object Object 𝔻
omap : .Object 𝔻.Object
fmap : {A B} [ A , B ] 𝔻 [ omap A , omap B ]
IsIdentity : Set _
IsIdentity = {A : Object } fmap (𝟙 {A}) 𝟙 𝔻 {omap A}
IsIdentity = {A : .Object} fmap (.identity {A}) 𝔻.identity {omap A}
IsDistributive : Set _
IsDistributive = {A B C : Object } {f : [ A , B ]} {g : [ B , C ]}
IsDistributive = {A B C : .Object} {f : [ A , B ]} {g : [ B , C ]}
fmap ( [ g f ]) 𝔻 [ fmap g fmap f ]
-- | Equality principle for raw functors
@ -120,11 +118,18 @@ module _ {c c' d d' : Level} { : Category c c'} {𝔻 : Cat
res : (λ i IsFunctor 𝔻 (eq i)) [ isFunctor F isFunctor G ]
res = IsFunctorIsProp' (isFunctor F) (isFunctor G)
module _ { ' : Level} {A B C : Category '} (F : Functor B C) (G : Functor A B) where
module _ {0 1 2 3 4 5 : Level}
{A : Category 0 1}
{B : Category 2 3}
{C : Category 4 5}
(F : Functor B C) (G : Functor A B) where
private
module A = Category A
module B = Category B
module C = Category C
module F = Functor F
module G = Functor G
module _ {a0 a1 a2 : Object A} {α0 : A [ a0 , a1 ]} {α1 : A [ a1 , a2 ]} where
module _ {a0 a1 a2 : A.Object} {α0 : A [ a0 , a1 ]} {α1 : A [ a1 , a2 ]} where
dist : (F.fmap G.fmap) (A [ α1 α0 ]) C [ (F.fmap G.fmap) α1 (F.fmap G.fmap) α0 ]
dist = begin
(F.fmap G.fmap) (A [ α1 α0 ])
@ -143,10 +148,10 @@ module _ { ' : Level} {A B C : Category '} (F : Functor B C) (G : F
isFunctor : IsFunctor A C raw
isFunctor = record
{ isIdentity = begin
(F.fmap G.fmap) (𝟙 A) ≡⟨ refl
F.fmap (G.fmap (𝟙 A)) ≡⟨ cong F.fmap (G.isIdentity)
F.fmap (𝟙 B) ≡⟨ F.isIdentity
𝟙 C
(F.fmap G.fmap) A.identity ≡⟨ refl
F.fmap (G.fmap A.identity) ≡⟨ cong F.fmap (G.isIdentity)
F.fmap B.identity ≡⟨ F.isIdentity
C.identity
; isDistributive = dist
}
@ -154,15 +159,42 @@ module _ { ' : Level} {A B C : Category '} (F : Functor B C) (G : F
Functor.raw F[_∘_] = raw
Functor.isFunctor F[_∘_] = isFunctor
-- The identity functor
identity : { '} {C : Category '} Functor C C
identity = record
{ raw = record
{ omap = λ x x
; fmap = λ x x
}
; isFunctor = record
{ isIdentity = refl
; isDistributive = refl
}
}
-- | The identity functor
module Functors where
module _ {c cc : Level} { : Category c cc} where
private
raw : RawFunctor
RawFunctor.omap raw = idFun _
RawFunctor.fmap raw = idFun _
isFunctor : IsFunctor raw
IsFunctor.isIdentity isFunctor = refl
IsFunctor.isDistributive isFunctor = refl
identity : Functor
Functor.raw identity = raw
Functor.isFunctor identity = isFunctor
module _
{a aa b bb c cc d dd : Level}
{𝔸 : Category a aa}
{𝔹 : Category b bb}
{ : Category c cc}
{𝔻 : Category d dd}
{F : Functor 𝔸 𝔹} {G : Functor 𝔹 } {H : Functor 𝔻} where
isAssociative : F[ H F[ G F ] ] F[ F[ H G ] F ]
isAssociative = Functor≡ refl
module _
{c cc d dd : Level}
{ : Category c cc}
{𝔻 : Category d dd}
{F : Functor 𝔻} where
leftIdentity : F[ identity F ] F
leftIdentity = Functor≡ refl
rightIdentity : F[ F identity ] F
rightIdentity = Functor≡ refl
isIdentity : F[ identity F ] F × F[ F identity ] F
isIdentity = leftIdentity , rightIdentity

View file

@ -17,13 +17,13 @@ These two formulations are proven to be equivalent:
The monoidal representation is exposed by default from this module.
---}
{-# OPTIONS --cubical --allow-unsolved-metas #-}
{-# OPTIONS --cubical #-}
module Cat.Category.Monad where
open import Cat.Prelude
open import Cat.Category
open import Cat.Category.Functor as F
open import Cat.Category.NaturalTransformation
import Cat.Category.NaturalTransformation
import Cat.Category.Monad.Monoidal
import Cat.Category.Monad.Kleisli
open import Cat.Categories.Fun
@ -33,9 +33,10 @@ module Kleisli = Cat.Category.Monad.Kleisli
-- | The monoidal- and kleisli presentation of monads are equivalent.
module _ {a b : Level} ( : Category a b) where
open Cat.Category.NaturalTransformation using (NaturalTransformation ; propIsNatural)
private
module = Category
open using (Object ; Arrow ; 𝟙 ; _∘_ ; _>>>_)
open using (Object ; Arrow ; identity ; _<<<_ ; _>>>_)
module M = Monoidal
module K = Kleisli
@ -51,7 +52,7 @@ module _ {a b : Level} ( : Category a b) where
private
module MI = M.IsMonad m
forthIsMonad : K.IsMonad (forthRaw raw)
K.IsMonad.isIdentity forthIsMonad = proj₂ MI.isInverse
K.IsMonad.isIdentity forthIsMonad = snd MI.isInverse
K.IsMonad.isNatural forthIsMonad = MI.isNatural
K.IsMonad.isDistributive forthIsMonad = MI.isDistributive
@ -68,26 +69,28 @@ module _ {a b : Level} ( : Category a b) where
M.RawMonad.joinNT backRaw = joinNT
private
open M.RawMonad backRaw
open M.RawMonad backRaw renaming
( join to join*
; pure to pure*
; bind to bind*
; fmap to fmap*
)
module R = Functor (M.RawMonad.R backRaw)
backIsMonad : M.IsMonad backRaw
M.IsMonad.isAssociative backIsMonad {X} = begin
joinT X R.fmap (joinT X) ≡⟨⟩
join fmap (joinT X) ≡⟨⟩
join fmap join ≡⟨ isNaturalForeign
join join ≡⟨⟩
joinT X joinT (R.omap X)
M.IsMonad.isAssociative backIsMonad = begin
join* <<< R.fmap join* ≡⟨⟩
join <<< fmap join ≡⟨ isNaturalForeign
join <<< join
M.IsMonad.isInverse backIsMonad {X} = inv-l , inv-r
where
inv-l = begin
joinT X pureT (R.omap X) ≡⟨⟩
join pure ≡⟨ proj₁ isInverse
𝟙
join <<< pure ≡⟨ fst isInverse
identity
inv-r = begin
joinT X R.fmap (pureT X) ≡⟨⟩
join fmap pure ≡⟨ proj₂ isInverse
𝟙
joinT X <<< R.fmap (pureT X) ≡⟨⟩
join <<< fmap pure ≡⟨ snd isInverse
identity
back : K.Monad M.Monad
Monoidal.Monad.raw (back m) = backRaw m
@ -101,22 +104,22 @@ module _ {a b : Level} ( : Category a b) where
K.RawMonad.bind (K.Monad.raw m)
bindEq {X} {Y} = begin
K.RawMonad.bind (forthRaw (backRaw m)) ≡⟨⟩
(λ f join fmap f) ≡⟨⟩
(λ f bind (f >>> pure) >>> bind 𝟙) ≡⟨ funExt lem
(λ f join <<< fmap f) ≡⟨⟩
(λ f bind (f >>> pure) >>> bind identity) ≡⟨ funExt lem
(λ f bind f) ≡⟨⟩
bind
where
lem : (f : Arrow X (omap Y))
bind (f >>> pure) >>> bind 𝟙
bind (f >>> pure) >>> bind identity
bind f
lem f = begin
bind (f >>> pure) >>> bind 𝟙
bind (f >>> pure) >>> bind identity
≡⟨ isDistributive _ _
bind ((f >>> pure) >>> bind 𝟙)
bind ((f >>> pure) >>> bind identity)
≡⟨ cong bind .isAssociative
bind (f >>> (pure >>> bind 𝟙))
bind (f >>> (pure >>> bind identity))
≡⟨ cong (λ φ bind (f >>> φ)) (isNatural _)
bind (f >>> 𝟙)
bind (f >>> identity)
≡⟨ cong bind .leftIdentity
bind f
@ -139,29 +142,29 @@ module _ {a b : Level} ( : Category a b) where
bindEq : {X Y} {f : Arrow X (Romap Y)} KM.bind f bind f
bindEq {X} {Y} {f} = begin
KM.bind f ≡⟨⟩
joinT Y Rfmap f ≡⟨⟩
joinT Y <<< fmap f ≡⟨⟩
bind f
joinEq : {X} KM.join joinT X
joinEq {X} = begin
KM.join ≡⟨⟩
KM.bind 𝟙 ≡⟨⟩
bind 𝟙 ≡⟨⟩
joinT X Rfmap 𝟙 ≡⟨ cong (λ φ _ φ) R.isIdentity
joinT X 𝟙 ≡⟨ .rightIdentity
KM.bind identity ≡⟨⟩
bind identity ≡⟨⟩
joinT X <<< fmap identity ≡⟨ cong (λ φ _ <<< φ) R.isIdentity
joinT X <<< identity ≡⟨ .rightIdentity
joinT X
fmapEq : {A B} KM.fmap {A} {B} Rfmap
fmapEq : {A B} KM.fmap {A} {B} fmap
fmapEq {A} {B} = funExt (λ f begin
KM.fmap f ≡⟨⟩
KM.bind (f >>> KM.pure) ≡⟨⟩
bind (f >>> pureT _) ≡⟨⟩
Rfmap (f >>> pureT B) >>> joinT B ≡⟨⟩
Rfmap (f >>> pureT B) >>> joinT B ≡⟨ cong (λ φ φ >>> joinT B) R.isDistributive
Rfmap f >>> Rfmap (pureT B) >>> joinT B ≡⟨ .isAssociative
joinT B Rfmap (pureT B) Rfmap f ≡⟨ cong (λ φ φ Rfmap f) (proj₂ isInverse)
𝟙 Rfmap f ≡⟨ .leftIdentity
Rfmap f
fmap (f >>> pureT B) >>> joinT B ≡⟨⟩
fmap (f >>> pureT B) >>> joinT B ≡⟨ cong (λ φ φ >>> joinT B) R.isDistributive
fmap f >>> fmap (pureT B) >>> joinT B ≡⟨ .isAssociative
joinT B <<< fmap (pureT B) <<< fmap f ≡⟨ cong (λ φ φ <<< fmap f) (snd isInverse)
identity <<< fmap f ≡⟨ .leftIdentity
fmap f
)
rawEq : Functor.raw KM.R Functor.raw R
@ -171,21 +174,19 @@ module _ {a b : Level} ( : Category a b) where
Req : M.RawMonad.R (backRaw (forth m)) R
Req = Functor≡ rawEq
open NaturalTransformation
pureTEq : M.RawMonad.pureT (backRaw (forth m)) pureT
pureTEq = funExt (λ X refl)
pureNTEq : (λ i NaturalTransformation F.identity (Req i))
pureNTEq : (λ i NaturalTransformation Functors.identity (Req i))
[ M.RawMonad.pureNT (backRaw (forth m)) pureNT ]
pureNTEq = lemSigP (λ i propIsNatural F.identity (Req i)) _ _ pureTEq
pureNTEq = lemSigP (λ i propIsNatural Functors.identity (Req i)) _ _ pureTEq
joinTEq : M.RawMonad.joinT (backRaw (forth m)) joinT
joinTEq = funExt (λ X begin
M.RawMonad.joinT (backRaw (forth m)) X ≡⟨⟩
KM.join ≡⟨⟩
joinT X Rfmap 𝟙 ≡⟨ cong (λ φ joinT X φ) R.isIdentity
joinT X 𝟙 ≡⟨ .rightIdentity
joinT X <<< fmap identity ≡⟨ cong (λ φ joinT X <<< φ) R.isIdentity
joinT X <<< identity ≡⟨ .rightIdentity
joinT X )
joinNTEq : (λ i NaturalTransformation F[ Req i Req i ] (Req i))
@ -205,8 +206,8 @@ module _ {a b : Level} ( : Category a b) where
open import Cat.Equivalence
MonoidalKleisli : M.Monad K.Monad
Monoidal≅Kleisli = forth , (back , (record { verso-recto = funExt backeq ; recto-verso = funExt fortheq }))
MonoidalKleisli : M.Monad K.Monad
Monoidal≊Kleisli = forth , back , funExt backeq , funExt fortheq
Monoidal≃Kleisli : M.Monad K.Monad
Monoidal≃Kleisli = forth , eqv
Monoidal≡Kleisli : M.Monad K.Monad
Monoidal≡Kleisli = isoToPath Monoidal≊Kleisli

View file

@ -1,22 +1,24 @@
{---
The Kleisli formulation of monads
---}
{-# OPTIONS --cubical --allow-unsolved-metas #-}
{-# OPTIONS --cubical #-}
open import Agda.Primitive
open import Cat.Prelude
open import Cat.Category
open import Cat.Category.Functor as F
open import Cat.Category.NaturalTransformation
open import Cat.Categories.Fun
-- "A monad in the Kleisli form" [voe]
module Cat.Category.Monad.Kleisli {a b : Level} ( : Category a b) where
open import Cat.Category.NaturalTransformation
using (NaturalTransformation ; Transformation ; Natural)
private
= a b
module = Category
open using (Arrow ; 𝟙 ; Object ; _∘_ ; _>>>_)
open using (Arrow ; identity ; Object ; _<<<_ ; _>>>_)
-- | Data for a monad.
--
@ -32,7 +34,7 @@ record RawMonad : Set where
--
-- This should perhaps be defined in a "Klesli-version" of functors as well?
fmap : {A B} [ A , B ] [ omap A , omap B ]
fmap f = bind (pure f)
fmap f = bind (pure <<< f)
-- | Composition of monads aka. the kleisli-arrow.
_>=>_ : {A B C : Object} [ A , omap B ] [ B , omap C ] [ A , omap C ]
@ -40,7 +42,7 @@ record RawMonad : Set where
-- | Flattening nested monads.
join : {A : Object} [ omap (omap A) , omap A ]
join = bind 𝟙
join = bind identity
------------------
-- * Monad laws --
@ -48,26 +50,33 @@ record RawMonad : Set where
-- There may be better names than what I've chosen here.
-- `pure` is the neutral element for `bind`
IsIdentity = {X : Object}
bind pure 𝟙 {omap X}
bind pure identity {omap X}
-- pure is the left-identity for the kleisli arrow.
IsNatural = {X Y : Object} (f : [ X , omap Y ])
pure >>> (bind f) f
IsDistributive = {X Y Z : Object} (g : [ Y , omap Z ]) (f : [ X , omap Y ])
pure >=> f f
-- Composition interacts with bind in the following way.
IsDistributive = {X Y Z : Object}
(g : [ Y , omap Z ]) (f : [ X , omap Y ])
(bind f) >>> (bind g) bind (f >=> g)
RightIdentity = {A B : Object} {m : [ A , omap B ]}
m >=> pure m
-- | Functor map fusion.
--
-- This is really a functor law. Should we have a kleisli-representation of
-- functors as well and make them a super-class?
Fusion = {X Y Z : Object} {g : [ Y , Z ]} {f : [ X , Y ]}
fmap (g f) fmap g fmap f
fmap (g <<< f) fmap g <<< fmap f
-- In the ("foreign") formulation of a monad `IsNatural`'s analogue here would be:
IsNaturalForeign : Set _
IsNaturalForeign = {X : Object} join {X} fmap join join join
IsNaturalForeign = {X : Object} join {X} <<< fmap join join <<< join
IsInverse : Set _
IsInverse = {X : Object} join {X} pure 𝟙 × join {X} fmap pure 𝟙
IsInverse = {X : Object} join {X} <<< pure identity × join {X} <<< fmap pure identity
record IsMonad (raw : RawMonad) : Set where
open RawMonad raw public
@ -79,18 +88,21 @@ record IsMonad (raw : RawMonad) : Set where
-- | Map fusion is admissable.
fusion : Fusion
fusion {g = g} {f} = begin
fmap (g f) ≡⟨⟩
fmap (g <<< f) ≡⟨⟩
bind ((f >>> g) >>> pure) ≡⟨ cong bind .isAssociative
bind (f >>> (g >>> pure)) ≡⟨ cong (λ φ bind (f >>> φ)) (sym (isNatural _))
bind (f >>> (pure >>> (bind (g >>> pure)))) ≡⟨⟩
bind (f >>> (g >>> pure))
≡⟨ cong (λ φ bind (f >>> φ)) (sym (isNatural _))
bind (f >>> (pure >>> (bind (g >>> pure))))
≡⟨⟩
bind (f >>> (pure >>> fmap g)) ≡⟨⟩
bind ((fmap g pure) f) ≡⟨ cong bind (sym .isAssociative)
bind (fmap g (pure f)) ≡⟨ sym distrib
bind (pure g) bind (pure f) ≡⟨⟩
fmap g fmap f
bind ((fmap g <<< pure) <<< f) ≡⟨ cong bind (sym .isAssociative)
bind (fmap g <<< (pure <<< f)) ≡⟨ sym distrib
bind (pure <<< g) <<< bind (pure <<< f)
≡⟨⟩
fmap g <<< fmap f
where
distrib : fmap g fmap f bind (fmap g (pure f))
distrib = isDistributive (pure g) (pure f)
distrib : fmap g <<< fmap f bind (fmap g <<< (pure <<< f))
distrib = isDistributive (pure <<< g) (pure <<< f)
-- | This formulation gives rise to the following endo-functor.
private
@ -100,15 +112,15 @@ record IsMonad (raw : RawMonad) : Set where
isFunctorR : IsFunctor rawR
IsFunctor.isIdentity isFunctorR = begin
bind (pure 𝟙) ≡⟨ cong bind (.rightIdentity)
bind (pure <<< identity) ≡⟨ cong bind (.rightIdentity)
bind pure ≡⟨ isIdentity
𝟙
identity
IsFunctor.isDistributive isFunctorR {f = f} {g} = begin
bind (pure (g f)) ≡⟨⟩
fmap (g f) ≡⟨ fusion
fmap g fmap f ≡⟨⟩
bind (pure g) bind (pure f)
bind (pure <<< (g <<< f)) ≡⟨⟩
fmap (g <<< f) ≡⟨ fusion
fmap g <<< fmap f ≡⟨⟩
bind (pure <<< g) <<< bind (pure <<< f)
-- FIXME Naming!
R : EndoFunctor
@ -116,10 +128,8 @@ record IsMonad (raw : RawMonad) : Set where
Functor.isFunctor R = isFunctorR
private
open NaturalTransformation
R⁰ : EndoFunctor
R⁰ = F.identity
R⁰ = Functors.identity
: EndoFunctor
= F[ R R ]
module R = Functor R
@ -129,66 +139,66 @@ record IsMonad (raw : RawMonad) : Set where
pureT A = pure
pureN : Natural R⁰ R pureT
pureN {A} {B} f = begin
pureT B R⁰.fmap f ≡⟨⟩
pure f ≡⟨ sym (isNatural _)
bind (pure f) pure ≡⟨⟩
fmap f pure ≡⟨⟩
R.fmap f pureT A
pureT B <<< R⁰.fmap f ≡⟨⟩
pure <<< f ≡⟨ sym (isNatural _)
bind (pure <<< f) <<< pure ≡⟨⟩
fmap f <<< pure ≡⟨⟩
R.fmap f <<< pureT A
joinT : Transformation R
joinT C = join
joinN : Natural R joinT
joinN f = begin
join R².fmap f ≡⟨⟩
bind 𝟙 R².fmap f ≡⟨⟩
R².fmap f >>> bind 𝟙 ≡⟨⟩
fmap (fmap f) >>> bind 𝟙 ≡⟨⟩
fmap (bind (f >>> pure)) >>> bind 𝟙 ≡⟨⟩
bind (bind (f >>> pure) >>> pure) >>> bind 𝟙
join <<< R².fmap f ≡⟨⟩
bind identity <<< R².fmap f ≡⟨⟩
R².fmap f >>> bind identity ≡⟨⟩
fmap (fmap f) >>> bind identity ≡⟨⟩
fmap (bind (f >>> pure)) >>> bind identity ≡⟨⟩
bind (bind (f >>> pure) >>> pure) >>> bind identity
≡⟨ isDistributive _ _
bind ((bind (f >>> pure) >>> pure) >=> 𝟙)
bind ((bind (f >>> pure) >>> pure) >=> identity)
≡⟨⟩
bind ((bind (f >>> pure) >>> pure) >>> bind 𝟙)
bind ((bind (f >>> pure) >>> pure) >>> bind identity)
≡⟨ cong bind .isAssociative
bind (bind (f >>> pure) >>> (pure >>> bind 𝟙))
bind (bind (f >>> pure) >>> (pure >>> bind identity))
≡⟨ cong (λ φ bind (bind (f >>> pure) >>> φ)) (isNatural _)
bind (bind (f >>> pure) >>> 𝟙)
bind (bind (f >>> pure) >>> identity)
≡⟨ cong bind .leftIdentity
bind (bind (f >>> pure))
≡⟨ cong bind (sym .rightIdentity)
bind (𝟙 >>> bind (f >>> pure)) ≡⟨⟩
bind (𝟙 >=> (f >>> pure))
bind (identity >>> bind (f >>> pure)) ≡⟨⟩
bind (identity >=> (f >>> pure))
≡⟨ sym (isDistributive _ _)
bind 𝟙 >>> bind (f >>> pure) ≡⟨⟩
bind 𝟙 >>> fmap f ≡⟨⟩
bind 𝟙 >>> R.fmap f ≡⟨⟩
R.fmap f bind 𝟙 ≡⟨⟩
R.fmap f join
bind identity >>> bind (f >>> pure) ≡⟨⟩
bind identity >>> fmap f ≡⟨⟩
bind identity >>> R.fmap f ≡⟨⟩
R.fmap f <<< bind identity ≡⟨⟩
R.fmap f <<< join
pureNT : NaturalTransformation R⁰ R
proj₁ pureNT = pureT
proj₂ pureNT = pureN
fst pureNT = pureT
snd pureNT = pureN
joinNT : NaturalTransformation R
proj₁ joinNT = joinT
proj₂ joinNT = joinN
fst joinNT = joinT
snd joinNT = joinN
isNaturalForeign : IsNaturalForeign
isNaturalForeign = begin
fmap join >>> join ≡⟨⟩
bind (join >>> pure) >>> bind 𝟙
bind (join >>> pure) >>> bind identity
≡⟨ isDistributive _ _
bind ((join >>> pure) >>> bind 𝟙)
bind ((join >>> pure) >>> bind identity)
≡⟨ cong bind .isAssociative
bind (join >>> (pure >>> bind 𝟙))
bind (join >>> (pure >>> bind identity))
≡⟨ cong (λ φ bind (join >>> φ)) (isNatural _)
bind (join >>> 𝟙)
bind (join >>> identity)
≡⟨ cong bind .leftIdentity
bind join ≡⟨⟩
bind (bind 𝟙)
bind (bind identity)
≡⟨ cong bind (sym .rightIdentity)
bind (𝟙 >>> bind 𝟙) ≡⟨⟩
bind (𝟙 >=> 𝟙) ≡⟨ sym (isDistributive _ _)
bind 𝟙 >>> bind 𝟙 ≡⟨⟩
bind (identity >>> bind identity) ≡⟨⟩
bind (identity >=> identity) ≡⟨ sym (isDistributive _ _)
bind identity >>> bind identity ≡⟨⟩
join >>> join
isInverse : IsInverse
@ -196,21 +206,28 @@ record IsMonad (raw : RawMonad) : Set where
where
inv-l = begin
pure >>> join ≡⟨⟩
pure >>> bind 𝟙 ≡⟨ isNatural _
𝟙
pure >>> bind identity ≡⟨ isNatural _
identity
inv-r = begin
fmap pure >>> join ≡⟨⟩
bind (pure >>> pure) >>> bind 𝟙
bind (pure >>> pure) >>> bind identity
≡⟨ isDistributive _ _
bind ((pure >>> pure) >=> 𝟙) ≡⟨⟩
bind ((pure >>> pure) >>> bind 𝟙)
bind ((pure >>> pure) >=> identity) ≡⟨⟩
bind ((pure >>> pure) >>> bind identity)
≡⟨ cong bind .isAssociative
bind (pure >>> (pure >>> bind 𝟙))
bind (pure >>> (pure >>> bind identity))
≡⟨ cong (λ φ bind (pure >>> φ)) (isNatural _)
bind (pure >>> 𝟙)
bind (pure >>> identity)
≡⟨ cong bind .leftIdentity
bind pure ≡⟨ isIdentity
𝟙
identity
rightIdentity : RightIdentity
rightIdentity {m = m} = begin
m >=> pure ≡⟨⟩
m >>> bind pure ≡⟨ cong (m >>>_) isIdentity
m >>> identity ≡⟨ .leftIdentity
m
record Monad : Set where
field

View file

@ -1,14 +1,13 @@
{---
Monoidal formulation of monads
---}
{-# OPTIONS --cubical --allow-unsolved-metas #-}
{-# OPTIONS --cubical #-}
open import Agda.Primitive
open import Cat.Prelude
open import Cat.Category
open import Cat.Category.Functor as F
open import Cat.Category.NaturalTransformation
open import Cat.Categories.Fun
module Cat.Category.Monad.Monoidal {a b : Level} ( : Category a b) where
@ -17,43 +16,55 @@ module Cat.Category.Monad.Monoidal {a b : Level} ( : Category a b
private
= a b
open Category using (Object ; Arrow ; 𝟙 ; _∘_)
open NaturalTransformation
open Category using (Object ; Arrow ; identity ; _<<<_)
open import Cat.Category.NaturalTransformation
using (NaturalTransformation ; Transformation ; Natural)
record RawMonad : Set where
field
R : EndoFunctor
pureNT : NaturalTransformation F.identity R
pureNT : NaturalTransformation Functors.identity R
joinNT : NaturalTransformation F[ R R ] R
Romap = Functor.omap R
fmap = Functor.fmap R
-- Note that `pureT` and `joinT` differs from their definition in the
-- kleisli formulation only by having an explicit parameter.
pureT : Transformation F.identity R
pureT = proj₁ pureNT
pureN : Natural F.identity R pureT
pureN = proj₂ pureNT
pureT : Transformation Functors.identity R
pureT = fst pureNT
pure : {X : Object} [ X , Romap X ]
pure = pureT _
pureN : Natural Functors.identity R pureT
pureN = snd pureNT
joinT : Transformation F[ R R ] R
joinT = proj₁ joinNT
joinT = fst joinNT
join : {X : Object} [ Romap (Romap X) , Romap X ]
join = joinT _
joinN : Natural F[ R R ] R joinT
joinN = proj₂ joinNT
Romap = Functor.omap R
Rfmap = Functor.fmap R
joinN = snd joinNT
bind : {X Y : Object} [ X , Romap Y ] [ Romap X , Romap Y ]
bind {X} {Y} f = joinT Y Rfmap f
bind {X} {Y} f = join <<< fmap f
IsAssociative : Set _
IsAssociative = {X : Object}
joinT X Rfmap (joinT X) joinT X joinT (Romap X)
-- R and join commute
joinT X <<< fmap join join <<< join
IsInverse : Set _
IsInverse = {X : Object}
joinT X pureT (Romap X) 𝟙
× joinT X Rfmap (pureT X) 𝟙
IsNatural = {X Y} f joinT Y Rfmap f pureT X f
-- Talks about R's action on objects
join <<< pure identity {Romap X}
-- Talks about R's action on arrows
× join <<< fmap pure identity {Romap X}
IsNatural = {X Y} (f : Arrow X (Romap Y))
join <<< fmap f <<< pure f
IsDistributive = {X Y Z} (g : Arrow Y (Romap Z)) (f : Arrow X (Romap Y))
joinT Z Rfmap g (joinT Y Rfmap f)
joinT Z Rfmap (joinT Z Rfmap g f)
join <<< fmap g <<< (join <<< fmap f)
join <<< fmap (join <<< fmap g <<< f)
record IsMonad (raw : RawMonad) : Set where
open RawMonad raw public
@ -67,11 +78,11 @@ record IsMonad (raw : RawMonad) : Set where
isNatural : IsNatural
isNatural {X} {Y} f = begin
joinT Y R.fmap f pureT X ≡⟨ sym .isAssociative
joinT Y (R.fmap f pureT X) ≡⟨ cong (λ φ joinT Y φ) (sym (pureN f))
joinT Y (pureT (R.omap Y) f) ≡⟨ .isAssociative
joinT Y pureT (R.omap Y) f ≡⟨ cong (λ φ φ f) (proj₁ isInverse)
𝟙 f ≡⟨ .leftIdentity
joinT Y <<< R.fmap f <<< pureT X ≡⟨ sym .isAssociative
joinT Y <<< (R.fmap f <<< pureT X) ≡⟨ cong (λ φ joinT Y <<< φ) (sym (pureN f))
joinT Y <<< (pureT (R.omap Y) <<< f) ≡⟨ .isAssociative
joinT Y <<< pureT (R.omap Y) <<< f ≡⟨ cong (λ φ φ <<< f) (fst isInverse)
identity <<< f ≡⟨ .leftIdentity
f
isDistributive : IsDistributive
@ -79,36 +90,36 @@ record IsMonad (raw : RawMonad) : Set where
where
module R² = Functor F[ R R ]
distrib3 : {A B C D} {a : Arrow C D} {b : Arrow B C} {c : Arrow A B}
R.fmap (a b c)
R.fmap a R.fmap b R.fmap c
R.fmap (a <<< b <<< c)
R.fmap a <<< R.fmap b <<< R.fmap c
distrib3 {a = a} {b} {c} = begin
R.fmap (a b c) ≡⟨ R.isDistributive
R.fmap (a b) R.fmap c ≡⟨ cong (_ _) R.isDistributive
R.fmap a R.fmap b R.fmap c
R.fmap (a <<< b <<< c) ≡⟨ R.isDistributive
R.fmap (a <<< b) <<< R.fmap c ≡⟨ cong (_<<< _) R.isDistributive
R.fmap a <<< R.fmap b <<< R.fmap c
aux = begin
joinT Z R.fmap (joinT Z R.fmap g f)
≡⟨ cong (λ φ joinT Z φ) distrib3
joinT Z (R.fmap (joinT Z) R.fmap (R.fmap g) R.fmap f)
joinT Z <<< R.fmap (joinT Z <<< R.fmap g <<< f)
≡⟨ cong (λ φ joinT Z <<< φ) distrib3
joinT Z <<< (R.fmap (joinT Z) <<< R.fmap (R.fmap g) <<< R.fmap f)
≡⟨⟩
joinT Z (R.fmap (joinT Z) R².fmap g R.fmap f)
≡⟨ cong (__ (joinT Z)) (sym .isAssociative)
joinT Z (R.fmap (joinT Z) (R².fmap g R.fmap f))
joinT Z <<< (R.fmap (joinT Z) <<< R².fmap g <<< R.fmap f)
≡⟨ cong (_<<<_ (joinT Z)) (sym .isAssociative)
joinT Z <<< (R.fmap (joinT Z) <<< (R².fmap g <<< R.fmap f))
≡⟨ .isAssociative
(joinT Z R.fmap (joinT Z)) (R².fmap g R.fmap f)
≡⟨ cong (λ φ φ (R².fmap g R.fmap f)) isAssociative
(joinT Z joinT (R.omap Z)) (R².fmap g R.fmap f)
(joinT Z <<< R.fmap (joinT Z)) <<< (R².fmap g <<< R.fmap f)
≡⟨ cong (λ φ φ <<< (R².fmap g <<< R.fmap f)) isAssociative
(joinT Z <<< joinT (R.omap Z)) <<< (R².fmap g <<< R.fmap f)
≡⟨ .isAssociative
joinT Z joinT (R.omap Z) R².fmap g R.fmap f
joinT Z <<< joinT (R.omap Z) <<< R².fmap g <<< R.fmap f
≡⟨⟩
((joinT Z joinT (R.omap Z)) R².fmap g) R.fmap f
≡⟨ cong (_ R.fmap f) (sym .isAssociative)
(joinT Z (joinT (R.omap Z) R².fmap g)) R.fmap f
≡⟨ cong (λ φ φ R.fmap f) (cong (_∘_ (joinT Z)) (joinN g))
(joinT Z (R.fmap g joinT Y)) R.fmap f
≡⟨ cong (_ R.fmap f) .isAssociative
joinT Z R.fmap g joinT Y R.fmap f
((joinT Z <<< joinT (R.omap Z)) <<< R².fmap g) <<< R.fmap f
≡⟨ cong (_<<< R.fmap f) (sym .isAssociative)
(joinT Z <<< (joinT (R.omap Z) <<< R².fmap g)) <<< R.fmap f
≡⟨ cong (λ φ φ <<< R.fmap f) (cong (_<<<_ (joinT Z)) (joinN g))
(joinT Z <<< (R.fmap g <<< joinT Y)) <<< R.fmap f
≡⟨ cong (_<<< R.fmap f) .isAssociative
joinT Z <<< R.fmap g <<< joinT Y <<< R.fmap f
≡⟨ sym (Category.isAssociative )
joinT Z R.fmap g (joinT Y R.fmap f)
joinT Z <<< R.fmap g <<< (joinT Y <<< R.fmap f)
record Monad : Set where
@ -128,8 +139,8 @@ private
where
xX = x {X}
yX = y {X}
e1 = Category.arrowsAreSets _ _ (proj₁ xX) (proj₁ yX)
e2 = Category.arrowsAreSets _ _ (proj₂ xX) (proj₂ yX)
e1 = Category.arrowsAreSets _ _ (fst xX) (fst yX)
e2 = Category.arrowsAreSets _ _ (snd xX) (snd yX)
open IsMonad
propIsMonad : (raw : _) isProp (IsMonad raw)

View file

@ -1,25 +1,24 @@
{-
This module provides construction 2.3 in [voe]
-}
{-# OPTIONS --cubical --allow-unsolved-metas --caching #-}
{-# OPTIONS --cubical --caching #-}
module Cat.Category.Monad.Voevodsky where
open import Cat.Prelude
open import Function
open import Cat.Category
open import Cat.Category.Functor as F
open import Cat.Category.NaturalTransformation
import Cat.Category.NaturalTransformation
open import Cat.Category.Monad
open import Cat.Categories.Fun
open import Cat.Equivalence
module voe {a b : Level} ( : Category a b) where
open Cat.Category.NaturalTransformation
private
= a b
module = Category
open using (Object ; Arrow)
open NaturalTransformation
module M = Monoidal
module K = Kleisli
@ -50,9 +49,9 @@ module voe {a b : Level} ( : Category a b) where
pureT X = pure {X}
field
pureN : Natural F.identity R pureT
pureN : Natural Functors.identity R pureT
pureNT : NaturalTransformation F.identity R
pureNT : NaturalTransformation Functors.identity R
pureNT = pureT , pureN
joinT : (A : Object) [ omap (omap A) , omap A ]
@ -72,12 +71,12 @@ module voe {a b : Level} ( : Category a b) where
}
field
isMnd : IsMonad rawMnd
isMonad : IsMonad rawMnd
toMonad : Monad
toMonad = record
{ raw = rawMnd
; isMonad = isMnd
; isMonad = isMonad
}
record §2 : Set where
@ -94,43 +93,37 @@ module voe {a b : Level} ( : Category a b) where
}
field
isMnd : IsMonad rawMnd
isMonad : IsMonad rawMnd
toMonad : Monad
toMonad = record
{ raw = rawMnd
; isMonad = isMnd
; isMonad = isMonad
}
§1-fromMonad : (m : M.Monad) §2-3.§1 (M.Monad.Romap m) (λ {X} M.Monad.pureT m X)
-- voe-2-3-1-fromMonad : (m : M.Monad) → voe.§2-3.§1 (M.Monad.Romap m) (λ {X} → M.Monad.pureT m X)
§1-fromMonad m = record
{ fmap = Functor.fmap R
; RisFunctor = Functor.isFunctor R
; pureN = pureN
; join = λ {X} joinT X
; joinN = joinN
; isMnd = M.Monad.isMonad m
; isMonad = M.Monad.isMonad m
}
where
raw = M.Monad.raw m
R = M.RawMonad.R raw
pureT = M.RawMonad.pureT raw
pureN = M.RawMonad.pureN raw
joinT = M.RawMonad.joinT raw
joinN = M.RawMonad.joinN raw
open M.Monad m
§2-fromMonad : (m : K.Monad) §2-3.§2 (K.Monad.omap m) (K.Monad.pure m)
§2-fromMonad m = record
{ bind = K.Monad.bind m
; isMnd = K.Monad.isMonad m
; isMonad = K.Monad.isMonad m
}
-- | In the following we seek to transform the equivalence `Monoidal≃Kleisli`
-- | to talk about voevodsky's construction.
module _ (omap : Omap ) (pure : {X : Object} Arrow X (omap X)) where
private
module E = AreInverses (Monoidal≅Kleisli .proj₂ .proj₂)
module E = AreInverses {f = (fst (Monoidal≊Kleisli ))} {fst (snd (Monoidal≊Kleisli ))}(Monoidal≊Kleisli .snd .snd)
Monoidal→Kleisli : M.Monad K.Monad
Monoidal→Kleisli = E.obverse
@ -138,10 +131,10 @@ module voe {a b : Level} ( : Category a b) where
Kleisli→Monoidal : K.Monad M.Monad
Kleisli→Monoidal = E.reverse
ve-re : Kleisli→Monoidal Monoidal→Kleisli Function.id
ve-re : Kleisli→Monoidal Monoidal→Kleisli idFun _
ve-re = E.verso-recto
re-ve : Monoidal→Kleisli Kleisli→Monoidal Function.id
re-ve : Monoidal→Kleisli Kleisli→Monoidal idFun _
re-ve = E.recto-verso
forth : §2-3.§1 omap pure §2-3.§2 omap pure
@ -178,9 +171,6 @@ module voe {a b : Level} ( : Category a b) where
where
t' : ((Monoidal→Kleisli Kleisli→Monoidal) §2-3.§2.toMonad {omap} {pure})
§2-3.§2.toMonad
cong-d : {} {A : Set } {'} {B : A Set '} {x y : A}
(f : (x : A) B x) (eq : x y) PathP (\ i B (eq i)) (f x) (f y)
cong-d f p = λ i f (p i)
t' = cong (\ φ φ §2-3.§2.toMonad) re-ve
t : (§2-fromMonad (Monoidal→Kleisli Kleisli→Monoidal) §2-3.§2.toMonad {omap} {pure})
(§2-fromMonad §2-3.§2.toMonad)

View file

@ -1,3 +1,4 @@
{-# OPTIONS --allow-unsolved-metas #-}
module Cat.Category.Monoid where
open import Agda.Primitive
@ -6,9 +7,10 @@ open import Cat.Category
open import Cat.Category.Product
open import Cat.Category.Functor
import Cat.Categories.Cat as Cat
open import Cat.Prelude hiding (_×_ ; empty)
-- TODO: Incorrect!
module _ (a b : Level) where
module _ {a b : Level} where
private
= lsuc (a b)
@ -21,30 +23,34 @@ module _ (a b : Level) where
_×_ : {a b} Category a b Category a b Category a b
× 𝔻 = Cat.CatProduct.object 𝔻
record RawMonoidalCategory : Set where
record RawMonoidalCategory ( : Category a b) : Set where
open Category public hiding (IsAssociative)
field
category : Category a b
open Category category public
field
{{hasProducts}} : HasProducts category
empty : Object
-- aka. tensor product, monoidal product.
append : Functor (category × category) category
open HasProducts hasProducts public
append : Functor ( × )
record MonoidalCategory : Set where
module F = Functor append
_⊗_ = append
mappend = F.fmap
IsAssociative : Set _
IsAssociative = {A B : Object} (f g h : Arrow A A) mappend ({!mappend!} , {!mappend!}) mappend (f , mappend (g , h))
record MonoidalCategory ( : Category a b) : Set where
field
raw : RawMonoidalCategory
raw : RawMonoidalCategory
open RawMonoidalCategory raw public
module _ {a b : Level} ( : MonoidalCategory a b) where
module _ {a b : Level} ( : Category a b) {monoidal : MonoidalCategory } {hasProducts : HasProducts } where
private
= a b
open MonoidalCategory public
open MonoidalCategory monoidal public hiding (mappend)
open HasProducts hasProducts
record Monoid : Set where
record MonoidalObject (M : Object) : Set where
field
carrier : Object
mempty : Arrow empty carrier
mappend : Arrow (carrier × carrier) carrier
mempty : Arrow empty M
mappend : Arrow (M × M) M

View file

@ -17,27 +17,25 @@
-- Functions for manipulating the above:
--
-- * A composition operator.
{-# OPTIONS --allow-unsolved-metas --cubical #-}
module Cat.Category.NaturalTransformation where
{-# OPTIONS --cubical #-}
open import Cat.Prelude
open import Data.Nat using (_≤_ ; z≤n ; s≤s)
open import Data.Nat using (_≤_ ; ≤′-refl ; ≤′-step)
module Nat = Data.Nat
open import Cat.Category
open import Cat.Category.Functor hiding (identity)
open import Cat.Wishlist
open import Cat.Category.Functor
module NaturalTransformation {c c' d d' : Level}
module Cat.Category.NaturalTransformation
{c c' d d' : Level}
( : Category c c') (𝔻 : Category d d') where
open Category using (Object ; 𝟙)
private
open Category using (Object)
private
module = Category
module 𝔻 = Category 𝔻
module _ (F G : Functor 𝔻) where
module _ (F G : Functor 𝔻) where
private
module F = Functor F
module G = Functor G
@ -59,28 +57,28 @@ module NaturalTransformation {c c' d d' : Level}
propIsNatural θ x y i {A} {B} f = 𝔻.arrowsAreSets _ _ (x f) (y f) i
NaturalTransformation≡ : {α β : NaturalTransformation}
(eq₁ : α .proj₁ β .proj₁)
(eq₁ : α .fst β .fst)
α β
NaturalTransformation≡ eq = lemSig propIsNatural _ _ eq
identityTrans : (F : Functor 𝔻) Transformation F F
identityTrans F C = 𝟙 𝔻
identityTrans : (F : Functor 𝔻) Transformation F F
identityTrans F C = 𝔻.identity
identityNatural : (F : Functor 𝔻) Natural F F (identityTrans F)
identityNatural F {A = A} {B = B} f = begin
identityNatural : (F : Functor 𝔻) Natural F F (identityTrans F)
identityNatural F {A = A} {B = B} f = begin
𝔻 [ identityTrans F B F→ f ] ≡⟨⟩
𝔻 [ 𝟙 𝔻 F→ f ] ≡⟨ 𝔻.leftIdentity
𝔻 [ 𝔻.identity F→ f ] ≡⟨ 𝔻.leftIdentity
F→ f ≡⟨ sym 𝔻.rightIdentity
𝔻 [ F→ f 𝟙 𝔻 ] ≡⟨⟩
𝔻 [ F→ f 𝔻.identity ] ≡⟨⟩
𝔻 [ F→ f identityTrans F A ]
where
module F = Functor F
F→ = F.fmap
identity : (F : Functor 𝔻) NaturalTransformation F F
identity F = identityTrans F , identityNatural F
identity : (F : Functor 𝔻) NaturalTransformation F F
identity F = identityTrans F , identityNatural F
module _ {F G H : Functor 𝔻} where
module _ {F G H : Functor 𝔻} where
private
module F = Functor F
module G = Functor G
@ -89,8 +87,8 @@ module NaturalTransformation {c c' d d' : Level}
T[ θ η ] C = 𝔻 [ θ C η C ]
NT[_∘_] : NaturalTransformation G H NaturalTransformation F G NaturalTransformation F H
proj₁ NT[ (θ , _) (η , _) ] = T[ θ η ]
proj₂ NT[ (θ , θNat) (η , ηNat) ] {A} {B} f = begin
fst NT[ (θ , _) (η , _) ] = T[ θ η ]
snd NT[ (θ , θNat) (η , ηNat) ] {A} {B} f = begin
𝔻 [ T[ θ η ] B F.fmap f ] ≡⟨⟩
𝔻 [ 𝔻 [ θ B η B ] F.fmap f ] ≡⟨ sym 𝔻.isAssociative
𝔻 [ θ B 𝔻 [ η B F.fmap f ] ] ≡⟨ cong (λ φ 𝔻 [ θ B φ ]) (ηNat f)
@ -100,6 +98,7 @@ module NaturalTransformation {c c' d d' : Level}
𝔻 [ H.fmap f 𝔻 [ θ A η A ] ] ≡⟨⟩
𝔻 [ H.fmap f T[ θ η ] A ]
module Properties where
module _ {F G : Functor 𝔻} where
transformationIsSet : isSet (Transformation F G)
transformationIsSet _ _ p q i j C = 𝔻.arrowsAreSets _ _ (λ l p l C) (λ l q l C) i j
@ -112,9 +111,37 @@ module NaturalTransformation {c c' d d' : Level}
naturalIsSet : (θ : Transformation F G) isSet (Natural F G θ)
naturalIsSet θ =
ntypeCommulative
(s≤s {n = Nat.suc Nat.zero} z≤n)
ntypeCumulative {n = 1}
(Data.Nat.≤′-step Data.Nat.≤′-refl)
(naturalIsProp θ)
naturalTransformationIsSet : isSet (NaturalTransformation F G)
naturalTransformationIsSet = sigPresSet transformationIsSet naturalIsSet
module _
{F G H I : Functor 𝔻}
{θ : NaturalTransformation F G}
{η : NaturalTransformation G H}
{ζ : NaturalTransformation H I} where
-- isAssociative : NT[ ζ ∘ NT[ η ∘ θ ] ] ≡ NT[ NT[ ζ ∘ η ] ∘ θ ]
isAssociative
: NT[_∘_] {F} {H} {I} ζ (NT[_∘_] {F} {G} {H} η θ)
NT[_∘_] {F} {G} {I} (NT[_∘_] {G} {H} {I} ζ η) θ
isAssociative
= lemSig (naturalIsProp {F = F} {I}) _ _
(funExt (λ _ 𝔻.isAssociative))
module _ {F G : Functor 𝔻} {θNT : NaturalTransformation F G} where
private
propNat = naturalIsProp {F = F} {G}
rightIdentity : (NT[_∘_] {F} {F} {G} θNT (identity F)) θNT
rightIdentity = lemSig propNat _ _ (funExt (λ _ 𝔻.rightIdentity))
leftIdentity : (NT[_∘_] {F} {G} {G} (identity G) θNT) θNT
leftIdentity = lemSig propNat _ _ (funExt (λ _ 𝔻.leftIdentity))
isIdentity
: (NT[_∘_] {F} {G} {G} (identity G) θNT) θNT
× (NT[_∘_] {F} {F} {G} θNT (identity F)) θNT
isIdentity = leftIdentity , rightIdentity

View file

@ -1,13 +1,12 @@
{-# OPTIONS --allow-unsolved-metas #-}
{-# OPTIONS --cubical --caching #-}
module Cat.Category.Product where
open import Cat.Prelude hiding (_×_ ; proj₁ ; proj₂)
import Data.Product as P
open import Cat.Prelude as P hiding (_×_ ; fst ; snd)
open import Cat.Equivalence
open import Cat.Category
module _ {a b : Level} ( : Category a b) where
open Category
module _ (A B : Object) where
@ -15,21 +14,19 @@ module _ {a b : Level} ( : Category a b) where
no-eta-equality
field
object : Object
proj₁ : [ object , A ]
proj₂ : [ object , B ]
fst : [ object , A ]
snd : [ object , B ]
-- FIXME Not sure this is actually a proposition - so this name is
-- misleading.
record IsProduct (raw : RawProduct) : Set (a b) where
open RawProduct raw public
field
ump : {X : Object} (f : [ X , A ]) (g : [ X , B ])
∃![ f×g ] ( [ proj₁ f×g ] f P.× [ proj₂ f×g ] g)
∃![ f×g ] ( [ fst f×g ] f P.× [ snd f×g ] g)
-- | Arrow product
_P[_×_] : {X} (π₁ : [ X , A ]) (π₂ : [ X , B ])
[ X , object ]
_P[_×_] π₁ π₂ = P.proj₁ (ump π₁ π₂)
_P[_×_] π₁ π₂ = P.fst (ump π₁ π₂)
record Product : Set (a b) where
field
@ -50,8 +47,8 @@ module _ {a b : Level} ( : Category a b) where
-- The product mentioned in awodey in Def 6.1 is not the regular product of
-- arrows. It's a "parallel" product
module _ {A A' B B' : Object} where
open Product
open Product (product A B) hiding (_P[_×_]) renaming (proj₁ to fst ; proj₂ to snd)
open Product using (_P[_×_])
open Product (product A B) hiding (_P[_×_]) renaming (fst to fst ; snd to snd)
_|×|_ : [ A , A' ] [ B , B' ] [ A × B , A' × B' ]
f |×| g = product A' B'
P[ [ f fst ]
@ -68,8 +65,14 @@ module _ {a b : Level} { : Category a b} {A B : Category.Object
module y = IsProduct y
module _ {X : Object} (f : [ X , A ]) (g : [ X , B ]) where
module _ (f×g : Arrow X y.object) where
help : isProp ({y} ( [ y.fst y ] f) P.× ( [ y.snd y ] g) f×g y)
help = propPiImpl (λ _ propPi (λ _ arrowsAreSets _ _))
res = ∃-unique (x.ump f g) (y.ump f g)
prodAux : x.ump f g y.ump f g
prodAux = {!!}
prodAux = lemSig ((λ f×g propSig (propSig (arrowsAreSets _ _) λ _ arrowsAreSets _ _) (λ _ help f×g))) _ _ res
propIsProduct' : x y
propIsProduct' i = record { ump = λ f g prodAux f g i }
@ -83,6 +86,259 @@ module _ {a b : Level} { : Category a b} {A B : Category.Object
q : (λ i IsProduct A B (p i)) [ Product.isProduct x Product.isProduct y ]
q = lemPropF propIsProduct p
module Try0 {a b : Level} { : Category a b}
(let module = Category ) {𝒜 : .Object} where
open P
module _ where
raw : RawCategory _ _
raw = record
{ Object = Σ[ X .Object ] .Arrow X 𝒜 × .Arrow X
; Arrow = λ{ (A , a0 , a1) (B , b0 , b1)
Σ[ f .Arrow A B ]
[ b0 f ] a0
× [ b1 f ] a1
}
; identity = λ{ {X , f , g} .identity {X} , .rightIdentity , .rightIdentity}
; _<<<_ = λ { {_ , a0 , a1} {_ , b0 , b1} {_ , c0 , c1} (f , f0 , f1) (g , g0 , g1)
(f .<<< g)
, (begin
[ c0 [ f g ] ] ≡⟨ .isAssociative
[ [ c0 f ] g ] ≡⟨ cong (λ φ [ φ g ]) f0
[ b0 g ] ≡⟨ g0
a0
)
, (begin
[ c1 [ f g ] ] ≡⟨ .isAssociative
[ [ c1 f ] g ] ≡⟨ cong (λ φ [ φ g ]) f1
[ b1 g ] ≡⟨ g1
a1
)
}
}
module _ where
open RawCategory raw
propEqs : {X' : Object}{Y' : Object} (let X , xa , xb = X') (let Y , ya , yb = Y')
(xy : .Arrow X Y) isProp ( [ ya xy ] xa × [ yb xy ] xb)
propEqs xs = propSig (.arrowsAreSets _ _) (\ _ .arrowsAreSets _ _)
arrowEq : {X Y : Object} {f g : Arrow X Y} fst f fst g f g
arrowEq {X} {Y} {f} {g} p = λ i p i , lemPropF propEqs p {snd f} {snd g} i
private
isAssociative : IsAssociative
isAssociative {f = f , f0 , f1} {g , g0 , g1} {h , h0 , h1} = arrowEq .isAssociative
isIdentity : IsIdentity identity
isIdentity {AA@(A , a0 , a1)} {BB@(B , b0 , b1)} {f , f0 , f1} = arrowEq .leftIdentity , arrowEq .rightIdentity
arrowsAreSets : ArrowsAreSets
arrowsAreSets {X , x0 , x1} {Y , y0 , y1}
= sigPresSet .arrowsAreSets λ a propSet (propEqs _)
isPreCat : IsPreCategory raw
IsPreCategory.isAssociative isPreCat = isAssociative
IsPreCategory.isIdentity isPreCat = isIdentity
IsPreCategory.arrowsAreSets isPreCat = arrowsAreSets
open IsPreCategory isPreCat
module _ {𝕏 𝕐 : Object} where
open Σ 𝕏 renaming (fst to X ; snd to x)
open Σ x renaming (fst to xa ; snd to xb)
open Σ 𝕐 renaming (fst to Y ; snd to y)
open Σ y renaming (fst to ya ; snd to yb)
open import Cat.Equivalence using (composeIso) renaming (_≅_ to _≅_)
step0
: ((X , xa , xb) (Y , ya , yb))
(Σ[ p (X Y) ] (PathP (λ i .Arrow (p i) 𝒜) xa ya) × (PathP (λ i .Arrow (p i) ) xb yb))
step0
= (λ p cong fst p , cong-d (fst snd) p , cong-d (snd snd) p)
-- , (λ x → λ i → fst x i , (fst (snd x) i) , (snd (snd x) i))
, (λ{ (p , q , r) Σ≡ p λ i q i , r i})
, funExt (λ{ p refl})
, funExt (λ{ (p , q , r) refl})
step1
: (Σ[ p (X Y) ] (PathP (λ i .Arrow (p i) 𝒜) xa ya) × (PathP (λ i .Arrow (p i) ) xb yb))
Σ (X .≊ Y) (λ iso
let p = .isoToId iso
in
( PathP (λ i .Arrow (p i) 𝒜) xa ya)
× PathP (λ i .Arrow (p i) ) xb yb
)
step1
= symIso
(isoSigFst
{A = (X .≊ Y)}
{B = (X Y)}
(.groupoidObject _ _)
{Q = \ p (PathP (λ i .Arrow (p i) 𝒜) xa ya) × (PathP (λ i .Arrow (p i) ) xb yb)}
.isoToId
(symIso (_ , .asTypeIso {X} {Y}) .snd)
)
step2
: Σ (X .≊ Y) (λ iso
let p = .isoToId iso
in
( PathP (λ i .Arrow (p i) 𝒜) xa ya)
× PathP (λ i .Arrow (p i) ) xb yb
)
((X , xa , xb) (Y , ya , yb))
step2
= ( λ{ (iso@(f , f~ , inv-f) , p , q)
( f , sym (.domain-twist-sym iso p) , sym (.domain-twist-sym iso q))
, ( f~ , sym (.domain-twist iso p) , sym (.domain-twist iso q))
, arrowEq (fst inv-f)
, arrowEq (snd inv-f)
}
)
, (λ{ (f , f~ , inv-f , inv-f~)
let
iso : X .≊ Y
iso = fst f , fst f~ , cong fst inv-f , cong fst inv-f~
p : X Y
p = .isoToId iso
pA : .Arrow X 𝒜 .Arrow Y 𝒜
pA = cong (λ x .Arrow x 𝒜) p
pB : .Arrow X .Arrow Y
pB = cong (λ x .Arrow x ) p
k0 = begin
coe pB xb ≡⟨ .coe-dom iso
xb .<<< fst f~ ≡⟨ snd (snd f~)
yb
k1 = begin
coe pA xa ≡⟨ .coe-dom iso
xa .<<< fst f~ ≡⟨ fst (snd f~)
ya
in iso , coe-lem-inv k1 , coe-lem-inv k0})
, funExt (λ x lemSig
(λ x propSig prop0 (λ _ prop1))
_ _
(Σ≡ refl (.propIsomorphism _ _ _)))
, funExt (λ{ (f , _) lemSig propIsomorphism _ _ (Σ≡ refl (propEqs _ _ _))})
where
prop0 : {x} isProp (PathP (λ i .Arrow (.isoToId x i) 𝒜) xa ya)
prop0 {x} = pathJ (λ y p x isProp (PathP (λ i .Arrow (p i) 𝒜) xa x)) (λ x .arrowsAreSets _ _) Y (.isoToId x) ya
prop1 : {x} isProp (PathP (λ i .Arrow (.isoToId x i) ) xb yb)
prop1 {x} = pathJ (λ y p x isProp (PathP (λ i .Arrow (p i) ) xb x)) (λ x .arrowsAreSets _ _) Y (.isoToId x) yb
-- One thing to watch out for here is that the isomorphisms going forwards
-- must compose to give idToIso
iso
: ((X , xa , xb) (Y , ya , yb))
((X , xa , xb) (Y , ya , yb))
iso = step0 step1 step2
where
infixl 5 _⊙_
_⊙_ = composeIso
equiv1
: ((X , xa , xb) (Y , ya , yb))
((X , xa , xb) (Y , ya , yb))
equiv1 = _ , fromIso _ _ (snd iso)
univalent : Univalent
univalent = univalenceFrom≃ equiv1
isCat : IsCategory raw
IsCategory.isPreCategory isCat = isPreCat
IsCategory.univalent isCat = univalent
cat : Category _ _
cat = record
{ raw = raw
; isCategory = isCat
}
open Category cat
lemma : Terminal Product 𝒜
lemma = fromIsomorphism Terminal (Product 𝒜 ) (f , g , inv)
-- C-x 8 RET MATHEMATICAL BOLD SCRIPT CAPITAL A
-- 𝒜
where
f : Terminal Product 𝒜
f ((X , x0 , x1) , uniq) = p
where
rawP : RawProduct 𝒜
rawP = record
{ object = X
; fst = x0
; snd = x1
}
-- open RawProduct rawP renaming (fst to x0 ; snd to x1)
module _ {Y : .Object} (p0 : [ Y , 𝒜 ]) (p1 : [ Y , ]) where
uy : isContr (Arrow (Y , p0 , p1) (X , x0 , x1))
uy = uniq {Y , p0 , p1}
open Σ uy renaming (fst to Y→X ; snd to contractible)
open Σ Y→X renaming (fst to p0×p1 ; snd to cond)
ump : ∃![ f×g ] ( [ x0 f×g ] p0 P.× [ x1 f×g ] p1)
ump = p0×p1 , cond , λ {f} cond-f cong fst (contractible (f , cond-f))
isP : IsProduct 𝒜 rawP
isP = record { ump = ump }
p : Product 𝒜
p = record
{ raw = rawP
; isProduct = isP
}
g : Product 𝒜 Terminal
g p = 𝒳 , t
where
open Product p renaming (object to X ; fst to x₀ ; snd to x₁) using ()
module p = Product p
module isp = IsProduct p.isProduct
𝒳 : Object
𝒳 = X , x₀ , x₁
module _ {𝒴 : Object} where
open Σ 𝒴 renaming (fst to Y)
open Σ (snd 𝒴) renaming (fst to y₀ ; snd to y₁)
ump = p.ump y₀ y₁
open Σ ump renaming (fst to f')
open Σ (snd ump) renaming (fst to f'-cond)
𝒻 : Arrow 𝒴 𝒳
𝒻 = f' , f'-cond
contractible : (f : Arrow 𝒴 𝒳) 𝒻 f
contractible ff@(f , f-cond) = res
where
k : f' f
k = snd (snd ump) f-cond
prp : (a : .Arrow Y X) isProp
( ( [ x₀ a ] y₀)
× ( [ x₁ a ] y₁)
)
prp f f0 f1 = Σ≡
(.arrowsAreSets _ _ (fst f0) (fst f1))
(.arrowsAreSets _ _ (snd f0) (snd f1))
h :
( λ i
[ x₀ k i ] y₀
× [ x₁ k i ] y₁
) [ f'-cond f-cond ]
h = lemPropF prp k
res : (f' , f'-cond) (f , f-cond)
res = Σ≡ k h
t : IsTerminal 𝒳
t {𝒴} = 𝒻 , contractible
ve-re : x g (f x) x
ve-re x = Propositionality.propTerminal _ _
re-ve : p f (g p) p
re-ve p = Product≡ e
where
module p = Product p
-- RawProduct does not have eta-equality.
e : Product.raw (f (g p)) Product.raw p
RawProduct.object (e i) = p.object
RawProduct.fst (e i) = p.fst
RawProduct.snd (e i) = p.snd
inv : AreInverses f g
inv = funExt ve-re , funExt re-ve
propProduct : isProp (Product 𝒜 )
propProduct = equivPreservesNType {n = ⟨-1⟩} lemma Propositionality.propTerminal
module _ {a b : Level} { : Category a b} {A B : Category.Object } where
open Category
private
@ -90,31 +346,12 @@ module _ {a b : Level} { : Category a b} {A B : Category.Object
private
module x = HasProducts x
module y = HasProducts y
module _ (A B : Object) where
module pX = Product (x.product A B)
module pY = Product (y.product A B)
objEq : pX.object pY.object
objEq = {!!}
proj₁Eq : (λ i [ objEq i , A ]) [ pX.proj₁ pY.proj₁ ]
proj₁Eq = {!!}
proj₂Eq : (λ i [ objEq i , B ]) [ pX.proj₂ pY.proj₂ ]
proj₂Eq = {!!}
rawEq : pX.raw pY.raw
RawProduct.object (rawEq i) = objEq i
RawProduct.proj₁ (rawEq i) = {!!}
RawProduct.proj₂ (rawEq i) = {!!}
isEq : (λ i IsProduct A B (rawEq i)) [ pX.isProduct pY.isProduct ]
isEq = {!!}
appEq : x.product A B y.product A B
appEq = Product≡ rawEq
productEq : x.product y.product
productEq i = λ A B appEq A B i
propHasProducts' : x y
propHasProducts' i = record { product = productEq i }
productEq = funExt λ A funExt λ B Try0.propProduct _ _
propHasProducts : isProp (HasProducts )
propHasProducts = propHasProducts'
propHasProducts x y i = record { product = productEq x y i }
fmap≡ : {A : Set} {a0 a1 : A} {B : Set} (f : A B) Path a0 a1 Path (f a0) (f a1)
fmap≡ = cong

View file

@ -1,4 +1,4 @@
{-# OPTIONS --allow-unsolved-metas --cubical #-}
{-# OPTIONS --cubical #-}
module Cat.Category.Yoneda where
@ -6,8 +6,11 @@ open import Cat.Prelude
open import Cat.Category
open import Cat.Category.Functor
open import Cat.Category.NaturalTransformation
renaming (module Properties to F)
using ()
open import Cat.Categories.Fun
open import Cat.Categories.Fun using (module Fun)
open import Cat.Categories.Sets hiding (presheaf)
-- There is no (small) category of categories. So we won't use _⇑_ from
@ -47,10 +50,11 @@ module _ { : Level} { : Category } where
open RawFunctor rawYoneda hiding (fmap)
isIdentity : IsIdentity
isIdentity {c} = lemSig (naturalIsProp {F = presheaf c} {presheaf c}) _ _ eq
isIdentity {c} = lemSig prp _ _ eq
where
eq : (λ C x [ .𝟙 x ]) identityTrans (presheaf c)
eq : (λ C x [ .identity x ]) identityTrans (presheaf c)
eq = funExt λ A funExt λ B .leftIdentity
prp = F.naturalIsProp _ _ {F = presheaf c} {presheaf c}
isDistributive : IsDistributive
isDistributive {A} {B} {C} {f = f} {g}

View file

@ -1,11 +1,23 @@
{-# OPTIONS --allow-unsolved-metas --cubical #-}
{-# OPTIONS --cubical #-}
module Cat.Equivalence where
open import Cubical.Primitives
open import Cubical.FromStdLib renaming (-max to _⊔_)
open import Cubical.PathPrelude hiding (inverse ; _≃_)
open import Cubical.PathPrelude hiding (inverse)
open import Cubical.PathPrelude using (isEquiv ; isContr ; fiber) public
open import Cubical.GradLemma
open import Cubical.GradLemma hiding (isoToPath)
open import Cat.Prelude using
( lemPropF ; setPi ; lemSig ; propSet
; Preorder ; equalityIsEquivalence ; propSig ; id-coe
; Setoid ; _$_ ; propPi )
import Cubical.Univalence as U
module _ { : Level} {A B : Set } where
open Cubical.PathPrelude
ua : A B A B
ua (f , isEqv) = U.ua (U.con f isEqv)
module _ {a b : Level} where
private
@ -14,46 +26,90 @@ module _ {a b : Level} where
module _ {A : Set a} {B : Set b} where
-- Quasi-inverse in [HoTT] §2.4.6
-- FIXME Maybe rename?
record AreInverses (f : A B) (g : B A) : Set where
field
verso-recto : g f idFun A
recto-verso : f g idFun B
AreInverses : (f : A B) (g : B A) Set
AreInverses f g = g f idFun A × f g idFun B
module AreInverses {f : A B} {g : B A}
(inv : AreInverses f g) where
open Σ inv renaming (fst to verso-recto ; snd to recto-verso) public
obverse = f
reverse = g
inverse = reverse
toPair : Σ _ _
toPair = verso-recto , recto-verso
Isomorphism : (f : A B) Set _
Isomorphism f = Σ (B A) λ g AreInverses f g
module _ {f : A B} {g : B A}
(inv : (g f) idFun A
× (f g) idFun B) where
open Σ inv renaming (fst to ve-re ; snd to re-ve)
toAreInverses : AreInverses f g
toAreInverses = record
{ verso-recto = ve-re
; recto-verso = re-ve
}
_≅_ : Set a Set b Set _
A B = Σ (A B) Isomorphism
symIso : {a b} {A : Set a}{B : Set b} A B B A
symIso (f , g , p , q)= g , f , q , p
module _ {a b c} {A : Set a} {B : Set b} (sB : isSet B) {Q : B Set c} (f : A B) where
Σ-fst-map : Σ A (\ a Q (f a)) Σ B Q
Σ-fst-map (x , q) = f x , q
isoSigFst : Isomorphism f Σ A (Q f) Σ B Q
isoSigFst (g , g-f , f-g) = Σ-fst-map
, (\ { (b , q) g b , transp (\ i Q (f-g (~ i) b)) q })
, funExt (\ { (a , q) Cat.Prelude.Σ≡ (\ i g-f i a)
let r = (transp-iso' ((λ i Q (f-g (i) (f a)))) q) in
transp (\ i PathP (\ j Q (sB _ _ (λ j₁ f-g j₁ (f a)) (λ j₁ f (g-f j₁ a)) i j)) (transp (λ i₁ Q (f-g (~ i₁) (f a))) q) q) r })
, funExt (\ { (b , q) Cat.Prelude.Σ≡ (\ i f-g i b) (transp-iso' (λ i Q (f-g i b)) q)})
module _ { : Level} {A B : Set } {f : A B}
(g : B A) (s : {A B : Set } isSet (A B)) where
propAreInverses : isProp (AreInverses {A = A} {B} f g)
propAreInverses x y i = record
{ verso-recto = ve-re
; recto-verso = re-ve
}
propAreInverses x y i = ve-re , re-ve
where
open AreInverses
ve-re : g f idFun A
ve-re = s (g f) (idFun A) (verso-recto x) (verso-recto y) i
ve-re = s (g f) (idFun A) (fst x) (fst y) i
re-ve : f g idFun B
re-ve = s (f g) (idFun B) (recto-verso x) (recto-verso y) i
re-ve = s (f g) (idFun B) (snd x) (snd y) i
module _ { : Level} {A B : Set } (f : A B)
(sA : isSet A) (sB : isSet B) where
propIsIso : isProp (Isomorphism f)
propIsIso = res
where
module _ (x y : Isomorphism f) where
module x = Σ x renaming (fst to inverse ; snd to areInverses)
module y = Σ y renaming (fst to inverse ; snd to areInverses)
module xA = AreInverses {f = f} {x.inverse} x.areInverses
module yA = AreInverses {f = f} {y.inverse} y.areInverses
-- I had a lot of difficulty using the corresponding proof where
-- AreInverses is defined. This is sadly a bit anti-modular. The
-- reason for my troubles is probably related to the type of objects
-- being hSet's rather than sets.
p : {f} g isProp (AreInverses {A = A} {B} f g)
p {f} g xx yy i = ve-re , re-ve
where
module xxA = AreInverses {f = f} {g} xx
module yyA = AreInverses {f = f} {g} yy
setPiB : {X : Set } isSet (X B)
setPiB = setPi (λ _ sB)
setPiA : {X : Set } isSet (X A)
setPiA = setPi (λ _ sA)
ve-re : g f idFun _
ve-re = setPiA _ _ xxA.verso-recto yyA.verso-recto i
re-ve : f g idFun _
re-ve = setPiB _ _ xxA.recto-verso yyA.recto-verso i
1eq : x.inverse y.inverse
1eq = begin
x.inverse ≡⟨⟩
x.inverse idFun _ ≡⟨ cong (λ φ x.inverse φ) (sym yA.recto-verso)
x.inverse (f y.inverse) ≡⟨⟩
(x.inverse f) y.inverse ≡⟨ cong (λ φ φ y.inverse) xA.verso-recto
idFun _ y.inverse ≡⟨⟩
y.inverse
2eq : (λ i AreInverses f (1eq i)) [ x.areInverses y.areInverses ]
2eq = lemPropF p 1eq
res : x y
res i = 1eq i , 2eq i
-- In HoTT they generalize an equivalence to have the following 3 properties:
module _ {a b : Level} (A : Set a) (B : Set b) where
@ -74,43 +130,34 @@ module _ {a b : Level} (A : Set a) (B : Set b) where
fromIso (toIso x) ≡⟨ propIsEquiv _ (fromIso (toIso x)) x
x
-- `toIso` is abstract - so I probably can't close this proof.
-- | The other inverse law does not hold in general, it does hold, however,
-- | if `A` and `B` are sets.
module _ (sA : isSet A) (sB : isSet B) where
module _ {f : A B} (iso : Isomorphism f) where
module _ {f : A B} where
module _ (iso-x iso-y : Isomorphism f) where
open Σ iso-x renaming (fst to x ; snd to inv-x)
open Σ iso-y renaming (fst to y ; snd to inv-y)
module inv-x = AreInverses inv-x
module inv-y = AreInverses inv-y
fx≡fy : x y
fx≡fy = begin
x ≡⟨ cong (λ φ x φ) (sym inv-y.recto-verso)
x ≡⟨ cong (λ φ x φ) (sym (snd inv-y))
x (f y) ≡⟨⟩
(x f) y ≡⟨ cong (λ φ φ y) inv-x.verso-recto
(x f) y ≡⟨ cong (λ φ φ y) (fst inv-x)
y
open import Cat.Prelude
propInv : g isProp (AreInverses f g)
propInv g t u i = record { verso-recto = a i ; recto-verso = b i }
propInv g t u = λ i a i , b i
where
module t = AreInverses t
module u = AreInverses u
a : t.verso-recto u.verso-recto
a i = h
a : (fst t) (fst u)
a i = funExt hh
where
hh : a (g f) a a
hh a = sA ((g f) a) a (λ i t.verso-recto i a) (λ i u.verso-recto i a) i
h : g f idFun A
h i a = hh a i
b : t.recto-verso u.recto-verso
b i = h
hh a = sA ((g f) a) a (λ i (fst t) i a) (λ i (fst u) i a) i
b : (snd t) (snd u)
b i = funExt hh
where
hh : b (f g) b b
hh b = sB _ _ (λ i t.recto-verso i b) (λ i u.recto-verso i b) i
h : f g idFun B
h i b = hh b i
hh b = sB _ _ (λ i snd t i b) (λ i snd u i b) i
inx≡iny : (λ i AreInverses f (fx≡fy i)) [ inv-x inv-y ]
inx≡iny = lemPropF propInv fx≡fy
@ -118,6 +165,7 @@ module _ {a b : Level} (A : Set a) (B : Set b) where
propIso : iso-x iso-y
propIso i = fx≡fy i , inx≡iny i
module _ (iso : Isomorphism f) where
inverse-to-from-iso : (toIso {f} fromIso {f}) iso iso
inverse-to-from-iso = begin
(toIso fromIso) iso ≡⟨⟩
@ -132,7 +180,7 @@ module _ {a b : Level} (A : Set a) (B : Set b) where
module _ {a b : Level} (A : Set a) (B : Set b) where
-- A wrapper around PathPrelude.≃
open Cubical.PathPrelude using (_≃_ ; isEquiv)
open Cubical.PathPrelude using (_≃_)
private
module _ {obverse : A B} (e : isEquiv A B obverse) where
inverse : B A
@ -142,10 +190,7 @@ module _ {a b : Level} (A : Set a) (B : Set b) where
reverse = inverse
areInverses : AreInverses obverse inverse
areInverses = record
{ verso-recto = funExt verso-recto
; recto-verso = funExt recto-verso
}
areInverses = funExt verso-recto , funExt recto-verso
where
recto-verso : b (obverse inverse) b b
recto-verso b = begin
@ -186,105 +231,314 @@ module _ {a b : Level} (A : Set a) (B : Set b) where
≃isEquiv : Equiv A B (isEquiv A B)
Equiv.fromIso ≃isEquiv {f} (f~ , iso) = gradLemma f f~ rv vr
where
open AreInverses iso
rv : (b : B) _ b
rv b i = recto-verso i b
rv b i = snd iso i b
vr : (a : A) _ a
vr a i = verso-recto i a
vr a i = fst iso i a
Equiv.toIso ≃isEquiv = toIsomorphism
Equiv.propIsEquiv ≃isEquiv = P.propIsEquiv
where
import Cubical.NType.Properties as P
module Equiv where
open Equiv ≃isEquiv public
module _ {a b : Level} {A : Set a} {B : Set b} where
open Cubical.PathPrelude using (_≃_)
-- Gives the quasi inverse from an equivalence.
module Equivalence (e : A B) where
open Equiv≃ A B public
private
iso : Isomorphism (fst e)
iso = snd (toIsomorphism e)
module _ {c : Level} {C : Set c} {f : A B} {g : B C} where
open AreInverses (snd iso) public
composeIso : {c : Level} {C : Set c} (B C) A C
composeIso {C = C} (g , g' , iso-g) = g obverse , inverse g' , inv
composeIsomorphism : Isomorphism f Isomorphism g Isomorphism (g f)
composeIsomorphism a b = f~ g~ , inv
where
module iso-g = AreInverses iso-g
inv : AreInverses (g obverse) (inverse g')
AreInverses.verso-recto inv = begin
(inverse g') (g obverse) ≡⟨⟩
(inverse (g' g) obverse)
≡⟨ cong (λ φ φ obverse) (cong (λ φ inverse φ) iso-g.verso-recto)
(inverse idFun B obverse) ≡⟨⟩
(inverse obverse) ≡⟨ verso-recto
idFun A
AreInverses.recto-verso inv = begin
g obverse inverse g'
≡⟨ cong (λ φ φ g') (cong (λ φ g φ) recto-verso)
g idFun B g' ≡⟨⟩
g g' ≡⟨ iso-g.recto-verso
idFun C
compose : {c : Level} {C : Set c} (B C) A C
compose {C = C} e = A≃C.fromIsomorphism is
where
module B≃C = Equiv≃ B C
module A≃C = Equiv≃ A C
is : A C
is = composeIso (B≃C.toIsomorphism e)
symmetryIso : B A
symmetryIso
= inverse
, obverse
, record
{ verso-recto = recto-verso
; recto-verso = verso-recto
open Σ a renaming (fst to f~ ; snd to inv-a)
open Σ b renaming (fst to g~ ; snd to inv-b)
inv : AreInverses (g f) (f~ g~)
inv = record
{ fst = begin
(f~ g~) (g f)≡⟨⟩
f~ (g~ g) f ≡⟨ cong (λ φ f~ φ f) (fst inv-b)
f~ idFun _ f ≡⟨⟩
f~ f ≡⟨ (fst inv-a)
idFun A
; snd = begin
(g f) (f~ g~)≡⟨⟩
g (f f~) g~ ≡⟨ cong (λ φ g φ g~) (snd inv-a)
g g~ ≡⟨ (snd inv-b)
idFun C
}
symmetry : B A
symmetry = B≃A.fromIsomorphism symmetryIso
composeIsEquiv : isEquiv A B f isEquiv B C g isEquiv A C (g f)
composeIsEquiv a b = fromIso A C (composeIsomorphism a' b')
where
module B≃A = Equiv≃ B A
a' = toIso A B a
b' = toIso B C b
composeIso : {c : Level} {C : Set c} (A B) (B C) A C
composeIso {C = C} (f , iso-f) (g , iso-g) = g f , composeIsomorphism iso-f iso-g
symmetryIso : (A B) B A
symmetryIso (inverse , obverse , verso-recto , recto-verso)
= obverse
, inverse
, recto-verso
, verso-recto
-- Gives the quasi inverse from an equivalence.
module Equivalence (e : A B) where
compose : {c : Level} {C : Set c} (B C) A C
compose e' = fromIsomorphism _ _ (composeIso (toIsomorphism _ _ e) (toIsomorphism _ _ e'))
symmetry : B A
symmetry = fromIsomorphism _ _ (symmetryIso (toIsomorphism _ _ e))
preorder≅ : ( : Level) Preorder _ _ _
preorder≅ = record
{ Carrier = Set ; _≈_ = _≡_ ; __ = _≅_
; isPreorder = record
{ isEquivalence = equalityIsEquivalence
; reflexive = λ p
coe p
, coe (sym p)
, funExt (λ x inv-coe p)
, funExt (λ x inv-coe' p)
; trans = composeIso
}
}
where
module _ { : Level} {A B : Set } {a : A} where
inv-coe : (p : A B) coe (sym p) (coe p a) a
inv-coe p =
let
D : (y : Set ) _ y Set _
D _ q = coe (sym q) (coe q a) a
d : D A refl
d = begin
coe (sym refl) (coe refl a) ≡⟨⟩
coe refl (coe refl a) ≡⟨ id-coe
coe refl a ≡⟨ id-coe
a
in pathJ D d B p
inv-coe' : (p : B A) coe p (coe (sym p) a) a
inv-coe' p =
let
D : (y : Set ) _ y Set _
D _ q = coe (sym q) (coe q a) a
k : coe p (coe (sym p) a) a
k = pathJ D (trans id-coe id-coe) B (sym p)
in k
setoid≅ : ( : Level) Setoid _ _
setoid≅ = record
{ Carrier = Set
; _≈_ = _≅_
; isEquivalence = record
{ refl = idFun _ , idFun _ , (funExt λ _ refl) , (funExt λ _ refl)
; sym = symmetryIso
; trans = composeIso
}
}
setoid≃ : ( : Level) Setoid _ _
setoid≃ = record
{ Carrier = Set
; _≈_ = _≃_
; isEquivalence = record
{ refl = idEquiv
; sym = Equivalence.symmetry
; trans = λ x x₁ Equivalence.compose x x₁
}
}
-- If the second component of a pair is propositional, then equality of such
-- pairs is equivalent to equality of their first components.
module _ {a b : Level} {A : Set a} {P : A Set b} where
equivSigProp : ((x : A) isProp (P x)) {p q : Σ A P}
(p q) (fst p fst q)
equivSigProp pA {p} {q} = fromIsomorphism _ _ iso
where
f : {p q} p q fst p fst q
f = cong fst
g : {p q} fst p fst q p q
g = lemSig pA _ _
ve-re : (e : p q) (g f) e e
ve-re = pathJ (\ q (e : p q) (g f) e e)
(\ i j p .fst , propSet (pA (p .fst)) (p .snd) (p .snd) (λ i (g {p} {p} f) (λ i₁ p) i .snd) (λ i p .snd) i j ) q
re-ve : (e : fst p fst q) (f {p} {q} g {p} {q}) e e
re-ve e = refl
inv : AreInverses (f {p} {q}) (g {p} {q})
inv = funExt ve-re , funExt re-ve
iso : (p q) (fst p fst q)
iso = f , g , inv
module _ { : Level} {A B : Set } where
isoToPath : (A B) (A B)
isoToPath = ua fromIsomorphism _ _
univalence : (A B) (A B)
univalence = Equivalence.compose u' aux
where
module _ {a b : Level} {A : Set a} {B : Set b} where
deEta : A B A U.≃ B
deEta (a , b) = U.con a b
doEta : A U.≃ B A B
doEta (U.con eqv isEqv) = eqv , isEqv
u : (A B) U.≃ (A U.≃ B)
u = U.univalence
u' : (A B) (A U.≃ B)
u' = doEta u
aux : (A U.≃ B) (A B)
aux = fromIsomorphism _ _ (doEta , deEta , funExt (λ{ (U.con _ _) refl}) , refl)
-- Equivalence is equivalent to isomorphism when the equivalence (resp.
-- isomorphism) acts on sets.
module _ (sA : isSet A) (sB : isSet B) where
equiv≃iso : (f : A B) isEquiv A B f Isomorphism f
equiv≃iso f =
let
obv : isEquiv A B f Isomorphism f
obv = toIso A B
inv : Isomorphism f isEquiv A B f
inv = fromIso A B
re-ve : (x : isEquiv A B f) (inv obv) x x
re-ve = inverse-from-to-iso A B
ve-re : (x : Isomorphism f) (obv inv) x x
ve-re = inverse-to-from-iso A B sA sB
iso : isEquiv A B f Isomorphism f
iso = obv , inv , funExt re-ve , funExt ve-re
in fromIsomorphism _ _ iso
-- A few results that I have not generalized to work with both the eta and no-eta variable of ≃
module _ {a b : Level} {A : Set a} {P : A Set b} where
-- Equality on sigma's whose second component is a proposition is equivalent
-- to equality on their first components.
equivPropSig : ((x : A) isProp (P x)) (p q : Σ A P)
(p q) (fst p fst q)
equivPropSig pA p q = fromIsomorphism _ _ iso
where
f : {p q} p q fst p fst q
f = cong fst
g : {p q} fst p fst q p q
g {p} {q} = lemSig pA p q
ve-re : (e : p q) (g f) e e
ve-re = pathJ (\ q (e : p q) (g f) e e)
(\ i j p .fst , propSet (pA (p .fst)) (p .snd) (p .snd) (λ i (g {p} {p} f) (λ i₁ p) i .snd) (λ i p .snd) i j ) q
re-ve : (e : fst p fst q) (f {p} {q} g {p} {q}) e e
re-ve e = refl
inv : AreInverses (f {p} {q}) (g {p} {q})
inv = funExt ve-re , funExt re-ve
iso : (p q) (fst p fst q)
iso = f , g , inv
-- Sigma that are equivalent on all points in the second projection are
-- equivalent.
equivSigSnd : {c} {Q : A Set (c b)}
((a : A) P a Q a) Σ A P Σ A Q
equivSigSnd {Q = Q} eA = res
where
f : Σ A P Σ A Q
f (a , pA) = a , fst (eA a) pA
g : Σ A Q Σ A P
g (a , qA) = a , g' qA
where
k : Isomorphism _
k = toIso _ _ (snd (eA a))
open Σ k renaming (fst to g')
ve-re : (x : Σ A P) (g f) x x
ve-re x i = fst x , eq i
where
eq : snd ((g f) x) snd x
eq = begin
snd ((g f) x) ≡⟨⟩
snd (g (f (a , pA))) ≡⟨⟩
g' (fst (eA a) pA) ≡⟨ lem
pA
where
open Σ x renaming (fst to a ; snd to pA)
k : Isomorphism _
k = toIso _ _ (snd (eA a))
open Σ k renaming (fst to g' ; snd to inv)
lem : (g' (fst (eA a))) pA pA
lem i = fst inv i pA
re-ve : (x : Σ A Q) (f g) x x
re-ve x i = fst x , eq i
where
open Σ x renaming (fst to a ; snd to qA)
eq = begin
snd ((f g) x) ≡⟨⟩
fst (eA a) (g' qA) ≡⟨ (λ i snd inv i qA)
qA
where
k : Isomorphism _
k = toIso _ _ (snd (eA a))
open Σ k renaming (fst to g' ; snd to inv)
inv : AreInverses f g
inv = funExt ve-re , funExt re-ve
iso : Σ A P Σ A Q
iso = f , g , inv
res : Σ A P Σ A Q
res = fromIsomorphism _ _ iso
module _ {a b : Level} {A : Set a} {B : Set b} where
open import Cubical.PathPrelude renaming (_≃_ to _≃η_)
open import Cubical.Univalence using (_≃_)
-- Equivalence is equivalent to isomorphism when the domain and codomain of
-- the equivalence is a set.
equivSetIso : isSet A isSet B (f : A B)
isEquiv A B f Isomorphism f
equivSetIso sA sB f =
let
obv : isEquiv A B f Isomorphism f
obv = toIso A B
inv : Isomorphism f isEquiv A B f
inv = fromIso A B
re-ve : (x : isEquiv A B f) (inv obv) x x
re-ve = inverse-from-to-iso A B
ve-re : (x : Isomorphism f) (obv inv) x x
ve-re = inverse-to-from-iso A B sA sB
iso : isEquiv A B f Isomorphism f
iso = obv , inv , funExt re-ve , funExt ve-re
in fromIsomorphism _ _ iso
doEta : A B A ≃η B
doEta (_≃_.con eqv isEqv) = eqv , isEqv
deEta : A ≃η B A B
deEta (eqv , isEqv) = _≃_.con eqv isEqv
module NoEta {a b : Level} {A : Set a} {B : Set b} where
open import Cubical.PathPrelude renaming (_≃_ to _≃η_)
open import Cubical.Univalence using (_≃_)
module Equivalence (e : A B) where
open Equivalence (doEta e) hiding
( toIsomorphism ; fromIsomorphism ; _~_
; compose ; symmetryIso ; symmetry ) public
compose : {c : Level} {C : Set c} (B C) A C
compose ee = deEta (Equivalence.compose (doEta e) (doEta ee))
symmetry : B A
symmetry = deEta (Equivalence.symmetry (doEta e))
-- fromIso : {f : A → B} → Isomorphism f → isEquiv f
-- fromIso = ?
-- toIso : {f : A → B} → isEquiv f → Isomorphism f
-- toIso = ?
fromIsomorphism : A B A B
fromIsomorphism (f , iso) = _≃_.con f (Equiv≃.fromIso _ _ iso)
toIsomorphism : A B A B
toIsomorphism (_≃_.con f eqv) = f , Equiv≃.toIso _ _ eqv
module _ {a b : Level} {A : Set a} {P : A Set b} where
-- Equivalence of pairs whose first components are identitical can be obtained
-- from an equivalence of their seecond components.
equivSig : {c : Level} {Q : A Set c}
((a : A) P a Q a) Σ A P Σ A Q
equivSig {Q = Q} eA = res
where
P≅Q : {a} P a Q a
P≅Q {a} = toIsomorphism _ _ (eA a)
f : Σ A P Σ A Q
f (a , pA) = a , fst P≅Q pA
g : Σ A Q Σ A P
g (a , qA) = a , fst (snd P≅Q) qA
ve-re : (x : Σ A P) (g f) x x
ve-re (a , pA) i = a , eq i
where
eq : snd ((g f) (a , pA)) pA
eq = begin
snd ((g f) (a , pA)) ≡⟨⟩
snd (g (f (a , pA))) ≡⟨⟩
g' (fst (eA a) pA) ≡⟨ lem
pA
where
open Σ (snd P≅Q) renaming (fst to g' ; snd to inv)
-- anti-funExt
lem : (g' (fst (eA a))) pA pA
lem = cong (_$ pA) (fst (snd (snd P≅Q)))
re-ve : (x : Σ A Q) (f g) x x
re-ve x i = fst x , eq i
where
open Σ x renaming (fst to a ; snd to qA)
eq = begin
snd ((f g) x) ≡⟨⟩
fst (eA a) (g' qA) ≡⟨ (λ i snd inv i qA)
qA
where
k : Isomorphism _
k = toIso _ _ (snd (eA a))
open Σ k renaming (fst to g' ; snd to inv)
inv : AreInverses f g
inv = funExt ve-re , funExt re-ve
iso : Σ A P Σ A Q
iso = f , g , inv
res : Σ A P Σ A Q
res = fromIsomorphism _ _ iso

View file

@ -3,12 +3,16 @@ module Cat.Prelude where
open import Agda.Primitive public
-- FIXME Use:
-- open import Agda.Builtin.Sigma public
open import Agda.Builtin.Sigma public
-- Rather than
open import Data.Product public
renaming (∃! to ∃!≈)
using (_×_ ; Σ-syntax ; swap)
-- TODO Import Data.Function under appropriate names.
open import Function using (_∘_ ; _∘_ ; _$_ ; case_of_ ; flip) public
idFun : {a} (A : Set a) A A
idFun A a = a
open import Cubical public
-- FIXME rename `gradLemma` to `fromIsomorphism` - perhaps just use wrapper
@ -17,18 +21,19 @@ open import Cubical.GradLemma
using (gradLemma)
public
open import Cubical.NType
using (⟨-2⟩ ; ⟨-1⟩ ; ⟨0⟩ ; TLevel ; HasLevel)
using (⟨-2⟩ ; ⟨-1⟩ ; ⟨0⟩ ; TLevel ; HasLevel ; isGrpd)
public
open import Cubical.NType.Properties
using
( lemPropF ; lemSig ; lemSigP ; isSetIsProp
; propPi ; propHasLevel ; setPi ; propSet)
; propPi ; propPiImpl ; propHasLevel ; setPi ; propSet
; propSig ; equivPreservesNType)
public
propIsContr : { : Level} {A : Set } isProp (isContr A)
propIsContr = propHasLevel ⟨-2⟩
open import Cubical.Sigma using (setSig ; sigPresSet) public
open import Cubical.Sigma using (setSig ; sigPresSet ; sigPresNType) public
module _ ( : Level) where
-- FIXME Ask if we can push upstream.
@ -46,20 +51,57 @@ module _ ( : Level) where
-- * Utilities --
-----------------
-- | Unique existensials.
-- | Unique existentials.
∃! : {a b} {A : Set a}
(A Set b) Set (a b)
∃! = ∃!≈ _≡_
∃!-syntax : {a b} {A : Set a} (A Set b) Set (a b)
∃!-syntax =
∃!-syntax = !
syntax ∃!-syntax (λ x B) = ∃![ x ] B
module _ {a b} {A : Set a} {P : A Set b} (f g : ∃! P) where
∃-unique : fst f fst g
∃-unique = (snd (snd f)) (fst (snd g))
module _ {a b : Level} {A : Set a} {B : A Set b} {a b : Σ A B}
(proj₁≡ : (λ _ A) [ proj₁ a proj₁ b ])
(proj₂≡ : (λ i B (proj₁≡ i)) [ proj₂ a proj₂ b ]) where
(fst : (λ _ A) [ fst a fst b ])
(snd : (λ i B (fst≡ i)) [ snd a snd b ]) where
Σ≡ : a b
proj₁ (Σ≡ i) = proj₁≡ i
proj₂ (Σ≡ i) = proj₂≡ i
fst (Σ≡ i) = fst≡ i
snd (Σ≡ i) = snd≡ i
import Relation.Binary
open Relation.Binary public using
( Preorder ; Transitive ; IsEquivalence ; Rel
; Setoid )
equalityIsEquivalence : { : Level} {A : Set } IsEquivalence {A = A} _≡_
IsEquivalence.refl equalityIsEquivalence = refl
IsEquivalence.sym equalityIsEquivalence = sym
IsEquivalence.trans equalityIsEquivalence = trans
IsPreorder
: {a : Level} {A : Set a}
(__ : Rel A ) -- The relation.
Set _
IsPreorder _~_ = Relation.Binary.IsPreorder _≡_ _~_
module _ { : Level} {A : Set } {a : A} where
-- FIXME rename to `coe-neutral`
id-coe : coe refl a a
id-coe = begin
coe refl a ≡⟨⟩
pathJ (λ y x A) _ A refl ≡⟨ pathJprop {x = a} (λ y x A) _
_ ≡⟨ pathJprop {x = a} (λ y x A) _
a
module _ { : Level} {A : Set } where
open import Cubical.NType
open import Data.Nat using (_≤_ ; ≤′-refl ; ≤′-step ; zero ; suc)
open import Cubical.NType.Properties
ntypeCumulative : {n m} n ≤′ m HasLevel n ⟩₋₂ A HasLevel m ⟩₋₂ A
ntypeCumulative {m} ≤′-refl lvl = lvl
ntypeCumulative {n} {suc m} (≤′-step le) lvl = HasLevel+1 m ⟩₋₂ (ntypeCumulative le lvl)

View file

@ -1,41 +0,0 @@
{-# OPTIONS --allow-unsolved-metas #-}
module Cat.Wishlist where
open import Level hiding (suc)
open import Cubical
open import Cubical.NType
open import Data.Nat using (_≤_ ; z≤n ; s≤s ; zero ; suc)
open import Agda.Builtin.Sigma
open import Cubical.NType.Properties
step : {} {A : Set } isContr A (x y : A) isContr (x y)
step (a , contr) x y = {!p , c!}
-- where
-- p : x ≡ y
-- p = begin
-- x ≡⟨ sym (contr x) ⟩
-- a ≡⟨ contr y ⟩
-- y ∎
-- c : (q : x ≡ y) → p ≡ q
-- c q i j = contr (p {!!}) {!!}
-- Contractible types have any given homotopy level.
contrInitial : { : Level} {A : Set } n isContr A HasLevel n A
contrInitial ⟨-2⟩ contr = contr
-- lem' (S ⟨-2⟩) (a , contr) = {!step!}
contrInitial (S ⟨-2⟩) (a , contr) x y = begin
x ≡⟨ sym (contr x)
a ≡⟨ contr y
y
contrInitial (S (S n)) contr x y = {!lvl!} -- Why is this not well-founded?
where
c : isContr (x y)
c = step contr x y
lvl : HasLevel (S n) (x y)
lvl = contrInitial {A = x y} (S n) c
module _ { : Level} {A : Set } where
ntypeCommulative : {n m} n m HasLevel n ⟩₋₂ A HasLevel m ⟩₋₂ A
ntypeCommulative {n = zero} {m} z≤n lvl = {!contrInitial ⟨ m ⟩₋₂ lvl!}
ntypeCommulative {n = .(suc _)} {.(suc _)} (s≤s x) lvl = {!!}