Cat theory example to learn from?

Stream: general

[Daniel Donnelly]

Hi, I am in the middle of coding critical parts to BananaCats. I am confident enough now in Lean that I can start doing project-motivated learning, and my project is about category theory. So could someone point me to the simplest (takes least effort in the long-run to use) way of "defining a variable C, that is an abstract category?" And why not declare an object X in Ob(C) as well.

[Chris Hughes]

import category_theory.category

open category_theory

variables {C : Type*} [category C] (X : C)

[Chris Hughes]

X : C means X is an object in C.

[Daniel Donnelly]

What does Type* mean?

[Daniel Donnelly]

Klean closure?

[Johan Commelin]

@Chris Hughes You'll have some hidden universe variables that way...

[Johan Commelin]

maybe just use large_category for now.

[Daniel Donnelly]

that includes all categories?

[Daniel Donnelly]

I.e. does it mean not-neccessarily large category?

[Johan Commelin]

@EnjoysMath Type* mean that C is a type.

[Johan Commelin]

Lean uses type theory in its foundations, see TPIL

[Daniel Donnelly]

I thought C : Type would accomplish that

[Daniel Donnelly]

I will work with the Chris Hughes example for now, since I'm okay with any implications regarding Universes for now

[Johan Commelin]

Type* is Type u for a fresh univers u

[Daniel Donnelly]

Should BananaCats have a Universe setting as well, where needed?

[Daniel Donnelly]

That's as easy as adding a GUI field from my perspective

[Johan Commelin]

You can add that later

[Daniel Donnelly]

Category lives in Universe: [int spinbox] Use first free universe: [*]

[Johan Commelin]

Just use Type for now.

[Daniel Donnelly]

@Johan Commelin sure thing. I will use Type for now :)

[Daniel Donnelly]

I'ma use Jinja2 (a python library) for making a "create new category" template, and so on...

[Daniel Donnelly]

The question is, can I get away with generalizing the template to declaring a variable of a certain type?

[Daniel Donnelly]

And another question is what does the application in brackets [category C] do to the declaration?

[Daniel Donnelly]

Finallly is variable declaration the formal term for this?

[Daniel Donnelly]

*formal vocabulary

[Daniel Donnelly]

Btw, the comm to / from Lean VSCode will be 2-way, I.e. a change in the code which Bancats cares about will be detected and reflected in the PyQt5 app ("BananaCats"), and obviously vise versa is the typical usage.

[Daniel Donnelly]

To answer one question, I shouldn't generalize, as that would move more logic framework over to BananaCats by necessity, since I'd have to call multiple atomic calls, and organize them correctly. Whereas if I just do the hard coded script for Create a Category, and do the same for each thing, then I should be okay in finishing this.

[Daniel Donnelly]

If I need to generalize it should be done with lean code I think

[Daniel Donnelly]

I take back that lean should drive BananaCats

[Daniel Donnelly]

That would necessitate parsing of Lean!

[Daniel Donnelly]

I have to KISS keep it simple

[Johan Commelin]

@EnjoysMath [category C] means that C is endowed with the structure of a category.

[Daniel Donnelly]

Thx

[Daniel Donnelly]

{% if "category_theory.category" not in context.imported_names %}
    import category_theory.category
{% endif %}

{% if "category_theory" not in context.open_modules %}
    open category_theory
{% endif %}

variables {{{decl.name}} : {{decl.type}}} [category {{decl.name}}]

It's a Jinja2 template for declaring a variable an abstract category

[Scott Morrison]

If universe polymorphism doesn't matter to you (this is pretty much synonymous with "you're not trying to write library code"), then I'd recommend:

import category_theory.category

open category_theory

variables {C : Type} [small_category C] (X : C)

[Scott Morrison]

If universe polymorphism does matter to you, and you want the most general case (which in "real maths" means that you either have a small category, where the objects and morphisms live in the same universe, or a large category, where the objects live in a universe one higher than the morphisms, but in "Lean math", because we can't specify this dichotomy, the objects and morphisms just live in two entirely independent universes, I'd recommend:

import category_theory.category

universes v u
open category_theory

variables {C : Type u} [𝒞 : category.{v} C] (X : C)
include 𝒞

[Scott Morrison]

Here we need include𝒞because Lean's typeclass inference algorithm is not willing to pull in the instance C until it is sure that the universe parameter v is the desired one, and often it can't tell this without explicit universe annotations everywhere --- instead we just tell Lean to include 𝒞 as an argument to every definition that follows. This is a little dangerous, as you need to be careful to then explicitly omit it again if you write any functions that don't refer to C. (Such functions probably belong higher in the file, or in another file, in any case...)