diff --git a/agda/src/Monad/Instance/Setoids/K.lagda.md b/agda/src/Monad/Instance/Setoids/K.lagda.md index 96a00e4..321af36 100644 --- a/agda/src/Monad/Instance/Setoids/K.lagda.md +++ b/agda/src/Monad/Instance/Setoids/K.lagda.md @@ -118,7 +118,7 @@ module Monad.Instance.Setoids.K {ℓ : Level} where helper'' rewrite eqx = ∼-refl (A ⊥ₛ ⊎ₛ Y) helper : (A ⊥ₛ ⊎ₛ Y) [ inj₂ (h ⟨$⟩ a) ∼ inj₁ c ] helper rewrite (≡-sym eqc) = ∼-trans (A ⊥ₛ ⊎ₛ Y) helper'' helper' - ... | inj₂ c = ≈-trans (later≈ {A} {_} {♯ (iter {A} {Y} (g ._⟨$⟩_)) (h ⟨$⟩ a)} (♯ (iter-uni {A} {X} {Y} {f} {g} {h} hf≈gh (∼-refl X)))) (later≈ (♯ iter-cong g (∼-sym Y helper))) + ... | inj₂ c = later≈ {! !} -- ≈-trans (later≈ {A} {_} {♯ (iter {A} {Y} (g ._⟨$⟩_)) (h ⟨$⟩ a)} (♯ (iter-uni {A} {X} {Y} {f} {g} {h} hf≈gh (∼-refl X)))) (later≈ (♯ iter-cong g (∼-sym Y helper))) -- why does this not terminate?? -- | inj₂ c = ≈-trans (later≈ {A} {_} {♯ (iter {A} {Y} (g ._⟨$⟩_)) (h ⟨$⟩ a)} (♯ (iter-uni {A} {X} {Y} {f} {g} {h} hf≈gh (∼-refl X)))) (later≈ (♯ iter-cong g (∼-sym Y helper))) where @@ -193,7 +193,7 @@ module Monad.Instance.Setoids.K {ℓ : Level} where delay-lift' : ∀ {A B : Set ℓ} → (A → B) → A ⊥ → B delay-lift' {A} {B} f (now x) = f x - delay-lift' {A} {B} f (later x) = {! !} + delay-lift' {A} {B} f (later x) = {! !} -- (id + f ∘ out)#b delay-lift : ∀ {A : Setoid ℓ ℓ} {B : Elgot-Algebra} → A ⟶ ⟦ B ⟧ → Elgot-Algebra-Morphism (delay-algebras A) B delay-lift {A} {B} f = record { h = record { _⟨$⟩_ = delay-lift' {∣ A ∣} {∣ ⟦ B ⟧ ∣} (f ._⟨$⟩_) ; cong = {! !} } ; preserves = {! !} } diff --git a/thesis/main.tex b/thesis/main.tex index 2c93d52..f170940 100644 --- a/thesis/main.tex +++ b/thesis/main.tex @@ -103,10 +103,11 @@ Erlangen, \today{} \rule{7cm}{1pt}\\ %%% - introduce notions in latex and later give agda code (maybe in appendix) %%% - introduce notions in agda directly (maybe unreadable, maybe duplication with appendix) \include{src/01_preliminaries} -\include{src/02_agda-categories} -\include{src/03_iteration} -\include{src/04_partiality-monads} -\include{src/05_monadK} +%\include{src/03_iteration} +%\include{src/04_partiality-monads} +\chapter{Modelling partiality} +% \include{src/05_monadK} +\chapter{Case Study: The Quotiented Delay Monad} \include{src/10_conclusion} \appendix diff --git a/thesis/src/01_preliminaries.tex b/thesis/src/01_preliminaries.tex index ad1112f..7a008a8 100644 --- a/thesis/src/01_preliminaries.tex +++ b/thesis/src/01_preliminaries.tex @@ -1,15 +1,30 @@ -\chapter{Preliminaries} +\chapter{Category Theory in Agda} + +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. + + +% TODO move We assume familiarity with basic concepts of category theory that should be taught in any introductory course, or can be looked up in~\cite{Lane1971}. In particular we will need the notions of category, functor, functor algebra, natural transformation, product and coproduct. -In the rest of this section we will look at other categorical notions that are either less well-known, or crucial for this thesis and therefore require special attention. - -% TODO add conventions i.e. \C for categories, how do products and coproducts look, etc. - -\section{Stable Natural Numbers Object} - -\section{Extensive and Distributive Categories} - \section{Monads} +% TODO do in Agda Monads are widely known among programmers as a way of modelling effects in pure languages. Categorically a Monad is a monoid in the category of endofunctors of a category, or in more accessible terms: \begin{definition}[Monad~\cite{Lane1971}] @@ -98,4 +113,8 @@ Now we can express the above condition: \[ \tau_{X,Y}^* \circ \hat{\tau}_{X, MY} = \hat{\tau}_{X,Y}^* \circ \tau_{X, MY} \] -\end{definition} \ No newline at end of file +\end{definition} + +\section{Stable Natural Numbers Object} + +\section{Extensive and Distributive Categories} \ No newline at end of file diff --git a/thesis/src/02_agda-categories.tex b/thesis/src/02_agda-categories.tex deleted file mode 100644 index 7f462ca..0000000 --- a/thesis/src/02_agda-categories.tex +++ /dev/null @@ -1,19 +0,0 @@ -\chapter{Formalizing Category Theory in Agda} -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.