Skip to content

Commit d3a1489

Browse files
shaoweilinclaude
andcommitted
Add section dividers and clean up slide styling
- Add section divider slides to Categories tutorial using state attribute - Replace backgroundColor hack with state := some "title-slide" for title and thank-you slides across all tutorials - Use state := some "section-divider" for section dividers (proper VersoSlides approach using data-state attribute) - Consolidate repeated CSS colors into named variables - Simplify CSS to closely follow upstream ETAPSTutorial2026 structure - Add --baif-green (logo color) and --baif-green-dark color scheme Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
1 parent 3563005 commit d3a1489

7 files changed

Lines changed: 110 additions & 106 deletions

File tree

Categories/Basic.lean

Lines changed: 26 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -9,13 +9,21 @@ set_option linter.unusedVariables false
99
# Category Theory
1010

1111
%%%
12-
backgroundColor := some "#22C55E"
12+
state := some "title-slide"
1313
%%%
1414

1515
From Sets to Categories
1616

1717
Beneficial AI Foundation
1818

19+
# Material → Structural
20+
21+
%%%
22+
state := some "section-divider"
23+
%%%
24+
25+
Rethinking mathematical foundations
26+
1927
# Sets, Elements, and Functions
2028

2129
In set theory, we work with three concepts:
@@ -64,6 +72,14 @@ $$`A : \mathbb{R}^n \to \mathbb{R}^m`
6472

6573
We want a *coordinate-free* view of linear algebra.
6674

75+
# Monoids → Categories
76+
77+
%%%
78+
state := some "section-divider"
79+
%%%
80+
81+
From partial to total structure
82+
6783
# Square Matrices Form a Monoid
6884

6985
When input and output dimensions are the *same*, the linear maps form a *monoid*:
@@ -147,6 +163,14 @@ A ───→ B ───→ C
147163
- Objects: $`A`, $`B`, $`C`
148164
- Morphisms: $`f`, $`g`, $`g \circ f`, and identities
149165

166+
# Representations and Semantics
167+
168+
%%%
169+
state := some "section-divider"
170+
%%%
171+
172+
Embedding categories into Sets
173+
150174
# Representing Categories
151175

152176
Given a small category $`\mathcal{C}`, can we *represent* it (or its opposite) using sets and functions?
@@ -201,7 +225,7 @@ Instead of asking "what are the elements?", we ask:
201225
# Thank You
202226

203227
%%%
204-
backgroundColor := some "#22C55E"
228+
state := some "title-slide"
205229
%%%
206230

207231
*Beneficial AI Foundation*

Categories/outline.md

Lines changed: 17 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,19 @@
1-
0. title page
2-
1. from set theory as "sets, elements and functions", to thinking of elements as functions from * to a set, so we now only have "sets and functions".
3-
2. in programming languages and type theory, types are not collections of elements, but a symbol with constructors (functions into the type). In Nat example, say that Nat is
1+
* title page
2+
3+
# Material -> Structural
4+
* from set theory as "sets, elements and functions", to thinking of elements as functions from * to a set, so we now only have "sets and functions".
5+
* in programming languages and type theory, types are not collections of elements, but a symbol with constructors (functions into the type). In Nat example, say that Nat is
46
freely generated by these constructors.
5-
3. in algebra, we think of matrices as linear maps (functions) between fixed dimensional spaces. If input and output dimensions are the same, then we have the monoid of square matrices. But if input/output dims are different, they don't form a monoid because multiplication can fail.
6-
4. Instead, they form a category, with natural numbers as objects, and the matrices as morphisms. you can only "multiply" or compose them if the dimensions match up
7-
5. What is a category? Talk about $C^{op}$ the opposite category.
8-
6. Category theory is not just about "sets and functions", but any abstract structure has some notion of "objects and morphisms". Give an example of a small category, generated from a graph.
9-
7. Given a small category $C$, we often ask if it can be "represented" by some sets and functions. In fact, we have many "functors" from C^{op} to the category of Sets that preserves the structure of C^{op} (and therefore of $C$). Pick some object a in C, and map all objects $b$ in $C$ to the set of morphisms $C[b,a]$ from b to a. Describe map on morphisms. A functor C^{op} -> Set is also called a presheaf.
10-
7. what is a functor?
11-
8. Similar to Cayley's theorem in group theory, that any finite group can be represented by a matrix group. What is Yoneda embedding?
7+
* in algebra, we think of matrices as linear maps (functions) between fixed dimensional spaces.
8+
9+
# Monoids -> Categories
10+
* For linear maps, If input and output dimensions are the same, then we have the monoid of square matrices. But if input/output dims are different, they don't form a monoid because multiplication can fail.
11+
* Instead, they form a category, with natural numbers as objects, and the matrices as morphisms. you can only "multiply" or compose them if the dimensions match up
12+
* What is a category? Talk about $C^{op}$ the opposite category.
13+
* Category theory is not just about "sets and functions", but any abstract structure has some notion of "objects and morphisms". Give an example of a small category, generated from a graph.
14+
15+
# Representations and Semantics
16+
* Given a small category $C$, we often ask if it can be "represented" by some sets and functions. In fact, we have many "functors" from C^{op} to the category of Sets that preserves the structure of C^{op} (and therefore of $C$). Pick some object a in C, and map all objects $b$ in $C$ to the set of morphisms $C[b,a]$ from b to a. Describe map on morphisms. A functor C^{op} -> Set is also called a presheaf.
17+
* what is a functor?
18+
* Similar to Cayley's theorem in group theory, that any finite group can be represented by a matrix group. What is Yoneda embedding?
1219

Double/Basic.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ set_option linter.unusedVariables false
99
# Double Categories
1010

1111
%%%
12-
backgroundColor := some "#22C55E"
12+
state := some "title-slide"
1313
%%%
1414

1515
Categories Internal to Cat
@@ -444,7 +444,7 @@ The double category $`\mathbf{Prof}` arises as $`\mathbf{Mnd}(\mathbf{Span})`!
444444
# Thank You
445445

446446
%%%
447-
backgroundColor := some "#22C55E"
447+
state := some "title-slide"
448448
%%%
449449

450450
*Beneficial AI Foundation*

Main.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -30,12 +30,12 @@ def postProcessSlides (outputDir : FilePath) (logoFile : String) (title : String
3030
let html := html.replace "<section data-transition=\"fade\">\n" s!"<section data-transition=\"fade\">\n {slideHeader}\n"
3131

3232
-- Transform title slide
33-
let titleSlideOld := s!"<section data-background-color=\"#22C55E\">\n <h2>\n {title}</h2>\n <p>\n {subtitle}</p>\n <p>\n {org}</p>\n </section>"
33+
let titleSlideOld := s!"<section data-state=\"title-slide\">\n <h2>\n {title}</h2>\n <p>\n {subtitle}</p>\n <p>\n {org}</p>\n </section>"
3434
let titleSlideNew := s!"<section class=\"title-slide\">\n <div class=\"top-area\"><img class=\"logo\" src=\"{logoFile}\" alt=\"BAIF Logo\"></div>\n <div class=\"thick-band\"><h1>{title}</h1>\n <div class=\"meta\"><strong>{subtitle}</strong></div>\n <div class=\"date\">{org}</div>\n </div></section>"
3535
let html := html.replace titleSlideOld titleSlideNew
3636

3737
-- Transform Thank You slide
38-
let thankSlideOld := s!"<section data-background-color=\"#22C55E\">\n <h2>\n Thank You</h2>\n <p>\n <strong>{org}</strong></p>\n <p>\n beneficialaifoundation.org\n</p>\n </section>"
38+
let thankSlideOld := s!"<section data-state=\"title-slide\">\n <h2>\n Thank You</h2>\n <p>\n <strong>{org}</strong></p>\n <p>\n beneficialaifoundation.org\n</p>\n </section>"
3939
let thankSlideNew := s!"<section class=\"title-slide\">\n <div class=\"top-area\"><img class=\"logo\" src=\"{logoFile}\" alt=\"BAIF Logo\"></div>\n <div class=\"thick-band\"><h1>Thank You</h1>\n <div class=\"meta\"><strong>{org}</strong><br><a href=\"https://beneficialaifoundation.org\" style=\"color:#bbf7d0;\">beneficialaifoundation.org</a></div>\n <div class=\"date\"></div>\n </div></section>"
4040
let html := html.replace thankSlideOld thankSlideNew
4141

Monads/Basic.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ set_option linter.unusedVariables false
99
# Monads
1010

1111
%%%
12-
backgroundColor := some "#22C55E"
12+
state := some "title-slide"
1313
%%%
1414

1515
In Mathematics and Programming
@@ -109,7 +109,7 @@ Given a monad `T` on `C`, the *Kleisli category* has:
109109
# Thank You
110110

111111
%%%
112-
backgroundColor := some "#22C55E"
112+
state := some "title-slide"
113113
%%%
114114

115115
*Beneficial AI Foundation*

SSProve/Basic.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ set_option linter.unusedVariables false
99
# SSProve
1010

1111
%%%
12-
backgroundColor := some "#22C55E"
12+
state := some "title-slide"
1313
%%%
1414

1515
Modular Cryptographic Proofs in Coq
@@ -456,7 +456,7 @@ Instead of trusting paper proofs, we can *verify* them.
456456
# Thank You
457457

458458
%%%
459-
backgroundColor := some "#22C55E"
459+
state := some "title-slide"
460460
%%%
461461

462462
*Beneficial AI Foundation*

0 commit comments

Comments
 (0)