CoYoneda lemmas for endofunctors of functional categories.

Stream: general

[Luc Duponcheel]

Folks,

I would like to announce that I finished the proofs of my
Pointfree CoYoneda lemmas for endofunctors of functional categories.

Afaik the lemma's at the end are original mathematical results (the code is self-contained).

For the moment the formulations and the proofs are "low profile". Helping me making them more "high profile" (cfr. MathLib), as suggested in the beginning of the README.md file of the GitHub Repository, would be appreciated.

I cannot include the code because it consists of too many lines. You'll have to copy/paste the raw code.

[Joël Riou]

It seems what you define as Category/CategoryProperties is mostly what we call a concrete category. The only chance it might enter mathlib is that you use more standard terminology and do not duplicate existing definitions. In the current form of the code, I have absolutely no idea what is the statement that you have formalised.

[Luc Duponcheel]

Joël, thanks for the quick reply

I'll have a look at the concrete category code of Mathlib asap.
Of course I want to throw away my self contained supporting code.
The code is really a first approach to be sure that the proofs are correct.

As far as what I have proved, in short
(btc standing for binary type constructor, cfr. Category)
(utc standing for unary type constructor, cfr. Functor) :

The standard CoYoneda lemma for categories btc is about the relationship between,
on the one hand,
natural transformations between the CoYoneda functor, coYonedaFunctorOf s and function valued functors utc, and,
on the other hand,
values of type utc s.
See pointfulCoYonedaLemma1, lines 603-686

My two CoEndoYoneda lemmas for functional categories are about the relationship between,
on the one hand,
natural transformations between the CoEndoYoneda endoFunctor, coEndoYonedaFunctorOf s and endoFunctors utc, and,
on the other hand,
global values of type btc Unit (utc s),
resp. global values of type btc Unit (btc Unit (utc s)).
See pointfreeCoEndoYonedaLemma1, lines 1292-1510,
resp. pointfreeCoEndoYonedaLemma3, lines 1798-1991.

[Luc Duponcheel]

Joël, I am aware that my calc based proofs are long. That is one of the reasons why I hope to do better using simp using the capabilities of Mathlib. But first, I wanted to do everything manually, if only to have an idea which axioms I needed.
My work is not about writing an existing proof in Lean, but to use Lean to help me proving my (a.f.a.i.k.) new idea.

[Luc Duponcheel]

Joël, from the wiki page :

In mathematics, a concrete category is a category that is equipped with a faithful functor to the category of sets.

What I call a functional category is a category that is equipped with a functor from the category of sets.

I do not want to add structure to sets, I just want to treat functions as morphisms.

In functional programming functions are morphisms that are "effectfree programs" but there are other morphisms that are "effectful programs", for example, morphisms manipulating internal or external state.

[Joël Riou]

Ok, your Category/CategoryClasses look more like attempting to defining a category structure on a type C where C happens to be Type. But, I still have no idea what is the mathematical content of your file.

[Luc Duponcheel]

Joël,

It is always a bit challenging to try to understand something new.

The least one can require from a category btc to model functional programming
is that there is a functor from function, the category of functions, to btc.

The standard (Co)Yoneda lemma is about functors from btc to function.
They can then be composed with the functor from function, to btc above,
obtaining endofunctors.

No more functions involved, everything is pointfree.

So it is natural to ask yourself: is it possible to formulate and prove
a pointfree (Co)Yoneda lemma about endofunctors of such functional categories.

coYonedaLemma1 (mentioned in a previous reply) simply proves that
τ = σ,
where τ is the natural transformation morphism involved,
and σ is defined in terms of a value. It is a simplified version of
pointfulCoYonedaLemma1 using functional extension. funext

pointfreeCoYonedaLemma3 (mentioned in a previous reply) proves that
gₛₜ btc_s_t ≫ τ ≫ γν = gₛₜ btc_s_t ≫ σ,
where τ is the natural transformation morphism involved,
σ is defined in terms of a global value and gₛₜ btc_s_t
is a global value (actually a global morphism),
and γν is the neutral element of the triple globalTriple.
It is not possible to simplify it to
τ ≫ γν = σ since gₛₜ btc_s_t
is not a general enough. Maybe quotients of equivalence
relations can be used to simplify?

Similarly

pointfreeCoYonedaLemma4 (mentioned in a previous reply) proves that
gₛₜ btc_s_t ≫ τ = gₛₜ btc_s_t ≫ σ, wbere the proof now
also involves γμ, the multiplication of the triple globalTriple.
It is not possible to simplify it to
τ = σ for the same reason.

Hopefully this helps.

[Joël Riou]

I will not try to understand what you are trying to say if you continue to use confusing terminology.
One major problem with your code is that it is highly obfuscated: most of the definitions start with an extravagant number of let ... := in the statement itself, and as the proofs also start with a bunch of let ... :=, it is basically impossible to see where the statements are. Basically, anytime you need a let in a statement, this is a sign that there is a missing definition.

[Luc Duponcheel]

Joël, You have a valid point. I will do my best to extract the local let definitions and replace them with global def definitions. The (slight) advantage of using local let definitions is that they need less context, but, yes, the (more important) advantage of using global def definitions is reusability and less obfuscated code.

As far as terminology is concerned, I only used category, functor, natural transformation, triple and global value. Agreed I should, maybe, have used global element, but in the typed programming world value is more commonly used than element.

Do not get me wrong I highly appreciate your constructive feedback. It motivates me to improve my code. Thanks so much.

[Luc Duponcheel]

FYI

CoEndoYoneda02.lean in my repo now almost does not contain any local let definitions any more.

Less code, but, more complex, explicit, equalities.

BTW
No need to try to review the code at this point.
(Lean reviewed both CoEndoYoneda01.lean and CoEndoYoneda02.lean)

Starting from now on I am going (to try to) integrate the code with the Mathlib category library code. I may need some help. Like I already mentioned, It is always a bit challenging to try to understand something new (in my case that library is new for me).