diff --git a/proposal/.gitignore b/proposal/.gitignore new file mode 100644 index 0000000..b19d31d --- /dev/null +++ b/proposal/.gitignore @@ -0,0 +1,8 @@ +*.aux +*.fdb_latexmk +*.fls +*.log +*.out +*.pdf +*.bbl +*.blg diff --git a/proposal/chalmerstitle.sty b/proposal/chalmerstitle.sty new file mode 100644 index 0000000..c2aa355 --- /dev/null +++ b/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} +} diff --git a/proposal/macros.tex b/proposal/macros.tex new file mode 100644 index 0000000..604ae8b --- /dev/null +++ b/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}} diff --git a/proposal/proposal.tex b/proposal/proposal.tex new file mode 100644 index 0000000..7237479 --- /dev/null +++ b/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} diff --git a/proposal/refs.bib b/proposal/refs.bib new file mode 100644 index 0000000..93665a7 --- /dev/null +++ b/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} +} \ No newline at end of file diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda new file mode 100644 index 0000000..79efc49 --- /dev/null +++ b/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 + } diff --git a/src/Category/Rel.agda b/src/Cat/Categories/Rel.agda similarity index 94% rename from src/Category/Rel.agda rename to src/Cat/Categories/Rel.agda index e9bbdc4..32e07f4 100644 --- a/src/Category/Rel.agda +++ b/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) diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda new file mode 100644 index 0000000..bd026dc --- /dev/null +++ b/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 ℂ diff --git a/src/Category.agda b/src/Cat/Category.agda similarity index 66% rename from src/Category.agda rename to src/Cat/Category.agda index d1aa814..a30aee4 100644 --- a/src/Category.agda +++ b/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 Cubical.PathPrelude +open import Data.Product renaming (proj₁ to fst ; proj₂ to snd) 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 - dom {a = a} _ = a - cod : { a b : Object } → Arrow a b → Object - cod {b = b} _ = b + domain : { a b : Object } → Arrow a b → Object + domain {a = a} _ = a + codomain : { a b : Object } → Arrow a b → Object + 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 (ℓ ⊔ ℓ')} {ℓ ⊔ ℓ'} -CatCat {ℓ} {ℓ'} = - 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 +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 diff --git a/src/Category/Bij.agda b/src/Cat/Category/Bij.agda similarity index 100% rename from src/Category/Bij.agda rename to src/Cat/Category/Bij.agda diff --git a/src/Category/Free.agda b/src/Cat/Category/Free.agda similarity index 100% rename from src/Category/Free.agda rename to src/Cat/Category/Free.agda diff --git a/src/Category/Pathy.agda b/src/Cat/Category/Pathy.agda similarity index 100% rename from src/Category/Pathy.agda rename to src/Cat/Category/Pathy.agda diff --git a/src/Cat/Category/Properties.agda b/src/Cat/Category/Properties.agda new file mode 100644 index 0000000..d8bd40c --- /dev/null +++ b/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 = {!!} diff --git a/src/Cat/Cubical.agda b/src/Cat/Cubical.agda new file mode 100644 index 0000000..cba1c41 --- /dev/null +++ b/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 = {!!} + } diff --git a/src/Cat/Functor.agda b/src/Cat/Functor.agda new file mode 100644 index 0000000..4daaef3 --- /dev/null +++ b/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 + } diff --git a/src/Category/Sets.agda b/src/Category/Sets.agda deleted file mode 100644 index fb2c332..0000000 --- a/src/Category/Sets.agda +++ /dev/null @@ -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 = {!!} - }