finished congruence proof

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

@@ -9,12 +9,13 @@ open import Data.Sum.Relation.Binary.Pointwise
 open import Function.Bundles using (_⟨$⟩_) renaming (Func to _⟶_)
 open import Function.Construct.Identity renaming (function to idₛ)
 open import Function.Construct.Setoid renaming (setoid to _⇨_; _∙_ to _∘_)
-open import Function using (_∘′_) renaming (_∘_ to _∘f_)
+open import Function using (_∘′_; id) renaming (_∘_ to _∘f_)
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_) renaming (sym to ≣-sym; refl to ≣-refl; trans to ≣-trans)
 open import FreeObject
 open import Categories.FreeObjects.Free
 open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
+open import Data.Product.Function.NonDependent.Setoid using (proj₁ₛ)
 open import Categories.Category.Instance.Properties.Setoids.Choice using ()
 open import Data.Product.Relation.Binary.Pointwise.NonDependent
 open import Data.Product
@@ -154,11 +155,11 @@ 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) 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
-  delay-lift {A} {B} f = record { h = delay-lift' ; preserves = λ {X} {g} {x} → ? }
+  delay-lift {A} {B} f = record { h = delay-lift' ; preserves = λ {X} {g} {x} → {!   !} }
     where
     open Elgot-Algebra B using (_#)
     -- (f + id) ∘ out
@@ -195,7 +196,7 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
         z₁    = delta {A} ineq₁
         z₂    = delta {A} ineq₂
 
-    helper#≈-cong' {z} = ≡-trans ⟦ B ⟧ (≡-sym ⟦ B ⟧ eq₁) eq₂
+    helper#≈-cong' {z} = ≡-trans ⟦ B ⟧ (≡-trans ⟦ B ⟧ (≡-sym ⟦ B ⟧ eq₁) (≡-sym ⟦ B ⟧ eq₀)) eq₂
       where
         outer : A ⟶ (A ×ₛ ℕ-setoid {ℓ})
         outer = record { to = λ z → z , zero ; cong = λ {x} {y} x≡y → x≡y , ≣-refl }
@@ -215,55 +216,75 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
         helper' : (Delayₛ∼ (A ×ₛ ℕ-setoid)) ⟶ (⟦ B ⟧ ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid))
         helper' = record { to = helper₁' ; cong = helper₁-cong'}
 
-        -- an unfolding lemma for delay (on setoids)
+        helper₁'' : Delay (∣ A ∣ × ℕ {ℓ}) → ∣ ⟦ B ⟧ ∣ ⊎ Delay (∣ A ∣ × ℕ {ℓ})
+        helper₁'' (now (x , _))  = inj₁ (< f > x)
+        helper₁'' (later y)      = inj₂ (force y)
 
-        out : ∀ {X} → Delay X → X ⊎ Delay′ X
-        out {X} (now x) = inj₁ x
-        out {X} (later x) = inj₂ x
+        helper₁-cong'' : {x y : Delay (∣ A ∣ × ℕ {ℓ})} → (x∼y : [ A ×ₛ ℕ-setoid ][ x ∼ y ]) → [ ⟦ B ⟧ ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid) ][ helper₁'' x ≡ helper₁'' y ]
+        helper₁-cong'' {now (x , _)}  (now∼ (x≡y , ≣-refl)) = inj₁ (cong f x≡y)
+        helper₁-cong'' (later∼ x∼y) = inj₂ (force∼ x∼y)
 
-        out⁻¹ : ∀ {X} → X ⊎ Delay′ X → Delay X
-        out⁻¹ {X} = [ now , later ]
+        helper'' : (Delayₛ∼ (A ×ₛ ℕ-setoid)) ⟶ (⟦ B ⟧ ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid))
+        helper'' = record { to = helper₁'' ; cong = helper₁-cong''}
 
-        out∼ : ∀ {X} → (Delayₛ∼ X) ⟶ (X ⊎ₛ (Delayₛ∼′ X))
-        out∼ {X} = record { to = out {∣ X ∣} ; cong = out-cong }
+        -- Needs #-Diamond
+        eq₀ : ∀ {z} → [ ⟦ B ⟧ ][ helper' # ⟨$⟩ z ≡ helper'' # ⟨$⟩ z ]
+        eq₀ {z} = ≡-trans ⟦ B ⟧ 
+                    (#-resp-≈ B {Delayₛ∼ (A ×ₛ ℕ-setoid)} {helper'} step₁)
+                    (≡-trans ⟦ B ⟧
+                      (#-Diamond B {Delayₛ∼ (A ×ₛ ℕ-setoid)} helper''') 
+                      (#-resp-≈ B (λ {x} → (≡-trans (⟦ B ⟧ ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid)) (stepid {x}) (step₂ {x})))))
           where
-            out-cong : ∀ {x y} → [ X ][ x ∼ y ] → [ X ⊎ₛ (Delayₛ∼′ X) ][ out x ≡ out y ]
-            out-cong {.(now _)} {.(now _)} (now∼ x≡y) = inj₁ x≡y
-            out-cong {.(later _)} {.(later _)} (later∼ x∼y) = inj₂ (record { force∼′′ = force∼ x∼y })
+            helper₁''' : Delay (∣ A ∣ × ℕ {ℓ}) → ∣ ⟦ B ⟧ ∣ ⊎ (Delay (∣ A ∣ × ℕ {ℓ}) ⊎ Delay (∣ A ∣ × ℕ {ℓ}))
+            helper₁''' (now (x , zero))  = inj₁ (< f > x)
+            helper₁''' (now (x , suc n)) = inj₂ (inj₁ (< liftFₛ∼ outer > (ι {A} (x , n))))
+            helper₁''' (later y)         = inj₂ (inj₂ (force y))
 
-        -- TODO move
-        nowₛ∼ : ∀ {X} → X ⟶ Delayₛ∼ X
-        nowₛ∼ {X} = record { to = now ; cong = {!   !} }
-        laterₛ∼ : ∀ {X} → Delayₛ∼′ X ⟶ Delayₛ∼ X
-        laterₛ∼ {X} = record { to = later ; cong = {!   !} }
+            helper₁-cong''' : {x y : Delay (∣ A ∣ × ℕ {ℓ})} → (x∼y : [ A ×ₛ ℕ-setoid ][ x ∼ y ]) → [ ⟦ B ⟧ ⊎ₛ (Delayₛ∼ (A ×ₛ ℕ-setoid) ⊎ₛ 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₂ (inj₁ (cong (liftFₛ∼ outer) (cong ιₛ' (x≡y , ≣-refl))))
+            helper₁-cong''' (later∼ x∼y) = inj₂ (inj₂ (force∼ x∼y))
             
-        out⁻¹∼ : ∀ {X} → (X ⊎ₛ Delayₛ∼′ X) ⟶ (Delayₛ∼ X)
-        out⁻¹∼ {X} = [ nowₛ∼ , laterₛ∼ ]ₛ
+            helper''' : (Delayₛ∼ (A ×ₛ ℕ-setoid)) ⟶ (⟦ B ⟧ ⊎ₛ (Delayₛ∼ (A ×ₛ ℕ-setoid) ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid)))
+            helper''' = record { to = helper₁''' ; cong = helper₁-cong''' }
 
-        -- TODO out∘out⁻¹≡id and out⁻¹∘out≡id
+            step₁ : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid) ][ helper' ⟨$⟩ x ≡ ([ inj₁ , inj₂ ∘′ [ id , id ] ] ∘′ helper₁''') x ]
+            step₁ {now (a , zero)} = ≡-refl (⟦ B ⟧ ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid))
+            step₁ {now (a , suc n)} = ≡-refl (⟦ B ⟧ ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid))
+            step₁ {later x} = ≡-refl (⟦ B ⟧ ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid))
 
-        -- Should follow by compositionality + fixpoint
-        eq₁ : ∀ {z} → [ ⟦ B ⟧ ][ helper' # ⟨$⟩ z ≡ helper # ⟨$⟩ liftF proj₁ z ]
-        eq₁ {z} = {!   !}
+            step₂ : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid) ][ ([ inj₁ , [ inj₁ ∘′ < ([ inj₁ₛ , inj₂ₛ ∘ [ idₛ (Delayₛ∼ (A ×ₛ ℕ-setoid)) , idₛ (Delayₛ∼ (A ×ₛ ℕ-setoid)) ]ₛ ]ₛ ∘ helper''') # > , inj₂ ] ] ∘′ helper₁''') x ≡ helper'' ⟨$⟩ x ]
+            step₂ {now (a , zero)} = ≡-refl (⟦ B ⟧ ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid))
+            step₂ {now (x , suc n)} = inj₁ (by-induction n)
               where
-            step₁ : [ ⟦ B ⟧ ][ helper' # ⟨$⟩ z ≡ (< ([ inj₁ₛ , inj₂ₛ ∘ out∼ ]ₛ ∘ helper' ∘ out⁻¹∼) # > ∘′ out) z ]
-            step₁ = {!   !} -- should follow by uniformity
+                by-induction : ∀ n → [ ⟦ B ⟧ ][ < ([ inj₁ₛ , inj₂ₛ ∘ [ idₛ (Delayₛ∼ (A ×ₛ ℕ-setoid)) , idₛ (Delayₛ∼ (A ×ₛ ℕ-setoid)) ]ₛ ]ₛ ∘ helper''') # > (< liftFₛ∼ outer > (ι (x , n))) ≡ f ⟨$⟩ x ]
+                by-induction zero = #-Fixpoint B
+                by-induction (suc n) = ≡-trans ⟦ B ⟧ (#-Fixpoint B) (by-induction n)
+            step₂ {later y} = ≡-refl (⟦ B ⟧ ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid))
 
-            step₂ : ∀ {x} → [ ⟦ B ⟧ ][ (< ([ inj₁ₛ , inj₂ₛ ∘ out∼ ]ₛ ∘ helper' ∘ out⁻¹∼) # > ∘′ out) x ≡ helper # ⟨$⟩ liftF proj₁ x ]
-            step₂ {now x} = {!   !}
-            step₂ {later x} = {!   !} -- ?
+            -- 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
+            by-uni : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ Delayₛ∼ A ][ [ inj₁ , inj₂ ∘′ (liftF proj₁) ] (helper₁'' x) ≡ (< helper > ∘′ liftF proj₁) x ]
+            by-uni {now (a , b)} = ≡-refl (⟦ B ⟧ ⊎ₛ Delayₛ∼ A)
+            by-uni {later x} = ≡-refl (⟦ B ⟧ ⊎ₛ Delayₛ∼ A)
 
         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'
+        eq {now (x , n)} {now (y , .n)} (now∼ (x∼y , ≣-refl)) = eq' {n}
           where
             eq' : ∀ {n} → [ ⟦ B ⟧ ⊎ₛ Delayₛ∼ A ][ [ inj₁ , inj₂ ∘′ μ ∘′ liftF ι ] (helper₁' (now (x , n))) ≡ (helper₁ ∘′ μ {A} ∘′ liftF ι) (now (y , n)) ]
             eq' {zero}  = inj₁ (cong f x∼y)
             eq' {suc n} = inj₂ (∼-trans A (cong (μₛ∼ A) (∼-sym (Delayₛ∼ A) (lift-comp∼ {f = outer} {g = ιₛ'} {ι (x , n)} (∼-refl A)))) (∼-trans A identityˡ∼ (cong ιₛ' (x∼y , ≣-refl)))) -- (identityˡ∼ (cong ιₛ' (x∼y , ≣-refl))))
         eq (later∼ x∼y) = inj₂ (cong (μₛ∼ A) (cong (liftFₛ∼ ιₛ') (force∼ x∼y)))
 
-        -- Should follow by uniformity
         eq₂ : [ ⟦ B ⟧ ][ helper' # ⟨$⟩ z ≡ helper # ⟨$⟩ μ {A} (liftF (ι {A}) z)]
-        eq₂ = Elgot-Algebra.#-Uniformity B {Delayₛ∼ (A ×ₛ ℕ-setoid {ℓ})} {Delayₛ∼ A} {helper'} {helper} {μₛ∼ A ∘ liftFₛ∼ ιₛ'} {!   !} -- eq (∼-refl (A ×ₛ ℕ-setoid))
+        eq₂ = Elgot-Algebra.#-Uniformity B {Delayₛ∼ (A ×ₛ ℕ-setoid {ℓ})} {Delayₛ∼ A} {helper'} {helper} {μₛ∼ A ∘ liftFₛ∼ ιₛ'} (λ {x} → eq {x} {x} (∼-refl (A ×ₛ ℕ-setoid)))
 
     delay-lift' = record { to = < helper # > ; cong = helper#≈-cong }