Skip to content

Instantly share code, notes, and snippets.

@Taneb

Taneb/Distributive.agda

Created March 18, 2024 14:57
Show Gist options
  • Save Taneb/f3764425be3cb578ae2ff3feb6acb322 to your computer and use it in GitHub Desktop.
Save Taneb/f3764425be3cb578ae2ff3feb6acb322 to your computer and use it in GitHub Desktop.
Download ZIP
Recursion Schemes from Comonads in Agda
Raw
Distributive.agda
{-# OPTIONS --safe --without-K #-}
module Categories.Comonad.Distributive where
open import Categories.Category
open import Categories.Category.Construction.F-Algebras
open import Categories.Comonad
open import Categories.Functor
open import Categories.Functor.Algebra
open import Categories.Functor.DistributiveLaw
open import Categories.Functor.Properties
import Categories.Morphism.Reasoning
open import Categories.NaturalTransformation
open import Level
record DistributiveComonad {o ℓ e} (C : Category o ℓ e) (F : Endofunctor C) : Set (o ⊔ ℓ ⊔ e) where
open Category C
private module F = Functor F
field
comonad : Comonad C
open Comonad comonad public renaming (F to N; module F to N)
field
distrib : DistributiveLaw F N
module distrib = NaturalTransformation distrib
field
ε-distrib : ∀ {A} → ε.η (F.₀ A) ∘ distrib.η A ≈ F.₁ (ε.η A)
δ-distrib : ∀ {A} → δ.η (F.₀ A) ∘ distrib.η A ≈ N.₁ (distrib.η A) ∘ distrib.η (N.₀ A) ∘ F.₁ (δ.η A)
-- An F-distributive comonad lifts to a comonad on F-algebras
-- Do I even need this? I guess it's an interesting exercise
lifted : Comonad (F-Algebras F)
lifted = record
{ F = record
{ F₀ = λ X → record
{ A = N.₀ (F-Algebra.A X)
; α = N.₁ (F-Algebra.α X) ∘ distrib.η _
}
; F₁ = λ {A} {B} f → record
{ f = N.₁ (F-Algebra-Morphism.f f)
; commutes = glue′ ([ N ]-resp-square (F-Algebra-Morphism.commutes f)) (distrib.sym-commute (F-Algebra-Morphism.f f))
}
; identity = N.identity
; homomorphism = N.homomorphism
; F-resp-≈ = N.F-resp-≈
}
; ε = record
{ η = λ X → record
{ f = ε.η _
; commutes = glue◽◃ (ε.commute _) ε-distrib
}
; commute = λ f → ε.commute _
; sym-commute = λ f → ε.sym-commute _
}
; δ = record
{ η = λ X → record
{ f = δ.η _
; commutes = begin
δ.η (F-Algebra.A X) ∘ N.₁ (F-Algebra.α X) ∘ distrib.η (F-Algebra.A X) ≈⟨ extendʳ (δ.commute (F-Algebra.α X)) ⟩
N.₁ (N.₁ (F-Algebra.α X)) ∘ δ.η (F.₀ (F-Algebra.A X)) ∘ distrib.η (F-Algebra.A X) ≈⟨ refl⟩∘⟨ δ-distrib ⟩
N.₁ (N.₁ (F-Algebra.α X)) ∘ N.₁ (distrib.η (F-Algebra.A X)) ∘ distrib.η (N.₀ (F-Algebra.A X)) ∘ F.₁ (δ.η (F-Algebra.A X)) ≈⟨ pullˡ (Equiv.sym N.homomorphism) ⟩
N.₁ (N.₁ (F-Algebra.α X) ∘ distrib.η (F-Algebra.A X)) ∘ distrib.η (N.₀ (F-Algebra.A X)) ∘ F.₁ (δ.η (F-Algebra.A X)) ≈⟨ Category.sym-assoc C ⟩
(N.₁ (N.₁ (F-Algebra.α X) ∘ distrib.η (F-Algebra.A X)) ∘ distrib.η (N.₀ (F-Algebra.A X))) ∘ F.₁ (δ.η (F-Algebra.A X)) ∎
}
; commute = λ f → δ.commute _
; sym-commute = λ f → δ.sym-commute _
}
; assoc = Comonad.assoc comonad
; sym-assoc = Comonad.sym-assoc comonad
; identityˡ = Comonad.identityˡ comonad
; identityʳ = Comonad.identityʳ comonad
}
where
open HomReasoning
open Categories.Morphism.Reasoning C
Raw
Recursion.agda
{-# OPTIONS --safe --without-K #-}
open import Categories.Category
module Recursion {o ℓ e} (𝒞 : Category o ℓ e) where
open import Categories.Category.Construction.F-Algebras
open import Categories.Comonad.Distributive
open import Categories.Functor hiding (id)
open import Categories.Functor.Algebra
open import Categories.Functor.Properties
open import Categories.Morphism.Reasoning 𝒞
open import Categories.Object.Initial
open import Function.Base using (_$_)
open Category 𝒞
open HomReasoning
------------------------------------------------------------------------
-- Catamorphisms
module _ {F : Endofunctor 𝒞} (⊥ : Initial (F-Algebras F)) where
private
module F = Functor F
module ⊥ = Initial ⊥
module ⊥⊥ = F-Algebra ⊥.⊥
module ⊥! {A} = F-Algebra-Morphism (⊥.! {A})
module _ {A} (φ : F-Algebra-on F A) where
private
X : F-Algebra F
X = record { α = φ }
cata : ⊥⊥.A ⇒ A
cata = ⊥!.f {X}
cata-cancel : cata ∘ ⊥⊥.α ≈ φ ∘ F.₁ cata
cata-cancel = ⊥!.commutes {X}
cata-unique : (f : ⊥⊥.A ⇒ A) → f ∘ ⊥⊥.α ≈ φ ∘ F.₁ f → cata ≈ f
cata-unique f f-cancel = ⊥.!-unique record { commutes = f-cancel }
cata-reflect : cata ⊥⊥.α ≈ id
cata-reflect = cata-unique ⊥⊥.α id $ begin
id ∘ ⊥⊥.α ≈⟨ id-comm-sym ⟩
⊥⊥.α ∘ id ≈˘⟨ refl⟩∘⟨ F.identity ⟩
⊥⊥.α ∘ F.₁ id ∎
cata-fuse : ∀ {A B} (φ : F-Algebra-on F A) (ψ : F-Algebra-on F B) (f : A ⇒ B) → f ∘ φ ≈ ψ ∘ F.₁ f → f ∘ cata φ ≈ cata ψ
cata-fuse φ ψ f prop = Equiv.sym $ cata-unique ψ (f ∘ cata φ) $ begin
(f ∘ cata φ) ∘ ⊥⊥.α ≈⟨ pullʳ (cata-cancel φ) ⟩
f ∘ (φ ∘ F.₁ (cata φ)) ≈⟨ pullˡ prop ⟩
(ψ ∘ F.₁ f) ∘ F.₁ (cata φ) ≈⟨ pullʳ (Equiv.sym F.homomorphism) ⟩
ψ ∘ F.₁ (f ∘ cata φ) ∎
-- TODO: cata-absorb
module Generic (N : DistributiveComonad 𝒞 F) where
module N = DistributiveComonad N
open N using (module distrib; module ε; module δ)
¡ : ⊥⊥.A ⇒ N.N.₀ ⊥⊥.A
¡ = cata (N.N.₁ ⊥⊥.α ∘ distrib.η ⊥⊥.A)
module _ {A} (φ : F-Algebra-on F A) where
ε-cata : ε.η A ∘ cata (N.N.₁ φ ∘ distrib.η A) ≈ cata φ
ε-cata = cata-fuse (N.N.₁ φ ∘ distrib.η A) φ (ε.η A) $ glue◽◃ (ε.commute φ) N.ε-distrib
δ-cata : δ.η A ∘ cata (N.N.₁ φ ∘ distrib.η A) ≈ cata (N.N.₁ (N.N.₁ φ ∘ distrib.η A) ∘ distrib.η (N.N.₀ A))
δ-cata = cata-fuse (N.N.₁ φ ∘ distrib.η A) (N.N.₁ (N.N.₁ φ ∘ distrib.η A) ∘ distrib.η (N.N.₀ A)) (δ.η A) $ begin
δ.η A ∘ N.N.₁ φ ∘ distrib.η A ≈⟨ pullˡ (δ.commute φ) ⟩
(N.N.₁ (N.N.₁ φ) ∘ δ.η (F.₀ A)) ∘ distrib.η A ≈⟨ pullʳ N.δ-distrib ⟩
N.N.₁ (N.N.₁ φ) ∘ N.N.₁ (distrib.η A) ∘ distrib.η (N.N.₀ A) ∘ F.₁ (δ.η A) ≈⟨ pullˡ (Equiv.sym N.N.homomorphism) ⟩
N.N.₁ (N.N.₁ φ ∘ distrib.η A) ∘ distrib.η (N.N.₀ A) ∘ F.₁ (δ.η A) ≈⟨ sym-assoc ⟩
(N.N.₁ (N.N.₁ φ ∘ distrib.η A) ∘ distrib.η (N.N.₀ A)) ∘ F.₁ (δ.η A) ∎
N-cata-¡ : N.N.₁ (cata φ) ∘ ¡ ≈ cata (N.N.₁ φ ∘ distrib.η A)
N-cata-¡ = cata-fuse (N.N.₁ ⊥⊥.α ∘ distrib.η ⊥⊥.A) (N.N.₁ φ ∘ distrib.η A) (N.N.₁ (cata φ)) $ begin
N.N.₁ (cata φ) ∘ N.N.₁ ⊥⊥.α ∘ distrib.η ⊥⊥.A ≈⟨ extendʳ ([ N.N ]-resp-square (cata-cancel φ)) ⟩
N.N.₁ φ ∘ N.N.₁ (F.₁ (cata φ)) ∘ distrib.η ⊥⊥.A ≈⟨ refl⟩∘⟨ distrib.sym-commute (cata φ) ⟩
N.N.₁ φ ∘ distrib.η A ∘ F.₁ (N.N.₁ (cata φ)) ≈⟨ sym-assoc ⟩
(N.N.₁ φ ∘ distrib.η A) ∘ F.₁ (N.N.₁ (cata φ)) ∎
ε-¡ : ε.η ⊥⊥.A ∘ ¡ ≈ id
ε-¡ = ε-cata ⊥⊥.α ○ cata-reflect
δ-¡ : δ.η ⊥⊥.A ∘ ¡ ≈ N.N.₁ ¡ ∘ ¡
δ-¡ = δ-cata ⊥⊥.α ○ Equiv.sym (N-cata-¡ (N.N.₁ ⊥⊥.α ∘ distrib.η ⊥⊥.A))
private
-- cokleisli stuff
-- TODO: just import this or define distributive cokleisli triples properly
_† : ∀ {A B} → N.N.₀ A ⇒ B → N.N.₀ A ⇒ N.N.₀ B
f † = N.N.₁ f ∘ δ.η _
ε-† : ∀ {A B} (f : N.N.₀ A ⇒ B) → ε.η B ∘ f † ≈ f
ε-† f = pullˡ (ε.commute f) ○ cancelʳ N.identityʳ
†-ε : ∀ {A} → ε.η A † ≈ id
†-ε = N.identityˡ
_‡ : ∀ {A B} → F.₀ (N.N.₀ A) ⇒ B → F.₀ (N.N.₀ A) ⇒ N.N.₀ B
φ ‡ = N.N.₁ φ ∘ distrib.η (N.N.₀ _) ∘ F.₁ (δ.η _)
lemma₁₄ : ∀ {A B} {φ : F.₀ (N.N.₀ A) ⇒ B} → ε.η B ∘ φ ‡ ≈ φ
lemma₁₄ {A} {B} {φ} = begin
ε.η B ∘ N.N.₁ φ ∘ distrib.η (N.N.₀ A) ∘ F.₁ (δ.η A) ≈⟨ pullˡ (ε.commute φ) ⟩
(φ ∘ ε.η (F.₀ (N.N.₀ A))) ∘ distrib.η (N.N.₀ A) ∘ F.₁ (δ.η A) ≈⟨ assoc²γβ ⟩
(φ ∘ ε.η (F.₀ (N.N.₀ A)) ∘ distrib.η (N.N.₀ A)) ∘ F.₁ (δ.η A) ≈⟨ pushˡ (∘-resp-≈ʳ N.ε-distrib) ⟩
φ ∘ F.₁ (ε.η (N.N.₀ A)) ∘ F.₁ (δ.η A) ≈⟨ elimʳ ([ F ]-resp-∘ N.identityʳ ○ F.identity) ⟩
φ ∎
lemma₁₅ : ∀ {A B C} {φ : F.₀ (N.N.₀ A) ⇒ B} {f : N.N.₀ B ⇒ C} → f † ∘ φ ‡ ≈ (f ∘ φ ‡) ‡
lemma₁₅ {A} {B} {C} {φ} {f} = begin
f † ∘ φ ‡ ≡⟨⟩
(N.N.₁ f ∘ δ.η B) ∘ (N.N.₁ φ ∘ distrib.η (N.N.₀ A) ∘ F.₁ (δ.η A)) ≈⟨ assoc²γδ ⟩
N.N.₁ f ∘ (δ.η B ∘ N.N.₁ φ) ∘ (distrib.η (N.N.₀ A) ∘ F.₁ (δ.η A)) ≈⟨ refl⟩∘⟨ δ.commute φ ⟩∘⟨refl ⟩
N.N.₁ f ∘ (N.N.₁ (N.N.₁ φ) ∘ δ.η (F.₀ (N.N.₀ A))) ∘ (distrib.η (N.N.₀ A) ∘ F.₁ (δ.η A)) ≈⟨ ∘-resp-≈ʳ assoc²γδ ○ sym-assoc ⟩
(N.N.₁ f ∘ N.N.₁ (N.N.₁ φ)) ∘ (δ.η (F.₀ (N.N.₀ A)) ∘ distrib.η (N.N.₀ A)) ∘ F.₁ (δ.η A) ≈⟨ Equiv.sym N.N.homomorphism ⟩∘⟨ N.δ-distrib ⟩∘⟨refl ⟩
N.N.₁ (f ∘ N.N.₁ φ) ∘ (N.N.₁ (distrib.η (N.N.₀ A)) ∘ distrib.η (N.N.₀ (N.N.₀ A)) ∘ F.₁ (δ.η (N.N.₀ A))) ∘ F.₁ (δ.η A) ≈⟨ ∘-resp-≈ʳ assoc²βε ○ sym-assoc ⟩
(N.N.₁ (f ∘ N.N.₁ φ) ∘ N.N.₁ (distrib.η (N.N.₀ A))) ∘ distrib.η (N.N.₀ (N.N.₀ A)) ∘ (F.₁ (δ.η (N.N.₀ A)) ∘ F.₁ (δ.η A)) ≈⟨ [ N.N ]-resp-∘ assoc ⟩∘⟨ refl⟩∘⟨ [ F ]-resp-square N.assoc ⟩
N.N.₁ (f ∘ N.N.₁ φ ∘ distrib.η (N.N.₀ A)) ∘ distrib.η (N.N.₀ (N.N.₀ A)) ∘ (F.₁ (N.N.₁ (δ.η A)) ∘ F.₁ (δ.η A)) ≈⟨ refl⟩∘⟨ pullˡ (distrib.commute (δ.η A)) ⟩
N.N.₁ (f ∘ N.N.₁ φ ∘ distrib.η (N.N.₀ A)) ∘ (N.N.₁ (F.₁ (δ.η A)) ∘ distrib.η (N.N.₀ A)) ∘ F.₁ (δ.η A) ≈⟨ assoc²δγ ⟩
(N.N.₁ (f ∘ N.N.₁ φ ∘ distrib.η (N.N.₀ A)) ∘ N.N.₁ (F.₁ (δ.η A))) ∘ distrib.η (N.N.₀ A) ∘ F.₁ (δ.η A) ≈⟨ [ N.N ]-resp-∘ assoc²βε ⟩∘⟨refl ⟩
N.N.₁ (f ∘ N.N.₁ φ ∘ distrib.η (N.N.₀ A) ∘ F.₁ (δ.η A)) ∘ distrib.η (N.N.₀ A) ∘ F.₁ (δ.η A) ≡⟨⟩
(f ∘ φ ‡) ‡ ∎
lemma₁₆ : ∀ {A B C} {f : N.N.₀ A ⇒ B} {ψ : F.₀ (N.N.₀ B) ⇒ C} → ψ ‡ ∘ F.₁ (f †) ≈ (ψ ∘ F.₁ (f †)) ‡
lemma₁₆ {A} {B} {C} {f} {ψ} = begin
ψ ‡ ∘ F.₁ (f †) ≡⟨⟩
(N.N.₁ ψ ∘ distrib.η (N.N.₀ B) ∘ F.₁ (δ.η B)) ∘ F.₁ (N.N.₁ f ∘ δ.η A) ≈⟨ assoc²βγ ⟩
(N.N.₁ ψ ∘ distrib.η (N.N.₀ B)) ∘ F.₁ (δ.η B) ∘ F.₁ (N.N.₁ f ∘ δ.η A) ≈⟨ refl⟩∘⟨ [ F ]-resp-square (extendʳ (δ.commute f)) ⟩
(N.N.₁ ψ ∘ distrib.η (N.N.₀ B)) ∘ F.₁ (N.N.₁ (N.N.₁ f)) ∘ F.₁ (δ.η (N.N.₀ A) ∘ δ.η A) ≈⟨ assoc²γδ ⟩
N.N.₁ ψ ∘ (distrib.η (N.N.₀ B) ∘ F.₁ (N.N.₁ (N.N.₁ f))) ∘ F.₁ (δ.η (N.N.₀ A) ∘ δ.η A) ≈⟨ refl⟩∘⟨ distrib.commute (N.N.₁ f) ⟩∘⟨ F.F-resp-≈ N.assoc ⟩
N.N.₁ ψ ∘ (N.N.₁ (F.₁ (N.N.₁ f)) ∘ distrib.η (N.N.₀ (N.N.₀ A))) ∘ F.₁ (N.N.₁ (δ.η A) ∘ δ.η A) ≈⟨ assoc²δγ ⟩
(N.N.₁ ψ ∘ N.N.₁ (F.₁ (N.N.₁ f))) ∘ (distrib.η (N.N.₀ (N.N.₀ A)) ∘ F.₁ (N.N.₁ (δ.η A) ∘ δ.η A)) ≈⟨ Equiv.sym N.N.homomorphism ⟩∘⟨ refl⟩∘⟨ F.homomorphism ⟩
N.N.₁ (ψ ∘ F.₁ (N.N.₁ f)) ∘ (distrib.η (N.N.₀ (N.N.₀ A)) ∘ F.₁ (N.N.₁ (δ.η A)) ∘ F.₁ (δ.η A)) ≈⟨ refl⟩∘⟨ extendʳ (distrib.commute (δ.η A)) ⟩
N.N.₁ (ψ ∘ F.₁ (N.N.₁ f)) ∘ (N.N.₁ (F.₁ (δ.η A)) ∘ distrib.η (N.N.₀ A) ∘ F.₁ (δ.η A)) ≈⟨ sym-assoc ⟩
(N.N.₁ (ψ ∘ F.₁ (N.N.₁ f)) ∘ N.N.₁ (F.₁ (δ.η A))) ∘ (distrib.η (N.N.₀ A) ∘ F.₁ (δ.η A)) ≈⟨ [ N.N ]-resp-∘ (pullʳ (Equiv.sym (F.homomorphism))) ⟩∘⟨refl ⟩
N.N.₁ (ψ ∘ F.₁ (N.N.₁ f ∘ δ.η A)) ∘ distrib.η (N.N.₀ A) ∘ F.₁ (δ.η A) ≡⟨⟩
(ψ ∘ F.₁ (f †)) ‡ ∎
lemma₁₈ : ∀ {A B} {f : F.₀ A ⇒ B} → N.N.₁ f ∘ distrib.η A ≈ (f ∘ F.₁ (ε.η A)) ‡
lemma₁₈ {A} {B} {f} = begin
N.N.₁ f ∘ distrib.η A ≈⟨ refl⟩∘⟨ introʳ F.identity ⟩
N.N.₁ f ∘ distrib.η A ∘ F.₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ F.F-resp-≈ (Equiv.sym N.identityˡ) ⟩
N.N.₁ f ∘ distrib.η A ∘ F.₁ (N.N.₁ (ε.η A) ∘ δ.η A) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ F.homomorphism ⟩
N.N.₁ f ∘ distrib.η A ∘ F.₁ (N.N.₁ (ε.η A)) ∘ F.₁ (δ.η A) ≈⟨ refl⟩∘⟨ extendʳ (distrib.commute (ε.η A)) ⟩
N.N.₁ f ∘ N.N.₁ (F.₁ (ε.η A)) ∘ distrib.η (N.N.₀ A) ∘ F.₁ (δ.η A) ≈⟨ pullˡ (Equiv.sym (N.N.homomorphism)) ⟩
N.N.₁ (f ∘ F.₁ (ε.η A)) ∘ distrib.η (N.N.₀ A) ∘ F.₁ (δ.η A) ≡⟨⟩
(f ∘ F.₁ (ε.η A)) ‡ ∎
lemma₁₉ : ∀ {A B} {φ : F.₀ (N.N.₀ A) ⇒ B} → δ.η B ∘ φ ‡ ≈ φ ‡ ‡
lemma₁₉ {A} {B} {φ} = begin
δ.η B ∘ φ ‡ ≡⟨⟩
δ.η B ∘ N.N.₁ φ ∘ distrib.η (N.N.₀ A) ∘ F.₁ (δ.η A) ≈⟨ extendʳ (δ.commute φ) ⟩
N.N.₁ (N.N.₁ φ) ∘ δ.η (F.₀ (N.N.₀ A)) ∘ distrib.η (N.N.₀ A) ∘ F.₁ (δ.η A) ≈⟨ refl⟩∘⟨ extendʳ N.δ-distrib ⟩
N.N.₁ (N.N.₁ φ) ∘ N.N.₁ (distrib.η (N.N.₀ A)) ∘ (distrib.η (N.N.₀ (N.N.₀ A)) ∘ F.₁ (δ.η (N.N.₀ A))) ∘ F.₁ (δ.η A) ≈⟨ sym-assoc ○ ∘-resp-≈ʳ assoc ⟩
(N.N.₁ (N.N.₁ φ) ∘ N.N.₁ (distrib.η (N.N.₀ A))) ∘ distrib.η (N.N.₀ (N.N.₀ A)) ∘ F.₁ (δ.η (N.N.₀ A)) ∘ F.₁ (δ.η A) ≈⟨ Equiv.sym N.N.homomorphism ⟩∘⟨ refl⟩∘⟨ [ F ]-resp-square N.assoc ⟩
N.N.₁ (N.N.₁ φ ∘ distrib.η (N.N.₀ A)) ∘ distrib.η (N.N.₀ (N.N.₀ A)) ∘ F.₁ (N.N.₁ (δ.η A)) ∘ F.₁ (δ.η A) ≈⟨ refl⟩∘⟨ extendʳ (distrib.commute (δ.η A)) ⟩
N.N.₁ (N.N.₁ φ ∘ distrib.η (N.N.₀ A)) ∘ N.N.₁ (F.₁ (δ.η A)) ∘ distrib.η (N.N.₀ A) ∘ F.₁ (δ.η A) ≈⟨ pullˡ ([ N.N ]-resp-∘ assoc) ⟩
N.N.₁ (N.N.₁ φ ∘ distrib.η (N.N.₀ A) ∘ F.₁ (δ.η A)) ∘ distrib.η (N.N.₀ A) ∘ F.₁ (δ.η A) ≡⟨⟩
φ ‡ ‡ ∎
module _ {A} (φ : F-Algebra-on (F ∘F N.N) A) where
lemma₂₂ : δ.η A ∘ cata (φ ‡) ≈ cata (N.N.₁ (φ ‡) ∘ distrib.η (N.N.₀ A))
lemma₂₂ = cata-fuse (N.N.₁ φ ∘ distrib.η (N.N.₀ A) ∘ F.₁ (δ.η A)) (N.N.₁ (φ ‡) ∘ distrib.η (N.N.₀ A)) (δ.η A) (lemma₁₉ ○ sym-assoc)
lemma₂₇ : δ.η A ∘ cata (φ ‡) ≈ N.N.₁ (cata (φ ‡)) ∘ ¡
lemma₂₇ = lemma₂₂ ○ Equiv.sym (N-cata-¡ (φ ‡))
-- Theorem 1
module _ {A} (φ : F-Algebra-on (F ∘F N.N) A) where
gcata : ⊥⊥.A ⇒ A
gcata = ε.η A ∘ cata (φ ‡)
gcata-cancel : gcata ∘ ⊥⊥.α ≈ φ ∘ F.₁ (N.N.₁ gcata ∘ ¡)
gcata-cancel = begin
gcata ∘ ⊥⊥.α ≈⟨ pullʳ (cata-cancel (φ ‡)) ⟩
ε.η A ∘ φ ‡ ∘ F.₁ (cata (φ ‡)) ≈⟨ pullˡ lemma₁₄ ⟩
φ ∘ F.₁ (cata (φ ‡)) ≈⟨ refl⟩∘⟨ F.F-resp-≈ (insertˡ N.identityˡ) ⟩
φ ∘ F.₁ (N.N.₁ (ε.η A) ∘ δ.η A ∘ cata (φ ‡)) ≈⟨ refl⟩∘⟨ F.F-resp-≈ (∘-resp-≈ʳ (lemma₂₇ φ)) ⟩
φ ∘ F.₁ (N.N.₁ (ε.η A) ∘ N.N.₁ (cata (φ ‡)) ∘ ¡) ≈⟨ refl⟩∘⟨ F.F-resp-≈ (pullˡ (Equiv.sym N.N.homomorphism)) ⟩
φ ∘ F.₁ (N.N.₁ gcata ∘ ¡) ∎
gcata-unique : (f : ⊥⊥.A ⇒ A) → f ∘ ⊥⊥.α ≈ φ ∘ F.₁ (N.N.₁ f ∘ ¡) → gcata ≈ f
gcata-unique f f-cancel = begin
gcata ≡⟨⟩
ε.η A ∘ cata (φ ‡) ≈⟨ refl⟩∘⟨ cata-unique (N.N.₁ φ ∘ distrib.η (N.N.₀ A) ∘ F.₁ (δ.η A)) (N.N.₁ f ∘ ¡) lemma ⟩
ε.η A ∘ N.N.₁ f ∘ ¡ ≈⟨ extendʳ (ε.commute f) ⟩
f ∘ ε.η ⊥⊥.A ∘ ¡ ≈⟨ elimʳ ε-¡ ⟩
f ∎
where
lemma : (N.N.₁ f ∘ ¡) ∘ ⊥⊥.α ≈ φ ‡ ∘ F.₁ (N.N.₁ f ∘ ¡)
lemma = begin
(N.N.₁ f ∘ ¡) ∘ ⊥⊥.α ≈⟨ extendˡ (cata-cancel (N.N.₁ ⊥⊥.α ∘ distrib.η ⊥⊥.A)) ⟩
(N.N.₁ f ∘ N.N.₁ ⊥⊥.α ∘ distrib.η ⊥⊥.A) ∘ F.₁ ¡ ≈⟨ extendʳ ([ N.N ]-resp-square f-cancel) ⟩∘⟨refl ⟩
(N.N.₁ φ ∘ N.N.₁ (F.₁ (N.N.₁ f ∘ ¡)) ∘ distrib.η ⊥⊥.A) ∘ F.₁ ¡ ≈⟨ ∘-resp-≈ʳ (distrib.sym-commute (N.N.₁ f ∘ ¡)) ⟩∘⟨refl ⟩
(N.N.₁ φ ∘ distrib.η (N.N.₀ A) ∘ F.₁ (N.N.₁ (N.N.₁ f ∘ ¡))) ∘ F.₁ ¡ ≈⟨ assoc²βγ ⟩
(N.N.₁ φ ∘ distrib.η (N.N.₀ A)) ∘ F.₁ (N.N.₁ (N.N.₁ f ∘ ¡)) ∘ F.₁ ¡ ≈⟨ refl⟩∘⟨ [ F ]-resp-∘ (pushˡ N.N.homomorphism ○ ∘-resp-≈ʳ (Equiv.sym δ-¡)) ⟩
(N.N.₁ φ ∘ distrib.η (N.N.₀ A)) ∘ F.₁ (N.N.₁ (N.N.₁ f) ∘ δ.η ⊥⊥.A ∘ ¡) ≈⟨ refl⟩∘⟨ F.F-resp-≈ (extendʳ (δ.sym-commute f)) ⟩
(N.N.₁ φ ∘ distrib.η (N.N.₀ A)) ∘ F.₁ (δ.η A ∘ N.N.₁ f ∘ ¡) ≈⟨ refl⟩∘⟨ F.homomorphism ⟩
(N.N.₁ φ ∘ distrib.η (N.N.₀ A)) ∘ F.₁ (δ.η A) ∘ F.₁ (N.N.₁ f ∘ ¡) ≈⟨ assoc²γβ ⟩
(N.N.₁ φ ∘ distrib.η (N.N.₀ A) ∘ F.₁ (δ.η A)) ∘ F.₁ (N.N.₁ f ∘ ¡) ≡⟨⟩
φ ‡ ∘ F.₁ (N.N.₁ f ∘ ¡) ∎
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment