leonv/bsc-leon-vatthauer
1
0
Fork 0
mirror of https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git synced 2024-05-31 07:28:34 +02:00
Code Issues Projects Releases Packages Wiki Activity

minor

Browse source
This commit is contained in:
Leon Vatthauer 2024-03-11 18:15:55 +01:00
parent c631cf1bc3
commit 5f836b4d89
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
1 changed files with 1 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
agda/src/Monad/Instance/Setoids/K.lagda.md
View file

@ -323,11 +323,9 @@ To show preservation we need some facts about discretizing setoids:
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})
... | inj₂ a = later∼ λ { .force∼ → iter-g-var {X} g {a} }
```
Now we show that helper # is iteration preserving: