minor progress

This commit is contained in:
Leon Vatthauer 2024-02-01 14:00:54 +01:00
parent 86e45d7b71
commit d90381d11a
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8

View file

@ -370,45 +370,16 @@ module Category.Construction.ElgotAlgebras {o e} {C : Category o e} wher
eval ∘ ((λg < f > ∘ (Elgot-Algebra._# A) g) ⁂ id) ≈⟨ refl⟩∘⟨ ⁂-cong₂ subst refl ⟩ eval ∘ ((λg < f > ∘ (Elgot-Algebra._# A) g) ⁂ id) ≈⟨ refl⟩∘⟨ ⁂-cong₂ subst refl ⟩
eval ∘ ((λg (< f > ∘ (((Elgot-Algebra._# A) g) ⁂ id))) ⁂ id) ≈⟨ β′ ⟩ eval ∘ ((λg (< f > ∘ (((Elgot-Algebra._# A) g) ⁂ id))) ⁂ id) ≈⟨ β′ ⟩
< f > ∘ (((Elgot-Algebra._# A) g) ⁂ id) ≈⟨ {! !} ⟩ < f > ∘ (((Elgot-Algebra._# A) g) ⁂ id) ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩ {! !} ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩ {! !} ≈˘⟨ {! !} ⟩
{! !} ≈˘⟨ {! !} ⟩
{! !} ≈˘⟨ {! !} ⟩
< f > ∘ ⟨ [ id , (Elgot-Algebra._# A) ((π₁ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id))) ] ∘ ((π₁ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id))) , [ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id))) ] ∘ ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id))) ⟩ ≈˘⟨ refl⟩∘⟨ (⟨⟩-cong₂ (Elgot-Algebra.#-Fixpoint A) (Elgot-Algebra.#-Fixpoint B)) ⟩
< f > ∘ ⟨ (Elgot-Algebra._# A) ((π₁ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id))) , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id))) ⟩ ≈⟨ Elgot-Algebra-Morphism.preserves f ⟩ < 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) ((< 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) ∘ (((λ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) ⁂ id) ∘ (g ⁂ id)) ≈⟨ Elgot-Algebra.#-resp-≈ C (refl⟩∘⟨ (refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ refl identity²))) ⟩
(Elgot-Algebra._# C) ((eval +₁ id) ∘ distributeʳ⁻¹ ∘ (((λg < f > +₁ id) ∘ g) ⁂ id)) ∎) (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 = λ-unique eq
-- record
-- { = Terminal. Terminal-Elgot-Algebras
-- ; _×_ = λ X Y → A×B-Helper {X} {Y}
-- ; ! = Terminal.! Terminal-Elgot-Algebras
-- ; π₁ = λ {X} {Y} → Product.π₁ (Product-Elgot-Algebras X Y)
-- ; π₂ = λ {X} {Y} → Product.π₂ (Product-Elgot-Algebras X Y)
-- ; ⟨_,_⟩ = λ {X} {Y} {Z} f g → Product.⟨_,_⟩ (Product-Elgot-Algebras Y Z) f g
-- ; !-unique = Terminal.!-unique Terminal-Elgot-Algebras
-- ; π₁-comp = λ {X} {Y} {f} {Z} {g} → Product.project₁ (Product-Elgot-Algebras Y Z) {h = f} {i = g}
-- ; π₂-comp = λ {X} {Y} {f} {Z} {g} → Product.project₂ (Product-Elgot-Algebras Y Z) {h = f} {i = g}
-- ; ⟨,⟩-unique = λ {C} {A} {B} {f} {g} {h} eq₁ eq₂ → Product.unique (Product-Elgot-Algebras A B) {h = h} {i = f} {j = g} eq₁ eq₂
-- ; _^_ = λ A X → B^A-Helper {A} {Elgot-Algebra.A X}
-- ; eval = λ {A} {B} → record { h = eval ; preserves = λ {X} {f} → begin
-- eval ∘ ⟨ (λg ((Elgot-Algebra._# A) ((eval +₁ id) ∘ distributeʳ⁻¹ ∘ ((π₁ +₁ id) ∘ f ⁂ id)))) , _ ⟩ ≈˘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ) ⟩
-- eval ∘ ((λg ((Elgot-Algebra._# A) ((eval +₁ id) ∘ distributeʳ⁻¹ ∘ ((π₁ +₁ id) ∘ f ⁂ id)))) ⁂ id) ∘ ⟨ id , _ ⟩ ≈⟨ pullˡ β′ ⟩
-- ((Elgot-Algebra._# A) ((eval +₁ id) ∘ distributeʳ⁻¹ ∘ ((π₁ +₁ id) ∘ f ⁂ id))) ∘ ⟨ id , _ ⟩ ≈⟨ {! !} ⟩
-- (Elgot-Algebra._# A) ((eval +₁ id) ∘ f) ∎ } -- ⟨ ((π₁ +₁ id) ∘ h)#ᵃ , ((π₂ +₁ id) ∘ h)#ᵇ ⟩
-- ; curry = λ {C} {A} {B} f → record { h = λg (Elgot-Algebra-Morphism.h f) ; preserves = {! !} }
-- ; eval-comp = λ {A} {B} {C} {f} → {! !}
-- ; curry-unique = λ {A} {B} {C} {f} {g} eq → {! !}
-- }
Exponential-Elgot-Algebras : ∀ (EA EB : Elgot-Algebra) → Exponential Elgot-Algebras EA EB
Exponential-Elgot-Algebras EA EB = record
{ B^A = B^A-Helper {EA} {Elgot-Algebra.A EB}
; product = Product-Elgot-Algebras (B^A-Helper {EA} {Elgot-Algebra.A EB}) EA
; eval = record { h = {! eval {Elgot-Algebra.A EB} {Elgot-Algebra.A EA} !} ; preserves = {! !} }
; λg = {! λ {X} prod → !}
; β = {! !}
; λ-unique = {! !}
}
-- TODO instead show canonical ccc
``` ```