sync

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

@@ -210,19 +210,16 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
         outer : A ⟶ A ×ₛ ℕ-setoid {ℓ}
         outer = record { _⟨$⟩_ = λ z → z , zero ; cong = λ {x} {y} x≡y → x≡y , ≣-refl }
 
-        zero-helper : Delayₛ∼ A ⟶ Delayₛ∼ (A ×ₛ ℕ-setoid {ℓ})
+        ι-cancel : ∀ {x} → [ A ][ (ι {A} ∘′ (λ z → z , zero)) x ∼ now x ]
-        zero-helper = liftFₛ∼ outer
-
-        ι-cancel : ∀ {x} → [ A ][ (ι ∘′ (λ z → z , zero)) x ∼ now x ]
         ι-cancel = ∼-refl A
         helper₁' : Delay (∣ A ∣ × ℕ {ℓ}) → ∣ ⟦ B ⟧ ∣ ⊎ Delay (∣ A ∣ × ℕ {ℓ})
         helper₁' (now (x , zero))  = inj₁ (< f > x)
-        helper₁' (now (x , suc n)) = inj₂ (< zero-helper > (ι {A} (x , n)))
+        helper₁' (now (x , suc n)) = inj₂ (< liftFₛ∼ outer > (ι {A} (x , n)))
         helper₁' (later y)         = inj₂ (force y)
 
         helper₁-cong' : {x y : Delay (∣ A ∣ × ℕ {ℓ})} → (x∼y : [ A ×ₛ ℕ-setoid ][ x ∼ y ]) → [ ⟦ B ⟧ ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid) ][ helper₁' x ≡ helper₁' y ]
         helper₁-cong' {now (x , zero)}  (now∼ (x≡y , ≣-refl)) = inj₁ (cong f x≡y)
-        helper₁-cong' {now (x , suc n)} {now (y , suc _)} (now∼ (x≡y , ≣-refl)) = inj₂ (cong zero-helper (cong ιₛ' (x≡y , ≣-refl)))
+        helper₁-cong' {now (x , suc n)} {now (y , suc _)} (now∼ (x≡y , ≣-refl)) = inj₂ (cong (liftFₛ∼ outer) (cong ιₛ' (x≡y , ≣-refl)))
         helper₁-cong' (later∼ x∼y) = inj₂ (force∼ x∼y)
 
         helper' : Delayₛ∼ (A ×ₛ ℕ-setoid) ⟶ ⟦ B ⟧ ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid)
@@ -257,13 +254,14 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
 
         -- Should follow by compositionality + fixpoint
         eq₁ : ∀ {z} → [ ⟦ B ⟧ ][ helper' # ⟨$⟩ z ≡ helper # ⟨$⟩ liftF proj₁ z ]
-        eq₁ {x} = {!   !}
+        eq₁ {z} = {!   !}
           where
             step₁ : [ ⟦ B ⟧ ][ helper' # ⟨$⟩ z ≡ (< ([ inj₁ₛ , inj₂ₛ ∘ out∼ ]ₛ ∘ helper' ∘ out⁻¹∼) # > ∘′ out) z ]
             step₁ = {!   !} -- should follow by uniformity
 
-            step₂ : [ ⟦ B ⟧ ][ (< ([ inj₁ₛ , inj₂ₛ ∘ out∼ ]ₛ ∘ helper' ∘ out⁻¹∼) # > ∘′ out) z ≡ helper # ⟨$⟩ liftF proj₁ z ]
+            step₂ : ∀ {x} → [ ⟦ B ⟧ ][ (< ([ inj₁ₛ , inj₂ₛ ∘ out∼ ]ₛ ∘ helper' ∘ out⁻¹∼) # > ∘′ out) x ≡ helper # ⟨$⟩ liftF proj₁ x ]
-            step₂ = {!   !} -- ?
+            step₂ {now x} = {!   !}
+            step₂ {later x} = {!   !} -- ?
 
         eq : ∀ {x y} → [ A ×ₛ ℕ-setoid ][ x ∼ y ] → [ ⟦ B ⟧ ⊎ₛ Delayₛ∼ A ][ [ inj₁ , inj₂ ∘′ μ ∘′ (liftF ι) ] (helper₁' x) ≡ (helper₁ ∘′ μ ∘′ (liftF ι)) y ]
         eq {now (x , n)} {now (y , .n)} (now∼ (x∼y , ≣-refl)) = eq'