From f0412fa091ff84c3986ca5dea04bda3a79415b87 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Sun, 26 Nov 2017 14:57:19 +0100 Subject: [PATCH 01/19] Add stub for implementing the cubical type system --- src/Category/Cubical.agda | 47 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 47 insertions(+) create mode 100644 src/Category/Cubical.agda diff --git a/src/Category/Cubical.agda b/src/Category/Cubical.agda new file mode 100644 index 0000000..22709be --- /dev/null +++ b/src/Category/Cubical.agda @@ -0,0 +1,47 @@ +module Category.Cubical where + +open import Agda.Primitive +open import Category +open import Data.Bool +open import Data.Product +open import Data.Sum +open import Data.Unit +open import Data.Empty + +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 = {!!} + } From 9876dec4467bac78c56eabe707c7beb10232a4d1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Sun, 26 Nov 2017 14:59:05 +0100 Subject: [PATCH 02/19] Add verbatim copy of proposal tex template --- proposal/proposal.tex | 159 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 159 insertions(+) create mode 100644 proposal/proposal.tex diff --git a/proposal/proposal.tex b/proposal/proposal.tex new file mode 100644 index 0000000..861f377 --- /dev/null +++ b/proposal/proposal.tex @@ -0,0 +1,159 @@ +\documentclass{article} + + + +\usepackage[utf8]{inputenc} + +\usepackage{natbib} +\usepackage{hyperref} + +\usepackage{graphicx} + +\usepackage[colorinlistoftodos]{todonotes} + +\usepackage{parskip} +\setlength{\parskip}{10pt} + +\usepackage{tikz} +\usetikzlibrary{arrows, decorations.markings} + +\usepackage{chngcntr} +\counterwithout{figure}{section} + + + +\begin{document} + + +\begin{titlepage} + + +\centering + + +{\scshape\LARGE Master thesis project proposal\\} + +\vspace{0.5cm} + +{\huge\bfseries Title of the project\\} + +\vspace{2cm} + +{\Large name and email adress of student 1\\} + +\vspace{0.2cm} + +{\Large name and email adress of student 2\\} + +\vspace{1.0cm} + +{\large Suggested Supervisor at CSE (if you have one, otherwise skip this row): Name of supervisor\\} + +\vspace{1.5cm} + +{\large Supervisor at Company (if applicable): Name of supervisor, name of company\\} + +\vspace{1.5cm} + +{\large Relevant completed courses student 1:\par} + +{\itshape List (course code, name of course)\\} + +\vspace{1.5cm} + +{\large Relevant completed courses student 2:\par} + +{\itshape List (course code, name of course)\\} + +\vfill + + + +\vfill + +{\large \today\\} + + +\end{titlepage} + +\section{Introduction} + + +Briefly describe and motivate the project, and convince the reader of the importance of the proposed thesis work. +A good introduction will answer these questions: Why is addressing these challenges significant for gaining new knowledge +in the studied domain? How and where can this new knowledge be applied? + + + +\section{Problem} + + + +This section is optional. It may be used if there is a need to describe the problem that you want to solve in more technical +detail and if this problem description is too extensive to fit in the introduction. + + + + +\section{Context} + + + +Use one or two relevant and high quality references for providing evidence from the literature that the proposed study indeed +includes scientific and engineering challenges, or is related to existing ones. Convince the reader that the problem addressed +in this thesis has not been solved prior to this project. + + + + + +\section{Goals and Challenges} + + + +Describe your contribution with respect to concepts, theory and technical goals. Ensure that the scientific and engineering +challenges stand out so that the reader can easily recognize that you are planning to solve an advanced problem. + + +\section{Approach} + + + +Various scientific approaches are appropriate for different challenges and project goals. Outline and justify the ones that +you have selected. For example, when your project considers systematic data collection, you need to explain how you will analyze +the data, in order to address your challenges and project goals. + +One scientific approach is to use formal models and rigorous +mathematical argumentation to address aspects like correctness and efficiency. If this is relevant, describe the related algorithmic +subjects, and how you plan to address the studied problem. For example, if your plan is to study the problem from a computability aspect, +address the relevant issues, such as algorithm and data structure design, complexity analysis, etc. If you plan to develop and +evaluate a prototype, briefly describe your plans to design, implement, and evaluate your prototype by reviewing at most two relevant +issues, such as key functionalities and their evaluation criteria. + +The design and implementation should specify prototype properties, +such as functionalities and performance goals, e.g., scalability, memory, energy. Motivate key design selection, with respect to state +of the art and existing platforms, libraries, etc. + +When discussing evaluation criteria, describe the testing environment, e.g., test-bed +experiments, simulation, and user studies, which you plan to use when assessing your prototype. Specify key tools, and preliminary +test-case scenarios. Explain how and why you plan to use the evaluation criteria in order to demonstrate the functionalities and +design goals. Explain how you plan to compare your prototype to the state of the art using the proposed test-case evaluation scenarios +and benchmarks. + + + +\section{References} + + + +%\bibliographystyle{plain} + +%\bibliography{references} + + + +Reference all sources that are cited in your proposal using, e.g. the APA, Harvard2, or IEEE3 style. + + + +\end{document} From fdf82775c07b2c8460223b25ba8a3149dcefb35c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Sun, 26 Nov 2017 14:59:29 +0100 Subject: [PATCH 03/19] Remove trailing whitespace --- proposal/proposal.tex | 98 +++++++++++++++++++++---------------------- 1 file changed, 49 insertions(+), 49 deletions(-) diff --git a/proposal/proposal.tex b/proposal/proposal.tex index 861f377..80f87bf 100644 --- a/proposal/proposal.tex +++ b/proposal/proposal.tex @@ -12,7 +12,7 @@ \usepackage[colorinlistoftodos]{todonotes} \usepackage{parskip} -\setlength{\parskip}{10pt} +\setlength{\parskip}{10pt} \usepackage{tikz} \usetikzlibrary{arrows, decorations.markings} @@ -26,52 +26,52 @@ \begin{titlepage} - + \centering - - + + {\scshape\LARGE Master thesis project proposal\\} - + \vspace{0.5cm} - + {\huge\bfseries Title of the project\\} - + \vspace{2cm} - + {\Large name and email adress of student 1\\} - + \vspace{0.2cm} - + {\Large name and email adress of student 2\\} - + \vspace{1.0cm} - + {\large Suggested Supervisor at CSE (if you have one, otherwise skip this row): Name of supervisor\\} - + \vspace{1.5cm} - + {\large Supervisor at Company (if applicable): Name of supervisor, name of company\\} - + \vspace{1.5cm} - + {\large Relevant completed courses student 1:\par} - + {\itshape List (course code, name of course)\\} - + \vspace{1.5cm} - + {\large Relevant completed courses student 2:\par} - + {\itshape List (course code, name of course)\\} - -\vfill - - \vfill - -{\large \today\\} + + + +\vfill + +{\large \today\\} \end{titlepage} @@ -79,17 +79,17 @@ \section{Introduction} -Briefly describe and motivate the project, and convince the reader of the importance of the proposed thesis work. -A good introduction will answer these questions: Why is addressing these challenges significant for gaining new knowledge +Briefly describe and motivate the project, and convince the reader of the importance of the proposed thesis work. +A good introduction will answer these questions: Why is addressing these challenges significant for gaining new knowledge in the studied domain? How and where can this new knowledge be applied? -\section{Problem} +\section{Problem} -This section is optional. It may be used if there is a need to describe the problem that you want to solve in more technical +This section is optional. It may be used if there is a need to describe the problem that you want to solve in more technical detail and if this problem description is too extensive to fit in the introduction. @@ -99,8 +99,8 @@ detail and if this problem description is too extensive to fit in the introducti -Use one or two relevant and high quality references for providing evidence from the literature that the proposed study indeed -includes scientific and engineering challenges, or is related to existing ones. Convince the reader that the problem addressed +Use one or two relevant and high quality references for providing evidence from the literature that the proposed study indeed +includes scientific and engineering challenges, or is related to existing ones. Convince the reader that the problem addressed in this thesis has not been solved prior to this project. @@ -111,34 +111,34 @@ in this thesis has not been solved prior to this project. -Describe your contribution with respect to concepts, theory and technical goals. Ensure that the scientific and engineering -challenges stand out so that the reader can easily recognize that you are planning to solve an advanced problem. +Describe your contribution with respect to concepts, theory and technical goals. Ensure that the scientific and engineering +challenges stand out so that the reader can easily recognize that you are planning to solve an advanced problem. \section{Approach} -Various scientific approaches are appropriate for different challenges and project goals. Outline and justify the ones that -you have selected. For example, when your project considers systematic data collection, you need to explain how you will analyze +Various scientific approaches are appropriate for different challenges and project goals. Outline and justify the ones that +you have selected. For example, when your project considers systematic data collection, you need to explain how you will analyze the data, in order to address your challenges and project goals. -One scientific approach is to use formal models and rigorous -mathematical argumentation to address aspects like correctness and efficiency. If this is relevant, describe the related algorithmic -subjects, and how you plan to address the studied problem. For example, if your plan is to study the problem from a computability aspect, -address the relevant issues, such as algorithm and data structure design, complexity analysis, etc. If you plan to develop and -evaluate a prototype, briefly describe your plans to design, implement, and evaluate your prototype by reviewing at most two relevant +One scientific approach is to use formal models and rigorous +mathematical argumentation to address aspects like correctness and efficiency. If this is relevant, describe the related algorithmic +subjects, and how you plan to address the studied problem. For example, if your plan is to study the problem from a computability aspect, +address the relevant issues, such as algorithm and data structure design, complexity analysis, etc. If you plan to develop and +evaluate a prototype, briefly describe your plans to design, implement, and evaluate your prototype by reviewing at most two relevant issues, such as key functionalities and their evaluation criteria. -The design and implementation should specify prototype properties, -such as functionalities and performance goals, e.g., scalability, memory, energy. Motivate key design selection, with respect to state -of the art and existing platforms, libraries, etc. +The design and implementation should specify prototype properties, +such as functionalities and performance goals, e.g., scalability, memory, energy. Motivate key design selection, with respect to state +of the art and existing platforms, libraries, etc. -When discussing evaluation criteria, describe the testing environment, e.g., test-bed -experiments, simulation, and user studies, which you plan to use when assessing your prototype. Specify key tools, and preliminary -test-case scenarios. Explain how and why you plan to use the evaluation criteria in order to demonstrate the functionalities and -design goals. Explain how you plan to compare your prototype to the state of the art using the proposed test-case evaluation scenarios -and benchmarks. +When discussing evaluation criteria, describe the testing environment, e.g., test-bed +experiments, simulation, and user studies, which you plan to use when assessing your prototype. Specify key tools, and preliminary +test-case scenarios. Explain how and why you plan to use the evaluation criteria in order to demonstrate the functionalities and +design goals. Explain how you plan to compare your prototype to the state of the art using the proposed test-case evaluation scenarios +and benchmarks. From 35c246f17dc82ddd806797c4b1155293fd7ebc94 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Sun, 26 Nov 2017 15:00:26 +0100 Subject: [PATCH 04/19] Add gitignore --- proposal/.gitignore | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 proposal/.gitignore diff --git a/proposal/.gitignore b/proposal/.gitignore new file mode 100644 index 0000000..c0ed534 --- /dev/null +++ b/proposal/.gitignore @@ -0,0 +1,6 @@ +*.aux +*.fdb_latexmk +*.fls +*.log +*.out +*.pdf \ No newline at end of file From 6497357040adcbed045f3d89c92c6f150bffeee9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Sat, 2 Dec 2017 01:34:04 +0100 Subject: [PATCH 05/19] Add missing tex-files --- proposal/chalmerstitle.sty | 56 +++++++++++++++++++++++ proposal/macros.tex | 14 ++++++ proposal/refs.bib | 94 ++++++++++++++++++++++++++++++++++++++ 3 files changed, 164 insertions(+) create mode 100644 proposal/chalmerstitle.sty create mode 100644 proposal/macros.tex create mode 100644 proposal/refs.bib diff --git a/proposal/chalmerstitle.sty b/proposal/chalmerstitle.sty new file mode 100644 index 0000000..5a48b93 --- /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\\ +Models of Computation\\ +Research topic in Computer Science\\ +Types for programs and proofs +} + +\vfill + +{\large \@institution\\\today\\} + +\end{center} +\end{titlepage} +} diff --git a/proposal/macros.tex b/proposal/macros.tex new file mode 100644 index 0000000..abf3d42 --- /dev/null +++ b/proposal/macros.tex @@ -0,0 +1,14 @@ +\newcommand*{\defeq}{\mathrel{\vcenter{\baselineskip0.5ex \lineskiplimit0pt + \hbox{\scriptsize.}\hbox{\scriptsize.}}}% + =} + +\newcommand{\defeq}{\coloneqq} +\newcommand{\bN}{\mathbb{N}} +\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} diff --git a/proposal/refs.bib b/proposal/refs.bib new file mode 100644 index 0000000..559ab63 --- /dev/null +++ b/proposal/refs.bib @@ -0,0 +1,94 @@ +@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{cubical-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} +} \ No newline at end of file From 4175bd87ac1492f8ce2b8dfa8764b0785cfa12a4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Sat, 2 Dec 2017 01:34:33 +0100 Subject: [PATCH 06/19] Commit finished proposal Was done writing this a week ago --- proposal/.gitignore | 4 +- proposal/proposal.tex | 386 ++++++++++++++++++++++++++++++------------ 2 files changed, 278 insertions(+), 112 deletions(-) diff --git a/proposal/.gitignore b/proposal/.gitignore index c0ed534..b19d31d 100644 --- a/proposal/.gitignore +++ b/proposal/.gitignore @@ -3,4 +3,6 @@ *.fls *.log *.out -*.pdf \ No newline at end of file +*.pdf +*.bbl +*.blg diff --git a/proposal/proposal.tex b/proposal/proposal.tex index 80f87bf..aa51f51 100644 --- a/proposal/proposal.tex +++ b/proposal/proposal.tex @@ -5,155 +5,319 @@ \usepackage[utf8]{inputenc} \usepackage{natbib} -\usepackage{hyperref} +\usepackage[hidelinks]{hyperref} \usepackage{graphicx} +\usepackage{color,soul} \usepackage[colorinlistoftodos]{todonotes} \usepackage{parskip} -\setlength{\parskip}{10pt} +\usepackage{multicol} +\usepackage{amsmath,amssymb} +% \setlength{\parskip}{10pt} -\usepackage{tikz} -\usetikzlibrary{arrows, decorations.markings} +% \usepackage{tikz} +% \usetikzlibrary{arrows, decorations.markings} -\usepackage{chngcntr} -\counterwithout{figure}{section} +% \usepackage{chngcntr} +% \counterwithout{figure}{section} +\usepackage{chalmerstitle} +\input{macros.tex} +% \newcommand{\sectiondescription}[1]{\todo[inline,color=green!40]{#1}} +\newcommand{\sectiondescription}[1]{\iffalse #1\fi} +\newcommand{\mycomment}[1]{\hl{#1}} +\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} - -\begin{titlepage} - - -\centering - - -{\scshape\LARGE Master thesis project proposal\\} - -\vspace{0.5cm} - -{\huge\bfseries Title of the project\\} - -\vspace{2cm} - -{\Large name and email adress of student 1\\} - -\vspace{0.2cm} - -{\Large name and email adress of student 2\\} - -\vspace{1.0cm} - -{\large Suggested Supervisor at CSE (if you have one, otherwise skip this row): Name of supervisor\\} - -\vspace{1.5cm} - -{\large Supervisor at Company (if applicable): Name of supervisor, name of company\\} - -\vspace{1.5cm} - -{\large Relevant completed courses student 1:\par} - -{\itshape List (course code, name of course)\\} - -\vspace{1.5cm} - -{\large Relevant completed courses student 2:\par} - -{\itshape List (course code, name of course)\\} - -\vfill - - - -\vfill - -{\large \today\\} - - -\end{titlepage} - +\maketitle +% +\mycomment{Text marked like this are todo-comments.} +\sectiondescription{Text marked like this describe what should go in the section.} +% \section{Introduction} +% +\sectiondescription{% +Briefly describe and motivate the project, and convince the reader of the +importance of the proposed thesis work. A good introduction will answer these +questions: Why is addressing these challenges significant for gaining new +knowledge in the studied domain? How and where can this new knowledge be +applied? +} +% +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 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 case-study 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. -Briefly describe and motivate the project, and convince the reader of the importance of the proposed thesis work. -A good introduction will answer these questions: Why is addressing these challenges significant for gaining new knowledge -in the studied domain? How and where can this new knowledge be applied? - - - +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 \emph{model} for CTT. +% \section{Problem} +% +\sectiondescription{% +This section is optional. It may be used if there is a need to describe the +problem that you want to solve in more technical detail and if this problem +description is too extensive to fit in the introduction. +} +% +In the following two subsections I present two examples that illustrate the +limitaiton 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{defnitional 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 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. +% +\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} +% +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. -This section is optional. It may be used if there is a need to describe the problem that you want to solve in more technical -detail and if this problem description is too extensive to fit in the introduction. +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 an isomorphism is give an \nomen{isomorphism} between the two types. +That is, a function $f : A \to B$ for which it has 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$. +What we want is to identify isomorphic types. This is 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{Category Theory as a case-study} +% +The above examples serves to illustrate the limitation of Agda. One case where +these limitations are particularly prohibitive is in the case of Category +Theory. Category Theory -- at a glance -- is ``is the mathematical study of +(abstract) algebras of functions'' (\cite{awodey-2006}). So by that token +functional extensionality is particularly useful for formulating Category +Theory. Another aspect of Category Theory is that one usually want to talk about +things ``up to isomorphism''. Another way of phrasing this is that we want to +identify isomorphic objects. This is exactly what we get from univalence. +\mycomment{Can there be issues with identifying isomoprhic types? Suddenly many +seemingly different objects collaps into the same thing (e.g.: $\{1\} \equiv +\{2\}$, $\mathbb{Z} \equiv \mathbb{N}$, \ldots)} +\subsection{Category Theory as a model for Cubical Type Theory} +% +Certain categories give rise to a model for Cubical Type Theory +(\cite{bezem-2014}). \cite{dybjer-1995} describe how to construct a model for a +type theory. One part of which is to `check equations' - that is, that the model +satisfies the axioms -- i.e. typing rules -- for the type theory under study. In +this case the Cubical Sets have to satisfy the corresponding `translation' of +those axioms in the categorical setting. The \emph{translation} will not be +given formally (i.e. as a function in Agda). That translation will be given +informally, and I will show that the model satisfies these. +% +\mycomment{Quickly explain that we can formulate the language of Cubical Type +Theory and show that Cubical Sets are a model of this.} +% \section{Context} +% +\sectiondescription{% +Use one or two relevant and high quality references for providing evidence from +the literature that the proposed study indeed includes scientific and +engineering challenges, or is related to existing ones. Convince the reader that +the problem addressed in this thesis has not been solved prior to this project. +} +% +Work by \citeauthor{bezem-2014} resulted in a model for type theory where +univalence is expressible. This model is an example of a \nomen{categorical +model} -- that is, a model formulated in terms of categories. As such this +paper will also serve as a further object of study for the concepts from +Category Theory that I will have formalized. +Work by \citeauthor{cohen-2016} have resulted in a type system where univalence +is expressible. The categorical model from above is a model of this type theory. +So these two ideas are closely related. +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. As such, my work with this extension will serve as evidence to the +merrit of this implementation. -Use one or two relevant and high quality references for providing evidence from the literature that the proposed study indeed -includes scientific and engineering challenges, or is related to existing ones. Convince the reader that the problem addressed -in this thesis has not been solved prior to this project. - - +The idea of formalizing Category Theory in proof assistants is not a new idea +(\mycomment{citations \ldots}). The contribution of this thesis is to explore +how working in a cubical setting will make it possible to proove more things and +to resuse proofs. There are alternative approaches to working in a cubical +setting where one can still have univalence and functional extensionality. One +could e.g. postulate these as axioms. This approach has other shortcomings, +e.g.; you loose canonicity (\mycomment{citation}). \mycomment{Perhaps we could + also formulate equality as another type. What are some downsides of this + approach?} +\mycomment{Mention internal type theory c.f. Dybjers paper? He talks about two +types of internal type theory. One of them is where you express the typing +rules of your languages within that languages} +\mycomment{Other aspects that I think are interesting: Type Theory as a foundational +system; why is ``nice'' to have a categorical model?} +\mycomment{Should perhaps mention how Cubical Type Theory came out out of Homotopy +Type Theory that came out of Topology} +% \section{Goals and Challenges} +% +\sectiondescription{% +Describe your contribution with respect to concepts, theory and technical goals. +Ensure that the scientific and engineering challenges stand out so that the +reader can easily recognize that you are planning to solve an advanced problem. +} +% +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 I will do will be based on previous work. These proofs are +pen-and-paper proof. Translating such proofs to a type system is not always +straight-forward. A further challenge is that in cubical Agda there can be +multiple distinct terms that inhabit a given equality proof. 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. This is not +a strict goal for this thesis but would certainly be a natural extension of it. - -Describe your contribution with respect to concepts, theory and technical goals. Ensure that the scientific and engineering -challenges stand out so that the reader can easily recognize that you are planning to solve an advanced problem. - - +The final thesis should also include a discussion about the pros/cons of using +Cubical Agda; \mycomment{have Agda become more useful, easy to work with, +\ldots ? } Ideally my work will serve as an argument that working in a Cubical +setting is useful. +% \section{Approach} +% +\sectiondescription{% +Various scientific approaches are appropriate for different challenges and +project goals. Outline and justify the ones that you have selected. For example, +when your project considers systematic data collection, you need to explain how +you will analyze the data, in order to address your challenges and project +goals. +One scientific approach is to use formal models and rigorous mathematical +argumentation to address aspects like correctness and efficiency. If this is +relevant, describe the related algorithmic subjects, and how you plan to address +the studied problem. For example, if your plan is to study the problem from a +computability aspect, address the relevant issues, such as algorithm and data +structure design, complexity analysis, etc. If you plan to develop and evaluate +a prototype, briefly describe your plans to design, implement, and evaluate your +prototype by reviewing at most two relevant issues, such as key functionalities +and their evaluation criteria. +The design and implementation should specify prototype properties, such as +functionalities and performance goals, e.g., scalability, memory, energy. +Motivate key design selection, with respect to state of the art and existing +platforms, libraries, etc. -Various scientific approaches are appropriate for different challenges and project goals. Outline and justify the ones that -you have selected. For example, when your project considers systematic data collection, you need to explain how you will analyze -the data, in order to address your challenges and project goals. - -One scientific approach is to use formal models and rigorous -mathematical argumentation to address aspects like correctness and efficiency. If this is relevant, describe the related algorithmic -subjects, and how you plan to address the studied problem. For example, if your plan is to study the problem from a computability aspect, -address the relevant issues, such as algorithm and data structure design, complexity analysis, etc. If you plan to develop and -evaluate a prototype, briefly describe your plans to design, implement, and evaluate your prototype by reviewing at most two relevant -issues, such as key functionalities and their evaluation criteria. - -The design and implementation should specify prototype properties, -such as functionalities and performance goals, e.g., scalability, memory, energy. Motivate key design selection, with respect to state -of the art and existing platforms, libraries, etc. - -When discussing evaluation criteria, describe the testing environment, e.g., test-bed -experiments, simulation, and user studies, which you plan to use when assessing your prototype. Specify key tools, and preliminary -test-case scenarios. Explain how and why you plan to use the evaluation criteria in order to demonstrate the functionalities and -design goals. Explain how you plan to compare your prototype to the state of the art using the proposed test-case evaluation scenarios -and benchmarks. - - - +When discussing evaluation criteria, describe the testing environment, e.g., +test-bed experiments, simulation, and user studies, which you plan to use when +assessing your prototype. Specify key tools, and preliminary test-case +scenarios. Explain how and why you plan to use the evaluation criteria in order +to demonstrate the functionalities and design goals. Explain how you plan to +compare your prototype to the state of the art using the proposed test-case +evaluation scenarios and benchmarks. +} +% +\mycomment{I don't know what more I can say here than has already been +explained. Perhaps this section is not needed for me?} +% \section{References} +% +\bibliographystyle{plainnat} - - -%\bibliographystyle{plain} - -%\bibliography{references} - - - -Reference all sources that are cited in your proposal using, e.g. the APA, Harvard2, or IEEE3 style. - - - +\bibliography{refs} \mycomment{I have a bunch of other relevant references that +I haven't been able to incorporate into my text yet...} \end{document} From 3e717d4b1fc8bf4d102766a15c18952be4e1a733 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Sat, 2 Dec 2017 01:36:16 +0100 Subject: [PATCH 07/19] Prove that functor composition gives rise to a functor --- src/Category.agda | 136 +++++++++++++++++++++++++++++++--------------- 1 file changed, 91 insertions(+), 45 deletions(-) diff --git a/src/Category.agda b/src/Category.agda index d1aa814..7504bd1 100644 --- a/src/Category.agda +++ b/src/Category.agda @@ -11,6 +11,7 @@ open import Data.Empty postulate undefined : {ℓ : Level} → {A : Set ℓ} → A record Category {ℓ ℓ'} : Set (lsuc (ℓ' ⊔ ℓ)) where + constructor category field Object : Set ℓ Arrow : Object → Object → Set ℓ' @@ -21,51 +22,67 @@ 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 + constructor functor 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} + 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''} - → f (a' C.⊕ a) ≡ f a' D.⊕ f a + → func→ (a' C.⊕ a) ≡ func→ a' D.⊕ func→ 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 +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 : {ℓ ℓ' : Level} → {C : Category {ℓ} {ℓ'}} → Functor C C +-- Identity = record { F* = λ x → x ; F→ = λ x → x ; ident = refl ; distrib = refl } +identity = functor (λ x → x) (λ x → x) (refl) (refl) module _ {ℓ ℓ' : Level} {ℂ : Category {ℓ} {ℓ'}} { A B : Object ℂ } where private @@ -116,9 +133,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 +140,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,19 +182,50 @@ 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} - } +-- 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 {ℓ-suc (ℓ ⊔ ℓ')} {ℓ ⊔ ℓ'} + CatCat = + record + { Object = Category {ℓ} {ℓ'} + ; Arrow = Functor + ; 𝟙 = identity + ; _⊕_ = functor-comp + ; assoc = {!!} + ; ident = ident-r , ident-l + } Hom : {ℓ ℓ' : Level} → {ℂ : Category {ℓ} {ℓ'}} → (A B : Object ℂ) → Set ℓ' Hom {ℂ = ℂ} A B = Arrow ℂ A B From 4a98b2aa3d6db03840f37cac4eeb5626b14eb61d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Tue, 12 Dec 2017 12:39:58 +0100 Subject: [PATCH 08/19] Leftovers... --- src/Category.agda | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/Category.agda b/src/Category.agda index 7504bd1..b1f7c88 100644 --- a/src/Category.agda +++ b/src/Category.agda @@ -4,9 +4,11 @@ module 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 @@ -216,7 +218,7 @@ module _ {ℓ ℓ' : Level} where ident-l : identity ⊛ f ≡ f ident-l = {!!} - CatCat : Category {ℓ-suc (ℓ ⊔ ℓ')} {ℓ ⊔ ℓ'} + CatCat : Category {lsuc (ℓ ⊔ ℓ')} {ℓ ⊔ ℓ'} CatCat = record { Object = Category {ℓ} {ℓ'} From a28d0986beb03ab0e135d027d322ba07d5d7af69 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Tue, 12 Dec 2017 15:45:20 +0100 Subject: [PATCH 09/19] Incorporate some changes suggested by Inaari --- proposal/chalmerstitle.sty | 8 +- proposal/proposal.tex | 202 +++++++++++++++++++------------------ proposal/refs.bib | 22 +++- 3 files changed, 128 insertions(+), 104 deletions(-) diff --git a/proposal/chalmerstitle.sty b/proposal/chalmerstitle.sty index 5a48b93..c2aa355 100644 --- a/proposal/chalmerstitle.sty +++ b/proposal/chalmerstitle.sty @@ -41,10 +41,10 @@ {\large Relevant completed courses:\par} {\itshape -Logic in Computer Science\\ -Models of Computation\\ -Research topic in Computer Science\\ -Types for programs and proofs +Logic in Computer Science -- DAT060\\ +Models of Computation -- TDA184\\ +Research topic in Computer Science -- DAT235\\ +Types for programs and proofs -- DAT140 } \vfill diff --git a/proposal/proposal.tex b/proposal/proposal.tex index aa51f51..77d5289 100644 --- a/proposal/proposal.tex +++ b/proposal/proposal.tex @@ -42,7 +42,6 @@ \maketitle % -\mycomment{Text marked like this are todo-comments.} \sectiondescription{Text marked like this describe what should go in the section.} % \section{Introduction} @@ -61,18 +60,18 @@ 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 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 case-study 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. +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 \emph{model} for CTT. +\nomen{Cubical Sets} give rise to a model of CTT. % \section{Problem} % @@ -94,8 +93,8 @@ $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{defnitional equality} -and write $n + 0 = n$ to assert this fact. We call it definitional +$n + 0$ is definitionally equal to $n$. We call this \nomen{defnitional +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: % @@ -108,10 +107,10 @@ which is: % 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 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$. +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 @@ -136,59 +135,62 @@ I also want to talk about: \fi \subsection{Equality of isomorphic types} % -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. +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 an isomorphism is give an \nomen{isomorphism} between the two types. -That is, a function $f : A \to B$ for which it has 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$. +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$. -What we want is to identify isomorphic types. This is 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'.} +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{Category Theory as a case-study} +\subsection{Formalizing Category Theory} % The above examples serves to illustrate the limitation of Agda. One case where -these limitations are particularly prohibitive is in the case of Category -Theory. Category Theory -- at a glance -- is ``is the mathematical study of -(abstract) algebras of functions'' (\cite{awodey-2006}). So by that token +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. Another aspect of Category Theory is that one usually want to talk about -things ``up to isomorphism''. Another way of phrasing this is that we want to -identify isomorphic objects. This is exactly what we get from univalence. +Theory. In Category theory it is also common to identify isomorphic structures +and this is exactly what we get from univalence. -\mycomment{Can there be issues with identifying isomoprhic types? Suddenly many -seemingly different objects collaps into the same thing (e.g.: $\{1\} \equiv -\{2\}$, $\mathbb{Z} \equiv \mathbb{N}$, \ldots)} +\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. -\subsection{Category Theory as a model for Cubical Type Theory} -% -Certain categories give rise to a model for Cubical Type Theory -(\cite{bezem-2014}). \cite{dybjer-1995} describe how to construct a model for a -type theory. One part of which is to `check equations' - that is, that the model -satisfies the axioms -- i.e. typing rules -- for the type theory under study. In -this case the Cubical Sets have to satisfy the corresponding `translation' of -those axioms in the categorical setting. The \emph{translation} will not be -given formally (i.e. as a function in Agda). That translation will be given -informally, and I will show that the model satisfies these. -% -\mycomment{Quickly explain that we can formulate the language of Cubical Type -Theory and show that Cubical Sets are a model of this.} +In the context of a given type theory and restricting ourselves to +\emph{categorical} models a model will consists 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 device 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. In stead the translation will be accounted +for informally. % \section{Context} % @@ -199,40 +201,38 @@ engineering challenges, or is related to existing ones. Convince the reader that the problem addressed in this thesis has not been solved prior to this project. } % -Work by \citeauthor{bezem-2014} resulted in a model for type theory where -univalence is expressible. This model is an example of a \nomen{categorical -model} -- that is, a model formulated in terms of categories. As such this -paper will also serve as a further object of study for the concepts from -Category Theory that I will have formalized. - -Work by \citeauthor{cohen-2016} have resulted in a type system where univalence -is expressible. The categorical model from above is a model of this type theory. -So these two ideas are closely related. +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. As such, my work with this extension will serve as evidence to the -merrit of this implementation. +this thesis. -The idea of formalizing Category Theory in proof assistants is not a new idea -(\mycomment{citations \ldots}). The contribution of this thesis is to explore -how working in a cubical setting will make it possible to proove more things and -to resuse proofs. There are alternative approaches to working in a cubical -setting where one can still have univalence and functional extensionality. One -could e.g. postulate these as axioms. This approach has other shortcomings, -e.g.; you loose canonicity (\mycomment{citation}). \mycomment{Perhaps we could - also formulate equality as another type. What are some downsides of this - approach?} +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{so-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. -\mycomment{Mention internal type theory c.f. Dybjers paper? He talks about two -types of internal type theory. One of them is where you express the typing -rules of your languages within that languages} +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$ +application 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. -\mycomment{Other aspects that I think are interesting: Type Theory as a foundational -system; why is ``nice'' to have a categorical model?} - -\mycomment{Should perhaps mention how Cubical Type Theory came out out of Homotopy -Type Theory that came out of Topology} +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} % @@ -259,25 +259,28 @@ 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 I will do will be based on previous work. These proofs are -pen-and-paper proof. Translating such proofs to a type system is not always -straight-forward. A further challenge is that in cubical Agda there can be -multiple distinct terms that inhabit a given equality proof. 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. +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 that enjoys \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. This is not -a strict goal for this thesis but would certainly be a natural extension of it. +a goal for this thesis but rather a natural extension of it. -The final thesis should also include a discussion about the pros/cons of using -Cubical Agda; \mycomment{have Agda become more useful, easy to work with, -\ldots ? } Ideally my work will serve as an argument that working in a Cubical -setting is useful. +The thesis shall conclude with a discussion about the benefits of Cubical Agda. % +\iffalse \section{Approach} % \sectiondescription{% @@ -314,10 +317,11 @@ evaluation scenarios and benchmarks. \mycomment{I don't know what more I can say here than has already been explained. Perhaps this section is not needed for me?} % +\fi \section{References} % \bibliographystyle{plainnat} - -\bibliography{refs} \mycomment{I have a bunch of other relevant references that -I haven't been able to incorporate into my text yet...} +\nocite{cubical-demo} +\nocite{coquand-2013} +\bibliography{refs} \end{document} diff --git a/proposal/refs.bib b/proposal/refs.bib index 559ab63..50e3853 100644 --- a/proposal/refs.bib +++ b/proposal/refs.bib @@ -49,7 +49,7 @@ howpublished = {\url{https://github.com/agda/agda}}, commit = {92de32c0669cb414f329fff25497a9ddcd58b951} } -@misc{cubical-agda, +@misc{agda, author = {Ulf Norell}, title = {Agda}, year = {2017}, @@ -91,4 +91,24 @@ 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{so-formalizations, + TITLE = {Formalizations of category theory in proof assistants}, + AUTHOR = {Jason Gross (\url{https://mathoverflow.net/users/30462/jason-gross})}, + HOWPUBLISHED = {MathOverflow}, + NOTE = {Version: 2014-01-19}, + year={2014}, + EPRINT = {https://mathoverflow.net/q/152497}, + URL = {https://mathoverflow.net/q/152497} } \ No newline at end of file From c9042c682e75148b0f2e7d88fea36c674170d0c4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Mon, 8 Jan 2018 22:16:11 +0100 Subject: [PATCH 10/19] Changes to proposal --- proposal/proposal.tex | 75 +------------------------------------------ proposal/refs.bib | 6 ++-- 2 files changed, 4 insertions(+), 77 deletions(-) diff --git a/proposal/proposal.tex b/proposal/proposal.tex index 77d5289..74a1835 100644 --- a/proposal/proposal.tex +++ b/proposal/proposal.tex @@ -8,9 +8,6 @@ \usepackage[hidelinks]{hyperref} \usepackage{graphicx} -\usepackage{color,soul} - -\usepackage[colorinlistoftodos]{todonotes} \usepackage{parskip} \usepackage{multicol} @@ -25,9 +22,6 @@ \usepackage{chalmerstitle} \input{macros.tex} -% \newcommand{\sectiondescription}[1]{\todo[inline,color=green!40]{#1}} -\newcommand{\sectiondescription}[1]{\iffalse #1\fi} -\newcommand{\mycomment}[1]{\hl{#1}} \title{Category Theory and Cubical Type Theory} \author{Frederik Hanghøj Iversen} @@ -42,18 +36,8 @@ \maketitle % -\sectiondescription{Text marked like this describe what should go in the section.} -% \section{Introduction} % -\sectiondescription{% -Briefly describe and motivate the project, and convince the reader of the -importance of the proposed thesis work. A good introduction will answer these -questions: Why is addressing these challenges significant for gaining new -knowledge in the studied domain? How and where can this new knowledge be -applied? -} -% 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. @@ -75,12 +59,6 @@ parts that will be useful in the second part of the project: Showing that % \section{Problem} % -\sectiondescription{% -This section is optional. It may be used if there is a need to describe the -problem that you want to solve in more technical detail and if this problem -description is too extensive to fit in the introduction. -} -% In the following two subsections I present two examples that illustrate the limitaiton inherent in ITT and by extension to the expressiveness of Agda. % @@ -194,13 +172,6 @@ for informally. % \section{Context} % -\sectiondescription{% -Use one or two relevant and high quality references for providing evidence from -the literature that the proposed study indeed includes scientific and -engineering challenges, or is related to existing ones. Convince the reader that -the problem addressed in this thesis has not been solved prior to this project. -} -% 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 @@ -214,7 +185,7 @@ 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{so-formalizations}}. The +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. @@ -236,12 +207,6 @@ theory and is cumbersome to work with in practice (\cite[p. 4]{huber-2016}). % \section{Goals and Challenges} % -\sectiondescription{% -Describe your contribution with respect to concepts, theory and technical goals. -Ensure that the scientific and engineering challenges stand out so that the -reader can easily recognize that you are planning to solve an advanced problem. -} -% In summary, the aim of the project is to: % \begin{itemize} @@ -280,44 +245,6 @@ a goal for this thesis but rather a natural extension of it. The thesis shall conclude with a discussion about the benefits of Cubical Agda. % -\iffalse -\section{Approach} -% -\sectiondescription{% -Various scientific approaches are appropriate for different challenges and -project goals. Outline and justify the ones that you have selected. For example, -when your project considers systematic data collection, you need to explain how -you will analyze the data, in order to address your challenges and project -goals. - -One scientific approach is to use formal models and rigorous mathematical -argumentation to address aspects like correctness and efficiency. If this is -relevant, describe the related algorithmic subjects, and how you plan to address -the studied problem. For example, if your plan is to study the problem from a -computability aspect, address the relevant issues, such as algorithm and data -structure design, complexity analysis, etc. If you plan to develop and evaluate -a prototype, briefly describe your plans to design, implement, and evaluate your -prototype by reviewing at most two relevant issues, such as key functionalities -and their evaluation criteria. - -The design and implementation should specify prototype properties, such as -functionalities and performance goals, e.g., scalability, memory, energy. -Motivate key design selection, with respect to state of the art and existing -platforms, libraries, etc. - -When discussing evaluation criteria, describe the testing environment, e.g., -test-bed experiments, simulation, and user studies, which you plan to use when -assessing your prototype. Specify key tools, and preliminary test-case -scenarios. Explain how and why you plan to use the evaluation criteria in order -to demonstrate the functionalities and design goals. Explain how you plan to -compare your prototype to the state of the art using the proposed test-case -evaluation scenarios and benchmarks. -} -% -\mycomment{I don't know what more I can say here than has already been -explained. Perhaps this section is not needed for me?} -% -\fi \section{References} % \bibliographystyle{plainnat} diff --git a/proposal/refs.bib b/proposal/refs.bib index 50e3853..93665a7 100644 --- a/proposal/refs.bib +++ b/proposal/refs.bib @@ -103,12 +103,12 @@ year={1995}, publisher={University of Edinburgh. College of Science and Engineering. School of Informatics.} } -@MISC{so-formalizations, +@MISC{mo-formalizations, TITLE = {Formalizations of category theory in proof assistants}, - AUTHOR = {Jason Gross (\url{https://mathoverflow.net/users/30462/jason-gross})}, + AUTHOR = {Jason Gross}, HOWPUBLISHED = {MathOverflow}, NOTE = {Version: 2014-01-19}, year={2014}, - EPRINT = {https://mathoverflow.net/q/152497}, + EPRINT = {\url{https://mathoverflow.net/q/152497}}, URL = {https://mathoverflow.net/q/152497} } \ No newline at end of file From e3d2c0d39ee5d6baec9a5ec00a85042ecb0a1bc8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Mon, 8 Jan 2018 22:29:29 +0100 Subject: [PATCH 11/19] Move category of Categories to own module --- src/Category.agda | 45 -------------------------- src/Category/Categories/Cat.agda | 55 ++++++++++++++++++++++++++++++++ 2 files changed, 55 insertions(+), 45 deletions(-) create mode 100644 src/Category/Categories/Cat.agda diff --git a/src/Category.agda b/src/Category.agda index b1f7c88..568f93b 100644 --- a/src/Category.agda +++ b/src/Category.agda @@ -184,51 +184,6 @@ Opposite ℂ = where open module ℂ = 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 - } - Hom : {ℓ ℓ' : Level} → {ℂ : Category {ℓ} {ℓ'}} → (A B : Object ℂ) → Set ℓ' Hom {ℂ = ℂ} A B = Arrow ℂ A B diff --git a/src/Category/Categories/Cat.agda b/src/Category/Categories/Cat.agda new file mode 100644 index 0000000..79efc49 --- /dev/null +++ b/src/Category/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 + } From 7d6db415a1a8277df7841675aacf300e880fa4ab Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Mon, 8 Jan 2018 22:48:59 +0100 Subject: [PATCH 12/19] Move modules around again. Henceforth all modules shall be placed under the top-level module-name `Cat` (at least until I've come up with a better name) Also fixes an issue caused by https://github.com/Saizan/cubical-demo/ redefining Sigma. --- src/{Category => Cat}/Categories/Cat.agda | 0 src/{Category => Cat/Categories}/Rel.agda | 15 +++++++++------ src/{Category => Cat/Categories}/Sets.agda | 0 src/{ => Cat}/Category.agda | 2 +- src/{ => Cat}/Category/Bij.agda | 0 src/{ => Cat}/Category/Free.agda | 0 src/{ => Cat}/Category/Pathy.agda | 0 src/{Category => Cat}/Cubical.agda | 5 +++-- 8 files changed, 13 insertions(+), 9 deletions(-) rename src/{Category => Cat}/Categories/Cat.agda (100%) rename src/{Category => Cat/Categories}/Rel.agda (94%) rename src/{Category => Cat/Categories}/Sets.agda (100%) rename src/{ => Cat}/Category.agda (99%) rename src/{ => Cat}/Category/Bij.agda (100%) rename src/{ => Cat}/Category/Free.agda (100%) rename src/{ => Cat}/Category/Pathy.agda (100%) rename src/{Category => Cat}/Cubical.agda (95%) diff --git a/src/Category/Categories/Cat.agda b/src/Cat/Categories/Cat.agda similarity index 100% rename from src/Category/Categories/Cat.agda rename to src/Cat/Categories/Cat.agda 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/Category/Sets.agda b/src/Cat/Categories/Sets.agda similarity index 100% rename from src/Category/Sets.agda rename to src/Cat/Categories/Sets.agda diff --git a/src/Category.agda b/src/Cat/Category.agda similarity index 99% rename from src/Category.agda rename to src/Cat/Category.agda index 568f93b..c3ce34f 100644 --- a/src/Category.agda +++ b/src/Cat/Category.agda @@ -1,6 +1,6 @@ {-# OPTIONS --cubical #-} -module Category where +module Cat.Category where open import Agda.Primitive open import Data.Unit.Base 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/Category/Cubical.agda b/src/Cat/Cubical.agda similarity index 95% rename from src/Category/Cubical.agda rename to src/Cat/Cubical.agda index 22709be..cba1c41 100644 --- a/src/Category/Cubical.agda +++ b/src/Cat/Cubical.agda @@ -1,13 +1,14 @@ -module Category.Cubical where +module Cat.Cubical where open import Agda.Primitive -open import Category 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 ⊔ ℓ) From 0cd75e6e31999cba3a34242f9a6d4c9321ffbfbd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Mon, 8 Jan 2018 22:54:53 +0100 Subject: [PATCH 13/19] Move functor-stuff to own module --- src/Cat/Category.agda | 56 -------------------------------------- src/Cat/Functor.agda | 62 +++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 62 insertions(+), 56 deletions(-) create mode 100644 src/Cat/Functor.agda diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda index c3ce34f..f508633 100644 --- a/src/Cat/Category.agda +++ b/src/Cat/Category.agda @@ -7,7 +7,6 @@ open import Data.Unit.Base 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 @@ -31,61 +30,6 @@ record Category {ℓ ℓ'} : Set (lsuc (ℓ' ⊔ ℓ)) where open Category public -record Functor {ℓc ℓc' ℓd ℓd'} (C : Category {ℓc} {ℓc'}) (D : Category {ℓd} {ℓd'}) - : Set (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') where - constructor functor - 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 = functor (λ x → x) (λ x → x) (refl) (refl) - module _ {ℓ ℓ' : Level} {ℂ : Category {ℓ} {ℓ'}} { A B : Object ℂ } where private open module ℂ = Category ℂ diff --git a/src/Cat/Functor.agda b/src/Cat/Functor.agda new file mode 100644 index 0000000..7f9e2af --- /dev/null +++ b/src/Cat/Functor.agda @@ -0,0 +1,62 @@ +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 + constructor functor + 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 = functor (λ x → x) (λ x → x) (refl) (refl) From 26d449771ac563b0a3e59c1de879c632d65cff33 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Mon, 15 Jan 2018 16:13:23 +0100 Subject: [PATCH 14/19] Unfinished stuff about HOM-sets and exponentials --- src/Cat/Categories/Sets.agda | 40 ++++++++++++++++++++++++++------ src/Cat/Category/Properties.agda | 23 ++++++++++++++++++ src/Cat/Functor.agda | 8 +++++-- 3 files changed, 62 insertions(+), 9 deletions(-) create mode 100644 src/Cat/Category/Properties.agda diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index fb2c332..b8584bc 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -1,8 +1,14 @@ -module Category.Sets where +{-# OPTIONS --allow-unsolved-metas #-} + +module Cat.Categories.Sets where open import Cubical.PathPrelude open import Agda.Primitive -open import Category +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. @@ -27,8 +33,28 @@ module _ {ℓ ℓ' : Level} {ℂ : Category {ℓ} {ℓ}} where RepFunctor : Functor ℂ Sets RepFunctor = record - { F = λ A → (B : C-Obj) → Hom {ℂ = ℂ} A B - ; f = λ { {c' = c'} f g → {!HomFromArrow {ℂ = } c' g!}} - ; ident = {!!} - ; distrib = {!!} - } + { func* = λ A → (B : C-Obj) → Hom {ℂ = ℂ} A B + ; func→ = λ { {c} {c'} f g → {!HomFromArrow {ℂ = {!!}} c' g!} } + ; ident = {!!} + ; distrib = {!!} + } + +Hom0 : {ℓ ℓ' : Level} → {ℂ : Category {ℓ} {ℓ'}} → Category.Object ℂ → Functor ℂ (Sets {ℓ'}) +Hom0 {ℂ = ℂ} 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 ℂ + +Hom1 : {ℓ ℓ' : Level} → {ℂ : Category {ℓ} {ℓ'}} → Category.Object ℂ → Functor (Opposite ℂ) (Sets {ℓ'}) +Hom1 {ℂ = ℂ} B = record + { func* = λ A → ℂ.Arrow A B + ; func→ = λ f g → {!!} ℂ.⊕ {!!} + ; ident = {!!} + ; distrib = {!!} + } + where + open module ℂ = Category ℂ 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/Functor.agda b/src/Cat/Functor.agda index 7f9e2af..4daaef3 100644 --- a/src/Cat/Functor.agda +++ b/src/Cat/Functor.agda @@ -8,7 +8,6 @@ open import Cat.Category record Functor {ℓc ℓc' ℓd ℓd'} (C : Category {ℓc} {ℓc'}) (D : Category {ℓd} {ℓd'}) : Set (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') where - constructor functor private open module C = Category C open module D = Category D @@ -59,4 +58,9 @@ module _ {ℓ ℓ' : Level} {A B C : Category {ℓ} {ℓ'}} (F : Functor B C) (G -- The identity functor identity : {ℓ ℓ' : Level} → {C : Category {ℓ} {ℓ'}} → Functor C C -- Identity = record { F* = λ x → x ; F→ = λ x → x ; ident = refl ; distrib = refl } -identity = functor (λ x → x) (λ x → x) (refl) (refl) +identity = record + { func* = λ x → x + ; func→ = λ x → x + ; ident = refl + ; distrib = refl + } From 69adb726de548202a2daf30a562cd7adabffa5fb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Mon, 15 Jan 2018 16:20:14 +0100 Subject: [PATCH 15/19] Fix typos as spotted by HUghes --- proposal/macros.tex | 2 +- proposal/proposal.tex | 16 ++++++++-------- 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/proposal/macros.tex b/proposal/macros.tex index abf3d42..90d7382 100644 --- a/proposal/macros.tex +++ b/proposal/macros.tex @@ -1,4 +1,4 @@ -\newcommand*{\defeq}{\mathrel{\vcenter{\baselineskip0.5ex \lineskiplimit0pt +\newcommand{\coloneqq}{\mathrel{\vcenter{\baselineskip0.5ex \lineskiplimit0pt \hbox{\scriptsize.}\hbox{\scriptsize.}}}% =} diff --git a/proposal/proposal.tex b/proposal/proposal.tex index 74a1835..679856c 100644 --- a/proposal/proposal.tex +++ b/proposal/proposal.tex @@ -60,7 +60,7 @@ parts that will be useful in the second part of the project: Showing that \section{Problem} % In the following two subsections I present two examples that illustrate the -limitaiton inherent in ITT and by extension to the expressiveness of Agda. +limitation inherent in ITT and by extension to the expressiveness of Agda. % \subsection{Functional extensionality} Consider the functions: @@ -71,7 +71,7 @@ $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{defnitional +$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: @@ -97,7 +97,7 @@ 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 +\nomen{pointwise equality}, where the \emph{points} of a function refers to it's arguments. % \iffalse @@ -142,7 +142,7 @@ $$(A \cong B) \cong (A \equiv B)$$ % \subsection{Formalizing Category Theory} % -The above examples serves to illustrate the limitation of Agda. One case where +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 @@ -157,17 +157,17 @@ 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 consists of mapping `things' from the +\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 device a CwF for Cubical Type Theory. This +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. In stead the translation will be accounted +the type theory and the meta-theory. Instead the translation will be accounted for informally. % \section{Context} @@ -195,7 +195,7 @@ 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$ -application of $\mathit{suc}$ to $0$ for some $n$; $e = \mathit{suc}^n\ 0$. +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. From 7090c2c6bf6825d00f8411258c7aacc87d22ef88 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Mon, 15 Jan 2018 17:56:08 +0100 Subject: [PATCH 16/19] Clarify some points about the project aim. --- proposal/macros.tex | 5 +++++ proposal/proposal.tex | 36 +++++++++++++++++++++++++++++++++--- 2 files changed, 38 insertions(+), 3 deletions(-) diff --git a/proposal/macros.tex b/proposal/macros.tex index 90d7382..604ae8b 100644 --- a/proposal/macros.tex +++ b/proposal/macros.tex @@ -4,6 +4,7 @@ \newcommand{\defeq}{\coloneqq} \newcommand{\bN}{\mathbb{N}} +\newcommand{\bC}{\mathbb{C}} \newcommand{\to}{\rightarrow}} \newcommand{\mto}{\mapsto}} \newcommand{\UU}{\ensuremath{\mathcal{U}}\xspace} @@ -12,3 +13,7 @@ \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 index 679856c..61be25a 100644 --- a/proposal/proposal.tex +++ b/proposal/proposal.tex @@ -99,6 +99,26 @@ 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: @@ -169,6 +189,15 @@ 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} % @@ -230,7 +259,7 @@ 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 that enjoys \nomen{Uniqueness of identity proofs} +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. @@ -240,8 +269,9 @@ 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. This is not -a goal for this thesis but rather a natural extension of it. +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. % From 902b953ad0232876c2a7c7de0c474e420047c3c2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Wed, 17 Jan 2018 12:10:18 +0100 Subject: [PATCH 17/19] Implement representable functors --- src/Cat/Categories/Sets.agda | 28 +++++++--------------------- src/Cat/Category.agda | 6 +++--- 2 files changed, 10 insertions(+), 24 deletions(-) diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index b8584bc..4e784b6 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -25,22 +25,8 @@ Sets {ℓ} = record ; ident = funExt (λ x → refl) , funExt (λ x → refl) } -module _ {ℓ ℓ' : Level} {ℂ : Category {ℓ} {ℓ}} where - private - C-Obj = Object ℂ - _+_ = Arrow ℂ - - RepFunctor : Functor ℂ Sets - RepFunctor = - record - { func* = λ A → (B : C-Obj) → Hom {ℂ = ℂ} A B - ; func→ = λ { {c} {c'} f g → {!HomFromArrow {ℂ = {!!}} c' g!} } - ; ident = {!!} - ; distrib = {!!} - } - -Hom0 : {ℓ ℓ' : Level} → {ℂ : Category {ℓ} {ℓ'}} → Category.Object ℂ → Functor ℂ (Sets {ℓ'}) -Hom0 {ℂ = ℂ} A = record +representable : {ℓ ℓ' : Level} → {ℂ : Category {ℓ} {ℓ'}} → Category.Object ℂ → Functor ℂ (Sets {ℓ'}) +representable {ℂ = ℂ} A = record { func* = λ B → ℂ.Arrow A B ; func→ = λ f g → f ℂ.⊕ g ; ident = funExt λ _ → snd ℂ.ident @@ -49,12 +35,12 @@ Hom0 {ℂ = ℂ} A = record where open module ℂ = Category ℂ -Hom1 : {ℓ ℓ' : Level} → {ℂ : Category {ℓ} {ℓ'}} → Category.Object ℂ → Functor (Opposite ℂ) (Sets {ℓ'}) -Hom1 {ℂ = ℂ} B = record +coRepresentable : {ℓ ℓ' : Level} → {ℂ : Category {ℓ} {ℓ'}} → Category.Object (Opposite ℂ) → Functor (Opposite ℂ) (Sets {ℓ'}) +coRepresentable {ℂ = ℂ} B = record { func* = λ A → ℂ.Arrow A B - ; func→ = λ f g → {!!} ℂ.⊕ {!!} - ; ident = {!!} - ; distrib = {!!} + ; func→ = λ f g → g ℂ.⊕ f + ; ident = funExt λ x → fst ℂ.ident + ; distrib = funExt λ x → ℂ.assoc } where open module ℂ = Category ℂ diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda index f508633..a30aee4 100644 --- a/src/Cat/Category.agda +++ b/src/Cat/Category.agda @@ -128,8 +128,8 @@ Opposite ℂ = where open module ℂ = Category ℂ -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 @@ -138,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 From acacfac31ced4b5856a7b90c495dafd8401e126c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Wed, 17 Jan 2018 12:16:07 +0100 Subject: [PATCH 18/19] Type-synonyms for Representable functors and Presheafs --- src/Cat/Categories/Sets.agda | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index 4e784b6..bd026dc 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -25,7 +25,10 @@ Sets {ℓ} = record ; ident = funExt (λ x → refl) , funExt (λ x → refl) } -representable : {ℓ ℓ' : Level} → {ℂ : Category {ℓ} {ℓ'}} → Category.Object ℂ → Functor ℂ (Sets {ℓ'}) +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 @@ -35,8 +38,11 @@ representable {ℂ = ℂ} A = record where open module ℂ = Category ℂ -coRepresentable : {ℓ ℓ' : Level} → {ℂ : Category {ℓ} {ℓ'}} → Category.Object (Opposite ℂ) → Functor (Opposite ℂ) (Sets {ℓ'}) -coRepresentable {ℂ = ℂ} B = record +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 From e98793a62049447a7a79dabf030aa5de9617c078 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Wed, 17 Jan 2018 12:19:04 +0100 Subject: [PATCH 19/19] Remove duplicate section for references --- proposal/proposal.tex | 2 -- 1 file changed, 2 deletions(-) diff --git a/proposal/proposal.tex b/proposal/proposal.tex index 61be25a..7237479 100644 --- a/proposal/proposal.tex +++ b/proposal/proposal.tex @@ -275,8 +275,6 @@ project. The thesis shall conclude with a discussion about the benefits of Cubical Agda. % -\section{References} -% \bibliographystyle{plainnat} \nocite{cubical-demo} \nocite{coquand-2013}