Type Theory

Posts

HEq and Axiom K: An Exploration in Lean
February 23, 2026

berberman
- Lean
- Type Theory
8 min read
While reading A Few Constructions on Constructors¹, I came across this definition of Heterogeneous Equality (represented here using Lean axioms):
Read more