From 2e28faeda6ade55443bd63b4aedc74c54a612a87 Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Fri, 2 Feb 2024 16:03:47 +0100 Subject: [PATCH] build on recent PR to agda-categories --- agda/shell.nix | 12 ++-- agda/src/Monad/Instance/Setoids/K.lagda.md | 68 +++++++++++----------- 2 files changed, 41 insertions(+), 39 deletions(-) diff --git a/agda/shell.nix b/agda/shell.nix index bda1a4d..2efe747 100644 --- a/agda/shell.nix +++ b/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 = "a1c797e935432702d25fd729802aeb155b423761"; - hash = "sha256-p9rrQq3aFSG14sJ65aYDvAoPkTsa/UmdkkxD5suhClY="; # sha256-GQuQxzYSQxAIVSJ1vf0blRC0juoxAqD1AHW66H/6NSk= - }; + src = fetchFromGitHub { + repo = "agda-categories"; + owner = "agda"; + rev = "944a487b92ab3a9d3b3ee54d209cd7ea95dc58ed"; + hash = "sha256-G5QgEMj6U+5s3o7HUfORn+Y3gQA9KvpUuAvHAXn7TKk="; + }; # without this nix might use a wrong version of the stdlib to try and typecheck agda-categories buildInputs = [ diff --git a/agda/src/Monad/Instance/Setoids/K.lagda.md b/agda/src/Monad/Instance/Setoids/K.lagda.md index bf67e95..2de8e86 100644 --- a/agda/src/Monad/Instance/Setoids/K.lagda.md +++ b/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; #-resp-≈; #-Diamond) renaming (A to ⟦_⟧) + open Elgot-Algebra using (#-Fixpoint; #-Uniformity; #-Compositionality; #-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} → (≡-trans (⟦ B ⟧ ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid)) (stepid {x}) (step₂ {x}))))) + (#-resp-≈ B (λ {x} → (step₂ {x})))) where helper₁''' : Delay (∣ A ∣ × ℕ {ℓ}) → ∣ ⟦ B ⟧ ∣ ⊎ (Delay (∣ A ∣ × ℕ {ℓ}) ⊎ Delay (∣ A ∣ × ℕ {ℓ})) helper₁''' (now (x , zero)) = inj₁ (< f > x) @@ -284,12 +284,6 @@ 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 @@ -310,18 +304,41 @@ 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 ] - -- 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)) + preserves' {X} {g} {x} = ≡-trans ⟦ B ⟧ step₁ step₂ where - 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) + 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} <<_>> = Elgot-Algebra-Morphism.h @@ -339,21 +356,6 @@ 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 = {! !} } ``` \ No newline at end of file