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

Finish proof that quotient of D is freealgebra

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

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

@ -350,7 +350,7 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
... | inj₁ y = ≡-refl (⟦ B ⟧ ⊎ₛ X) ... | inj₁ y = ≡-refl (⟦ B ⟧ ⊎ₛ X)
... | inj₂ y = ≡-refl (⟦ B ⟧ ⊎ₛ X) ... | inj₂ y = ≡-refl (⟦ B ⟧ ⊎ₛ X)
<<_>> = Elgot-Algebra-Morphism.h open Elgot-Algebra-Morphism using (preserves) renaming (h to <<_>>)
freeAlgebra : ∀ (A : Setoid ℓ ℓ) → FreeObject elgotForgetfulF A freeAlgebra : ∀ (A : Setoid ℓ ℓ) → FreeObject elgotForgetfulF A
freeAlgebra A = record freeAlgebra A = record
@ -358,13 +358,41 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
; η = ηₛ A ; η = ηₛ A
; _* = delay-lift ; _* = delay-lift
; *-lift = λ {B} f {x} → Elgot-Algebra.#-Fixpoint B ; *-lift = λ {B} f {x} → Elgot-Algebra.#-Fixpoint B
; *-uniq = λ {B} f g eq {x} → *-uniq' {B} f g eq {x} ; *-uniq = λ {B} f g eq {x} → *-uniq' {B} f g (delay-lift f) eq (#-Fixpoint B) {x}
} }
where where
*-uniq' : ∀ {B : Elgot-Algebra} (f : A ⟶ ⟦ B ⟧) (g : Elgot-Algebra-Morphism (delay-algebras A) B) (eq : (<< g >> ∘ (ηₛ A)) ≋ f) {x : Delay ∣ A ∣} → [_][_≡_] (⟦ B ⟧) ((<< g >>) ⟨$⟩ x) ((<< delay-lift {A} {B} f >>) ⟨$⟩ x) *-uniq' : ∀ {B : Elgot-Algebra} (f : A ⟶ ⟦ B ⟧) (g h : Elgot-Algebra-Morphism (delay-algebras A) B)
*-uniq' {B} f g eq {now x} = ≡-trans ⟦ B ⟧ (eq {x}) (≡-sym ⟦ B ⟧ (#-Fixpoint B)) → (<< g >> ∘ (ηₛ A)) ≋ f
*-uniq' {B} f g eq {later x} = ≡-trans ⟦ B ⟧ {! !} (≡-sym ⟦ B ⟧ (#-Fixpoint B)) → (<< h >> ∘ (ηₛ A)) ≋ f
-- *-uniq' {B} f g eq {later x} = ≡-trans ⟦ B ⟧ {! *-uniq' {B} f g eq {force x} !} (≡-sym ⟦ B ⟧ (#-Fixpoint B)) → << g >> ≋ << h >>
*-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 ⟧ (#-resp-≈ B (λ {x} → helper-eq' {x}) {x})
(≡-trans ⟦ B ⟧ (≡-sym ⟦ B ⟧ (preserves h {Delayₛ∼ A} {[ inj₁ₛ ∘ quot-morph , inj₂ₛ ]ₛ ∘ helper-now} {x = x}))
(≡-sym ⟦ B ⟧ (cong << h >> iter-id)))))
where
open Elgot-Algebra B using (_#)
quot-morph : ∀ {A : Setoid ℓ ℓ} → Delayₛ∼ A ⟶ Delayₛ A
quot-morph {A} = record { to = λ x → x ; cong = λ eq → ∼⇒≈ eq }
helper-now₁ : (Delay ∣ A ∣) → (Delay ∣ A ∣ ⊎ (Delay ∣ A ∣))
helper-now₁ (now x) = inj₁ (now x)
helper-now₁ (later x) = inj₂ (force x)
helper-now : Delayₛ∼ A ⟶ ((Delayₛ∼ A) ⊎ₛ (Delayₛ∼ A))
helper-now = record { to = helper-now₁ ; cong = λ { (now∼ eq) → inj₁ (now∼ eq)
; (later∼ eq) → inj₂ (force∼ eq) } }
helper-eq' : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ Delayₛ∼ A ][ ([ inj₁ₛ ∘ << g >> , inj₂ₛ ]ₛ ∘ [ inj₁ₛ ∘ quot-morph , inj₂ₛ ]ₛ ∘ helper-now) ⟨$⟩ x
≡ ([ inj₁ₛ ∘ << h >> , inj₂ₛ ]ₛ ∘ [ inj₁ₛ ∘ quot-morph , inj₂ₛ ]ₛ ∘ helper-now) ⟨$⟩ x ]
helper-eq' {now x} = inj₁ (≡-trans ⟦ B ⟧ eqᵍ (≡-sym ⟦ B ⟧ eqʰ))
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₁ₛ ∘ quot-morph , inj₂ₛ ]ₛ ∘ helper-now) ⟨$⟩ x ]
force≈ (iter-id′ {x}) = iter-id {x}
iter-id {now x} = ≈-refl A
iter-id {later x} = later≈ (iter-id′ {force x})
delayK : MonadK delayK : MonadK
delayK = record { freealgebras = freeAlgebra ; stable = {! !} } delayK = record { freealgebras = freeAlgebra ; stable = {! !} }