Add CSS, small fixes, rewrite delay monad documentation

Literature.md

@@ -0,0 +1,5 @@
+# Literature
+1. *The* paper https://arxiv.org/pdf/2102.11828.pdf
+2. Delay Monad by Capretta https://arxiv.org/pdf/cs/0505037.pdf
+3. Altenkirch et al. show problems of the delay monad https://arxiv.org/pdf/1610.09254.pdf
+4. Chapman et al. agda formalization of the delay monad https://niccoloveltri.github.io/mscs_final.pdf

Makefile

@@ -5,11 +5,13 @@ all: agda
 
 pandoc: public/*.md
 	@$(foreach file,$^, \
-		pandoc $(file) -s -c Agda.css -o $(file:.md=.html) ; \
+		pandoc $(file) -s --to=html+TEX_MATH_DOLLARS --mathjax -c Agda.css -o $(file:.md=.html) ; \
 	)
 
 agda: Everything.agda
 	agda --html --html-dir=public Everything.agda --html-highlight=auto -i.
+	rm -f public/Agda.css
+	cp Agda.css public/Agda.css
 	mv public/Everything.html public/index.html
 
 clean:
@@ -17,9 +19,6 @@ clean:
 	rm -rf public/*
 	find . -name '*.agdai' -exec rm \{\} \;
 
-open:
-	firefox public/Everything.html
-
 # push compiled html to my cip directory
 push: all push'
 

src/Algebra/Elgot/Properties.lagda.md

@@ -1,5 +1,6 @@
 <!--
 ```agda
+{-# OPTIONS --allow-unsolved-metas #-}
 open import Level
 open import Category.Instance.AmbientCategory
 open import Categories.Functor
@@ -30,12 +31,5 @@ module Algebra.Elgot.Properties {o ℓ e} (ambient : Ambient o ℓ e) where
     commutes = {!   !}
       where
         α∘ι : α ∘ ι ≈ π₁
-        α∘ι = sym (begin 
+        α∘ι = {!   !}    
-          π₁ ≈⟨ unique {f = idC} {g = idC} (sym project₁) (sym project₁) ⟩ 
-          universal idC idC ≈⟨ {!   !} ⟩
-          {!   !} ≈⟨ {!   !} ⟩
-          universal {!   !} {!   !} ≈˘⟨ unique {!   !} {!   !} ⟩
-          α ∘ ι ∎)
-
-    
 ```

src/Algebra/Search.lagda.md

@@ -6,7 +6,7 @@ open import Categories.Functor.Algebra
 ```
 -->
 ## Summary
-A *D-Algebra* `(A, α : D₀ A ⇒ A)` is called a *search-algebra* if it satiesfies
+A *D-Algebra* `(A, α : D₀ A ⇒ A)` is called a *search-algebra* if it satisfies
 
 - α now ≈ id
 - α ▷ ≈ α

src/Category/Instance/AmbientCategory.lagda.md

@@ -20,6 +20,7 @@ import Categories.Morphism.Reasoning as MR'
 
 ## Summary
 We work in an ambient category that
+
 - is extensive (has finite coproducts and pullbacks along injections)
 - is cartesian (has finite products, extensive + cartesian also gives a distributivity isomorphism)
 - has a parametrized NNO ℕ

src/Monad/Instance/Delay.lagda.md

@@ -14,16 +14,21 @@ open import Categories.Category.Construction.F-Coalgebras
 open import Category.Instance.AmbientCategory using (Ambient)
 ```
 -->
-
-## Summary
-This file introduces the delay monad ***D***
-
-## Code
-
 ```agda
 module Monad.Instance.Delay {o ℓ e} (ambient : Ambient o ℓ e) where
   open Ambient ambient
 ```
+
+## Definition
+
+The delay monad is usually defined as a coinductive type with two constructors `now : X → D X` and `later : D X → D X`, e.g. in the [agda-stdlib](https://agda.github.io/agda-stdlib/Effect.Monad.Partiality.html#1523)
+
+We will now define it categorically by existence of final coalgebras for the functor `(X + -)` where `X` is some object. 
+This functor trivially sends objects `Y` to `X + Y` and functions `f` to `id + f`.
+
+In this definition `D X` is the underlying object of the final coalgebra given by `X`. 
+We then use Lambek's Lemma to gain an isomorphism `D X ≅ X + D X`, whose inverse can be factored into the constructors `now` and `later`.
+
 <!--
 ```agda
   open import Categories.Object.NaturalNumbers.Properties.F-Algebras using (PNNO⇒Initial₂; PNNO-Algebra)
@@ -38,22 +43,10 @@ module Monad.Instance.Delay {o ℓ e} (ambient : Ambient o ℓ e) where
 ```
 -->
 
-The Delay monad is usually described by existence of final coalgebras for the functor `(X + -)` where `X` is some arbitrary object.
-This functor trivially sends objects `Y` to `X + Y` and functions `f` to `id + f`.
-
 ```agda
   record DelayM : Set (o ⊔ ℓ ⊔ e) where
     field
       coalgebras : ∀ (A : Obj) → Terminal (F-Coalgebras (A +-))
-```
-
-These are all the fields this record needs! 
-Of course this doesn't tell us very much, so our goal will be to extract a monad from this definition.
-
-Conventionally the delay monad is described via functions `now` and `later` where the former lifts a value into a computation and the latter postpones a computation by one time unit.
-We can now define these functions by bisecting the isomorphism `out : DX ≅ X + DX` which we get by Lambek's lemma. (Here `DX` is the element of the final coalgebra for `X`)
-
-```agda
 
     module _ {X : Obj} where
       open Terminal (coalgebras X) using (⊤; !; !-unique)
@@ -79,9 +72,10 @@ We can now define these functions by bisecting the isomorphism `out : DX ≅ X +
 
 ```
 
-Since `Y ⇒ X + Y` is an algebra for the `(X + -)` functor, we can use our terminal coalgebras to get a *coiteration operator* `coit`:
+Since `Y ⇒ X + Y` is an algebra for the `(X + -)` functor, we can use the final coalgebras to get a *coiteration operator* `coit`:
 
-TODO add diagram
+<!-- https://q.uiver.app/#q=WzAsNCxbMCwwLCJZIl0sWzIsMCwiWCArIFkiXSxbMCwxLCJEWCJdLFsyLDEsIlggKyBEWCJdLFswLDEsImYiXSxbMCwyLCIhID06IGNvaXQgXFw7IGYiLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJkYXNoZWQifX19XSxbMiwzLCJvdXQiXSxbMSwzLCJGISIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dXQ== -->
+<iframe class="quiver-embed" src="https://q.uiver.app/#q=WzAsNCxbMCwwLCJZIl0sWzIsMCwiWCArIFkiXSxbMCwxLCJEWCJdLFsyLDEsIlggKyBEWCJdLFswLDEsImYiXSxbMCwyLCIhID06IGNvaXQgXFw7IGYiLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJkYXNoZWQifX19XSxbMiwzLCJvdXQiXSxbMSwzLCJGISIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dXQ==&embed" width="490" height="304" style="border-radius: 8px; border: none;"></iframe>
 
 ```agda
       module _ {Y : Obj} where 
@@ -92,31 +86,41 @@ TODO add diagram
         coit-commutes f = commutes (! {A = record { A = Y ; α = f }})
 ```
 
-If we combine the internal algebra structure of Parametrized NNOs with Lambek's lemma, we get the isomorphism `X × N ≅ X + X × N`.
+Furthermore if we combine the internal algebra structure of Parametrized NNOs with Lambek's lemma, we get the isomorphism `X × N ≅ X + X × N`.
 At the same time the morphism `X × N ⇒ X + X × N` is a coalgebra for the `(Y + \_)`-functor defined above, this gives us another morphism `ι : X × N ⇒ DX` by using the final coalgebras.
-TODO add diagram
 
+<!-- https://q.uiver.app/#q=WzAsNCxbMCwwLCJYIFxcdGltZXMgXFxtYXRoYmJ7Tn0iXSxbMiwwLCJYICsgKFggXFx0aW1lcyBcXG1hdGhiYntOfSkiXSxbMCwxLCJEIFgiXSxbMiwxLCJYICsgRCBYIl0sWzAsMSwi4omFIl0sWzAsMiwiISA9OiBcXGlvdGEiLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJkYXNoZWQifX19XSxbMiwzLCJvdXQiXSxbMSwzLCJGIFxcaW90YSIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dXQ== -->
+<iframe class="quiver-embed" src="https://q.uiver.app/#q=WzAsNCxbMCwwLCJYIFxcdGltZXMgXFxtYXRoYmJ7Tn0iXSxbMiwwLCJYICsgKFggXFx0aW1lcyBcXG1hdGhiYntOfSkiXSxbMCwxLCJEIFgiXSxbMiwxLCJYICsgRCBYIl0sWzAsMSwi4omFIl0sWzAsMiwiISA9OiBcXGlvdGEiLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJkYXNoZWQifX19XSxbMiwzLCJvdXQiXSxbMSwzLCJGIFxcaW90YSIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dXQ==&embed" width="575" height="304" style="border-radius: 8px; border: none;"></iframe>
 ```agda
-      iso : X × N ≅ X + X × N
+      nno-iso : X × N ≅ X + X × N
-      iso = Lambek.lambek (record { ⊥ = PNNO-Algebra cartesianCategory coproducts X N z s ; ⊥-is-initial = PNNO⇒Initial₂ cartesianCategory coproducts ℕ X })
+      nno-iso = Lambek.lambek (record { ⊥ = PNNO-Algebra cartesianCategory coproducts X N z s ; ⊥-is-initial = PNNO⇒Initial₂ cartesianCategory coproducts ℕ X })
 
       ι : X × N ⇒ DX
-      ι = u (! {A = record { A = X × N ; α = _≅_.from iso }})
+      ι = u (! {A = record { A = X × N ; α = _≅_.from nno-iso }})
 
 ```
-Make `DX` conveniently accessible
+
+## Delay is a monad
+
+The next step is showing that this actually yields a monad. Some parts for this are already given, we can construct `D X` from `X` and `now : D X ⇒ D X` is the monad unit.
+What's missing is Kleisli-lifting, given a morphism `f : X ⇒ D Y` we need to construct a morphism `extend f : D X ⇒ D Y`. 
+To do so we go from `D X` to `D X + D Y` via injection and then construct a coalgebra `D X + D Y ⇒ Y + (D X + D Y)`, the final coalgebra `D Y ⇒ Y + D Y` then yields a coalgebra-morphism from `D X + D Y` to `D Y`, see the following diagram:
+
+<!-- https://q.uiver.app/#q=WzAsNSxbMCwxLCJEWCArIERZIl0sWzIsMSwiWSArIChEWCArIERZKSJdLFswLDAsIkRYIl0sWzAsMiwiRFkiXSxbMiwyLCJZICsgRFkiXSxbMCwxLCJcXGFscGhhIl0sWzIsMCwiaV8xIl0sWzAsMywiISIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dLFszLDQsIm91dCJdLFsxLDQsIkYgISIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dXQ== -->
+<iframe class="quiver-embed" src="https://q.uiver.app/#q=WzAsNSxbMCwxLCJEWCArIERZIl0sWzIsMSwiWSArIChEWCArIERZKSJdLFswLDAsIkRYIl0sWzAsMiwiRFkiXSxbMiwyLCJZICsgRFkiXSxbMCwxLCJcXGFscGhhIl0sWzIsMCwiaV8xIl0sWzAsMywiISIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dLFszLDQsIm91dCJdLFsxLDQsIkYgISIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dXQ==&embed" width="551" height="304" style="border-radius: 8px; border: none;"></iframe>
+
+Proving the monad laws then requires two key lemmas, first of all that the following diagram commutes for any `f` (this is `extendlaw`)
+
+<!-- https://q.uiver.app/#q=WzAsNCxbMCwwLCJEWCJdLFszLDAsIkRZIl0sWzAsMSwiWCArIERYIl0sWzMsMSwiWSArIERZIl0sWzAsMSwiZXh0ZW5kXFw7ZiJdLFswLDIsIm91dCIsMl0sWzIsMywiW291dFxcO2YsaV8yXFw7KGV4dGVuZFxcO2YpXSIsMl0sWzEsMywib3V0Il1d -->
+<iframe class="quiver-embed" src="https://q.uiver.app/#q=WzAsNCxbMCwwLCJEWCJdLFszLDAsIkRZIl0sWzAsMSwiWCArIERYIl0sWzMsMSwiWSArIERZIl0sWzAsMSwiZXh0ZW5kXFw7ZiJdLFswLDIsIm91dCIsMl0sWzIsMywiW291dFxcO2YsaV8yXFw7KGV4dGVuZFxcO2YpXSIsMl0sWzEsMywib3V0Il1d&embed" width="670" height="304" style="border-radius: 8px; border: none;"></iframe>
+
+and second that `extend f` is the unique morphism satisfying the commutative diagram i.e. any other morphism for which the diagram commutes must be equivalent to `extend f` (this is `extend-unique`).
+
 ```agda
+    -- Make DX more accessible outside
     D₀ : Obj → Obj
     D₀ X = DX {X}
-```
 
-With these definitions at hand, we can now indeed construct a monad (in extension form) as the triple `(F₀, unit, extend)`.
-`F₀` corresponds to `D₀` of course and `unit` is `now`, the tricky part is kleisli lifting aka. `extend`.
-
-TODO
-
-
-```agda
     kleisli : KleisliTriple C
     kleisli = record
       { F₀ = D₀ 
@@ -277,11 +281,3 @@ TODO
     functor : Endofunctor C
     functor = Monad.F monad
 ```
-
-### Definition 30: Search-Algebras
-
-TODO
-
-### Proposition 31 : the category of uniform-iteration coalgebras coincides with the category of search-coalgebras
-
-TODO