From c84818473238e0d759f96e22068f4d47dd218f0f Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Sun, 17 Dec 2023 20:08:26 +0100 Subject: [PATCH] minor --- .../Instance/Setoids/Delay/PreElgot.lagda.md | 14 +++++++++---- thesis/bib.bib | 9 +++++++- thesis/main.tex | 8 ++++++- thesis/src/01_preliminaries.tex | 2 +- thesis/src/02_agda-categories.tex | 21 ++++++++++++++++--- thesis/src/A1_contributions.tex | 2 +- 6 files changed, 45 insertions(+), 11 deletions(-) diff --git a/agda/src/Monad/Instance/Setoids/Delay/PreElgot.lagda.md b/agda/src/Monad/Instance/Setoids/Delay/PreElgot.lagda.md index a8acf51..8a8d607 100644 --- a/agda/src/Monad/Instance/Setoids/Delay/PreElgot.lagda.md +++ b/agda/src/Monad/Instance/Setoids/Delay/PreElgot.lagda.md @@ -3,7 +3,7 @@ {-# OPTIONS --allow-unsolved-metas --guardedness #-} open import Level open import Relation.Binary -open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_]) +open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_]; [_,_]′) open import Data.Sum.Function.Setoid open import Data.Sum.Relation.Binary.Pointwise open import Function.Equality as SΠ renaming (id to idₛ) @@ -186,9 +186,15 @@ module Monad.Instance.Setoids.Delay.PreElgot {ℓ : Level} where ; *-uniq = λ {B} f g g≋f {x} {y} x∼y → g≋f x∼y } where - -- TODO use fixpoint for this - *-preserves : ∀ {B : Elgot-Algebra} (f : delaySetoid A ⟶ Elgot-Algebra.A B) {X : Setoid ℓ ℓ} {g : X ⟶ (delaySetoid A) ⊎ₛ X} → ∀ {x y : Setoid.Carrier X} → X [ x ∼ y ] → Elgot-Algebra.A B [ (f ._⟨$⟩_ ∘′ iter {A} {X} (g ._⟨$⟩_)) x ∼ ((B Elgot-Algebra.#) _) ⟨$⟩ y ] - *-preserves {B} f {X} {g} {x} {y} x∼y = {! !} + -- TODO use fixpoint for this + *-preserves : ∀ {B : Elgot-Algebra} (f : delaySetoid A ⟶ Elgot-Algebra.A B) {X : Setoid ℓ ℓ} {g : X ⟶ (delaySetoid A) ⊎ₛ X} → ∀ {x y : Setoid.Carrier X} → X [ x ∼ y ] → Elgot-Algebra.A B [ (f ._⟨$⟩_ ∘′ iter {A} {X} (g ._⟨$⟩_)) x ∼ ((B Elgot-Algebra.#) _) ⟨$⟩ y ] + *-preserves {B} f {X} {g} {x} {y} x∼y = ∼-sym (Elgot-Algebra.A B) (∼-trans (Elgot-Algebra.A B) (#-Fixpoint (∼-sym X x∼y)) helper) + where + open Elgot-Algebra B using (#-Fixpoint) + helper : Elgot-Algebra.A B [ {! !} x ∼ (f ._⟨$⟩_ ∘′ iter {A} {X} (g ._⟨$⟩_)) x ] -- ([ (f ._⟨$⟩_) , _ ] ∘′ g ._⟨$⟩_) + helper with g ⟨$⟩ x in eqx + ... | inj₁ a = {! !} + ... | inj₂ b = {! !} -- TODO remove delayPreElgot : IsPreElgot delayMonad diff --git a/thesis/bib.bib b/thesis/bib.bib index 7a694fc..c8d1f55 100644 --- a/thesis/bib.bib +++ b/thesis/bib.bib @@ -1,4 +1,11 @@ -@inproceedings{10.1145/3437992.3439922, +@inproceedings{agda, + title = {Towards a practical programming language based on dependent type theory}, + author = {Ulf Norell}, + year = {2007}, + url = {https://api.semanticscholar.org/CorpusID:118357515} +} + +@inproceedings{agda-categories, author = {Hu, Jason Z. S. and Carette, Jacques}, title = {Formalizing Category Theory in Agda}, year = {2021}, diff --git a/thesis/main.tex b/thesis/main.tex index cfccf5f..2c93d52 100644 --- a/thesis/main.tex +++ b/thesis/main.tex @@ -17,13 +17,19 @@ \usepackage{graphicx} \usepackage[style=ieee, sorting=ynt]{biblatex} %advanced citations \usepackage[english=british]{csquotes} %biblatex recommended to load this -\usepackage{listings}[language = haskell] +\usepackage{listings} + [ + language=agda, + extendedchars=true, + inputencoding=utf8, + ] \usepackage{multicol} \addbibresource{bib.bib} %\usepackage[right]{showlabels} %\usepackage[justific=raggedright,totoc]{idxlayout} \usepackage[type=CC, modifier=by-sa,version=4.0]{doclicense} +\lstset{mathescape} \addto\extrasenglish{% \renewcommand{\chapterautorefname}{Section} diff --git a/thesis/src/01_preliminaries.tex b/thesis/src/01_preliminaries.tex index 0475c64..ad1112f 100644 --- a/thesis/src/01_preliminaries.tex +++ b/thesis/src/01_preliminaries.tex @@ -34,7 +34,7 @@ For programmers a second equivalent definition is more useful: \end{enumerate} \end{definition} -In functional languages like Haskell the Kleisli lifting is usually called \textit{bind} or written infix as \lstinline{>>=} and $\eta$ is called $return$. Given two morphisms $f : X \rightarrow MY, g : Y \rightarrow MZ$, where $M$ is a Kleisli triple the composition $g^* \circ f$ can then be (pointfully) written as \lstinline{f x >>= g} or using Haskell's do-notation: +In functional languages like Haskell the Kleisli lifting is usually called \textit{bind} or written infix as \lstinline{>>=} and $\eta$ is called $return$. Given two morphisms $f : X \rightarrow MY, g : Y \rightarrow MZ$, where $M$ is a Kleisli triple the composition $g^* \circ f$ can then be (in a pointful manner) written as \lstinline{f x >>= g} or using Haskell's do-notation: \begin{lstlisting} do y <- f x g y diff --git a/thesis/src/02_agda-categories.tex b/thesis/src/02_agda-categories.tex index c002f41..7f462ca 100644 --- a/thesis/src/02_agda-categories.tex +++ b/thesis/src/02_agda-categories.tex @@ -1,4 +1,19 @@ \chapter{Formalizing Category Theory in Agda} -% IDEAS: -%% - why agda? talk about other approaches i.e. HOTT, coq, ... -%% - show some basic definitions like category and functor \ No newline at end of file +There are many formalizations of category theory in proof assistants like Coq or Agda. The benefits are clear, having a usable formalization allows one to reason about categorical notions in a typechecked environment that makes errors less likely. +Also ideally such a development will bring researchers together and enable them to work in a unified setting. +In this thesis we will work with the dependently typed programming language Agda~\cite{agda} and the agda-categories~\cite{agda-categories} library by Jason Hu and Jacques Carette that gives us a good foundation of categorical definitions to work with. In this section we will talk about some design decisions that Hu and Carette made in their library that influence this development. + +\section{Setoid Enriched Categories} +The usual textbook definition of category hides some design decisions that have to be made when implementing it in type theory. One would usually see something like this: +\begin{definition}[Category] +A category consists of +\begin{itemize} + \item A collection of objects + \item A collection of morphisms between objects + \item For every two morphisms $f : X \rightarrow Y, g : Y \rightarrow Z$ another morphism $g \circ f : X \rightarrow Z$ called the composition + \item For every object $X$ a morphism $id_X : X \rightarrow X$ called the identity +\end{itemize} +where the composition is associative and the identity morphisms are identities with respect to the composition. +\end{definition} + +Here a \textit{collection} usually is something that behaves set-like, but prevents size issues (there is no collection of all collections, avoiding Russel's Paradox). Agda's type theory does not have these size problems, so one can use Agda's built-in infinite \lstinline|Set| hierarchy for the collections. One question that is still open is how to express equality between morphisms. A tempting possibility is the built-in propositional equality \lstinline|_$\equiv$_| ... but bla bla use setoid, give category definition in agda. diff --git a/thesis/src/A1_contributions.tex b/thesis/src/A1_contributions.tex index 9f03bcc..95761cc 100644 --- a/thesis/src/A1_contributions.tex +++ b/thesis/src/A1_contributions.tex @@ -4,7 +4,7 @@ Many basic definitions that were needed for the formalization of this thesis wer % TODO chapter formalizing category theory first \section{Kleisli Triple} - +% citation for relative monad: https://arxiv.org/abs/1412.7148 \section{Commutative Monad} \section{Distributive Categories} \section{Stable Natural Numbers Object} \ No newline at end of file