I think it is due to the homotopy type theory book. There is an elegant connecti...

		hkopp on Sept 28, 2023 \| parent \| context \| favorite \| on: RZK: Experimental proof assistant for synthetic ∞-... I think it is due to the homotopy type theory book. There is an elegant connection between category theory and type theory. I guess most of the people submitting category theory to hacker news (or any graduate math) just do it to flex and seem clever.

Actually, category theory, type theory, and proof theory.