.gitignore

@@ -3,5 +3,4 @@
 *.log
 Everything.agda
 public/
-.direnv
-.DS_Store
+.direnv

src/Category/Instance/AmbientCategory.lagda.md

@@ -96,7 +96,6 @@ module Category.Instance.AmbientCategory where
     dstr-law₃ = (refl⟩∘⟨ (sym inject₁)) ○ (cancelˡ (IsIso.isoˡ isIsoʳ))
     dstr-law₄ : ∀ {A B C} → distributeʳ⁻¹ {A} {B} {C} ∘ (i₂ ⁂ idC) ≈ i₂
     dstr-law₄ = (refl⟩∘⟨ (sym inject₂)) ○ (cancelˡ (IsIso.isoˡ isIsoʳ))
-    -- TODO this is double...
     dstr-law₅ : ∀ {A B C} → (π₂ +₁ π₂) ∘ distributeˡ⁻¹ {A} {B} {C} ≈ π₂
     dstr-law₅ = Iso⇒Epi C (IsIso.iso isIsoˡ) ((π₂ +₁ π₂) ∘ distributeˡ⁻¹) π₂ (begin 
       (((π₂ +₁ π₂) ∘ distributeˡ⁻¹) ∘ distributeˡ) ≈⟨ cancelʳ (IsIso.isoˡ isIsoˡ) ⟩ 

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

@@ -27,7 +27,7 @@ module Monad.Instance.K.Commutative {o ℓ e} (ambient : Ambient o ℓ e) (MK :
 ```
 
 # K is a commutative monad
-The proof is analogous to the ones for strength, the relevant diagram is:
+The proof is analogous to the ones for strength, this is the relevant diagram is:
 
 <!-- https://q.uiver.app/#q=WzAsNyxbMCwxLCJLWCBcXHRpbWVzIEtZIl0sWzEsMCwiSyhLWCBcXHRpbWVzIFkpIl0sWzIsMCwiSyhLKFggXFx0aW1lcyBZKSkiXSxbMywxLCJLKFggXFx0aW1lcyBZKSJdLFsxLDIsIksoWCBcXHRpbWVzIEtZKSJdLFsyLDIsIksoSyhYIFxcdGltZXMgWSkpIl0sWzAsNCwiS1ggXFx0aW1lcyBZIl0sWzAsMSwiXFx0YXUiXSxbMSwyLCJLXFxoYXR7XFx0YXV9Il0sWzIsMywiXFxtdSJdLFswLDQsIlxcaGF0e1xcdGF1fSIsMl0sWzQsNSwiS1xcdGF1IiwyXSxbNSwzLCJcXG11IiwyXSxbNiwwLCJpZCBcXHRpbWVzIFxcZXRhIl0sWzYsMywiXFxoYXR7XFx0YXV9IiwwLHsiY3VydmUiOjV9XSxbMCwzLCJcXGhhdHtcXHRhdX1eXFwjIl1d -->
 <iframe class="quiver-embed" src="https://q.uiver.app/#q=WzAsNyxbMCwxLCJLWCBcXHRpbWVzIEtZIl0sWzEsMCwiSyhLWCBcXHRpbWVzIFkpIl0sWzIsMCwiSyhLKFggXFx0aW1lcyBZKSkiXSxbMywxLCJLKFggXFx0aW1lcyBZKSJdLFsxLDIsIksoWCBcXHRpbWVzIEtZKSJdLFsyLDIsIksoSyhYIFxcdGltZXMgWSkpIl0sWzAsNCwiS1ggXFx0aW1lcyBZIl0sWzAsMSwiXFx0YXUiXSxbMSwyLCJLXFxoYXR7XFx0YXV9Il0sWzIsMywiXFxtdSJdLFswLDQsIlxcaGF0e1xcdGF1fSIsMl0sWzQsNSwiS1xcdGF1IiwyXSxbNSwzLCJcXG11IiwyXSxbNiwwLCJpZCBcXHRpbWVzIFxcZXRhIl0sWzYsMywiXFxoYXR7XFx0YXV9IiwwLHsiY3VydmUiOjV9XSxbMCwzLCJcXGhhdHtcXHRhdX1eXFwjIl1d&embed" width="974" height="688" style="border-radius: 8px; border: none;"></iframe>
@@ -57,13 +57,10 @@ The proof is analogous to the ones for strength, the relevant diagram is:
       ≈ ((K.₁ swap +₁ τ) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∘ swap
       -}
       σ-preserve {Z} h = {!   !}
-      σ-preserve' : ∀ {X Y Z : Obj} (h : Z ⇒ K.₀ Y + Z) → σ (X , K.₀ Y) ∘ (idC ⁂ h #) ≈ ((σ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))#
-      σ-preserve' {Z} h = {!   !}
       commutes' : ∀ {X Y : Obj} → μ.η _ ∘ K.₁ (σ _) ∘ τ (K.₀ X , Y) ≈ μ.η _ ∘ K.₁ (τ _) ∘ σ _
       commutes' {X} {Y} = begin 
         μ.η _ ∘ K.₁ (σ _) ∘ τ _ ≈⟨ ♯-unique (stable _) (σ _) (μ.η (X × Y) ∘ K.₁ (σ _) ∘ τ _) comm₁ comm₂ ⟩ 
-        (σ _) ♯ ≈⟨ sym (♯-unique (stable _) (σ _) (μ.η _ ∘ K.₁ (τ _) ∘ σ _) comm₃ comm₄) ⟩
-        {!   !} ≈⟨ {!   !} ⟩
+        (σ _) ♯ ≈⟨ sym (♯-unique (stable _) (σ _) (μ.η _ ∘ K.₁ (τ _) ∘ σ _) comm₃ comm₄) ⟩ 
         μ.η _ ∘ K.₁ (τ _) ∘ σ _ ∎
         where
           comm₁ : σ _ ≈ (μ.η _ ∘ K.₁ (σ _) ∘ τ _) ∘ (idC ⁂ η _)
@@ -97,22 +94,25 @@ The proof is analogous to the ones for strength, the relevant diagram is:
           comm₄ : ∀ {Z : Obj} (h : Z ⇒ K.₀ Y + Z) → (μ.η _ ∘ K.₁ (τ _) ∘ σ _) ∘ (idC ⁂ h #) ≈ ((μ.η _ ∘ K.₁ (τ _) ∘ σ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))#
           comm₄ {Z} h = begin 
             (μ.η _ ∘ K.₁ (τ _) ∘ σ _) ∘ (idC ⁂ h #) ≈⟨ {!   !} ⟩ 
-            (μ.η _ ∘ K.₁ (τ _) ∘ σ _) ∘ ((i₁ # ∘ idC) ⁂ h #) ≈˘⟨ {!   !} ⟩
-            (μ.η _ ∘ K.₁ (τ _) ∘ σ _) ∘ (((i₁ #) ⁂ h #)) ≈˘⟨ refl⟩∘⟨ ⟨⟩-cong₂ (#-Uniformity (algebras _) helper₁) {!   !} ⟩
-            (μ.η _ ∘ K.₁ (τ _) ∘ σ _) ∘ ⟨ ((π₁ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # , ((π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ⟩ ≈⟨ {!   !} ⟩
+            μ.η (X × Y) ∘ K.₁ (τ _) ∘ K.₁ swap ∘ τ _ ∘ (h # ⁂ idC) ∘ swap ≈⟨ {!   !} ⟩ 
+            μ.η _ ∘ K.₁ (τ _) ∘ K.₁ swap ∘ τ _ ∘ (h # ⁂ K.₁ idC) ∘ swap ≈⟨ {!   !} ⟩ 
+            μ.η _ ∘ K.₁ (τ _) ∘ K.₁ swap ∘ K.₁ (h # ⁂ idC) ∘ τ _ ∘ swap ≈⟨ {!   !} ⟩ 
+            μ.η _ ∘ K.₁ (τ _) ∘ K.₁ (swap ∘ (h # ⁂ idC)) ∘ τ _ ∘ swap ≈⟨ {!   !} ⟩ 
+            μ.η _ ∘ K.₁ (τ _) ∘ K.₁ ((idC ⁂ h #) ∘ swap) ∘ τ _ ∘ swap ≈⟨ {!   !} ⟩ 
+            μ.η _ ∘ K.₁ (τ _) ∘ (K.₁ (idC ⁂ h #) ∘ K.₁ swap) ∘ τ _ ∘ swap ≈⟨ {!   !} ⟩ 
+            μ.η _ ∘ (K.₁ (τ _ ∘ (idC ⁂ h #)) ∘ K.₁ swap) ∘ τ _ ∘ swap ≈⟨ {!   !} ⟩ 
+            μ.η _ ∘ (K.₁ (((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #) ∘ K.₁ swap) ∘ τ _ ∘ swap ≈⟨ {!   !} ⟩ 
+            μ.η _ ∘ K.₁ (((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #) ∘ σ _ ≈⟨ {!   !} ⟩ 
             {!   !} ≈⟨ {!   !} ⟩
             {!   !} ≈⟨ {!   !} ⟩
             {!   !} ≈⟨ {!   !} ⟩
+            {!   !} ≈⟨ {!   !} ⟩
+            μ.η (X × Y) ∘ K.₁ (τ _) ∘ K.₁ swap ∘ ((τ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) # ∘ swap ≈⟨ {!   !} ⟩ 
+            μ.η _ ∘ K.₁ (τ _) ∘ K.₁ swap ∘ ((τ _ ∘ swap +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ≈⟨ {!   !} ⟩ 
+            μ.η _ ∘ K.₁ (τ _) ∘ ((σ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ≈⟨ {!   !} ⟩ 
+            μ.η _ ∘ ((K.₁ (τ _) ∘ σ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ≈⟨ {!   !} ⟩ 
             ((μ.η _ ∘ K.₁ (τ _) ∘ σ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∎
             where
-              -- this leads nowhere
-              helper₁ : (idC +₁ π₁) ∘ (π₁ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈ i₁ ∘ π₁
-              helper₁ = begin 
-                (idC +₁ π₁) ∘ (π₁ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ) ⟩ 
-                (π₁ +₁ π₁) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ {!   !} ⟩ 
-                i₁ ∘ π₁ ∘ (idC ⁂ h) ≈⟨ refl⟩∘⟨ π₁∘⁂ ⟩ 
-                i₁ ∘ idC ∘ π₁ ≈⟨ refl⟩∘⟨ identityˡ ⟩ 
-                i₁ ∘ π₁ ∎
               test : ((τ (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∘ swap ≈ ((τ (X , Y) ∘ swap +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) #
               test = sym (#-Uniformity (algebras _) (sym (begin 
                 ((τ (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ∘ swap ≈⟨ pullʳ (pullʳ (sym swap∘⁂)) ⟩ 

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