2025–2026, spring semester, NKUA Type-theoretic (foundations of) Mathematics and Proof Assistants

Participation points

(See also the section Grading.)

The following are all the students that are enrolled in the course, as far as I know.

If you think your name should be on this list but isn’t (or it should not be but is) then let me know about it (msg on Zulip if you have access; email me if you don’t).

(ZP: Zulip Participation; CP: Class Participation.)

For your CP and ZP points to show up here make sure you have complete info on your profile on Zulip (especially course & photo, see the FAQ on Zulip).

Homework (HW)

• Homework is assigned here, and also during classes as well as in Zulip.
• Usually pink in the blackboard PDF indicates hw.
• Ideally students should also invent their own hw—and work on it.
• References to pages ⟦like this⟧ refer to the blackboard PDF.
• Prerequisites to hw below are indicated by a ▸. If you have not studied the specified prereq, you may skip this hw.
• hw stay point-active for 1 week, unless stated otherwise. However, all hw stay indefinitely active (but just for the glory of solving them), so do post your thoughts/solutions/comments even if it’s an older hw, especially if we have no solutions for it.

Inventory of cats 🐈

• 𝟘, 𝟙, 𝟚, 𝟛, …, 𝕟, …
• ℂ[𝒫], where 𝒫 is a proset; special cases:
  • (ℤ ; ∣)
  • (ℤ ; ≤)
  • (℘A ; ⊆)
  • (Prop ; ⊢)
• ℂ[ℳ], where ℳ is a monoid
• 𝐒𝐞𝐭, 𝐅𝐢𝐧𝐒𝐞𝐭, 𝐒𝐞𝐭𝐈𝐧𝐣
• 𝐌𝐚𝐠𝐦𝐚, 𝐒𝐞𝐦𝐢𝐠𝐫𝐨𝐮𝐩, 𝐌𝐨𝐧𝐨𝐢𝐝, 𝐆𝐫𝐨𝐮𝐩, 𝐀𝐛𝐞𝐥, 𝐑𝐢𝐧𝐠, Semilattice, 𝐋𝐚𝐭𝐭𝐢𝐜𝐞, 𝐁𝐝𝐋𝐚𝐭𝐭𝐢𝐜𝐞
• 𝐏𝐫𝐨𝐬𝐞𝐭, 𝐏𝐨𝐬𝐞𝐭, 𝐓𝐨𝐩
• 𝐅𝐢𝐞𝐥𝐝
• ℂ[𝙻], where 𝙻 is a typed programming language
• 𝐓𝐲𝐩𝐞𝐅𝐮𝐧, 𝐏𝐫𝐨𝐩𝐏𝐫𝐨𝐨𝐟𝐬
• 𝐂𝐚𝐭

¹ Hask is not really a category

2026-02-16 (hw0)

1. Send me an email asking for a Zulip invitation for this course.
2. Post a hello message on #cafe.

2026-02-24 (hw1)

1. Come up with a few typing statements of your own (like the ones we saw in class), using zero or more holes.
2. Do the pink stuff in the blackboards PDF. (From now on this is considered automatic hw after each update of the blackboard.)
3. Set theory ▸ What do you think the specification for the ordered-pair operator ⟨_,_⟩ mandates? (Don’t check your set theory books/notes. Try to come up with a specification that makes sense to you.)

2026-02-27 (hw2)

1. Discuss: For each of the connectives (∨,∧,…) on ⟦p. 12⟧ suggest:
   1. What it means to prove it: what should count as a proof of such a proposition?
   2. How such a proposition should be used: what are we allowed to do in a proof in which we have such a proposition (on our givens), that we would not be allowed to do it otherwise?
2. Describe some elements of the following types:
   1. ? : Nat → Nat
   2. ? : (Nat × Nat) → Nat
   3. ? : Nat × (Nat → Nat)
   4. ? : Person → Nat
   5. ? : (Nat → Nat) → (Nat → Nat)
3. We have met (→) and (×). What are their types? (Write down their typings.)
4. Complete (informally) the proof that we left incomplete in ⟦p. 14⟧. Note which of the uses and which of the attacks (on ⟦p. 12⟧) are missing from our table for us to complete the proof within our custom language.
5. In (∀x:α)[φ(x)] and (∃x:α)[φ(x)] what is the type of φ?

2026-03-03 (hw3)

• For each of the following “law”, come to a conclusion regarding its (constructive) validity. Prove enough of these to become fluent of how each of the uses/attacks work. Ask for help if you are stuck. Some ingredients are still missing, and we will develop them in Zulip (but I will not do this by myself). Warning: not all of these are provable, of course, this is one of the main points of this excercise! 👓
  1. Reflexivity of ⇒:
     1. P ⇒ P
  2. Transitivity of ⇒:
     1. ((P ⇒ Q) ∧ (Q ⇒ R)) ⇒ (P ⇒ R)
  3. Commutativity:
     1. (P ∨ Q) ⇒ (Q ∨ P)
     2. (P ∧ Q) ⇒ (Q ∧ P)
  4. Double negation
     1. P ⇒ ¬¬P
     2. ¬¬P ⇒ P
  5. Interdefinability of ⇒,∨:
     1. (P ⇒ Q) ⇒ (¬P ∨ Q)
     2. (P ⇒ Q) ⇐ (¬P ∨ Q)
     3. (P ∨ Q) ⇒ (¬P ⇒ Q)
     4. (P ∨ Q) ⇐ (¬P ⇒ Q)
  6. Contrapositive:
     1. (P ⇒ Q) ⇒ (¬Q ⇒ ¬P)
     2. (¬Q ⇒ ¬P) ⇒ (P ⇒ Q)
  7. Peirce’s law and its “weak” version:
     1. ((P ⇒ Q) ⇒ P) ⇒ P
     2. ((P ⇒ Q) ⇒ P) ⇒ ¬¬P
  8. Interdefinability of ∨,∧:
     1. P∨Q ⇒ ¬(¬P∧¬Q)
     2. P∨Q ⇐ ¬(¬P∧¬Q)
     3. P∧Q ⇒ ¬(¬P∨¬Q)
     4. P∧Q ⇐ ¬(¬P∨¬Q)
  9. De Morgan laws for ∨,∧:
     1. ¬(P∨Q) ⇒ (¬P ∧ ¬Q)
     2. ¬(P∨Q) ⇐ (¬P ∧ ¬Q)
     3. ¬(P∧Q) ⇒ (¬Q ∨ ¬P)
     4. ¬(P∧Q) ⇐ (¬Q ∨ ¬P)
  10. Distributivity of ∨,∧:
      1. P∧(Q∨R) ⇒ (P∧Q)∨(P∧R)
      2. P∧(Q∨R) ⇐ (P∧Q)∨(P∧R)
      3. P∨(Q∧R) ⇒ (P∨Q)∧(P∨R)
      4. P∨(Q∧R) ⇐ (P∨Q)∧(P∨R)
  11. Currying
      1. ((P∧Q)⇒R) ⇒ (P⇒(Q⇒R))
      2. ((P∧Q)⇒R) ⇐ (P⇒(Q⇒R))
  12. De Morgan laws for ∃,∀:
      1. ¬(∀x)[φ(x)] ⇒ (∃x)[¬φ(x)]
      2. ¬(∀x)[φ(x)] ⇐ (∃x)[¬φ(x)]
      3. ¬(∃x)[φ(x)] ⇒ (∀x)[¬φ(x)]
      4. ¬(∃x)[φ(x)] ⇐ (∀x)[¬φ(x)]
  13. Interdefinability of ∃,∀:
      1. (∃x)[φ(x)] ⇒ ¬(∀x)[¬φ(x)]
      2. (∃x)[φ(x)] ⇐ ¬(∀x)[¬φ(x)]
      3. (∀x)[φ(x)] ⇒ ¬(∃x)[¬φ(x)]
      4. (∀x)[φ(x)] ⇐ ¬(∃x)[¬φ(x)]
  14. Distributivity of ∃,∀:
      1. (∃x)[φ(x) ∧ ψ(x)] ⇒ (∃x)[φ(x)] ∧ (∃x)[ψ(x)]
      2. (∃x)[φ(x) ∧ ψ(x)] ⇐ (∃x)[φ(x)] ∧ (∃x)[ψ(x)]
      3. (∃x)[φ(x) ∨ ψ(x)] ⇒ (∃x)[φ(x)] ∨ (∃x)[ψ(x)]
      4. (∃x)[φ(x) ∨ ψ(x)] ⇐ (∃x)[φ(x)] ∨ (∃x)[ψ(x)]
      5. (∀x)[φ(x) ∧ ψ(x)] ⇒ (∀x)[φ(x)] ∧ (∀x)[ψ(x)]
      6. (∀x)[φ(x) ∧ ψ(x)] ⇐ (∀x)[φ(x)] ∧ (∀x)[ψ(x)]
      7. (∀x)[φ(x) ∨ ψ(x)] ⇒ (∀x)[φ(x)] ∨ (∀x)[ψ(x)]
      8. (∀x)[φ(x) ∨ ψ(x)] ⇐ (∀x)[φ(x)] ∨ (∀x)[ψ(x)]
  15. Law of excluded middle and its so-called irrefutability:
      1. P ∨ ¬P
      2. ¬¬(P ∨ ¬P)

2026-03-07 (hw4)

1. Are the notions of stable and decidable comparable?
2. Prove that even though we cannot cancel 2 negations in ¬¬P, we can reduce 3 negations to 1:
   1. ¬¬¬P ⇔ ¬P
3. About (=): show transitivity and symmetry
4. Consider the following magic command: ⛤ LEM[P]. which, invoked on any proposition P gives you P ∨ ¬P. Using it show how to prove all the propositions of hw3.1 that are unprovable without “magic”.
5. Consider the following magic commands: ⛤ RAA. (Reductio Ad Absurdum), which can be executed at any time in a proof with state Γ ⊢ G and its effect is to transform the state to Γ, ¬G ⊢ ⊥; and ⛤ LDN[P]. (Law of Double Negation) which, invoked on any proposition P, gives you ¬¬P ⇒ P. Meta-show that adding any of these commands as a primitive to our working system, we can define the other two as macros/syntactic-sugar. (In other words, the three (LEM, LDN, RAA) are inter-inferrable.)
6. Are LEM and LDN equivalent?
7. Does your answer to the previous exercise contradict your answer to the first exercise?
8. ⟨2026-03-08⟩ Figure out how the Compute: mode we have been using so far (as if it was primitive) can be seen as convenient sugar for using and attacking equalities (so that it all boils down to refl and substitution). In other words: if I take away the Compute command it will only by a matter of comfort, not a matter of provability: any prove we have that uses Compute can be mechanically rewritten to a proof that doesn’t.

2026-03-18 (hw5)

1. Install Lean 4; then post an honest «I have a working Lean on my system.» on #meta-tt > Working Lean.
2. Prove the laws of the arithmetic of types that we have mentioned in class (pink hw).
3. Stipulate other laws you claim to be valid and prove them.
4. Can you find a law of elementary arithmetic that is not valid here? What about the converse?
5. Can you find a corresponding notion of (≤) among types? Does it play nicely with arithmetic?
6. Finding 1-ary versions of binary concepts or laws is usually trivial. 0-ary require some thought. Investigate 0-ary versions for the following concepts/laws:
   1. disjunction
   2. conjunction
   3. implication (Hint: does it have an identity? How about the 0-ary version of a^(u·v) = (a^v)^u?)
   4. of which law is a⁰ = 1 the 0-ary version?
7. We left (+) without: Elimination, (β), (η). Figure them out (in this order) and suggest notation for your idea.

2026-03-26 (hw6)

1. Show that both idempotence laws follow from the rest of the a-lattice laws.
2. In a poset 𝒫, investigate ⋁P, ⋀P, ⋁Ø, ⋀Ø. (⋁, ⋀ are lub and glb, respectively.)
3. Θ. monotonicity (isotonicity) of (∨) and (∧)
4. Θ. (∧) distributes over (∨) ⇔ (∨) distributes over (∧)
5. Θ. A proset that has all meets, also has all joins
6. Can you find a non-distributive lattice? Try first with: 0, 1, 2, … elements so that you have a minimal example.
7. Let L, K be lattices, and f : L → K an order-preserving map. Does f necessarily respect (∨) and (∧)? Investigate.
8. Let f : 𝒫 → 𝒬. (Remeber: this means that f preserves (≤).) Show that if f reflects (≤), then it is injective. What about the converse?
9. Group theory ▸ Let 𝒢 : Group. Does the set of all subgroups of 𝒢 form a lattice? What about all normal subgroups?

2026-03-27 (hw7)

1. Embrace pointless™ definitions and tacit programming (also check pointfree.io). Give point-free definitions for:
   1. f (n,m) ≝ (n + m)²
   2. f (n,m) ≝ n² + 2nm + m²
   3. f n ≝ n(n²+1) + 5
2. Describe pictorially the constructions of: 𝐧, 𝐧̄, (+), (⊕), (×ᶜʷ), (⊗ˡᵉˣ), (⊗ᵃⁿᵗⁱˡᵉˣ)
3. Come up with laws about the constructions on p(r)osets that we met so far, and prove them.
4. We call a subset D a downset iff D is closed downwards: (∀d∈D)(∀x≤d)[x ∈ D] Let 𝒪(𝒫) be the collection of all downsets of a poset 𝒫. Equip it with the obvious(?) order and show that it is itself a poset. Thus we have one more construction on posets: 𝒪(–).
5. Consider the posets: ᛞ, N. Draw 𝒪(ᛞ) and 𝒪(N).
6. State what (≅) should mean among posets. Then prove/refute/show-independence of:
   1. 𝒪(P⊕1) ≅ 𝒪(P) ⊕ 1
   2. 𝒪(1⊕P) ≅ 1 ⊕ 𝒪(P)
   3. 𝒪(P + Q) ≅ 𝒪(P) × 𝒪(Q)
7. Express using commutative diagrams the following ideas/laws:
   1. the commutativity of a group (a group is abelian iff such diagram commutes)
   2. φ is a group homomorphism (three diagrams, we did two in class)
   3. the group laws (three diagrams)
   4. the idempotency of a binary operation (like (∧))

2026-03-31 (hw8)

1. How would you define 𝟛? 𝕟?
2. Verify that all examples of cats we have seen, are indeed cats.
3. For each of the math-structure ones, see if you can get different categories by just changing the concept of arrow, but keeping the same collection of objects.
4. ⟨2026-04-01⟩ What is the Set, Magma, Semigroup, Monoid, Group, Lattice, Bounded Lattice freely generated by {a}?
5. ⟨2026-04-01⟩ What is the Semigroup, Monoid, Lattice greely generated by {a,b}?
6. ⟨2026-04-01⟩ What is the Lattice freely generated by {a,b,c}?

2026-04-05 (hw9)

1. State “uniqueness” for terminal objects and prove it. (Draw a diagram!)
2. State “uniqueness” for products and prove it. (Draw a diagram!)
3. Look in all categories we have met so far to identify the categorial concepts we have defined. Are they guaranteed? Do they correspond to some notion you already know?
4. What is the best way to prove split epi ⇒ epi?
5. Show that:
   1. mono & split epi ⊢ iso
   2. split mono & epi ⊢ iso
6. Can you find categories that show that:
   1. mono ⊬ split mono
   2. epi ⊬ split epi
   3. mono & epi ⊬ iso

2026-04-27 (hw10)

1. How would you define the following categorial constructions?:
   1. Given any cat ℂ, the category ℂ ⃗ that has as objects the arrows of ℂ.
   2. Given any cat ℂ and any object C : ℂ₀, the “over” category of arrows of ℂ that point to C. We denote this by ℂ/C or ℂ↓C.
   3. Similarly, the under category C/ℂ or C↓ℂ.
2. Define a cat where objects are natural numbers and arrows are matrices.
3. Come up with a good answer to the following question: how do we get from one cat to another? (In other words: what should be the arrows in a cat of cats?)

2026-05-01 (hw11)

1. Θ. (safe-distr) In any lattice, the following hold:
   1. x∧(y∨z) ≥ (x∧y)∨(x∧z)
   2. x∨(y∧z) ≤ (x∨y)∧(x∨z)
2. Θ. (safe-modul) In any lattice, the following holds:
   • x ≤ z ⇒ x∨(y∧z) ≤ (x∨y)∧z
3. D. A lattice is modular iff x ≤ z ⇒ x∨(y∧z) = (x∨y)∧z. D. A lattice is distributive iff (∨) distributes over (∧) and (∧) distributes over (∨).
   1. Prove/refute: In any lattice: (∨) distributes over (∧) ⇒ (∧) distributes over (∨)
   2. Prove/refute: In any lattice: (∨) distributes over (∧) ⇐ (∧) distributes over (∨)
   3. Prove/refute: For any lattice L: L modular ⇒ L distributive
   4. Prove/refute: For any lattice L: L modular ⇐ L distributive
4. Come up with a good answer to the following questions:
   1. How do we get from a functor to another (of the same type)? (In other words: Can we form a category whose objects are functors from ℂ to 𝔻?)
   2. (How) can we compose natural transformations? (Draw a picture!)
5. ⟨2026-05-02⟩ Prove the following mysterious lemmas:
   1. in any proset: (∀x)[x ≤ a ⇒ x ≤ b] ⇔ a ≤ b
   2. in any poset: (∀x)[x ≤ a ⇔ x ≤ b] ⇔ a = b
6. ⟨2026-05-02⟩ In any HA: c ∧ a ≤ b ⇔ c ≤ a ⊃ b (Here a ⊃ b denotes the exponential bᵃ.)
7. ⟨2026-05-04⟩ We have defined the diagonal arrow Δ : α → α×α. Dualizing it the concept we obtain is denoted by ∇. What is its type, its categorial definition, and how does it manifest it self in 𝐓𝐲𝐩𝐞?
8. ⟨2026-05-05⟩ Prove/refute: In any lattice: (∀a,b,c)[ d ∨ (a ∧ b) = (d ∨ a) ∧ (d ∨ b) ⇒ d ∧ (a ∨ b) = (d ∧ a) ∨ (d ∧ b) ]
9. ⟨2026-05-05⟩ Prove/refute: In any lattice: (∀a,b,c)[ d ∨ (a ∧ b) = (d ∨ a) ∧ (d ∨ b) ⇐ d ∧ (a ∨ b) = (d ∧ a) ∨ (d ∧ b) ]

2026-05-08 (hw12)

1. Verify whether each of the following is a functor (from where to where?), and decide if it is covariant or contravariant:
   1. (–)ᵒᵖ
   2. (–) ⃗
   3. (ℂ ↓ –)
   4. (– ↓ ℂ)
2. What is a functor from ℂ[𝒫] to ℂ[𝒬]?
3. What is a functor from ℂ[ℳ] to ℂ[𝒩]?
4. Investigate the new categorial constructions:
   1. When does a each of them have a terminal, an initial?
   2. When does a each of them have (co)products?
   3. What about special arrows like monos, split monos, epis, split epis?

2026-05-16 (hw13)

1. Functional programming ▸ Define a polymorphic function of type M α → L α and verify its naturality (see the commutative diagrams in ⟦p. 154⟧).
2. Functional programming ▸ If polymorphic functions end up being natural transformations between functors, what about functions of (polymorphic) types like repeat : α → L α or length : L α → Nat? If they are natural transformations what are their domain and codomain Functors?
3. We have seen how an element of the type a | b is a pair of an integer (the witness) and of a proof of the equality that establishes that such witness is valid. Which means that we need to construct an element-proof of an Id type. Think: how do/should we construct inhabitants of a type like Id_A a b (aka a =A b)?
4. Similarly in defining an element-proof of trans-| we ended up having access to some equations (named eab and ebc in ⟦p. 157⟧). How do/should we use such things?
5. Find a way to define inverses in the absence of units (identity). In this way, we discover an alternative path to reaching groups from semigroups: instead of adding identity first and then inverses, we may add inverses first, and then identity.
6. Let X be a carrier, (◦) and (•) binary operations on X. Suppose that: (i) (◦) unital; (ii) (•) unital; (iii) (a ◦ b) • (c ◦ d) = (a • c) ◦ (b • d). Prove: (◦) and (•) share the same unit, are in fact the same binary operation ((•)=(◦)), which must also be commutative and associative.

2026-05-19 (hw14)

1. Play the Natural Numbers Game (or some other that appeals more to you) on the Lean Game Server. Share your progress/woes on Zulip!
2. Use git to clone Glimpse of Lean, load Glimpse of Lean on VS Code, and play around! Share your progress/woes on Zulip!
3. ⟨2026-05-20⟩ Go back to the list of hw3 and prove all provable propositions by constructing an inhabitant of the corresponding type. How many different proofs can you find for P ∨ P ⇒ P ∧ P? What about P ∧ P ⇒ P ∨ P?
4. ⟨2026-05-20⟩ Do the same but now using lean tactics: download and “solve” Logic.lean. (See also the Lean FAQ for help.)

2026-05-26 (hw15)

1. Finish the definition of Group Object (provide the missing diagrams that correspond to the rest of the group laws).
2. Prove that the Group Objects of 𝐆𝐫𝐨𝐮𝐩 are the commutative groups (aka abelian) and that the Group Objects of 𝐀𝐛𝐞𝐥 are all of its objects.
3. ⟨2026-05-27⟩ Prove that the exp.does rule can be used as a two-way rule, i.e., in a HA prove: c ≤ bᵃ ⊢ c ∧ a ≤ b.
4. ⟨2026-05-27⟩ We proved the not-guaranteed half d ∧ (a ∨ b) ≤ (d ∧ a) ∨ (d ∧ b). What about the other not-guaranteed half?: (d ∨ a) ∧ (d ∨ b) ≤ d ∨ (a ∧ b)? Resolve this in two different ways: (i) in a similar way to what we did; (ii) by remembering/(re)solving hw11.3
5. ⟨2026-05-27⟩ Let A be a set and let ℱ be the monoid defined as the set of all strings formed from the alphabet A (concatenation is the binary operation, the empty string is the identity). Show that ℱ satisfies the universal property of the free monoid. Do the same for the definition of free group usually encountered in introductory algebra books.
6. ⟨2026-05-27⟩ For any m : ℤ define the binary relation on integers (≊ₘ) by: a ≊ₘ b ⇚def⇛ m | b - a. (Notice that we have defined a ℤ-family of relations.) Prove that (≊ₘ) is a congruence, i.e., (≊ₘ) is an equivalence relations that is compatible with the operations (in this case the operations are the 5 ring operations), i.e., the operations take (≊ₘ)-equivalent inputs to (≊ₘ)-equivalent outputs. Notice what this means: we can lift all these operations on the level of congruence classes.
7. ⟨2026-05-27⟩ Define the proset of all such congruences / congruence classes. Is it a lattice? Which (further) properties does it satisfy?
8. ⟨2026-05-27⟩ Are these all of the congruences on ℤ? In other words, prove/refute the following: «Let (≈) be a congruence relation on ℤ. Then there exists an m : ℤ such that (≈) = (≊ₘ).»

Log

Blackboards

• Blackboards PDF: lecs 01–21 (Last update: 2026-05-28)

2026-02-24: (1) Introduction [video]

• A map of the chaotic land of interest
  • (Computational) Trinitarianism
  • Type theory
  • Foundations (for mathematics)
  • Formalization
  • Proof theory
  • Category theory
  • Order theory
  • Programming
  • λ-calculus
  • Constructive mathematics
  • Specification – Implementation
• Sets – Types
• Intension – Extension
• (=), (≡), (≝), (⇔), (⇚⇛), …
• ($=_\alpha$), ($\in_\alpha$), ($\subseteq_\alpha$)
• ℕ ↪ℤ ↪ ℚ ↪ ℝ ↪ ℂ
  • type coercion
• Some invisible mathematics
• Specification – Implementation
  • Implementation-agnostic
• Typing statements
  • (→)
  • (×)
• Holes
• Currying

2026-02-27: (2) Intro/Language/Proofs [video]

• A bit more typing
• What counts as a proof for a conjunction? For an implication?
• Developing a language for proofs
• Cmd – Prop

2026-03-03: (3) Language for proofs [video]

• Further developing a language for proofs
• Defining (⇐) and (⇔)
• Defining (¬) and the notion of (⊥)
• Bound vs free “variables”
• Since P, thence Q. vs if P then Q
• Compute notation for using equations.
• Labels should not be restricted to being numbers; use meaningful/indicative names
• Proof-relevance and constructive mathematics
• Math as if humans matter: the meaning of the judgement A true
• Proving logical so-called “laws”
  • P ⇒ P
  • (P ∨ Q) ⇒ (Q ∨ P)
• LEM

2026-03-06: (4) Language for proofs [video]

• About double negation
  • ⊢ P ⇒ ¬¬P
  • it seems that: ⊬ ¬¬P ⇒ P
• About LEM
  • ⊢ ¬¬(P ∨ ¬P)
  • it seems that: ⊬ P ∨ ¬P
• stable and decidable propositions
• the compatibility of constructivism with so-called “classical” mathematics
• saving proofs and what your options are when you come across a use of LEM in a proof
• Inference rule notation and two ways to read it (↓ and ↑)
• About equality: what we expect, how to use it, how to attack it
• Justifying «apply the same function on both sides of the equation»
• transitivity and symmetry of (=) as derivable properties

2026-03-10: (5) Functions, inductive types [video]

• What does a derivation tree show/defend/establish?
• f vs f(x)
• fight for functions’ equal rights: anonymous functions, λ notation 🎉, (↦)
• (↦) vs (→)
• Defining functions directly vs indirectly
• (internal) operations vs (external) constructions
• Syntactic settings:
  • Syntactic associativity (vs. associativity)
  • Syntactic precedence
  • Syntactic default op by juxtaposition
• Functions: notation
• Types: formation rules, introduction rules, eliminations rules, (β), (η)
• Defining (×): (×)-F, (×)-I, (×)-E₁, (×)-E₂, (×)-β, (×)-η
• β, η for sets
• Hello Nat: three different ways to present the type Nat
  • listing rules
  • listing constructors
  • listing forms

2026-03-13: (6) [video]

• (partially) establishing (α × β) → ɣ ≅ α → β → ɣ
• different psychological value of equivalent definitions of a function: (to lambda or not to lambda?)
• (partially) establishing (α × β) → ɣ ≅ α → β → ɣ
• The choice of definition among equivalent ones matters
• Group and related definitions
  • why most definitions won’t even “compile”
  • who are the protagonists of a structure is part of what this structure is (and what its theory is about)
• More economic definitions are better, right? (No.)
  • Elegant and succint is good, but do not be a miser
  • The correct definition is one that captures and communicates the essense of the concept you are defining
  • a group homomorphism must respect three things
  • appreciate and use criteria
  • monomorphism does not mean injective homomorphism
• What is an algebraic (equational) theory?
  • this is a theorem: Herstein’s group theory is an algebraic theory
  • this is also a theorem (sorry): field theory is not an algebraic theory
  • this is also a theorem (sorry): if you require 0≠1 to be part of the definition of a ring, it is no longer an algebraic theory
• First steps to understanding what induction is: liberating it from the ℕ influence
• Hello Bools!
  • how to construct (I)
  • how to use (E)
  • how to compute and uniqueness (β & η)

2026-03-17: (7) [video]

• Gentzen’s natural deduction
• some proof theory for (∧),(⊃),(⊥),(⊤),(∨)
  • the judgements: A prop, A true
• Proofs compute!
• What is the so-called void of popular programming languages?
• Empty type (aka 𝟘)
• Unit type (aka 𝟙)
• arithmetic of types
• Propositions – Types
• Still missing: ∀,∃,=
• 🤢 Ugly mess for 15’—be glad if you missed this

2026-03-20: (8) [video]

• (+)-E (having functions)
  • match … with … (also: case … of …)
  • the [·|·] and {:] notations
• (+)-β, (+)-η
• Type families / dependend types
• Hello Π: (Π)-F, (Π)-I, (Π)-E & notation
• Hello Σ: (Σ)-F, (Σ)-I, (Σ)-E & notation
• Special cases of Σ, Π: obtaining (+),(×),(→)
• Functions for free: infer-the-obvious-function challenge
• The entailment (⊢) from an order-theoretic perspective
• structural properties: Weakening, Contraction, Permutation
• meets and joins; tops and bottoms
• (ℤ ; |) as a proset

2026-03-24: (9) [video]

• re-analyzing an example: gcd(12,18)
• warning: non-(=) dressed up as (=): d = gcd(a,b); ℓ = limₙ (aₙ)ₙ; etc.
• P(r)osets
• R-preserving, R-reflecting
• o-lattice ⇄ a-lattice
• kernel of a function f : A → B

2026-03-27: (10) BHK; Pointless; Commutative Diagrams; P(r)osets [video]

• proof-relevance; proof-objects/witnesses; propositions-as-types
  • term construction: direct vs indirect (tactics)
• BHK interpretation
• point-free style (tacit programming)
• Functions for free: (×) as a construction on functions
• Commutative diagrams ♥
• constructions on p(r)osets
  • (–)ᵒᵖ
  • (_ ⨯ᶜʷ _) ; (_ ⊗ˡᵉˣ _) ; (_ ⊗ᵃⁿᵗⁱˡᵉˣ _)
  • (_ + _)
  • 𝐧 ; 𝐧̄

2026-03-31: (11) 🐱 BabyCats [video]

• What is a category: data (interface) and laws
• Subsingletons
• Benefits of a thin categories
• Examples:
  • 𝟘, 𝟙, 𝟚, 𝟚̅, …
  • Categories of mathematical structures:
    • 𝐌𝐚𝐠𝐦𝐚, 𝐒𝐞𝐦𝐢𝐠𝐫𝐨𝐮𝐩, 𝐌𝐨𝐧𝐨𝐢𝐝, 𝐆𝐫𝐨𝐮𝐩, 𝐀𝐛𝐞𝐥, 𝐑𝐢𝐧𝐠, …
    • 𝐏𝐫𝐨𝐬𝐞𝐭, 𝐏𝐨𝐬𝐞𝐭, 𝐋𝐚𝐭𝐭𝐢𝐜𝐞, 𝐁𝐝𝐋𝐚𝐭𝐭𝐢𝐜𝐞, 𝐓𝐨𝐩, 𝐒𝐞𝐭, 𝐅𝐢𝐧𝐒𝐞𝐭, 𝐒𝐞𝐭𝐈𝐧𝐣, …
  • ℂ[𝒫] : Proset → Cat
  • ℂ[ℳ] : Monoid → Cat

2026-04-03: (12) 🐱 BabyCats: categorial definitions [video]

• categorial definitions
• duality
• terminal, initial
  • in 𝟙, 𝟚, (ℤ;≤), (ℤ;|), ℂ[𝒫], 𝐒𝐞𝐭
• universal properties
• isomorphic objects; iso f : A ⥲ B
• “uniqueness”
• products and coproducts (sums)
  • in (ℤ;|), (℘A;⊆), 𝐒𝐞𝐭
• point-freeing injectivity
• point-freeing membership (∈)
• special arrows: mono, epi, split mono, split epi
  • split mono ⇒ mono

2026-04-21: (cancelled)

2026-04-24: (13) 🐱 BabyCats [video]

• Unique up to unique isomorphisms
• Uniqueness of terminals, initials, products, coproducts
• Spans ℂ[A←•→B]
• writing proofs, chasing diagrams, back to school

2026-04-28: (14) 🐱 BabyCats ; HA [video]

• Null objects
• Functors
• Natural transformations
• Proof theory: (⊃): Introduction and Elimination
• Order theory: (⇒): exponentials in (semi)lattices

2026-05-05: (15) 🐱 BabyCats [video]

• Distributivity
• Modularity
• Σ-actions
• The exemplar ring End(𝒜)

2026-05-08: (16) 🐱 BabyCats [video]

• Actions and modules and vector spaces Are Just™ …
• over and under category: ℂ↓C and C↓C
• arrow category ℂ ⃗
• 𝐂𝐚𝐭
• More on Natural Transformations
• implementing Maybe α as α + 𝟭
• Significance of names of arrows/functions
• Two computational interpretations of Lists

2026-05-12: Exam

2026-05-15: (17) Type theory [video]

• Natural transformations vs functors (in programming)
• Predicates as families of types
• Σ, Π for ∀, ∃
• The type Id of identifications
• Naming projections
• Defining algebraic structures as Σ-types

2026-05-19: (18) Lean [video]

• Getting started with Lean and VS Code.
• Hands-on: Glimpse of Lean.

2026-05-22: (19) Lean; Cats

• More (lean with) Glimpse of Lean
• Some useful Lean options
  • set_option pp.parens true
  • set_option autoImplicit false
• Forgetful functors
• teaser: free groups, monoids, lattices

2026-05-26: (20) Abstract Nonsense™; ℕ-Induction

• functors ℂ[𝒫] → ℂ[𝒬]
• functors ℂ[ℳ] → ℂ[𝒩]
• groupoids and oidification
• Group Objects and Groups(ℂ)
• Natural Numbers Object (NNO)
• Polynomial functors and initial F-algebras
• From non-dependent recursion to dependent (recursion/induction)

2026-05-27: (21) Loose ends and teasers

• exponentials and distributivity
• teaser: free(ly generated)
• teaser: galois connections
• teaser: (=) as an omnicompatible congruence
• what is a congruence?

Future (fluid)