🎨 moved unused files to /src/Misc

.gitattributes

@@ -0,0 +1 @@
+*.lagda.md linguist-detectable=true

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

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

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

src/Misc/Kleene.lagda.md

@@ -1,5 +1,6 @@
 <!--
 ```agda
+{-# OPTIONS --allow-unsolved-metas #-}
 open import Level
 open import Data.Product using (_,_)
 open import Category.Instance.AmbientCategory
@@ -13,10 +14,15 @@ import Monad.Instance.K as MIK
 ```
 -->
 
+# 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

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

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

src/Monad/Instance/K/Compositionality.lagda.md

@@ -0,0 +1,5 @@
+# TODO: every KX satisfies compositionality
+
+```agda
+module Monad.Instance.K.Compositionality where
+```

src/thesis/motivation.agda

@@ -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