mirror of
https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git
synced 2024-05-31 07:28:34 +02:00
Finished part of elgot products
This commit is contained in:
parent
6add58340d
commit
9ef9d8e76c
1 changed files with 32 additions and 6 deletions
|
@ -171,7 +171,7 @@ module _ {C𝒞 : CocartesianCategory o ℓ e} where
|
|||
-- products and exponentials of elgot-algebras
|
||||
--*
|
||||
|
||||
-- product elgot-algebras
|
||||
-- if the carriers of the algebra form a product, so do the algebras
|
||||
Product-Elgot-Algebra : ∀ {EA EB : Elgot-Algebra} → Product 𝒞 (Elgot-Algebra.A EA) (Elgot-Algebra.A EB) → Elgot-Algebra
|
||||
Product-Elgot-Algebra {EA} {EB} p = record
|
||||
{ A = A×B
|
||||
|
@ -232,15 +232,41 @@ module _ {C𝒞 : CocartesianCategory o ℓ e} where
|
|||
((π₂ ∘ ⟨ ((π₁ +₁ idC) ∘ g)#ᵃ , ((π₂ +₁ idC) ∘ g)#ᵇ ⟩) ∘ h) ≈⟨ assoc ⟩
|
||||
π₂ ∘ ⟨ ((π₁ +₁ idC) ∘ g)#ᵃ , ((π₂ +₁ idC) ∘ g)#ᵇ ⟩ ∘ h ∎
|
||||
)
|
||||
; #-Folding = _ -- TODO
|
||||
; #-resp-≈ = _ -- TODO
|
||||
; #-Folding = λ {X} {Y} {f} {h} → ⟨⟩-cong₂ (foldingˡ {X} {Y}) (foldingʳ {X} {Y})
|
||||
; #-resp-≈ = λ fg → ⟨⟩-cong₂ (#ᵃ-resp-≈ (∘-resp-≈ʳ fg)) (#ᵇ-resp-≈ (∘-resp-≈ʳ fg))
|
||||
}
|
||||
where
|
||||
open Elgot-Algebra EA using (A) renaming (_# to _#ᵃ; #-Fixpoint to #ᵃ-Fixpoint; #-Uniformity to #ᵃ-Uniformity)
|
||||
open Elgot-Algebra EB using () renaming (A to B; _# to _#ᵇ; #-Fixpoint to #ᵇ-Fixpoint; #-Uniformity to #ᵇ-Uniformity)
|
||||
open Elgot-Algebra EA using (A) renaming (_# to _#ᵃ; #-Fixpoint to #ᵃ-Fixpoint; #-Uniformity to #ᵃ-Uniformity; #-Folding to #ᵃ-Folding; #-resp-≈ to #ᵃ-resp-≈)
|
||||
open Elgot-Algebra EB using () renaming (A to B; _# to _#ᵇ; #-Fixpoint to #ᵇ-Fixpoint; #-Uniformity to #ᵇ-Uniformity; #-Folding to #ᵇ-Folding; #-resp-≈ to #ᵇ-resp-≈)
|
||||
open Product 𝒞 p
|
||||
open HomReasoning
|
||||
open Equiv
|
||||
foldingˡ : ∀ {X} {Y} {f} {h} → (((π₁ +₁ idC) ∘ (⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ +₁ h))#ᵃ) ≈ ((π₁ +₁ idC) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ])#ᵃ
|
||||
foldingˡ {X} {Y} {f} {h} = begin
|
||||
((π₁ +₁ idC) ∘ (⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ +₁ h))#ᵃ ≈⟨ #ᵃ-resp-≈ +₁∘+₁ ⟩
|
||||
((π₁ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ +₁ idC ∘ h)#ᵃ) ≈⟨ #ᵃ-resp-≈ (+₁-cong₂ project₁ identityˡ) ⟩
|
||||
((((π₁ +₁ idC) ∘ f)#ᵃ +₁ h)#ᵃ) ≈⟨ #ᵃ-Folding ⟩
|
||||
([ (idC +₁ i₁) ∘ ((π₁ +₁ idC) ∘ f) , i₂ ∘ h ] #ᵃ) ≈⟨ #ᵃ-resp-≈ ([]-congʳ sym-assoc) ⟩
|
||||
([ ((idC +₁ i₁) ∘ (π₁ +₁ idC)) ∘ f , i₂ ∘ h ] #ᵃ) ≈⟨ #ᵃ-resp-≈ ([]-congʳ (∘-resp-≈ˡ +₁∘+₁)) ⟩
|
||||
([ ((idC ∘ π₁ +₁ i₁ ∘ idC)) ∘ f , i₂ ∘ h ] #ᵃ) ≈⟨ #ᵃ-resp-≈ ([]-congʳ (∘-resp-≈ˡ (+₁-cong₂ identityˡ identityʳ))) ⟩
|
||||
([ ((π₁ +₁ i₁)) ∘ f , i₂ ∘ h ] #ᵃ) ≈⟨ sym (#ᵃ-resp-≈ ([]-cong₂ (∘-resp-≈ˡ (+₁-cong₂ identityʳ identityˡ)) (∘-resp-≈ˡ identityʳ))) ⟩
|
||||
(([ (π₁ ∘ idC +₁ idC ∘ i₁) ∘ f , (i₂ ∘ idC) ∘ h ])#ᵃ) ≈⟨ sym (#ᵃ-resp-≈ ([]-cong₂ (∘-resp-≈ˡ +₁∘+₁) (∘-resp-≈ˡ +₁∘i₂))) ⟩
|
||||
(([ ((π₁ +₁ idC) ∘ (idC +₁ i₁)) ∘ f , ((π₁ +₁ idC) ∘ i₂) ∘ h ])#ᵃ) ≈⟨ #ᵃ-resp-≈ ([]-cong₂ assoc assoc) ⟩
|
||||
(([ (π₁ +₁ idC) ∘ (idC +₁ i₁) ∘ f , (π₁ +₁ idC) ∘ i₂ ∘ h ])#ᵃ) ≈⟨ sym (#ᵃ-resp-≈ ∘[]) ⟩
|
||||
((π₁ +₁ idC) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ])#ᵃ ∎
|
||||
foldingʳ : ∀ {X} {Y} {f} {h} → ((π₂ +₁ idC) ∘ (⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ +₁ h))#ᵇ ≈ ((π₂ +₁ idC) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ])#ᵇ
|
||||
foldingʳ {X} {Y} {f} {h} = begin
|
||||
((π₂ +₁ idC) ∘ (⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ +₁ h))#ᵇ ≈⟨ #ᵇ-resp-≈ +₁∘+₁ ⟩
|
||||
((π₂ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ +₁ idC ∘ h)#ᵇ) ≈⟨ #ᵇ-resp-≈ (+₁-cong₂ project₂ identityˡ) ⟩
|
||||
((((π₂ +₁ idC) ∘ f)#ᵇ +₁ h)#ᵇ) ≈⟨ #ᵇ-Folding ⟩
|
||||
[ (idC +₁ i₁) ∘ ((π₂ +₁ idC) ∘ f) , i₂ ∘ h ] #ᵇ ≈⟨ #ᵇ-resp-≈ ([]-congʳ sym-assoc) ⟩
|
||||
([ ((idC +₁ i₁) ∘ (π₂ +₁ idC)) ∘ f , i₂ ∘ h ] #ᵇ) ≈⟨ #ᵇ-resp-≈ ([]-congʳ (∘-resp-≈ˡ +₁∘+₁)) ⟩
|
||||
([ ((idC ∘ π₂ +₁ i₁ ∘ idC)) ∘ f , i₂ ∘ h ] #ᵇ) ≈⟨ #ᵇ-resp-≈ ([]-congʳ (∘-resp-≈ˡ (+₁-cong₂ identityˡ identityʳ))) ⟩
|
||||
([ ((π₂ +₁ i₁)) ∘ f , i₂ ∘ h ] #ᵇ) ≈⟨ sym (#ᵇ-resp-≈ ([]-cong₂ (∘-resp-≈ˡ (+₁-cong₂ identityʳ identityˡ)) (∘-resp-≈ˡ identityʳ))) ⟩
|
||||
(([ (π₂ ∘ idC +₁ idC ∘ i₁) ∘ f , (i₂ ∘ idC) ∘ h ])#ᵇ) ≈⟨ sym (#ᵇ-resp-≈ ([]-cong₂ (∘-resp-≈ˡ +₁∘+₁) (∘-resp-≈ˡ +₁∘i₂))) ⟩
|
||||
(([ ((π₂ +₁ idC) ∘ (idC +₁ i₁)) ∘ f , ((π₂ +₁ idC) ∘ i₂) ∘ h ])#ᵇ) ≈⟨ #ᵇ-resp-≈ ([]-cong₂ assoc assoc) ⟩
|
||||
(([ (π₂ +₁ idC) ∘ (idC +₁ i₁) ∘ f , (π₂ +₁ idC) ∘ i₂ ∘ h ])#ᵇ) ≈⟨ sym (#ᵇ-resp-≈ ∘[]) ⟩
|
||||
((π₂ +₁ idC) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ])#ᵇ ∎
|
||||
|
||||
--*
|
||||
-- Here follows the proof of equivalence for unguarded and Id-guarded Elgot-Algebras
|
||||
|
|
Loading…
Reference in a new issue