Zulip Chat Archive

Stream: general

Topic: Cat theory example to learn from?


view this post on Zulip Daniel Donnelly (Aug 28 2019 at 15:20):

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.

view this post on Zulip Chris Hughes (Aug 28 2019 at 15:24):

import category_theory.category

open category_theory

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

view this post on Zulip Chris Hughes (Aug 28 2019 at 15:25):

X : C means X is an object in C.

view this post on Zulip Daniel Donnelly (Aug 28 2019 at 15:25):

What does Type* mean?

view this post on Zulip Daniel Donnelly (Aug 28 2019 at 15:25):

Klean closure?

view this post on Zulip Johan Commelin (Aug 28 2019 at 15:26):

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

view this post on Zulip Johan Commelin (Aug 28 2019 at 15:26):

maybe just use large_category for now.

view this post on Zulip Daniel Donnelly (Aug 28 2019 at 15:26):

that includes all categories?

view this post on Zulip Daniel Donnelly (Aug 28 2019 at 15:26):

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

view this post on Zulip Johan Commelin (Aug 28 2019 at 15:27):

@EnjoysMath Type* mean that C is a type.

view this post on Zulip Johan Commelin (Aug 28 2019 at 15:27):

Lean uses type theory in its foundations, see TPIL

view this post on Zulip Daniel Donnelly (Aug 28 2019 at 15:27):

I thought C : Type would accomplish that

view this post on Zulip Daniel Donnelly (Aug 28 2019 at 15:29):

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

view this post on Zulip Johan Commelin (Aug 28 2019 at 15:29):

Type* is Type u for a fresh univers u

view this post on Zulip Daniel Donnelly (Aug 28 2019 at 15:29):

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

view this post on Zulip Daniel Donnelly (Aug 28 2019 at 15:30):

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

view this post on Zulip Johan Commelin (Aug 28 2019 at 15:33):

You can add that later

view this post on Zulip Daniel Donnelly (Aug 28 2019 at 15:33):

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

view this post on Zulip Johan Commelin (Aug 28 2019 at 15:33):

Just use Type for now.

view this post on Zulip Daniel Donnelly (Aug 28 2019 at 15:33):

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

view this post on Zulip Daniel Donnelly (Aug 28 2019 at 15:35):

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

view this post on Zulip Daniel Donnelly (Aug 28 2019 at 15:37):

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

view this post on Zulip Daniel Donnelly (Aug 28 2019 at 15:38):

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

view this post on Zulip Daniel Donnelly (Aug 28 2019 at 15:38):

Finallly is variable declaration the formal term for this?

view this post on Zulip Daniel Donnelly (Aug 28 2019 at 15:38):

*formal vocabulary

view this post on Zulip Daniel Donnelly (Aug 28 2019 at 15:40):

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.

view this post on Zulip Daniel Donnelly (Aug 28 2019 at 15:45):

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.

view this post on Zulip Daniel Donnelly (Aug 28 2019 at 15:46):

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

view this post on Zulip Daniel Donnelly (Aug 28 2019 at 15:48):

I take back that lean should drive BananaCats

view this post on Zulip Daniel Donnelly (Aug 28 2019 at 15:48):

That would necessitate parsing of Lean!

view this post on Zulip Daniel Donnelly (Aug 28 2019 at 15:49):

I have to KISS keep it simple

view this post on Zulip Johan Commelin (Aug 28 2019 at 15:54):

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

view this post on Zulip Daniel Donnelly (Aug 28 2019 at 15:54):

Thx

view this post on Zulip Daniel Donnelly (Aug 28 2019 at 15:58):

{% 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

view this post on Zulip Scott Morrison (Aug 28 2019 at 23:33):

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)

view this post on Zulip Scott Morrison (Aug 28 2019 at 23:34):

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 ๐’ž

view this post on Zulip Scott Morrison (Aug 28 2019 at 23:37):

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...)


Last updated: May 08 2021 at 19:11 UTC