Contents

This book introduces type theory, theorem proving, and mathematical foundations using Lean 4. It progresses systematically from basic type-theoretic concepts to advanced topics in category theory and homotopy type theory.

1. Lean

• Setup
• Naming Conventions
• Types & Data structures
• Functions
• Algorithms
• Modules and projects
• Debugging

2. Type Theory

• Introduction
• Universes and families
• Relations
• Equality
• Operations
• Products & Co-products
• Function Types
• Identity Types

3. Theorem Proving

• Introduction
• Strategies & Tactics

4. Logic and Boolean Algebra

• Introduction
• Boolean Algebra
• Equality
• Laws of Logic
• Decidability
• System F

❌ WIP - (Re-)Work in Progress ❌

5. Abstract Algebras

• Introduction
• Sets in Type Theory

5.1 Orders

• Ordered objects

5.2 Groups

• Groups and family
• Groups and family 2
• Group Morphisms

5.3 Rings

• Rings and family
• Rings and family 2
• Ring Morphisms

5.4 Fields

• Fields and family
• Fields and family 2
• Field Morphisms
• Numbers

-1. Agda [outdated]

• Setup
• Naming Conventions
• Data Structures
• Functions
• Modules, Records and Postulates
• Debugging

6. Category Theory

• Introduction
• Categories
• Morphisms
• Functors
• Natural Transformation
• Yoneda Lemma
• Limits and Co-Limits
• Adjunctions
• Ends and Co-Ends
• Kan Extensions

7. Homotopy Type Theory

• Introduction
• Identity Types and Paths
• Connected spaces
• The Univalence Principle
• The Fundamental Group and Groupoid
• Cubical Type Theory

8. Algebraic Topology

• Introduction
• Topology

Extras

α. Applied Type Theory

• Introduction
• Gödel’s T
• System F
• Bitcoin
• Verified Programming
• Binding with the outside world

Γ. Higher Category Theory

Δ. Topos Theory

ψ. Higher Topos Theory

Go up Gitlab Github

Up