module SOAS.Coalgebraic.Lift {T : Set} where
open import SOAS.Common
open import SOAS.Context {T}
open import SOAS.Variable
open import SOAS.Families.Core {T}
import SOAS.Families.Delta {T} as δ; open δ.Sorted
open import SOAS.Abstract.Hom {T}
import SOAS.Abstract.Box {T} as □ ; open □.Sorted
import SOAS.Abstract.Coalgebra {T} as →□ ; open →□.Sorted
open import SOAS.Coalgebraic.Map
open import SOAS.Coalgebraic.Strength
private
variable
Γ Δ Θ : Ctx
α : T
module _ {𝒫 : Familyₛ} (𝒫ᴮ : Coalgₚ 𝒫) where
open Coalgₚ 𝒫ᴮ
lift : (Ξ : Ctx) → Γ ~[ 𝒫 ]↝ Δ → (Ξ ∔ Γ) ~[ 𝒫 ]↝ (Ξ ∔ Δ)
lift ∅ σ v = σ v
lift (τ ∙ Ξ) σ new = η new
lift (τ ∙ Ξ) σ (old v) = r (lift Ξ σ v) old
lift₁ : {τ : T} → Γ ~[ 𝒫 ]↝ Δ → (τ ∙ Γ) ~[ 𝒫 ]↝ (τ ∙ Δ)
lift₁ {τ = τ} = lift ⌈ τ ⌋
rlift : (Ξ : Ctx) → Γ ↝ Δ → (Ξ ∔ Γ) ↝ (Ξ ∔ Δ)
rlift Ξ = lift ℐᴮ Ξ
δ:Strength : (Ξ : Ctx) → Strength (δF Ξ)
δ:Strength Ξ = record
{ str = λ 𝒫ᴮ 𝒳 h σ → h (lift 𝒫ᴮ Ξ σ)
; str-nat₁ = λ fᴮ⇒ h σ → cong h (dext (str-nat₁ Ξ fᴮ⇒ σ))
; str-nat₂ = λ f h σ → refl
; str-unit = λ 𝒳 h → cong h (dext (str-unit Ξ 𝒳))
; str-assoc = λ 𝒳 fᶜ h σ ς → cong h (dext (str-assoc Ξ 𝒳 fᶜ σ ς))
}
where
open ≡-Reasoning
open Coalgₚ
open Coalgₚ⇒
str-nat₁ : (Ξ : Ctx){𝒫 𝒬 : Familyₛ} {𝒫ᴮ : Coalgₚ 𝒫}
{𝒬ᴮ : Coalgₚ 𝒬} {f : 𝒬 ⇾̣ 𝒫}
→ Coalgₚ⇒ 𝒬ᴮ 𝒫ᴮ f
→ (σ : Γ ~[ 𝒬 ]↝ Δ)(v : ℐ α (Ξ ∔ Γ))
→ lift 𝒫ᴮ Ξ (f ∘ σ) v
≡ f (lift 𝒬ᴮ Ξ σ v)
str-nat₁ ∅ fᴮ⇒ σ v = refl
str-nat₁ (α ∙ Ξ) {𝒫ᴮ = 𝒫ᴮ} fᴮ⇒ σ new = sym (Coalgₚ⇒.⟨η⟩ fᴮ⇒)
str-nat₁ (α ∙ Ξ) {𝒫ᴮ = 𝒫ᴮ} {𝒬ᴮ}{f}fᴮ⇒ σ (old v) = begin
lift 𝒫ᴮ (α ∙ Ξ) (f ∘ σ) (old v)
≡⟨ congr (str-nat₁ Ξ fᴮ⇒ σ v) (λ - → r 𝒫ᴮ - old) ⟩
r 𝒫ᴮ (f (lift 𝒬ᴮ Ξ σ v)) old
≡˘⟨ ⟨r⟩ fᴮ⇒ ⟩
f (lift 𝒬ᴮ (α ∙ Ξ) σ (old v))
∎
str-unit : (Ξ : Ctx) (𝒳 : Familyₛ) (v : ℐ α (Ξ ∔ Γ))
→ lift ℐᴮ Ξ id v ≡ v
str-unit ∅ 𝒳 v = refl
str-unit (α ∙ Ξ) 𝒳 new = refl
str-unit (α ∙ Ξ) 𝒳 (old v) = cong old (str-unit Ξ 𝒳 v)
str-assoc : (Ξ : Ctx) (𝒳 : Familyₛ) {𝒫 𝒬 ℛ : Familyₛ}
{𝒫ᴮ : Coalgₚ 𝒫} {𝒬ᴮ : Coalgₚ 𝒬} {ℛᴮ : Coalgₚ ℛ}
{f : 𝒫 ⇾̣ 〖 𝒬 , ℛ 〗}
(fᶜ : Coalgebraic 𝒫ᴮ 𝒬ᴮ ℛᴮ f) (open Coalgebraic fᶜ)
(σ : Γ ~[ 𝒫 ]↝ Δ) (ς : Δ ~[ 𝒬 ]↝ Θ)(v : ℐ α (Ξ ∔ Γ))
→ lift ℛᴮ Ξ (λ u → f (σ u) ς) v
≡ lift 〖𝒫,𝒴〗ᴮ Ξ (f ∘ σ) v (lift 𝒬ᴮ Ξ ς)
str-assoc ∅ 𝒳 fᶜ σ ς v = refl
str-assoc (β ∙ Ξ) 𝒳 {𝒫ᴮ = 𝒫ᴮ}{𝒬ᴮ}{ℛᴮ} {f} fᶜ σ ς new = begin
η ℛᴮ new ≡˘⟨ f∘η ⟩
f (η 𝒫ᴮ new) (η 𝒬ᴮ) ≡⟨ eq-at-new refl ⟩
f (η 𝒫ᴮ new) (lift 𝒬ᴮ (β ∙ Ξ) ς) ∎
where open Coalgebraic fᶜ
str-assoc {Γ = Γ} (β ∙ Ξ) 𝒳 {𝒫 = 𝒫}{𝒬}{𝒫ᴮ = 𝒫ᴮ}{𝒬ᴮ}{ℛᴮ}{f} fᶜ σ ς (old v) =
begin
r ℛᴮ (lift ℛᴮ Ξ (λ u → f (σ u) ς) v) old
≡⟨ congr (str-assoc Ξ 𝒳 fᶜ σ ς v) (λ - → r ℛᴮ - old) ⟩
r ℛᴮ ( lift 〖𝒫,𝒴〗ᴮ Ξ (f ∘ σ) v (lift 𝒬ᴮ Ξ ς)) old
≡⟨ congr (str-nat₁ Ξ fᴮ⇒ (σ) v) (λ - → r ℛᴮ (- (lift 𝒬ᴮ Ξ ς)) old) ⟩
r ℛᴮ (f (lift 𝒫ᴮ Ξ σ v) (lift 𝒬ᴮ Ξ ς)) old
≡⟨ r∘f ⟩
f (lift 𝒫ᴮ Ξ σ v) (λ u → r 𝒬ᴮ (lift 𝒬ᴮ Ξ ς u) old)
≡˘⟨ congr (str-nat₁ Ξ fᴮ⇒ σ v) (λ - → - (λ u → r 𝒬ᴮ (lift 𝒬ᴮ Ξ ς u) old)) ⟩
lift 〖𝒫,𝒴〗ᴮ Ξ (f ∘ σ) v (λ u → r 𝒬ᴮ (lift 𝒬ᴮ Ξ ς u) old)
∎
where open Coalgebraic fᶜ renaming (ᴮ⇒ to fᴮ⇒)
module δ:Str Θ = Strength (δ:Strength Θ)
rlift-id : (𝒳 : Familyₛ)(Ξ : Ctx)(b : δ Ξ (□ 𝒳) α Γ)
→ b (rlift Ξ id) ≡ b id
rlift-id 𝒳 Ξ = Strength.str-unit (δ:Strength Ξ) 𝒳
lift-comp : {𝒫 𝒬 : Familyₛ}{𝒫ᴮ : Coalgₚ 𝒫}{𝒬ᴮ : Coalgₚ 𝒬}
(𝒳 : Familyₛ)(Ξ : Ctx){f : 𝒬 ⇾̣ 𝒫}
(fᴮ⇒ : Coalgₚ⇒ 𝒬ᴮ 𝒫ᴮ f)
(h : δ Ξ 〖 𝒫 , 𝒳 〗 α Γ) (σ : Γ ~[ 𝒬 ]↝ Δ)
→ h (lift 𝒫ᴮ Ξ (f ∘ σ))
≡ h (f ∘ lift 𝒬ᴮ Ξ σ)
lift-comp 𝒳 Ξ fᴮ⇒ h σ = Strength.str-nat₁ (δ:Strength Ξ) {𝒳 = 𝒳} fᴮ⇒ h σ
lift-assoc : {𝒫 𝒬 ℛ : Familyₛ}
{𝒫ᴮ : Coalgₚ 𝒫} {𝒬ᴮ : Coalgₚ 𝒬} {ℛᴮ : Coalgₚ ℛ}
(𝒳 : Familyₛ)(Ξ : Ctx) {f : 𝒫 ⇾̣ 〖 𝒬 , ℛ 〗}
(fᶜ : Coalgebraic 𝒫ᴮ 𝒬ᴮ ℛᴮ f)
(open Coalgebraic fᶜ)
(h : δ Ξ 〖 ℛ , 𝒳 〗 α Γ)
(σ : Γ ~[ 𝒫 ]↝ Δ) (ς : Δ ~[ 𝒬 ]↝ Θ)
→ h (lift ℛᴮ Ξ (λ v → f (σ v) ς))
≡ h (λ v → lift 〖𝒫,𝒴〗ᴮ Ξ (f ∘ σ) v (lift 𝒬ᴮ Ξ ς))
lift-assoc 𝒳 Ξ fᶜ h σ ς = Strength.str-assoc (δ:Strength Ξ) 𝒳 fᶜ h σ ς
lift-dist : {𝒫 𝒬 ℛ : Familyₛ}{𝒫ᴮ : Coalgₚ 𝒫}{𝒬ᴮ : Coalgₚ 𝒬}{ℛᴮ : Coalgₚ ℛ}
(𝒳 : Familyₛ){Ξ : Ctx}{f : 𝒫 ⇾̣ 〖 𝒬 , ℛ 〗}
(fᶜ : Coalgebraic 𝒫ᴮ 𝒬ᴮ ℛᴮ f)
(h : δ Ξ 〖 ℛ , 𝒳 〗 α Γ)
(σ : Γ ~[ 𝒫 ]↝ Δ) (ς : Δ ~[ 𝒬 ]↝ Θ)
→ h (lift ℛᴮ Ξ (λ v → f (σ v) ς))
≡ h (λ v → f (lift 𝒫ᴮ Ξ σ v) (lift 𝒬ᴮ Ξ ς))
lift-dist 𝒳 {Ξ} = Strength.str-dist (δ:Strength Ξ) 𝒳