Merge branch 'dev'

proposal/.gitignore

@@ -0,0 +1,8 @@
+*.aux
+*.fdb_latexmk
+*.fls
+*.log
+*.out
+*.pdf
+*.bbl
+*.blg

proposal/chalmerstitle.sty

@@ -0,0 +1,56 @@
+% 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}
+}

proposal/macros.tex

@@ -0,0 +1,19 @@
+\newcommand{\coloneqq}{\mathrel{\vcenter{\baselineskip0.5ex \lineskiplimit0pt
+                     \hbox{\scriptsize.}\hbox{\scriptsize.}}}%
+                     =}
+
+\newcommand{\defeq}{\coloneqq}
+\newcommand{\bN}{\mathbb{N}}
+\newcommand{\bC}{\mathbb{C}}
+\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}}

proposal/proposal.tex

@@ -0,0 +1,282 @@
+\documentclass{article}
+
+
+
+\usepackage[utf8]{inputenc}
+
+\usepackage{natbib}
+\usepackage[hidelinks]{hyperref}
+
+\usepackage{graphicx}
+
+\usepackage{parskip}
+\usepackage{multicol}
+\usepackage{amsmath,amssymb}
+% \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}
+\end{document}

proposal/refs.bib

@@ -0,0 +1,114 @@
+@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}
+}
+@misc{cubical-agda,
+  author = {Andrea Vezzosi},
+  title = {Cubical Extension to Agda},
+  year = {2017},
+  publisher = {GitHub},
+  journal = {GitHub repository},
+  howpublished = {\url{https://github.com/agda/agda}},
+  commit = {92de32c0669cb414f329fff25497a9ddcd58b951}
+}
+@misc{agda,
+  author = {Ulf Norell},
+  title = {Agda},
+  year = {2017},
+  publisher = {GitHub},
+  journal = {GitHub repository},
+  howpublished = {\url{https://github.com/agda/agda}},
+  commit = {92de32c0669cb414f329fff25497a9ddcd58b951}
+}
+@inproceedings{bezem-2014,
+  title={A model of type theory in cubical sets},
+  author={Bezem, Marc and Coquand, Thierry and Huber, Simon},
+  booktitle={19th International Conference on Types for Proofs and Programs (TYPES 2013)},
+  volume={26},
+  pages={107--128},
+  year={2014}
+}
+@article{coquand-2013,
+  title={Isomorphism is equality},
+  author={Coquand, Thierry and Danielsson, Nils Anders},
+  journal={Indagationes Mathematicae},
+  volume={24},
+  number={4},
+  pages={1105--1120},
+  year={2013},
+  publisher={Elsevier}
+}
+@inproceedings{dybjer-1995,
+  title={Internal type theory},
+  author={Dybjer, Peter},
+  booktitle={International Workshop on Types for Proofs and Programs},
+  pages={120--134},
+  year={1995},
+  organization={Springer}
+}
+@inproceedings{voevodsky-2011,
+  title={Univalent foundations of mathematics},
+  author={Voevodsky, Vladimir},
+  booktitle={International Workshop on Logic, Language, Information, and Computation},
+  pages={4--4},
+  year={2011},
+  organization={Springer}
+}
+@article{huber-2016,
+  title={Cubical Intepretations of Type Theory},
+  author={Huber, Simon},
+  year={2016}
+}
+@article{hofmann-1995,
+  title={Extensional concepts in intensional type theory},
+  author={Hofmann, Martin},
+  year={1995},
+  publisher={University of Edinburgh. College of Science and Engineering. School of Informatics.}
+}
+@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}
+}

src/Cat/Categories/Cat.agda

@@ -0,0 +1,55 @@
+{-# OPTIONS --cubical #-}
+
+module Category.Categories.Cat where
+
+open import Agda.Primitive
+open import Cubical
+open import Function
+open import Data.Product renaming (proj₁ to fst ; proj₂ to snd)
+
+open import Category
+
+-- The category of categories
+module _ {ℓ ℓ' : Level} where
+  private
+    _⊛_ = functor-comp
+    module _ {A B C D : Category {ℓ} {ℓ'}} {f : Functor A B} {g : Functor B C} {h : Functor C D} where
+      assc : h ⊛ (g ⊛ f) ≡ (h ⊛ g) ⊛ f
+      assc = {!!}
+
+    module _ {A B : Category {ℓ} {ℓ'}} where
+      lift-eq : (f g : Functor A B)
+        → (eq* : Functor.func* f ≡ Functor.func* g)
+        -- TODO: Must transport here using the equality from above.
+        -- Reason:
+        --   func→  : Arrow A dom cod → Arrow B (func* dom) (func* cod)
+        --   func→₁ : Arrow A dom cod → Arrow B (func*₁ dom) (func*₁ cod)
+        -- In other words, func→ and func→₁ does not have the same type.
+  --      → Functor.func→ f ≡ Functor.func→ g
+  --      → Functor.ident f ≡ Functor.ident g
+  --       → Functor.distrib f ≡ Functor.distrib g
+        → f ≡ g
+      lift-eq
+        (functor func* func→ idnt distrib)
+        (functor func*₁ func→₁ idnt₁ distrib₁)
+        eq-func* = {!!}
+
+    module _ {A B : Category {ℓ} {ℓ'}} {f : Functor A B} where
+      idHere = identity {ℓ} {ℓ'} {A}
+      lem : (Functor.func* f) ∘ (Functor.func* idHere) ≡ Functor.func* f
+      lem = refl
+      ident-r : f ⊛ identity ≡ f
+      ident-r = lift-eq (f ⊛ identity) f refl
+      ident-l : identity ⊛ f ≡ f
+      ident-l = {!!}
+
+  CatCat : Category {lsuc (ℓ ⊔ ℓ')} {ℓ ⊔ ℓ'}
+  CatCat =
+    record
+      { Object = Category {ℓ} {ℓ'}
+      ; Arrow = Functor
+      ; 𝟙 = identity
+      ; _⊕_ = functor-comp
+      ; assoc = {!!}
+      ; ident = ident-r , ident-l
+      }

src/Cat/Categories/Rel.agda

@@ -1,11 +1,14 @@
 {-# OPTIONS --cubical #-}
-module Category.Rel where
+module Cat.Categories.Rel where
 
-open import Data.Product
 open import Cubical.PathPrelude
 open import Cubical.GradLemma
 open import Agda.Primitive
-open import Category
+open import Data.Product renaming (proj₁ to fst ; proj₂ to snd)
+open import Function
+import Cubical.FromStdLib
+
+open import Cat.Category
 
 -- Subsets are predicates over some type.
 Subset : {ℓ : Level} → ( A : Set ℓ ) → Set (ℓ ⊔ lsuc lzero)
@@ -72,7 +75,7 @@ module _ {A B : Set} {S : Subset (A × B)} (ab : A × B) where
 
       equi : (Σ[ a' ∈ A ] (a , a') ∈ Diag A × (a' , b) ∈ S)
         ≃ (a , b) ∈ S
-      equi = backwards , isequiv
+      equi = backwards Cubical.FromStdLib., isequiv
 
     ident-l : (Σ[ a' ∈ A ] (a , a') ∈ Diag A × (a' , b) ∈ S)
       ≡ (a , b) ∈ S
@@ -106,7 +109,7 @@ module _ {A B : Set} {S : Subset (A × B)} (ab : A × B) where
 
       equi : (Σ[ b' ∈ B ] (a , b') ∈ S × (b' , b) ∈ Diag B)
         ≃ ab ∈ S
-      equi = backwards , isequiv
+      equi = backwards Cubical.FromStdLib., isequiv
 
     ident-r : (Σ[ b' ∈ B ] (a , b') ∈ S × (b' , b) ∈ Diag B)
       ≡ ab ∈ S
@@ -144,7 +147,7 @@ module _ {A B C D : Set} {S : Subset (A × B)} {R : Subset (B × C)} {Q : Subset
 
     equi : (Σ[ c ∈ C ] (Σ[ b ∈ B ] (a , b) ∈ S × (b , c) ∈ R) × (c , d) ∈ Q)
       ≃ (Σ[ b ∈ B ] (a , b) ∈ S × (Σ[ c ∈ C ] (b , c) ∈ R × (c , d) ∈ Q))
-    equi = fwd , isequiv
+    equi = fwd Cubical.FromStdLib., isequiv
 
     -- assocc : Q + (R + S) ≡ (Q + R) + S
   is-assoc : (Σ[ c ∈ C ] (Σ[ b ∈ B ] (a , b) ∈ S × (b , c) ∈ R) × (c , d) ∈ Q)

src/Cat/Categories/Sets.agda

@@ -0,0 +1,52 @@
+{-# OPTIONS --allow-unsolved-metas #-}
+
+module Cat.Categories.Sets where
+
+open import Cubical.PathPrelude
+open import Agda.Primitive
+open import Data.Product
+open import Data.Product renaming (proj₁ to fst ; proj₂ to snd)
+
+open import Cat.Category
+open import Cat.Functor
+
+-- Sets are built-in to Agda. The set of all small sets is called Set.
+
+Fun : {ℓ : Level} → ( T U : Set ℓ ) → Set ℓ
+Fun T U = T → U
+
+Sets : {ℓ : Level} → Category {lsuc ℓ} {ℓ}
+Sets {ℓ} = record
+  { Object = Set ℓ
+  ; Arrow = λ T U → Fun {ℓ} T U
+  ; 𝟙 = λ x → x
+  ; _⊕_  = λ g f x → g ( f x )
+  ; assoc = refl
+  ; ident = funExt (λ x → refl) , funExt (λ x → refl)
+  }
+
+Representable : {ℓ ℓ' : Level} → (ℂ : Category {ℓ} {ℓ'}) → Set (ℓ ⊔ lsuc ℓ')
+Representable {ℓ' = ℓ'} ℂ = Functor ℂ (Sets {ℓ'})
+
+representable : {ℓ ℓ' : Level} → {ℂ : Category {ℓ} {ℓ'}} → Category.Object ℂ → Representable ℂ
+representable {ℂ = ℂ} A = record
+  { func* = λ B → ℂ.Arrow A B
+  ; func→ = λ f g → f ℂ.⊕ g
+  ; ident = funExt λ _ → snd ℂ.ident
+  ; distrib = funExt λ x → sym ℂ.assoc
+  }
+  where
+    open module ℂ = Category ℂ
+
+Presheaf : {ℓ ℓ' : Level} → (ℂ : Category {ℓ} {ℓ'}) → Set (ℓ ⊔ lsuc ℓ')
+Presheaf {ℓ' = ℓ'} ℂ = Functor (Opposite ℂ) (Sets {ℓ'})
+
+presheaf : {ℓ ℓ' : Level} → {ℂ : Category {ℓ} {ℓ'}} → Category.Object (Opposite ℂ) → Presheaf ℂ
+presheaf {ℂ = ℂ} B = record
+  { func* = λ A → ℂ.Arrow A B
+  ; func→ = λ f g → g ℂ.⊕ f
+  ; ident = funExt λ x → fst ℂ.ident
+  ; distrib = funExt λ x → ℂ.assoc
+  }
+  where
+    open module ℂ = Category ℂ

src/Cat/Category.agda

@@ -1,16 +1,18 @@
 {-# OPTIONS --cubical #-}
 
-module Category where
+module Cat.Category where
 
 open import Agda.Primitive
 open import Data.Unit.Base
-open import Data.Product
+open import Data.Product renaming (proj₁ to fst ; proj₂ to snd)
-open import Cubical.PathPrelude
 open import Data.Empty
+open import Function
+open import Cubical
 
 postulate undefined : {ℓ : Level} → {A : Set ℓ} → A
 
 record Category {ℓ ℓ'} : Set (lsuc (ℓ' ⊔ ℓ)) where
+  constructor category
   field
     Object : Set ℓ
     Arrow  : Object → Object → Set ℓ'
@@ -21,52 +23,13 @@ record Category {ℓ ℓ'} : Set (lsuc (ℓ' ⊔ ℓ)) where
     ident  : { A B : Object } { f : Arrow A B }
       → f ⊕ 𝟙 ≡ f × 𝟙 ⊕ f ≡ f
   infixl 45 _⊕_
-  dom : { a b : Object } → Arrow a b → Object
+  domain : { a b : Object } → Arrow a b → Object
-  dom {a = a} _ = a
+  domain {a = a} _ = a
-  cod : { a b : Object } → Arrow a b → Object
+  codomain : { a b : Object } → Arrow a b → Object
-  cod {b = b} _ = b
+  codomain {b = b} _ = b
 
 open Category public
 
-record Functor {ℓc ℓc' ℓd ℓd'} (C : Category {ℓc} {ℓc'}) (D : Category {ℓd} {ℓd'})
-  : Set (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') where
-  private
-    open module C = Category C
-    open module D = Category D
-  field
-    F : C.Object → D.Object
-    f : {c c' : C.Object} → C.Arrow c c' → D.Arrow (F c) (F c')
-    ident   : { c : C.Object } → f (C.𝟙 {c}) ≡ D.𝟙 {F c}
-    -- TODO: Avoid use of ugly explicit arguments somehow.
-    -- This guy managed to do it:
-    --    https://github.com/copumpkin/categories/blob/master/Categories/Functor/Core.agda
-    distrib : { c c' c'' : C.Object} {a : C.Arrow c c'} {a' : C.Arrow c' c''}
-      → f (a' C.⊕ a) ≡ f a' D.⊕ f a
-
-FunctorComp : ∀ {ℓ ℓ'} {a b c : Category {ℓ} {ℓ'}} → Functor b c → Functor a b → Functor a c
-FunctorComp {a = a} {b = b} {c = c} F G =
-  record
-    { F = F.F ∘ G.F
-    ; f = F.f ∘ G.f
-    ; ident = λ { {c = obj} →
-      let --t : (F.f ∘ G.f) (𝟙 a) ≡ (𝟙 c)
-          g-ident = G.ident
-          k : F.f (G.f {c' = obj} (𝟙 a)) ≡ F.f (G.f (𝟙 a))
-          k = refl {x = F.f (G.f (𝟙 a))}
-          t : F.f (G.f (𝟙 a)) ≡ (𝟙 c)
-          -- t = subst F.ident (subst G.ident k)
-          t = undefined
-      in t }
-    ; distrib = undefined -- subst F.distrib (subst G.distrib refl)
-    }
-    where
-      open module F = Functor F
-      open module G = Functor G
-
--- The identity functor
-Identity : {ℓ ℓ' : Level} → {C : Category {ℓ} {ℓ'}} → Functor C C
-Identity = record { F = λ x → x ; f = λ x → x ; ident = refl ; distrib = refl }
-
 module _ {ℓ ℓ' : Level} {ℂ : Category {ℓ} {ℓ'}} { A B : Object ℂ } where
   private
     open module ℂ = Category ℂ
@@ -116,9 +79,6 @@ module _ {ℓ ℓ' : Level} {ℂ : Category {ℓ} {ℓ'}} { A B : Object ℂ } w
   iso-is-epi-mono : ∀ {X} (f : ℂ.Arrow A B ) → Isomorphism f → Epimorphism {X = X} f × Monomorphism {X = X} f
   iso-is-epi-mono f iso = iso-is-epi f iso , iso-is-mono f iso
 
-¬_ : {ℓ : Level} → Set ℓ → Set ℓ
-¬ A = A → ⊥
-
 {-
 epi-mono-is-not-iso : ∀ {ℓ ℓ'} → ¬ ((ℂ : Category {ℓ} {ℓ'}) {A B X : Object ℂ} (f : Arrow ℂ A B ) → Epimorphism {ℂ = ℂ} {X = X} f → Monomorphism {ℂ = ℂ} {X = X} f → Isomorphism {ℂ = ℂ} f)
 epi-mono-is-not-iso f =
@@ -126,6 +86,7 @@ epi-mono-is-not-iso f =
   in {!!}
 -}
 
+-- Isomorphism of objects
 _≅_ : { ℓ ℓ' : Level } → { ℂ : Category {ℓ} {ℓ'} } → ( A B : Object ℂ ) → Set ℓ'
 _≅_ {ℂ = ℂ} A B = Σ[ f ∈ ℂ.Arrow A B ] (Isomorphism {ℂ = ℂ} f)
   where
@@ -167,22 +128,8 @@ Opposite ℂ =
   where
     open module ℂ = Category ℂ
 
-CatCat : {ℓ ℓ' : Level} → Category {ℓ-suc (ℓ ⊔ ℓ')} {ℓ ⊔ ℓ'}
+Hom : {ℓ ℓ' : Level} → (ℂ : Category {ℓ} {ℓ'}) → (A B : Object ℂ) → Set ℓ'
-CatCat {ℓ} {ℓ'} =
+Hom ℂ A B = Arrow ℂ A B
-  record
-    { Object = Category {ℓ} {ℓ'}
-    ; Arrow = Functor
-    ; 𝟙 = Identity
-    ; _⊕_ = FunctorComp
-    ; assoc = undefined
-    ; ident = λ { {f = f} →
-      let eq : f ≡ f
-          eq = refl
-      in undefined , undefined}
-    }
-
-Hom : {ℓ ℓ' : Level} → {ℂ : Category {ℓ} {ℓ'}} → (A B : Object ℂ) → Set ℓ'
-Hom {ℂ = ℂ} A B = Arrow ℂ A B
 
 module _ {ℓ ℓ' : Level} {ℂ : Category {ℓ} {ℓ'}} where
   private
@@ -191,5 +138,5 @@ module _ {ℓ ℓ' : Level} {ℂ : Category {ℓ} {ℓ'}} where
     _+_ = _⊕_ ℂ
 
   HomFromArrow : (A : Obj) → {B B' : Obj} → (g : Arr B B')
-    → Hom {ℂ = ℂ} A B → Hom {ℂ = ℂ} A B'
+    → Hom ℂ A B → Hom ℂ A B'
   HomFromArrow _A g = λ f → g + f

src/Cat/Category/Properties.agda

@@ -0,0 +1,23 @@
+{-# OPTIONS --allow-unsolved-metas #-}
+
+module Cat.Category.Properties where
+
+open import Cat.Category
+open import Cat.Functor
+open import Cat.Categories.Sets
+
+module _ {ℓa ℓa' ℓb ℓb'} where
+  Exponential : Category {ℓa} {ℓa'} → Category {ℓb} {ℓb'} → Category {{!!}} {{!!}}
+  Exponential A B = record
+    { Object = {!!}
+    ; Arrow = {!!}
+    ; 𝟙 = {!!}
+    ; _⊕_ = {!!}
+    ; assoc = {!!}
+    ; ident = {!!}
+    }
+
+_⇑_ = Exponential
+
+yoneda : ∀ {ℓ ℓ'} → {ℂ : Category {ℓ} {ℓ'}} → Functor ℂ (Sets ⇑ (Opposite ℂ))
+yoneda = {!!}

src/Cat/Cubical.agda

@@ -0,0 +1,48 @@
+module Cat.Cubical where
+
+open import Agda.Primitive
+open import Data.Bool
+open import Data.Product
+open import Data.Sum
+open import Data.Unit
+open import Data.Empty
+
+open import Cat.Category
+
+module _ {ℓ ℓ' : Level} (Ns : Set ℓ) where
+  -- Σ is the "namespace"
+  ℓo = (lsuc lzero ⊔ ℓ)
+
+  FiniteDecidableSubset : Set ℓ
+  FiniteDecidableSubset = Ns → Bool
+
+  isTrue : Bool → Set
+  isTrue false = ⊥
+  isTrue true = ⊤
+
+  elmsof : (Ns → Bool) → Set ℓ
+  elmsof P = (σ : Ns) → isTrue (P σ)
+
+  𝟚 : Set
+  𝟚 = Bool
+
+  module _ (I J : FiniteDecidableSubset) where
+    private
+      themap : Set {!!}
+      themap = elmsof I → elmsof J ⊎ 𝟚
+      rules : (elmsof I → elmsof J ⊎ 𝟚) → Set
+      rules f = (i j : elmsof I) → {!!}
+
+    Mor = Σ themap rules
+
+  -- The category of names and substitutions
+  ℂ : Category -- {ℓo} {lsuc lzero ⊔ ℓo}
+  ℂ = record
+    -- { Object = FiniteDecidableSubset
+    { Object = Ns → Bool
+    ; Arrow = Mor
+    ; 𝟙 = {!!}
+    ; _⊕_ = {!!}
+    ; assoc = {!!}
+    ; ident = {!!}
+    }

src/Cat/Functor.agda

@@ -0,0 +1,66 @@
+module Cat.Functor where
+
+open import Agda.Primitive
+open import Cubical
+open import Function
+
+open import Cat.Category
+
+record Functor {ℓc ℓc' ℓd ℓd'} (C : Category {ℓc} {ℓc'}) (D : Category {ℓd} {ℓd'})
+  : Set (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') where
+  private
+    open module C = Category C
+    open module D = Category D
+  field
+    func* : C.Object → D.Object
+    func→ : {dom cod : C.Object} → C.Arrow dom cod → D.Arrow (func* dom) (func* cod)
+    ident   : { c : C.Object } → func→ (C.𝟙 {c}) ≡ D.𝟙 {func* c}
+    -- TODO: Avoid use of ugly explicit arguments somehow.
+    -- This guy managed to do it:
+    --    https://github.com/copumpkin/categories/blob/master/Categories/Functor/Core.agda
+    distrib : { c c' c'' : C.Object} {a : C.Arrow c c'} {a' : C.Arrow c' c''}
+      → func→ (a' C.⊕ a) ≡ func→ a' D.⊕ func→ a
+
+module _ {ℓ ℓ' : Level} {A B C : Category {ℓ} {ℓ'}} (F : Functor B C) (G : Functor A B) where
+  private
+    open module F = Functor F
+    open module G = Functor G
+    open module A = Category A
+    open module B = Category B
+    open module C = Category C
+
+    F* = F.func*
+    F→ = F.func→
+    G* = G.func*
+    G→ = G.func→
+    module _ {a0 a1 a2 : A.Object} {α0 : A.Arrow a0 a1} {α1 : A.Arrow a1 a2} where
+
+      dist : (F→ ∘ G→) (α1 A.⊕ α0) ≡ (F→ ∘ G→) α1 C.⊕ (F→ ∘ G→) α0
+      dist = begin
+        (F→ ∘ G→) (α1 A.⊕ α0)         ≡⟨ refl ⟩
+        F→ (G→ (α1 A.⊕ α0))           ≡⟨ cong F→ G.distrib ⟩
+        F→ ((G→ α1) B.⊕ (G→ α0))      ≡⟨ F.distrib ⟩
+        (F→ ∘ G→) α1 C.⊕ (F→ ∘ G→) α0 ∎
+
+  functor-comp : Functor A C
+  functor-comp =
+    record
+      { func* = F* ∘ G*
+      ; func→ = F→ ∘ G→
+      ; ident = begin
+        (F→ ∘ G→) (A.𝟙) ≡⟨ refl ⟩
+        F→ (G→ (A.𝟙))   ≡⟨ cong F→ G.ident ⟩
+        F→ (B.𝟙)        ≡⟨ F.ident ⟩
+        C.𝟙             ∎
+      ; distrib = dist
+      }
+
+-- The identity functor
+identity : {ℓ ℓ' : Level} → {C : Category {ℓ} {ℓ'}} → Functor C C
+-- Identity = record { F* = λ x → x ; F→ = λ x → x ; ident = refl ; distrib = refl }
+identity = record
+  { func* = λ x → x
+  ; func→ = λ x → x
+  ; ident = refl
+  ; distrib = refl
+  }

src/Category/Sets.agda

@@ -1,34 +0,0 @@
-module Category.Sets where
-
-open import Cubical.PathPrelude
-open import Agda.Primitive
-open import Category
-
--- Sets are built-in to Agda. The set of all small sets is called Set.
-
-Fun : {ℓ : Level} → ( T U : Set ℓ ) → Set ℓ
-Fun T U = T → U
-
-Sets : {ℓ : Level} → Category {lsuc ℓ} {ℓ}
-Sets {ℓ} = record
-  { Object = Set ℓ
-  ; Arrow = λ T U → Fun {ℓ} T U
-  ; 𝟙 = λ x → x
-  ; _⊕_  = λ g f x → g ( f x )
-  ; assoc = refl
-  ; ident = funExt (λ x → refl) , funExt (λ x → refl)
-  }
-
-module _ {ℓ ℓ' : Level} {ℂ : Category {ℓ} {ℓ}} where
-  private
-    C-Obj = Object ℂ
-    _+_   = Arrow ℂ
-
-  RepFunctor : Functor ℂ Sets
-  RepFunctor =
-    record
-    { F = λ A → (B : C-Obj) → Hom {ℂ = ℂ} A B
-    ; f = λ { {c' = c'} f g → {!HomFromArrow {ℂ = } c' g!}}
-    ; ident = {!!}
-    ; distrib = {!!}
-    }