Merge branch 'main' of git8.cs.fau.de:theses/bsc-leon-vatthauer

.gitignore

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

src/Category/Instance/AmbientCategory.lagda.md

@@ -96,6 +96,7 @@ 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

@@ -28,7 +28,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, this is the relevant diagram is:
+The proof is analogous to the ones for strength, 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>
@@ -58,10 +58,13 @@ The proof is analogous to the ones for strength, this is 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 ⁂ η _)
@@ -95,25 +98,22 @@ The proof is analogous to the ones for strength, this is 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 #) ≈⟨ {!   !} ⟩ 
-            μ.η (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)) #) ∘ σ _ ≈⟨ {!   !} ⟩ 
+            (μ.η _ ∘ 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 ∘ ((τ _ +₁ 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

@@ -0,0 +1,75 @@
+{-# 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