From 4d24b1d0e5a975c68dd39e884c67c17c4a9c679d Mon Sep 17 00:00:00 2001
From: Leon Vatthauer <leon.vatthauer@fau.de>
Date: Fri, 22 Dec 2023 19:41:00 +0100
Subject: [PATCH] minor comments (+ fix makefile)

---
 agda/Makefile                              | 2 +-
 agda/src/Monad/Instance/Setoids/K.lagda.md | 9 ++-------
 2 files changed, 3 insertions(+), 8 deletions(-)

diff --git a/agda/Makefile b/agda/Makefile
index 3a1a28f..1b8386c 100644
--- a/agda/Makefile
+++ b/agda/Makefile
@@ -27,7 +27,7 @@ push: all
 
 Everything.agda:
 	echo "{-# OPTIONS --guardedness #-}" > src/Everything.agda
-	git ls-tree --full-tree -r --name-only HEAD | egrep '^src/[^\.]*.l?agda(\.md)?' | grep -v 'index.lagda.md' | grep -v 'bsc.agda-lib' | sed -e 's|^src/[/]*|import |' -e 's|/|.|g' -e 's/.agda//' -e '/import Everything/d' -e 's/..md//' | LC_COLLATE='C' sort >> src/Everything.agda
+	git ls-files | egrep '^src/[^\.]*.l?agda(\.md)?' | grep -v 'index.lagda.md' | grep -v 'bsc.agda-lib' | sed -e 's|^src/[/]*|import |' -e 's|/|.|g' -e 's/.agda//' -e '/import Everything/d' -e 's/..md//' | LC_COLLATE='C' sort >> src/Everything.agda
 	
 
 open:
diff --git a/agda/src/Monad/Instance/Setoids/K.lagda.md b/agda/src/Monad/Instance/Setoids/K.lagda.md
index 22c3cbc..fd1876b 100644
--- a/agda/src/Monad/Instance/Setoids/K.lagda.md
+++ b/agda/src/Monad/Instance/Setoids/K.lagda.md
@@ -34,9 +34,6 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
   open Setoid using () renaming (Carrier to ∣_∣; _≈_ to [_][_≡_])
   open eq using () renaming (refl to ≡-refl; sym to ≡-sym; trans to ≡-trans)
 
-  ≡to≡ : ∀ {A : Setoid ℓ ℓ} {a b : ∣ A ∣} → a ≡ b → [ A ][ a ≡ b ]
-  ≡to≡ {A} a≡b rewrite a≡b = ≡-refl A
-
   conflict : ∀ {ℓ''} (X Y : Setoid ℓ ℓ) {Z : Set ℓ''}
     {x : ∣ X ∣} {y : ∣ Y ∣} → [ X ⊎ₛ Y ][ inj₁ x ≡ inj₂ y ] → Z
   conflict X Y ()
@@ -219,18 +216,16 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
       out-cong {later x} {now y} x≡y = {!   !}
       out-cong {later x} {later y} x≡y = {!   !}
 
-  lift'' : ∀ {A B : Set ℓ} → (∀ (C : Set ℓ) → (A ⊥ → B ⊎ A ⊥) → A ⊥ → B) → (A → B) → A ⊥ → B
-  lift'' {A} {B} [_]_# f = [ B ] (λ { (now x) → inj₁ (f x) ; (later x) → inj₂ (later (♯ {!   !})) }) #
-
   delay-lift : ∀ {A : Setoid ℓ ℓ} {B : Elgot-Algebra} → A ⟶ ⟦ B ⟧ → Elgot-Algebra-Morphism (delay-algebras A) B
   delay-lift {A} {B} f = record { h = (B Elgot-Algebra.#) helper ; preserves = {!   !} }
     where
+    -- this definition of helper₁ corresponds to `(f + id) ∘ out`, but using the representation of _⊥ as a positive coinductive type
     helper₁ : ∣ A ∣ ⊥ → ∣ ⟦ B ⟧ ∣ ⊎ ∣ A ∣ ⊥
     helper₁ (now x) = inj₁ (< f > x)
     helper₁ (later x) = inj₂ (♭ x)
     helper₁-cong : ∀ {x y : ∣ A ∣ ⊥} → [ A ][ x ≈ y ] → [ ⟦ B ⟧ ⊎ₛ A ⊥ₛ ][ helper₁ x ≡ helper₁ y ]
     helper₁-cong {now x} {now y} x≈y = {!   !} -- yes
-    helper₁-cong {now x} {later y} x≈y = {!   !}
+    helper₁-cong {now x} {later y} x≈y = {!   !} -- problematic, need to show inj₁ (f x) ≈ inj₂ y, which is contradictory, while the assumption now x ≈ later y is not contradictory.
     helper₁-cong {later x} {now y} (↓≈ a≡b (later↓ x↓a) (now↓ y≡b)) = {!   !}
     helper₁-cong {later x} {later y} (later≈ x≈y) = {!   !} -- cong inj₂ₛ (♭ x≈y)
     helper₁-cong {later x} {later y} (↓≈ a≡b (later↓ x↓a) (later↓ y↓b)) = {!   !} --cong inj₂ₛ (↓≈ a≡b x↓a y↓b)