Why can't I find any law violations for the NotQuiteCofree not-quite-comonad?
NotQuiteCofree
is pretty obviously distinct fromCofree
, so we would hope that there is at least somef
for whichNotQuiteCofree f
is not a comonad.
This does not follow. There is no contradiction between:
NotQuiteCofree f
is a comonad for every functorf
NotQuiteCofree f
is not a cofree comonad
"Generate a cofree comonad (from any functor)" is a strictly stronger requirement than "generate a comonad".
This was a doozy. I managed to get this working in Set
, but I suspect that we should be able to generalize. However, this proof uses the fact that we can compute nicely in Set
, so the general form is much, much, much more difficult.
Here's the proof in Agda, using the https://github.com/agda/agda-categories library:
{-# OPTIONS --without-K --safe #-}
module Categories.Comonad.Morphism where
open import Level
open import Data.Product hiding (_×_)
open import Categories.Category.Core
open import Categories.Comonad
open import Categories.Functor renaming (id to Id)
open import Categories.NaturalTransformation hiding (id)
open import Categories.Category.Cartesian
open import Categories.Category.Product
import Categories.Morphism.Reasoning as MR
open import Relation.Binary.PropositionalEquality
module Cofreeish-F {o ℓ e} ( : Category o ℓ e) (-Products : BinaryProducts ) where
open BinaryProducts -Products hiding (_⁂_)
open Category
open MR
open HomReasoning
Cofreeish : (F : Endofunctor ) → Endofunctor
Cofreeish F = record
{ F₀ = λ X → X × F₀ X
; F₁ = λ f → ⟨ f ∘ π₁ , F₁ f ∘ π₂ ⟩
; identity = λ {A} → unique id-comm (id-comm ○ ∘-resp-≈ˡ (⟺ identity)) ; homomorphism = λ {X} {Y} {Z} {f} {g} →
unique (pullˡ project₁ ○ pullʳ project₁ ○ ⟺ assoc) (pullˡ project₂ ○ pullʳ project₂ ○ pullˡ (⟺ homomorphism))
; F-resp-≈ = λ eq → unique (project₁ ○ ∘-resp-≈ˡ (⟺ eq)) (project₂ ○ ∘-resp-≈ˡ (F-resp-≈ (⟺ eq)))
}
where
open Functor F
Strong : (F : Endofunctor ) → Set (o ⊔ ℓ ⊔ e)
Strong F = NaturalTransformation (-×- ∘F (F ⁂ Id)) (F ∘F -×-)
open import Categories.Category.Instance.Sets
open import Categories.Category.Monoidal.Instance.Sets
module _ (c : Level) where
open Cofreeish-F (Sets c) Product.Sets-has-all
open Category (Sets c)
open MR (Sets c)
open BinaryProducts { = Sets c} Product.Sets-has-all
open ≡-Reasoning
strength : ∀ (F : Endofunctor (Sets c)) → Strong F
strength F = ntHelper record
{ η = λ X (fa , b) → F.F₁ (_, b) fa
; commute = λ (f , g) {(fa , b)} → trans (sym F.homomorphism) F.homomorphism
}
where
module F = Functor F
Cofreeish-Comonad : (F : Endofunctor (Sets c)) → Comonad (Sets c)
Cofreeish-Comonad F = record
{ F = Cofreeish F
; ε = ntHelper record
{ η = λ X → π₁
; commute = λ f → refl
}
; δ = ntHelper record
{ η = λ X → ⟨ id , F-strength.η _ ∘ Δ ∘ π₂ ⟩
; commute = λ f → cong₂ _,_ refl (trans (sym F.homomorphism) F.homomorphism)
}
; assoc = δ-assoc
; sym-assoc = sym δ-assoc
; identityˡ = ε-identityˡ
; identityʳ = ε-identityʳ
}
where
module F = Functor F
module F-strength = NaturalTransformation (strength F)
δ : ∀ X → X × F.F₀ X → (X × F.F₀ X) × F.F₀ (X × F.F₀ X)
δ _ = ⟨ id , F-strength.η _ ∘ Δ ∘ π₂ ⟩
ε : ∀ X → X × F.F₀ X → X
ε _ = π₁
δ-assoc : ∀ {X} → δ (X × F.F₀ X) ∘ δ X ≈ ⟨ id , F.F₁ (δ X) ∘ π₂ ⟩ ∘ δ X
δ-assoc {X} {(x , fx)} = cong₂ _,_ refl (trans (sym F.homomorphism) F.homomorphism)
ε-identityˡ : ∀ {X} → ⟨ ε X ∘ π₁ , F.F₁ (ε X) ∘ π₂ ⟩ ∘ δ X ≈ id
ε-identityˡ {X} {(x , fx)} = cong₂ _,_ refl (trans (sym F.homomorphism) F.identity)
ε-identityʳ : ∀ {X} → ε (X × F.F₀ X) ∘ δ X ≈ id
ε-identityʳ {X} {(x , fx)} = refl