diff --git a/.gitignore b/.gitignore index ee5aa9c..4d47fdc 100644 --- a/.gitignore +++ b/.gitignore @@ -3,4 +3,5 @@ *.log Everything.agda public/ -.direnv \ No newline at end of file +.direnv +.DS_Store diff --git a/src/Category/Instance/AmbientCategory.lagda.md b/src/Category/Instance/AmbientCategory.lagda.md index 98d1f83..f030136 100644 --- a/src/Category/Instance/AmbientCategory.lagda.md +++ b/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ˡ) ⟩ diff --git a/src/Monad/Instance/K/Commutative.lagda.md b/src/Monad/Instance/K/Commutative.lagda.md index 93ed533..e496038 100644 --- a/src/Monad/Instance/K/Commutative.lagda.md +++ b/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: @@ -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∘⁂)) ⟩ diff --git a/src/thesis/motivation.agda b/src/thesis/motivation.agda new file mode 100644 index 0000000..c6f15bf --- /dev/null +++ b/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