My Yoneda Lemma

Stream: general

[Luc Duponcheel]

Hello folks,

Here I am again with a technical question.

I have, temporarily, put my PSBP work "on hold".

FYI, I will be presenting it during the ITP 2025 lean workshop.

I have two other GitHub projects (yoneda and timeHybrids) that I want to convert to Lean.

They are more mathematics related than programming related.

I hope that, one day, they will be part of the famous MathLib project.

I am already preparing a "quick and dirty", "very low profile" version of my yoneda project in Lean.

Of course, the idea is to, eventually, use MathLib definitions instead of my own definitions.

I hope that I will have time to show it to some interested persons at the workshop.

See https://github.com/LucDuponcheelAtGitHub/yoneda for the project (in Scala).

The timeHybrids project is more challenging.

That being said (thx for keeping on reading) ... .

I encountered yet another "beginner issue".

It is related to the line in comments in the code below.

I define (on line 231) class PreFunctionalCategory.
It has a member ν (on line 247) that corresponds member ν (on line 134) of class PreTriple.

My question is:

can I avoid the error message

Parent type mismatch: has type
  Functor morphism morphism (GlobalElement morphism)
but is expected to have type
  Functor function morphism Id

when (on line 235) I want to extend PreTriple morphism (GlobalElement morphism) ?

Agreed, there are two Functors involved, but, there must be some way out, no?

Code listing

namespace Yoneda

#eval "- begin -"

abbrev function α β := α → β

class Identity
  (morphism : Type → Type → Type) where

    ι (α : Type) :
      morphism α α

export Identity (ι)

class Sequential
  (morphism : Type → Type → Type) where

    andThen (α β γ : Type) :
      morphism α β → morphism β γ → morphism α γ

export Sequential (andThen)

class Category
  (morphism : Type → Type → Type) extends
      Identity morphism
    , Sequential morphism

 class CategoryLaws
  (morphism : Type → Type → Type)
  (_ : Category morphism) : Prop where

  category_left_identity
      (αmβ : morphism α β) :
    (andThen α α β (ι α) αmβ) =
      αmβ

  category_right_identity
      (αmβ : morphism α β) :
    (andThen α β β αmβ (ι β)) =
      αmβ

  category_associativity
      (αmβ : morphism α β)
      (βmγ : morphism β γ)
      (γmδ : morphism γ δ) :
    (andThen α γ δ (andThen α β γ αmβ βmγ) γmδ) =
      (andThen α β δ αmβ (andThen β γ δ βmγ γmδ))

export CategoryLaws (
  category_right_identity
  category_left_identity
  category_associativity
  )

attribute [simp]
  category_right_identity
  category_left_identity
  category_associativity

class Functor
  (fromMorphism : Type → Type → Type)
  (toMorphism : Type → Type → Type)
  (morphed : Type → Type) where

    ζ :
      fromMorphism α β →
      toMorphism (morphed α) (morphed β)

class FunctorLaws
    (fromMorphism : Type → Type → Type)
    (toMorphism : Type → Type → Type)
    (morphed : Type → Type)
    (fromCategory : Category fromMorphism)
    (toCategory : Category toMorphism)
    (functor : Functor fromMorphism toMorphism morphed)
    : Prop where

  functor_identity :
    functor.ζ (fromCategory.ι α) =
      toCategory.ι (morphed α)

  functor_sequential :
    functor.ζ (andThen α β γ αmβ βmγ) =
      andThen (morphed α) (morphed β) (morphed γ)
        (functor.ζ αmβ) (functor.ζ βmγ)

export FunctorLaws (
  functor_identity
  functor_sequential
)

attribute [simp]
  functor_identity
  functor_sequential

class NaturalTransformation
  (fromMorphism : Type → Type → Type)
  (toMorphism : Type → Type → Type)
  (fromMorphed : Type → Type)
  (toMorphed : Type → Type) where

    τ : (ω : Type) →
        toMorphism (fromMorphed ω) (toMorphed ω)

 class NaturalTransformationLaws
  (fromMorphism : Type → Type → Type)
  (toMorphism : Type → Type → Type)
  (fromMorphed : Type → Type)
  (toMorphed : Type → Type)
  (toCategory : Category toMorphism)
  (fromFunctor :
    Functor fromMorphism toMorphism fromMorphed)
  (toFunctor :
    Functor fromMorphism toMorphism toMorphed) : Prop where

    naturalTransformation_natural
        (αfmβ : fromMorphism α β)
        (τ : (ω : Type) →
             toMorphism (fromMorphed ω) (toMorphed ω)):
      andThen
        (fromMorphed α) (toMorphed α) (toMorphed β)
        (τ α) (toFunctor.ζ αfmβ) =
        andThen
          (fromMorphed α) (fromMorphed β) (toMorphed β)
          (fromFunctor.ζ αfmβ) (τ β)

export NaturalTransformationLaws (
  naturalTransformation_natural
  )

attribute [simp]
  naturalTransformation_natural

class PreTriple
    (morphism : Type → Type → Type)
    (morphed : Type → Type) extends
  Functor morphism morphism morphed where

    ν :
      (ω : Type) →
      morphism ω (morphed ω)

class PreTripleLaws
  (morphism : Type → Type → Type)
  (morphed : Type → Type)
  (category : Category morphism)
  (preTriple : PreTriple morphism morphed)
  (αfmβ : morphism α β) : Prop where

    preTriple_natural
        (αfmβ : morphism α β) :
      andThen
        α (morphed α) (morphed β)
        (preTriple.ν α) (preTriple.ζ αfmβ) =
        andThen
          α β (morphed β)
          αfmβ (preTriple.ν β)

export PreTripleLaws (
  preTriple_natural
)

attribute [simp]
  preTriple_natural

class Triple
  (morphism : Type → Type → Type)
  (morphed : Type → Type) extends
    PreTriple morphism morphed where

      μ :
        (ω : Type) →
        morphism (morphed (morphed ω)) (morphed ω)

class TripleLaws
  (morphism : Type → Type → Type)
  (morphed : Type → Type)
  (category : Category morphism)
  (triple : Triple morphism morphed)
  (αfmβ : morphism α β) : Prop where

    triple_natural
        (αfmβ : morphism α β) :
      andThen
        (morphed (morphed α)) (morphed α) (morphed β)
        (triple.μ α) (triple.ζ αfmβ) =
        andThen
          (morphed (morphed α)) (morphed (morphed β)) (morphed β)
          ((triple.ζ ∘ triple.ζ) αfmβ) (triple.μ β)

    triple_left_identity :
      category.ι (morphed α) =
        andThen
          (morphed α) (morphed (morphed α)) (morphed α)
          (triple.ν (morphed α)) (triple.μ α)

    triple_right_identity :
      category.ι (morphed α) =
        andThen
          (morphed α) (morphed (morphed α)) (morphed α)
          (triple.ζ (triple.ν α)) (triple.μ α)

    triple_associativity :
       andThen
          (morphed (morphed (morphed α)))
          (morphed (morphed α))
          (morphed α)
          (triple.μ (morphed α)) (triple.μ α) =
        andThen
          (morphed (morphed (morphed α)))
          (morphed (morphed α))
          (morphed α)
          (triple.ζ (triple.μ α)) (triple.μ α)


export TripleLaws (
  triple_natural
  triple_left_identity
  triple_associativity
  )

attribute [simp]
  triple_natural
  triple_left_identity
  triple_associativity

abbrev GlobalElement
    (morphism : Type → Type → Type) : Type → Type :=
  λ α => morphism Unit α

class PreFunctionalCategory
  (morphism : Type → Type → Type) extends
      Category morphism
    , Functor function morphism Id
    -- , PreTriple morphism (GlobalElement morphism)
    where

  function2morphism :
    function α β → morphism α β := ζ

  global :
    (ω : Type) →
    function ω (GlobalElement morphism ω) :=
      λ _ =>
        λ z => function2morphism (λ _ => z)

  ν :
    (ω : Type) →
    morphism ω (GlobalElement morphism ω) :=
      λ ω =>
        function2morphism (global ω)

class FunctionalCategory
  (morphism : Type → Type → Type) extends
    PreFunctionalCategory morphism where

      μ :
        morphism
          (morphism Unit (GlobalElement morphism ω))
          (GlobalElement morphism ω)

def yonedaFunctor
  (_ : Category morphism) :
    (ω : Type) →
    morphism α β → function (morphism ω α) (morphism ω β) :=
      λ ω =>
        λ αmβ ωmα  => andThen ω α β ωmα αmβ

def yonedaEndoFunctor
  (preFunctionalCategory : PreFunctionalCategory morphism) :
    (ω : Type) →
    morphism α β → morphism (morphism ω α) (morphism ω β) :=
    λ ω =>
      preFunctionalCategory.function2morphism ∘
        λ αmβ ωmα => andThen ω α β ωmα αmβ

def globaElementFunctor
  (preFunctionalCategory : PreFunctionalCategory morphism) :
    morphism α β →
    morphism
      (GlobalElement morphism α)
      (GlobalElement morphism β) :=
      yonedaEndoFunctor preFunctionalCategory Unit

#eval "-- end --"

end Yoneda

[Luc Duponcheel]

FYI

For arbitrary categories, the Yoneda lemma deals with functors from (arbitrary category) morphisms to (Set category) functions. The Yoneda lemma is pointful (i.e. deals with elements of sets).

The idea behind my "lemma" is the following.

What I call functional categories, are categories for which there exists a functor from (Set category) functions to (functional category) morphisms.

Composing a functor from (functional category) morphisms to (Set category) functions with that functor from (Set category) functions to (functional category) morphisms yields an endofunctor from (functional category) morphisms to (functional category) morphisms.

My "lemma" is a pointfree Yoneda-like lemma for such endofunctors.