diff --git a/.gitattributes b/.gitattributes new file mode 100644 index 0000000..ed67cfc --- /dev/null +++ b/.gitattributes @@ -0,0 +1 @@ +*.lagda.md linguist-detectable=true \ No newline at end of file diff --git a/Makefile b/Makefile index cc9cd48..2c3c457 100644 --- a/Makefile +++ b/Makefile @@ -9,7 +9,7 @@ pandoc: public/*.md ) agda: Everything.agda - agda --html --html-dir=public index.lagda.md --html-highlight=auto -i. + agda --html --html-dir=public src/index.lagda.md --html-highlight=auto -i. rm -f public/Agda.css cp Agda.css public/Agda.css @@ -21,7 +21,7 @@ clean: # push compiled html to my cip directory push: all push' -# just push without building +# just push to CIP without rebuilding push': chmod +w public/Agda.css mv public bsc-thesis @@ -29,7 +29,7 @@ push': mv bsc-thesis public Everything.agda: - git ls-tree --full-tree -r --name-only HEAD | egrep '^src/[^\.]*.l?agda(\.md)?' | sed -e 's|^src/[/]*|import |' -e 's|/|.|g' -e 's/.agda//' -e '/import Everything/d' -e 's/..md//' | LC_COLLATE='C' sort > Everything.agda + git ls-tree --full-tree -r --name-only HEAD | egrep '^src/[^\.]*.l?agda(\.md)?' | grep -v 'index.lagda.md' | sed -e 's|^src/[/]*|import |' -e 's|/|.|g' -e 's/.agda//' -e '/import Everything/d' -e 's/..md//' | LC_COLLATE='C' sort > Everything.agda open: firefox public/index.html \ No newline at end of file diff --git a/src/Algebra/Elgot/Properties.lagda.md b/src/Misc/Algebra/Elgot/Properties.lagda.md similarity index 96% rename from src/Algebra/Elgot/Properties.lagda.md rename to src/Misc/Algebra/Elgot/Properties.lagda.md index 3bd934b..c265f53 100644 --- a/src/Algebra/Elgot/Properties.lagda.md +++ b/src/Misc/Algebra/Elgot/Properties.lagda.md @@ -13,13 +13,16 @@ open import Categories.Functor.Coalgebra ``` --> +## Note +This is currently removed, it would be needed for Theorem 35, 2⇒3 + ## Summary Some properties of elgot-algebras, namely: - Every elgot-algebra `(A, α : D₀ A ⇒ A)` satisfies `α (extend ι) ≈ α (D₁ π₁)` **[Lemma 32]** ```agda -module Algebra.Elgot.Properties {o ℓ e} (ambient : Ambient o ℓ e) where +module Misc.Algebra.Elgot.Properties {o ℓ e} (ambient : Ambient o ℓ e) where open Ambient ambient open import Monad.Instance.Delay ambient using (DelayM) open import Algebra.ElgotAlgebra ambient diff --git a/src/Monad/Core.lagda.md b/src/Misc/IsMonad.lagda.md similarity index 83% rename from src/Monad/Core.lagda.md rename to src/Misc/IsMonad.lagda.md index 726dd5d..d752e34 100644 --- a/src/Monad/Core.lagda.md +++ b/src/Misc/IsMonad.lagda.md @@ -11,8 +11,10 @@ open import Categories.NaturalTransformation # Monads In this file we define some predicates like 'F extends to a monad' +TODO: not needed without theorem 35 + ```agda -module Monad.Core {o ℓ e} (C : Category o ℓ e) where +module Misc.IsMonad {o ℓ e} (C : Category o ℓ e) where record ExtendsToMonad (F : Endofunctor C) : Set (o ⊔ ℓ ⊔ e) where field η : NaturalTransformation idF F diff --git a/src/Monad/Instance/K/PreElgot.lagda.md b/src/Misc/Kleene.lagda.md similarity index 99% rename from src/Monad/Instance/K/PreElgot.lagda.md rename to src/Misc/Kleene.lagda.md index 2f61ec3..8af4eb4 100644 --- a/src/Monad/Instance/K/PreElgot.lagda.md +++ b/src/Misc/Kleene.lagda.md @@ -1,5 +1,6 @@ +# Obsolete +This module contains some facts that are no longer needed, since Theorem 27 is not needed, namely: +- primitive recursion and induction for PNNO +- pre-order on a restriction category +- restrict operator ```agda -module Monad.Instance.K.PreElgot {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK.MonadK ambient) where +module Misc.Kleene {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK.MonadK ambient) where open Ambient ambient open import Monad.Instance.K.Strong ambient MK open import Monad.Instance.K.Commutative ambient MK diff --git a/src/Monad/Instance/Delay/Properties.lagda.md b/src/Misc/Monad/Instance/Delay/Properties.lagda.md similarity index 98% rename from src/Monad/Instance/Delay/Properties.lagda.md rename to src/Misc/Monad/Instance/Delay/Properties.lagda.md index ae73338..a5b1b27 100644 --- a/src/Monad/Instance/Delay/Properties.lagda.md +++ b/src/Misc/Monad/Instance/Delay/Properties.lagda.md @@ -17,7 +17,7 @@ open import Misc.FreeObject --> ```agda -module Monad.Instance.Delay.Properties {o ℓ e} (ambient : Ambient o ℓ e) where +module Misc.Monad.Instance.Delay.Properties {o ℓ e} (ambient : Ambient o ℓ e) where open Ambient ambient open import Categories.Diagram.Coequalizer C open import Monad.Instance.Delay ambient diff --git a/src/Monad/ElgotMonad.lagda.md b/src/Monad/ElgotMonad.lagda.md index 01b7aaa..fd37d0e 100644 --- a/src/Monad/ElgotMonad.lagda.md +++ b/src/Monad/ElgotMonad.lagda.md @@ -12,6 +12,8 @@ open import Categories.Functor ## Summary This file introduces Elgot Monads. +TODO: Probably only Pre-Elgot is needed + - [X] *Definition 13* Pre-Elgot Monads - [ ] *Definition 13* strong pre-Elgot - [X] *Definition 14* Elgot Monads diff --git a/src/Monad/Instance/K/Compositionality.lagda.md b/src/Monad/Instance/K/Compositionality.lagda.md new file mode 100644 index 0000000..771a00b --- /dev/null +++ b/src/Monad/Instance/K/Compositionality.lagda.md @@ -0,0 +1,5 @@ +# TODO: every KX satisfies compositionality + +```agda +module Monad.Instance.K.Compositionality where +``` \ No newline at end of file diff --git a/index.lagda.md b/src/index.lagda.md similarity index 100% rename from index.lagda.md rename to src/index.lagda.md diff --git a/src/thesis/motivation.agda b/src/thesis/motivation.agda deleted file mode 100644 index c6f15bf..0000000 --- a/src/thesis/motivation.agda +++ /dev/null @@ -1,75 +0,0 @@ -{-# OPTIONS --guardedness #-} - --- Take this example as motivation: --- https://stackoverflow.com/questions/21808186/agda-reading-a-line-of-standard-input-as-a-string-instead-of-a-costring - -open import Level -open import Agda.Builtin.Coinduction -module thesis.motivation where - -module old-delay where - private - variable - a : Level - data _⊥ (A : Set a) : Set a where - now : A → A ⊥ - later : ∞ (A ⊥) → A ⊥ - - never : ∀ {A : Set a} → A ⊥ - never = later (♯ never) - -module ReverseInput where - open import Data.Char - open import Data.Nat - open import Data.List using (List; []; _∷_) - open import Data.String - open import Data.Unit.Polymorphic - open import Codata.Musical.Costring - open import Codata.Musical.Colist using ([]; _∷_) - -- open import IO using (IO; seq; bind; return; Main; run; putStrLn) - open import IO.Primitive - open import IO.Primitive.Infinite using (getContents) - open import Agda.Builtin.IO using () - - open old-delay - -- IDEA: start in haskell, then motivate in agda and define delay type - -- next talk about bisimilarity. - -- idea for slide title: dlrowolleh.hs and dlrowolleh.agda - - private - variable - a : Level - - -- reverse : Costring → String ⊥ - -- reverse = go [] - -- where - -- go : List Char → Costring → String ⊥ - -- go acc [] = now (fromList acc) - -- go acc (x ∷ xs) = later (♯ go (x ∷ acc) (♭ xs)) - - -- putStrLn⊥ : String ⊥ → IO {a} ⊤ - -- putStrLn⊥ (now s) = putStrLn s - -- putStrLn⊥ (later s) = seq (♯ return tt) (♯ putStrLn⊥ (♭ s)) - - -- main : Main - -- main = run (bind (♯ {! getContents !}) {! !}) --(λ c → ♯ putStrLn⊥ (reverse c))) - --- NOTE: This is not very understandable... Better stick to the outdated syntax -module delay where - mutual - data _⊥ (A : Set) : Set where - now : A → A ⊥ - later : A ⊥' → A ⊥ - - record _⊥' (A : Set) : Set where - coinductive - field - force : A ⊥ - open _⊥' - - mutual - never : ∀ {A : Set} → A ⊥ - never = later never' - - never' : ∀ {A : Set} → A ⊥' - force never' = never