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

tidy up

Browse source
This commit is contained in:
Leon Vatthauer 2024-02-04 17:58:30 +01:00
parent bb49f23814
commit 1f4c0da823
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
1 changed files with 8 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -72,17 +72,6 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
helper : [ Y ⊎ₛ X ][ inj₁ a ≡ inj₂ b ] helper : [ Y ⊎ₛ X ][ inj₁ a ≡ inj₂ b ]
helper rewrite (≣-sym fi₁) | (≣-sym fi₂) = cong f x≡y helper rewrite (≣-sym fi₁) | (≣-sym fi₂) = cong f x≡y
-- TODO remove the following two later
iter-cong∼' : ∀ {A X : Setoid ℓ ℓ} (f : X ⟶ (Delayₛ A ⊎ₛ X)) {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ (iter {A} {X} < f > x) ∼ (iter {A} {X} < f > y) ]
iter-cong∼′' : ∀ {A X : Setoid ℓ ℓ} (f : X ⟶ (Delayₛ A ⊎ₛ X)) {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ (iter {A} {X} < f > x) ∼′ (iter {A} {X} < f > y) ]
force∼ (iter-cong∼′' {A} {X} f {x} {y} x≡y) = iter-cong∼' f x≡y
iter-cong∼' {A} {X} f {x} {y} x≡y with < f > x in eqx | < f > y in eqy
... | inj₁ a | inj₁ b = {! inj₁-helper f x≡y eqx eqy !} -- inj₁-helper f x≡y eqx eqy
... | inj₁ a | inj₂ b = absurd-helper f x≡y eqx eqy
... | inj₂ a | inj₁ b = absurd-helper f (≡-sym X x≡y) eqy eqx
... | inj₂ a | inj₂ b = {! !} -- later∼ (iter-cong∼′' {A} {X} f (inj₂-helper f x≡y eqx eqy))
iter-cong∼ : ∀ {A X : Setoid ℓ ℓ} (f : X ⟶ (Delayₛ∼ A ⊎ₛ X)) {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ (iter {A} {X} < f > x) ∼ (iter {A} {X} < f > y) ] iter-cong∼ : ∀ {A X : Setoid ℓ ℓ} (f : X ⟶ (Delayₛ∼ A ⊎ₛ X)) {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ (iter {A} {X} < f > x) ∼ (iter {A} {X} < f > y) ]
iter-cong∼′ : ∀ {A X : Setoid ℓ ℓ} (f : X ⟶ (Delayₛ∼ A ⊎ₛ X)) {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ (iter {A} {X} < f > x) ∼′ (iter {A} {X} < f > y) ] iter-cong∼′ : ∀ {A X : Setoid ℓ ℓ} (f : X ⟶ (Delayₛ∼ A ⊎ₛ X)) {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ (iter {A} {X} < f > x) ∼′ (iter {A} {X} < f > y) ]
force∼ (iter-cong∼′ {A} {X} f {x} {y} x≡y) = iter-cong∼ f x≡y force∼ (iter-cong∼′ {A} {X} f {x} {y} x≡y) = iter-cong∼ f x≡y
@ -366,14 +355,14 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
→ (<< h >> ∘ (ηₛ A)) ≋ f → (<< h >> ∘ (ηₛ A)) ≋ f
→ << g >> ≋ << h >> → << g >> ≋ << h >>
*-uniq' {B} f g h eqᵍ eqʰ {x} = ≡-trans ⟦ B ⟧ (cong << g >> iter-id) *-uniq' {B} f g h eqᵍ eqʰ {x} = ≡-trans ⟦ B ⟧ (cong << g >> iter-id)
(≡-trans ⟦ B ⟧ (preserves g {Delayₛ∼ A} {[ inj₁ₛ ∘ quot-morph , inj₂ₛ ]ₛ ∘ helper-now} {x = x}) (≡-trans ⟦ B ⟧ (preserves g {Delayₛ∼ A} {[ inj₁ₛ ∘ D∼⇒D≈ , inj₂ₛ ]ₛ ∘ helper-now} {x = x})
(≡-trans ⟦ B ⟧ (#-resp-≈ B (λ {x} → helper-eq' {x}) {x}) (≡-trans ⟦ B ⟧ (#-resp-≈ B (λ {x} → helper-eq' {x}) {x})
(≡-trans ⟦ B ⟧ (≡-sym ⟦ B ⟧ (preserves h {Delayₛ∼ A} {[ inj₁ₛ ∘ quot-morph , inj₂ₛ ]ₛ ∘ helper-now} {x = x})) (≡-trans ⟦ B ⟧ (≡-sym ⟦ B ⟧ (preserves h {Delayₛ∼ A} {[ inj₁ₛ ∘ D∼⇒D≈ , inj₂ₛ ]ₛ ∘ helper-now} {x = x}))
(≡-sym ⟦ B ⟧ (cong << h >> iter-id))))) (≡-sym ⟦ B ⟧ (cong << h >> iter-id)))))
where where
open Elgot-Algebra B using (_#) open Elgot-Algebra B using (_#)
quot-morph : ∀ {A : Setoid ℓ ℓ} → Delayₛ∼ A ⟶ Delayₛ A D∼⇒D≈ : ∀ {A : Setoid ℓ ℓ} → Delayₛ∼ A ⟶ Delayₛ A
quot-morph {A} = record { to = λ x → x ; cong = λ eq → ∼⇒≈ eq } D∼⇒D≈ {A} = record { to = λ x → x ; cong = λ eq → ∼⇒≈ eq }
helper-now₁ : (Delay ∣ A ∣) → (Delay ∣ A ∣ ⊎ (Delay ∣ A ∣)) helper-now₁ : (Delay ∣ A ∣) → (Delay ∣ A ∣ ⊎ (Delay ∣ A ∣))
helper-now₁ (now x) = inj₁ (now x) helper-now₁ (now x) = inj₁ (now x)
@ -382,13 +371,13 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
helper-now = record { to = helper-now₁ ; cong = λ { (now∼ eq) → inj₁ (now∼ eq) helper-now = record { to = helper-now₁ ; cong = λ { (now∼ eq) → inj₁ (now∼ eq)
; (later∼ eq) → inj₂ (force∼ eq) } } ; (later∼ eq) → inj₂ (force∼ eq) } }
helper-eq' : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ Delayₛ∼ A ][ ([ inj₁ₛ ∘ << g >> , inj₂ₛ ]ₛ ∘ [ inj₁ₛ ∘ quot-morph , inj₂ₛ ]ₛ ∘ helper-now) ⟨$⟩ x helper-eq' : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ Delayₛ∼ A ][ ([ inj₁ₛ ∘ << g >> , inj₂ₛ ]ₛ ∘ [ inj₁ₛ ∘ D∼⇒D≈ , inj₂ₛ ]ₛ ∘ helper-now) ⟨$⟩ x
≡ ([ inj₁ₛ ∘ << h >> , inj₂ₛ ]ₛ ∘ [ inj₁ₛ ∘ quot-morph , inj₂ₛ ]ₛ ∘ helper-now) ⟨$⟩ x ] ≡ ([ inj₁ₛ ∘ << h >> , inj₂ₛ ]ₛ ∘ [ inj₁ₛ ∘ D∼⇒D≈ , inj₂ₛ ]ₛ ∘ helper-now) ⟨$⟩ x ]
helper-eq' {now x} = inj₁ (≡-trans ⟦ B ⟧ eqᵍ (≡-sym ⟦ B ⟧ eqʰ)) helper-eq' {now x} = inj₁ (≡-trans ⟦ B ⟧ eqᵍ (≡-sym ⟦ B ⟧ eqʰ))
helper-eq' {later x} = inj₂ (∼-refl A) helper-eq' {later x} = inj₂ (∼-refl A)
iter-id : ∀ {x} → [ A ][ x ≈ iterₛ ([ inj₁ₛ ∘ quot-morph , inj₂ₛ ]ₛ ∘ helper-now) ⟨$⟩ x ] iter-id : ∀ {x} → [ A ][ x ≈ iterₛ ([ inj₁ₛ ∘ D∼⇒D≈ , inj₂ₛ ]ₛ ∘ helper-now) ⟨$⟩ x ]
iter-id′ : ∀ {x} → [ A ][ x ≈′ iterₛ ([ inj₁ₛ ∘ quot-morph , inj₂ₛ ]ₛ ∘ helper-now) ⟨$⟩ x ] iter-id′ : ∀ {x} → [ A ][ x ≈′ iterₛ ([ inj₁ₛ ∘ D∼⇒D≈ , inj₂ₛ ]ₛ ∘ helper-now) ⟨$⟩ x ]
force≈ (iter-id′ {x}) = iter-id {x} force≈ (iter-id′ {x}) = iter-id {x}
iter-id {now x} = ≈-refl A iter-id {now x} = ≈-refl A
iter-id {later x} = later≈ (iter-id′ {force x}) iter-id {later x} = later≈ (iter-id′ {force x})