agda/shell.nix

@@ -14,12 +14,12 @@ mkShell {
       }))
       (agdaPackages.agda-categories.overrideAttrs (oldAttrs : {
         version = "0.2.0";
-         src = fetchFromGitHub {
-           repo = "agda-categories";
-           owner = "agda";
-           rev = "944a487b92ab3a9d3b3ee54d209cd7ea95dc58ed";
-           hash = "sha256-G5QgEMj6U+5s3o7HUfORn+Y3gQA9KvpUuAvHAXn7TKk=";
-         };
+        src = fetchFromGitHub {
+          repo = "agda-categories";
+          owner = "agda";
+          rev = "a1c797e935432702d25fd729802aeb155b423761";
+          hash = "sha256-p9rrQq3aFSG14sJ65aYDvAoPkTsa/UmdkkxD5suhClY="; # sha256-GQuQxzYSQxAIVSJ1vf0blRC0juoxAqD1AHW66H/6NSk=
+        };
 
         # without this nix might use a wrong version of the stdlib to try and typecheck agda-categories
         buildInputs = [

agda/src/Monad/Instance/Setoids/K.lagda.md

@@ -178,7 +178,7 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
   delay-algebras : ∀ (A : Setoid ℓ ℓ) → Elgot-Algebra
   delay-algebras A = record { A = Delayₛ A ; algebra = delay-algebras-on {A}}
 
-  open Elgot-Algebra using (#-Fixpoint; #-Uniformity; #-Compositionality; #-resp-≈; #-Diamond) renaming (A to ⟦_⟧)
+  open Elgot-Algebra using (#-Fixpoint; #-Uniformity; #-resp-≈; #-Diamond) renaming (A to ⟦_⟧)
 
 
   delay-lift : ∀ {A : Setoid ℓ ℓ} {B : Elgot-Algebra} → A ⟶ ⟦ B ⟧ → Elgot-Algebra-Morphism (delay-algebras A) B
@@ -255,7 +255,7 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
                     (#-resp-≈ B {Delayₛ∼ (A ×ₛ ℕ-setoid)} {helper'} step₁)
                     (≡-trans ⟦ B ⟧
                       (#-Diamond B {Delayₛ∼ (A ×ₛ ℕ-setoid)} helper''') 
-                      (#-resp-≈ B (λ {x} → (step₂ {x}))))
+                      (#-resp-≈ B (λ {x} → (≡-trans (⟦ B ⟧ ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid)) (stepid {x}) (step₂ {x})))))
           where
             helper₁''' : Delay (∣ A ∣ × ℕ {ℓ}) → ∣ ⟦ B ⟧ ∣ ⊎ (Delay (∣ A ∣ × ℕ {ℓ}) ⊎ Delay (∣ A ∣ × ℕ {ℓ}))
             helper₁''' (now (x , zero))  = inj₁ (< f > x)
@@ -284,6 +284,12 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
                 by-induction (suc n) = ≡-trans ⟦ B ⟧ (#-Fixpoint B) (by-induction n)
             step₂ {later y} = ≡-refl (⟦ B ⟧ ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid))
 
+            -- this step should not be needed, the problem is the hole in its type, if we try to write down the type that should go into the hole, agda will reject it above.
+            stepid : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid) ][ ([ inj₁ , [ inj₁ ∘′ _ , inj₂ ] ] ∘′ helper₁''') x ≡ ([ inj₁ , [ inj₁ ∘′ < ([ inj₁ₛ , inj₂ₛ ∘ [ idₛ (Delayₛ∼ (A ×ₛ ℕ-setoid)) , idₛ (Delayₛ∼ (A ×ₛ ℕ-setoid)) ]ₛ ]ₛ ∘ helper''') # > , inj₂ ] ] ∘′ helper₁''') x ]
+            stepid {now (x , zero)} = ≡-refl (⟦ B ⟧ ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid))
+            stepid {now (x , suc n)} = inj₁ (#-resp-≈ B (≡-refl (⟦ B ⟧ ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid))))
+            stepid {later x} = ≡-refl (⟦ B ⟧ ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid))
+
         eq₁ : ∀ {z} → [ ⟦ B ⟧ ][ helper'' # ⟨$⟩ z ≡ helper # ⟨$⟩ liftF proj₁ z ]
         eq₁ {z} = #-Uniformity B {f = helper''} {g = helper} {h = liftFₛ∼ proj₁ₛ} by-uni
           where
@@ -304,41 +310,18 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
 
     delay-lift' = record { to = < helper # > ; cong = helper#≈-cong }
 
-    -- discretize a setoid
-    ‖_‖ : Setoid ℓ ℓ → Setoid ℓ ℓ
-    ∣_∣ ‖ X ‖      = ∣ X ∣
-    [_][_≡_] ‖ X ‖ = _≡_
-    Setoid.isEquivalence ‖ X ‖ = Eq.isEquivalence
-
-    ‖‖-quote : ∀ {X : Setoid ℓ ℓ} → ‖ X ‖ ⟶ X
-    _⟶_.to ‖‖-quote x          = x
-    cong (‖‖-quote {X}) ≣-refl = ≡-refl X
-
-    disc-dom : ∀ {X : Setoid ℓ ℓ} → X ⟶ (Delayₛ A ⊎ₛ X) → ‖ X ‖ ⟶ (Delayₛ∼ A ⊎ₛ ‖ X ‖)
-    _⟶_.to (disc-dom f) x = f ⟨$⟩ x
-    cong (disc-dom {X} f) {x} {y} x≡y rewrite x≡y = ≡-refl (Delayₛ∼ A ⊎ₛ ‖ X ‖) 
-
-    iter-g-var : ∀ {X : Setoid ℓ ℓ} → (g : X ⟶ (Delayₛ A ⊎ₛ X)) → ∀ {x} → [ A ][ (iter {A} {X} < g >) x ∼ (iterₛ∼ {A} {‖ X ‖} (disc-dom g)) ⟨$⟩ x ]
-    iter-g-var′ : ∀ {X : Setoid ℓ ℓ} → (g : X ⟶ (Delayₛ A ⊎ₛ X)) → ∀ {x} → [ A ][ (iter {A} {X} < g >) x ∼′ (iterₛ∼ {A} {‖ X ‖} (disc-dom g)) ⟨$⟩ x ]
-    force∼ (iter-g-var′ {X} g {x}) = iter-g-var {X} g {x}
-    iter-g-var {X} g {x} with g ⟨$⟩ x
-    ...                  | inj₁ a = ∼-refl A
-    ...                  | inj₂ a = later∼ (iter-g-var′ {X} g {a})
-
     preserves' : ∀ {X : Setoid ℓ ℓ} {g : X ⟶ (Delayₛ A ⊎ₛ X)} → ∀ {x} → [ ⟦ B ⟧ ][ (delay-lift' ∘ (iterₛ {A} {X} g)) ⟨$⟩ x ≡ ([ inj₁ₛ ∘ delay-lift' , inj₂ₛ ]ₛ ∘ g) # ⟨$⟩ x ]
-    preserves' {X} {g} {x} = ≡-trans ⟦ B ⟧ step₁ step₂
+    -- h would need iter-cong∼', which is not doable i think
+    preserves' {X} {g} {x} = ≡-sym ⟦ B ⟧ (#-Uniformity B {f = [ inj₁ₛ ∘ delay-lift' , inj₂ₛ ]ₛ ∘ g} {g = helper} {h = {!   !}} {!   !})--(≡-trans (⟦ B ⟧ ⊎ₛ Delayₛ A) by-uni trivial))
       where
-      step₁ : [ ⟦ B ⟧ ][ (delay-lift' ∘ (iterₛ {A} {X} g)) ⟨$⟩ x ≡ ([ inj₁ₛ ∘ (helper #) , inj₂ₛ ]ₛ ∘ (disc-dom g)) # ⟨$⟩ x ]
-      step₁ = {!   !}
-      step₂ : [ ⟦ B ⟧ ][ ([ inj₁ₛ ∘ (helper #) , inj₂ₛ ]ₛ ∘ (disc-dom g)) # ⟨$⟩ x ≡ ([ inj₁ₛ ∘ delay-lift' , inj₂ₛ ]ₛ ∘ g) # ⟨$⟩ x ]
-      step₂ = #-Uniformity B {h = ‖‖-quote} sub-step₂
-        where
-          sub-step₂ : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ X ][([ inj₁ₛ , inj₂ₛ ]ₛ ∘ ([ inj₁ₛ ∘ (helper #) , inj₂ₛ ]ₛ ∘ (disc-dom g))) ⟨$⟩ x ≡ ([ inj₁ₛ ∘ delay-lift' , inj₂ₛ ]ₛ ∘ g) ⟨$⟩ x ]
-          sub-step₂ {x} with g ⟨$⟩ x
-          ... | inj₁ y = ≡-refl (⟦ B ⟧ ⊎ₛ X)
-          ... | inj₂ y = ≡-refl (⟦ B ⟧ ⊎ₛ X)
-      comp-step : [ ⟦ B ⟧ ][ ([ inj₁ₛ ∘ (helper #) , inj₂ₛ ]ₛ ∘ disc-dom g) # ⟨$⟩ x ≡ ((([ ([ inj₁ₛ , (inj₂ₛ ∘ inj₁ₛ) ]ₛ ∘ helper) , (inj₂ₛ ∘ inj₂ₛ) ]ₛ ∘ [ inj₁ₛ , (disc-dom g) ]ₛ) #) ∘ inj₂ₛ) ⟨$⟩ x ]
-      comp-step = #-Compositionality B {f = helper} {h = disc-dom g}
+        by-uni : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ Delayₛ∼ A ][ < [ inj₁ₛ , inj₂ₛ ∘ iterₛ {A} {X} g ]ₛ ∘ ([ inj₁ₛ ∘ delay-lift' , inj₂ₛ ]ₛ ∘ g) > x ≡ (< helper > ∘′ (iter {A} {X} < g >)) x ]
+        by-uni {x} with g ⟨$⟩ x in eqa 
+        ...    | inj₁ a = {!   !}
+        -- ...    | inj₁ (now a) = {!   !} -- easy
+        -- ...    | inj₁ (later a) = {!   !} -- impossible?
+        ...    | inj₂ a = inj₂ (∼-refl A)
+        trivial : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ Delayₛ∼ A ][ (< helper > ∘′ iter < g >) x ≡ helper₁ (iter < g > x) ]
+        trivial {x} = ≡-refl (⟦ B ⟧ ⊎ₛ Delayₛ∼ A) 
 
   <<_>> = Elgot-Algebra-Morphism.h
 
@@ -356,6 +339,21 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
       *-uniq' {B} f g eq {later x} = ≡-trans ⟦ B ⟧ {!   !} (≡-sym ⟦ B ⟧ (#-Fixpoint B)) 
       -- *-uniq' {B} f g eq {later x} = ≡-trans ⟦ B ⟧ {! *-uniq' {B} f g eq {force x}  !} (≡-sym ⟦ B ⟧ (#-Fixpoint B)) 
 
+
+
+  -- -- TODO stability might be proven more general, since Setoids is CCC (whatever is easier)
+
+  -- delay-stability : ∀ (Y : Setoid ℓ ℓ) (X : Setoid ℓ ℓ) (B : Elgot-Algebra) (f : X ×ₛ Y ⟶ ⟦ B ⟧) → X ×ₛ Delayₛ Y ⟶ ⟦ B ⟧
+  -- delay-stability Y X B f = {!   !}
+
+  -- isStableFreeElgotAlgebra : ∀ (A : Setoid ℓ ℓ) → IsStableFreeElgotAlgebra (freeAlgebra A)
+  -- isStableFreeElgotAlgebra A = record 
+  --   { [_,_]♯ = λ {X} B f → delay-stability A X B f
+  --   ; ♯-law = {!   !} 
+  --   ; ♯-preserving = {!   !} 
+  --   ; ♯-unique = {!   !} 
+  --   }
+
   delayK : MonadK
   delayK = record { freealgebras = freeAlgebra ; stable = {!   !} }
 ```