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-02-01 12:51:13 +01:00
parent d3b63f632d
commit 86e45d7b71
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
1 changed files with 11 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
agda/src/Category/Construction/ElgotAlgebras.lagda.md
View file

@ -366,13 +366,17 @@ module Category.Construction.ElgotAlgebras {o ℓ e} {C : Category o ℓ e} wher
((i₂ ∘ id) ∘ (id ⁂ id)) ∘ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩ ≈⟨ (cancelʳ (identityˡ ○ ⟨⟩-unique id-comm id-comm)) ⟩∘⟨refl ⟩ ((i₂ ∘ id) ∘ (id ⁂ id)) ∘ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩ ≈⟨ (cancelʳ (identityˡ ○ ⟨⟩-unique id-comm id-comm)) ⟩∘⟨refl ⟩
i₂ ∘ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩ ∎ i₂ ∘ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩ ∎
Elgot-Algebra-Morphism.h (CanonicalCartesianClosed.curry cccc {A} {B} {C} f) = λg < f > Elgot-Algebra-Morphism.h (CanonicalCartesianClosed.curry cccc {A} {B} {C} f) = λg < f >
Elgot-Algebra-Morphism.preserves (CanonicalCartesianClosed.curry cccc {A} {B} {C} f) {X} {g} = begin Elgot-Algebra-Morphism.preserves (CanonicalCartesianClosed.curry cccc {A} {B} {C} f) {X} {g} = λ-unique′ (begin
λg < f > ∘ (Elgot-Algebra._# A) g ≈⟨ {! !} ⟩ eval′ ∘ ((λg < f > ∘ (Elgot-Algebra._# A) g) ⁂ id) ≈⟨ refl⟩∘⟨ ⁂-cong₂ subst refl ⟩
{! !} ≈⟨ {! !} ⟩ eval′ ∘ ((λg (< f > ∘ (((Elgot-Algebra._# A) g) ⁂ id))) ⁂ id) ≈⟨ β′ ⟩
{! !} ≈⟨ {! !} ⟩ < f > ∘ (((Elgot-Algebra._# A) g) ⁂ id) ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩ {! !} ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩ {! !} ≈⟨ {! !} ⟩
λg ((Elgot-Algebra._# C) ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (((λg < f > +₁ id) ∘ g) ⁂ id))) ∎ < f > ∘ ⟨ (Elgot-Algebra._# A) ((π₁ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id))) , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id))) ⟩ ≈⟨ Elgot-Algebra-Morphism.preserves f ⟩
(Elgot-Algebra._# C) ((< f > +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id)) ≈˘⟨ {! !} ⟩
(Elgot-Algebra._# C) ((eval′ +₁ id) ∘ (((λg < f > ⁂ id) +₁ (id ⁂ id)) ∘ distributeʳ⁻¹) ∘ (g ⁂ id)) ≈˘⟨ Elgot-Algebra.#-resp-≈ C (refl⟩∘⟨ (pullˡ (sym (distributeʳ⁻¹-natural id (λg < f >) id)))) ⟩
(Elgot-Algebra._# C) ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((λg < f > +₁ id) ⁂ id) ∘ (g ⁂ id)) ≈⟨ Elgot-Algebra.#-resp-≈ C (refl⟩∘⟨ (refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ refl identity²))) ⟩
(Elgot-Algebra._# C) ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (((λg < f > +₁ id) ∘ g) ⁂ id)) ∎)
CanonicalCartesianClosed.eval-comp cccc {A} {B} {C} {f} = {! !} CanonicalCartesianClosed.eval-comp cccc {A} {B} {C} {f} = {! !}
CanonicalCartesianClosed.curry-unique cccc {A} {B} {C} {f} {g} eq = {! !} CanonicalCartesianClosed.curry-unique cccc {A} {B} {C} {f} {g} eq = {! !}
-- record -- record